{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Tc.Solver.InertSet (
WorkList(..), isEmptyWorkList, emptyWorkList,
extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, extendWorkListCtList,
extendWorkListEq, extendWorkListEqs,
appendWorkList, extendWorkListImplic,
workListSize,
selectWorkItem,
InertSet(..),
InertCans(..),
emptyInert,
noMatchableGivenDicts,
noGivenNewtypeReprEqs, updGivenEqs,
mightEqualLater,
prohibitedSuperClassSolve,
InertEqs,
foldTyEqs, delEq, findEq,
partitionInertEqs, partitionFunEqs,
foldFunEqs, addEqToCans,
updDicts, delDict, addDict, filterDicts, partitionDicts,
addSolvedDict,
InertIrreds, delIrred, addIrreds, addIrred, foldIrreds,
findMatchingIrreds, updIrreds, addIrredToCans,
KickOutSpec(..), kickOutRewritableLHS,
CycleBreakerVarStack,
pushCycleBreakerVarStack,
addCycleBreakerBindings,
forAllCycleBreakerBindings_,
InteractResult(..), solveOneFromTheOther
) where
import GHC.Prelude
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Types.CtLoc( CtLoc, ctLocOrigin, ctLocSpan, ctLocLevel )
import GHC.Tc.Solver.Types
import GHC.Tc.Utils.TcType
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Unique( hasKey )
import GHC.Types.Basic( SwapFlag(..) )
import GHC.Core.Reduction
import GHC.Core.Predicate
import GHC.Core.TyCo.FVs
import qualified GHC.Core.TyCo.Rep as Rep
import GHC.Core.Class( Class )
import GHC.Core.TyCon
import GHC.Core.Class( classTyCon )
import GHC.Core.Unify
import GHC.Builtin.Names( eqPrimTyConKey, heqTyConKey, eqTyConKey )
import GHC.Utils.Misc ( partitionWith )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Data.Maybe
import GHC.Data.Bag
import Data.List.NonEmpty ( NonEmpty(..), (<|) )
import qualified Data.List.NonEmpty as NE
import Data.Function ( on )
import Control.Monad ( forM_ )
data WorkList
= WL { WorkList -> [Ct]
wl_eqs_N :: [Ct]
, WorkList -> [Ct]
wl_eqs_X :: [Ct]
, WorkList -> [Ct]
wl_rw_eqs :: [Ct]
, WorkList -> [Ct]
wl_rest :: [Ct]
, WorkList -> Bag Implication
wl_implics :: Bag Implication
}
isNominalEqualityCt :: Ct -> Bool
isNominalEqualityCt :: Ct -> Bool
isNominalEqualityCt Ct
ct
| Just TyCon
tc <- Type -> Maybe TyCon
tcTyConAppTyCon_maybe (Ct -> Type
ctPred Ct
ct)
= TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey Bool -> Bool -> Bool
|| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
heqTyConKey Bool -> Bool -> Bool
|| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqTyConKey
| Bool
otherwise
= Bool
False
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList
(WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs1_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs1_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs1
, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest1, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics1 })
(WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs2_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs2_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs2
, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest2, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics2 })
= WL { wl_eqs_N :: [Ct]
wl_eqs_N = [Ct]
eqs1_N [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
eqs2_N
, wl_eqs_X :: [Ct]
wl_eqs_X = [Ct]
eqs1_X [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
eqs2_X
, wl_rw_eqs :: [Ct]
wl_rw_eqs = [Ct]
rw_eqs1 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
rw_eqs2
, wl_rest :: [Ct]
wl_rest = [Ct]
rest1 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
rest2
, wl_implics :: Bag Implication
wl_implics = Bag Implication
implics1 Bag Implication -> Bag Implication -> Bag Implication
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Implication
implics2 }
workListSize :: WorkList -> Int
workListSize :: WorkList -> ScDepth
workListSize (WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
= [Ct] -> ScDepth
forall a. [a] -> ScDepth
forall (t :: * -> *) a. Foldable t => t a -> ScDepth
length [Ct]
eqs_N ScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ [Ct] -> ScDepth
forall a. [a] -> ScDepth
forall (t :: * -> *) a. Foldable t => t a -> ScDepth
length [Ct]
eqs_X ScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ [Ct] -> ScDepth
forall a. [a] -> ScDepth
forall (t :: * -> *) a. Foldable t => t a -> ScDepth
length [Ct]
rw_eqs ScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ [Ct] -> ScDepth
forall a. [a] -> ScDepth
forall (t :: * -> *) a. Foldable t => t a -> ScDepth
length [Ct]
rest
extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList
extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList
extendWorkListEq RewriterSet
rewriters Ct
ct
wl :: WorkList
wl@(WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs })
| RewriterSet -> Bool
isEmptyRewriterSet RewriterSet
rewriters
= if Ct -> Bool
isNominalEqualityCt Ct
ct
then WorkList
wl { wl_eqs_N = ct : eqs_N }
else WorkList
wl { wl_eqs_X = ct : eqs_X }
| Bool
otherwise
= WorkList
wl { wl_rw_eqs = ct : rw_eqs }
extendWorkListEqs :: RewriterSet -> Bag Ct -> WorkList -> WorkList
extendWorkListEqs :: RewriterSet -> Bag Ct -> WorkList -> WorkList
extendWorkListEqs RewriterSet
rewriters Bag Ct
new_eqs
wl :: WorkList
wl@(WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs })
| RewriterSet -> Bool
isEmptyRewriterSet RewriterSet
rewriters
= case (Ct -> Bool) -> Bag Ct -> (Bag Ct, Bag Ct)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag Ct -> Bool
isNominalEqualityCt Bag Ct
new_eqs of
(Bag Ct
new_eqs_N, Bag Ct
new_eqs_X)
| Bag Ct -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Ct
new_eqs_N -> WorkList
wl { wl_eqs_X = new_eqs_X `push_on_front` eqs_X }
| Bag Ct -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Ct
new_eqs_X -> WorkList
wl { wl_eqs_N = new_eqs_N `push_on_front` eqs_N }
| Bool
otherwise -> WorkList
wl { wl_eqs_N = new_eqs_N `push_on_front` eqs_N
, wl_eqs_X = new_eqs_X `push_on_front` eqs_X }
| Bool
otherwise
= WorkList
wl { wl_rw_eqs = new_eqs `push_on_front` rw_eqs }
where
push_on_front :: Bag Ct -> [Ct] -> [Ct]
push_on_front :: Bag Ct -> [Ct] -> [Ct]
push_on_front Bag Ct
new_eqs [Ct]
eqs = (Ct -> [Ct] -> [Ct]) -> [Ct] -> Bag Ct -> [Ct]
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]
eqs Bag Ct
new_eqs
extendWorkListNonEq :: Ct -> WorkList -> WorkList
extendWorkListNonEq :: Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl = WorkList
wl { wl_rest = ct : wl_rest wl }
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic Implication
implic WorkList
wl = WorkList
wl { wl_implics = implic `consBag` wl_implics wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt Ct
ct WorkList
wl
= case Type -> Pred
classifyPredType (CtEvidence -> Type
ctEvPred CtEvidence
ev) of
EqPred {}
-> RewriterSet -> Ct -> WorkList -> WorkList
extendWorkListEq RewriterSet
rewriters Ct
ct WorkList
wl
ClassPred Class
cls [Type]
_
| Class -> Bool
isEqualityClass Class
cls
-> RewriterSet -> Ct -> WorkList -> WorkList
extendWorkListEq RewriterSet
rewriters Ct
ct WorkList
wl
Pred
_ -> Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl
where
ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
ct
rewriters :: RewriterSet
rewriters = CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev
extendWorkListCtList :: [Ct] -> WorkList -> WorkList
extendWorkListCtList :: [Ct] -> WorkList -> WorkList
extendWorkListCtList [Ct]
cts WorkList
wl = (Ct -> WorkList -> WorkList) -> WorkList -> [Ct] -> WorkList
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> WorkList -> WorkList
extendWorkListCt WorkList
wl [Ct]
cts
extendWorkListCts :: Cts -> WorkList -> WorkList
extendWorkListCts :: Bag Ct -> WorkList -> WorkList
extendWorkListCts Bag Ct
cts WorkList
wl = (Ct -> WorkList -> WorkList) -> WorkList -> Bag Ct -> 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 Bag Ct
cts
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList (WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X
, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
= [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs_N Bool -> Bool -> Bool
&& [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs_X Bool -> Bool -> Bool
&& [Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rest Bool -> Bool -> Bool
&& Bag Implication -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics
emptyWorkList :: WorkList
emptyWorkList :: WorkList
emptyWorkList = WL { wl_eqs_N :: [Ct]
wl_eqs_N = [], wl_eqs_X :: [Ct]
wl_eqs_X = []
, wl_rw_eqs :: [Ct]
wl_rw_eqs = [], wl_rest :: [Ct]
wl_rest = [], wl_implics :: Bag Implication
wl_implics = Bag Implication
forall a. Bag a
emptyBag }
selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
selectWorkItem wl :: WorkList
wl@(WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X
, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
| Ct
ct:[Ct]
cts <- [Ct]
eqs_N = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_eqs_N = cts })
| Ct
ct:[Ct]
cts <- [Ct]
eqs_X = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_eqs_X = cts })
| Ct
ct:[Ct]
cts <- [Ct]
rw_eqs = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_rw_eqs = cts })
| Ct
ct:[Ct]
cts <- [Ct]
rest = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_rest = cts })
| Bool
otherwise = Maybe (Ct, WorkList)
forall a. Maybe a
Nothing
instance Outputable WorkList where
ppr :: WorkList -> SDoc
ppr (WL { wl_eqs_N :: WorkList -> [Ct]
wl_eqs_N = [Ct]
eqs_N, wl_eqs_X :: WorkList -> [Ct]
wl_eqs_X = [Ct]
eqs_X, wl_rw_eqs :: WorkList -> [Ct]
wl_rw_eqs = [Ct]
rw_eqs
, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
= String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"WL" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs_N) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Eqs_N =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
eqs_N)
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs_X) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Eqs_X =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
eqs_X)
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rw_eqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"RwEqs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
rw_eqs)
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([Ct] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
rest) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Non-eqs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
rest)
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (Bag Implication -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Implication
implics) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
SDoc -> SDoc -> SDoc
forall doc. IsOutput doc => doc -> doc -> doc
ifPprDebug (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Implics =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((Implication -> SDoc) -> [Implication] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Implication -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Bag Implication -> [Implication]
forall a. Bag a -> [a]
bagToList Bag Implication
implics)))
(String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"(Implics omitted)")
])
type CycleBreakerVarStack = NonEmpty (Bag (TcTyVar, TcType))
data InertSet
= IS { InertSet -> InertCans
inert_cans :: InertCans
, InertSet -> CycleBreakerVarStack
inert_cycle_breakers :: CycleBreakerVarStack
, InertSet -> FunEqMap Reduction
inert_famapp_cache :: FunEqMap Reduction
, InertSet -> DictMap DictCt
inert_solved_dicts :: DictMap DictCt
}
instance Outputable InertSet where
ppr :: InertSet -> SDoc
ppr (IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
ics
, inert_solved_dicts :: InertSet -> DictMap DictCt
inert_solved_dicts = DictMap DictCt
solved_dicts })
= [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
ics
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([DictCt] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DictCt]
dicts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Solved dicts =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((DictCt -> SDoc) -> [DictCt] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr [DictCt]
dicts) ]
where
dicts :: [DictCt]
dicts = Bag DictCt -> [DictCt]
forall a. Bag a -> [a]
bagToList (DictMap DictCt -> Bag DictCt
forall a. DictMap a -> Bag a
dictsToBag DictMap DictCt
solved_dicts)
emptyInertCans :: InertCans
emptyInertCans :: InertCans
emptyInertCans
= IC { inert_eqs :: InertEqs
inert_eqs = InertEqs
emptyTyEqs
, inert_funeqs :: InertFunEqs
inert_funeqs = InertFunEqs
forall a. TcAppMap a
emptyFunEqs
, inert_given_eq_lvl :: TcLevel
inert_given_eq_lvl = TcLevel
topTcLevel
, inert_given_eqs :: Bool
inert_given_eqs = Bool
False
, inert_dicts :: DictMap DictCt
inert_dicts = DictMap DictCt
forall a. TcAppMap a
emptyDictMap
, inert_safehask :: DictMap DictCt
inert_safehask = DictMap DictCt
forall a. TcAppMap a
emptyDictMap
, inert_insts :: [QCInst]
inert_insts = []
, inert_irreds :: InertIrreds
inert_irreds = InertIrreds
forall a. Bag a
emptyBag }
emptyInert :: InertSet
emptyInert :: InertSet
emptyInert
= IS { inert_cans :: InertCans
inert_cans = InertCans
emptyInertCans
, inert_cycle_breakers :: CycleBreakerVarStack
inert_cycle_breakers = Bag (TcTyVar, Type)
forall a. Bag a
emptyBag Bag (TcTyVar, Type)
-> [Bag (TcTyVar, Type)] -> CycleBreakerVarStack
forall a. a -> [a] -> NonEmpty a
:| []
, inert_famapp_cache :: FunEqMap Reduction
inert_famapp_cache = FunEqMap Reduction
forall a. TcAppMap a
emptyFunEqs
, inert_solved_dicts :: DictMap DictCt
inert_solved_dicts = DictMap DictCt
forall a. TcAppMap a
emptyDictMap }
data InertCans
= IC { InertCans -> InertEqs
inert_eqs :: InertEqs
, InertCans -> InertFunEqs
inert_funeqs :: InertFunEqs
, InertCans -> DictMap DictCt
inert_dicts :: DictMap DictCt
, InertCans -> [QCInst]
inert_insts :: [QCInst]
, InertCans -> DictMap DictCt
inert_safehask :: DictMap DictCt
, InertCans -> InertIrreds
inert_irreds :: InertIrreds
, InertCans -> TcLevel
inert_given_eq_lvl :: TcLevel
, InertCans -> Bool
inert_given_eqs :: Bool
}
type InertEqs = DTyVarEnv EqualCtList
type InertFunEqs = FunEqMap EqualCtList
type InertIrreds = Bag IrredCt
instance Outputable InertCans where
ppr :: InertCans -> SDoc
ppr (IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs
, inert_funeqs :: InertCans -> InertFunEqs
inert_funeqs = InertFunEqs
funeqs
, inert_dicts :: InertCans -> DictMap DictCt
inert_dicts = DictMap DictCt
dicts
, inert_safehask :: InertCans -> DictMap DictCt
inert_safehask = DictMap DictCt
safehask
, inert_irreds :: InertCans -> InertIrreds
inert_irreds = InertIrreds
irreds
, inert_given_eq_lvl :: InertCans -> TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl
, inert_given_eqs :: InertCans -> Bool
inert_given_eqs = Bool
given_eqs
, inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
insts })
= SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat
[ Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (InertEqs -> Bool
forall a. DVarEnv a -> Bool
isEmptyDVarEnv InertEqs
eqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Equalities ="
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bag EqCt -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag ((EqCt -> Bag EqCt -> Bag EqCt) -> InertEqs -> Bag EqCt -> Bag EqCt
forall b. (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs EqCt -> Bag EqCt -> Bag EqCt
forall a. a -> Bag a -> Bag a
consBag InertEqs
eqs Bag EqCt
forall a. Bag a
emptyBag)
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (InertFunEqs -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap InertFunEqs
funeqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Type-function equalities ="
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bag EqCt -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag ((EqCt -> Bag EqCt -> Bag EqCt)
-> InertFunEqs -> Bag EqCt -> Bag EqCt
forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b
foldFunEqs EqCt -> Bag EqCt -> Bag EqCt
forall a. a -> Bag a -> Bag a
consBag InertFunEqs
funeqs Bag EqCt
forall a. Bag a
emptyBag)
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (DictMap DictCt -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap DictCt
dicts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Dictionaries =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bag DictCt -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag (DictMap DictCt -> Bag DictCt
forall a. DictMap a -> Bag a
dictsToBag DictMap DictCt
dicts)
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (DictMap DictCt -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap DictCt
safehask) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Safe Haskell unsafe overlap =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bag DictCt -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag (DictMap DictCt -> Bag DictCt
forall a. DictMap a -> Bag a
dictsToBag DictMap DictCt
safehask)
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless (InertIrreds -> Bool
forall a. Bag a -> Bool
isEmptyBag InertIrreds
irreds) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Irreds =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> InertIrreds -> SDoc
forall a. Outputable a => Bag a -> SDoc
pprBag InertIrreds
irreds
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([QCInst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [QCInst]
insts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Given instances =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((QCInst -> SDoc) -> [QCInst] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr [QCInst]
insts)
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Innermost given equalities =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
ge_lvl
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Given eqs at this level =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
given_eqs
]
emptyTyEqs :: InertEqs
emptyTyEqs :: InertEqs
emptyTyEqs = InertEqs
forall a. DVarEnv a
emptyDVarEnv
addEqToCans :: TcLevel -> EqCt -> InertCans -> InertCans
addEqToCans :: TcLevel -> EqCt -> InertCans -> InertCans
addEqToCans TcLevel
tc_lvl eq_ct :: EqCt
eq_ct@(EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs })
ics :: InertCans
ics@(IC { inert_funeqs :: InertCans -> InertFunEqs
inert_funeqs = InertFunEqs
funeqs, inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs })
= TcLevel -> Ct -> InertCans -> InertCans
updGivenEqs TcLevel
tc_lvl (EqCt -> Ct
CEqCan EqCt
eq_ct) (InertCans -> InertCans) -> InertCans -> InertCans
forall a b. (a -> b) -> a -> b
$
case CanEqLHS
lhs of
TyFamLHS TyCon
tc [Type]
tys -> InertCans
ics { inert_funeqs = addCanFunEq funeqs tc tys eq_ct }
TyVarLHS TcTyVar
tv -> InertCans
ics { inert_eqs = addTyEq eqs tv eq_ct }
addTyEq :: InertEqs -> TcTyVar -> EqCt -> InertEqs
addTyEq :: InertEqs -> TcTyVar -> EqCt -> InertEqs
addTyEq InertEqs
old_eqs TcTyVar
tv EqCt
ct
= (EqualCtList -> EqualCtList -> EqualCtList)
-> InertEqs -> TcTyVar -> EqualCtList -> InertEqs
forall a. (a -> a -> a) -> DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv_C EqualCtList -> EqualCtList -> EqualCtList
add_eq InertEqs
old_eqs TcTyVar
tv [EqCt
ct]
where
add_eq :: EqualCtList -> EqualCtList -> EqualCtList
add_eq EqualCtList
old_eqs EqualCtList
_ = EqCt -> EqualCtList -> EqualCtList
addToEqualCtList EqCt
ct EqualCtList
old_eqs
foldTyEqs :: (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs :: forall b. (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs EqCt -> b -> b
k InertEqs
eqs b
z
= (EqualCtList -> b -> b) -> b -> InertEqs -> b
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv (\EqualCtList
cts b
z -> (EqCt -> b -> b) -> b -> EqualCtList -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr EqCt -> b -> b
k b
z EqualCtList
cts) b
z InertEqs
eqs
findTyEqs :: InertCans -> TyVar -> [EqCt]
findTyEqs :: InertCans -> TcTyVar -> EqualCtList
findTyEqs InertCans
icans TcTyVar
tv = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat @Maybe (InertEqs -> TcTyVar -> Maybe EqualCtList
forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv (InertCans -> InertEqs
inert_eqs InertCans
icans) TcTyVar
tv)
delEq :: EqCt -> InertCans -> InertCans
delEq :: EqCt -> InertCans -> InertCans
delEq (EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs, eq_rhs :: EqCt -> Type
eq_rhs = Type
rhs }) InertCans
ic = case CanEqLHS
lhs of
TyVarLHS TcTyVar
tv
-> InertCans
ic { inert_eqs = alterDVarEnv upd (inert_eqs ic) tv }
TyFamLHS TyCon
tf [Type]
args
-> InertCans
ic { inert_funeqs = alterTcApp (inert_funeqs ic) tf args upd }
where
isThisOne :: EqCt -> Bool
isThisOne :: EqCt -> Bool
isThisOne (EqCt { eq_rhs :: EqCt -> Type
eq_rhs = Type
t1 }) = Type -> Type -> Bool
tcEqTypeNoKindCheck Type
rhs Type
t1
upd :: Maybe EqualCtList -> Maybe EqualCtList
upd :: Maybe EqualCtList -> Maybe EqualCtList
upd (Just EqualCtList
eq_ct_list) = (EqCt -> Bool) -> EqualCtList -> Maybe EqualCtList
filterEqualCtList (Bool -> Bool
not (Bool -> Bool) -> (EqCt -> Bool) -> EqCt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqCt -> Bool
isThisOne) EqualCtList
eq_ct_list
upd Maybe EqualCtList
Nothing = Maybe EqualCtList
forall a. Maybe a
Nothing
findEq :: InertCans -> CanEqLHS -> [EqCt]
findEq :: InertCans -> CanEqLHS -> EqualCtList
findEq InertCans
icans (TyVarLHS TcTyVar
tv) = InertCans -> TcTyVar -> EqualCtList
findTyEqs InertCans
icans TcTyVar
tv
findEq InertCans
icans (TyFamLHS TyCon
fun_tc [Type]
fun_args)
= forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat @Maybe (InertFunEqs -> TyCon -> [Type] -> Maybe EqualCtList
forall a. FunEqMap a -> TyCon -> [Type] -> Maybe a
findFunEq (InertCans -> InertFunEqs
inert_funeqs InertCans
icans) TyCon
fun_tc [Type]
fun_args)
{-# INLINE partition_eqs_container #-}
partition_eqs_container
:: forall container
. container
-> (forall b. (EqCt -> b -> b) -> container -> b -> b)
-> (EqCt -> container -> container)
-> (EqCt -> Bool)
-> container
-> ([EqCt], container)
partition_eqs_container :: forall container.
container
-> (forall b. (EqCt -> b -> b) -> container -> b -> b)
-> (EqCt -> container -> container)
-> (EqCt -> Bool)
-> container
-> (EqualCtList, container)
partition_eqs_container container
empty_container forall b. (EqCt -> b -> b) -> container -> b -> b
fold_container EqCt -> container -> container
extend_container EqCt -> Bool
pred container
orig_inerts
= (EqCt -> (EqualCtList, container) -> (EqualCtList, container))
-> container
-> (EqualCtList, container)
-> (EqualCtList, container)
forall b. (EqCt -> b -> b) -> container -> b -> b
fold_container EqCt -> (EqualCtList, container) -> (EqualCtList, container)
folder container
orig_inerts ([], container
empty_container)
where
folder :: EqCt -> ([EqCt], container) -> ([EqCt], container)
folder :: EqCt -> (EqualCtList, container) -> (EqualCtList, container)
folder EqCt
eq_ct (EqualCtList
acc_true, container
acc_false)
| EqCt -> Bool
pred EqCt
eq_ct = (EqCt
eq_ct EqCt -> EqualCtList -> EqualCtList
forall a. a -> [a] -> [a]
: EqualCtList
acc_true, container
acc_false)
| Bool
otherwise = (EqualCtList
acc_true, EqCt -> container -> container
extend_container EqCt
eq_ct container
acc_false)
partitionInertEqs :: (EqCt -> Bool)
-> InertEqs
-> ([EqCt], InertEqs)
partitionInertEqs :: (EqCt -> Bool) -> InertEqs -> (EqualCtList, InertEqs)
partitionInertEqs = InertEqs
-> (forall b. (EqCt -> b -> b) -> InertEqs -> b -> b)
-> (EqCt -> InertEqs -> InertEqs)
-> (EqCt -> Bool)
-> InertEqs
-> (EqualCtList, InertEqs)
forall container.
container
-> (forall b. (EqCt -> b -> b) -> container -> b -> b)
-> (EqCt -> container -> container)
-> (EqCt -> Bool)
-> container
-> (EqualCtList, container)
partition_eqs_container InertEqs
emptyTyEqs (EqCt -> b -> b) -> InertEqs -> b -> b
forall b. (EqCt -> b -> b) -> InertEqs -> b -> b
foldTyEqs EqCt -> InertEqs -> InertEqs
addInertEqs
addInertEqs :: EqCt -> InertEqs -> InertEqs
addInertEqs :: EqCt -> InertEqs -> InertEqs
addInertEqs eq_ct :: EqCt
eq_ct@(EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = TyVarLHS TcTyVar
tv }) InertEqs
eqs = InertEqs -> TcTyVar -> EqCt -> InertEqs
addTyEq InertEqs
eqs TcTyVar
tv EqCt
eq_ct
addInertEqs EqCt
other InertEqs
_ = String -> SDoc -> InertEqs
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendInertEqs" (EqCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr EqCt
other)
addCanFunEq :: InertFunEqs -> TyCon -> [TcType] -> EqCt -> InertFunEqs
addCanFunEq :: InertFunEqs -> TyCon -> [Type] -> EqCt -> InertFunEqs
addCanFunEq InertFunEqs
old_eqs TyCon
fun_tc [Type]
fun_args EqCt
ct
= InertFunEqs
-> TyCon
-> [Type]
-> (Maybe EqualCtList -> Maybe EqualCtList)
-> InertFunEqs
forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
alterTcApp InertFunEqs
old_eqs TyCon
fun_tc [Type]
fun_args Maybe EqualCtList -> Maybe EqualCtList
upd
where
upd :: Maybe EqualCtList -> Maybe EqualCtList
upd (Just EqualCtList
old_equal_ct_list) = EqualCtList -> Maybe EqualCtList
forall a. a -> Maybe a
Just (EqualCtList -> Maybe EqualCtList)
-> EqualCtList -> Maybe EqualCtList
forall a b. (a -> b) -> a -> b
$ EqCt -> EqualCtList -> EqualCtList
addToEqualCtList EqCt
ct EqualCtList
old_equal_ct_list
upd Maybe EqualCtList
Nothing = EqualCtList -> Maybe EqualCtList
forall a. a -> Maybe a
Just [EqCt
ct]
foldFunEqs :: (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b
foldFunEqs :: forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b
foldFunEqs EqCt -> b -> b
k InertFunEqs
fun_eqs b
z = (EqualCtList -> b -> b) -> InertFunEqs -> b -> b
forall a b. (a -> b -> b) -> TcAppMap a -> b -> b
foldTcAppMap (\EqualCtList
eqs b
z -> (EqCt -> b -> b) -> b -> EqualCtList -> b
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr EqCt -> b -> b
k b
z EqualCtList
eqs) InertFunEqs
fun_eqs b
z
partitionFunEqs :: (EqCt -> Bool)
-> InertFunEqs
-> ([EqCt], InertFunEqs)
partitionFunEqs :: (EqCt -> Bool) -> InertFunEqs -> (EqualCtList, InertFunEqs)
partitionFunEqs = InertFunEqs
-> (forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b)
-> (EqCt -> InertFunEqs -> InertFunEqs)
-> (EqCt -> Bool)
-> InertFunEqs
-> (EqualCtList, InertFunEqs)
forall container.
container
-> (forall b. (EqCt -> b -> b) -> container -> b -> b)
-> (EqCt -> container -> container)
-> (EqCt -> Bool)
-> container
-> (EqualCtList, container)
partition_eqs_container InertFunEqs
forall a. TcAppMap a
emptyFunEqs (EqCt -> b -> b) -> InertFunEqs -> b -> b
forall b. (EqCt -> b -> b) -> InertFunEqs -> b -> b
foldFunEqs EqCt -> InertFunEqs -> InertFunEqs
addFunEqs
addFunEqs :: EqCt -> InertFunEqs -> InertFunEqs
addFunEqs :: EqCt -> InertFunEqs -> InertFunEqs
addFunEqs eq_ct :: EqCt
eq_ct@(EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = TyFamLHS TyCon
tc [Type]
args }) InertFunEqs
fun_eqs
= InertFunEqs -> TyCon -> [Type] -> EqCt -> InertFunEqs
addCanFunEq InertFunEqs
fun_eqs TyCon
tc [Type]
args EqCt
eq_ct
addFunEqs EqCt
other InertFunEqs
_ = String -> SDoc -> InertFunEqs
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendFunEqs" (EqCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr EqCt
other)
updDicts :: (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
updDicts :: (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
updDicts DictMap DictCt -> DictMap DictCt
upd InertCans
ics = InertCans
ics { inert_dicts = upd (inert_dicts ics) }
delDict :: DictCt -> DictMap a -> DictMap a
delDict :: forall a. DictCt -> DictMap a -> DictMap a
delDict (DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys }) DictMap a
m
= DictMap a -> TyCon -> [Type] -> DictMap a
forall a. TcAppMap a -> TyCon -> [Type] -> TcAppMap a
delTcApp DictMap a
m (Class -> TyCon
classTyCon Class
cls) [Type]
tys
addDict :: DictCt -> DictMap DictCt -> DictMap DictCt
addDict :: DictCt -> DictMap DictCt -> DictMap DictCt
addDict item :: DictCt
item@(DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys }) DictMap DictCt
dm
= DictMap DictCt -> TyCon -> [Type] -> DictCt -> DictMap DictCt
forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp DictMap DictCt
dm (Class -> TyCon
classTyCon Class
cls) [Type]
tys DictCt
item
addSolvedDict :: DictCt -> DictMap DictCt -> DictMap DictCt
addSolvedDict :: DictCt -> DictMap DictCt -> DictMap DictCt
addSolvedDict item :: DictCt
item@(DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys }) DictMap DictCt
dm
= DictMap DictCt -> TyCon -> [Type] -> DictCt -> DictMap DictCt
forall a. TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
insertTcApp DictMap DictCt
dm (Class -> TyCon
classTyCon Class
cls) [Type]
tys DictCt
item
filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt
filterDicts :: (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt
filterDicts DictCt -> Bool
f DictMap DictCt
m = (DictCt -> Bool) -> DictMap DictCt -> DictMap DictCt
forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
filterTcAppMap DictCt -> Bool
f DictMap DictCt
m
partitionDicts :: (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt)
partitionDicts :: (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt)
partitionDicts DictCt -> Bool
f DictMap DictCt
m = (DictCt
-> (Bag DictCt, DictMap DictCt) -> (Bag DictCt, DictMap DictCt))
-> DictMap DictCt
-> (Bag DictCt, DictMap DictCt)
-> (Bag DictCt, DictMap DictCt)
forall a b. (a -> b -> b) -> TcAppMap a -> b -> b
foldTcAppMap DictCt
-> (Bag DictCt, DictMap DictCt) -> (Bag DictCt, DictMap DictCt)
k DictMap DictCt
m (Bag DictCt
forall a. Bag a
emptyBag, DictMap DictCt
forall a. TcAppMap a
emptyDictMap)
where
k :: DictCt
-> (Bag DictCt, DictMap DictCt) -> (Bag DictCt, DictMap DictCt)
k DictCt
ct (Bag DictCt
yeses, DictMap DictCt
noes) | DictCt -> Bool
f DictCt
ct = (DictCt
ct DictCt -> Bag DictCt -> Bag DictCt
forall a. a -> Bag a -> Bag a
`consBag` Bag DictCt
yeses, DictMap DictCt
noes)
| Bool
otherwise = (Bag DictCt
yeses, DictCt -> DictMap DictCt -> DictMap DictCt
addDict DictCt
ct DictMap DictCt
noes)
addIrredToCans :: TcLevel -> IrredCt -> InertCans -> InertCans
addIrredToCans :: TcLevel -> IrredCt -> InertCans -> InertCans
addIrredToCans TcLevel
tc_lvl IrredCt
irred InertCans
ics
= TcLevel -> Ct -> InertCans -> InertCans
updGivenEqs TcLevel
tc_lvl (IrredCt -> Ct
CIrredCan IrredCt
irred) (InertCans -> InertCans) -> InertCans -> InertCans
forall a b. (a -> b) -> a -> b
$
(InertIrreds -> InertIrreds) -> InertCans -> InertCans
updIrreds (IrredCt -> InertIrreds -> InertIrreds
addIrred IrredCt
irred) InertCans
ics
addIrreds :: [IrredCt] -> InertIrreds -> InertIrreds
addIrreds :: [IrredCt] -> InertIrreds -> InertIrreds
addIrreds [IrredCt]
extras InertIrreds
irreds
| [IrredCt] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IrredCt]
extras = InertIrreds
irreds
| Bool
otherwise = InertIrreds
irreds InertIrreds -> InertIrreds -> InertIrreds
forall a. Bag a -> Bag a -> Bag a
`unionBags` [IrredCt] -> InertIrreds
forall a. [a] -> Bag a
listToBag [IrredCt]
extras
addIrred :: IrredCt -> InertIrreds -> InertIrreds
addIrred :: IrredCt -> InertIrreds -> InertIrreds
addIrred IrredCt
extra InertIrreds
irreds = InertIrreds
irreds InertIrreds -> IrredCt -> InertIrreds
forall a. Bag a -> a -> Bag a
`snocBag` IrredCt
extra
updIrreds :: (InertIrreds -> InertIrreds) -> InertCans -> InertCans
updIrreds :: (InertIrreds -> InertIrreds) -> InertCans -> InertCans
updIrreds InertIrreds -> InertIrreds
upd InertCans
ics = InertCans
ics { inert_irreds = upd (inert_irreds ics) }
delIrred :: IrredCt -> InertCans -> InertCans
delIrred :: IrredCt -> InertCans -> InertCans
delIrred (IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev }) InertCans
ics
= (InertIrreds -> InertIrreds) -> InertCans -> InertCans
updIrreds ((IrredCt -> Bool) -> InertIrreds -> InertIrreds
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag IrredCt -> Bool
keep) InertCans
ics
where
ev_id :: TcTyVar
ev_id = CtEvidence -> TcTyVar
ctEvEvId CtEvidence
ev
keep :: IrredCt -> Bool
keep (IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev' }) = TcTyVar
ev_id TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
/= CtEvidence -> TcTyVar
ctEvEvId CtEvidence
ev'
foldIrreds :: (IrredCt -> b -> b) -> InertIrreds -> b -> b
foldIrreds :: forall b. (IrredCt -> b -> b) -> InertIrreds -> b -> b
foldIrreds IrredCt -> b -> b
k InertIrreds
irreds b
z = (IrredCt -> b -> b) -> b -> InertIrreds -> b
forall a b. (a -> b -> b) -> b -> Bag a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr IrredCt -> b -> b
k b
z InertIrreds
irreds
findMatchingIrreds :: InertIrreds -> CtEvidence
-> (Bag (IrredCt, SwapFlag), InertIrreds)
findMatchingIrreds :: InertIrreds -> CtEvidence -> (Bag (IrredCt, SwapFlag), InertIrreds)
findMatchingIrreds InertIrreds
irreds CtEvidence
ev
| EqPred EqRel
eq_rel1 Type
lty1 Type
rty1 <- Type -> Pred
classifyPredType Type
pred
= (IrredCt -> Either (IrredCt, SwapFlag) IrredCt)
-> InertIrreds -> (Bag (IrredCt, SwapFlag), InertIrreds)
forall a b c. (a -> Either b c) -> Bag a -> (Bag b, Bag c)
partitionBagWith (EqRel
-> Type -> Type -> IrredCt -> Either (IrredCt, SwapFlag) IrredCt
match_eq EqRel
eq_rel1 Type
lty1 Type
rty1) InertIrreds
irreds
| Bool
otherwise
= (IrredCt -> Either (IrredCt, SwapFlag) IrredCt)
-> InertIrreds -> (Bag (IrredCt, SwapFlag), InertIrreds)
forall a b c. (a -> Either b c) -> Bag a -> (Bag b, Bag c)
partitionBagWith IrredCt -> Either (IrredCt, SwapFlag) IrredCt
match_non_eq InertIrreds
irreds
where
pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
match_non_eq :: IrredCt -> Either (IrredCt, SwapFlag) IrredCt
match_non_eq IrredCt
irred
| IrredCt -> Type
irredCtPred IrredCt
irred HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
pred = (IrredCt, SwapFlag) -> Either (IrredCt, SwapFlag) IrredCt
forall a b. a -> Either a b
Left (IrredCt
irred, SwapFlag
NotSwapped)
| Bool
otherwise = IrredCt -> Either (IrredCt, SwapFlag) IrredCt
forall a b. b -> Either a b
Right IrredCt
irred
match_eq :: EqRel
-> Type -> Type -> IrredCt -> Either (IrredCt, SwapFlag) IrredCt
match_eq EqRel
eq_rel1 Type
lty1 Type
rty1 IrredCt
irred
| EqPred EqRel
eq_rel2 Type
lty2 Type
rty2 <- Type -> Pred
classifyPredType (IrredCt -> Type
irredCtPred IrredCt
irred)
, EqRel
eq_rel1 EqRel -> EqRel -> Bool
forall a. Eq a => a -> a -> Bool
== EqRel
eq_rel2
, Just SwapFlag
swap <- Type -> Type -> Type -> Type -> Maybe SwapFlag
match_eq_help Type
lty1 Type
rty1 Type
lty2 Type
rty2
= (IrredCt, SwapFlag) -> Either (IrredCt, SwapFlag) IrredCt
forall a b. a -> Either a b
Left (IrredCt
irred, SwapFlag
swap)
| Bool
otherwise
= IrredCt -> Either (IrredCt, SwapFlag) IrredCt
forall a b. b -> Either a b
Right IrredCt
irred
match_eq_help :: Type -> Type -> Type -> Type -> Maybe SwapFlag
match_eq_help Type
lty1 Type
rty1 Type
lty2 Type
rty2
| Type
lty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
lty2, Type
rty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
rty2
= SwapFlag -> Maybe SwapFlag
forall a. a -> Maybe a
Just SwapFlag
NotSwapped
| Type
lty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
rty2, Type
rty1 HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
lty2
= SwapFlag -> Maybe SwapFlag
forall a. a -> Maybe a
Just SwapFlag
IsSwapped
| Bool
otherwise
= Maybe SwapFlag
forall a. Maybe a
Nothing
updGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
updGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
updGivenEqs TcLevel
tclvl Ct
ct InertCans
inerts
| Bool -> Bool
not (Ct -> Bool
isGivenCt Ct
ct) = InertCans
inerts
| TcLevel -> Ct -> Bool
isLetBoundSkolemCt TcLevel
tclvl Ct
ct = InertCans
inerts { inert_given_eqs = True }
| Bool
otherwise = InertCans
inerts { inert_given_eq_lvl = tclvl
, inert_given_eqs = True }
isLetBoundSkolemCt :: TcLevel -> Ct -> Bool
isLetBoundSkolemCt :: TcLevel -> Ct -> Bool
isLetBoundSkolemCt TcLevel
tclvl (CEqCan (EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs, eq_rhs :: EqCt -> Type
eq_rhs = Type
rhs }))
= case CanEqLHS
lhs of
TyVarLHS TcTyVar
tv -> Bool -> Bool
not (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv)
TyFamLHS {} -> case Type -> Maybe TcTyVar
getTyVar_maybe Type
rhs of
Just TcTyVar
tv -> Bool -> Bool
not (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv)
Maybe TcTyVar
Nothing -> Bool
False
isLetBoundSkolemCt TcLevel
_ Ct
_ = Bool
False
data KickOutSpec
= KOAfterUnify TcTyVarSet
| KOAfterAdding CanEqLHS
instance Outputable KickOutSpec where
ppr :: KickOutSpec -> SDoc
ppr (KOAfterUnify TcTyVarSet
tvs) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"KOAfterUnify" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> TcTyVarSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVarSet
tvs
ppr (KOAfterAdding CanEqLHS
lhs) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"KOAfterAdding" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs)
data WhereToLook = LookEverywhere | LookOnlyUnderFamApps
deriving( WhereToLook -> WhereToLook -> Bool
(WhereToLook -> WhereToLook -> Bool)
-> (WhereToLook -> WhereToLook -> Bool) -> Eq WhereToLook
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WhereToLook -> WhereToLook -> Bool
== :: WhereToLook -> WhereToLook -> Bool
$c/= :: WhereToLook -> WhereToLook -> Bool
/= :: WhereToLook -> WhereToLook -> Bool
Eq )
kickOutRewritableLHS :: KickOutSpec -> CtFlavourRole -> InertCans -> (Cts, InertCans)
kickOutRewritableLHS :: KickOutSpec -> CtFlavourRole -> InertCans -> (Bag Ct, InertCans)
kickOutRewritableLHS KickOutSpec
ko_spec new_fr :: CtFlavourRole
new_fr@(CtFlavour
_, EqRel
new_role)
ics :: InertCans
ics@(IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
tv_eqs
, inert_dicts :: InertCans -> DictMap DictCt
inert_dicts = DictMap DictCt
dictmap
, inert_funeqs :: InertCans -> InertFunEqs
inert_funeqs = InertFunEqs
funeqmap
, inert_irreds :: InertCans -> InertIrreds
inert_irreds = InertIrreds
irreds
, inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
old_insts })
= (Bag Ct
kicked_out, InertCans
inert_cans_in)
where
inert_cans_in :: InertCans
inert_cans_in = InertCans
ics { inert_eqs = tv_eqs_in
, inert_dicts = dicts_in
, inert_funeqs = feqs_in
, inert_irreds = irs_in
, inert_insts = insts_in }
kicked_out :: Cts
kicked_out :: Bag Ct
kicked_out = ((DictCt -> Ct) -> Bag DictCt -> Bag Ct
forall a b. (a -> b) -> Bag a -> Bag b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DictCt -> Ct
CDictCan Bag DictCt
dicts_out Bag Ct -> Bag Ct -> Bag Ct
`andCts` (IrredCt -> Ct) -> InertIrreds -> Bag Ct
forall a b. (a -> b) -> Bag a -> Bag b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap IrredCt -> Ct
CIrredCan InertIrreds
irs_out)
Bag Ct -> [Ct] -> Bag Ct
`extendCtsList` [Ct]
insts_out
Bag Ct -> [Ct] -> Bag Ct
`extendCtsList` (EqCt -> Ct) -> EqualCtList -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map EqCt -> Ct
CEqCan EqualCtList
tv_eqs_out
Bag Ct -> [Ct] -> Bag Ct
`extendCtsList` (EqCt -> Ct) -> EqualCtList -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map EqCt -> Ct
CEqCan EqualCtList
feqs_out
(EqualCtList
tv_eqs_out, InertEqs
tv_eqs_in) = (EqCt -> Bool) -> InertEqs -> (EqualCtList, InertEqs)
partitionInertEqs EqCt -> Bool
kick_out_eq InertEqs
tv_eqs
(EqualCtList
feqs_out, InertFunEqs
feqs_in) = (EqCt -> Bool) -> InertFunEqs -> (EqualCtList, InertFunEqs)
partitionFunEqs EqCt -> Bool
kick_out_eq InertFunEqs
funeqmap
(Bag DictCt
dicts_out, DictMap DictCt
dicts_in) = (DictCt -> Bool) -> DictMap DictCt -> (Bag DictCt, DictMap DictCt)
partitionDicts DictCt -> Bool
kick_out_dict DictMap DictCt
dictmap
(InertIrreds
irs_out, InertIrreds
irs_in) = (IrredCt -> Bool) -> InertIrreds -> (InertIrreds, InertIrreds)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag IrredCt -> Bool
kick_out_irred InertIrreds
irreds
insts_out :: [Ct]
insts_in :: [QCInst]
([Ct]
insts_out, [QCInst]
insts_in)
| CtFlavourRole -> Bool
fr_may_rewrite (CtFlavour
Given, EqRel
NomEq)
= (QCInst -> Either Ct QCInst) -> [QCInst] -> ([Ct], [QCInst])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith QCInst -> Either Ct QCInst
kick_out_qci [QCInst]
old_insts
| Bool
otherwise
= ([], [QCInst]
old_insts)
kick_out_qci :: QCInst -> Either Ct QCInst
kick_out_qci QCInst
qci
| let ev :: CtEvidence
ev = QCInst -> CtEvidence
qci_ev QCInst
qci
, WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
LookEverywhere EqRel
NomEq (CtEvidence -> Type
ctEvPred (QCInst -> CtEvidence
qci_ev QCInst
qci))
= Ct -> Either Ct QCInst
forall a b. a -> Either a b
Left (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev)
| Bool
otherwise
= QCInst -> Either Ct QCInst
forall a b. b -> Either a b
Right QCInst
qci
fr_tv_can_rewrite_ty :: WhereToLook -> (TyVar -> Bool) -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty :: WhereToLook -> (TcTyVar -> Bool) -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty WhereToLook
where_to_look TcTyVar -> Bool
check_tv EqRel
role Type
ty
= EqRel -> (Bool -> EqRel -> TcTyVar -> Bool) -> Type -> Bool
anyRewritableTyVar EqRel
role Bool -> EqRel -> TcTyVar -> Bool
can_rewrite Type
ty
where
can_rewrite :: UnderFam -> EqRel -> TyVar -> Bool
can_rewrite :: Bool -> EqRel -> TcTyVar -> Bool
can_rewrite Bool
is_under_famapp EqRel
old_role TcTyVar
tv
= (WhereToLook
where_to_look WhereToLook -> WhereToLook -> Bool
forall a. Eq a => a -> a -> Bool
== WhereToLook
LookEverywhere Bool -> Bool -> Bool
|| Bool
is_under_famapp) Bool -> Bool -> Bool
&&
EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&& TcTyVar -> Bool
check_tv TcTyVar
tv
fr_tf_can_rewrite_ty :: WhereToLook -> TyCon -> [TcType] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty :: WhereToLook -> TyCon -> [Type] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty WhereToLook
where_to_look TyCon
new_tf [Type]
new_tf_args EqRel
role Type
ty
= EqRel -> (Bool -> EqRel -> TyCon -> [Type] -> Bool) -> Type -> Bool
anyRewritableTyFamApp EqRel
role Bool -> EqRel -> TyCon -> [Type] -> Bool
can_rewrite Type
ty
where
can_rewrite :: UnderFam -> EqRel -> TyCon -> [TcType] -> Bool
can_rewrite :: Bool -> EqRel -> TyCon -> [Type] -> Bool
can_rewrite Bool
is_under_famapp EqRel
old_role TyCon
old_tf [Type]
old_tf_args
= (WhereToLook
where_to_look WhereToLook -> WhereToLook -> Bool
forall a. Eq a => a -> a -> Bool
== WhereToLook
LookEverywhere Bool -> Bool -> Bool
|| Bool
is_under_famapp) Bool -> Bool -> Bool
&&
EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&&
TyCon -> [Type] -> TyCon -> [Type] -> Bool
tcEqTyConApps TyCon
new_tf [Type]
new_tf_args TyCon
old_tf [Type]
old_tf_args
fr_can_rewrite_ty :: WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty :: WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
uf = case KickOutSpec
ko_spec of
KOAfterUnify TcTyVarSet
tvs -> WhereToLook -> (TcTyVar -> Bool) -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty WhereToLook
uf (TcTyVar -> TcTyVarSet -> Bool
`elemVarSet` TcTyVarSet
tvs)
KOAfterAdding (TyVarLHS TcTyVar
tv) -> WhereToLook -> (TcTyVar -> Bool) -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty WhereToLook
uf (TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv)
KOAfterAdding (TyFamLHS TyCon
tf [Type]
tf_args) -> WhereToLook -> TyCon -> [Type] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty WhereToLook
uf TyCon
tf [Type]
tf_args
fr_may_rewrite :: CtFlavourRole -> Bool
fr_may_rewrite :: CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs = CtFlavourRole
new_fr CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fs
kick_out_dict :: DictCt -> Bool
kick_out_dict :: DictCt -> Bool
kick_out_dict (DictCt { di_tys :: DictCt -> [Type]
di_tys = [Type]
tys, di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev })
= CtFlavourRole -> Bool
fr_may_rewrite (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
NomEq)
Bool -> Bool -> Bool
&& (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
LookEverywhere EqRel
NomEq) [Type]
tys
kick_out_irred :: IrredCt -> Bool
kick_out_irred :: IrredCt -> Bool
kick_out_irred (IrredCt { ir_ev :: IrredCt -> CtEvidence
ir_ev = CtEvidence
ev })
= CtFlavourRole -> Bool
fr_may_rewrite (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel)
Bool -> Bool -> Bool
&& WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
LookEverywhere EqRel
eq_rel Type
pred
where
pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
eq_rel :: EqRel
eq_rel = Type -> EqRel
predTypeEqRel Type
pred
kick_out_eq :: EqCt -> Bool
kick_out_eq :: EqCt -> Bool
kick_out_eq (EqCt { eq_lhs :: EqCt -> CanEqLHS
eq_lhs = CanEqLHS
lhs, eq_rhs :: EqCt -> Type
eq_rhs = Type
rhs_ty
, eq_ev :: EqCt -> CtEvidence
eq_ev = CtEvidence
ev, eq_eq_rel :: EqCt -> EqRel
eq_eq_rel = EqRel
eq_rel })
| Bool -> Bool
not (CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs)
= Bool
False
| WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
LookEverywhere EqRel
eq_rel (CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs)
= Bool
True
| let where_to_look :: WhereToLook
where_to_look | Bool
fs_can_rewrite_fr = WhereToLook
LookOnlyUnderFamApps
| Bool
otherwise = WhereToLook
LookEverywhere
, WhereToLook -> EqRel -> Type -> Bool
fr_can_rewrite_ty WhereToLook
where_to_look EqRel
eq_rel Type
rhs_ty
= Bool
True
| Bool -> Bool
not Bool
fs_can_rewrite_fr
, case EqRel
eq_rel of
EqRel
NomEq -> Type -> Bool
is_new_lhs Type
rhs_ty
EqRel
ReprEq -> Type -> Bool
head_is_new_lhs Type
rhs_ty
= Bool
True
| Bool
otherwise = Bool
False
where
fs_can_rewrite_fr :: Bool
fs_can_rewrite_fr = CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
new_fr
fs :: CtFlavourRole
fs = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel)
is_new_lhs :: Type -> Bool
is_new_lhs :: Type -> Bool
is_new_lhs = case KickOutSpec
ko_spec of
KOAfterUnify TcTyVarSet
tvs -> TcTyVarSet -> Type -> Bool
is_tyvar_ty_for TcTyVarSet
tvs
KOAfterAdding CanEqLHS
lhs -> (HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`eqType` CanEqLHS -> Type
canEqLHSType CanEqLHS
lhs)
is_tyvar_ty_for :: TcTyVarSet -> Type -> Bool
is_tyvar_ty_for :: TcTyVarSet -> Type -> Bool
is_tyvar_ty_for TcTyVarSet
tvs Type
ty
= case Type -> Maybe TcTyVar
getTyVar_maybe Type
ty of
Maybe TcTyVar
Nothing -> Bool
False
Just TcTyVar
tv -> TcTyVar
tv TcTyVar -> TcTyVarSet -> Bool
`elemVarSet` TcTyVarSet
tvs
head_is_new_lhs :: Type -> Bool
head_is_new_lhs :: Type -> Bool
head_is_new_lhs = case KickOutSpec
ko_spec of
KOAfterUnify TcTyVarSet
tvs -> (TcTyVar -> Bool) -> Type -> Bool
tv_at_head (TcTyVar -> TcTyVarSet -> Bool
`elemVarSet` TcTyVarSet
tvs)
KOAfterAdding (TyVarLHS TcTyVar
tv) -> (TcTyVar -> Bool) -> Type -> Bool
tv_at_head (TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv)
KOAfterAdding (TyFamLHS TyCon
tf [Type]
tf_args) -> TyCon -> [Type] -> Type -> Bool
fam_at_head TyCon
tf [Type]
tf_args
tv_at_head :: (TyVar -> Bool) -> Type -> Bool
tv_at_head :: (TcTyVar -> Bool) -> Type -> Bool
tv_at_head TcTyVar -> Bool
is_tv = Type -> Bool
go
where
go :: Type -> Bool
go (Rep.TyVarTy TcTyVar
tv) = TcTyVar -> Bool
is_tv TcTyVar
tv
go (Rep.AppTy Type
fun Type
_) = Type -> Bool
go Type
fun
go (Rep.CastTy Type
ty KindCoercion
_) = Type -> Bool
go Type
ty
go (Rep.TyConApp {}) = Bool
False
go (Rep.LitTy {}) = Bool
False
go (Rep.ForAllTy {}) = Bool
False
go (Rep.FunTy {}) = Bool
False
go (Rep.CoercionTy {}) = Bool
False
fam_at_head :: TyCon -> [Type] -> Type -> Bool
fam_at_head :: TyCon -> [Type] -> Type -> Bool
fam_at_head TyCon
fun_tc [Type]
fun_args = Type -> Bool
go
where
go :: Type -> Bool
go (Rep.TyVarTy {}) = Bool
False
go (Rep.AppTy {}) = Bool
False
go (Rep.CastTy Type
ty KindCoercion
_) = Type -> Bool
go Type
ty
go (Rep.TyConApp TyCon
tc [Type]
args) = TyCon -> [Type] -> TyCon -> [Type] -> Bool
tcEqTyConApps TyCon
fun_tc [Type]
fun_args TyCon
tc [Type]
args
go (Rep.LitTy {}) = Bool
False
go (Rep.ForAllTy {}) = Bool
False
go (Rep.FunTy {}) = Bool
False
go (Rep.CoercionTy {}) = Bool
False
isOuterTyVar :: TcLevel -> TyCoVar -> Bool
isOuterTyVar :: TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv
| TcTyVar -> Bool
isTyVar TcTyVar
tv = Bool -> SDoc -> Bool -> Bool
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Bool -> Bool
not (TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar TcLevel
tclvl TcTyVar
tv)) (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl) (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
TcLevel
tclvl TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
tv
| Bool
otherwise = Bool
False
noGivenNewtypeReprEqs :: TyCon -> InertSet -> Bool
noGivenNewtypeReprEqs :: TyCon -> InertSet -> Bool
noGivenNewtypeReprEqs TyCon
tc InertSet
inerts
= Bool -> Bool
not ((IrredCt -> Bool) -> InertIrreds -> Bool
forall a. (a -> Bool) -> Bag a -> Bool
anyBag IrredCt -> Bool
might_help (InertCans -> InertIrreds
inert_irreds (InertSet -> InertCans
inert_cans InertSet
inerts)))
where
might_help :: IrredCt -> Bool
might_help IrredCt
irred
= case Type -> Pred
classifyPredType (CtEvidence -> Type
ctEvPred (IrredCt -> CtEvidence
irredCtEvidence IrredCt
irred)) of
EqPred EqRel
ReprEq Type
t1 Type
t2
| Just (TyCon
tc1,[Type]
_) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
t1
, TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc1
, Just (TyCon
tc2,[Type]
_) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe Type
t2
, TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
-> Bool
True
Pred
_ -> Bool
False
noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [TcType] -> Bool
noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [Type] -> Bool
noMatchableGivenDicts inerts :: InertSet
inerts@(IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
inert_cans }) CtLoc
loc_w Class
clas [Type]
tys
= Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (DictCt -> Bool) -> Bag DictCt -> Bool
forall a. (a -> Bool) -> Bag a -> Bool
anyBag DictCt -> Bool
matchable_given (Bag DictCt -> Bool) -> Bag DictCt -> Bool
forall a b. (a -> b) -> a -> b
$
DictMap DictCt -> Class -> Bag DictCt
forall a. DictMap a -> Class -> Bag a
findDictsByClass (InertCans -> DictMap DictCt
inert_dicts InertCans
inert_cans) Class
clas
where
pred_w :: Type
pred_w = Class -> [Type] -> Type
mkClassPred Class
clas [Type]
tys
matchable_given :: DictCt -> Bool
matchable_given :: DictCt -> Bool
matchable_given (DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev })
| CtGiven { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc_g, ctev_pred :: CtEvidence -> Type
ctev_pred = Type
pred_g } <- CtEvidence
ev
= Maybe Subst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Subst -> Bool) -> Maybe Subst -> Bool
forall a b. (a -> b) -> a -> b
$ InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst
mightEqualLater InertSet
inerts Type
pred_g CtLoc
loc_g Type
pred_w CtLoc
loc_w
| Bool
otherwise
= Bool
False
mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Maybe Subst
mightEqualLater :: InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst
mightEqualLater InertSet
inert_set Type
given_pred CtLoc
given_loc Type
wanted_pred CtLoc
wanted_loc
| CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
given_loc CtLoc
wanted_loc
= Maybe Subst
forall a. Maybe a
Nothing
| Bool
otherwise
= case BindFun -> [Type] -> [Type] -> UnifyResult
tcUnifyTysFG BindFun
bind_fun [Type
flattened_given] [Type
flattened_wanted] of
Unifiable Subst
subst
-> Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
subst
MaybeApart MaybeApartReason
reason Subst
subst
| MaybeApartReason
MARInfinite <- MaybeApartReason
reason
-> Maybe Subst
forall a. Maybe a
Nothing
| Bool
otherwise
-> Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
subst
UnifyResult
SurelyApart -> Maybe Subst
forall a. Maybe a
Nothing
where
in_scope :: InScopeSet
in_scope = TcTyVarSet -> InScopeSet
mkInScopeSet (TcTyVarSet -> InScopeSet) -> TcTyVarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Type] -> TcTyVarSet
tyCoVarsOfTypes [Type
given_pred, Type
wanted_pred]
([Type
flattened_given, Type
flattened_wanted], TyVarEnv (TyCon, [Type])
var_mapping)
= InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type]))
flattenTysX InScopeSet
in_scope [Type
given_pred, Type
wanted_pred]
bind_fun :: BindFun
bind_fun :: BindFun
bind_fun TcTyVar
tv Type
rhs_ty
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
, TcTyVar -> MetaInfo -> Type -> Bool
can_unify TcTyVar
tv (TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv) Type
rhs_ty
= BindFlag
BindMe
| Just (TyCon
_fam_tc, [Type]
fam_args) <- TyVarEnv (TyCon, [Type]) -> TcTyVar -> Maybe (TyCon, [Type])
forall a. VarEnv a -> TcTyVar -> Maybe a
lookupVarEnv TyVarEnv (TyCon, [Type])
var_mapping TcTyVar
tv
, (TcTyVar -> Bool) -> [Type] -> Bool
anyFreeVarsOfTypes TcTyVar -> Bool
mentions_meta_ty_var [Type]
fam_args
= BindFlag
BindMe
| Bool
otherwise
= BindFlag
Apart
mentions_meta_ty_var :: TyVar -> Bool
mentions_meta_ty_var :: TcTyVar -> Bool
mentions_meta_ty_var TcTyVar
tv
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
= case TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv of
MetaInfo
CycleBreakerTv
-> (TcTyVar -> Bool) -> Type -> Bool
anyFreeVarsOfType TcTyVar -> Bool
mentions_meta_ty_var
(TcTyVar -> InertSet -> Type
lookupCycleBreakerVar TcTyVar
tv InertSet
inert_set)
MetaInfo
_ -> Bool
True
| Bool
otherwise
= Bool
False
can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
can_unify TcTyVar
_lhs_tv MetaInfo
TyVarTv Type
rhs_ty
| Just TcTyVar
rhs_tv <- Type -> Maybe TcTyVar
getTyVar_maybe Type
rhs_ty
= case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
rhs_tv of
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
TyVarTv } -> Bool
True
MetaTv {} -> Bool
False
SkolemTv {} -> Bool
True
TcTyVarDetails
RuntimeUnk -> Bool
True
| Bool
otherwise
= Bool
False
can_unify TcTyVar
lhs_tv MetaInfo
_other Type
_rhs_ty = TcTyVar -> Bool
mentions_meta_ty_var TcTyVar
lhs_tv
prohibitedSuperClassSolve :: CtLoc
-> CtLoc
-> Bool
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
given_loc CtLoc
wanted_loc
| GivenSCOrigin SkolemInfoAnon
_ ScDepth
_ Bool
blocked <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
given_loc
, Bool
blocked
, ScOrigin ClsInstOrQC
_ NakedScFlag
NakedSc <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
wanted_loc
= Bool
True
| Bool
otherwise
= Bool
False
lookupCycleBreakerVar :: TcTyVar
-> InertSet
-> TcType
lookupCycleBreakerVar :: TcTyVar -> InertSet -> Type
lookupCycleBreakerVar TcTyVar
cbv (IS { inert_cycle_breakers :: InertSet -> CycleBreakerVarStack
inert_cycle_breakers = CycleBreakerVarStack
cbvs_stack })
| Just Type
tyfam_app <- Bool -> Maybe Type -> Maybe Type
forall a. HasCallStack => Bool -> a -> a
assert (TcTyVar -> Bool
isCycleBreakerTyVar TcTyVar
cbv) (Maybe Type -> Maybe Type) -> Maybe Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$
NonEmpty (Maybe Type) -> Maybe Type
forall (f :: * -> *) a. Foldable f => f (Maybe a) -> Maybe a
firstJusts ((Bag (TcTyVar, Type) -> Maybe Type)
-> CycleBreakerVarStack -> NonEmpty (Maybe Type)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (TcTyVar -> Bag (TcTyVar, Type) -> Maybe Type
forall a b. Eq a => a -> Bag (a, b) -> Maybe b
lookupBag TcTyVar
cbv) CycleBreakerVarStack
cbvs_stack)
= Type
tyfam_app
| Bool
otherwise
= String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"lookupCycleBreakerVar found an unbound cycle breaker" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
cbv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CycleBreakerVarStack -> SDoc
forall a. Outputable a => a -> SDoc
ppr CycleBreakerVarStack
cbvs_stack)
pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack
pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack
pushCycleBreakerVarStack = (Bag (TcTyVar, Type)
forall a. Bag a
emptyBag Bag (TcTyVar, Type) -> CycleBreakerVarStack -> CycleBreakerVarStack
forall a. a -> NonEmpty a -> NonEmpty a
<|)
addCycleBreakerBindings :: Bag (TcTyVar, Type)
-> InertSet -> InertSet
addCycleBreakerBindings :: Bag (TcTyVar, Type) -> InertSet -> InertSet
addCycleBreakerBindings Bag (TcTyVar, Type)
prs InertSet
ics
= Bool -> SDoc -> InertSet -> InertSet
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (((TcTyVar, Type) -> Bool) -> Bag (TcTyVar, Type) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TcTyVar -> Bool
isCycleBreakerTyVar (TcTyVar -> Bool)
-> ((TcTyVar, Type) -> TcTyVar) -> (TcTyVar, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TcTyVar, Type) -> TcTyVar
forall a b. (a, b) -> a
fst) Bag (TcTyVar, Type)
prs) (Bag (TcTyVar, Type) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag (TcTyVar, Type)
prs) (InertSet -> InertSet) -> InertSet -> InertSet
forall a b. (a -> b) -> a -> b
$
InertSet
ics { inert_cycle_breakers = add_to (inert_cycle_breakers ics) }
where
add_to :: CycleBreakerVarStack -> CycleBreakerVarStack
add_to (Bag (TcTyVar, Type)
top_env :| [Bag (TcTyVar, Type)]
rest_envs) = (Bag (TcTyVar, Type)
prs Bag (TcTyVar, Type) -> Bag (TcTyVar, Type) -> Bag (TcTyVar, Type)
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag (TcTyVar, Type)
top_env) Bag (TcTyVar, Type)
-> [Bag (TcTyVar, Type)] -> CycleBreakerVarStack
forall a. a -> [a] -> NonEmpty a
:| [Bag (TcTyVar, Type)]
rest_envs
forAllCycleBreakerBindings_ :: Monad m
=> CycleBreakerVarStack
-> (TcTyVar -> TcType -> m ()) -> m ()
forAllCycleBreakerBindings_ :: forall (m :: * -> *).
Monad m =>
CycleBreakerVarStack -> (TcTyVar -> Type -> m ()) -> m ()
forAllCycleBreakerBindings_ (Bag (TcTyVar, Type)
top_env :| [Bag (TcTyVar, Type)]
_rest_envs) TcTyVar -> Type -> m ()
action
= Bag (TcTyVar, Type) -> ((TcTyVar, Type) -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Bag (TcTyVar, Type)
top_env ((TcTyVar -> Type -> m ()) -> (TcTyVar, Type) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TcTyVar -> Type -> m ()
action)
{-# INLINABLE forAllCycleBreakerBindings_ #-}
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
`sameDepthAs` 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 :: Type
pred = CtEvidence -> Type
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
| Type -> Bool
isIPLikePred Type
pred = if TcLevel
lvl_w TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lvl_i then InteractResult
KeepWork else InteractResult
KeepInert
| Bool
otherwise = if TcLevel
lvl_w TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` 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