`Note [Equality on AppTys]` looks wrong
This Note says
Note [Equality on AppTys]
~~~~~~~~~~~~~~~~~~~~~~~~~
In our cast-ignoring equality, we want to say that the following two
are equal:
(Maybe |> co) (Int |> co') ~? Maybe Int
But the left is an AppTy while the right is a TyConApp. The solution is
to use splitAppTyNoView_maybe to break up the TyConApp into its pieces and
then continue. Easy to do, but also easy to forget to do.
But in GHC.Core.TyCo.Rep we see
Note [Respecting definitional equality]
...
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
ForAllTy to a ForAllTy.
It seems that (EQ1) means that the example in Note [Equality on AppTys]
isn't possible. After all:
Maybe :: Type -> Type
- So
co :: (Type->Type) ~ (k1 -> k2)
, for some kindsk1
andk2
- So
co
is decomposable - So (EQ1) does not hold
Question: is Note [Equality on AppTys]
needed? Is there another example to illustrate why we need splitAppTyNoView_maybe
in tcEqType
and friends?
@rae: this is a question for you!