Commit 832f8db2 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Implement a fast path for new constraints looking like (a~b), namely unifyWanted

Looking at some typechecker traces I could see places where we were laboriously
creating a Refl coercion.  This patch short-circuits the process.

See TcCanonical:
  Note [unifyWanted and unifyDerived]
  Note [Decomposing TyConApps]

I ended up with some refactoring, notably

  * I moved xCtEvidence, rewriteEvidence, rewriteEqEvidence
    from TcSMonad to TcCanonical

There are some knock-on effects, but only minor ones.
parent bcb967ab
{-# LANGUAGE CPP #-}
module TcCanonical( canonicalize ) where
module TcCanonical(
canonicalize,
unifyDerived,
StopOrContinue(..), stopWith, continueWith
) where
#include "HsVersions.h"
......@@ -18,12 +23,14 @@ import Var
import Name( isSystemName )
import OccName( OccName )
import Outputable
import Control.Monad ( when )
import Control.Monad
import DynFlags( DynFlags )
import VarSet
import Pair
import Util
import BasicTypes
import FastString
{-
************************************************************************
......@@ -427,7 +434,9 @@ can_eq_nc' ev (TyConApp tc1 _) ps_ty1 (FunTy {}) ps_ty2
= canEqFailure ev ps_ty1 ps_ty2
can_eq_nc' ev (FunTy s1 t1) _ (FunTy s2 t2) _
= canDecomposableTyConAppOK ev funTyCon [s1,t1] [s2,t2]
= do { canDecomposableTyConAppOK ev funTyCon [s1,t1] [s2,t2]
; stopWith ev "Decomposed FunTyCon" }
can_eq_nc' ev (FunTy {}) ps_ty1 (TyConApp tc2 _) ps_ty2
| isDecomposableTyCon tc2
......@@ -517,14 +526,11 @@ try_decompose_app ev ty1 ty2
= do { emitNewDerived loc (mkTcEqPred t1 t2)
; try_decompose_app ev s1 s2 }
| CtWanted { ctev_evar = evar, ctev_loc = loc } <- ev
= do { (ev_s,fr_s) <- newWantedEvVar loc (mkTcEqPred s1 s2)
; (ev_t,fr_t) <- newWantedEvVar loc (mkTcEqPred t1 t2)
; let co = mkTcAppCo (ctEvCoercion ev_s) (ctEvCoercion ev_t)
= do { ev_s <- newWantedEvVarNC loc (mkTcEqPred s1 s2)
; co_t <- unifyWanted loc t1 t2
; let co = mkTcAppCo (ctEvCoercion ev_s) co_t
; setEvBind evar (EvCoercion co)
; when (isFresh fr_t) $ emitWorkNC [ev_t]
; case fr_s of
Fresh -> try_decompose_app ev_s s1 s2
Cached -> return (Stop ev (text "Decomposed app")) }
; try_decompose_app ev_s s1 s2 }
| CtGiven { ctev_evtm = ev_tm, ctev_loc = loc } <- ev
= do { let co = evTermCoercion ev_tm
co_s = mkTcLRCo CLeft co
......@@ -541,25 +547,38 @@ canDecomposableTyConApp :: CtEvidence
-> TyCon -> [TcType]
-> TyCon -> [TcType]
-> TcS (StopOrContinue Ct)
-- See Note [Decomposing TyConApps]
canDecomposableTyConApp ev tc1 tys1 tc2 tys2
| tc1 /= tc2 || length tys1 /= length tys2
-- Fail straight away for better error messages
= canEqFailure ev (mkTyConApp tc1 tys1) (mkTyConApp tc2 tys2)
| otherwise
= do { traceTcS "canDecomposableTyConApp" (ppr ev $$ ppr tc1 $$ ppr tys1 $$ ppr tys2)
; canDecomposableTyConAppOK ev tc1 tys1 tys2 }
; canDecomposableTyConAppOK ev tc1 tys1 tys2
; stopWith ev "Decomposed TyConApp" }
canDecomposableTyConAppOK :: CtEvidence
-> TyCon -> [TcType] -> [TcType]
-> TcS (StopOrContinue Ct)
-> TcS ()
-- Precondition: tys1 and tys2 are the same length, hence "OK"
canDecomposableTyConAppOK ev tc1 tys1 tys2
= do { let xcomp xs = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
xev = XEvTerm (zipWith mkTcEqPred tys1 tys2) xcomp xdecomp
; xCtEvidence ev xev
; stopWith ev "Decomposed TyConApp" }
= case ev of
CtDerived { ctev_loc = loc }
-> mapM_ (unifyDerived loc) (zipWith Pair tys1 tys2)
CtWanted { ctev_evar = evar, ctev_loc = loc }
-> do { cos <- zipWithM (unifyWanted loc) tys1 tys2
; setEvBind evar (EvCoercion (mkTcTyConAppCo Nominal tc1 cos)) }
CtGiven { ctev_evtm = ev_tm, ctev_loc = loc }
-> do { given_evs <- newGivenEvVars loc $
zipWith3 (mk_given ev_tm) tys1 tys2 [0..]
; emitWorkNC given_evs }
where
mk_given ev_tm ty1 ty2 i
= (mkTcEqPred ty1 ty2, EvCoercion (mkTcNthCo i (evTermCoercion ev_tm)))
--------------------
canEqFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct)
-- See Note [Make sure that insolubles are fully rewritten]
canEqFailure ev ty1 ty2
......@@ -572,6 +591,20 @@ canEqFailure ev ty1 ty2
Stop ev s -> pprPanic "canEqFailure" (s $$ ppr ev $$ ppr ty1 $$ ppr ty2) }
{-
Note [Decomposing TyConApps]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
(s1 ~ s2, t1 ~ t2)
and push those back into the work list. But if
s1 = K k1 s2 = K k2
then we will jus decomopose s1~s2, and it might be better to
do so on the spot. An important special case is where s1=s2,
and we get just Refl.
So canDecomposableTyCon is a fast-path decomposition that uses
unifyWanted etc to short-cut that work.
Note [Canonicalising type applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given (s1 t1) ~ ty2, how should we proceed?
......@@ -1027,3 +1060,321 @@ we first try expanding each of the ti to types which no longer contain
a. If this turns out to be impossible, we next try expanding F
itself, and so on. See Note [Occurs check expansion] in TcType
-}
{-
************************************************************************
* *
Evidence transformation
* *
************************************************************************
-}
{-
Note [xCtEvidence]
~~~~~~~~~~~~~~~~~~
A call might look like this:
xCtEvidence ev evidence-transformer
ev is Given => use ev_decomp to create new Givens for ev_preds,
and return them
ev is Wanted => create new wanteds for ev_preds,
use ev_comp to bind ev,
return fresh wanteds (ie ones not cached in inert_cans or solved)
ev is Derived => create new deriveds for ev_preds
(unless cached in inert_cans or solved)
Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
Ones that are already cached are not returned
Example
ev : Tree a b ~ Tree c d
xCtEvidence ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
, ev_decomp = \c. [nth 1 c, nth 2 c] })
(\fresh-goals. stuff)
Note [Bind new Givens immediately]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For Givens we make new EvVars and bind them immediately. We don't worry
about caching, but we don't expect complicated calculations among Givens.
It is important to bind each given:
class (a~b) => C a b where ....
f :: C a b => ....
Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
But that superclass selector can't (yet) appear in a coercion
(see evTermCoercion), so the easy thing is to bind it to an Id.
See Note [Coercion evidence terms] in TcEvidence.
-}
xCtEvidence :: CtEvidence -- Original evidence
-> XEvTerm -- Instructions about how to manipulate evidence
-> TcS ()
xCtEvidence (CtWanted { ctev_evar = evar, ctev_loc = loc })
(XEvTerm { ev_preds = ptys, ev_comp = comp_fn })
= do { new_evars <- mapM (newWantedEvVar loc) ptys
; setEvBind evar (comp_fn (map (ctEvTerm . fst) new_evars))
; emitWorkNC (freshGoals new_evars) }
-- Note the "NC": these are fresh goals, not necessarily canonical
xCtEvidence (CtGiven { ctev_evtm = tm, ctev_loc = loc })
(XEvTerm { ev_preds = ptys, ev_decomp = decomp_fn })
= ASSERT( equalLength ptys (decomp_fn tm) )
do { given_evs <- newGivenEvVars loc (ptys `zip` decomp_fn tm)
; emitWorkNC given_evs }
xCtEvidence (CtDerived { ctev_loc = loc })
(XEvTerm { ev_preds = ptys })
= mapM_ (emitNewDerived loc) ptys
-----------------------------
data StopOrContinue a
= ContinueWith a -- The constraint was not solved, although it may have
-- been rewritten
| Stop CtEvidence -- The (rewritten) constraint was solved
SDoc -- Tells how it was solved
-- Any new sub-goals have been put on the work list
instance Functor StopOrContinue where
fmap f (ContinueWith x) = ContinueWith (f x)
fmap _ (Stop ev s) = Stop ev s
instance Outputable a => Outputable (StopOrContinue a) where
ppr (Stop ev s) = ptext (sLit "Stop") <> parens s <+> ppr ev
ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
continueWith :: a -> TcS (StopOrContinue a)
continueWith = return . ContinueWith
stopWith :: CtEvidence -> String -> TcS (StopOrContinue a)
stopWith ev s = return (Stop ev (text s))
andWhenContinue :: TcS (StopOrContinue a)
-> (a -> TcS (StopOrContinue b))
-> TcS (StopOrContinue b)
andWhenContinue tcs1 tcs2
= do { r <- tcs1
; case r of
Stop ev s -> return (Stop ev s)
ContinueWith ct -> tcs2 ct }
rewriteEvidence :: CtEvidence -- old evidence
-> TcPredType -- new predicate
-> TcCoercion -- Of type :: new predicate ~ <type of old evidence>
-> TcS (StopOrContinue CtEvidence)
-- Returns Just new_ev iff either (i) 'co' is reflexivity
-- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
-- In either case, there is nothing new to do with new_ev
{-
rewriteEvidence old_ev new_pred co
Main purpose: create new evidence for new_pred;
unless new_pred is cached already
* Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev
* If old_ev was wanted, create a binding for old_ev, in terms of new_ev
* If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev
* Returns Nothing if new_ev is already cached
Old evidence New predicate is Return new evidence
flavour of same flavor
-------------------------------------------------------------------
Wanted Already solved or in inert Nothing
or Derived Not Just new_evidence
Given Already in inert Nothing
Not Just new_evidence
Note [Rewriting with Refl]
~~~~~~~~~~~~~~~~~~~~~~~~~~
If the coercion is just reflexivity then you may re-use the same
variable. But be careful! Although the coercion is Refl, new_pred
may reflect the result of unification alpha := ty, so new_pred might
not _look_ the same as old_pred, and it's vital to proceed from now on
using new_pred.
The flattener preserves type synonyms, so they should appear in new_pred
as well as in old_pred; that is important for good error messages.
-}
rewriteEvidence old_ev@(CtDerived { ctev_loc = loc }) new_pred _co
= -- If derived, don't even look at the coercion.
-- This is very important, DO NOT re-order the equations for
-- rewriteEvidence to put the isTcReflCo test first!
-- Why? Because for *Derived* constraints, c, the coercion, which
-- was produced by flattening, may contain suspended calls to
-- (ctEvTerm c), which fails for Derived constraints.
-- (Getting this wrong caused Trac #7384.)
do { mb_ev <- newDerived loc new_pred
; case mb_ev of
Just new_ev -> continueWith new_ev
Nothing -> stopWith old_ev "Cached derived" }
rewriteEvidence old_ev new_pred co
| isTcReflCo co -- See Note [Rewriting with Refl]
= return (ContinueWith (old_ev { ctev_pred = new_pred }))
rewriteEvidence (CtGiven { ctev_evtm = old_tm , ctev_loc = loc }) new_pred co
= do { new_ev <- newGivenEvVar loc (new_pred, new_tm) -- See Note [Bind new Givens immediately]
; return (ContinueWith new_ev) }
where
new_tm = mkEvCast old_tm (mkTcSubCo (mkTcSymCo co)) -- mkEvCast optimises ReflCo
rewriteEvidence ev@(CtWanted { ctev_evar = evar, ctev_loc = loc }) new_pred co
= do { (new_ev, freshness) <- newWantedEvVar loc new_pred
; MASSERT( tcCoercionRole co == Nominal )
; setEvBind evar (mkEvCast (ctEvTerm new_ev) (mkTcSubCo co))
; case freshness of
Fresh -> continueWith new_ev
Cached -> stopWith ev "Cached wanted" }
rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped)
-- or orhs ~ olhs (swapped)
-> SwapFlag
-> TcType -> TcType -- New predicate nlhs ~ nrhs
-- Should be zonked, because we use typeKind on nlhs/nrhs
-> TcCoercion -- lhs_co, of type :: nlhs ~ olhs
-> TcCoercion -- rhs_co, of type :: nrhs ~ orhs
-> TcS (StopOrContinue CtEvidence) -- Of type nlhs ~ nrhs
-- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co)
-- we generate
-- If not swapped
-- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co
-- If 'swapped'
-- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co
--
-- For (Wanted w) we do the dual thing.
-- New w1 : nlhs ~ nrhs
-- If not swapped
-- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co
-- If swapped
-- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co
--
-- It's all a form of rewwriteEvidence, specialised for equalities
rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co
| CtDerived { ctev_loc = loc } <- old_ev
= do { mb <- newDerived loc new_pred
; case mb of
Just new_ev -> continueWith new_ev
Nothing -> stopWith old_ev "Cached derived" }
| NotSwapped <- swapped
, isTcReflCo lhs_co -- See Note [Rewriting with Refl]
, isTcReflCo rhs_co
= return (ContinueWith (old_ev { ctev_pred = new_pred }))
| CtGiven { ctev_evtm = old_tm , ctev_loc = loc } <- old_ev
= do { let new_tm = EvCoercion (lhs_co
`mkTcTransCo` maybeSym swapped (evTermCoercion old_tm)
`mkTcTransCo` mkTcSymCo rhs_co)
; new_ev <- newGivenEvVar loc (new_pred, new_tm) -- See Note [Bind new Givens immediately]
; return (ContinueWith new_ev) }
| CtWanted { ctev_evar = evar, ctev_loc = loc } <- old_ev
= do { new_evar <- newWantedEvVarNC loc new_pred
; let co = maybeSym swapped $
mkTcSymCo lhs_co
`mkTcTransCo` ctEvCoercion new_evar
`mkTcTransCo` rhs_co
; setEvBind evar (EvCoercion co)
; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co])
; return (ContinueWith new_evar) }
| otherwise
= panic "rewriteEvidence"
where
new_pred = mkTcEqPred nlhs nrhs
{- Note [unifyWanted and unifyDerived]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When decomposing equalities we often create new wanted constraints for
(s ~ t). But what if s=t? Then it'd be faster to return Refl right away.
Similar remarks apply for Derived.
Rather than making an equality test (which traverses the structure of the
type, perhaps fruitlessly, unifyWanted traverses the common structure, and
bales out when it finds a difference by creating a new Wanted constraint.
But where it succeeds in finding common structure, it just builds a coercion
to reflect it.
-}
unifyWanted :: CtLoc -> TcType -> TcType -> TcS TcCoercion
-- Return coercion witnessing the equality of the two types,
-- emitting new work equalities where necessary to achieve that
-- Very good short-cut when the two types are equal, or nearly so
-- See Note [unifyWanted and unifyDerived]
unifyWanted loc orig_ty1 orig_ty2
= go orig_ty1 orig_ty2
where
go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
go (FunTy s1 t1) (FunTy s2 t2)
= do { co_s <- unifyWanted loc s1 s2
; co_t <- unifyWanted loc t1 t2
; return (mkTcTyConAppCo Nominal funTyCon [co_s,co_t]) }
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
= do { cos <- zipWithM (unifyWanted loc) tys1 tys2
; return (mkTcTyConAppCo Nominal tc1 cos) }
go (TyVarTy tv) ty2
= do { mb_ty <- isFilledMetaTyVar_maybe tv
; case mb_ty of
Just ty1' -> go ty1' ty2
Nothing -> bale_out }
go ty1 (TyVarTy tv)
= do { mb_ty <- isFilledMetaTyVar_maybe tv
; case mb_ty of
Just ty2' -> go ty1 ty2'
Nothing -> bale_out }
go _ _ = bale_out
bale_out = do { ev <- newWantedEvVarNC loc (mkTcEqPred orig_ty1 orig_ty2)
; emitWorkNC [ev]
; return (ctEvCoercion ev) }
unifyDeriveds :: CtLoc -> [TcType] -> [TcType] -> TcS ()
-- See Note [unifyWanted and unifyDerived]
unifyDeriveds loc tys1 tys2 = zipWithM_ (unify_derived loc) tys1 tys2
unifyDerived :: CtLoc -> Pair TcType -> TcS ()
-- See Note [unifyWanted and unifyDerived]
unifyDerived loc (Pair ty1 ty2) = unify_derived loc ty1 ty2
unify_derived :: CtLoc -> TcType -> TcType -> TcS ()
-- Create new Derived and put it in the work list
-- Should do nothing if the two types are equal
-- See Note [unifyWanted and unifyDerived]
unify_derived loc orig_ty1 orig_ty2
= go orig_ty1 orig_ty2
where
go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
go (FunTy s1 t1) (FunTy s2 t2)
= do { unify_derived loc s1 s2
; unify_derived loc t1 t2 }
go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
| tc1 == tc2, isDecomposableTyCon tc1, tys1 `equalLength` tys2
= unifyDeriveds loc tys1 tys2
go (TyVarTy tv) ty2
= do { mb_ty <- isFilledMetaTyVar_maybe tv
; case mb_ty of
Just ty1' -> go ty1' ty2
Nothing -> bale_out }
go ty1 (TyVarTy tv)
= do { mb_ty <- isFilledMetaTyVar_maybe tv
; case mb_ty of
Just ty2' -> go ty1 ty2'
Nothing -> bale_out }
go _ _ = bale_out
bale_out = emitNewDerived loc (mkTcEqPred orig_ty1 orig_ty2)
maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
maybeSym IsSwapped co = mkTcSymCo co
maybeSym NotSwapped co = co
......@@ -684,7 +684,7 @@ interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
= do { let matching_funeqs = findFunEqsByTyCon funeqs tc
; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk)
do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev })
= mapM_ (emitNewDerivedEq (ctEvLoc iev))
= mapM_ (unifyDerived (ctEvLoc iev))
(interact iargs (lookupFlattenTyVar eqs ifsk))
do_one ct = pprPanic "interactFunEq" (ppr ct)
; mapM_ do_one matching_funeqs
......@@ -1496,7 +1496,7 @@ instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
; mapM_ (do_one subst) eqs }
where
do_one subst (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
= emitNewDerivedEq loc (Pair (Type.substTy subst ty1) (Type.substTy subst ty2))
= unifyDerived loc (Pair (Type.substTy subst ty1) (Type.substTy subst ty2))
{-
*********************************************************************************
......@@ -1629,6 +1629,9 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
| otherwise -- We must not assign ufsk := ...ufsk...!
-> do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
; emitWorkNC [new_ev]
-- By emitting this as non-canonical, we deal with all
-- flattening, occurs-check, and ufsk := ufsk issues
; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
-- ax_co :: fam_tc args ~ rhs_ty
-- ev :: alpha ~ rhs_ty
......@@ -1639,9 +1642,6 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
vcat [ text "old_ev:" <+> ppr old_ev
, nest 2 (text ":=") <+> ppr final_co
, text "new_ev:" <+> ppr new_ev ]
; emitWorkNC [new_ev]
-- By emitting this as non-canonical, we deal with all
-- flattening, occurs-check, and ufsk := ufsk issues
; stopWith old_ev "Fun/Top (wanted)" } } }
where
loc = ctEvLoc old_ev
......@@ -1651,7 +1651,7 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
= do { inert_eqs <- getInertEqs
; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
; mapM_ (emitNewDerivedEq loc) eqns }
; mapM_ (unifyDerived loc) eqns }
| otherwise
= return ()
......@@ -2190,9 +2190,8 @@ requestCoercible :: CtLoc -> TcType -> TcType
, TcCoercion ) -- Coercion witnessing (Coercible t1 t2)
requestCoercible loc ty1 ty2
= ASSERT2( typeKind ty1 `tcEqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
do { (new_ev, freshness) <- newWantedEvVar loc' (mkCoerciblePred ty1 ty2)
; return ( case freshness of { Fresh -> [new_ev]; Cached -> [] }
, ctEvCoercion new_ev) }
do { new_ev <- newWantedEvVarNC loc' (mkCoerciblePred ty1 ty2)
; return ( [new_ev], ctEvCoercion new_ev) }
-- Evidence for a Coercible constraint is always a coercion t1 ~R t2
where
loc' = bumpCtLocDepth CountConstraints loc
......
......@@ -26,18 +26,11 @@ module TcSMonad (
XEvTerm(..),
Freshness(..), freshGoals, isFresh,
StopOrContinue(..), continueWith, stopWith, andWhenContinue,
xCtEvidence, -- Transform a CtEvidence during a step
rewriteEvidence, -- Specialized version of xCtEvidence for coercions
rewriteEqEvidence, -- Yet more specialised, for equality coercions
maybeSym,
newTcEvBinds, newWantedEvVar, newWantedEvVarNC,
setWantedTyBind, reportUnifications,
setEvBind,
newEvVar, newGivenEvVar,
emitNewDerived, emitNewDerivedEq,
newEvVar, newGivenEvVar, newGivenEvVars,
newDerived, emitNewDerived,
instDFunConstraints,
getInstEnvs, getFamInstEnvs, -- Getting the environments
......@@ -134,13 +127,12 @@ import Util
import Id
import TcRnTypes
import BasicTypes
import Unique
import UniqFM
import Maybes ( orElse, firstJusts )
import TrieMap
import Control.Monad( ap, when, unless )
import Control.Monad( ap, when, unless, MonadPlus(..) )
import MonadUtils
import Data.IORef
import Data.List ( partition, foldl' )
......@@ -821,16 +813,12 @@ lookupFlatCache fam_tc tys
lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
-- Is this exact predicate type cached in the solved or canonicals of the InertSet?
lookupInInerts loc pty
| ClassPred cls tys <- classifyPredType pty
= do { inerts <- getTcSInerts
; return $ case (classifyPredType pty) of
ClassPred cls tys
| Just ev <- lookupSolvedDict inerts loc cls tys
-> Just ev
| otherwise
-> lookupInertDict (inert_cans inerts) loc cls tys
_other -> Nothing -- NB: No caching for equalities, IPs, holes, or errors
}
; return (lookupSolvedDict inerts loc cls tys `mplus`
lookupInertDict (inert_cans inerts) loc cls tys) }
| otherwise -- NB: No caching for equalities, IPs, holes, or errors
= return Nothing
lookupInertDict :: InertCans -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupInertDict (IC { inert_dicts = dicts }) loc cls tys
......@@ -1647,98 +1635,27 @@ newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
-- Make a new variable of the given PredType,
-- immediately bind it to the given term
-- and return its CtEvidence
-- Precondition: this is not a kind equality
-- See Note [Do not create Given kind equalities]
newGivenEvVar loc (pred, rhs)
= do { new_ev <- newEvVar pred
= ASSERT2( not (isKindEquality pred), ppr pred $$ pprCtOrigin (ctLocOrigin loc) )
do { new_ev <- newEvVar pred
; setEvBind new_ev rhs
; return (CtGiven { ctev_pred = pred, ctev_evtm = EvId new_ev, ctev_loc = loc }) }
newWantedEvVarNC :: CtLoc -> TcPredType -> TcS CtEvidence
-- Don't look up in the solved/inerts; we know it's not there
newWantedEvVarNC loc pty
= do { new_ev <- newEvVar pty
; return (CtWanted { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc })}
newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
-- Like newGivenEvVar, but automatically discard kind equalities
-- See Note [Do not create Given kind equalities]
newGivenEvVars loc pts = mapM (newGivenEvVar loc) (filterOut (isKindEquality . fst) pts)
newWantedEvVar :: CtLoc -> TcPredType -> TcS (CtEvidence, Freshness)
newWantedEvVar loc pty
= do { mb_ct <- lookupInInerts loc pty
; case mb_ct of
Just ctev | not (isDerived ctev)
-> do { traceTcS "newWantedEvVar/cache hit" $ ppr ctev
; return (ctev, Cached) }
_ -> do { ctev <- newWantedEvVarNC loc pty
; traceTcS "newWantedEvVar/cache miss" $ ppr ctev
; return (ctev, Fresh) } }
emitNewDerivedEq :: CtLoc -> Pair TcType -> TcS ()
-- Create new Derived and put it in the work list
emitNewDerivedEq loc (Pair ty1 ty2)
| ty1 `tcEqType` ty2 -- Quite common!
= return ()
| otherwise
= emitNewDerived loc (mkTcEqPred ty1 ty2)