Skip to content

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.

Edited by sheaf
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information