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