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 splitTyConApp
on t1
and 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 nonDetCmpTypeX
, the 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
-
TcType.tc_eq_type
-
CoreMap
-
Pure unifier in Unify
, which probably also needs to recur in kinds on aFunTy
. Or maybe this works via decomposition into aTyConApp
, so all is OK. But it needs to be checked.
I believe Simon has some preliminary work on a branch.