{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Tc.Solver.Interact (
solveSimpleGivens,
solveSimpleWanteds
) where
import GHC.Prelude
import GHC.Types.Basic ( SwapFlag(..), IntWithInf, intGtLimit )
import GHC.Tc.Solver.Canonical
import GHC.Types.Var.Set
import GHC.Types.Var
import GHC.Tc.Errors.Types
import GHC.Tc.Utils.TcType
import GHC.Builtin.Names ( coercibleTyConKey, heqTyConKey, eqTyConKey, ipClassKey )
import GHC.Tc.Instance.FunDeps
import GHC.Tc.Instance.Family
import GHC.Tc.Instance.Class ( InstanceWhat(..), safeOverlap )
import GHC.Tc.Types.Evidence
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Tc.Types
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcMType( promoteMetaTyVarTo )
import GHC.Tc.Solver.Types
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad
import GHC.Core
import GHC.Core.Type as Type
import GHC.Core.InstEnv ( DFunInstType )
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Core.Reduction
import GHC.Core.Predicate
import GHC.Core.Coercion
import GHC.Core.FamInstEnv
import GHC.Core.Unify ( tcUnifyTyWithTFs, ruleMatchTyKiX )
import GHC.Core.Coercion.Axiom ( CoAxBranch (..), CoAxiom (..), TypeEqn, fromBranches
, sfInteractInert, sfInteractTop )
import GHC.Types.SrcLoc
import GHC.Types.Var.Env
import GHC.Types.Unique( hasKey )
import GHC.Data.Bag
import GHC.Data.Pair (Pair(..))
import GHC.Utils.Monad ( concatMapM, foldlM )
import GHC.Utils.Misc
import GHC.Driver.Session
import qualified GHC.LanguageExtensions as LangExt
import Data.List( deleteFirstsBy )
import Data.Maybe ( listToMaybe, mapMaybe )
import Data.Function ( on )
import qualified Data.Semigroup as S
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe
import Control.Monad
solveSimpleGivens :: [Ct] -> TcS ()
solveSimpleGivens :: [Ct] -> TcS ()
solveSimpleGivens [Ct]
givens
| [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
givens
= () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"solveSimpleGivens {" ([Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
givens)
; [Ct] -> TcS ()
go [Ct]
givens
; String -> SDoc -> TcS ()
traceTcS String
"End solveSimpleGivens }" SDoc
forall doc. IsOutput doc => doc
empty }
where
go :: [Ct] -> TcS ()
go [Ct]
givens = do { Cts -> TcS ()
solveSimples ([Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
givens)
; [Ct]
new_givens <- TcS [Ct]
runTcPluginsGiven
; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Ct] -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull [Ct]
new_givens) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
[Ct] -> TcS ()
go [Ct]
new_givens }
solveSimpleWanteds :: Cts -> TcS WantedConstraints
solveSimpleWanteds :: Cts -> TcS WantedConstraints
solveSimpleWanteds Cts
simples
= do { String -> SDoc -> TcS ()
traceTcS String
"solveSimpleWanteds {" (Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
simples)
; DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; (ScDepth
n,WantedConstraints
wc) <- ScDepth
-> IntWithInf
-> WantedConstraints
-> TcS (ScDepth, WantedConstraints)
go ScDepth
1 (DynFlags -> IntWithInf
solverIterations DynFlags
dflags) (WantedConstraints
emptyWC { wc_simple = simples })
; String -> SDoc -> TcS ()
traceTcS String
"solveSimpleWanteds end }" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"iterations =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ScDepth -> SDoc
forall a. Outputable a => a -> SDoc
ppr ScDepth
n
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"residual =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wc ]
; WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return WantedConstraints
wc }
where
go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
go :: ScDepth
-> IntWithInf
-> WantedConstraints
-> TcS (ScDepth, WantedConstraints)
go ScDepth
n IntWithInf
limit WantedConstraints
wc
| ScDepth
n ScDepth -> IntWithInf -> Bool
`intGtLimit` IntWithInf
limit
= TcRnMessage -> TcS (ScDepth, WantedConstraints)
forall a. TcRnMessage -> TcS a
failTcS (TcRnMessage -> TcS (ScDepth, WantedConstraints))
-> TcRnMessage -> TcS (ScDepth, WantedConstraints)
forall a b. (a -> b) -> a -> b
$ Cts -> IntWithInf -> WantedConstraints -> TcRnMessage
TcRnSimplifierTooManyIterations Cts
simples IntWithInf
limit WantedConstraints
wc
| Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag (WantedConstraints -> Cts
wc_simple WantedConstraints
wc)
= (ScDepth, WantedConstraints) -> TcS (ScDepth, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (ScDepth
n,WantedConstraints
wc)
| Bool
otherwise
= do {
WantedConstraints
wc1 <- WantedConstraints -> TcS WantedConstraints
solve_simple_wanteds WantedConstraints
wc
; (Bool
rerun_plugin, WantedConstraints
wc2) <- WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted WantedConstraints
wc1
; if Bool
rerun_plugin
then do { String -> SDoc -> TcS ()
traceTcS String
"solveSimple going round again:" (Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
rerun_plugin)
; ScDepth
-> IntWithInf
-> WantedConstraints
-> TcS (ScDepth, WantedConstraints)
go (ScDepth
nScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ScDepth
1) IntWithInf
limit WantedConstraints
wc2 }
else (ScDepth, WantedConstraints) -> TcS (ScDepth, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (ScDepth
n, WantedConstraints
wc2) }
solve_simple_wanteds :: WantedConstraints -> TcS WantedConstraints
solve_simple_wanteds :: WantedConstraints -> TcS WantedConstraints
solve_simple_wanteds (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples1, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics1, wc_errors :: WantedConstraints -> Bag DelayedError
wc_errors = Bag DelayedError
errs })
= TcS WantedConstraints -> TcS WantedConstraints
forall a. TcS a -> TcS a
nestTcS (TcS WantedConstraints -> TcS WantedConstraints)
-> TcS WantedConstraints -> TcS WantedConstraints
forall a b. (a -> b) -> a -> b
$
do { Cts -> TcS ()
solveSimples Cts
simples1
; (Bag Implication
implics2, Cts
unsolved) <- TcS (Bag Implication, Cts)
getUnsolvedInerts
; WantedConstraints -> TcS WantedConstraints
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (WC { wc_simple :: Cts
wc_simple = Cts
unsolved
, wc_impl :: Bag Implication
wc_impl = Bag Implication
implics1 Bag Implication -> Bag Implication -> Bag Implication
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Implication
implics2
, wc_errors :: Bag DelayedError
wc_errors = Bag DelayedError
errs }) }
solveSimples :: Cts -> TcS ()
solveSimples :: Cts -> TcS ()
solveSimples Cts
cts
= {-# SCC "solveSimples" #-}
do { (WorkList -> WorkList) -> TcS ()
updWorkListTcS (\WorkList
wl -> (Ct -> WorkList -> WorkList) -> WorkList -> Cts -> WorkList
forall a b. (a -> b -> b) -> b -> Bag a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> WorkList -> WorkList
extendWorkListCt WorkList
wl Cts
cts)
; TcS ()
solve_loop }
where
solve_loop :: TcS ()
solve_loop
= {-# SCC "solve_loop" #-}
do { Maybe Ct
sel <- TcS (Maybe Ct)
selectNextWorkItem
; case Maybe Ct
sel of
Maybe Ct
Nothing -> () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Ct
ct -> do { [(String, SimplifierStage)] -> Ct -> TcS ()
runSolverPipeline [(String, SimplifierStage)]
thePipeline Ct
ct
; TcS ()
solve_loop } }
runTcPluginsGiven :: TcS [Ct]
runTcPluginsGiven :: TcS [Ct]
runTcPluginsGiven
= do { [TcPluginSolver]
solvers <- TcS [TcPluginSolver]
getTcPluginSolvers
; if [TcPluginSolver] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcPluginSolver]
solvers then [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else
do { [Ct]
givens <- TcS [Ct]
getInertGivens
; if [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
givens then [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else
do { TcPluginProgress
p <- [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPluginSolvers [TcPluginSolver]
solvers ([Ct]
givens,[])
; let ([Ct]
solved_givens, [(EvTerm, Ct)]
_) = TcPluginProgress -> ([Ct], [(EvTerm, Ct)])
pluginSolvedCts TcPluginProgress
p
insols :: [Ct]
insols = TcPluginProgress -> [Ct]
pluginBadCts TcPluginProgress
p
; (InertCans -> InertCans) -> TcS ()
updInertCans ([Ct] -> InertCans -> InertCans
removeInertCts [Ct]
solved_givens)
; (Cts -> Cts) -> TcS ()
updInertIrreds (\Cts
irreds -> Cts -> [Ct] -> Cts
extendCtsList Cts
irreds [Ct]
insols)
; [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginProgress -> [Ct]
pluginNewCts TcPluginProgress
p) } } }
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
runTcPluginsWanted wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples1 })
| Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag Cts
simples1
= (Bool, WantedConstraints) -> TcS (Bool, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, WantedConstraints
wc)
| Bool
otherwise
= do { [TcPluginSolver]
solvers <- TcS [TcPluginSolver]
getTcPluginSolvers
; if [TcPluginSolver] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcPluginSolver]
solvers then (Bool, WantedConstraints) -> TcS (Bool, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, WantedConstraints
wc) else
do { [Ct]
given <- TcS [Ct]
getInertGivens
; Cts
wanted <- Cts -> TcS Cts
zonkSimples Cts
simples1
; TcPluginProgress
p <- [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPluginSolvers [TcPluginSolver]
solvers ([Ct]
given, Cts -> [Ct]
forall a. Bag a -> [a]
bagToList Cts
wanted)
; let ([Ct]
_, [(EvTerm, Ct)]
solved_wanted) = TcPluginProgress -> ([Ct], [(EvTerm, Ct)])
pluginSolvedCts TcPluginProgress
p
([Ct]
_, [Ct]
unsolved_wanted) = TcPluginProgress -> SplitCts
pluginInputCts TcPluginProgress
p
new_wanted :: [Ct]
new_wanted = TcPluginProgress -> [Ct]
pluginNewCts TcPluginProgress
p
insols :: [Ct]
insols = TcPluginProgress -> [Ct]
pluginBadCts TcPluginProgress
p
; ((EvTerm, Ct) -> TcS ()) -> [(EvTerm, Ct)] -> TcS ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (EvTerm, Ct) -> TcS ()
setEv [(EvTerm, Ct)]
solved_wanted
; (Bool, WantedConstraints) -> TcS (Bool, WantedConstraints)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [Ct] -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull (TcPluginProgress -> [Ct]
pluginNewCts TcPluginProgress
p)
, WantedConstraints
wc { wc_simple = listToBag new_wanted `andCts`
listToBag unsolved_wanted `andCts`
listToBag insols } ) } }
where
setEv :: (EvTerm,Ct) -> TcS ()
setEv :: (EvTerm, Ct) -> TcS ()
setEv (EvTerm
ev,Ct
ct) = case Ct -> CtEvidence
ctEvidence Ct
ct of
CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest } -> TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm TcEvDest
dest EvTerm
ev
CtEvidence
_ -> String -> TcS ()
forall a. HasCallStack => String -> a
panic String
"runTcPluginsWanted.setEv: attempt to solve non-wanted!"
type SplitCts = ([Ct], [Ct])
type SolvedCts = ([Ct], [(EvTerm,Ct)])
data TcPluginProgress = TcPluginProgress
{ TcPluginProgress -> SplitCts
pluginInputCts :: SplitCts
, TcPluginProgress -> ([Ct], [(EvTerm, Ct)])
pluginSolvedCts :: SolvedCts
, TcPluginProgress -> [Ct]
pluginBadCts :: [Ct]
, TcPluginProgress -> [Ct]
pluginNewCts :: [Ct]
}
getTcPluginSolvers :: TcS [TcPluginSolver]
getTcPluginSolvers :: TcS [TcPluginSolver]
getTcPluginSolvers
= do { TcGblEnv
tcg_env <- TcS TcGblEnv
getGblEnv; [TcPluginSolver] -> TcS [TcPluginSolver]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcGblEnv -> [TcPluginSolver]
tcg_tc_plugin_solvers TcGblEnv
tcg_env) }
runTcPluginSolvers :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPluginSolvers :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
runTcPluginSolvers [TcPluginSolver]
solvers SplitCts
all_cts
= do { EvBindsVar
ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
; (TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress)
-> TcPluginProgress -> [TcPluginSolver] -> TcS TcPluginProgress
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (EvBindsVar
-> TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
do_plugin EvBindsVar
ev_binds_var) TcPluginProgress
initialProgress [TcPluginSolver]
solvers }
where
do_plugin :: EvBindsVar -> TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
do_plugin :: EvBindsVar
-> TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
do_plugin EvBindsVar
ev_binds_var TcPluginProgress
p TcPluginSolver
solver = do
TcPluginSolveResult
result <- TcPluginM TcPluginSolveResult -> TcS TcPluginSolveResult
forall a. TcPluginM a -> TcS a
runTcPluginTcS (([Ct] -> [Ct] -> TcPluginM TcPluginSolveResult)
-> SplitCts -> TcPluginM TcPluginSolveResult
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (TcPluginSolver
solver EvBindsVar
ev_binds_var) (TcPluginProgress -> SplitCts
pluginInputCts TcPluginProgress
p))
TcPluginProgress -> TcS TcPluginProgress
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginProgress -> TcS TcPluginProgress)
-> TcPluginProgress -> TcS TcPluginProgress
forall a b. (a -> b) -> a -> b
$ TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress
progress TcPluginProgress
p TcPluginSolveResult
result
progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress
progress :: TcPluginProgress -> TcPluginSolveResult -> TcPluginProgress
progress TcPluginProgress
p
(TcPluginSolveResult
{ tcPluginInsolubleCts :: TcPluginSolveResult -> [Ct]
tcPluginInsolubleCts = [Ct]
bad_cts
, tcPluginSolvedCts :: TcPluginSolveResult -> [(EvTerm, Ct)]
tcPluginSolvedCts = [(EvTerm, Ct)]
solved_cts
, tcPluginNewCts :: TcPluginSolveResult -> [Ct]
tcPluginNewCts = [Ct]
new_cts
}
) =
TcPluginProgress
p { pluginInputCts = discard (bad_cts ++ map snd solved_cts) (pluginInputCts p)
, pluginSolvedCts = add solved_cts (pluginSolvedCts p)
, pluginNewCts = new_cts ++ pluginNewCts p
, pluginBadCts = bad_cts ++ pluginBadCts p
}
initialProgress :: TcPluginProgress
initialProgress = SplitCts
-> ([Ct], [(EvTerm, Ct)]) -> [Ct] -> [Ct] -> TcPluginProgress
TcPluginProgress SplitCts
all_cts ([], []) [] []
discard :: [Ct] -> SplitCts -> SplitCts
discard :: [Ct] -> SplitCts -> SplitCts
discard [Ct]
cts ([Ct]
xs, [Ct]
ys) =
([Ct]
xs [Ct] -> [Ct] -> [Ct]
`without` [Ct]
cts, [Ct]
ys [Ct] -> [Ct] -> [Ct]
`without` [Ct]
cts)
without :: [Ct] -> [Ct] -> [Ct]
without :: [Ct] -> [Ct] -> [Ct]
without = (Ct -> Ct -> Bool) -> [Ct] -> [Ct] -> [Ct]
forall a. (a -> a -> Bool) -> [a] -> [a] -> [a]
deleteFirstsBy Ct -> Ct -> Bool
eqCt
eqCt :: Ct -> Ct -> Bool
eqCt :: Ct -> Ct -> Bool
eqCt Ct
c Ct
c' = Ct -> CtFlavour
ctFlavour Ct
c CtFlavour -> CtFlavour -> Bool
forall a. Eq a => a -> a -> Bool
== Ct -> CtFlavour
ctFlavour Ct
c'
Bool -> Bool -> Bool
&& Ct -> TcPredType
ctPred Ct
c (() :: Constraint) => TcPredType -> TcPredType -> Bool
TcPredType -> TcPredType -> Bool
`tcEqType` Ct -> TcPredType
ctPred Ct
c'
add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
add :: [(EvTerm, Ct)] -> ([Ct], [(EvTerm, Ct)]) -> ([Ct], [(EvTerm, Ct)])
add [(EvTerm, Ct)]
xs ([Ct], [(EvTerm, Ct)])
scs = (([Ct], [(EvTerm, Ct)]) -> (EvTerm, Ct) -> ([Ct], [(EvTerm, Ct)]))
-> ([Ct], [(EvTerm, Ct)])
-> [(EvTerm, Ct)]
-> ([Ct], [(EvTerm, Ct)])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([Ct], [(EvTerm, Ct)]) -> (EvTerm, Ct) -> ([Ct], [(EvTerm, Ct)])
addOne ([Ct], [(EvTerm, Ct)])
scs [(EvTerm, Ct)]
xs
addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
addOne :: ([Ct], [(EvTerm, Ct)]) -> (EvTerm, Ct) -> ([Ct], [(EvTerm, Ct)])
addOne ([Ct]
givens, [(EvTerm, Ct)]
wanteds) (EvTerm
ev,Ct
ct) = case Ct -> CtEvidence
ctEvidence Ct
ct of
CtGiven {} -> (Ct
ctCt -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
:[Ct]
givens, [(EvTerm, Ct)]
wanteds)
CtWanted {} -> ([Ct]
givens, (EvTerm
ev,Ct
ct)(EvTerm, Ct) -> [(EvTerm, Ct)] -> [(EvTerm, Ct)]
forall a. a -> [a] -> [a]
:[(EvTerm, Ct)]
wanteds)
type WorkItem = Ct
type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
runSolverPipeline :: [(String,SimplifierStage)]
-> WorkItem
-> TcS ()
runSolverPipeline :: [(String, SimplifierStage)] -> Ct -> TcS ()
runSolverPipeline [(String, SimplifierStage)]
pipeline Ct
workItem
= do { WorkList
wl <- TcS WorkList
getWorkList
; InertSet
inerts <- TcS InertSet
getTcSInerts
; TcLevel
tclevel <- TcS TcLevel
getTcLevel
; String -> SDoc -> TcS ()
traceTcS String
"----------------------------- " SDoc
forall doc. IsOutput doc => doc
empty
; String -> SDoc -> TcS ()
traceTcS String
"Start solver pipeline {" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tclevel =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclevel
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"work item =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
workItem
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"inerts =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InertSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertSet
inerts
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"rest of worklist =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> WorkList -> SDoc
forall a. Outputable a => a -> SDoc
ppr WorkList
wl ]
; TcS ()
bumpStepCountTcS
; StopOrContinue Ct
final_res <- [(String, SimplifierStage)]
-> StopOrContinue Ct -> TcS (StopOrContinue Ct)
run_pipeline [(String, SimplifierStage)]
pipeline (Ct -> StopOrContinue Ct
forall a. a -> StopOrContinue a
ContinueWith Ct
workItem)
; case StopOrContinue Ct
final_res of
Stop CtEvidence
ev SDoc
s -> do { CtEvidence -> SDoc -> TcS ()
traceFireTcS CtEvidence
ev SDoc
s
; String -> SDoc -> TcS ()
traceTcS String
"End solver pipeline (discharged) }" SDoc
forall doc. IsOutput doc => doc
empty
; () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return () }
ContinueWith Ct
ct -> do { Ct -> TcS ()
addInertCan Ct
ct
; CtEvidence -> SDoc -> TcS ()
traceFireTcS (Ct -> CtEvidence
ctEvidence Ct
ct) (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Kept as inert")
; String -> SDoc -> TcS ()
traceTcS String
"End solver pipeline (kept as inert) }" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
(String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"final_item =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct) }
}
where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
-> TcS (StopOrContinue Ct)
run_pipeline :: [(String, SimplifierStage)]
-> StopOrContinue Ct -> TcS (StopOrContinue Ct)
run_pipeline [] StopOrContinue Ct
res = StopOrContinue Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return StopOrContinue Ct
res
run_pipeline [(String, SimplifierStage)]
_ (Stop CtEvidence
ev SDoc
s) = StopOrContinue Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> SDoc -> StopOrContinue Ct
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev SDoc
s)
run_pipeline ((String
stg_name,SimplifierStage
stg):[(String, SimplifierStage)]
stgs) (ContinueWith Ct
ct)
= do { String -> SDoc -> TcS ()
traceTcS (String
"runStage " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
stg_name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" {")
(String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"workitem = " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
; StopOrContinue Ct
res <- SimplifierStage
stg Ct
ct
; String -> SDoc -> TcS ()
traceTcS (String
"end stage " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
stg_name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" }") SDoc
forall doc. IsOutput doc => doc
empty
; [(String, SimplifierStage)]
-> StopOrContinue Ct -> TcS (StopOrContinue Ct)
run_pipeline [(String, SimplifierStage)]
stgs StopOrContinue Ct
res }
thePipeline :: [(String,SimplifierStage)]
thePipeline :: [(String, SimplifierStage)]
thePipeline = [ (String
"canonicalization", SimplifierStage
GHC.Tc.Solver.Canonical.canonicalize)
, (String
"interact with inerts", SimplifierStage
interactWithInertsStage)
, (String
"top-level reactions", SimplifierStage
topReactionsStage) ]
interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
interactWithInertsStage :: SimplifierStage
interactWithInertsStage Ct
wi
= do { InertSet
inerts <- TcS InertSet
getTcSInerts
; let ics :: InertCans
ics = InertSet -> InertCans
inert_cans InertSet
inerts
; case Ct
wi of
CEqCan {} -> InertCans -> SimplifierStage
interactEq InertCans
ics Ct
wi
CIrredCan {} -> InertCans -> SimplifierStage
interactIrred InertCans
ics Ct
wi
CDictCan {} -> InertCans -> SimplifierStage
interactDict InertCans
ics Ct
wi
Ct
_ -> String -> SDoc -> TcS (StopOrContinue Ct)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"interactWithInerts" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
wi) }
data InteractResult
= KeepInert
| KeepWork
instance Outputable InteractResult where
ppr :: InteractResult -> SDoc
ppr InteractResult
KeepInert = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"keep inert"
ppr InteractResult
KeepWork = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"keep work-item"
solveOneFromTheOther :: Ct
-> Ct
-> InteractResult
solveOneFromTheOther :: Ct -> Ct -> InteractResult
solveOneFromTheOther Ct
ct_i Ct
ct_w
| CtWanted { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc_w } <- CtEvidence
ev_w
, CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
loc_i CtLoc
loc_w
=
InteractResult
KeepWork
| CtWanted {} <- CtEvidence
ev_w
=
case CtEvidence
ev_i of
CtGiven {} -> InteractResult
KeepInert
CtWanted {}
| Bool -> Bool
not Bool
is_psc_i, Bool
is_psc_w -> InteractResult
KeepInert
| Bool
is_psc_i, Bool -> Bool
not Bool
is_psc_w -> InteractResult
KeepWork
| Bool -> Bool
not Bool
is_wsc_orig_i, Bool
is_wsc_orig_w -> InteractResult
KeepInert
| Bool
is_wsc_orig_i, Bool -> Bool
not Bool
is_wsc_orig_w -> InteractResult
KeepWork
| (RealSrcSpan -> RealSrcSpan -> Bool
forall a. Ord a => a -> a -> Bool
(<) (RealSrcSpan -> RealSrcSpan -> Bool)
-> (CtLoc -> RealSrcSpan) -> CtLoc -> CtLoc -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` CtLoc -> RealSrcSpan
ctLocSpan) CtLoc
loc_i CtLoc
loc_w -> InteractResult
KeepInert
| Bool
otherwise -> InteractResult
KeepWork
| CtWanted { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc_i } <- CtEvidence
ev_i
, CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
loc_w CtLoc
loc_i
= InteractResult
KeepInert
| CtWanted {} <- CtEvidence
ev_i
= InteractResult
KeepWork
| TcLevel
lvl_i TcLevel -> TcLevel -> Bool
forall a. Eq a => a -> a -> Bool
== TcLevel
lvl_w
= InteractResult
same_level_strategy
| Bool
otherwise
= InteractResult
different_level_strategy
where
ev_i :: CtEvidence
ev_i = Ct -> CtEvidence
ctEvidence Ct
ct_i
ev_w :: CtEvidence
ev_w = Ct -> CtEvidence
ctEvidence Ct
ct_w
pred :: TcPredType
pred = CtEvidence -> TcPredType
ctEvPred CtEvidence
ev_i
loc_i :: CtLoc
loc_i = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_i
loc_w :: CtLoc
loc_w = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w
orig_i :: CtOrigin
orig_i = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc_i
orig_w :: CtOrigin
orig_w = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc_w
lvl_i :: TcLevel
lvl_i = CtLoc -> TcLevel
ctLocLevel CtLoc
loc_i
lvl_w :: TcLevel
lvl_w = CtLoc -> TcLevel
ctLocLevel CtLoc
loc_w
is_psc_w :: Bool
is_psc_w = Ct -> Bool
isPendingScDict Ct
ct_w
is_psc_i :: Bool
is_psc_i = Ct -> Bool
isPendingScDict Ct
ct_i
is_wsc_orig_i :: Bool
is_wsc_orig_i = CtOrigin -> Bool
isWantedSuperclassOrigin CtOrigin
orig_i
is_wsc_orig_w :: Bool
is_wsc_orig_w = CtOrigin -> Bool
isWantedSuperclassOrigin CtOrigin
orig_w
different_level_strategy :: InteractResult
different_level_strategy
| TcPredType -> Bool
isIPLikePred TcPredType
pred = if TcLevel
lvl_w TcLevel -> TcLevel -> Bool
forall a. Ord a => a -> a -> Bool
> TcLevel
lvl_i then InteractResult
KeepWork else InteractResult
KeepInert
| Bool
otherwise = if TcLevel
lvl_w TcLevel -> TcLevel -> Bool
forall a. Ord a => a -> a -> Bool
> TcLevel
lvl_i then InteractResult
KeepInert else InteractResult
KeepWork
same_level_strategy :: InteractResult
same_level_strategy
= case (CtOrigin
orig_i, CtOrigin
orig_w) of
(GivenSCOrigin SkolemInfoAnon
_ ScDepth
depth_i Bool
blocked_i, GivenSCOrigin SkolemInfoAnon
_ ScDepth
depth_w Bool
blocked_w)
| Bool
blocked_i, Bool -> Bool
not Bool
blocked_w -> InteractResult
KeepWork
| Bool -> Bool
not Bool
blocked_i, Bool
blocked_w -> InteractResult
KeepInert
| ScDepth
depth_w ScDepth -> ScDepth -> Bool
forall a. Ord a => a -> a -> Bool
< ScDepth
depth_i -> InteractResult
KeepWork
| Bool
otherwise -> InteractResult
KeepInert
(GivenSCOrigin {}, CtOrigin
_) -> InteractResult
KeepWork
(CtOrigin, CtOrigin)
_ -> InteractResult
KeepInert
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
interactIrred :: InertCans -> SimplifierStage
interactIrred InertCans
inerts ct_w :: Ct
ct_w@(CIrredCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev_w, cc_reason :: Ct -> CtIrredReason
cc_reason = CtIrredReason
reason })
| CtIrredReason -> Bool
isInsolubleReason CtIrredReason
reason
= SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
ct_w
| let (Bag (Ct, SwapFlag)
matching_irreds, Cts
others) = Cts -> CtEvidence -> (Bag (Ct, SwapFlag), Cts)
findMatchingIrreds (InertCans -> Cts
inert_irreds InertCans
inerts) CtEvidence
ev_w
, ((Ct
ct_i, SwapFlag
swap) : [(Ct, SwapFlag)]
_rest) <- Bag (Ct, SwapFlag) -> [(Ct, SwapFlag)]
forall a. Bag a -> [a]
bagToList Bag (Ct, SwapFlag)
matching_irreds
, let ev_i :: CtEvidence
ev_i = Ct -> CtEvidence
ctEvidence Ct
ct_i
= do { String -> SDoc -> TcS ()
traceTcS String
"iteractIrred" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"wanted:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct_w SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CtOrigin -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Ct -> CtOrigin
ctOrigin Ct
ct_w))
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"inert: " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct_i SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CtOrigin -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Ct -> CtOrigin
ctOrigin Ct
ct_i)) ]
; case Ct -> Ct -> InteractResult
solveOneFromTheOther Ct
ct_i Ct
ct_w of
InteractResult
KeepInert -> do { CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev_w (SwapFlag -> CtEvidence -> EvTerm
swap_me SwapFlag
swap CtEvidence
ev_i)
; StopOrContinue Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> SDoc -> StopOrContinue Ct
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev_w (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Irred equal:KeepInert" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct_w)) }
InteractResult
KeepWork -> do { CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev_i (SwapFlag -> CtEvidence -> EvTerm
swap_me SwapFlag
swap CtEvidence
ev_w)
; (Cts -> Cts) -> TcS ()
updInertIrreds (\Cts
_ -> Cts
others)
; SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
ct_w } }
| Bool
otherwise
= SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
ct_w
where
swap_me :: SwapFlag -> CtEvidence -> EvTerm
swap_me :: SwapFlag -> CtEvidence -> EvTerm
swap_me SwapFlag
swap CtEvidence
ev
= case SwapFlag
swap of
SwapFlag
NotSwapped -> CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev
SwapFlag
IsSwapped -> TcCoercion -> EvTerm
evCoercion (TcCoercion -> TcCoercion
mkSymCo (EvTerm -> TcCoercion
evTermCoercion (CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev)))
interactIrred InertCans
_ Ct
wi = String -> SDoc -> TcS (StopOrContinue Ct)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"interactIrred" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
wi)
findMatchingIrreds :: Cts -> CtEvidence -> (Bag (Ct, SwapFlag), Bag Ct)
findMatchingIrreds :: Cts -> CtEvidence -> (Bag (Ct, SwapFlag), Cts)
findMatchingIrreds Cts
irreds CtEvidence
ev
| EqPred EqRel
eq_rel1 TcPredType
lty1 TcPredType
rty1 <- TcPredType -> Pred
classifyPredType TcPredType
pred
= (Ct -> Either (Ct, SwapFlag) Ct)
-> Cts -> (Bag (Ct, SwapFlag), Cts)
forall a b c. (a -> Either b c) -> Bag a -> (Bag b, Bag c)
partitionBagWith (EqRel -> TcPredType -> TcPredType -> Ct -> Either (Ct, SwapFlag) Ct
match_eq EqRel
eq_rel1 TcPredType
lty1 TcPredType
rty1) Cts
irreds
| Bool
otherwise
= (Ct -> Either (Ct, SwapFlag) Ct)
-> Cts -> (Bag (Ct, SwapFlag), Cts)
forall a b c. (a -> Either b c) -> Bag a -> (Bag b, Bag c)
partitionBagWith Ct -> Either (Ct, SwapFlag) Ct
match_non_eq Cts
irreds
where
pred :: TcPredType
pred = CtEvidence -> TcPredType
ctEvPred CtEvidence
ev
match_non_eq :: Ct -> Either (Ct, SwapFlag) Ct
match_non_eq Ct
ct
| Ct -> TcPredType
ctPred Ct
ct TcPredType -> TcPredType -> Bool
`tcEqTypeNoKindCheck` TcPredType
pred = (Ct, SwapFlag) -> Either (Ct, SwapFlag) Ct
forall a b. a -> Either a b
Left (Ct
ct, SwapFlag
NotSwapped)
| Bool
otherwise = Ct -> Either (Ct, SwapFlag) Ct
forall a b. b -> Either a b
Right Ct
ct
match_eq :: EqRel -> TcPredType -> TcPredType -> Ct -> Either (Ct, SwapFlag) Ct
match_eq EqRel
eq_rel1 TcPredType
lty1 TcPredType
rty1 Ct
ct
| EqPred EqRel
eq_rel2 TcPredType
lty2 TcPredType
rty2 <- TcPredType -> Pred
classifyPredType (Ct -> TcPredType
ctPred Ct
ct)
, EqRel
eq_rel1 EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
eq_rel2
, Just SwapFlag
swap <- TcPredType
-> TcPredType -> TcPredType -> TcPredType -> Maybe SwapFlag
match_eq_help TcPredType
lty1 TcPredType
rty1 TcPredType
lty2 TcPredType
rty2
= (Ct, SwapFlag) -> Either (Ct, SwapFlag) Ct
forall a b. a -> Either a b
Left (Ct
ct, SwapFlag
swap)
| Bool
otherwise
= Ct -> Either (Ct, SwapFlag) Ct
forall a b. b -> Either a b
Right Ct
ct
match_eq_help :: TcPredType
-> TcPredType -> TcPredType -> TcPredType -> Maybe SwapFlag
match_eq_help TcPredType
lty1 TcPredType
rty1 TcPredType
lty2 TcPredType
rty2
| TcPredType
lty1 TcPredType -> TcPredType -> Bool
`tcEqTypeNoKindCheck` TcPredType
lty2, TcPredType
rty1 TcPredType -> TcPredType -> Bool
`tcEqTypeNoKindCheck` TcPredType
rty2
= SwapFlag -> Maybe SwapFlag
forall a. a -> Maybe a
Just SwapFlag
NotSwapped
| TcPredType
lty1 TcPredType -> TcPredType -> Bool
`tcEqTypeNoKindCheck` TcPredType
rty2, TcPredType
rty1 TcPredType -> TcPredType -> Bool
`tcEqTypeNoKindCheck` TcPredType
lty2
= SwapFlag -> Maybe SwapFlag
forall a. a -> Maybe a
Just SwapFlag
IsSwapped
| Bool
otherwise
= Maybe SwapFlag
forall a. Maybe a
Nothing
interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
interactDict :: InertCans -> SimplifierStage
interactDict InertCans
inerts ct_w :: Ct
ct_w@(CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev_w, cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [TcPredType]
cc_tyargs = [TcPredType]
tys })
| Just Ct
ct_i <- InertCans -> CtLoc -> Class -> [TcPredType] -> Maybe Ct
lookupInertDict InertCans
inerts (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w) Class
cls [TcPredType]
tys
, let ev_i :: CtEvidence
ev_i = Ct -> CtEvidence
ctEvidence Ct
ct_i
loc_i :: CtLoc
loc_i = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_i
loc_w :: CtLoc
loc_w = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w
=
do {
DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; Bool
short_cut_worked <- DynFlags -> CtEvidence -> CtEvidence -> TcS Bool
shortCutSolver DynFlags
dflags CtEvidence
ev_w CtEvidence
ev_i
; if Bool
short_cut_worked
then CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev_w String
"interactDict/solved from instance"
else if CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
loc_i CtLoc
loc_w
then SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
ct_w
else
do {
; case Ct -> Ct -> InteractResult
solveOneFromTheOther Ct
ct_i Ct
ct_w of
InteractResult
KeepInert -> do { String -> SDoc -> TcS ()
traceTcS String
"lookupInertDict:KeepInert" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct_w)
; CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev_w (CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev_i)
; StopOrContinue Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (StopOrContinue Ct -> TcS (StopOrContinue Ct))
-> StopOrContinue Ct -> TcS (StopOrContinue Ct)
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc -> StopOrContinue Ct
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev_w (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Dict equal" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct_w) }
InteractResult
KeepWork -> do { String -> SDoc -> TcS ()
traceTcS String
"lookupInertDict:KeepWork" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct_w)
; CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev_i (CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev_w)
; (DictMap Ct -> DictMap Ct) -> TcS ()
updInertDicts ((DictMap Ct -> DictMap Ct) -> TcS ())
-> (DictMap Ct -> DictMap Ct) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ DictMap Ct
ds -> DictMap Ct -> Class -> [TcPredType] -> DictMap Ct
forall a. DictMap a -> Class -> [TcPredType] -> DictMap a
delDict DictMap Ct
ds Class
cls [TcPredType]
tys
; SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
ct_w } } }
| Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
ipClassKey
, CtEvidence -> Bool
isGiven CtEvidence
ev_w
= InertCans -> SimplifierStage
interactGivenIP InertCans
inerts Ct
ct_w
| Bool
otherwise
= do { InertCans -> CtEvidence -> Class -> TcS ()
addFunDepWork InertCans
inerts CtEvidence
ev_w Class
cls
; SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
ct_w }
interactDict InertCans
_ Ct
wi = String -> SDoc -> TcS (StopOrContinue Ct)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"interactDict" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
wi)
shortCutSolver :: DynFlags
-> CtEvidence
-> CtEvidence
-> TcS Bool
shortCutSolver :: DynFlags -> CtEvidence -> CtEvidence -> TcS Bool
shortCutSolver DynFlags
dflags CtEvidence
ev_w CtEvidence
ev_i
| CtEvidence -> Bool
isWanted CtEvidence
ev_w
Bool -> Bool -> Bool
&& CtEvidence -> Bool
isGiven CtEvidence
ev_i
Bool -> Bool -> Bool
&& Bool -> Bool
not (TcPredType -> Bool
isIPLikePred (CtEvidence -> TcPredType
ctEvPred CtEvidence
ev_w))
Bool -> Bool -> Bool
&& Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.IncoherentInstances DynFlags
dflags)
Bool -> Bool -> Bool
&& GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_SolveConstantDicts DynFlags
dflags
= do { EvBindsVar
ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
; EvBindMap
ev_binds <- Bool -> SDoc -> TcS EvBindMap -> TcS EvBindMap
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Bool -> Bool
not (EvBindsVar -> Bool
isCoEvBindsVar EvBindsVar
ev_binds_var )) (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev_w) (TcS EvBindMap -> TcS EvBindMap) -> TcS EvBindMap -> TcS EvBindMap
forall a b. (a -> b) -> a -> b
$
EvBindsVar -> TcS EvBindMap
getTcEvBindsMap EvBindsVar
ev_binds_var
; DictMap CtEvidence
solved_dicts <- TcS (DictMap CtEvidence)
getSolvedDicts
; Maybe (EvBindMap, DictMap CtEvidence)
mb_stuff <- MaybeT TcS (EvBindMap, DictMap CtEvidence)
-> TcS (Maybe (EvBindMap, DictMap CtEvidence))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TcS (EvBindMap, DictMap CtEvidence)
-> TcS (Maybe (EvBindMap, DictMap CtEvidence)))
-> MaybeT TcS (EvBindMap, DictMap CtEvidence)
-> TcS (Maybe (EvBindMap, DictMap CtEvidence))
forall a b. (a -> b) -> a -> b
$ (EvBindMap, DictMap CtEvidence)
-> CtEvidence -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
try_solve_from_instance
(EvBindMap
ev_binds, DictMap CtEvidence
solved_dicts) CtEvidence
ev_w
; case Maybe (EvBindMap, DictMap CtEvidence)
mb_stuff of
Maybe (EvBindMap, DictMap CtEvidence)
Nothing -> Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just (EvBindMap
ev_binds', DictMap CtEvidence
solved_dicts')
-> do { EvBindsVar -> EvBindMap -> TcS ()
setTcEvBindsMap EvBindsVar
ev_binds_var EvBindMap
ev_binds'
; DictMap CtEvidence -> TcS ()
setSolvedDicts DictMap CtEvidence
solved_dicts'
; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True } }
| Bool
otherwise
= Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
where
loc_w :: CtLoc
loc_w = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w
try_solve_from_instance
:: (EvBindMap, DictMap CtEvidence) -> CtEvidence
-> MaybeT TcS (EvBindMap, DictMap CtEvidence)
try_solve_from_instance :: (EvBindMap, DictMap CtEvidence)
-> CtEvidence -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
try_solve_from_instance (EvBindMap
ev_binds, DictMap CtEvidence
solved_dicts) CtEvidence
ev
| let pred :: TcPredType
pred = CtEvidence -> TcPredType
ctEvPred CtEvidence
ev
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
, ClassPred Class
cls [TcPredType]
tys <- TcPredType -> Pred
classifyPredType TcPredType
pred
= do { ClsInstResult
inst_res <- TcS ClsInstResult -> MaybeT TcS ClsInstResult
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcS ClsInstResult -> MaybeT TcS ClsInstResult)
-> TcS ClsInstResult -> MaybeT TcS ClsInstResult
forall a b. (a -> b) -> a -> b
$ DynFlags -> Bool -> Class -> [TcPredType] -> TcS ClsInstResult
matchGlobalInst DynFlags
dflags Bool
True Class
cls [TcPredType]
tys
; case ClsInstResult
inst_res of
OneInst { cir_new_theta :: ClsInstResult -> [TcPredType]
cir_new_theta = [TcPredType]
preds
, cir_mk_ev :: ClsInstResult -> [EvExpr] -> EvTerm
cir_mk_ev = [EvExpr] -> EvTerm
mk_ev
, cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what }
| InstanceWhat -> Bool
safeOverlap InstanceWhat
what
, (TcPredType -> Bool) -> [TcPredType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TcPredType -> Bool
isTyFamFree [TcPredType]
preds
-> do { let solved_dicts' :: DictMap CtEvidence
solved_dicts' = DictMap CtEvidence
-> Class -> [TcPredType] -> CtEvidence -> DictMap CtEvidence
forall a. DictMap a -> Class -> [TcPredType] -> a -> DictMap a
addDict DictMap CtEvidence
solved_dicts Class
cls [TcPredType]
tys CtEvidence
ev
; TcS () -> MaybeT TcS ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcS () -> MaybeT TcS ()) -> TcS () -> MaybeT TcS ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcS ()
traceTcS String
"shortCutSolver: found instance" ([TcPredType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcPredType]
preds)
; CtLoc
loc' <- TcS CtLoc -> MaybeT TcS CtLoc
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcS CtLoc -> MaybeT TcS CtLoc) -> TcS CtLoc -> MaybeT TcS CtLoc
forall a b. (a -> b) -> a -> b
$ CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
checkInstanceOK CtLoc
loc InstanceWhat
what TcPredType
pred
; TcS () -> MaybeT TcS ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcS () -> MaybeT TcS ()) -> TcS () -> MaybeT TcS ()
forall a b. (a -> b) -> a -> b
$ CtLoc -> TcPredType -> TcS ()
checkReductionDepth CtLoc
loc' TcPredType
pred
; [MaybeNew]
evc_vs <- (TcPredType -> MaybeT TcS MaybeNew)
-> [TcPredType] -> MaybeT TcS [MaybeNew]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CtEvidence
-> CtLoc -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
new_wanted_cached CtEvidence
ev CtLoc
loc' DictMap CtEvidence
solved_dicts') [TcPredType]
preds
; let ev_tm :: EvTerm
ev_tm = [EvExpr] -> EvTerm
mk_ev ((MaybeNew -> EvExpr) -> [MaybeNew] -> [EvExpr]
forall a b. (a -> b) -> [a] -> [b]
map MaybeNew -> EvExpr
getEvExpr [MaybeNew]
evc_vs)
ev_binds' :: EvBindMap
ev_binds' = EvBindMap -> EvBind -> EvBindMap
extendEvBinds EvBindMap
ev_binds (EvBind -> EvBindMap) -> EvBind -> EvBindMap
forall a b. (a -> b) -> a -> b
$
TyVar -> EvTerm -> EvBind
mkWantedEvBind (CtEvidence -> TyVar
ctEvEvId CtEvidence
ev) EvTerm
ev_tm
; ((EvBindMap, DictMap CtEvidence)
-> CtEvidence -> MaybeT TcS (EvBindMap, DictMap CtEvidence))
-> (EvBindMap, DictMap CtEvidence)
-> [CtEvidence]
-> MaybeT TcS (EvBindMap, DictMap CtEvidence)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (EvBindMap, DictMap CtEvidence)
-> CtEvidence -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
try_solve_from_instance
(EvBindMap
ev_binds', DictMap CtEvidence
solved_dicts')
([MaybeNew] -> [CtEvidence]
freshGoals [MaybeNew]
evc_vs) }
ClsInstResult
_ -> MaybeT TcS (EvBindMap, DictMap CtEvidence)
forall a. MaybeT TcS a
forall (m :: * -> *) a. MonadPlus m => m a
mzero }
| Bool
otherwise = MaybeT TcS (EvBindMap, DictMap CtEvidence)
forall a. MaybeT TcS a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
new_wanted_cached :: CtEvidence -> CtLoc
-> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
new_wanted_cached :: CtEvidence
-> CtLoc -> DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
new_wanted_cached CtEvidence
ev_w CtLoc
loc DictMap CtEvidence
cache TcPredType
pty
| ClassPred Class
cls [TcPredType]
tys <- TcPredType -> Pred
classifyPredType TcPredType
pty
= TcS MaybeNew -> MaybeT TcS MaybeNew
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcS MaybeNew -> MaybeT TcS MaybeNew)
-> TcS MaybeNew -> MaybeT TcS MaybeNew
forall a b. (a -> b) -> a -> b
$ case DictMap CtEvidence
-> CtLoc -> Class -> [TcPredType] -> Maybe CtEvidence
forall a. DictMap a -> CtLoc -> Class -> [TcPredType] -> Maybe a
findDict DictMap CtEvidence
cache CtLoc
loc_w Class
cls [TcPredType]
tys of
Just CtEvidence
ctev -> MaybeNew -> TcS MaybeNew
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeNew -> TcS MaybeNew) -> MaybeNew -> TcS MaybeNew
forall a b. (a -> b) -> a -> b
$ EvExpr -> MaybeNew
Cached ((() :: Constraint) => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
ctev)
Maybe CtEvidence
Nothing -> CtEvidence -> MaybeNew
Fresh (CtEvidence -> MaybeNew) -> TcS CtEvidence -> TcS MaybeNew
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> RewriterSet -> TcPredType -> TcS CtEvidence
newWantedNC CtLoc
loc (CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev_w) TcPredType
pty
| Bool
otherwise = MaybeT TcS MaybeNew
forall a. MaybeT TcS a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
addFunDepWork InertCans
inerts CtEvidence
work_ev Class
cls
= (Ct -> TcS ()) -> Cts -> TcS ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> Bag a -> m ()
mapBagM_ Ct -> TcS ()
add_fds (DictMap Ct -> Class -> Cts
forall a. DictMap a -> Class -> Bag a
findDictsByClass (InertCans -> DictMap Ct
inert_dicts InertCans
inerts) Class
cls)
where
work_pred :: TcPredType
work_pred = CtEvidence -> TcPredType
ctEvPred CtEvidence
work_ev
work_loc :: CtLoc
work_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
work_ev
add_fds :: Ct -> TcS ()
add_fds Ct
inert_ct
= do { String -> SDoc -> TcS ()
traceTcS String
"addFunDepWork" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat
[ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
work_ev
, CtLoc -> SDoc
pprCtLoc CtLoc
work_loc, Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> Bool
isGivenLoc CtLoc
work_loc)
, CtLoc -> SDoc
pprCtLoc CtLoc
inert_loc, Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> Bool
isGivenLoc CtLoc
inert_loc)
, CtLoc -> SDoc
pprCtLoc CtLoc
derived_loc, Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> Bool
isGivenLoc CtLoc
derived_loc) ])
; Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (CtEvidence -> Bool
isGiven CtEvidence
work_ev Bool -> Bool -> Bool
&& CtEvidence -> Bool
isGiven CtEvidence
inert_ev) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
RewriterSet -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
emitFunDepWanteds (CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
work_ev) ([FunDepEqn (CtLoc, RewriterSet)] -> TcS ())
-> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
forall a b. (a -> b) -> a -> b
$
(CtLoc, RewriterSet)
-> TcPredType -> TcPredType -> [FunDepEqn (CtLoc, RewriterSet)]
forall loc. loc -> TcPredType -> TcPredType -> [FunDepEqn loc]
improveFromAnother (CtLoc
derived_loc, RewriterSet
inert_rewriters) TcPredType
inert_pred TcPredType
work_pred
}
where
inert_ev :: CtEvidence
inert_ev = Ct -> CtEvidence
ctEvidence Ct
inert_ct
inert_pred :: TcPredType
inert_pred = CtEvidence -> TcPredType
ctEvPred CtEvidence
inert_ev
inert_loc :: CtLoc
inert_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
inert_ev
inert_rewriters :: RewriterSet
inert_rewriters = Ct -> RewriterSet
ctRewriters Ct
inert_ct
derived_loc :: CtLoc
derived_loc = CtLoc
work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth`
ctl_depth inert_loc
, ctl_origin = FunDepOrigin1 work_pred
(ctLocOrigin work_loc)
(ctLocSpan work_loc)
inert_pred
(ctLocOrigin inert_loc)
(ctLocSpan inert_loc) }
interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
interactGivenIP :: InertCans -> SimplifierStage
interactGivenIP InertCans
inerts workItem :: Ct
workItem@(CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_class :: Ct -> Class
cc_class = Class
cls
, cc_tyargs :: Ct -> [TcPredType]
cc_tyargs = tys :: [TcPredType]
tys@(TcPredType
ip_str:[TcPredType]
_) })
= do { (InertCans -> InertCans) -> TcS ()
updInertCans ((InertCans -> InertCans) -> TcS ())
-> (InertCans -> InertCans) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \InertCans
cans -> InertCans
cans { inert_dicts = addDict filtered_dicts cls tys workItem }
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Given IP" }
where
dicts :: DictMap Ct
dicts = InertCans -> DictMap Ct
inert_dicts InertCans
inerts
ip_dicts :: Cts
ip_dicts = DictMap Ct -> Class -> Cts
forall a. DictMap a -> Class -> Bag a
findDictsByClass DictMap Ct
dicts Class
cls
other_ip_dicts :: Cts
other_ip_dicts = (Ct -> Bool) -> Cts -> Cts
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag (Bool -> Bool
not (Bool -> Bool) -> (Ct -> Bool) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> Bool
is_this_ip) Cts
ip_dicts
filtered_dicts :: DictMap Ct
filtered_dicts = DictMap Ct -> Class -> Cts -> DictMap Ct
addDictsByClass DictMap Ct
dicts Class
cls Cts
other_ip_dicts
is_this_ip :: Ct -> Bool
is_this_ip (CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_tyargs :: Ct -> [TcPredType]
cc_tyargs = TcPredType
ip_str':[TcPredType]
_ })
= CtEvidence -> Bool
isGiven CtEvidence
ev Bool -> Bool -> Bool
&& TcPredType
ip_str (() :: Constraint) => TcPredType -> TcPredType -> Bool
TcPredType -> TcPredType -> Bool
`tcEqType` TcPredType
ip_str'
is_this_ip Ct
_ = Bool
False
interactGivenIP InertCans
_ Ct
wi = String -> SDoc -> TcS (StopOrContinue Ct)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"interactGivenIP" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
wi)
improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcType
-> TcS ()
improveLocalFunEqs :: CtEvidence
-> InertCans -> TyCon -> [TcPredType] -> TcPredType -> TcS ()
improveLocalFunEqs CtEvidence
work_ev InertCans
inerts TyCon
fam_tc [TcPredType]
args TcPredType
rhs
= Bool -> TcS () -> TcS ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([FunDepEqn (CtLoc, RewriterSet)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns) (TcS () -> TcS ()) -> TcS () -> TcS ()
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcS ()
traceTcS String
"interactFunEq improvements: " (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Eqns:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [FunDepEqn (CtLoc, RewriterSet)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Candidates:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
funeqs_for_tc
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Inert eqs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InertEqs -> SDoc
forall a. Outputable a => a -> SDoc
ppr (InertCans -> InertEqs
inert_eqs InertCans
inerts) ]
; RewriterSet -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
emitFunDepWanteds (CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
work_ev) [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns }
where
funeqs :: FunEqMap [Ct]
funeqs = InertCans -> FunEqMap [Ct]
inert_funeqs InertCans
inerts
funeqs_for_tc :: [Ct]
funeqs_for_tc = [ Ct
funeq_ct | [Ct]
equal_ct_list <- FunEqMap [Ct] -> TyCon -> [[Ct]]
forall a. FunEqMap a -> TyCon -> [a]
findFunEqsByTyCon FunEqMap [Ct]
funeqs TyCon
fam_tc
, Ct
funeq_ct <- [Ct]
equal_ct_list
, EqRel
NomEq EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== Ct -> EqRel
ctEqRel Ct
funeq_ct ]
work_loc :: CtLoc
work_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
work_ev
work_pred :: TcPredType
work_pred = CtEvidence -> TcPredType
ctEvPred CtEvidence
work_ev
fam_inj_info :: Injectivity
fam_inj_info = TyCon -> Injectivity
tyConInjectivityInfo TyCon
fam_tc
improvement_eqns :: [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns :: [FunDepEqn (CtLoc, RewriterSet)]
improvement_eqns
| Just BuiltInSynFamily
ops <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
fam_tc
=
(Ct -> [FunDepEqn (CtLoc, RewriterSet)])
-> [Ct] -> [FunDepEqn (CtLoc, RewriterSet)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (BuiltInSynFamily
-> TcPredType -> Ct -> [FunDepEqn (CtLoc, RewriterSet)]
do_one_built_in BuiltInSynFamily
ops TcPredType
rhs) [Ct]
funeqs_for_tc
| Injective [Bool]
injective_args <- Injectivity
fam_inj_info
=
(Ct -> [FunDepEqn (CtLoc, RewriterSet)])
-> [Ct] -> [FunDepEqn (CtLoc, RewriterSet)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Bool] -> TcPredType -> Ct -> [FunDepEqn (CtLoc, RewriterSet)]
do_one_injective [Bool]
injective_args TcPredType
rhs) [Ct]
funeqs_for_tc
| Bool
otherwise
= []
do_one_built_in :: BuiltInSynFamily
-> TcPredType -> Ct -> [FunDepEqn (CtLoc, RewriterSet)]
do_one_built_in BuiltInSynFamily
ops TcPredType
rhs (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyFamLHS TyCon
_ [TcPredType]
iargs, cc_rhs :: Ct -> TcPredType
cc_rhs = TcPredType
irhs, cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
inert_ev })
| Bool -> Bool
not (CtEvidence -> Bool
isGiven CtEvidence
inert_ev Bool -> Bool -> Bool
&& CtEvidence -> Bool
isGiven CtEvidence
work_ev)
= CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
mk_fd_eqns CtEvidence
inert_ev (BuiltInSynFamily
-> [TcPredType]
-> TcPredType
-> [TcPredType]
-> TcPredType
-> [TypeEqn]
sfInteractInert BuiltInSynFamily
ops [TcPredType]
args TcPredType
rhs [TcPredType]
iargs TcPredType
irhs)
| Bool
otherwise
= []
do_one_built_in BuiltInSynFamily
_ TcPredType
_ Ct
_ = String -> SDoc -> [FunDepEqn (CtLoc, RewriterSet)]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"interactFunEq 1" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc)
do_one_injective :: [Bool] -> TcPredType -> Ct -> [FunDepEqn (CtLoc, RewriterSet)]
do_one_injective [Bool]
inj_args TcPredType
rhs (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyFamLHS TyCon
_ [TcPredType]
inert_args
, cc_rhs :: Ct -> TcPredType
cc_rhs = TcPredType
irhs, cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
inert_ev })
| Bool -> Bool
not (CtEvidence -> Bool
isGiven CtEvidence
inert_ev Bool -> Bool -> Bool
&& CtEvidence -> Bool
isGiven CtEvidence
work_ev)
, TcPredType
rhs (() :: Constraint) => TcPredType -> TcPredType -> Bool
TcPredType -> TcPredType -> Bool
`tcEqType` TcPredType
irhs
= CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
mk_fd_eqns CtEvidence
inert_ev ([TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)])
-> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
forall a b. (a -> b) -> a -> b
$ [ TcPredType -> TcPredType -> TypeEqn
forall a. a -> a -> Pair a
Pair TcPredType
arg TcPredType
iarg
| (TcPredType
arg, TcPredType
iarg, Bool
True) <- [TcPredType]
-> [TcPredType] -> [Bool] -> [(TcPredType, TcPredType, Bool)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [TcPredType]
args [TcPredType]
inert_args [Bool]
inj_args ]
| Bool
otherwise
= []
do_one_injective [Bool]
_ TcPredType
_ Ct
_ = String -> SDoc -> [FunDepEqn (CtLoc, RewriterSet)]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"interactFunEq 2" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc)
mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]
mk_fd_eqns CtEvidence
inert_ev [TypeEqn]
eqns
| [TypeEqn] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeEqn]
eqns = []
| Bool
otherwise = [ FDEqn { fd_qtvs :: [TyVar]
fd_qtvs = [], fd_eqs :: [TypeEqn]
fd_eqs = [TypeEqn]
eqns
, fd_pred1 :: TcPredType
fd_pred1 = TcPredType
work_pred
, fd_pred2 :: TcPredType
fd_pred2 = TcPredType
inert_pred
, fd_loc :: (CtLoc, RewriterSet)
fd_loc = (CtLoc
loc, RewriterSet
inert_rewriters) } ]
where
initial_loc :: CtLoc
initial_loc
| CtEvidence -> Bool
isGiven CtEvidence
work_ev = CtLoc
inert_loc
| Bool
otherwise = CtLoc
work_loc
eqn_orig :: CtOrigin
eqn_orig = TcPredType
-> CtOrigin
-> RealSrcSpan
-> TcPredType
-> CtOrigin
-> RealSrcSpan
-> CtOrigin
InjTFOrigin1 TcPredType
work_pred (CtLoc -> CtOrigin
ctLocOrigin CtLoc
work_loc) (CtLoc -> RealSrcSpan
ctLocSpan CtLoc
work_loc)
TcPredType
inert_pred (CtLoc -> CtOrigin
ctLocOrigin CtLoc
inert_loc) (CtLoc -> RealSrcSpan
ctLocSpan CtLoc
inert_loc)
eqn_loc :: CtLoc
eqn_loc = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
initial_loc CtOrigin
eqn_orig
inert_pred :: TcPredType
inert_pred = CtEvidence -> TcPredType
ctEvPred CtEvidence
inert_ev
inert_loc :: CtLoc
inert_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
inert_ev
inert_rewriters :: RewriterSet
inert_rewriters = CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
inert_ev
loc :: CtLoc
loc = CtLoc
eqn_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth`
ctl_depth work_loc }
inertsCanDischarge :: InertCans -> Ct
-> Maybe ( CtEvidence
, SwapFlag )
inertsCanDischarge :: InertCans -> Ct -> Maybe (CtEvidence, SwapFlag)
inertsCanDischarge InertCans
inerts (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs_w, cc_rhs :: Ct -> TcPredType
cc_rhs = TcPredType
rhs_w
, cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev_w, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
| (CtEvidence
ev_i : [CtEvidence]
_) <- [ CtEvidence
ev_i | CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev_i, cc_rhs :: Ct -> TcPredType
cc_rhs = TcPredType
rhs_i
, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel }
<- InertCans -> CanEqLHS -> [Ct]
findEq InertCans
inerts CanEqLHS
lhs_w
, TcPredType
rhs_i (() :: Constraint) => TcPredType -> TcPredType -> Bool
TcPredType -> TcPredType -> Bool
`tcEqType` TcPredType
rhs_w
, CtEvidence -> EqRel -> Bool
inert_beats_wanted CtEvidence
ev_i EqRel
eq_rel ]
=
(CtEvidence, SwapFlag) -> Maybe (CtEvidence, SwapFlag)
forall a. a -> Maybe a
Just (CtEvidence
ev_i, SwapFlag
NotSwapped)
| Just CanEqLHS
rhs_lhs <- TcPredType -> Maybe CanEqLHS
canEqLHS_maybe TcPredType
rhs_w
, (CtEvidence
ev_i : [CtEvidence]
_) <- [ CtEvidence
ev_i | CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev_i, cc_rhs :: Ct -> TcPredType
cc_rhs = TcPredType
rhs_i
, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel }
<- InertCans -> CanEqLHS -> [Ct]
findEq InertCans
inerts CanEqLHS
rhs_lhs
, TcPredType
rhs_i (() :: Constraint) => TcPredType -> TcPredType -> Bool
TcPredType -> TcPredType -> Bool
`tcEqType` CanEqLHS -> TcPredType
canEqLHSType CanEqLHS
lhs_w
, CtEvidence -> EqRel -> Bool
inert_beats_wanted CtEvidence
ev_i EqRel
eq_rel ]
=
(CtEvidence, SwapFlag) -> Maybe (CtEvidence, SwapFlag)
forall a. a -> Maybe a
Just (CtEvidence
ev_i, SwapFlag
IsSwapped)
where
loc_w :: CtLoc
loc_w = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w
flav_w :: CtFlavour
flav_w = CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev_w
fr_w :: (CtFlavour, EqRel)
fr_w = (CtFlavour
flav_w, EqRel
eq_rel)
inert_beats_wanted :: CtEvidence -> EqRel -> Bool
inert_beats_wanted CtEvidence
ev_i EqRel
eq_rel
=
(CtFlavour, EqRel)
fr_i (CtFlavour, EqRel) -> (CtFlavour, EqRel) -> Bool
`eqCanRewriteFR` (CtFlavour, EqRel)
fr_w
Bool -> Bool -> Bool
&& Bool -> Bool
not ((CtLoc
loc_w CtLoc -> CtLoc -> Bool
`strictly_more_visible` CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_i)
Bool -> Bool -> Bool
&& ((CtFlavour, EqRel)
fr_w (CtFlavour, EqRel) -> (CtFlavour, EqRel) -> Bool
`eqCanRewriteFR` (CtFlavour, EqRel)
fr_i))
where
fr_i :: (CtFlavour, EqRel)
fr_i = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev_i, EqRel
eq_rel)
strictly_more_visible :: CtLoc -> CtLoc -> Bool
strictly_more_visible CtLoc
loc1 CtLoc
loc2
= Bool -> Bool
not (CtOrigin -> Bool
isVisibleOrigin (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc2)) Bool -> Bool -> Bool
&&
CtOrigin -> Bool
isVisibleOrigin (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc1)
inertsCanDischarge InertCans
_ Ct
_ = Maybe (CtEvidence, SwapFlag)
forall a. Maybe a
Nothing
interactEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
interactEq :: InertCans -> SimplifierStage
interactEq InertCans
inerts workItem :: Ct
workItem@(CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs
, cc_rhs :: Ct -> TcPredType
cc_rhs = TcPredType
rhs
, cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev
, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
| Just (CtEvidence
ev_i, SwapFlag
swapped) <- InertCans -> Ct -> Maybe (CtEvidence, SwapFlag)
inertsCanDischarge InertCans
inerts Ct
workItem
= do { CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev (EvTerm -> TcS ()) -> EvTerm -> TcS ()
forall a b. (a -> b) -> a -> b
$
TcCoercion -> EvTerm
evCoercion (SwapFlag -> TcCoercion -> TcCoercion
maybeSymCo SwapFlag
swapped (TcCoercion -> TcCoercion) -> TcCoercion -> TcCoercion
forall a b. (a -> b) -> a -> b
$
Role -> Role -> TcCoercion -> TcCoercion
downgradeRole (EqRel -> Role
eqRelRole EqRel
eq_rel)
(CtEvidence -> Role
ctEvRole CtEvidence
ev_i)
((() :: Constraint) => CtEvidence -> TcCoercion
CtEvidence -> TcCoercion
ctEvCoercion CtEvidence
ev_i))
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Solved from inert" }
| EqRel
ReprEq <- EqRel
eq_rel
= do { String -> SDoc -> TcS ()
traceTcS String
"Not unifying representational equality" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
workItem)
; SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
workItem }
| Bool
otherwise
= case CanEqLHS
lhs of
TyVarLHS TyVar
tv -> Ct -> CtEvidence -> TyVar -> TcPredType -> TcS (StopOrContinue Ct)
tryToSolveByUnification Ct
workItem CtEvidence
ev TyVar
tv TcPredType
rhs
TyFamLHS TyCon
tc [TcPredType]
args -> do { CtEvidence
-> InertCans -> TyCon -> [TcPredType] -> TcPredType -> TcS ()
improveLocalFunEqs CtEvidence
ev InertCans
inerts TyCon
tc [TcPredType]
args TcPredType
rhs
; SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
workItem }
interactEq InertCans
_ Ct
wi = String -> SDoc -> TcS (StopOrContinue Ct)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"interactEq" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
wi)
tryToSolveByUnification :: Ct -> CtEvidence
-> TcTyVar
-> TcType
-> TcS (StopOrContinue Ct)
tryToSolveByUnification :: Ct -> CtEvidence -> TyVar -> TcPredType -> TcS (StopOrContinue Ct)
tryToSolveByUnification Ct
work_item CtEvidence
ev TyVar
tv TcPredType
rhs
= do { (TouchabilityTestResult
is_touchable, TcPredType
rhs) <- CtFlavour
-> TyVar -> TcPredType -> TcS (TouchabilityTestResult, TcPredType)
touchabilityTest (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev) TyVar
tv TcPredType
rhs
; String -> SDoc -> TcS ()
traceTcS String
"tryToSolveByUnification" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'~' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
rhs
, TouchabilityTestResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr TouchabilityTestResult
is_touchable ])
; case TouchabilityTestResult
is_touchable of
TouchabilityTestResult
Untouchable -> SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
work_item
TouchabilityTestResult
TouchableSameLevel -> CtEvidence -> TyVar -> TcPredType -> TcS (StopOrContinue Ct)
solveByUnification CtEvidence
ev TyVar
tv TcPredType
rhs
TouchableOuterLevel [TyVar]
free_metas TcLevel
tv_lvl
-> do { TcM () -> TcS ()
forall a. TcM a -> TcS a
wrapTcS (TcM () -> TcS ()) -> TcM () -> TcS ()
forall a b. (a -> b) -> a -> b
$ (TyVar -> IOEnv (Env TcGblEnv TcLclEnv) Bool) -> [TyVar] -> TcM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((() :: Constraint) =>
TcLevel -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) Bool
TcLevel -> TyVar -> IOEnv (Env TcGblEnv TcLclEnv) Bool
promoteMetaTyVarTo TcLevel
tv_lvl) [TyVar]
free_metas
; TcLevel -> TcS ()
setUnificationFlag TcLevel
tv_lvl
; CtEvidence -> TyVar -> TcPredType -> TcS (StopOrContinue Ct)
solveByUnification CtEvidence
ev TyVar
tv TcPredType
rhs } }
solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS (StopOrContinue Ct)
solveByUnification :: CtEvidence -> TyVar -> TcPredType -> TcS (StopOrContinue Ct)
solveByUnification CtEvidence
wd TyVar
tv TcPredType
xi
= do { let tv_ty :: TcPredType
tv_ty = TyVar -> TcPredType
mkTyVarTy TyVar
tv
; String -> SDoc -> TcS ()
traceTcS String
"Sneaky unification:" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Unifies:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
xi,
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Coercion:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcPredType -> TcPredType -> SDoc
pprEq TcPredType
tv_ty TcPredType
xi,
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Left Kind is:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => TcPredType -> TcPredType
TcPredType -> TcPredType
typeKind TcPredType
tv_ty),
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Right Kind is:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => TcPredType -> TcPredType
TcPredType -> TcPredType
typeKind TcPredType
xi) ]
; TyVar -> TcPredType -> TcS ()
unifyTyVar TyVar
tv TcPredType
xi
; CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
wd (TcCoercion -> EvTerm
evCoercion (TcPredType -> TcCoercion
mkNomReflCo TcPredType
xi))
; ScDepth
n_kicked <- TyVar -> TcS ScDepth
kickOutAfterUnification TyVar
tv
; StopOrContinue Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> SDoc -> StopOrContinue Ct
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
wd (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Solved by unification" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ScDepth -> SDoc
pprKicked ScDepth
n_kicked)) }
doTopFundepImprovement :: Ct -> TcS ()
doTopFundepImprovement :: Ct -> TcS ()
doTopFundepImprovement work_item :: Ct
work_item@(CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_class :: Ct -> Class
cc_class = Class
cls
, cc_tyargs :: Ct -> [TcPredType]
cc_tyargs = [TcPredType]
xis })
= do { String -> SDoc -> TcS ()
traceTcS String
"try_fundeps" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
work_item)
; InstEnvs
instEnvs <- TcS InstEnvs
getInstEnvs
; let fundep_eqns :: [FunDepEqn (CtLoc, RewriterSet)]
fundep_eqns = InstEnvs
-> (TcPredType -> SrcSpan -> (CtLoc, RewriterSet))
-> Class
-> [TcPredType]
-> [FunDepEqn (CtLoc, RewriterSet)]
forall loc.
InstEnvs
-> (TcPredType -> SrcSpan -> loc)
-> Class
-> [TcPredType]
-> [FunDepEqn loc]
improveFromInstEnv InstEnvs
instEnvs TcPredType -> SrcSpan -> (CtLoc, RewriterSet)
mk_ct_loc Class
cls [TcPredType]
xis
; RewriterSet -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
emitFunDepWanteds (CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev) [FunDepEqn (CtLoc, RewriterSet)]
fundep_eqns }
where
dict_pred :: TcPredType
dict_pred = Class -> [TcPredType] -> TcPredType
mkClassPred Class
cls [TcPredType]
xis
dict_loc :: CtLoc
dict_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
dict_origin :: CtOrigin
dict_origin = CtLoc -> CtOrigin
ctLocOrigin CtLoc
dict_loc
mk_ct_loc :: PredType
-> SrcSpan
-> (CtLoc, RewriterSet)
mk_ct_loc :: TcPredType -> SrcSpan -> (CtLoc, RewriterSet)
mk_ct_loc TcPredType
inst_pred SrcSpan
inst_loc
= ( CtLoc
dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
inst_pred inst_loc }
, RewriterSet
emptyRewriterSet )
doTopFundepImprovement Ct
work_item = String -> SDoc -> TcS ()
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"doTopFundepImprovement" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
work_item)
emitFunDepWanteds :: RewriterSet
-> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
emitFunDepWanteds :: RewriterSet -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
emitFunDepWanteds RewriterSet
_ [] = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
emitFunDepWanteds RewriterSet
work_rewriters [FunDepEqn (CtLoc, RewriterSet)]
fd_eqns
= (FunDepEqn (CtLoc, RewriterSet) -> TcS ())
-> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ FunDepEqn (CtLoc, RewriterSet) -> TcS ()
do_one_FDEqn [FunDepEqn (CtLoc, RewriterSet)]
fd_eqns
where
do_one_FDEqn :: FunDepEqn (CtLoc, RewriterSet) -> TcS ()
do_one_FDEqn (FDEqn { fd_qtvs :: forall loc. FunDepEqn loc -> [TyVar]
fd_qtvs = [TyVar]
tvs, fd_eqs :: forall loc. FunDepEqn loc -> [TypeEqn]
fd_eqs = [TypeEqn]
eqs, fd_loc :: forall loc. FunDepEqn loc -> loc
fd_loc = (CtLoc
loc, RewriterSet
rewriters) })
| [TyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs
= do { String -> SDoc -> TcS ()
traceTcS String
"emitFunDepWanteds 1" (SubGoalDepth -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> SubGoalDepth
ctl_depth CtLoc
loc) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TypeEqn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TypeEqn]
eqs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> Bool
isGivenLoc CtLoc
loc))
; (TypeEqn -> TcS TcCoercion) -> [TypeEqn] -> TcS ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Pair TcPredType
ty1 TcPredType
ty2) -> RewriterSet
-> CtLoc -> Role -> TcPredType -> TcPredType -> TcS TcCoercion
unifyWanted RewriterSet
all_rewriters CtLoc
loc Role
Nominal TcPredType
ty1 TcPredType
ty2)
([TypeEqn] -> [TypeEqn]
forall a. [a] -> [a]
reverse [TypeEqn]
eqs) }
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"emitFunDepWanteds 2" (SubGoalDepth -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> SubGoalDepth
ctl_depth CtLoc
loc) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
tvs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TypeEqn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TypeEqn]
eqs)
; Subst
subst <- Subst -> [TyVar] -> TcS Subst
instFlexiX Subst
emptySubst [TyVar]
tvs
; (TypeEqn -> TcS TcCoercion) -> [TypeEqn] -> TcS ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (CtLoc -> RewriterSet -> Subst -> TypeEqn -> TcS TcCoercion
do_one_eq CtLoc
loc RewriterSet
all_rewriters Subst
subst) ([TypeEqn] -> [TypeEqn]
forall a. [a] -> [a]
reverse [TypeEqn]
eqs) }
where
all_rewriters :: RewriterSet
all_rewriters = RewriterSet
work_rewriters RewriterSet -> RewriterSet -> RewriterSet
forall a. Semigroup a => a -> a -> a
S.<> RewriterSet
rewriters
do_one_eq :: CtLoc -> RewriterSet -> Subst -> TypeEqn -> TcS TcCoercion
do_one_eq CtLoc
loc RewriterSet
rewriters Subst
subst (Pair TcPredType
ty1 TcPredType
ty2)
= RewriterSet
-> CtLoc -> Role -> TcPredType -> TcPredType -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
Nominal (Subst -> TcPredType -> TcPredType
substTyUnchecked Subst
subst' TcPredType
ty1) TcPredType
ty2
where
subst' :: Subst
subst' = Subst -> VarSet -> Subst
extendSubstInScopeSet Subst
subst (TcPredType -> VarSet
tyCoVarsOfType TcPredType
ty1)
topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
topReactionsStage :: SimplifierStage
topReactionsStage Ct
work_item
= do { String -> SDoc -> TcS ()
traceTcS String
"doTopReact" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
work_item)
; case Ct
work_item of
CDictCan {} ->
do { InertSet
inerts <- TcS InertSet
getTcSInerts
; InertSet -> SimplifierStage
doTopReactDict InertSet
inerts Ct
work_item }
CEqCan {} ->
SimplifierStage
doTopReactEq Ct
work_item
CIrredCan {} ->
SimplifierStage
doTopReactOther Ct
work_item
Ct
_ -> SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
work_item }
doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
doTopReactOther :: SimplifierStage
doTopReactOther Ct
work_item
| CtEvidence -> Bool
isGiven CtEvidence
ev
= SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
work_item
| EqPred EqRel
eq_rel TcPredType
t1 TcPredType
t2 <- TcPredType -> Pred
classifyPredType TcPredType
pred
= Ct -> EqRel -> TcPredType -> TcPredType -> TcS (StopOrContinue Ct)
doTopReactEqPred Ct
work_item EqRel
eq_rel TcPredType
t1 TcPredType
t2
| Bool
otherwise
= do { ClsInstResult
res <- TcPredType -> CtLoc -> TcS ClsInstResult
matchLocalInst TcPredType
pred CtLoc
loc
; case ClsInstResult
res of
OneInst {} -> CtEvidence -> ClsInstResult -> TcS (StopOrContinue Ct)
chooseInstance CtEvidence
ev ClsInstResult
res
ClsInstResult
_ -> SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
work_item }
where
ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
work_item
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
pred :: TcPredType
pred = CtEvidence -> TcPredType
ctEvPred CtEvidence
ev
doTopReactEqPred :: Ct -> EqRel -> TcType -> TcType -> TcS (StopOrContinue Ct)
doTopReactEqPred :: Ct -> EqRel -> TcPredType -> TcPredType -> TcS (StopOrContinue Ct)
doTopReactEqPred Ct
work_item EqRel
eq_rel TcPredType
lhs TcPredType
rhs
= do { EvBindsVar
ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
; InertCans
ics <- TcS InertCans
getInertCans
; if CtEvidence -> Bool
isWanted CtEvidence
ev
Bool -> Bool -> Bool
&& Bool -> Bool
not ([QCInst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (InertCans -> [QCInst]
inert_insts InertCans
ics))
Bool -> Bool -> Bool
&& Bool -> Bool
not (EvBindsVar -> Bool
isCoEvBindsVar EvBindsVar
ev_binds_var)
then TcS (StopOrContinue Ct)
try_for_qci
else SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
work_item }
where
ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
work_item
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
role :: Role
role = EqRel -> Role
eqRelRole EqRel
eq_rel
try_for_qci :: TcS (StopOrContinue Ct)
try_for_qci
| Just (Class
cls, [TcPredType]
tys) <- EqRel -> TcPredType -> TcPredType -> Maybe (Class, [TcPredType])
boxEqPred EqRel
eq_rel TcPredType
lhs TcPredType
rhs
= do { ClsInstResult
res <- TcPredType -> CtLoc -> TcS ClsInstResult
matchLocalInst (Class -> [TcPredType] -> TcPredType
mkClassPred Class
cls [TcPredType]
tys) CtLoc
loc
; String -> SDoc -> TcS ()
traceTcS String
"final_qci_check:1" (TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> [TcPredType] -> TcPredType
mkClassPred Class
cls [TcPredType]
tys))
; case ClsInstResult
res of
OneInst { cir_mk_ev :: ClsInstResult -> [EvExpr] -> EvTerm
cir_mk_ev = [EvExpr] -> EvTerm
mk_ev }
-> CtEvidence -> ClsInstResult -> TcS (StopOrContinue Ct)
chooseInstance CtEvidence
ev (ClsInstResult
res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
ClsInstResult
_ -> TcS (StopOrContinue Ct)
try_swapping }
| Bool
otherwise
= SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
work_item
try_swapping :: TcS (StopOrContinue Ct)
try_swapping
| Just (Class
cls, [TcPredType]
tys) <- EqRel -> TcPredType -> TcPredType -> Maybe (Class, [TcPredType])
boxEqPred EqRel
eq_rel TcPredType
rhs TcPredType
lhs
= do { ClsInstResult
res <- TcPredType -> CtLoc -> TcS ClsInstResult
matchLocalInst (Class -> [TcPredType] -> TcPredType
mkClassPred Class
cls [TcPredType]
tys) CtLoc
loc
; String -> SDoc -> TcS ()
traceTcS String
"final_qci_check:2" (TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> [TcPredType] -> TcPredType
mkClassPred Class
cls [TcPredType]
tys))
; case ClsInstResult
res of
OneInst { cir_mk_ev :: ClsInstResult -> [EvExpr] -> EvTerm
cir_mk_ev = [EvExpr] -> EvTerm
mk_ev }
-> do { CtEvidence
ev' <- RewriterSet
-> CtEvidence
-> SwapFlag
-> Reduction
-> Reduction
-> TcS CtEvidence
rewriteEqEvidence RewriterSet
emptyRewriterSet CtEvidence
ev SwapFlag
IsSwapped
(Role -> TcPredType -> Reduction
mkReflRedn Role
role TcPredType
rhs) (Role -> TcPredType -> Reduction
mkReflRedn Role
role TcPredType
lhs)
; CtEvidence -> ClsInstResult -> TcS (StopOrContinue Ct)
chooseInstance CtEvidence
ev' (ClsInstResult
res { cir_mk_ev = mk_eq_ev cls tys mk_ev }) }
ClsInstResult
_ -> do { String -> SDoc -> TcS ()
traceTcS String
"final_qci_check:3" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
work_item)
; SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
work_item }}
| Bool
otherwise
= SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
work_item
mk_eq_ev :: Class -> [TcPredType] -> (t -> EvTerm) -> t -> EvTerm
mk_eq_ev Class
cls [TcPredType]
tys t -> EvTerm
mk_ev t
evs
= case (t -> EvTerm
mk_ev t
evs) of
EvExpr EvExpr
e -> EvExpr -> EvTerm
EvExpr (TyVar -> EvExpr
forall b. TyVar -> Expr b
Var TyVar
sc_id EvExpr -> [TcPredType] -> EvExpr
forall b. Expr b -> [TcPredType] -> Expr b
`mkTyApps` [TcPredType]
tys EvExpr -> EvExpr -> EvExpr
forall b. Expr b -> Expr b -> Expr b
`App` EvExpr
e)
EvTerm
ev -> String -> SDoc -> EvTerm
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mk_eq_ev" (EvTerm -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvTerm
ev)
where
[TyVar
sc_id] = Class -> [TyVar]
classSCSelIds Class
cls
doTopReactEq :: Ct -> TcS (StopOrContinue Ct)
doTopReactEq :: SimplifierStage
doTopReactEq work_item :: Ct
work_item@(CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
old_ev, cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyFamLHS TyCon
fam_tc [TcPredType]
args
, cc_rhs :: Ct -> TcPredType
cc_rhs = TcPredType
rhs })
= do { CtEvidence -> TyCon -> [TcPredType] -> TcPredType -> TcS ()
improveTopFunEqs CtEvidence
old_ev TyCon
fam_tc [TcPredType]
args TcPredType
rhs
; SimplifierStage
doTopReactOther Ct
work_item }
doTopReactEq Ct
work_item = SimplifierStage
doTopReactOther Ct
work_item
improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcType -> TcS ()
improveTopFunEqs :: CtEvidence -> TyCon -> [TcPredType] -> TcPredType -> TcS ()
improveTopFunEqs CtEvidence
ev TyCon
fam_tc [TcPredType]
args TcPredType
rhs
| CtEvidence -> Bool
isGiven CtEvidence
ev
= () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do { (FamInstEnv, FamInstEnv)
fam_envs <- TcS (FamInstEnv, FamInstEnv)
getFamInstEnvs
; [TypeEqn]
eqns <- (FamInstEnv, FamInstEnv)
-> TyCon -> [TcPredType] -> TcPredType -> TcS [TypeEqn]
improve_top_fun_eqs (FamInstEnv, FamInstEnv)
fam_envs TyCon
fam_tc [TcPredType]
args TcPredType
rhs
; String -> SDoc -> TcS ()
traceTcS String
"improveTopFunEqs" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
fam_tc SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [TcPredType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcPredType]
args SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
rhs
, [TypeEqn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TypeEqn]
eqns ])
; (TypeEqn -> TcS TcCoercion) -> [TypeEqn] -> TcS ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Pair TcPredType
ty1 TcPredType
ty2) -> RewriterSet
-> CtLoc -> Role -> TcPredType -> TcPredType -> TcS TcCoercion
unifyWanted RewriterSet
rewriters CtLoc
loc Role
Nominal TcPredType
ty1 TcPredType
ty2)
([TypeEqn] -> [TypeEqn]
forall a. [a] -> [a]
reverse [TypeEqn]
eqns) }
where
loc :: CtLoc
loc = CtLoc -> CtLoc
bumpCtLocDepth (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev)
rewriters :: RewriterSet
rewriters = CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev
improve_top_fun_eqs :: FamInstEnvs
-> TyCon -> [TcType] -> TcType
-> TcS [TypeEqn]
improve_top_fun_eqs :: (FamInstEnv, FamInstEnv)
-> TyCon -> [TcPredType] -> TcPredType -> TcS [TypeEqn]
improve_top_fun_eqs (FamInstEnv, FamInstEnv)
fam_envs TyCon
fam_tc [TcPredType]
args TcPredType
rhs_ty
| Just BuiltInSynFamily
ops <- TyCon -> Maybe BuiltInSynFamily
isBuiltInSynFamTyCon_maybe TyCon
fam_tc
= [TypeEqn] -> TcS [TypeEqn]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (BuiltInSynFamily -> [TcPredType] -> TcPredType -> [TypeEqn]
sfInteractTop BuiltInSynFamily
ops [TcPredType]
args TcPredType
rhs_ty)
| TyCon -> Bool
isOpenTypeFamilyTyCon TyCon
fam_tc
, Injective [Bool]
injective_args <- TyCon -> Injectivity
tyConInjectivityInfo TyCon
fam_tc
, let fam_insts :: [FamInst]
fam_insts = (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
lookupFamInstEnvByTyCon (FamInstEnv, FamInstEnv)
fam_envs TyCon
fam_tc
=
do { let improvs :: [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
improvs = [FamInst]
-> (FamInst -> [TyVar])
-> (FamInst -> [TcPredType])
-> (FamInst -> TcPredType)
-> (FamInst -> Maybe CoAxBranch)
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
forall a.
[a]
-> (a -> [TyVar])
-> (a -> [TcPredType])
-> (a -> TcPredType)
-> (a -> Maybe CoAxBranch)
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
buildImprovementData [FamInst]
fam_insts
FamInst -> [TyVar]
fi_tvs FamInst -> [TcPredType]
fi_tys FamInst -> TcPredType
fi_rhs (Maybe CoAxBranch -> FamInst -> Maybe CoAxBranch
forall a b. a -> b -> a
const Maybe CoAxBranch
forall a. Maybe a
Nothing)
; String -> SDoc -> TcS ()
traceTcS String
"improve_top_fun_eqs2" ([([TcPredType], Subst, [TyVar], Maybe CoAxBranch)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
improvs)
; (([TcPredType], Subst, [TyVar], Maybe CoAxBranch) -> TcS [TypeEqn])
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
-> TcS [TypeEqn]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM ([Bool]
-> ([TcPredType], Subst, [TyVar], Maybe CoAxBranch)
-> TcS [TypeEqn]
injImproveEqns [Bool]
injective_args) ([([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
-> TcS [TypeEqn])
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
-> TcS [TypeEqn]
forall a b. (a -> b) -> a -> b
$
ScDepth
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
forall a. ScDepth -> [a] -> [a]
take ScDepth
1 [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
improvs }
| Just CoAxiom Branched
ax <- TyCon -> Maybe (CoAxiom Branched)
isClosedSynFamilyTyConWithAxiom_maybe TyCon
fam_tc
, Injective [Bool]
injective_args <- TyCon -> Injectivity
tyConInjectivityInfo TyCon
fam_tc
= (([TcPredType], Subst, [TyVar], Maybe CoAxBranch) -> TcS [TypeEqn])
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
-> TcS [TypeEqn]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM ([Bool]
-> ([TcPredType], Subst, [TyVar], Maybe CoAxBranch)
-> TcS [TypeEqn]
injImproveEqns [Bool]
injective_args) ([([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
-> TcS [TypeEqn])
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
-> TcS [TypeEqn]
forall a b. (a -> b) -> a -> b
$
[CoAxBranch]
-> (CoAxBranch -> [TyVar])
-> (CoAxBranch -> [TcPredType])
-> (CoAxBranch -> TcPredType)
-> (CoAxBranch -> Maybe CoAxBranch)
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
forall a.
[a]
-> (a -> [TyVar])
-> (a -> [TcPredType])
-> (a -> TcPredType)
-> (a -> Maybe CoAxBranch)
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
buildImprovementData (Branches Branched -> [CoAxBranch]
forall (br :: BranchFlag). Branches br -> [CoAxBranch]
fromBranches (CoAxiom Branched -> Branches Branched
forall (br :: BranchFlag). CoAxiom br -> Branches br
co_ax_branches CoAxiom Branched
ax))
CoAxBranch -> [TyVar]
cab_tvs CoAxBranch -> [TcPredType]
cab_lhs CoAxBranch -> TcPredType
cab_rhs CoAxBranch -> Maybe CoAxBranch
forall a. a -> Maybe a
Just
| Bool
otherwise
= [TypeEqn] -> TcS [TypeEqn]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []
where
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (TcPredType -> VarSet
tyCoVarsOfType TcPredType
rhs_ty)
buildImprovementData
:: [a]
-> (a -> [TyVar])
-> (a -> [Type])
-> (a -> Type)
-> (a -> Maybe CoAxBranch)
-> [( [Type], Subst, [TyVar], Maybe CoAxBranch )]
buildImprovementData :: forall a.
[a]
-> (a -> [TyVar])
-> (a -> [TcPredType])
-> (a -> TcPredType)
-> (a -> Maybe CoAxBranch)
-> [([TcPredType], Subst, [TyVar], Maybe CoAxBranch)]
buildImprovementData [a]
axioms a -> [TyVar]
axiomTVs a -> [TcPredType]
axiomLHS a -> TcPredType
axiomRHS a -> Maybe CoAxBranch
wrap =
[ ([TcPredType]
ax_args, Subst
subst, [TyVar]
unsubstTvs, a -> Maybe CoAxBranch
wrap a
axiom)
| a
axiom <- [a]
axioms
, let ax_args :: [TcPredType]
ax_args = a -> [TcPredType]
axiomLHS a
axiom
ax_rhs :: TcPredType
ax_rhs = a -> TcPredType
axiomRHS a
axiom
ax_tvs :: [TyVar]
ax_tvs = a -> [TyVar]
axiomTVs a
axiom
in_scope1 :: InScopeSet
in_scope1 = InScopeSet
in_scope InScopeSet -> [TyVar] -> InScopeSet
`extendInScopeSetList` [TyVar]
ax_tvs
, Just Subst
subst <- [Bool -> InScopeSet -> TcPredType -> TcPredType -> Maybe Subst
tcUnifyTyWithTFs Bool
False InScopeSet
in_scope1 TcPredType
ax_rhs TcPredType
rhs_ty]
, let notInSubst :: TyVar -> Bool
notInSubst TyVar
tv = Bool -> Bool
not (TyVar
tv TyVar -> VarEnv TcPredType -> Bool
forall a. TyVar -> VarEnv a -> Bool
`elemVarEnv` Subst -> VarEnv TcPredType
getTvSubstEnv Subst
subst)
unsubstTvs :: [TyVar]
unsubstTvs = (TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (TyVar -> Bool
notInSubst (TyVar -> Bool) -> (TyVar -> Bool) -> TyVar -> Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<&&> TyVar -> Bool
isTyVar) [TyVar]
ax_tvs ]
injImproveEqns :: [Bool]
-> ([Type], Subst, [TyCoVar], Maybe CoAxBranch)
-> TcS [TypeEqn]
injImproveEqns :: [Bool]
-> ([TcPredType], Subst, [TyVar], Maybe CoAxBranch)
-> TcS [TypeEqn]
injImproveEqns [Bool]
inj_args ([TcPredType]
ax_args, Subst
subst, [TyVar]
unsubstTvs, Maybe CoAxBranch
cabr)
= do { Subst
subst <- Subst -> [TyVar] -> TcS Subst
instFlexiX Subst
subst [TyVar]
unsubstTvs
; [TypeEqn] -> TcS [TypeEqn]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [ TcPredType -> TcPredType -> TypeEqn
forall a. a -> a -> Pair a
Pair ((() :: Constraint) => Subst -> TcPredType -> TcPredType
Subst -> TcPredType -> TcPredType
substTy Subst
subst TcPredType
ax_arg) TcPredType
arg
| case Maybe CoAxBranch
cabr of
Just CoAxBranch
cabr' -> [TcPredType] -> CoAxBranch -> Bool
apartnessCheck ((() :: Constraint) => Subst -> [TcPredType] -> [TcPredType]
Subst -> [TcPredType] -> [TcPredType]
substTys Subst
subst [TcPredType]
ax_args) CoAxBranch
cabr'
Maybe CoAxBranch
_ -> Bool
True
, (TcPredType
ax_arg, TcPredType
arg, Bool
True) <- [TcPredType]
-> [TcPredType] -> [Bool] -> [(TcPredType, TcPredType, Bool)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [TcPredType]
ax_args [TcPredType]
args [Bool]
inj_args ] }
doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
doTopReactDict :: InertSet -> SimplifierStage
doTopReactDict InertSet
inerts work_item :: Ct
work_item@(CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_class :: Ct -> Class
cc_class = Class
cls
, cc_tyargs :: Ct -> [TcPredType]
cc_tyargs = [TcPredType]
xis })
| CtEvidence -> Bool
isGiven CtEvidence
ev
= SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
work_item
| Just CtEvidence
solved_ev <- InertSet -> CtLoc -> Class -> [TcPredType] -> Maybe CtEvidence
lookupSolvedDict InertSet
inerts CtLoc
dict_loc Class
cls [TcPredType]
xis
= do { CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev (CtEvidence -> EvTerm
ctEvTerm CtEvidence
solved_ev)
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Dict/Top (cached)" }
| Bool
otherwise
= do { DynFlags
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; ClsInstResult
lkup_res <- DynFlags
-> InertSet -> Class -> [TcPredType] -> CtLoc -> TcS ClsInstResult
matchClassInst DynFlags
dflags InertSet
inerts Class
cls [TcPredType]
xis CtLoc
dict_loc
; case ClsInstResult
lkup_res of
OneInst { cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what }
-> do { InstanceWhat -> Ct -> TcS ()
insertSafeOverlapFailureTcS InstanceWhat
what Ct
work_item
; InstanceWhat -> CtEvidence -> Class -> [TcPredType] -> TcS ()
addSolvedDict InstanceWhat
what CtEvidence
ev Class
cls [TcPredType]
xis
; CtEvidence -> ClsInstResult -> TcS (StopOrContinue Ct)
chooseInstance CtEvidence
ev ClsInstResult
lkup_res }
ClsInstResult
_ ->
do { Ct -> TcS ()
doTopFundepImprovement Ct
work_item
; InertSet -> SimplifierStage
tryLastResortProhibitedSuperclass InertSet
inerts Ct
work_item } }
where
dict_loc :: CtLoc
dict_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
doTopReactDict InertSet
_ Ct
w = String -> SDoc -> TcS (StopOrContinue Ct)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"doTopReactDict" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
w)
tryLastResortProhibitedSuperclass :: InertSet -> Ct -> TcS (StopOrContinue Ct)
tryLastResortProhibitedSuperclass :: InertSet -> SimplifierStage
tryLastResortProhibitedSuperclass InertSet
inerts
work_item :: Ct
work_item@(CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev_w, cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [TcPredType]
cc_tyargs = [TcPredType]
xis })
| let loc_w :: CtLoc
loc_w = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w
orig_w :: CtOrigin
orig_w = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc_w
, ScOrigin ClsInstOrQC
_ NakedScFlag
NakedSc <- CtOrigin
orig_w
, Just Ct
ct_i <- InertCans -> CtLoc -> Class -> [TcPredType] -> Maybe Ct
lookupInertDict (InertSet -> InertCans
inert_cans InertSet
inerts) CtLoc
loc_w Class
cls [TcPredType]
xis
, let ev_i :: CtEvidence
ev_i = Ct -> CtEvidence
ctEvidence Ct
ct_i
, CtEvidence -> Bool
isGiven CtEvidence
ev_i
= do { CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev_w (CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev_i)
; CtLoc -> TcRnMessage -> TcS ()
ctLocWarnTcS CtLoc
loc_w (TcRnMessage -> TcS ()) -> TcRnMessage -> TcS ()
forall a b. (a -> b) -> a -> b
$
CtLoc -> TcPredType -> TcRnMessage
TcRnLoopySuperclassSolve CtLoc
loc_w (Ct -> TcPredType
ctPred Ct
work_item)
; StopOrContinue Ct -> TcS (StopOrContinue Ct)
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (StopOrContinue Ct -> TcS (StopOrContinue Ct))
-> StopOrContinue Ct -> TcS (StopOrContinue Ct)
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc -> StopOrContinue Ct
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev_w (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Loopy superclass") }
tryLastResortProhibitedSuperclass InertSet
_ Ct
work_item
= SimplifierStage
forall a. a -> TcS (StopOrContinue a)
continueWith Ct
work_item
chooseInstance :: CtEvidence -> ClsInstResult -> TcS (StopOrContinue Ct)
chooseInstance :: CtEvidence -> ClsInstResult -> TcS (StopOrContinue Ct)
chooseInstance CtEvidence
work_item
(OneInst { cir_new_theta :: ClsInstResult -> [TcPredType]
cir_new_theta = [TcPredType]
theta
, cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what
, cir_mk_ev :: ClsInstResult -> [EvExpr] -> EvTerm
cir_mk_ev = [EvExpr] -> EvTerm
mk_ev })
= do { String -> SDoc -> TcS ()
traceTcS String
"doTopReact/found instance for" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
work_item
; CtLoc
deeper_loc <- CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
checkInstanceOK CtLoc
loc InstanceWhat
what TcPredType
pred
; CtLoc -> TcPredType -> TcS ()
checkReductionDepth CtLoc
deeper_loc TcPredType
pred
; TcS Bool -> SDoc -> TcS ()
forall (m :: * -> *).
(HasCallStack, Monad m) =>
m Bool -> SDoc -> m ()
assertPprM (TcS EvBindsVar
getTcEvBindsVar TcS EvBindsVar -> (EvBindsVar -> TcS Bool) -> TcS Bool
forall a b. TcS a -> (a -> TcS b) -> TcS b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> TcS Bool)
-> (EvBindsVar -> Bool) -> EvBindsVar -> TcS Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> (EvBindsVar -> Bool) -> EvBindsVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvBindsVar -> Bool
isCoEvBindsVar)
(CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
work_item)
; [MaybeNew]
evc_vars <- (TcPredType -> TcS MaybeNew) -> [TcPredType] -> TcS [MaybeNew]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CtLoc -> RewriterSet -> TcPredType -> TcS MaybeNew
newWanted CtLoc
deeper_loc (CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
work_item)) [TcPredType]
theta
; CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
work_item ([EvExpr] -> EvTerm
mk_ev ((MaybeNew -> EvExpr) -> [MaybeNew] -> [EvExpr]
forall a b. (a -> b) -> [a] -> [b]
map MaybeNew -> EvExpr
getEvExpr [MaybeNew]
evc_vars))
; [CtEvidence] -> TcS ()
emitWorkNC ([MaybeNew] -> [CtEvidence]
freshGoals [MaybeNew]
evc_vars)
; CtEvidence -> String -> TcS (StopOrContinue Ct)
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
work_item String
"Dict/Top (solved wanted)" }
where
pred :: TcPredType
pred = CtEvidence -> TcPredType
ctEvPred CtEvidence
work_item
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
work_item
chooseInstance CtEvidence
work_item ClsInstResult
lookup_res
= String -> SDoc -> TcS (StopOrContinue Ct)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"chooseInstance" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
work_item SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ ClsInstResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInstResult
lookup_res)
checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
checkInstanceOK CtLoc
loc InstanceWhat
what TcPredType
pred
= do { CtLoc -> InstanceWhat -> TcPredType -> TcS ()
checkWellStagedDFun CtLoc
loc InstanceWhat
what TcPredType
pred
; CtLoc -> TcS CtLoc
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return CtLoc
deeper_loc }
where
deeper_loc :: CtLoc
deeper_loc = CtLoc -> CtLoc
zap_origin (CtLoc -> CtLoc
bumpCtLocDepth CtLoc
loc)
origin :: CtOrigin
origin = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc
zap_origin :: CtLoc -> CtLoc
zap_origin CtLoc
loc
| ScOrigin ClsInstOrQC
what NakedScFlag
_ <- CtOrigin
origin
= CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
loc (ClsInstOrQC -> NakedScFlag -> CtOrigin
ScOrigin ClsInstOrQC
what NakedScFlag
NotNakedSc)
| Bool
otherwise
= CtLoc
loc
matchClassInst :: DynFlags -> InertSet
-> Class -> [Type]
-> CtLoc -> TcS ClsInstResult
matchClassInst :: DynFlags
-> InertSet -> Class -> [TcPredType] -> CtLoc -> TcS ClsInstResult
matchClassInst DynFlags
dflags InertSet
inerts Class
clas [TcPredType]
tys CtLoc
loc
| Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.IncoherentInstances DynFlags
dflags)
, Bool -> Bool
not (Class -> Bool
naturallyCoherentClass Class
clas)
, Bool -> Bool
not (InertSet -> CtLoc -> Class -> [TcPredType] -> Bool
noMatchableGivenDicts InertSet
inerts CtLoc
loc Class
clas [TcPredType]
tys)
= do { String -> SDoc -> TcS ()
traceTcS String
"Delaying instance application" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Work item=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Class -> [TcPredType] -> SDoc
pprClassPred Class
clas [TcPredType]
tys ]
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NotSure }
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"matchClassInst" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"pred =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
pred SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'{'
; ClsInstResult
local_res <- TcPredType -> CtLoc -> TcS ClsInstResult
matchLocalInst TcPredType
pred CtLoc
loc
; case ClsInstResult
local_res of
OneInst {} ->
do { String -> SDoc -> TcS ()
traceTcS String
"} matchClassInst local match" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ ClsInstResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInstResult
local_res
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
local_res }
ClsInstResult
NotSure ->
do { String -> SDoc -> TcS ()
traceTcS String
"} matchClassInst local not sure" SDoc
forall doc. IsOutput doc => doc
empty
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
local_res }
ClsInstResult
NoInstance
-> do { ClsInstResult
global_res <- DynFlags -> Bool -> Class -> [TcPredType] -> TcS ClsInstResult
matchGlobalInst DynFlags
dflags Bool
False Class
clas [TcPredType]
tys
; String -> SDoc -> TcS ()
traceTcS String
"} matchClassInst global result" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ ClsInstResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInstResult
global_res
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
global_res } }
where
pred :: TcPredType
pred = Class -> [TcPredType] -> TcPredType
mkClassPred Class
clas [TcPredType]
tys
naturallyCoherentClass :: Class -> Bool
naturallyCoherentClass :: Class -> Bool
naturallyCoherentClass Class
cls
= Class -> Bool
isCTupleClass Class
cls
Bool -> Bool -> Bool
|| Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey
Bool -> Bool -> Bool
|| Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
Bool -> Bool -> Bool
|| Class
cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
coercibleTyConKey
matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
matchLocalInst TcPredType
pred CtLoc
loc
= do { inerts :: InertSet
inerts@(IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
ics }) <- TcS InertSet
getTcSInerts
; case InertSet
-> [QCInst]
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
match_local_inst InertSet
inerts (InertCans -> [QCInst]
inert_insts InertCans
ics) of
{ ([], []) -> do { String -> SDoc -> TcS ()
traceTcS String
"No local instance for" (TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
pred)
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NoInstance }
; ([(CtEvidence, [DFunInstType])]
matches, [(CtEvidence, [DFunInstType])]
unifs) ->
do { [InstDFun]
matches <- ((CtEvidence, [DFunInstType]) -> TcS InstDFun)
-> [(CtEvidence, [DFunInstType])] -> TcS [InstDFun]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CtEvidence, [DFunInstType]) -> TcS InstDFun
mk_instDFun [(CtEvidence, [DFunInstType])]
matches
; [InstDFun]
unifs <- ((CtEvidence, [DFunInstType]) -> TcS InstDFun)
-> [(CtEvidence, [DFunInstType])] -> TcS [InstDFun]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CtEvidence, [DFunInstType]) -> TcS InstDFun
mk_instDFun [(CtEvidence, [DFunInstType])]
unifs
; case [InstDFun] -> Maybe InstDFun
dominatingMatch [InstDFun]
matches of
{ Just (TyVar
dfun_id, [TcPredType]
tys, [TcPredType]
theta)
| (InstDFun -> Bool) -> [InstDFun] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (([TcPredType]
theta [TcPredType] -> [TcPredType] -> Bool
`impliedBySCs`) ([TcPredType] -> Bool)
-> (InstDFun -> [TcPredType]) -> InstDFun -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InstDFun -> [TcPredType]
forall a b c. (a, b, c) -> c
thdOf3) [InstDFun]
unifs
->
do { let result :: ClsInstResult
result = OneInst { cir_new_theta :: [TcPredType]
cir_new_theta = [TcPredType]
theta
, cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev = TyVar -> [TcPredType] -> [EvExpr] -> EvTerm
evDFunApp TyVar
dfun_id [TcPredType]
tys
, cir_what :: InstanceWhat
cir_what = InstanceWhat
LocalInstance }
; String -> SDoc -> TcS ()
traceTcS String
"Best local instance found:" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"pred:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
pred
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"result:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ClsInstResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInstResult
result
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"matches:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
matches
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"unifs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
unifs ]
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
result }
; Maybe InstDFun
mb_best ->
do { String -> SDoc -> TcS ()
traceTcS String
"Multiple local instances; not committing to any"
(SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"pred:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
pred
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"matches:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
matches
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"unifs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
unifs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"best_match:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Maybe InstDFun -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe InstDFun
mb_best ]
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NotSure }}}}}
where
pred_tv_set :: VarSet
pred_tv_set = TcPredType -> VarSet
tyCoVarsOfType TcPredType
pred
mk_instDFun :: (CtEvidence, [DFunInstType]) -> TcS InstDFun
mk_instDFun :: (CtEvidence, [DFunInstType]) -> TcS InstDFun
mk_instDFun (CtEvidence
ev, [DFunInstType]
tys) =
let dfun_id :: TyVar
dfun_id = CtEvidence -> TyVar
ctEvEvId CtEvidence
ev
in do { ([TcPredType]
tys, [TcPredType]
theta) <- TyVar -> [DFunInstType] -> TcS ([TcPredType], [TcPredType])
instDFunType (CtEvidence -> TyVar
ctEvEvId CtEvidence
ev) [DFunInstType]
tys
; InstDFun -> TcS InstDFun
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
dfun_id, [TcPredType]
tys, [TcPredType]
theta) }
match_local_inst :: InertSet
-> [QCInst]
-> ( [(CtEvidence, [DFunInstType])]
, [(CtEvidence, [DFunInstType])] )
match_local_inst :: InertSet
-> [QCInst]
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
match_local_inst InertSet
_inerts []
= ([], [])
match_local_inst InertSet
inerts (qci :: QCInst
qci@(QCI { qci_tvs :: QCInst -> [TyVar]
qci_tvs = [TyVar]
qtvs
, qci_pred :: QCInst -> TcPredType
qci_pred = TcPredType
qpred
, qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
qev })
:[QCInst]
qcis)
| let in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet
qtv_set VarSet -> VarSet -> VarSet
`unionVarSet` VarSet
pred_tv_set)
, Just VarEnv TcPredType
tv_subst <- VarSet
-> RnEnv2
-> VarEnv TcPredType
-> TcPredType
-> TcPredType
-> Maybe (VarEnv TcPredType)
ruleMatchTyKiX VarSet
qtv_set (InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope)
VarEnv TcPredType
emptyTvSubstEnv TcPredType
qpred TcPredType
pred
, let match :: (CtEvidence, [DFunInstType])
match = (CtEvidence
qev, (TyVar -> DFunInstType) -> [TyVar] -> [DFunInstType]
forall a b. (a -> b) -> [a] -> [b]
map (VarEnv TcPredType -> TyVar -> DFunInstType
forall a. VarEnv a -> TyVar -> Maybe a
lookupVarEnv VarEnv TcPredType
tv_subst) [TyVar]
qtvs)
= ((CtEvidence, [DFunInstType])
match(CtEvidence, [DFunInstType])
-> [(CtEvidence, [DFunInstType])] -> [(CtEvidence, [DFunInstType])]
forall a. a -> [a] -> [a]
:[(CtEvidence, [DFunInstType])]
matches, [(CtEvidence, [DFunInstType])]
unifs)
| Bool
otherwise
= Bool
-> SDoc
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (VarSet -> VarSet -> Bool
disjointVarSet VarSet
qtv_set (TcPredType -> VarSet
tyCoVarsOfType TcPredType
pred))
(QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr QCInst
qci SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcPredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcPredType
pred)
([(CtEvidence, [DFunInstType])]
matches, Maybe (CtEvidence, [DFunInstType])
this_unif Maybe (CtEvidence, [DFunInstType])
-> [(CtEvidence, [DFunInstType])] -> [(CtEvidence, [DFunInstType])]
forall {a}. Maybe a -> [a] -> [a]
`combine` [(CtEvidence, [DFunInstType])]
unifs)
where
qloc :: CtLoc
qloc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
qev
qtv_set :: VarSet
qtv_set = [TyVar] -> VarSet
mkVarSet [TyVar]
qtvs
([(CtEvidence, [DFunInstType])]
matches, [(CtEvidence, [DFunInstType])]
unifs) = InertSet
-> [QCInst]
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
match_local_inst InertSet
inerts [QCInst]
qcis
this_unif :: Maybe (CtEvidence, [DFunInstType])
this_unif
| Just Subst
subst <- InertSet
-> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Maybe Subst
mightEqualLater InertSet
inerts TcPredType
qpred CtLoc
qloc TcPredType
pred CtLoc
loc
= (CtEvidence, [DFunInstType]) -> Maybe (CtEvidence, [DFunInstType])
forall a. a -> Maybe a
Just (CtEvidence
qev, (TyVar -> DFunInstType) -> [TyVar] -> [DFunInstType]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> TyVar -> DFunInstType
lookupTyVar Subst
subst) [TyVar]
qtvs)
| Bool
otherwise
= Maybe (CtEvidence, [DFunInstType])
forall a. Maybe a
Nothing
combine :: Maybe a -> [a] -> [a]
combine Maybe a
Nothing [a]
us = [a]
us
combine (Just a
u) [a]
us = a
u a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
us
type InstDFun = (DFunId, [TcType], TcThetaType)
dominatingMatch :: [InstDFun] -> Maybe InstDFun
dominatingMatch :: [InstDFun] -> Maybe InstDFun
dominatingMatch [InstDFun]
matches =
[InstDFun] -> Maybe InstDFun
forall a. [a] -> Maybe a
listToMaybe ([InstDFun] -> Maybe InstDFun) -> [InstDFun] -> Maybe InstDFun
forall a b. (a -> b) -> a -> b
$ ((InstDFun, [InstDFun]) -> Maybe InstDFun)
-> [(InstDFun, [InstDFun])] -> [InstDFun]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((InstDFun -> [InstDFun] -> Maybe InstDFun)
-> (InstDFun, [InstDFun]) -> Maybe InstDFun
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry InstDFun -> [InstDFun] -> Maybe InstDFun
go) ([InstDFun] -> [(InstDFun, [InstDFun])]
forall a. [a] -> [(a, [a])]
holes [InstDFun]
matches)
where
go :: InstDFun -> [InstDFun] -> Maybe InstDFun
go :: InstDFun -> [InstDFun] -> Maybe InstDFun
go InstDFun
this [] = InstDFun -> Maybe InstDFun
forall a. a -> Maybe a
Just InstDFun
this
go this :: InstDFun
this@(TyVar
_,[TcPredType]
_,[TcPredType]
this_theta) ((TyVar
_,[TcPredType]
_,[TcPredType]
other_theta):[InstDFun]
others)
| [TcPredType]
this_theta [TcPredType] -> [TcPredType] -> Bool
`impliedBySCs` [TcPredType]
other_theta
= InstDFun -> [InstDFun] -> Maybe InstDFun
go InstDFun
this [InstDFun]
others
| Bool
otherwise
= Maybe InstDFun
forall a. Maybe a
Nothing
impliedBySCs :: TcThetaType -> TcThetaType -> Bool
impliedBySCs :: [TcPredType] -> [TcPredType] -> Bool
impliedBySCs [TcPredType]
c1 [TcPredType]
c2 = (TcPredType -> Bool) -> [TcPredType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TcPredType -> Bool
in_c2 [TcPredType]
c1
where
in_c2 :: TcPredType -> Bool
in_c2 :: TcPredType -> Bool
in_c2 TcPredType
pred = (TcPredType -> Bool) -> [TcPredType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TcPredType
pred (() :: Constraint) => TcPredType -> TcPredType -> Bool
TcPredType -> TcPredType -> Bool
`tcEqType`) [TcPredType]
c2_expanded
c2_expanded :: [TcPredType]
c2_expanded :: [TcPredType]
c2_expanded = [ TcPredType
q | TcPredType
p <- [TcPredType]
c2, TcPredType
q <- TcPredType
p TcPredType -> [TcPredType] -> [TcPredType]
forall a. a -> [a] -> [a]
: TcPredType -> [TcPredType]
transSuperClasses TcPredType
p ]