Note [Eta-expanding rep-poly unlifted newtypes]
Any occurrence of a newtype constructor must appear at a known representation. If the newtype is applied to an argument, then we are done: by (I2) in Note [Representation polymorphism invariants], the argument has a known representation, and we are done. So we are left with the situation of an unapplied newtype constructor. For example: type N :: TYPE r -> TYPE r newtype N a = MkN a ok :: N Int# -> N Int# ok = MkN bad :: forall r (a :: TYPE r). N (# Int, r #) -> N (# Int, r #) bad = MkN The difficulty is that, unlike the situation described in Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete, it is not necessarily the case that we simply need to check the instantiation of a single variable. Consider for example: type RR :: Type -> Type -> RuntimeRep type family RR a b where ... type T :: forall a -> forall b -> TYPE (RR a b) type family T a b where ... type M :: forall a -> forall b -> TYPE (RR a b) newtype M a b = MkM (T a b) Now, suppose we instantiate MkM, say with two types X, Y from the environment: foo :: T X Y -> M X Y foo = MkM @X @Y we need to check that we can eta-expand MkM, for which we need to know the representation of its argument, which is "RR X Y". To do this, in "rejectRepPolyNewtypes", we perform a syntactic representation- polymorphism check on the instantiated argument of the newtype, and reject the definition if the representation isn't concrete (in the sense of Note [Concrete types] in GHC.Tc.Utils.Concrete). For example, we would accept "ok" above, as "IntRep" is a concrete RuntimeRep. However, we would reject "foo", because "RR X Y" is not a concrete RuntimeRep. If we wanted to accept "foo" (performing a PHASE 2 check (in the sense of Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete), we would have to significantly re-engineer unlifted newtypes in GHC. Currently, "MkM" has type: MkM :: forall a b. T a b %1 -> M a b However, we should only be able to use MkM when we know the representation of T a b (which is RR a b). This means that MkM should instead have type: MkM :: forall {must_be_conc} a b (co :: RR a b ~# must_be_conc) . T a b |> GRefl Nominal (TYPE co) %1 -> M a b where "must_be_conc" is a skolem type variable that must be instantiated to a concrete type, just as in Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete. This means that any instantiation of "MkM", such as "MkM @X @Y" from "foo", would create a fresh concrete metavariable "gamma[conc]" and emit a Wanted constraint [W] co :: RR X Y ~# gamma[conc] However, this all seems like a lot of work for a feature that no one is asking for, so we decided to keep the much simpler syntactic check. Note that one possible advantage of this approach is that we should be able to stop skipping representation-polymorphism checks in the output of the desugarer; see (C) in Wrinkle [Representation-polymorphic lambdas] in Note [Typechecking data constructors].
References 5
- Representation polymorphism invariants GHC.Core
- Typechecking data constructors GHC.Tc.Gen.Head
- Concrete types GHC.Tc.Utils.Concrete
- Representation-polymorphism checking built-ins GHC.Tc.Utils.Concrete
- The Concrete mechanism GHC.Tc.Utils.Concrete
Referenced by 4
- GHC.Tc.Gen.App call site
- GHC.Tc.Gen.Head call site
- Representation-polymorphic Ids with no binding GHC.Tc.Utils.Concrete
- Representation-polymorphism checking built-ins GHC.Tc.Utils.Concrete