I’m very puzzled about topNormaliseTYpe_maybe. Here it is:

topNormaliseType_maybe env ty
  = topNormaliseTypeX stepper mkTransCo ty
  where
    stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper

    tyFamStepper rec_nts tc tys  -- Try to step a type/data family
      = let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
          -- NB: It's OK to use normaliseTcArgs here instead of
          -- normalise_tc_args (which takes the LiftingContext described
          -- in Note [Normalising types]) because the reduceTyFamApp below
          -- works only at top level. We'll never recur in this function
          -- after reducing the kind of a bound tyvar.

        case reduceTyFamApp_maybe env Representational tc ntys of
          Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
          _              -> NS_Done

I have two puzzlements

1. First, it seems utterly wrong to normalise the arguments using Representational. Consider

F (N Int)
where newtype N x = [x]

We don’t want to reduce (N Int) to [Int], and then try reducing (F [Int])!! That is totally bogus. Surely we should use (the role-aware) normalise_tc_args here?

1. I have literally no clue what Note [Normalising types] is all about. Moreover there is no Lifting Context passed to normalise_tc_args, so I don’t know what this stuff about LiftingContext is about. Is this historical baggage?

Richard and I discussed this. (1) is a bug; for (2) the comment is misleading and should be deleted.

Richard will do these things -- and will add examples to the mysterious Note [Normalising types]