Commit 857ef25e authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix and document cloneWC

The cloneWC, cloneWanted, cloneImplication family are used by
  * TcHoleErrors
  * TcRule
to clone the /bindings/ in a constraint, so that solving the
constraint will not add bindings to the program. The idea is only
to affect unifications.

But I had it wrong -- I failed to clone the EvBindsVar of an
implication.  That gave an assert failure, I think, as well as
useless dead code.

The fix is easy.  I'm not adding a test case.

In the type 'TcEvidence.EvBindsVar', I also renamed the
'NoEvBindsVar' constructor to 'CoEvBindsVar'.  It's not that we
have /no/ evidence bindings, just that we can only have coercion
bindings, done via HoleDest.
parent c5d31df7
......@@ -408,7 +408,7 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope
implic' = implic { ic_skols = tvs'
, ic_given = map (tidyEvVar env1) given
, ic_info = info' }
ctxt1 | NoEvBindsVar{} <- evb = noDeferredBindings ctxt
ctxt1 | CoEvBindsVar{} <- evb = noDeferredBindings ctxt
| otherwise = ctxt
-- If we go inside an implication that has no term
-- evidence (e.g. unifying under a forall), we can't defer
......
......@@ -16,7 +16,7 @@ module TcEvidence (
lookupEvBind, evBindMapBinds, foldEvBindMap, filterEvBindMap,
isEmptyEvBindMap,
EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
evBindVar, isNoEvBindsVar,
evBindVar, isCoEvBindsVar,
-- EvTerm (already a CoreExpr)
EvTerm(..), EvExpr,
......@@ -408,7 +408,7 @@ data EvBindsVar
-- See Note [Tracking redundant constraints] in TcSimplify
}
| NoEvBindsVar { -- See Note [No evidence bindings]
| CoEvBindsVar { -- See Note [Coercion evidence only]
-- See above for comments on ebv_uniq, evb_tcvs
ebv_uniq :: Unique,
......@@ -421,11 +421,11 @@ instance Data.Data TcEvBinds where
gunfold _ _ = error "gunfold"
dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
{- Note [No evidence bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
{- Note [Coercion evidence only]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Class constraints etc give rise to /term/ bindings for evidence, and
we have nowhere to put term bindings in /types/. So in some places we
use NoEvBindsVar (see newNoTcEvBinds) to signal that no term-level
use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level
evidence bindings are allowed. Notebly ():
- Places in types where we are solving kind constraints (all of which
......@@ -435,9 +435,9 @@ evidence bindings are allowed. Notebly ():
- When unifying forall-types
-}
isNoEvBindsVar :: EvBindsVar -> Bool
isNoEvBindsVar (NoEvBindsVar {}) = True
isNoEvBindsVar (EvBindsVar {}) = False
isCoEvBindsVar :: EvBindsVar -> Bool
isCoEvBindsVar (CoEvBindsVar {}) = True
isCoEvBindsVar (EvBindsVar {}) = False
-----------------
newtype EvBindMap
......@@ -928,8 +928,8 @@ instance Outputable TcEvBinds where
instance Outputable EvBindsVar where
ppr (EvBindsVar { ebv_uniq = u })
= text "EvBindsVar" <> angleBrackets (ppr u)
ppr (NoEvBindsVar { ebv_uniq = u })
= text "NoEvBindsVar" <> angleBrackets (ppr u)
ppr (CoEvBindsVar { ebv_uniq = u })
= text "CoEvBindsVar" <> angleBrackets (ppr u)
instance Uniquable EvBindsVar where
getUnique = ebv_uniq
......
......@@ -955,7 +955,7 @@ tcCheckHoleFit relevantCts implics hole_ty ty = discardErrs $
else do { fresh_binds <- newTcEvBinds
-- The relevant constraints may contain HoleDests, so we must
-- take care to clone them as well (to avoid #15370).
; cloned_relevants <- mapBagM cloneSimple relevantCts
; cloned_relevants <- mapBagM cloneWanted relevantCts
-- We wrap the WC in the nested implications, see
-- Note [Nested Implications]
; let outermost_first = reverse implics
......
......@@ -1549,7 +1549,7 @@ zonkEvBindsVar :: ZonkEnv -> EvBindsVar -> TcM (ZonkEnv, Bag EvBind)
zonkEvBindsVar env (EvBindsVar { ebv_binds = ref })
= do { bs <- readMutVar ref
; zonkEvBinds env (evBindMapBinds bs) }
zonkEvBindsVar env (NoEvBindsVar {}) = return (env, emptyBag)
zonkEvBindsVar env (CoEvBindsVar {}) = return (env, emptyBag)
zonkEvBinds :: ZonkEnv -> Bag EvBind -> TcM (ZonkEnv, Bag EvBind)
zonkEvBinds env binds
......
......@@ -1082,7 +1082,7 @@ shortCutSolver dflags ev_w ev_i
&& gopt Opt_SolveConstantDicts dflags
-- Enabled by the -fsolve-constant-dicts flag
= do { ev_binds_var <- getTcEvBindsVar
; ev_binds <- ASSERT2( not (isNoEvBindsVar ev_binds_var ), ppr ev_w )
; ev_binds <- ASSERT2( not (isCoEvBindsVar ev_binds_var ), ppr ev_w )
getTcEvBindsMap ev_binds_var
; solved_dicts <- getSolvedDicts
......@@ -2267,7 +2267,7 @@ chooseInstance work_item
-- Precondition: evidence term matches the predicate workItem
finish_wanted loc theta mk_ev
= do { evb <- getTcEvBindsVar
; if isNoEvBindsVar evb
; if isCoEvBindsVar evb
then -- See Note [Instances in no-evidence implications]
continueWith work_item
else
......
......@@ -39,7 +39,7 @@ module TcMType (
--------------------------------
-- Creating new evidence variables
newEvVar, newEvVars, newDict,
newWanted, newWanteds, cloneWanted, cloneSimple, cloneWC,
newWanted, newWanteds, cloneWanted, cloneWC,
emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
newTcEvBinds, newNoTcEvBinds, addTcEvBind,
......@@ -181,24 +181,38 @@ newWanted orig t_or_k pty
newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
newWanteds orig = mapM (newWanted orig Nothing)
cloneWanted :: Ct -> TcM CtEvidence
cloneWanted ct
= newWanted (ctEvOrigin ev) Nothing (ctEvPred ev)
where
ev = ctEvidence ct
----------------------------------------------
-- Cloning constraints
----------------------------------------------
cloneSimple :: Ct -> TcM Ct
cloneSimple = fmap mkNonCanonical . cloneWanted
cloneWanted :: Ct -> TcM Ct
cloneWanted ct
| ev@(CtWanted { ctev_dest = HoleDest {}, ctev_pred = pty }) <- ctEvidence ct
= do { co_hole <- newCoercionHole pty
; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) }
| otherwise
= return ct
cloneWC :: WantedConstraints -> TcM WantedConstraints
-- Clone all the evidence bindings in
-- a) the ic_bind field of any implications
-- b) the CoercionHoles of any wanted constraints
-- so that solving the WantedConstraints will not have any visible side
-- effect, /except/ from causing unifications
cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
= do { simples' <- mapBagM cloneSimple simples
; implics' <- mapBagM clone_implic implics
= do { simples' <- mapBagM cloneWanted simples
; implics' <- mapBagM cloneImplication implics
; return (wc { wc_simple = simples', wc_impl = implics' }) }
where
clone_implic implic@(Implic { ic_wanted = inner_wanted })
= do { inner_wanted' <- cloneWC inner_wanted
; return (implic { ic_wanted = inner_wanted' }) }
cloneImplication :: Implication -> TcM Implication
cloneImplication implic@(Implic { ic_binds = binds, ic_wanted = inner_wanted })
= do { binds' <- cloneEvBindsVar binds
; inner_wanted' <- cloneWC inner_wanted
; return (implic { ic_binds = binds', ic_wanted = inner_wanted' }) }
----------------------------------------------
-- Emitting constraints
----------------------------------------------
-- | Emits a new Wanted. Deals with both equalities and non-equalities.
emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
......
......@@ -89,7 +89,7 @@ module TcRnMonad(
mkErrInfo,
-- * Type constraints
newTcEvBinds, newNoTcEvBinds,
newTcEvBinds, newNoTcEvBinds, cloneEvBindsVar,
addTcEvBind,
getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
chooseUniqueOccTc,
......@@ -1372,9 +1372,21 @@ newNoTcEvBinds
= do { tcvs_ref <- newTcRef emptyVarSet
; uniq <- newUnique
; traceTc "newNoTcEvBinds" (text "unique =" <+> ppr uniq)
; return (NoEvBindsVar { ebv_tcvs = tcvs_ref
; return (CoEvBindsVar { ebv_tcvs = tcvs_ref
, ebv_uniq = uniq }) }
cloneEvBindsVar :: EvBindsVar -> TcM EvBindsVar
-- Clone the refs, so that any binding created when
-- solving don't pollute the original
cloneEvBindsVar ebv@(EvBindsVar {})
= do { binds_ref <- newTcRef emptyEvBindMap
; tcvs_ref <- newTcRef emptyVarSet
; return (ebv { ebv_binds = binds_ref
, ebv_tcvs = tcvs_ref }) }
cloneEvBindsVar ebv@(CoEvBindsVar {})
= do { tcvs_ref <- newTcRef emptyVarSet
; return (ebv { ebv_tcvs = tcvs_ref }) }
getTcEvTyCoVars :: EvBindsVar -> TcM TyCoVarSet
getTcEvTyCoVars ev_binds_var
= readTcRef (ebv_tcvs ev_binds_var)
......@@ -1382,13 +1394,13 @@ getTcEvTyCoVars ev_binds_var
getTcEvBindsMap :: EvBindsVar -> TcM EvBindMap
getTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref })
= readTcRef ev_ref
getTcEvBindsMap (NoEvBindsVar {})
getTcEvBindsMap (CoEvBindsVar {})
= return emptyEvBindMap
setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcM ()
setTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref }) binds
= writeTcRef ev_ref binds
setTcEvBindsMap v@(NoEvBindsVar {}) ev_binds
setTcEvBindsMap v@(CoEvBindsVar {}) ev_binds
| isEmptyEvBindMap ev_binds
= return ()
| otherwise
......@@ -1401,8 +1413,8 @@ addTcEvBind (EvBindsVar { ebv_binds = ev_ref, ebv_uniq = u }) ev_bind
ppr ev_bind
; bnds <- readTcRef ev_ref
; writeTcRef ev_ref (extendEvBinds bnds ev_bind) }
addTcEvBind (NoEvBindsVar { ebv_uniq = u }) ev_bind
= pprPanic "addTcEvBind NoEvBindsVar" (ppr ev_bind $$ ppr u)
addTcEvBind (CoEvBindsVar { ebv_uniq = u }) ev_bind
= pprPanic "addTcEvBind CoEvBindsVar" (ppr ev_bind $$ ppr u)
chooseUniqueOccTc :: (OccSet -> OccName) -> TcM OccName
chooseUniqueOccTc fn =
......
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