Commit a492af06 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 72938f58
......@@ -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)
......
......@@ -386,13 +386,13 @@ orphNamesOfCo (CoherenceCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNames
orphNamesOfCo (KindCo co) = orphNamesOfCo co
orphNamesOfCo (SubCo co) = orphNamesOfCo co
orphNamesOfCo (AxiomRuleCo _ cs) = orphNamesOfCos cs
orphNamesOfCo (HoleCo _) = emptyNameSet
orphNamesOfProv :: UnivCoProvenance -> NameSet
orphNamesOfProv UnsafeCoerceProv = emptyNameSet
orphNamesOfProv (PhantomProv co) = orphNamesOfCo co
orphNamesOfProv (ProofIrrelProv co) = orphNamesOfCo co
orphNamesOfProv (PluginProv _) = emptyNameSet
orphNamesOfProv (HoleProv _) = emptyNameSet
orphNamesOfCos :: [Coercion] -> NameSet
orphNamesOfCos = orphNamesOfThings orphNamesOfCo
......
......@@ -1666,8 +1666,6 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
; check_kinds kco k1 k2 }
PluginProv _ -> return () -- no extra checks
HoleProv h -> addErrL $
text "Unfilled coercion hole:" <+> ppr h
; when (r /= Phantom && classifiesTypeWithValues k1
&& classifiesTypeWithValues k2)
......@@ -1874,6 +1872,11 @@ lintCoercion this@(AxiomRuleCo co cs)
[ text "Expected:" <+> int (n + length es)
, text "Provided:" <+> int n ]
lintCoercion (HoleCo h)
= do { addErrL $ text "Unfilled coercion hole:" <+> ppr h
; lintCoercion (CoVarCo (coHoleCoVar h)) }
----------
lintUnliftedCoVar :: CoVar -> LintM ()
lintUnliftedCoVar cv
......
......@@ -1434,8 +1434,8 @@ freeNamesIfCoercion (IfaceAppCo c1 c2)
freeNamesIfCoercion (IfaceForAllCo _ kind_co co)
= freeNamesIfCoercion kind_co &&& freeNamesIfCoercion co
freeNamesIfCoercion (IfaceFreeCoVar _) = emptyNameSet
freeNamesIfCoercion (IfaceCoVarCo _)
= emptyNameSet
freeNamesIfCoercion (IfaceCoVarCo _) = emptyNameSet
freeNamesIfCoercion (IfaceHoleCo _) = emptyNameSet
freeNamesIfCoercion (IfaceAxiomInstCo ax _ cos)
= unitNameSet ax &&& fnList freeNamesIfCoercion cos
freeNamesIfCoercion (IfaceUnivCo p _ t1 t2)
......@@ -1465,7 +1465,6 @@ freeNamesIfProv IfaceUnsafeCoerceProv = emptyNameSet
freeNamesIfProv (IfacePhantomProv co) = freeNamesIfCoercion co
freeNamesIfProv (IfaceProofIrrelProv co) = freeNamesIfCoercion co
freeNamesIfProv (IfacePluginProv _) = emptyNameSet
freeNamesIfProv (IfaceHoleProv _) = emptyNameSet
freeNamesIfTyVarBndr :: TyVarBndr IfaceTvBndr vis -> NameSet
freeNamesIfTyVarBndr (TvBndr tv _) = freeNamesIfTvBndr tv
......
......@@ -196,8 +196,8 @@ data IfaceTyConSort = IfaceNormalTyCon -- ^ a regular tycon
{- Note [Free tyvars in IfaceType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to an
IfaceType and pretty printing that. This eliminates a lot of
Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to
an IfaceType and pretty printing that. This eliminates a lot of
pretty-print duplication, and it matches what we do with
pretty-printing TyThings.
......@@ -255,7 +255,6 @@ data IfaceCoercion
| IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion]
| IfaceAppCo IfaceCoercion IfaceCoercion
| IfaceForAllCo IfaceTvBndr IfaceCoercion IfaceCoercion
| IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType]
| IfaceCoVarCo IfLclName
| IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
| IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType
......@@ -268,29 +267,26 @@ data IfaceCoercion
| IfaceKindCo IfaceCoercion
| IfaceSubCo IfaceCoercion
| IfaceAxiomRuleCo IfLclName [IfaceCoercion]
| IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType]
| IfaceHoleCo CoVar -- ^ See Note [Holes in IfaceCoercion]
data IfaceUnivCoProv
= IfaceUnsafeCoerceProv
| IfacePhantomProv IfaceCoercion
| IfaceProofIrrelProv IfaceCoercion
| IfacePluginProv String
| IfaceHoleProv Unique
-- ^ See Note [Holes in IfaceUnivCoProv]
{-
Note [Holes in IfaceUnivCoProv]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When typechecking fails the typechecker will produce a HoleProv UnivCoProv to
stand in place of the unproven assertion. While we generally don't want to let
these unproven assertions leak into interface files, we still need to be able to
pretty-print them as we use IfaceType's pretty-printer to render Types. For this
reason IfaceUnivCoProv has a IfaceHoleProv constructor; however, we fails when
asked to serialize to a IfaceHoleProv to ensure that they don't end up in an
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.
-}
{- Note [Holes in IfaceCoercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When typechecking fails the typechecker will produce a HoleCo to stand
in place of the unproven assertion. While we generally don't want to
let these unproven assertions leak into interface files, we still need
to be able to pretty-print them as we use IfaceType's pretty-printer
to render Types. For this reason IfaceCoercion has a IfaceHoleCo
constructor; however, we fails when asked to serialize to a
IfaceHoleCo to ensure that they don't end up in an interface file.
{-
%************************************************************************
%* *
Functions over IFaceTypes
......@@ -419,6 +415,7 @@ substIfaceType env ty
go_co (IfaceForAllCo {}) = pprPanic "substIfaceCoercion" (ppr ty)
go_co (IfaceFreeCoVar cv) = IfaceFreeCoVar 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 (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2)
go_co (IfaceSymCo co) = IfaceSymCo (go_co co)
......@@ -437,7 +434,6 @@ substIfaceType env ty
go_prov (IfacePhantomProv co) = IfacePhantomProv (go_co co)
go_prov (IfaceProofIrrelProv co) = IfaceProofIrrelProv (go_co co)
go_prov (IfacePluginProv str) = IfacePluginProv str
go_prov (IfaceHoleProv h) = IfaceHoleProv h
substIfaceTcArgs :: IfaceTySubst -> IfaceTcArgs -> IfaceTcArgs
substIfaceTcArgs env args
......@@ -1077,19 +1073,17 @@ ppr_co ctxt_prec co@(IfaceForAllCo {})
= let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
split_co co' = ([], co')
-- Why these two? See Note [TcTyVars in IfaceType]
ppr_co _ (IfaceFreeCoVar covar) = ppr covar
ppr_co _ (IfaceCoVarCo covar) = ppr covar
-- Why these three? See Note [TcTyVars in IfaceType]
ppr_co _ (IfaceFreeCoVar 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)
= maybeParen ctxt_prec TyConPrec $
text "UnsafeCo" <+> ppr r <+>
pprParendIfaceType ty1 <+> pprParendIfaceType ty2
ppr_co _ctxt_prec (IfaceUnivCo (IfaceHoleProv u) _ _ _)
= braces $ ppr u
ppr_co _ (IfaceUnivCo _ _ ty1 ty2)
ppr_co _ (IfaceUnivCo _ _ ty1 ty2)
= angleBrackets ( ppr ty1 <> comma <+> ppr ty2 )
ppr_co ctxt_prec (IfaceInstCo co ty)
......@@ -1358,8 +1352,6 @@ instance Binary IfaceCoercion where
put_ bh a
put_ bh b
put_ bh c
put_ _ (IfaceFreeCoVar cv)
= pprPanic "Can't serialise IfaceFreeCoVar" (ppr cv)
put_ bh (IfaceCoVarCo a) = do
putByte bh 6
put_ bh a
......@@ -1407,6 +1399,11 @@ instance Binary IfaceCoercion where
putByte bh 17
put_ bh a
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
tag <- getByte bh
......@@ -1477,9 +1474,6 @@ instance Binary IfaceUnivCoProv where
put_ bh (IfacePluginProv a) = do
putByte bh 4
put_ bh a
put_ _ (IfaceHoleProv _) =
pprPanic "Binary(IfaceUnivCoProv) hit a hole" empty
-- See Note [Holes in IfaceUnivCoProv]
get bh = do
tag <- getByte bh
......
......@@ -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")
{-
************************************************************************
......
......@@ -218,7 +218,9 @@ toIfaceCoercionX fr co
go (CoVarCo cv)
-- See [TcTyVars in IfaceType] in IfaceType
| 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 (SymCo co) = IfaceSymCo (go co)
go (TransCo co1 co2) = IfaceTransCo (go co1) (go co2)
......@@ -250,7 +252,6 @@ toIfaceCoercionX fr co
go_prov (PhantomProv co) = IfacePhantomProv (go co)
go_prov (ProofIrrelProv co) = IfaceProofIrrelProv (go co)
go_prov (PluginProv str) = IfacePluginProv str
go_prov (HoleProv h) = IfaceHoleProv (chUnique h)
toIfaceTcArgs :: TyCon -> [Type] -> IfaceTcArgs
toIfaceTcArgs = toIfaceTcArgsX emptyVarSet
......
......@@ -172,7 +172,7 @@ solveCallStack ev ev_cs = do
-- dictionary, so we have to coerce ev_cs to a dictionary for
-- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev))
setWantedEvBind (ctEvId ev) ev_tm
setWantedEvBind (ctEvEvId ev) ev_tm
canClass :: CtEvidence
-> Class -> [Type]
......
......@@ -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
= case closed of
ClosedLet ->
ASSERT2( isEmptyVarSet id_tvs, ppr id $$ ppr (idType id) ) tvs
_ ->
tvs `unionVarSet` id_tvs
where id_tvs = tyCoVarsOfType (idType id)
ClosedLet -> ASSERT2( is_closed_type, ppr id $$ ppr (idType id) )
tvs
_other -> tvs `unionVarSet` id_tvs
where
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]
= tvs `unionVarSet` tyCoVarsOfType (tyVarKind tv) `extendVarSet` tv
......
......@@ -805,9 +805,9 @@ addDeferredBinding ctxt err ct
-> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
HoleDest hole
-> do { -- See Note [Deferred errors for coercion holes]
evar <- newEvVar pred
; addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
; fillCoercionHole hole (mkTcCoVarCo evar) }}
let co_var = coHoleCoVar hole
; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm
; fillCoercionHole hole (mkTcCoVarCo co_var) }}
| otherwise -- Do not set any evidence for Given/Derived
= return ()
......
......@@ -52,6 +52,7 @@ import TcEvidence
import TysPrim
import TyCon ( isUnboxedTupleTyCon )
import TysWiredIn
import TyCoRep( CoercionHole(..) )
import Type
import Coercion
import ConLike
......@@ -1580,35 +1581,30 @@ zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
Just tv' -> return (mkTyVarTy tv')
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
= return $ mkCoVarCo cv'
| otherwise
= mkCoVarCo <$> updateVarTypeM (zonkTcTypeToType env) cv
zonkCoHole :: ZonkEnv -> CoercionHole
-> Role -> Type -> Type -- these are all redundant with
-- the details in the hole,
-- unzonked
-> TcM Coercion
zonkCoHole env h r t1 t2
= do { contents <- unpackCoercionHole_maybe h
= do { cv' <- zonkCoVar cv; return (mkCoVarCo cv') }
zonkCoHole :: ZonkEnv -> CoercionHole -> TcM Coercion
zonkCoHole env hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
= do { contents <- readTcRef ref
; case contents of
Just co -> do { co <- zonkCoToCo env co
; checkCoercionHole co h r t1 t2 }
Just co -> do { co' <- zonkCoToCo env co
; checkCoercionHole cv co' }
-- This next case should happen only in the presence of
-- (undeferred) type errors. Originally, I put in a panic
-- 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 $
whenNoErrs $
MASSERT2( False
, text "Type-correct unfilled coercion hole"
<+> ppr h )
; t1 <- zonkTcTypeToType env t1
; t2 <- zonkTcTypeToType env t2
; return $ mkHoleCo h r t1 t2 } }
<+> ppr hole )
; cv' <- zonkCoVar cv
; return $ mkHoleCo (hole { ch_co_var = cv' }) } }
zonk_tycomapper :: TyCoMapper ZonkEnv TcM
zonk_tycomapper = TyCoMapper
......
......@@ -590,7 +590,7 @@ solveOneFromTheOther ev_i ev_w
| otherwise
= KeepInert
has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
has_binding binds ev = isJust (lookupEvBind binds (ctEvEvId ev))
{-
Note [Replacement vs keeping]
......@@ -990,7 +990,7 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
; try_inst_res <- shortCutSolver dflags ev_w ev_i
; case try_inst_res of
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 }
; stopWith ev_w "interactDict/solved from instance" }
......@@ -2239,7 +2239,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
finish_wanted theta mk_ev
= do { addSolvedDict fl cls xis
; 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)
; stopWith fl "Dict/Top (solved wanted)" }
......
......@@ -79,7 +79,9 @@ module TcMType (
zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind, zonkTcTypeMapper,
zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
zonkEvVar, zonkWC, zonkSimples,
zonkId, zonkCoVar,
zonkCt, zonkSkolemInfo,
tcGetGlobalTyCoVars,
......@@ -172,7 +174,7 @@ newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
-- Deals with both equality and non-equality predicates
newWanted orig t_or_k pty
= 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
return $ CtWanted { ctev_dest = d
, ctev_pred = pty
......@@ -210,12 +212,12 @@ emitWanted origin pty
-- | Emits a new equality constraint
emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
emitWantedEq origin t_or_k role ty1 ty2
= do { hole <- newCoercionHole
= do { hole <- newCoercionHole pty
; loc <- getCtLocM origin (Just t_or_k)
; emitSimple $ mkNonCanonical $
CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
, ctev_nosh = WDeriv, ctev_loc = loc }
; return (mkHoleCo hole role ty1 ty2) }
; return (HoleCo hole) }
where
pty = mkPrimEqPredRole role ty1 ty2
......@@ -254,28 +256,28 @@ predTypeOccName ty = case classifyPredType ty of
************************************************************************
-}
newCoercionHole :: TcM CoercionHole
newCoercionHole
= do { u <- newUnique
; traceTc "New coercion hole:" (ppr u)
newCoercionHole :: TcPredType -> TcM CoercionHole
newCoercionHole pred_ty
= do { co_var <- newEvVar pred_ty
; traceTc "New coercion hole:" (ppr co_var)
; ref <- newMutVar Nothing
; return $ CoercionHole u ref }
; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
-- | Put a value in a coercion hole
fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
fillCoercionHole (CoercionHole u ref) co
fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co
= do {
#if defined(DEBUG)
; cts <- readTcRef ref
; whenIsJust cts $ \old_co ->
pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co)
pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co)
#endif
; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co)
; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co)
; writeTcRef ref (Just co) }
-- | Is a coercion hole filled in?
isFilledCoercionHole :: CoercionHole -> TcM Bool
isFilledCoercionHole (CoercionHole _ ref) = isJust <$> readTcRef ref
isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref
-- | Retrieve the contents of a coercion hole. Panics if the hole
-- is unfilled
......@@ -288,30 +290,36 @@ unpackCoercionHole hole
-- | Retrieve the contents of a coercion hole, if it is filled
unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
unpackCoercionHole_maybe (CoercionHole _ ref) = readTcRef ref
unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
-- | Check that a coercion is appropriate for filling a hole. (The hole
-- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
-- as it's used in TcHsSyn in the presence of knots.
-- Always returns the checked coercion, but this return value is necessary
-- so that the input coercion is forced only when the output is forced.
checkCoercionHole :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion
checkCoercionHole co h r t1 t2
-- co is already zonked, but t1 and t2 might not be
checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
checkCoercionHole cv co
| debugIsOn
= do { t1 <- zonkTcType t1
; t2 <- zonkTcType t2
; let (Pair _t1 _t2, _role) = coercionKindRole co
= do { cv_ty <- zonkTcType (varType cv)
-- co is already zonked, but cv might not be
; return $
ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role
ASSERT2( ok cv_ty
, (text "Bad coercion hole" <+>
ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role
, ppr co, ppr t1, ppr t2
, ppr r ]) )
ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
, ppr cv_ty ]) )
co }
| otherwise
= return co
where
(Pair t1 t2, role) = coercionKindRole co
ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty
= t1 `eqType` cv_t1
&& t2 `eqType` cv_t2
&& role == eqRelRole cv_rel
| otherwise
= False
{-
************************************************************************
*
......@@ -1476,6 +1484,9 @@ zonkId id
= do { ty' <- zonkTcType (idType id)
; return (Id.setIdType id ty') }
zonkCoVar :: CoVar -> TcM CoVar
zonkCoVar = zonkId
-- | A suitable TyCoMapper for zonking a type inside the knot, and
-- before all metavars are filled in.
zonkTcTypeMapper :: TyCoMapper () TcM
......@@ -1486,16 +1497,14 @@ zonkTcTypeMapper = TyCoMapper
, tcm_hole = hole
, tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
where
hole :: () -> CoercionHole -> Role -> Type -> Type
-> TcM Coercion
hole _ h r t1 t2
= do { contents <- unpackCoercionHole_maybe h
hole :: () -> CoercionHole -> TcM Coercion
hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
= do { contents <- readTcRef ref
; case contents of
Just co -> do { co <- zonkCo co
; checkCoercionHole co h r t1 t2 }
Nothing -> do { t1 <- zonkTcType t1
; t2 <- zonkTcType t2
; return $ mkHoleCo h r t1 t2 } }
Just co -> do { co' <- zonkCo co
; checkCoercionHole cv co' }
Nothing -> do { cv' <- zonkCoVar cv
; return $ HoleCo (hole { ch_co_var = cv' }) } }
-- For unbound, mutable tyvars, zonkType uses the function given to it
......
......@@ -181,8 +181,8 @@ newEvVar :: PredType -> TcPluginM EvVar
newEvVar = unsafeTcPluginTcM . TcM.newEvVar
-- | Create a fresh coercion hole.
newCoercionHole :: TcPluginM CoercionHole
newCoercionHole = unsafeTcPluginTcM $ TcM.newCoercionHole
newCoercionHole :: PredType -> TcPluginM CoercionHole
newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole
-- | Bind an evidence variable. This must not be invoked from
-- 'tcPluginInit' or 'tcPluginStop', or it will panic.
......
......@@ -74,11 +74,11 @@ module TcRnTypes(
isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
isUserTypeErrorCt, getUserTypeErrorMsg,
ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
mkTcEqPredLikeEv,
ctEvId, mkTcEqPredLikeEv,
mkNonCanonical, mkNonCanonicalCt, mkGivens,
mkIrredCt, mkInsolubleCt,
ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
ctEvTerm, ctEvCoercion, ctEvId,
ctEvTerm, ctEvCoercion, ctEvEvId,
tyCoVarsOfCt, tyCoVarsOfCts,
tyCoVarsOfCtList, tyCoVarsOfCtsList,
......@@ -151,6 +151,7 @@ import TcEvidence
import Type
import Class ( Class )
import TyCon ( TyCon, tyConKind )
import TyCoRep ( CoercionHole(..), coHoleCoVar )
import Coercion ( Coercion, mkHoleCo )
import ConLike ( ConLike(..) )
import DataCon ( DataCon, dataConUserType, dataConOrigArgTys )
......@@ -1790,6 +1791,10 @@ ctPred :: Ct -> PredType
-- See Note [Ct/evidence invariant]
ctPred ct = ctEvPred (cc_ev ct)
ctEvId :: Ct -> EvVar
-- The evidence Id for this Ct
ctEvId ct = ctEvEvId (ctEvidence ct)
-- | Makes a new equality predicate with the same role as the given
-- evidence.
mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType
......@@ -2644,26 +2649,26 @@ ctEvRole = eqRelRole . ctEvEqRel
ctEvTerm :: CtEvidence -> EvTerm
ctEvTerm ev@(CtWanted { ctev_dest = HoleDest _ }) = EvCoercion $ ctEvCoercion ev
ctEvTerm ev = EvId (ctEvId ev)
ctEvTerm ev = EvId (ctEvEvId ev)
-- Always returns a coercion whose type is precisely ctev_pred of the CtEvidence.
-- See also Note [Given in ctEvCoercion]
ctEvCoercion :: CtEvidence -> Coercion
ctEvCoercion (CtGiven { ctev_pred = pred_ty, ctev_evar = ev_id })
= mkTcCoVarCo (setVarType ev_id pred_ty) -- See Note [Given in ctEvCoercion]
ctEvCoercion (CtWanted { ctev_dest = dest, ctev_pred = pred })
ctEvCoercion (CtWanted { ctev_dest = dest })
| HoleDest hole <- dest
, Just (role, ty1, ty2) <- getEqPredTys_maybe pred
= -- ctEvCoercion is only called on type equalities
-- and they always have HoleDests
mkHoleCo hole role ty1 ty2
mkHoleCo hole
ctEvCoercion ev
= pprPanic "ctEvCoercion" (ppr ev)
ctEvId :: CtEvidence -> TcId
ctEvId (CtWanted { ctev_dest = EvVarDest ev }) = ev
ctEvId (CtGiven { ctev_evar = ev }) = ev
ctEvId ctev = pprPanic "ctEvId:" (ppr ctev)
ctEvEvId :: CtEvidence -> EvVar
ctEvEvId (CtWanted { ctev_dest = EvVarDest ev }) = ev
ctEvEvId (CtWanted { ctev_dest = HoleDest h }) = coHoleCoVar h
ctEvEvId (CtGiven { ctev_evar = ev }) = ev
ctEvEvId ctev@(CtDerived {}) = pprPanic "ctEvId:" (ppr ctev)
instance Outputable TcEvDest where
ppr (HoleDest h) = text "hole" <> ppr h
......
......@@ -3079,12 +3079,12 @@ emitNewWantedEq loc role ty1 ty2
-- | Make a new equality CtEvidence
newWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion)
newWantedEq loc role ty1 ty2
= do { hole <- wrapTcS $ TcM.newCoercionHole
= do { hole <- wrapTcS $ TcM.newCoercionHole pty
; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
, ctev_nosh = WDeriv
, ctev_loc = loc}
, mkHoleCo hole role ty1 ty2 ) }
, mkHoleCo hole ) }
where
pty = mkPrimEqPredRole role ty1 ty2
......
......@@ -117,6 +117,7 @@ synonymTyConsOfType ty
go_co (ForAllCo