opt_univ is fishy for non-injective TyConApps
Take a look at https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/GHC/Core/Coercion/Opt.hs#L517:
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'
Given a UnivCo
proving equality of two TyConApp
s 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.