Note [Coercion holes]
During typechecking, constraint solving for type classes works by
- Generate an evidence Id, d7 :: Num a
- Wrap it in a Wanted constraint, [W] d7 :: Num a
- Use the evidence Id where the evidence is needed
- Solve the constraint later
- When solved, add an enclosing let-binding let d7 = .... in ....
which actually binds d7 to the (Num a) evidence
For equality constraints we use a different strategy. See Note [The
equality types story] in GHC.Builtin.Types.Prim for background on equality constraints.
- For /boxed/ equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just
like type classes above. (Indeed, boxed equality constraints *are* classes.)
- But for /unboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2)
we use a different plan
For unboxed equalities:
- Generate a CoercionHole, a mutable variable just like a unification
variable
- Wrap the CoercionHole in a Wanted constraint; see GHC.Tc.Utils.TcEvDest
- Use the CoercionHole in a Coercion, via HoleCo
- Solve the constraint later
- When solved, fill in the CoercionHole by side effect, instead of
doing the let-binding thing
The main reason for all this is that there may be no good place to let-bind
the evidence for unboxed equalities:
- We emit constraints for kind coercions, to be used to cast a
type's kind. These coercions then must be used in types. Because
they might appear in a top-level type, there is no place to bind
these (unlifted) coercions in the usual way.
- A coercion for (forall a. t1) ~ (forall a. t2) will look like
forall a. (coercion for t1~t2)
But the coercion for (t1~t2) may mention 'a', and we don't have
let-bindings within coercions. We could add them, but coercion
holes are easier.
- Moreover, nothing is lost from the lack of let-bindings. For
dictionaries want to achieve sharing to avoid recomputing the
dictionary. But coercions are entirely erased, so there's little
benefit to sharing. Indeed, even if we had a let-binding, we
always inline types and coercions at every use site and drop the
binding.
Other notes about HoleCo:
* INVARIANT: CoercionHole and HoleCo are used only during type checking,
and should never appear in Core. Just like unification variables; a Type
can contain a TcTyVar, but only during type checking. If, one day, we
use type-level information to separate out forms that can appear during
type-checking vs forms that can appear in core proper, holes in Core will
be ruled out.
* See Note [CoercionHoles and coercion free variables]
* Coercion holes can be compared for equality like other coercions:
by looking at the types coerced. References 1
- CoercionHoles and coercion free variables GHC.Core.TyCo.Rep
Referenced by 6
- GHC.Core.TyCo.Rep call site ×3
- The equality types story GHC.Builtin.Types.Prim
- GHC.Core.Type call site
- GHC.Tc.Types.Constraint call site