Commit b586f77b authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari
Browse files

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.

(cherry picked from commit a492af06)
parent 87e517c1
...@@ -654,6 +654,7 @@ rnIfaceCo (IfaceForAllCo bndr co1 co2) ...@@ -654,6 +654,7 @@ rnIfaceCo (IfaceForAllCo bndr co1 co2)
= IfaceForAllCo <$> rnIfaceTvBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2 = IfaceForAllCo <$> rnIfaceTvBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2
rnIfaceCo (IfaceFreeCoVar c) = pure (IfaceFreeCoVar c) rnIfaceCo (IfaceFreeCoVar c) = pure (IfaceFreeCoVar c)
rnIfaceCo (IfaceCoVarCo lcl) = IfaceCoVarCo <$> pure lcl rnIfaceCo (IfaceCoVarCo lcl) = IfaceCoVarCo <$> pure lcl
rnIfaceCo (IfaceHoleCo lcl) = IfaceHoleCo <$> pure lcl
rnIfaceCo (IfaceAxiomInstCo n i cs) rnIfaceCo (IfaceAxiomInstCo n i cs)
= IfaceAxiomInstCo <$> rnIfaceGlobal n <*> pure i <*> mapM rnIfaceCo cs = IfaceAxiomInstCo <$> rnIfaceGlobal n <*> pure i <*> mapM rnIfaceCo cs
rnIfaceCo (IfaceUnivCo s r t1 t2) rnIfaceCo (IfaceUnivCo s r t1 t2)
......
...@@ -386,13 +386,13 @@ orphNamesOfCo (CoherenceCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNames ...@@ -386,13 +386,13 @@ orphNamesOfCo (CoherenceCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNames
orphNamesOfCo (KindCo co) = orphNamesOfCo co orphNamesOfCo (KindCo co) = orphNamesOfCo co
orphNamesOfCo (SubCo co) = orphNamesOfCo co orphNamesOfCo (SubCo co) = orphNamesOfCo co
orphNamesOfCo (AxiomRuleCo _ cs) = orphNamesOfCos cs orphNamesOfCo (AxiomRuleCo _ cs) = orphNamesOfCos cs
orphNamesOfCo (HoleCo _) = emptyNameSet
orphNamesOfProv :: UnivCoProvenance -> NameSet orphNamesOfProv :: UnivCoProvenance -> NameSet
orphNamesOfProv UnsafeCoerceProv = emptyNameSet orphNamesOfProv UnsafeCoerceProv = emptyNameSet
orphNamesOfProv (PhantomProv co) = orphNamesOfCo co orphNamesOfProv (PhantomProv co) = orphNamesOfCo co
orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co
orphNamesOfProv (PluginProv _) = emptyNameSet orphNamesOfProv (PluginProv _) = emptyNameSet
orphNamesOfProv (HoleProv _) = emptyNameSet
orphNamesOfCos :: [Coercion] -> NameSet orphNamesOfCos :: [Coercion] -> NameSet
orphNamesOfCos = orphNamesOfThings orphNamesOfCo orphNamesOfCos = orphNamesOfThings orphNamesOfCo
......
...@@ -1666,8 +1666,6 @@ lintCoercion co@(UnivCo prov r ty1 ty2) ...@@ -1666,8 +1666,6 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
; check_kinds kco k1 k2 } ; check_kinds kco k1 k2 }
PluginProv _ -> return () -- no extra checks PluginProv _ -> return () -- no extra checks
HoleProv h -> addErrL $
text "Unfilled coercion hole:" <+> ppr h
; when (r /= Phantom && classifiesTypeWithValues k1 ; when (r /= Phantom && classifiesTypeWithValues k1
&& classifiesTypeWithValues k2) && classifiesTypeWithValues k2)
...@@ -1874,6 +1872,11 @@ lintCoercion this@(AxiomRuleCo co cs) ...@@ -1874,6 +1872,11 @@ lintCoercion this@(AxiomRuleCo co cs)
[ text "Expected:" <+> int (n + length es) [ text "Expected:" <+> int (n + length es)
, text "Provided:" <+> int n ] , text "Provided:" <+> int n ]
lintCoercion (HoleCo h)
= do { addErrL $ text "Unfilled coercion hole:" <+> ppr h
; lintCoercion (CoVarCo (coHoleCoVar h)) }
---------- ----------
lintUnliftedCoVar :: CoVar -> LintM () lintUnliftedCoVar :: CoVar -> LintM ()
lintUnliftedCoVar cv lintUnliftedCoVar cv
......
...@@ -1434,8 +1434,8 @@ freeNamesIfCoercion (IfaceAppCo c1 c2) ...@@ -1434,8 +1434,8 @@ freeNamesIfCoercion (IfaceAppCo c1 c2)
freeNamesIfCoercion (IfaceForAllCo _ kind_co co) freeNamesIfCoercion (IfaceForAllCo _ kind_co co)
= freeNamesIfCoercion kind_co &&& freeNamesIfCoercion co = freeNamesIfCoercion kind_co &&& freeNamesIfCoercion co
freeNamesIfCoercion (IfaceFreeCoVar _) = emptyNameSet freeNamesIfCoercion (IfaceFreeCoVar _) = emptyNameSet
freeNamesIfCoercion (IfaceCoVarCo _) freeNamesIfCoercion (IfaceCoVarCo _) = emptyNameSet
= emptyNameSet freeNamesIfCoercion (IfaceHoleCo _) = emptyNameSet
freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos) freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos)
= unitNameSet ax &&& fnList freeNamesIfCoercion cos = unitNameSet ax &&& fnList freeNamesIfCoercion cos
freeNamesIfCoercion (IfaceUnivCo p _ t1 t2) freeNamesIfCoercion (IfaceUnivCo p _ t1 t2)
...@@ -1465,7 +1465,6 @@ freeNamesIfProv IfaceUnsafeCoerceProv = emptyNameSet ...@@ -1465,7 +1465,6 @@ freeNamesIfProv IfaceUnsafeCoerceProv = emptyNameSet
freeNamesIfProv (IfacePhantomProv co) = freeNamesIfCoercion co freeNamesIfProv (IfacePhantomProv co) = freeNamesIfCoercion co
freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
freeNamesIfProv (IfacePluginProv _) = emptyNameSet freeNamesIfProv (IfacePluginProv _) = emptyNameSet
freeNamesIfProv (IfaceHoleProv _) = emptyNameSet
freeNamesIfTyVarBndr :: TyVarBndr IfaceTvBndr vis -> NameSet freeNamesIfTyVarBndr :: TyVarBndr IfaceTvBndr vis -> NameSet
freeNamesIfTyVarBndr (TvBndr tv _) = freeNamesIfTvBndr tv freeNamesIfTyVarBndr (TvBndr tv _) = freeNamesIfTvBndr tv
......
...@@ -196,8 +196,8 @@ data IfaceTyConSort = IfaceNormalTyCon -- ^ a regular tycon ...@@ -196,8 +196,8 @@ data IfaceTyConSort = IfaceNormalTyCon -- ^ a regular tycon
{- Note [Free tyvars in IfaceType] {- Note [Free tyvars in IfaceType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to an Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to
IfaceType and pretty printing that. This eliminates a lot of an IfaceType and pretty printing that. This eliminates a lot of
pretty-print duplication, and it matches what we do with pretty-print duplication, and it matches what we do with
pretty-printing TyThings. pretty-printing TyThings.
...@@ -255,7 +255,6 @@ data IfaceCoercion ...@@ -255,7 +255,6 @@ data IfaceCoercion
| IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion] | IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion]
| IfaceAppCo IfaceCoercion IfaceCoercion | IfaceAppCo IfaceCoercion IfaceCoercion
| IfaceForAllCo IfaceTvBndr IfaceCoercion IfaceCoercion | IfaceForAllCo IfaceTvBndr IfaceCoercion IfaceCoercion
| IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType]
| IfaceCoVarCo IfLclName | IfaceCoVarCo IfLclName
| IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion] | IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
| IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType | IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType
...@@ -268,29 +267,26 @@ data IfaceCoercion ...@@ -268,29 +267,26 @@ data IfaceCoercion
| IfaceKindCo IfaceCoercion | IfaceKindCo IfaceCoercion
| IfaceSubCo IfaceCoercion | IfaceSubCo IfaceCoercion
| IfaceAxiomRuleCo IfLclName [IfaceCoercion] | IfaceAxiomRuleCo IfLclName [IfaceCoercion]
| IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType]
| IfaceHoleCo CoVar -- ^ See Note [Holes in IfaceCoercion]
data IfaceUnivCoProv data IfaceUnivCoProv
= IfaceUnsafeCoerceProv = IfaceUnsafeCoerceProv
| IfacePhantomProv IfaceCoercion | IfacePhantomProv IfaceCoercion
| IfaceProofIrrelProv IfaceCoercion | IfaceProofIrrelProv IfaceCoercion
| IfacePluginProv String | IfacePluginProv String
| IfaceHoleProv Unique
-- ^ See Note [Holes in IfaceUnivCoProv]
{- {- Note [Holes in IfaceCoercion]
Note [Holes in IfaceUnivCoProv] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When typechecking fails the typechecker will produce a HoleCo to stand
When typechecking fails the typechecker will produce a HoleProv UnivCoProv to in place of the unproven assertion. While we generally don't want to
stand in place of the unproven assertion. While we generally don't want to let let these unproven assertions leak into interface files, we still need
these unproven assertions leak into interface files, we still need to be able to to be able to pretty-print them as we use IfaceType's pretty-printer
pretty-print them as we use IfaceType's pretty-printer to render Types. For this to render Types. For this reason IfaceCoercion has a IfaceHoleCo
reason IfaceUnivCoProv has a IfaceHoleProv constructor; however, we fails when constructor; however, we fails when asked to serialize to a
asked to serialize to a IfaceHoleProv to ensure that they don't end up in an IfaceHoleCo to ensure that they don't end up in an interface file.
interface file. To avoid an import loop between IfaceType and TyCoRep we only
keep the hole's Unique, since that is all we need to print.
-}
{-
%************************************************************************ %************************************************************************
%* * %* *
Functions over IFaceTypes Functions over IFaceTypes
...@@ -419,6 +415,7 @@ substIfaceType env ty ...@@ -419,6 +415,7 @@ substIfaceType env ty
go_co (IfaceForAllCo {}) = pprPanic "substIfaceCoercion" (ppr ty) go_co (IfaceForAllCo {}) = pprPanic "substIfaceCoercion" (ppr ty)
go_co (IfaceFreeCoVar cv) = IfaceFreeCoVar cv go_co (IfaceFreeCoVar cv) = IfaceFreeCoVar cv
go_co (IfaceCoVarCo cv) = IfaceCoVarCo cv go_co (IfaceCoVarCo cv) = IfaceCoVarCo cv
go_co (IfaceHoleCo cv) = IfaceHoleCo cv
go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos) go_co (IfaceAxiomInstCo a i cos) = IfaceAxiomInstCo a i (go_cos cos)
go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2) go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2)
go_co (IfaceSymCo co) = IfaceSymCo (go_co co) go_co (IfaceSymCo co) = IfaceSymCo (go_co co)
...@@ -437,7 +434,6 @@ substIfaceType env ty ...@@ -437,7 +434,6 @@ substIfaceType env ty
go_prov (IfacePhantomProv co) = IfacePhantomProv (go_co co) go_prov (IfacePhantomProv co) = IfacePhantomProv (go_co co)
go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co) go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
go_prov (IfacePluginProv str) = IfacePluginProv str go_prov (IfacePluginProv str) = IfacePluginProv str
go_prov (IfaceHoleProv h) = IfaceHoleProv h
substIfaceTcArgs :: IfaceTySubst -> IfaceTcArgs -> IfaceTcArgs substIfaceTcArgs :: IfaceTySubst -> IfaceTcArgs -> IfaceTcArgs
substIfaceTcArgs env args substIfaceTcArgs env args
...@@ -1077,19 +1073,17 @@ ppr_co ctxt_prec co@(IfaceForAllCo {}) ...@@ -1077,19 +1073,17 @@ ppr_co ctxt_prec co@(IfaceForAllCo {})
= let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'') = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
split_co co' = ([], co') split_co co' = ([], co')
-- Why these two? See Note [TcTyVars in IfaceType] -- Why these three? See Note [TcTyVars in IfaceType]
ppr_co _ (IfaceFreeCoVar covar) = ppr covar ppr_co _ (IfaceFreeCoVar covar) = ppr covar
ppr_co _ (IfaceCoVarCo covar) = ppr covar ppr_co _ (IfaceCoVarCo covar) = ppr covar
ppr_co _ (IfaceHoleCo covar) = braces (ppr covar)
ppr_co ctxt_prec (IfaceUnivCo IfaceUnsafeCoerceProv r ty1 ty2) ppr_co ctxt_prec (IfaceUnivCo IfaceUnsafeCoerceProv r ty1 ty2)
= maybeParen ctxt_prec TyConPrec $ = maybeParen ctxt_prec TyConPrec $
text "UnsafeCo" <+> ppr r <+> text "UnsafeCo" <+> ppr r <+>
pprParendIfaceType ty1 <+> pprParendIfaceType ty2 pprParendIfaceType ty1 <+> pprParendIfaceType ty2
ppr_co _ctxt_prec (IfaceUnivCo (IfaceHoleProv u) _ _ _) ppr_co _ (IfaceUnivCo _ _ ty1 ty2)
= braces $ ppr u
ppr_co _ (IfaceUnivCo _ _ ty1 ty2)
= angleBrackets ( ppr ty1 <> comma <+> ppr ty2 ) = angleBrackets ( ppr ty1 <> comma <+> ppr ty2 )
ppr_co ctxt_prec (IfaceInstCo co ty) ppr_co ctxt_prec (IfaceInstCo co ty)
...@@ -1358,8 +1352,6 @@ instance Binary IfaceCoercion where ...@@ -1358,8 +1352,6 @@ instance Binary IfaceCoercion where
put_ bh a put_ bh a
put_ bh b put_ bh b
put_ bh c put_ bh c
put_ _ (IfaceFreeCoVar cv)
= pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv)
put_ bh (IfaceCoVarCo a) = do put_ bh (IfaceCoVarCo a) = do
putByte bh 6 putByte bh 6
put_ bh a put_ bh a
...@@ -1407,6 +1399,11 @@ instance Binary IfaceCoercion where ...@@ -1407,6 +1399,11 @@ instance Binary IfaceCoercion where
putByte bh 17 putByte bh 17
put_ bh a put_ bh a
put_ bh b put_ bh b
put_ _ (IfaceFreeCoVar cv)
= pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv)
put_ _ (IfaceHoleCo cv)
= pprPanic "Can't serialise IfaceHoleCo" (ppr cv)
-- See Note [Holes in IfaceUnivCoProv]
get bh = do get bh = do
tag <- getByte bh tag <- getByte bh
...@@ -1477,9 +1474,6 @@ instance Binary IfaceUnivCoProv where ...@@ -1477,9 +1474,6 @@ instance Binary IfaceUnivCoProv where
put_ bh (IfacePluginProv a) = do put_ bh (IfacePluginProv a) = do
putByte bh 4 putByte bh 4
put_ bh a put_ bh a
put_ _ (IfaceHoleProv _) =
pprPanic "Binary(IfaceUnivCoProv) hit a hole" empty
-- See Note [Holes in IfaceUnivCoProv]
get bh = do get bh = do
tag <- getByte bh tag <- getByte bh
......
...@@ -1341,7 +1341,6 @@ tcIfaceCo = go ...@@ -1341,7 +1341,6 @@ tcIfaceCo = go
go (IfaceForAllCo tv k c) = do { k' <- go k go (IfaceForAllCo tv k c) = do { k' <- go k
; bindIfaceTyVar tv $ \ tv' -> ; bindIfaceTyVar tv $ \ tv' ->
ForAllCo tv' k' <$> go c } ForAllCo tv' k' <$> go c }
go (IfaceFreeCoVar c) = pprPanic "tcIfaceCo:IfaceFreeCoVar" (ppr c)
go (IfaceCoVarCo n) = CoVarCo <$> go_var n go (IfaceCoVarCo n) = CoVarCo <$> go_var n
go (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n <*> pure i <*> mapM go cs go (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n <*> pure i <*> mapM go cs
go (IfaceUnivCo p r t1 t2) = UnivCo <$> tcIfaceUnivCoProv p <*> pure r go (IfaceUnivCo p r t1 t2) = UnivCo <$> tcIfaceUnivCoProv p <*> pure r
...@@ -1359,6 +1358,8 @@ tcIfaceCo = go ...@@ -1359,6 +1358,8 @@ tcIfaceCo = go
go (IfaceSubCo c) = SubCo <$> go c go (IfaceSubCo c) = SubCo <$> go c
go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> go_axiom_rule ax go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> go_axiom_rule ax
<*> mapM go cos <*> 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 :: FastString -> IfL CoVar
go_var = tcIfaceLclId go_var = tcIfaceLclId
...@@ -1374,8 +1375,6 @@ tcIfaceUnivCoProv IfaceUnsafeCoerceProv = return UnsafeCoerceProv ...@@ -1374,8 +1375,6 @@ tcIfaceUnivCoProv IfaceUnsafeCoerceProv = return UnsafeCoerceProv
tcIfaceUnivCoProv (IfacePhantomProv kco) = PhantomProv <$> tcIfaceCo kco tcIfaceUnivCoProv (IfacePhantomProv kco) = PhantomProv <$> tcIfaceCo kco
tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco tcIfaceUnivCoProv (IfaceProofIrrelProv kco) = ProofIrrelProv <$> tcIfaceCo kco
tcIfaceUnivCoProv (IfacePluginProv str) = return $ PluginProv str tcIfaceUnivCoProv (IfacePluginProv str) = return $ PluginProv str
tcIfaceUnivCoProv (IfaceHoleProv _) =
pprPanic "tcIfaceUnivCoProv" (text "holes can't occur in interface files")
{- {-
************************************************************************ ************************************************************************
......
...@@ -218,7 +218,9 @@ toIfaceCoercionX fr co ...@@ -218,7 +218,9 @@ toIfaceCoercionX fr co
go (CoVarCo cv) go (CoVarCo cv)
-- See [TcTyVars in IfaceType] in IfaceType -- See [TcTyVars in IfaceType] in IfaceType
| cv `elemVarSet` fr = IfaceFreeCoVar cv | cv `elemVarSet` fr = IfaceFreeCoVar cv
| otherwise = IfaceCoVarCo (toIfaceCoVar cv) | otherwise = IfaceCoVarCo (toIfaceCoVar cv)
go (HoleCo h) = IfaceHoleCo (coHoleCoVar h)
go (AppCo co1 co2) = IfaceAppCo (go co1) (go co2) go (AppCo co1 co2) = IfaceAppCo (go co1) (go co2)
go (SymCo co) = IfaceSymCo (go co) go (SymCo co) = IfaceSymCo (go co)
go (TransCo co1 co2) = IfaceTransCo (go co1) (go co2) go (TransCo co1 co2) = IfaceTransCo (go co1) (go co2)
...@@ -250,7 +252,6 @@ toIfaceCoercionX fr co ...@@ -250,7 +252,6 @@ toIfaceCoercionX fr co
go_prov (PhantomProv co) = IfacePhantomProv (go co) go_prov (PhantomProv co) = IfacePhantomProv (go co)
go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co) go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
go_prov (PluginProv str) = IfacePluginProv str go_prov (PluginProv str) = IfacePluginProv str
go_prov (HoleProv h) = IfaceHoleProv (chUnique h)
toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs
toIfaceTcArgs = toIfaceTcArgsX emptyVarSet toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
......
...@@ -172,7 +172,7 @@ solveCallStack ev ev_cs = do ...@@ -172,7 +172,7 @@ solveCallStack ev ev_cs = do
-- dictionary, so we have to coerce ev_cs to a dictionary for -- dictionary, so we have to coerce ev_cs to a dictionary for
-- `IP ip CallStack`. See Note [Overview of implicit CallStacks] -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev)) let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev))
setWantedEvBind (ctEvId ev) ev_tm setWantedEvBind (ctEvEvId ev) ev_tm
canClass :: CtEvidence canClass :: CtEvidence
-> Class -> [Type] -> Class -> [Type]
......
...@@ -537,11 +537,17 @@ tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things ...@@ -537,11 +537,17 @@ tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things
get_tvs (_, ATcId { tct_id = id, tct_info = closed }) tvs get_tvs (_, ATcId { tct_id = id, tct_info = closed }) tvs
= case closed of = case closed of
ClosedLet -> ClosedLet -> ASSERT2( is_closed_type, ppr id $$ ppr (idType id) )
ASSERT2( isEmptyVarSet id_tvs, ppr id $$ ppr (idType id) ) tvs tvs
_ -> _other -> tvs `unionVarSet` id_tvs
tvs `unionVarSet` id_tvs where
where id_tvs = tyCoVarsOfType (idType id) id_tvs = tyCoVarsOfType (idType id)
is_closed_type = not (anyVarSet isTyVar id_tvs)
-- We only care about being closed wrt /type/ variables
-- E.g. a top-level binding might have a type like
-- foo :: t |> co
-- where co :: * ~ *
-- or some other as-yet-unsolved kind coercion
get_tvs (_, ATyVar _ tv) tvs -- See Note [Global TyVars] get_tvs (_, ATyVar _ tv) tvs -- See Note [Global TyVars]
= tvs `unionVarSet` tyCoVarsOfType (tyVarKind tv) `extendVarSet` tv = tvs `unionVarSet` tyCoVarsOfType (tyVarKind tv) `extendVarSet` tv
......
...@@ -805,9 +805,9 @@ addDeferredBinding ctxt err ct ...@@ -805,9 +805,9 @@ addDeferredBinding ctxt err ct
-> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm -> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
HoleDest hole HoleDest hole
-> do { -- See Note [Deferred errors for coercion holes] -> do { -- See Note [Deferred errors for coercion holes]
evar <- newEvVar pred let co_var = coHoleCoVar hole
; addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm
; fillCoercionHole hole (mkTcCoVarCo evar) }} ; fillCoercionHole hole (mkTcCoVarCo co_var) }}
| otherwise -- Do not set any evidence for Given/Derived | otherwise -- Do not set any evidence for Given/Derived
= return () = return ()
......
...@@ -52,6 +52,7 @@ import TcEvidence ...@@ -52,6 +52,7 @@ import TcEvidence
import TysPrim import TysPrim
import TyCon ( isUnboxedTupleTyCon ) import TyCon ( isUnboxedTupleTyCon )
import TysWiredIn import TysWiredIn
import TyCoRep( CoercionHole(..) )
import Type import Type
import Coercion import Coercion
import ConLike import ConLike
...@@ -1572,35 +1573,30 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv ...@@ -1572,35 +1573,30 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
Just tv' -> return (mkTyVarTy tv') Just tv' -> return (mkTyVarTy tv')
zonkCoVarOcc :: ZonkEnv -> CoVar -> TcM Coercion zonkCoVarOcc :: ZonkEnv -> CoVar -> TcM Coercion
zonkCoVarOcc env@(ZonkEnv _ tyco_env _) cv zonkCoVarOcc (ZonkEnv _ tyco_env _) cv
| Just cv' <- lookupVarEnv tyco_env cv -- don't look in the knot-tied env | Just cv' <- lookupVarEnv tyco_env cv -- don't look in the knot-tied env
= return $ mkCoVarCo cv' = return $ mkCoVarCo cv'
| otherwise | otherwise
= mkCoVarCo <$> updateVarTypeM (zonkTcTypeToType env) cv = do { cv' <- zonkCoVar cv; return (mkCoVarCo cv') }
zonkCoHole :: ZonkEnv -> CoercionHole zonkCoHole :: ZonkEnv -> CoercionHole -> TcM Coercion
-> Role -> Type -> Type -- these are all redundant with zonkCoHole env hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
-- the details in the hole, = do { contents <- readTcRef ref
-- unzonked
-> TcM Coercion
zonkCoHole env h r t1 t2
= do { contents <- unpackCoercionHole_maybe h
; case contents of ; case contents of
Just co -> do { co <- zonkCoToCo env co Just co -> do { co' <- zonkCoToCo env co
; checkCoercionHole co h r t1 t2 } ; checkCoercionHole cv co' }
-- This next case should happen only in the presence of -- This next case should happen only in the presence of
-- (undeferred) type errors. Originally, I put in a panic -- (undeferred) type errors. Originally, I put in a panic
-- here, but that caused too many uses of `failIfErrsM`. -- here, but that caused too many uses of `failIfErrsM`.
Nothing -> do { traceTc "Zonking unfilled coercion hole" (ppr h) Nothing -> do { traceTc "Zonking unfilled coercion hole" (ppr hole)
; when debugIsOn $ ; when debugIsOn $
whenNoErrs $ whenNoErrs $
MASSERT2( False MASSERT2( False
, text "Type-correct unfilled coercion hole" , text "Type-correct unfilled coercion hole"
<+> ppr h ) <+> ppr hole )
; t1 <- zonkTcTypeToType env t1 ; cv' <- zonkCoVar cv
; t2 <- zonkTcTypeToType env t2 ; return $ mkHoleCo (hole { ch_co_var = cv' }) } }
; return $ mkHoleCo h r t1 t2 } }
zonk_tycomapper :: TyCoMapper ZonkEnv TcM zonk_tycomapper :: TyCoMapper ZonkEnv TcM
zonk_tycomapper = TyCoMapper zonk_tycomapper = TyCoMapper
......
...@@ -589,7 +589,7 @@ solveOneFromTheOther ev_i ev_w ...@@ -589,7 +589,7 @@ solveOneFromTheOther ev_i ev_w
| otherwise | otherwise
= KeepInert = KeepInert
has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev)) has_binding binds ev = isJust (lookupEvBind binds (ctEvEvId ev))
{- {-
Note [Replacement vs keeping] Note [Replacement vs keeping]
...@@ -989,7 +989,7 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs ...@@ -989,7 +989,7 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
; try_inst_res <- shortCutSolver dflags ev_w ev_i ; try_inst_res <- shortCutSolver dflags ev_w ev_i
; case try_inst_res of ; case try_inst_res of
Just evs -> do { flip mapM_ evs $ \ (ev_t, ct_ev, cls, typ) -> Just evs -> do { flip mapM_ evs $ \ (ev_t, ct_ev, cls, typ) ->
do { setWantedEvBind (ctEvId ct_ev) ev_t do { setWantedEvBind (ctEvEvId ct_ev) ev_t
; addSolvedDict ct_ev cls typ } ; addSolvedDict ct_ev cls typ }
; stopWith ev_w "interactDict/solved from instance" } ; stopWith ev_w "interactDict/solved from instance" }
...@@ -2238,7 +2238,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls ...@@ -2238,7 +2238,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
finish_wanted theta mk_ev finish_wanted theta mk_ev
= do { addSolvedDict fl cls xis = do { addSolvedDict fl cls xis
; evc_vars <- mapM (newWanted deeper_loc) theta ; evc_vars <- mapM (newWanted deeper_loc) theta
; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars)) ; setWantedEvBind (ctEvEvId fl) (mk_ev (map getEvTerm evc_vars))
; emitWorkNC (freshGoals evc_vars) ; emitWorkNC (freshGoals evc_vars)
; stopWith fl "Dict/Top (solved wanted)" } ; stopWith fl "Dict/Top (solved wanted)" }
......
...@@ -79,7 +79,9 @@ module TcMType ( ...@@ -79,7 +79,9 @@ module TcMType (
zonkTcType, zonkTcTypes, zonkCo, zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind, zonkTcTypeMapper, zonkTyCoVarKind, zonkTcTypeMapper,
zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo, zonkEvVar, zonkWC, zonkSimples,
zonkId, zonkCoVar,
zonkCt, zonkSkolemInfo,
tcGetGlobalTyCoVars, tcGetGlobalTyCoVars,
...@@ -172,7 +174,7 @@ newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence ...@@ -172,7 +174,7 @@ newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
-- Deals with both equality and non-equality predicates -- Deals with both equality and non-equality predicates
newWanted orig t_or_k pty newWanted orig t_or_k pty
= do loc <- getCtLocM orig t_or_k = do loc <- getCtLocM orig t_or_k
d <- if isEqPred pty then HoleDest <$> newCoercionHole d <- if isEqPred pty then HoleDest <$> newCoercionHole pty
else EvVarDest <$> newEvVar pty else EvVarDest <$> newEvVar pty
return $ CtWanted { ctev_dest = d return $ CtWanted { ctev_dest = d
, ctev_pred = pty , ctev_pred = pty
...@@ -210,12 +212,12 @@ emitWanted origin pty ...@@ -210,12 +212,12 @@ emitWanted origin pty
-- | Emits a new equality constraint -- | Emits a new equality constraint
emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
emitWantedEq origin t_or_k role ty1 ty2 emitWantedEq origin t_or_k role ty1 ty2
= do { hole <- newCoercionHole = do { hole <- newCoercionHole pty
; loc <- getCtLocM origin (Just t_or_k) ; loc <- getCtLocM origin (Just t_or_k)
; emitSimple $ mkNonCanonical $ ; emitSimple $ mkNonCanonical $
CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
, ctev_nosh = WDeriv, ctev_loc = loc } , ctev_nosh = WDeriv, ctev_loc = loc }
; return (mkHoleCo hole role ty1 ty2) } ; return (HoleCo hole) }
where where
pty = mkPrimEqPredRole role ty1 ty2 pty = mkPrimEqPredRole role ty1 ty2
...@@ -254,28 +256,28 @@ predTypeOccName ty = case classifyPredType ty of ...@@ -254,28 +256,28 @@ predTypeOccName ty = case classifyPredType ty of
************************************************************************ ************************************************************************
-} -}
newCoercionHole :: TcM CoercionHole newCoercionHole :: TcPredType -> TcM CoercionHole
newCoercionHole newCoercionHole pred_ty
= do { u <- newUnique