eqType fails on comparing FunTys
Suppose I have
co :: IntRep ~ r and
a :: TYPE IntRep. Consider
t1 = a -> () and
t2 = (a |> TYPE co) -> (). We have
t1 `eqType` t2, but if we call
t2, we'll get different arguments (the first arg in
t1 will be
IntRep while the first arg in
t2 will be
r). This violates property EQ of Note [Non-trivial definitional equality] in TyCoRep.
The fix is easy: in
FunTy case should recur into
nonDetCmpTypeX for both argument and result. This does a kind check. Recurring into
go skips the kind check.
Unfortunately, there are other places that also work with equality. This list includes at least
Pure unifier in
Unify, which probably also needs to recur in kinds on a
FunTy. Or maybe this works via decomposition into a
TyConApp, so all is OK. But it needs to be checked.
I believe Simon has some preliminary work on a branch.