Note [Representation polymorphism invariants]

GHC/Core.hs:652 compiler

GHC allows us to abstract over calling conventions using **representation polymorphism**.
For example, we have:

  ($) :: forall (r :: RuntimeRep) (a :: Type) (b :: TYPE r). (a -> b) -> a -> b

In this example, the type `b` is representation-polymorphic: it has kind `TYPE r`,
where the type variable `r :: RuntimeRep` abstracts over the runtime representation
of values of type `b`.

To ensure that programs containing representation-polymorphism remain compilable,
we enforce the following representation-polymorphism invariants:

The paper "Levity Polymorphism" [PLDI'17] states the first two invariants:

  I1. The type of a bound variable must have a fixed runtime representation
      (except for join points: See Note [Invariants on join points])
  I2. The type of a function argument must have a fixed runtime representation.

Example of I1:

  \(r::RuntimeRep). \(a::TYPE r). \(x::a). e

    This contravenes I1 because x's type has kind (TYPE r), which has 'r' free.
    We thus wouldn't know how to compile this lambda abstraction.

Example of I2:

  f (undefined :: (a :: TYPE r))

    This contravenes I2: we are applying the function `f` to a value
    with an unknown runtime representation.

Note that these two invariants require us to check other types than just the
types of bound variables and types of function arguments, due to transformations
that GHC performs. For example, the definition

  myCoerce :: forall {r} (a :: TYPE r) (b :: TYPE r). Coercible a b => a -> b
  myCoerce = coerce

is invalid, because `coerce` has no binding (see GHC.Types.Id.Make.coerceId).
So, before code-generation, GHC saturates the RHS of 'myCoerce' by performing
an eta-expansion (see GHC.CoreToStg.Prep.maybeSaturate):

  myCoerce = \ (x :: TYPE r) -> coerce x

However, this transformation would be invalid, because now the binding of x
in the lambda abstraction would violate I1.

See Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete
and Note [Linting representation-polymorphic builtins] in GHC.Core.Lint for
more details.

Note that we currently require something slightly stronger than a fixed runtime
representation: we check whether bound variables and function arguments have a
/fixed RuntimeRep/ in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
See Note [Representation polymorphism checking] in GHC.Tc.Utils.Concrete
for an overview of how we enforce these invariants in the typechecker.