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 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.