Note [Concrete overview]

GHC/Tc/Utils/Concrete.hs:52 compiler

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

Referenced by 1