Note [The Concrete mechanism]

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

To check (ty :: ki) has a fixed runtime representation, we proceed as follows:

  - Create a new concrete metavariable `concrete_tv`, i.e. a metavariable
    with 'ConcreteTv' 'MetaInfo' (see Note [ConcreteTv]).

  - Emit an equality constraint:

      ki ~# concrete_tv

    The origin for such an equality constraint uses
    `GHC.Tc.Types.Origin.FixedRuntimeRepOrigin`, so that we can report the
    appropriate representation-polymorphism error if any such constraint
    goes unsolved.

To solve `ki ~# concrete_ki`, we must unify `concrete_tv := concrete_ki`,
where `concrete_ki` is some concrete type. We can then compute `kindPrimRep`
on `concrete_ki` to compute the representation: this means `ty` indeed
has a fixed runtime representation.


PHASE 1 and PHASE 2 --


The Concrete mechanism is being implemented in two separate phases.

In PHASE 1, we enforce that we only solve the emitted constraints
`co :: ki ~# concrete_tv` with `Refl`. This forbids any program
which requires type family evaluation in order to determine that a 'RuntimeRep'
is fixed.
To achieve this, instead of creating a new concrete metavariable, we directly
ensure that 'ki' is concrete, using 'makeTypeConcrete'. If it fails, then
we report an error (even though rewriting might have allowed us to proceed).

In PHASE 2, we lift this restriction. This means we replace a call to
`hasFixedRuntimeRep_syntactic` with a call to `hasFixedRuntimeRep`, and insert the
obtained coercion in the typechecked result. To illustrate what this entails,
recall that the code generator needs to be able to compute 'PrimRep's, so that it
can put function arguments in the correct registers, etc.
As a result, we must insert additional casts in Core to ensure that no type family
reduction is needed to be able to compute 'PrimRep's. For example, the Core

  f = /\ ( a :: F Int ). \ ( x :: a ). some_expression

is problematic when 'F' is a type family: we don't know what runtime representation to use
for 'x', so we can't compile this function (we can't evaluate type family applications
after we are done with typechecking). Instead, we ensure the 'RuntimeRep' is always
explicitly visible:

  f = /\ ( a :: F Int ). \ ( x :: ( a |> kco ) ). some_expression

where 'kco' is the appropriate coercion; for example if `F Int = TYPE Int#`
this would be:

  kco :: F Int ~# TYPE Int#

As `( a |> kco ) :: TYPE Int#`, the code generator knows to use a machine-sized
integer register for `x`, and all is good again.

Because we can convert calls from hasFixedRuntimeRep_syntactic to
hasFixedRuntimeRep one at a time, we can migrate from PHASE 1 to PHASE 2
incrementally.

Example test cases that require PHASE 2: T13105, T17021, T20363b.

References 1

Referenced by 12