opt_univ is fishy for non-injective TyConApps
opt_univ env sym prov role oty1 oty2 | Just (tc1, tys1) <- splitTyConApp_maybe oty1 , Just (tc2, tys2) <- splitTyConApp_maybe oty2 , tc1 == tc2 , equalLength tys1 tys2 -- see Note [Differing kinds] -- NB: prov must not be the two interesting ones (ProofIrrel & Phantom); -- Phantom is already taken care of, and ProofIrrel doesn't relate tyconapps = let roles = tyConRolesX role tc1 arg_cos = zipWith3 (mkUnivCo prov') roles tys1 tys2 arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos in mkTyConAppCo role tc1 arg_cos'
UnivCo proving equality of two
TyConApps where the heads are the same, this assumes that we can push the coercion inside and equate the arguments. But that only holds for injective type constructors! So we can have something like
type family F x where F Int = Int F Bool = Int
and a perfectly legitimate
UnivCo :: F Int ~ F Bool will be turned into
F (UnivCo :: Int ~ Bool) which seems rather fishy.
I'm not aware of a way to actually make this break anything. But it confused me when working on another patch, because I was getting perfectly sensible coercions with
-ddump-ds-preopt that turned into nonsense with
-ddump-ds. I have a (tiny) fix.