mkSelCo produces the wrong role
In GHC.Core.Coercion.mkSelCo we see
mkSelCo_maybe cs co
= assertPpr (good_call cs) bad_call_msg $
go cs co
where
Pair ty1 ty2 = coercionKind co
go cs co
| Just (ty, r) <- isReflCo_maybe co
= Just (mkReflCo r (getNthFromType cs ty)) <--------- Yikes!
...
Assigning role r
to the returned Refl is just wrong. It should be
go cs co
| Just (ty, r) <- isReflCo_maybe co
= Just (mkReflCo (mkSelCoResRole cs r) (getNthFromType cs ty))
where
mkSelCoResRole :: CoSel -> Role -> Role
-- What is the role of (SelCo cs co), if co has role 'r'?
-- It is not just 'r'!
-- c.f. the SelCo case of coercionRole
mkSelCoResRole SelForAll _ = Nominal
mkSelCoResRole (SelTyCon _ r') _ = r'
mkSelCoResRole (SelFun fs) r = funRole r fs
This came up when I was debugging something else, so I don't have a stand-alone reproducer.