diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2017-12-21 13:31:13 +0000 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2017-12-21 14:14:21 +0000 |
| commit | a492af06d3264530d134584f22ffb726a16c78ec (patch) | |
| tree | 294b0c21775d6a7cb9b79c86145d7b6ca47c81ea /compiler/backpack | |
| parent | 72938f5890dac81afad52bf58175c1e29ffbc6dd (diff) | |
| download | haskell-a492af06d3264530d134584f22ffb726a16c78ec.tar.gz | |
Refactor coercion holes
In fixing Trac #14584 I found that it would be /much/ more
convenient if a "hole" in a coercion (much like a unification
variable in a type) acutally had a CoVar associated with it
rather than just a Unique. Then I can ask what the free variables
of a coercion is, and get a set of CoVars including those
as-yet-un-filled in holes.
Once that is done, it makes no sense to stuff coercion holes
inside UnivCo. They were there before so we could know the
kind and role of a "hole" coercion, but once there is a CoVar
we can get that info from the CoVar. So I removed HoleProv
from UnivCoProvenance and added HoleCo to Coercion.
In summary:
* Add HoleCo to Coercion and remove HoleProv from UnivCoProvanance
* Similarly in IfaceCoercion
* Make CoercionHole have a CoVar in it, not a Unique
* Make tyCoVarsOfCo return the free coercion-hole variables
as well as the ordinary free CoVars. Similarly, remember
to zonk the CoVar in a CoercionHole
We could go further, and remove CoercionHole as a distinct type
altogther, just collapsing it into HoleCo. But I have not done
that yet.
Diffstat (limited to 'compiler/backpack')
| -rw-r--r-- | compiler/backpack/RnModIface.hs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs index 2199965d13..c52fce772d 100644 --- a/compiler/backpack/RnModIface.hs +++ b/compiler/backpack/RnModIface.hs @@ -654,6 +654,7 @@ rnIfaceCo (IfaceForAllCo bndr co1 co2) = IfaceForAllCo <$> rnIfaceTvBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2 rnIfaceCo (IfaceFreeCoVar c) = pure (IfaceFreeCoVar c) rnIfaceCo (IfaceCoVarCo lcl) = IfaceCoVarCo <$> pure lcl +rnIfaceCo (IfaceHoleCo lcl) = IfaceHoleCo <$> pure lcl rnIfaceCo (IfaceAxiomInstCo n i cs) = IfaceAxiomInstCo <$> rnIfaceGlobal n <*> pure i <*> mapM rnIfaceCo cs rnIfaceCo (IfaceUnivCo s r t1 t2) |