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/iface/TcIface.hs | |
| 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/iface/TcIface.hs')
| -rw-r--r-- | compiler/iface/TcIface.hs | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs index 1a2d737726..6fad8da87c 100644 --- a/compiler/iface/TcIface.hs +++ b/compiler/iface/TcIface.hs @@ -1341,7 +1341,6 @@ tcIfaceCo = go go (IfaceForAllCo tv k c) = do { k' <- go k ; bindIfaceTyVar tv $ \ tv' -> ForAllCo tv' k' <$> go c } - go (IfaceFreeCoVar c) = pprPanic "tcIfaceCo:IfaceFreeCoVar" (ppr c) go (IfaceCoVarCo n) = CoVarCo <$> go_var n go (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n <*> pure i <*> mapM go cs go (IfaceUnivCo p r t1 t2) = UnivCo <$> tcIfaceUnivCoProv p <*> pure r @@ -1359,6 +1358,8 @@ tcIfaceCo = go go (IfaceSubCo c) = SubCo <$> go c go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> go_axiom_rule ax <*> mapM go cos + go (IfaceFreeCoVar c) = pprPanic "tcIfaceCo:IfaceFreeCoVar" (ppr c) + go (IfaceHoleCo c) = pprPanic "tcIfaceCo:IfaceHoleCo" (ppr c) go_var :: FastString -> IfL CoVar go_var = tcIfaceLclId @@ -1374,8 +1375,6 @@ tcIfaceUnivCoProv IfaceUnsafeCoerceProv = return UnsafeCoerceProv tcIfaceUnivCoProv (IfacePhantomProv kco) = PhantomProv <$> tcIfaceCo kco tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco tcIfaceUnivCoProv (IfacePluginProv str) = return $ PluginProv str -tcIfaceUnivCoProv (IfaceHoleProv _) = - pprPanic "tcIfaceUnivCoProv" (text "holes can't occur in interface files") {- ************************************************************************ |