GitLab

Required reading: Note [The Purely Kinded Type Invariant (PKTI)] and Note [mkAppTyM], both in TcHsType.

The PKTI has at least two problems.

1. Suppose we have the type a -> b stored in ty. If we say splitTyConApp ty, we should expect to get (funTyCon, [r1, r2, a, b]) where a :: TYPE r1 and b :: TYPE r2. But what if a doesn't have type TYPE r1 or b doesn't have type TYPE r2? This can happen if, say, a :: kappa and kappa := TYPE r1, but we haven't zonked. The PKTI must address this. This means that we will have to write mkFunTyM just like mkAppTyM. We might even need mkTyConAppM to handle the case when the tycon is (->). :(

2. Nasty case 2 of Note [mkAppTyM] isn't sufficient. That case considers a type synonym. What about a type family?

   type family F (a :: Type -> Type) (b :: Type) where
     F a b = a b

   According to its current text of the PKTI, F (a :: kappa1) (b :: kappa2) satisfies the PKTI. Yet if we reduce this type family, a b does not satisfy the PKTI. Yet we sometimes reduce type families in a pure context (normaliseType) and, moreover, the main type-family-reduction engine in TcFlatten does not respect the PKTI in this case as it does rewriting. (Actually, it does, because the flattener zonks thoroughly. But we're exploring the possibility of not zonking as thoroughly in the future. And, in any case, there is no documented connection between the flattener's desire to zonk and the PKTI.)

With some plumbing, etc., I'm confident we can fix (1). But I really have no idea how to fix (2). I worry we will have to abandon the idea of pure reductions, and we'll have to teach the flattener to check for "tricky tvs" (see isTrickyTvBinder) much like mkAppTyM does. Or, we can abandon pure reductions and just keep the flattener zonking thoroughly. :)