The Purely Kinded Type Invariant (PKTI) is not good enough
Required reading: Note [The Purely Kinded Type Invariant (PKTI)]
and Note [mkAppTyM]
, both in TcHsType.
The PKTI has at least two problems.
-
Suppose we have the type
a -> b
stored inty
. If we saysplitTyConApp ty
, we should expect to get(funTyCon, [r1, r2, a, b])
wherea :: TYPE r1
andb :: TYPE r2
. But what ifa
doesn't have typeTYPE r1
orb
doesn't have typeTYPE r2
? This can happen if, say,a :: kappa
andkappa := TYPE r1
, but we haven't zonked. The PKTI must address this. This means that we will have to writemkFunTyM
just likemkAppTyM
. We might even needmkTyConAppM
to handle the case when the tycon is(->)
. :( -
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. :)