Unify wastes effort on casts
In GHC.Core.Unify the main unify_ty
function has signature
unify_ty :: UMEnv
-> Type -> Type -- Types to be unified and a co
-> CoercionN -- A coercion between their kinds
-- See Note [Kind coercions in Unify]
-> UM ()
That CoercionN
, called kco
in code, is derived from the idea in eqType
that we
are comparing types ignoring casts.
The point of this ticket is we do not know a single example where carrying kco makes unification succeed, where it would otherwise fail.
The simpler alternative is to have
unify_ty :: UMEnv
-> Type -> Type
-> UM ()
and code like
unify_ty env (CastTy ty1' co1) (CastTy ty2 co2)
| isReflexiveCo (co1 `mkTransCo` sym co2)
= = unify_ty env ty1' ty2' (co1 `mkTransCo` kco `mkTransCo` mkSymCo co2)
unify_ty env (Cast {}) ty2 = surelyApart
unify_ty env ty1 (Cast {}) = surelyApart
You might think this would not work on something like
f :: t1 -> t2
x :: t1
f x ~ ((f |> co1) (x |> co2)) |> co3
where
co1 :: t1 -> t2 ~ t3 -> t4
co2 :: t1 ~ t3
co3 :: t4 ~ t2
But that's ruled out by invariant (EQ1) in Note [Respecting definitional equality]
in GHC.Core.TyCo.Rep.
Similarly
(forall a. t1 |> co) ~ (forall a. t2) |> co2
is ruled out by (EQ4).