Fix and document cloneWC
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 25 Jul 2018 10:47:45 +0000 (11:47 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 25 Jul 2018 11:04:31 +0000 (12:04 +0100)
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.

compiler/typecheck/TcErrors.hs
compiler/typecheck/TcEvidence.hs
compiler/typecheck/TcHoleErrors.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcRnMonad.hs

index 355a9e3..ecb4042 100644 (file)
@@ -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
index 50c49bc..e6cbfed 100644 (file)
@@ -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
index 7dde74f..1f6e068 100644 (file)
@@ -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
index 73fdda9..a4a2562 100644 (file)
@@ -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
index 18d9525..9b50b09 100644 (file)
@@ -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
index 873b50b..1a13cb9 100644 (file)
@@ -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
index 4382467..aa95c1e 100644 (file)
@@ -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 =