Skip to content

Incorrect role for multiplicity coercion in tyConAppFunCo_maybe

Currently we have:

tyConAppFunCo_maybe :: HasDebugCallStack => Role -> TyCon -> [Coercion]
                    -> Maybe Coercion
-- ^ Return Just if this TyConAppCo should be represented as a FunCo
tyConAppFunCo_maybe r tc cos
  | Just (af, mult, arg, res) <- ty_con_app_fun_maybe (mkReflCo r manyDataConTy) tc cos
            = Just (mkFunCo r af mult arg res)
  | otherwise = Nothing

The mkReflCo r manyDataConTy is wrong: the multiplicity argument to the function arrow TyCon has Nominal role. So we should never make a Representational coercion: it should be either Nominal or Phantom. This is what funRole r SelMult computes, so we should use that.

I ran into a Core Lint error due to this in the directed coercions patch on test T20231, but I don't have a reproducer on HEAD.

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