Commit d3ce4172 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu
Browse files

Tweak comments around UnivCos.

parent 721d56d5
......@@ -880,18 +880,19 @@ role and kind, which is done in the UnivCo constructor.
-- | For simplicity, we have just one UnivCo that represents a coercion from
-- some type to some other type, with (in general) no restrictions on the
-- type. To make better sense of these, we tag a UnivCo with a
-- UnivCoProvenance. This provenance is rarely consulted and is more
-- for debugging info than anything else.
-- An important exception to this rule is that we also use a UnivCo
-- for coercion holes. See Note [Coercion holes].
-- type. The UnivCoProvenance specifies more exactly what the coercion really
-- is and why a program should (or shouldn't!) trust the coercion.
-- It is reasonable to consider each constructor of 'UnivCoProvenance'
-- as a totally independent coercion form; their only commonality is
-- that they don't tell you what types they coercion between. (That info
-- is in the 'UnivCo' constructor of 'Coercion'.
data UnivCoProvenance
= UnsafeCoerceProv -- ^ From @unsafeCoerce#@. These are unsound.
| PhantomProv Coercion -- ^ See Note [Phantom coercions]
| PhantomProv CoercionN -- ^ See Note [Phantom coercions]
| ProofIrrelProv Coercion -- ^ From the fact that any two coercions are
-- considered equivalent. See Note [ProofIrrelProv]
| ProofIrrelProv CoercionN -- ^ From the fact that any two coercions are
-- considered equivalent. See Note [ProofIrrelProv]
| PluginProv String -- ^ From a plugin, which asserts that this coercion
-- is sound. The string is for the use of the plugin.
......@@ -929,10 +930,11 @@ Consider
data T a = T1 | T2
Then we have
T s ~R T t
for any old s,t. The witness for this is a phantom coercion built with
PhantomProv. The role ofthe UnivCo is always representational. The
Coercion stored is the (nominal) kind coercion between the types
kind(T s) ~ kind (T t)
for any old s,t. The witness for this is (TyConAppCo T Rep co),
where (co :: s ~P t) is a phantom coercion built with PhantomProv.
The role of the UnivCo is always Phantom. The Coercion stored is the
(nominal) kind coercion between the types
kind(s) ~N kind (t)
Note [Coercion holes]
~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -947,14 +949,14 @@ During typechecking, constraint solving for type classes works by
For equality constraints we use a different strategy. See Note [The
equality types story] in TysPrim for background on equality constraints.
- For boxed equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just
liek type classes above
- But for /unxboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2)
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 TcRnType.TcEvDest
- Wrap the CoercionHole in a Wanted constraint; see TcRnTypes.TcEvDest
- Use the CoercionHole in a Coercion, via HoleProv
- Solve the constraint later
- When solved, fill in the CoercionHole by side effect, instead of
......@@ -992,7 +994,7 @@ Other notes about HoleCo:
Note [ProofIrrelProv]
~~~~~~~~~~~~~~~~~~~~~
A ProofIreelProv is a coercion between coercions. For example:
A ProofIrrelProv is a coercion between coercions. For example:
data G a where
MkG :: G Bool
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment