Note [Representation polymorphism invariants]
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. References 5
- Linting representation-polymorphic builtins GHC.Core.Lint
- Invariants on join points GHC.Core
- Fixed RuntimeRep GHC.Tc.Utils.Concrete
- Representation polymorphism checking GHC.Tc.Utils.Concrete
- Representation-polymorphism checking built-ins GHC.Tc.Utils.Concrete
Referenced by 25
- GHC.Core call site ×3
- GHC.Core.Lint call site ×2
- Concrete overview GHC.Tc.Utils.Concrete ×2
- Return arguments with a fixed RuntimeRep GHC.Tc.Utils.Unify ×2
- Primop wrappers GHC.Builtin.PrimOps
- Linting representation-polymorphic builtins GHC.Core.Lint
- Checking for representation polymorphism GHC.Core.Lint
- GHC.Core.Opt.Arity call site
- GHC.Core.Opt.SetLevels call site
- GHC.Core.Opt.Simplify.Iteration call site
- Eliminate casts in function position GHC.Core.SimpleOpt
- GHC.Core.Unfold.Make call site
- Eta-expanding rep-poly unlifted newtypes GHC.Tc.Gen.App
- Typechecking data constructors GHC.Tc.Gen.Head
- GHC.Tc.Types.Evidence call site
- Representation polymorphism checking GHC.Tc.Utils.Concrete
- Fixed RuntimeRep GHC.Tc.Utils.Concrete
- Representation-polymorphic Ids with no binding GHC.Tc.Utils.Concrete
- FunTy vs FunTy case in tc_sub_type_deep GHC.Tc.Utils.Unify
- GHC.Types.Id.Make call site