Note [Concrete overview]
GHC ensures that certain types have a fixed runtime representation in the
typechecker, by emitting certain constraints.
Emitting constraints to be solved later allows us to accept more programs:
if we directly inspected the type (using e.g. `typePrimRep`), we might not
have enough information available (e.g. if the type has kind `TYPE r` for
a metavariable `r` which has not yet been filled in.)
We give here an overview of the various moving parts, to serve
as a central point of reference for this topic.
* Representation polymorphism
Note [Representation polymorphism invariants] in GHC.Core
Note [Representation polymorphism checking]
The first note explains why we require that certain types have
a fixed runtime representation.
The second note details why we sometimes need a constraint to
perform such checks in the typechecker: we might not know immediately
whether a type has a fixed runtime representation. For example, we might
need further unification to take place before being able to decide.
So, instead of checking immediately, we emit a constraint.
* What does it mean for a type to be concrete?
Note [Concrete types] explains what it means for a type to be concrete.
To compute which representation to use for a type, `typePrimRep` expects
its kind to be concrete: something specific like `BoxedRep Lifted` or
`IntRep`; certainly not a type involving type variables or type families.
* What constraints do we emit?
Note [The Concrete mechanism]
Instead of simply checking that a type `ty` is concrete (i.e. computing
'isConcreteType`), we emit an equality constraint:
co :: ty ~# concrete_ty
where 'concrete_ty' is a concrete metavariable: a metavariable whose 'MetaInfo'
is 'ConcreteTv', signifying that it can only be unified with a concrete type.
The Note explains that this allows us to accept more programs. The Note
also explains that the implementation is happening in two phases
(PHASE 1 and PHASE 2).
In PHASE 1 (the current implementation) we only allow trivial evidence
of the form `co = Refl`.
* Fixed runtime representation vs fixed RuntimeRep
Note [Fixed RuntimeRep]
We currently enforce the representation-polymorphism invariants by checking
that binders and function arguments have a "fixed RuntimeRep".
This is slightly less general than we might like, as this rules out
types with kind `TYPE (BoxedRep l)`: we know that this will be represented
by a pointer, which should be enough to go on in many situations.
* When do we emit these constraints?
Note [hasFixedRuntimeRep]
We introduce constraints to satisfy the representation-polymorphism
invariants outlined in Note [Representation polymorphism invariants] in GHC.Core,
which mostly amounts to the following two cases:
- checking that a binder has a fixed runtime representation,
- checking that a function argument has a fixed runtime representation.
The Note explains precisely how and where these constraints are emitted.
* Reporting unsolved constraints
Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin
When we emit a constraint to enforce a fixed representation, we also provide
a 'FixedRuntimeRepOrigin' which gives context about the check being done.
This origin gets reported to the user if we end up with such an an unsolved Wanted constraint. References 7
- Representation polymorphism invariants GHC.Core
- Reporting representation-polymorphism errors GHC.Tc.Types.Origin
- Concrete types GHC.Tc.Utils.Concrete
- Fixed RuntimeRep GHC.Tc.Utils.Concrete
- hasFixedRuntimeRep GHC.Tc.Utils.Concrete
- Representation polymorphism checking GHC.Tc.Utils.Concrete
- The Concrete mechanism GHC.Tc.Utils.Concrete
Referenced by 1
- Representation polymorphism checking GHC.Tc.Utils.Concrete