Note [Eta-expanding rep-poly unlifted newtypes]

GHC/Tc/Gen/App.hs:2235 compiler

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

Referenced by 4