topNormaliseType is wrong
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
- 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
[Int], and then try reducing
(F [Int])!! That is totally bogus. Surely we should use (the role-aware)
- 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
LiftingContextis 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]