{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Tc.Solver.InertSet (
WorkList(..), isEmptyWorkList, emptyWorkList,
extendWorkListNonEq, extendWorkListCt,
extendWorkListCts, extendWorkListEq,
appendWorkList, extendWorkListImplic,
workListSize,
selectWorkItem,
InertSet(..),
InertCans(..),
InertEqs,
emptyInert,
addInertItem,
matchableGivens,
mightEqualLater,
prohibitedSuperClassSolve,
foldTyEqs, delEq, findEq,
partitionInertEqs, partitionFunEqs,
kickOutRewritableLHS
) where
import GHC.Prelude
import GHC.Tc.Solver.Types
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Core.Reduction
import GHC.Core.Predicate
import GHC.Core.TyCo.FVs
import qualified GHC.Core.TyCo.Rep as Rep
import GHC.Core.TyCon
import GHC.Core.Unify
import GHC.Data.Bag
import GHC.Utils.Misc ( partitionWith )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import Data.List ( partition )
data WorkList
= WL { WorkList -> [Ct]
wl_eqs :: [Ct]
, WorkList -> [Ct]
wl_rest :: [Ct]
, WorkList -> Bag Implication
wl_implics :: Bag Implication
}
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList :: WorkList -> WorkList -> WorkList
appendWorkList
(WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs1, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest1
, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics1 })
(WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs2, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest2
, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics2 })
= WL :: [Ct] -> [Ct] -> Bag Implication -> WorkList
WL { wl_eqs :: [Ct]
wl_eqs = [Ct]
eqs1 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
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 -> Int
workListSize (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
= [Ct] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
eqs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Ct] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Ct]
rest
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq :: Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl = WorkList
wl { wl_eqs :: [Ct]
wl_eqs = Ct
ct Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: WorkList -> [Ct]
wl_eqs WorkList
wl }
extendWorkListNonEq :: Ct -> WorkList -> WorkList
extendWorkListNonEq :: Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl = WorkList
wl { wl_rest :: [Ct]
wl_rest = Ct
ct Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: WorkList -> [Ct]
wl_rest WorkList
wl }
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic :: Implication -> WorkList -> WorkList
extendWorkListImplic Implication
implic WorkList
wl = WorkList
wl { wl_implics :: Bag Implication
wl_implics = Implication
implic Implication -> Bag Implication -> Bag Implication
forall a. a -> Bag a -> Bag a
`consBag` WorkList -> Bag Implication
wl_implics WorkList
wl }
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt :: Ct -> WorkList -> WorkList
extendWorkListCt Ct
ct WorkList
wl
= case PredType -> Pred
classifyPredType (Ct -> PredType
ctPred Ct
ct) of
EqPred {}
-> Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl
ClassPred Class
cls [PredType]
_
| Class -> Bool
isEqPredClass Class
cls
-> Ct -> WorkList -> WorkList
extendWorkListEq Ct
ct WorkList
wl
Pred
_ -> Ct -> WorkList -> WorkList
extendWorkListNonEq Ct
ct WorkList
wl
extendWorkListCts :: [Ct] -> WorkList -> WorkList
extendWorkListCts :: [Ct] -> WorkList -> WorkList
extendWorkListCts [Ct]
cts WorkList
wl = (Ct -> WorkList -> WorkList) -> WorkList -> [Ct] -> WorkList
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> WorkList -> WorkList
extendWorkListCt WorkList
wl [Ct]
cts
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList :: WorkList -> Bool
isEmptyWorkList (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
= [Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs Bool -> Bool -> Bool
&& [Ct] -> 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 :: [Ct] -> [Ct] -> Bag Implication -> WorkList
WL { wl_eqs :: [Ct]
wl_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 :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest })
| Ct
ct:[Ct]
cts <- [Ct]
eqs = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_eqs :: [Ct]
wl_eqs = [Ct]
cts })
| Ct
ct:[Ct]
cts <- [Ct]
rest = (Ct, WorkList) -> Maybe (Ct, WorkList)
forall a. a -> Maybe a
Just (Ct
ct, WorkList
wl { wl_rest :: [Ct]
wl_rest = [Ct]
cts })
| Bool
otherwise = Maybe (Ct, WorkList)
forall a. Maybe a
Nothing
instance Outputable WorkList where
ppr :: WorkList -> SDoc
ppr (WL { wl_eqs :: WorkList -> [Ct]
wl_eqs = [Ct]
eqs, wl_rest :: WorkList -> [Ct]
wl_rest = [Ct]
rest, wl_implics :: WorkList -> Bag Implication
wl_implics = Bag Implication
implics })
= String -> SDoc
text String
"WL" SDoc -> SDoc -> SDoc
<+> (SDoc -> SDoc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Bool -> SDoc -> SDoc
ppUnless ([Ct] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
eqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Eqs =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((Ct -> SDoc) -> [Ct] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
eqs)
, Bool -> SDoc -> SDoc
ppUnless ([Ct] -> 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
text String
"Non-eqs =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
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
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
ifPprDebug (String -> SDoc
text String
"Implics =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
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
text String
"(Implics omitted)")
])
data InertSet
= IS { InertSet -> InertCans
inert_cans :: InertCans
, InertSet -> [(TcTyVar, PredType)]
inert_cycle_breakers :: [(TcTyVar, TcType)]
, InertSet -> FunEqMap Reduction
inert_famapp_cache :: FunEqMap Reduction
, InertSet -> DictMap CtEvidence
inert_solved_dicts :: DictMap CtEvidence
}
instance Outputable InertSet where
ppr :: InertSet -> SDoc
ppr (IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
ics
, inert_solved_dicts :: InertSet -> DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
solved_dicts })
= [SDoc] -> SDoc
vcat [ InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
ics
, Bool -> SDoc -> SDoc
ppUnless ([CtEvidence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CtEvidence]
dicts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Solved dicts =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat ((CtEvidence -> SDoc) -> [CtEvidence] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CtEvidence]
dicts) ]
where
dicts :: [CtEvidence]
dicts = Bag CtEvidence -> [CtEvidence]
forall a. Bag a -> [a]
bagToList (DictMap CtEvidence -> Bag CtEvidence
forall a. DictMap a -> Bag a
dictsToBag DictMap CtEvidence
solved_dicts)
emptyInertCans :: InertCans
emptyInertCans :: InertCans
emptyInertCans
= IC :: InertEqs
-> FunEqMap [Ct]
-> DictMap Ct
-> [QCInst]
-> DictMap Ct
-> Cts
-> TcLevel
-> Bool
-> InertCans
IC { inert_eqs :: InertEqs
inert_eqs = InertEqs
forall a. DVarEnv a
emptyDVarEnv
, inert_given_eq_lvl :: TcLevel
inert_given_eq_lvl = TcLevel
topTcLevel
, inert_given_eqs :: Bool
inert_given_eqs = Bool
False
, inert_dicts :: DictMap Ct
inert_dicts = DictMap Ct
forall a. DictMap a
emptyDictMap
, inert_safehask :: DictMap Ct
inert_safehask = DictMap Ct
forall a. DictMap a
emptyDictMap
, inert_funeqs :: FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct]
forall a. DictMap a
emptyFunEqs
, inert_insts :: [QCInst]
inert_insts = []
, inert_irreds :: Cts
inert_irreds = Cts
emptyCts }
emptyInert :: InertSet
emptyInert :: InertSet
emptyInert
= IS :: InertCans
-> [(TcTyVar, PredType)]
-> FunEqMap Reduction
-> DictMap CtEvidence
-> InertSet
IS { inert_cans :: InertCans
inert_cans = InertCans
emptyInertCans
, inert_cycle_breakers :: [(TcTyVar, PredType)]
inert_cycle_breakers = []
, inert_famapp_cache :: FunEqMap Reduction
inert_famapp_cache = FunEqMap Reduction
forall a. DictMap a
emptyFunEqs
, inert_solved_dicts :: DictMap CtEvidence
inert_solved_dicts = DictMap CtEvidence
forall a. DictMap a
emptyDictMap }
data InertCans
= IC { InertCans -> InertEqs
inert_eqs :: InertEqs
, InertCans -> FunEqMap [Ct]
inert_funeqs :: FunEqMap EqualCtList
, InertCans -> DictMap Ct
inert_dicts :: DictMap Ct
, InertCans -> [QCInst]
inert_insts :: [QCInst]
, InertCans -> DictMap Ct
inert_safehask :: DictMap Ct
, InertCans -> Cts
inert_irreds :: Cts
, InertCans -> TcLevel
inert_given_eq_lvl :: TcLevel
, InertCans -> Bool
inert_given_eqs :: Bool
}
type InertEqs = DTyVarEnv EqualCtList
instance Outputable InertCans where
ppr :: InertCans -> SDoc
ppr (IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs
, inert_funeqs :: InertCans -> FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct]
funeqs
, inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
dicts
, inert_safehask :: InertCans -> DictMap Ct
inert_safehask = DictMap Ct
safehask
, inert_irreds :: InertCans -> Cts
inert_irreds = Cts
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
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
[ Bool -> SDoc -> SDoc
ppUnless (InertEqs -> Bool
forall a. DVarEnv a -> Bool
isEmptyDVarEnv InertEqs
eqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Equalities:"
SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
pprCts (([Ct] -> Cts -> Cts) -> Cts -> InertEqs -> Cts
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv [Ct] -> Cts -> Cts
folder Cts
emptyCts InertEqs
eqs)
, Bool -> SDoc -> SDoc
ppUnless (FunEqMap [Ct] -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap FunEqMap [Ct]
funeqs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Type-function equalities =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
pprCts (([Ct] -> Cts -> Cts) -> FunEqMap [Ct] -> Cts -> Cts
forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs [Ct] -> Cts -> Cts
folder FunEqMap [Ct]
funeqs Cts
emptyCts)
, Bool -> SDoc -> SDoc
ppUnless (DictMap Ct -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap Ct
dicts) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Dictionaries =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
pprCts (DictMap Ct -> Cts
forall a. DictMap a -> Bag a
dictsToBag DictMap Ct
dicts)
, Bool -> SDoc -> SDoc
ppUnless (DictMap Ct -> Bool
forall a. TcAppMap a -> Bool
isEmptyTcAppMap DictMap Ct
safehask) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Safe Haskell unsafe overlap =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
pprCts (DictMap Ct -> Cts
forall a. DictMap a -> Bag a
dictsToBag DictMap Ct
safehask)
, Bool -> SDoc -> SDoc
ppUnless (Cts -> Bool
isEmptyCts Cts
irreds) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Irreds =" SDoc -> SDoc -> SDoc
<+> Cts -> SDoc
pprCts Cts
irreds
, Bool -> SDoc -> SDoc
ppUnless ([QCInst] -> 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
text String
"Given instances =" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
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
text String
"Innermost given equalities =" SDoc -> SDoc -> SDoc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
ge_lvl
, String -> SDoc
text String
"Given eqs at this level =" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
given_eqs
]
where
folder :: [Ct] -> Cts -> Cts
folder [Ct]
eqs Cts
rest = [Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
eqs Cts -> Cts -> Cts
`andCts` Cts
rest
addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq InertEqs
old_eqs TcTyVar
tv Ct
ct
= ([Ct] -> [Ct] -> [Ct]) -> InertEqs -> TcTyVar -> [Ct] -> InertEqs
forall a. (a -> a -> a) -> DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv_C [Ct] -> [Ct] -> [Ct]
add_eq InertEqs
old_eqs TcTyVar
tv [Ct
ct]
where
add_eq :: [Ct] -> [Ct] -> [Ct]
add_eq [Ct]
old_eqs [Ct]
_ = Ct -> [Ct] -> [Ct]
addToEqualCtList Ct
ct [Ct]
old_eqs
addCanFunEq :: FunEqMap EqualCtList -> TyCon -> [TcType] -> Ct
-> FunEqMap EqualCtList
addCanFunEq :: FunEqMap [Ct] -> TyCon -> [PredType] -> Ct -> FunEqMap [Ct]
addCanFunEq FunEqMap [Ct]
old_eqs TyCon
fun_tc [PredType]
fun_args Ct
ct
= FunEqMap [Ct] -> TyCon -> [PredType] -> XT [Ct] -> FunEqMap [Ct]
forall a. TcAppMap a -> TyCon -> [PredType] -> XT a -> TcAppMap a
alterTcApp FunEqMap [Ct]
old_eqs TyCon
fun_tc [PredType]
fun_args XT [Ct]
upd
where
upd :: XT [Ct]
upd (Just [Ct]
old_equal_ct_list) = [Ct] -> Maybe [Ct]
forall a. a -> Maybe a
Just ([Ct] -> Maybe [Ct]) -> [Ct] -> Maybe [Ct]
forall a b. (a -> b) -> a -> b
$ Ct -> [Ct] -> [Ct]
addToEqualCtList Ct
ct [Ct]
old_equal_ct_list
upd Maybe [Ct]
Nothing = [Ct] -> Maybe [Ct]
forall a. a -> Maybe a
Just [Ct
ct]
foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
foldTyEqs Ct -> b -> b
k InertEqs
eqs b
z
= ([Ct] -> b -> b) -> b -> InertEqs -> b
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv (\[Ct]
cts b
z -> (Ct -> b -> b) -> b -> [Ct] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> b -> b
k b
z [Ct]
cts) b
z InertEqs
eqs
findTyEqs :: InertCans -> TyVar -> [Ct]
findTyEqs :: InertCans -> TcTyVar -> [Ct]
findTyEqs InertCans
icans TcTyVar
tv = Maybe [Ct] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat @Maybe (InertEqs -> TcTyVar -> Maybe [Ct]
forall a. DVarEnv a -> TcTyVar -> Maybe a
lookupDVarEnv (InertCans -> InertEqs
inert_eqs InertCans
icans) TcTyVar
tv)
delEq :: InertCans -> CanEqLHS -> TcType -> InertCans
delEq :: InertCans -> CanEqLHS -> PredType -> InertCans
delEq InertCans
ic CanEqLHS
lhs PredType
rhs = case CanEqLHS
lhs of
TyVarLHS TcTyVar
tv
-> InertCans
ic { inert_eqs :: InertEqs
inert_eqs = XT [Ct] -> InertEqs -> TcTyVar -> InertEqs
forall a. (Maybe a -> Maybe a) -> DVarEnv a -> TcTyVar -> DVarEnv a
alterDVarEnv XT [Ct]
upd (InertCans -> InertEqs
inert_eqs InertCans
ic) TcTyVar
tv }
TyFamLHS TyCon
tf [PredType]
args
-> InertCans
ic { inert_funeqs :: FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct] -> TyCon -> [PredType] -> XT [Ct] -> FunEqMap [Ct]
forall a. TcAppMap a -> TyCon -> [PredType] -> XT a -> TcAppMap a
alterTcApp (InertCans -> FunEqMap [Ct]
inert_funeqs InertCans
ic) TyCon
tf [PredType]
args XT [Ct]
upd }
where
isThisOne :: Ct -> Bool
isThisOne :: Ct -> Bool
isThisOne (CEqCan { cc_rhs :: Ct -> PredType
cc_rhs = PredType
t1 }) = PredType -> PredType -> Bool
tcEqTypeNoKindCheck PredType
rhs PredType
t1
isThisOne Ct
other = String -> SDoc -> Bool
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"delEq" (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
lhs SDoc -> SDoc -> SDoc
$$ InertCans -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertCans
ic SDoc -> SDoc -> SDoc
$$ Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
other)
upd :: Maybe EqualCtList -> Maybe EqualCtList
upd :: XT [Ct]
upd (Just [Ct]
eq_ct_list) = (Ct -> Bool) -> [Ct] -> Maybe [Ct]
filterEqualCtList (Bool -> Bool
not (Bool -> Bool) -> (Ct -> Bool) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> Bool
isThisOne) [Ct]
eq_ct_list
upd Maybe [Ct]
Nothing = Maybe [Ct]
forall a. Maybe a
Nothing
findEq :: InertCans -> CanEqLHS -> [Ct]
findEq :: InertCans -> CanEqLHS -> [Ct]
findEq InertCans
icans (TyVarLHS TcTyVar
tv) = InertCans -> TcTyVar -> [Ct]
findTyEqs InertCans
icans TcTyVar
tv
findEq InertCans
icans (TyFamLHS TyCon
fun_tc [PredType]
fun_args)
= Maybe [Ct] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat @Maybe (FunEqMap [Ct] -> TyCon -> [PredType] -> Maybe [Ct]
forall a. FunEqMap a -> TyCon -> [PredType] -> Maybe a
findFunEq (InertCans -> FunEqMap [Ct]
inert_funeqs InertCans
icans) TyCon
fun_tc [PredType]
fun_args)
{-# INLINE partition_eqs_container #-}
partition_eqs_container
:: forall container
. container
-> (forall b. (EqualCtList -> b -> b) -> b -> container -> b)
-> (container -> CanEqLHS -> EqualCtList -> container)
-> (Ct -> Bool)
-> container
-> ([Ct], container)
partition_eqs_container :: container
-> (forall b. ([Ct] -> b -> b) -> b -> container -> b)
-> (container -> CanEqLHS -> [Ct] -> container)
-> (Ct -> Bool)
-> container
-> ([Ct], container)
partition_eqs_container container
empty_container forall b. ([Ct] -> b -> b) -> b -> container -> b
fold_container container -> CanEqLHS -> [Ct] -> container
extend_container Ct -> Bool
pred container
orig_inerts
= ([Ct] -> ([Ct], container) -> ([Ct], container))
-> ([Ct], container) -> container -> ([Ct], container)
forall b. ([Ct] -> b -> b) -> b -> container -> b
fold_container [Ct] -> ([Ct], container) -> ([Ct], container)
folder ([], container
empty_container) container
orig_inerts
where
folder :: EqualCtList -> ([Ct], container) -> ([Ct], container)
folder :: [Ct] -> ([Ct], container) -> ([Ct], container)
folder [Ct]
eqs ([Ct]
acc_true, container
acc_false)
= ([Ct]
eqs_true [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
acc_true, container
acc_false')
where
([Ct]
eqs_true, [Ct]
eqs_false) = (Ct -> Bool) -> [Ct] -> ([Ct], [Ct])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Ct -> Bool
pred [Ct]
eqs
acc_false' :: container
acc_false'
| CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs } : [Ct]
_ <- [Ct]
eqs_false
= container -> CanEqLHS -> [Ct] -> container
extend_container container
acc_false CanEqLHS
lhs [Ct]
eqs_false
| Bool
otherwise
= container
acc_false
partitionInertEqs :: (Ct -> Bool)
-> InertEqs
-> ([Ct], InertEqs)
partitionInertEqs :: (Ct -> Bool) -> InertEqs -> ([Ct], InertEqs)
partitionInertEqs = InertEqs
-> (forall b. ([Ct] -> b -> b) -> b -> InertEqs -> b)
-> (InertEqs -> CanEqLHS -> [Ct] -> InertEqs)
-> (Ct -> Bool)
-> InertEqs
-> ([Ct], InertEqs)
forall container.
container
-> (forall b. ([Ct] -> b -> b) -> b -> container -> b)
-> (container -> CanEqLHS -> [Ct] -> container)
-> (Ct -> Bool)
-> container
-> ([Ct], container)
partition_eqs_container InertEqs
forall a. DVarEnv a
emptyDVarEnv forall b. ([Ct] -> b -> b) -> b -> InertEqs -> b
forall a b. (a -> b -> b) -> b -> DVarEnv a -> b
foldDVarEnv InertEqs -> CanEqLHS -> [Ct] -> InertEqs
extendInertEqs
extendInertEqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
extendInertEqs :: InertEqs -> CanEqLHS -> [Ct] -> InertEqs
extendInertEqs InertEqs
eqs (TyVarLHS TcTyVar
tv) [Ct]
new_eqs = InertEqs -> TcTyVar -> [Ct] -> InertEqs
forall a. DVarEnv a -> TcTyVar -> a -> DVarEnv a
extendDVarEnv InertEqs
eqs TcTyVar
tv [Ct]
new_eqs
extendInertEqs InertEqs
_ CanEqLHS
other [Ct]
_ = String -> SDoc -> InertEqs
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendInertEqs" (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
other)
partitionFunEqs :: (Ct -> Bool)
-> FunEqMap EqualCtList
-> ([Ct], FunEqMap EqualCtList)
partitionFunEqs :: (Ct -> Bool) -> FunEqMap [Ct] -> ([Ct], FunEqMap [Ct])
partitionFunEqs
= FunEqMap [Ct]
-> (forall b. ([Ct] -> b -> b) -> b -> FunEqMap [Ct] -> b)
-> (FunEqMap [Ct] -> CanEqLHS -> [Ct] -> FunEqMap [Ct])
-> (Ct -> Bool)
-> FunEqMap [Ct]
-> ([Ct], FunEqMap [Ct])
forall container.
container
-> (forall b. ([Ct] -> b -> b) -> b -> container -> b)
-> (container -> CanEqLHS -> [Ct] -> container)
-> (Ct -> Bool)
-> container
-> ([Ct], container)
partition_eqs_container FunEqMap [Ct]
forall a. DictMap a
emptyFunEqs (\ [Ct] -> b -> b
f b
z FunEqMap [Ct]
eqs -> ([Ct] -> b -> b) -> FunEqMap [Ct] -> b -> b
forall a b. (a -> b -> b) -> FunEqMap a -> b -> b
foldFunEqs [Ct] -> b -> b
f FunEqMap [Ct]
eqs b
z) FunEqMap [Ct] -> CanEqLHS -> [Ct] -> FunEqMap [Ct]
extendFunEqs
extendFunEqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList -> FunEqMap EqualCtList
extendFunEqs :: FunEqMap [Ct] -> CanEqLHS -> [Ct] -> FunEqMap [Ct]
extendFunEqs FunEqMap [Ct]
eqs (TyFamLHS TyCon
tf [PredType]
args) [Ct]
new_eqs = FunEqMap [Ct] -> TyCon -> [PredType] -> [Ct] -> FunEqMap [Ct]
forall a. TcAppMap a -> TyCon -> [PredType] -> a -> TcAppMap a
insertTcApp FunEqMap [Ct]
eqs TyCon
tf [PredType]
args [Ct]
new_eqs
extendFunEqs FunEqMap [Ct]
_ CanEqLHS
other [Ct]
_ = String -> SDoc -> FunEqMap [Ct]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendFunEqs" (CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
other)
addInertItem :: TcLevel -> InertCans -> Ct -> InertCans
addInertItem :: TcLevel -> InertCans -> Ct -> InertCans
addInertItem TcLevel
tc_lvl
ics :: InertCans
ics@(IC { inert_funeqs :: InertCans -> FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct]
funeqs, inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
eqs })
item :: Ct
item@(CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs })
= TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tc_lvl Ct
item (InertCans -> InertCans) -> InertCans -> InertCans
forall a b. (a -> b) -> a -> b
$
case CanEqLHS
lhs of
TyFamLHS TyCon
tc [PredType]
tys -> InertCans
ics { inert_funeqs :: FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct] -> TyCon -> [PredType] -> Ct -> FunEqMap [Ct]
addCanFunEq FunEqMap [Ct]
funeqs TyCon
tc [PredType]
tys Ct
item }
TyVarLHS TcTyVar
tv -> InertCans
ics { inert_eqs :: InertEqs
inert_eqs = InertEqs -> TcTyVar -> Ct -> InertEqs
addTyEq InertEqs
eqs TcTyVar
tv Ct
item }
addInertItem TcLevel
tc_lvl ics :: InertCans
ics@(IC { inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds }) item :: Ct
item@(CIrredCan {})
= TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tc_lvl Ct
item (InertCans -> InertCans) -> InertCans -> InertCans
forall a b. (a -> b) -> a -> b
$
InertCans
ics { inert_irreds :: Cts
inert_irreds = Cts
irreds Cts -> Ct -> Cts
forall a. Bag a -> a -> Bag a
`snocBag` Ct
item }
addInertItem TcLevel
_ InertCans
ics item :: Ct
item@(CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls, cc_tyargs :: Ct -> [PredType]
cc_tyargs = [PredType]
tys })
= InertCans
ics { inert_dicts :: DictMap Ct
inert_dicts = DictMap Ct -> Class -> [PredType] -> Ct -> DictMap Ct
forall a. DictMap a -> Class -> [PredType] -> a -> DictMap a
addDict (InertCans -> DictMap Ct
inert_dicts InertCans
ics) Class
cls [PredType]
tys Ct
item }
addInertItem TcLevel
_ ics :: InertCans
ics@( IC { inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds }) item :: Ct
item@(CSpecialCan {})
= InertCans
ics { inert_irreds :: Cts
inert_irreds = Cts
irreds Cts -> Ct -> Cts
forall a. Bag a -> a -> Bag a
`snocBag` Ct
item }
addInertItem TcLevel
_ InertCans
_ Ct
item
= String -> SDoc -> InertCans
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"upd_inert set: can't happen! Inserting " (SDoc -> InertCans) -> SDoc -> InertCans
forall a b. (a -> b) -> a -> b
$
Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
item
updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
updateGivenEqs TcLevel
tclvl Ct
ct inerts :: InertCans
inerts@(IC { inert_given_eq_lvl :: InertCans -> TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl })
| Bool -> Bool
not (Ct -> Bool
isGivenCt Ct
ct) = InertCans
inerts
| Ct -> Bool
not_equality Ct
ct = InertCans
inerts
| Bool
otherwise = InertCans
inerts { inert_given_eq_lvl :: TcLevel
inert_given_eq_lvl = TcLevel
ge_lvl'
, inert_given_eqs :: Bool
inert_given_eqs = Bool
True }
where
ge_lvl' :: TcLevel
ge_lvl' | TcLevel -> CtEvidence -> Bool
mentionsOuterVar TcLevel
tclvl (Ct -> CtEvidence
ctEvidence Ct
ct)
= TcLevel
tclvl
| Bool
otherwise
= TcLevel
ge_lvl
not_equality :: Ct -> Bool
not_equality :: Ct -> Bool
not_equality (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = TyVarLHS TcTyVar
tv }) = Bool -> Bool
not (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl TcTyVar
tv)
not_equality (CDictCan {}) = Bool
True
not_equality Ct
_ = Bool
False
kickOutRewritableLHS :: CtFlavourRole
-> CanEqLHS
-> InertCans
-> (WorkList, InertCans)
kickOutRewritableLHS :: CtFlavourRole -> CanEqLHS -> InertCans -> (WorkList, InertCans)
kickOutRewritableLHS CtFlavourRole
new_fr CanEqLHS
new_lhs
ics :: InertCans
ics@(IC { inert_eqs :: InertCans -> InertEqs
inert_eqs = InertEqs
tv_eqs
, inert_dicts :: InertCans -> DictMap Ct
inert_dicts = DictMap Ct
dictmap
, inert_funeqs :: InertCans -> FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct]
funeqmap
, inert_irreds :: InertCans -> Cts
inert_irreds = Cts
irreds
, inert_insts :: InertCans -> [QCInst]
inert_insts = [QCInst]
old_insts })
= (WorkList
kicked_out, InertCans
inert_cans_in)
where
inert_cans_in :: InertCans
inert_cans_in = InertCans
ics { inert_eqs :: InertEqs
inert_eqs = InertEqs
tv_eqs_in
, inert_dicts :: DictMap Ct
inert_dicts = DictMap Ct
dicts_in
, inert_funeqs :: FunEqMap [Ct]
inert_funeqs = FunEqMap [Ct]
feqs_in
, inert_irreds :: Cts
inert_irreds = Cts
irs_in
, inert_insts :: [QCInst]
inert_insts = [QCInst]
insts_in }
kicked_out :: WorkList
kicked_out :: WorkList
kicked_out = (Ct -> WorkList -> WorkList) -> WorkList -> Cts -> WorkList
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ct -> WorkList -> WorkList
extendWorkListCt
(WorkList
emptyWorkList { wl_eqs :: [Ct]
wl_eqs = [Ct]
tv_eqs_out [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
feqs_out })
((Cts
dicts_out Cts -> Cts -> Cts
`andCts` Cts
irs_out)
Cts -> [Ct] -> Cts
`extendCtsList` [Ct]
insts_out)
([Ct]
tv_eqs_out, InertEqs
tv_eqs_in) = (Ct -> Bool) -> InertEqs -> ([Ct], InertEqs)
partitionInertEqs Ct -> Bool
kick_out_eq InertEqs
tv_eqs
([Ct]
feqs_out, FunEqMap [Ct]
feqs_in) = (Ct -> Bool) -> FunEqMap [Ct] -> ([Ct], FunEqMap [Ct])
partitionFunEqs Ct -> Bool
kick_out_eq FunEqMap [Ct]
funeqmap
(Cts
dicts_out, DictMap Ct
dicts_in) = (Ct -> Bool) -> DictMap Ct -> (Cts, DictMap Ct)
partitionDicts Ct -> Bool
kick_out_ct DictMap Ct
dictmap
(Cts
irs_out, Cts
irs_in) = (Ct -> Bool) -> Cts -> (Cts, Cts)
forall a. (a -> Bool) -> Bag a -> (Bag a, Bag a)
partitionBag Ct -> Bool
kick_out_ct Cts
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
, EqRel -> PredType -> Bool
fr_can_rewrite_ty EqRel
NomEq (CtEvidence -> PredType
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
(CtFlavour
_, EqRel
new_role) = CtFlavourRole
new_fr
fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool
fr_tv_can_rewrite_ty :: TcTyVar -> EqRel -> PredType -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv EqRel
role PredType
ty
= EqRel -> (EqRel -> TcTyVar -> Bool) -> PredType -> Bool
anyRewritableTyVar EqRel
role EqRel -> TcTyVar -> Bool
can_rewrite PredType
ty
where
can_rewrite :: EqRel -> TyVar -> Bool
can_rewrite :: EqRel -> TcTyVar -> Bool
can_rewrite EqRel
old_role TcTyVar
tv = EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&& TcTyVar
tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
new_tv
fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> Type -> Bool
fr_tf_can_rewrite_ty :: TyCon -> [PredType] -> EqRel -> PredType -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [PredType]
new_tf_args EqRel
role PredType
ty
= EqRel -> (EqRel -> TyCon -> [PredType] -> Bool) -> PredType -> Bool
anyRewritableTyFamApp EqRel
role EqRel -> TyCon -> [PredType] -> Bool
can_rewrite PredType
ty
where
can_rewrite :: EqRel -> TyCon -> [TcType] -> Bool
can_rewrite :: EqRel -> TyCon -> [PredType] -> Bool
can_rewrite EqRel
old_role TyCon
old_tf [PredType]
old_tf_args
= EqRel
new_role EqRel -> EqRel -> Bool
`eqCanRewrite` EqRel
old_role Bool -> Bool -> Bool
&&
TyCon -> [PredType] -> TyCon -> [PredType] -> Bool
tcEqTyConApps TyCon
new_tf [PredType]
new_tf_args TyCon
old_tf [PredType]
old_tf_args
{-# INLINE fr_can_rewrite_ty #-}
fr_can_rewrite_ty :: EqRel -> Type -> Bool
fr_can_rewrite_ty :: EqRel -> PredType -> Bool
fr_can_rewrite_ty = case CanEqLHS
new_lhs of
TyVarLHS TcTyVar
new_tv -> TcTyVar -> EqRel -> PredType -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv
TyFamLHS TyCon
new_tf [PredType]
new_tf_args -> TyCon -> [PredType] -> EqRel -> PredType -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [PredType]
new_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
{-# INLINE kick_out_ct #-}
kick_out_ct :: Ct -> Bool
kick_out_ct :: Ct -> Bool
kick_out_ct = case CanEqLHS
new_lhs of
TyVarLHS TcTyVar
new_tv -> \Ct
ct -> let fs :: CtFlavourRole
fs@(CtFlavour
_,EqRel
role) = Ct -> CtFlavourRole
ctFlavourRole Ct
ct in
CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs
Bool -> Bool -> Bool
&& TcTyVar -> EqRel -> PredType -> Bool
fr_tv_can_rewrite_ty TcTyVar
new_tv EqRel
role (Ct -> PredType
ctPred Ct
ct)
TyFamLHS TyCon
new_tf [PredType]
new_tf_args
-> \Ct
ct -> let fs :: CtFlavourRole
fs@(CtFlavour
_, EqRel
role) = Ct -> CtFlavourRole
ctFlavourRole Ct
ct in
CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs
Bool -> Bool -> Bool
&& TyCon -> [PredType] -> EqRel -> PredType -> Bool
fr_tf_can_rewrite_ty TyCon
new_tf [PredType]
new_tf_args EqRel
role (Ct -> PredType
ctPred Ct
ct)
kick_out_eq :: Ct -> Bool
kick_out_eq :: Ct -> Bool
kick_out_eq (CEqCan { cc_lhs :: Ct -> CanEqLHS
cc_lhs = CanEqLHS
lhs, cc_rhs :: Ct -> PredType
cc_rhs = PredType
rhs_ty
, cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
| Bool -> Bool
not (CtFlavourRole -> Bool
fr_may_rewrite CtFlavourRole
fs)
= Bool
False
| TyVarLHS TcTyVar
_ <- CanEqLHS
lhs
, CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
new_fr
= Bool
False
| EqRel -> PredType -> Bool
fr_can_rewrite_ty EqRel
eq_rel (CanEqLHS -> PredType
canEqLHSType CanEqLHS
lhs)
= Bool
True
| Bool
kick_out_for_inertness = Bool
True
| Bool
kick_out_for_completeness = Bool
True
| Bool
otherwise = Bool
False
where
fs :: CtFlavourRole
fs = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel)
kick_out_for_inertness :: Bool
kick_out_for_inertness
= (CtFlavourRole
fs CtFlavourRole -> CtFlavourRole -> Bool
`eqCanRewriteFR` CtFlavourRole
fs)
Bool -> Bool -> Bool
&& EqRel -> PredType -> Bool
fr_can_rewrite_ty EqRel
eq_rel PredType
rhs_ty
kick_out_for_completeness :: Bool
kick_out_for_completeness
= case EqRel
eq_rel of
EqRel
NomEq -> PredType
rhs_ty PredType -> PredType -> Bool
`eqType` CanEqLHS -> PredType
canEqLHSType CanEqLHS
new_lhs
EqRel
ReprEq -> CanEqLHS -> PredType -> Bool
is_can_eq_lhs_head CanEqLHS
new_lhs PredType
rhs_ty
kick_out_eq Ct
ct = String -> SDoc -> Bool
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"kick_out_eq" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
is_can_eq_lhs_head :: CanEqLHS -> PredType -> Bool
is_can_eq_lhs_head (TyVarLHS TcTyVar
tv) = PredType -> Bool
go
where
go :: PredType -> Bool
go (Rep.TyVarTy TcTyVar
tv') = TcTyVar
tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv'
go (Rep.AppTy PredType
fun PredType
_) = PredType -> Bool
go PredType
fun
go (Rep.CastTy PredType
ty KindCoercion
_) = PredType -> Bool
go PredType
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
is_can_eq_lhs_head (TyFamLHS TyCon
fun_tc [PredType]
fun_args) = PredType -> Bool
go
where
go :: PredType -> Bool
go (Rep.TyVarTy {}) = Bool
False
go (Rep.AppTy {}) = Bool
False
go (Rep.CastTy PredType
ty KindCoercion
_) = PredType -> Bool
go PredType
ty
go (Rep.TyConApp TyCon
tc [PredType]
args) = TyCon -> [PredType] -> TyCon -> [PredType] -> Bool
tcEqTyConApps TyCon
fun_tc [PredType]
fun_args TyCon
tc [PredType]
args
go (Rep.LitTy {}) = Bool
False
go (Rep.ForAllTy {}) = Bool
False
go (Rep.FunTy {}) = Bool
False
go (Rep.CoercionTy {}) = Bool
False
mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
mentionsOuterVar TcLevel
tclvl CtEvidence
ev
= (TcTyVar -> Bool) -> PredType -> Bool
anyFreeVarsOfType (TcLevel -> TcTyVar -> Bool
isOuterTyVar TcLevel
tclvl) (PredType -> Bool) -> PredType -> Bool
forall a b. (a -> b) -> a -> b
$
CtEvidence -> PredType
ctEvPred CtEvidence
ev
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
<+> 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
matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
matchableGivens CtLoc
loc_w PredType
pred_w inerts :: InertSet
inerts@(IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
inert_cans })
= (Ct -> Bool) -> Cts -> Cts
forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
matchable_given Cts
all_relevant_givens
where
all_relevant_givens :: Cts
all_relevant_givens :: Cts
all_relevant_givens
| Just (Class
clas, [PredType]
_) <- PredType -> Maybe (Class, [PredType])
getClassPredTys_maybe PredType
pred_w
= DictMap Ct -> Class -> Cts
forall a. DictMap a -> Class -> Bag a
findDictsByClass (InertCans -> DictMap Ct
inert_dicts InertCans
inert_cans) Class
clas
Cts -> Cts -> Cts
forall a. Bag a -> Bag a -> Bag a
`unionBags` InertCans -> Cts
inert_irreds InertCans
inert_cans
| Bool
otherwise
= InertCans -> Cts
inert_irreds InertCans
inert_cans
matchable_given :: Ct -> Bool
matchable_given :: Ct -> Bool
matchable_given Ct
ct
| CtGiven { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc_g, ctev_pred :: CtEvidence -> PredType
ctev_pred = PredType
pred_g } <- Ct -> CtEvidence
ctEvidence Ct
ct
= InertSet -> PredType -> CtLoc -> PredType -> CtLoc -> Bool
mightEqualLater InertSet
inerts PredType
pred_g CtLoc
loc_g PredType
pred_w CtLoc
loc_w
| Bool
otherwise
= Bool
False
mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
mightEqualLater :: InertSet -> PredType -> CtLoc -> PredType -> CtLoc -> Bool
mightEqualLater (IS { inert_cycle_breakers :: InertSet -> [(TcTyVar, PredType)]
inert_cycle_breakers = [(TcTyVar, PredType)]
cbvs })
PredType
given_pred CtLoc
given_loc PredType
wanted_pred CtLoc
wanted_loc
| CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
given_loc CtLoc
wanted_loc
= Bool
False
| Bool
otherwise
= case BindFun -> [PredType] -> [PredType] -> UnifyResult
tcUnifyTysFG BindFun
bind_fun [PredType
flattened_given] [PredType
flattened_wanted] of
UnifyResult
SurelyApart -> Bool
False
MaybeApart MaybeApartReason
MARInfinite TCvSubst
_ -> Bool
False
UnifyResult
_ -> Bool
True
where
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [PredType] -> VarSet
tyCoVarsOfTypes [PredType
given_pred, PredType
wanted_pred]
([PredType
flattened_given, PredType
flattened_wanted], TyVarEnv (TyCon, [PredType])
var_mapping)
= InScopeSet
-> [PredType] -> ([PredType], TyVarEnv (TyCon, [PredType]))
flattenTysX InScopeSet
in_scope [PredType
given_pred, PredType
wanted_pred]
bind_fun :: BindFun
bind_fun :: BindFun
bind_fun TcTyVar
tv PredType
rhs_ty
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
, TcTyVar -> MetaInfo -> PredType -> Bool
can_unify TcTyVar
tv (TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv) PredType
rhs_ty
= BindFlag
BindMe
| Just (TyCon
_fam_tc, [PredType]
fam_args) <- TyVarEnv (TyCon, [PredType])
-> TcTyVar -> Maybe (TyCon, [PredType])
forall a. VarEnv a -> TcTyVar -> Maybe a
lookupVarEnv TyVarEnv (TyCon, [PredType])
var_mapping TcTyVar
tv
, (TcTyVar -> Bool) -> [PredType] -> Bool
anyFreeVarsOfTypes TcTyVar -> Bool
mentions_meta_ty_var [PredType]
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
| Just PredType
tyfam_app <- TcTyVar -> [(TcTyVar, PredType)] -> Maybe PredType
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TcTyVar
tv [(TcTyVar, PredType)]
cbvs
-> (TcTyVar -> Bool) -> PredType -> Bool
anyFreeVarsOfType TcTyVar -> Bool
mentions_meta_ty_var PredType
tyfam_app
| Bool
otherwise
-> String -> SDoc -> Bool
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mightEqualLater finds an unbound cbv" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv SDoc -> SDoc -> SDoc
$$ [(TcTyVar, PredType)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(TcTyVar, PredType)]
cbvs)
MetaInfo
_ -> Bool
True
| Bool
otherwise
= Bool
False
can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
can_unify :: TcTyVar -> MetaInfo -> PredType -> Bool
can_unify TcTyVar
_lhs_tv MetaInfo
TyVarTv PredType
rhs_ty
| Just TcTyVar
rhs_tv <- PredType -> Maybe TcTyVar
tcGetTyVar_maybe PredType
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 PredType
_rhs_ty = TcTyVar -> Bool
mentions_meta_ty_var TcTyVar
lhs_tv
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
prohibitedSuperClassSolve CtLoc
from_loc CtLoc
solve_loc
| InstSCOrigin Int
_ TypeSize
given_size <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
from_loc
, ScOrigin TypeSize
wanted_size <- CtLoc -> CtOrigin
ctLocOrigin CtLoc
solve_loc
= TypeSize
given_size TypeSize -> TypeSize -> Bool
forall a. Ord a => a -> a -> Bool
>= TypeSize
wanted_size
| Bool
otherwise
= Bool
False