{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
module GHC.Tc.Types.Constraint (
QCInst(..), isPendingScInst,
Xi, Ct(..), Cts,
emptyCts, andCts, andManyCts, pprCts,
singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
isEmptyCts,
isPendingScDict, superClassesMightHelp, getPendingWantedScs,
isWantedCt, isDerivedCt, isGivenCt,
isUserTypeErrorCt, getUserTypeErrorMsg,
ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
ctEvId, mkTcEqPredLikeEv,
mkNonCanonical, mkNonCanonicalCt, mkGivens,
mkIrredCt,
ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
tyCoVarsOfCt, tyCoVarsOfCts,
tyCoVarsOfCtList, tyCoVarsOfCtsList,
CtIrredReason(..), HoleSet, isInsolubleReason,
CheckTyEqResult, CheckTyEqProblem, cteProblem, cterClearOccursCheck,
cteOK, cteImpredicative, cteTypeFamily, cteHoleBlocker,
cteInsolubleOccurs, cteSolubleOccurs, cterSetOccursCheckSoluble,
cterHasNoProblem, cterHasProblem, cterHasOnlyProblem,
cterRemoveProblem, cterHasOccursCheck, cterFromKind,
CanEqLHS(..), canEqLHS_maybe, canEqLHSKind, canEqLHSType,
eqCanEqLHS,
Hole(..), HoleSort(..), isOutOfScopeHole,
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC,
addInsols, dropMisleading, addSimples, addImplics, addHoles,
tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples,
tyCoVarsOfWCList, insolubleCt, insolubleEqCt,
isDroppableCt, insolubleImplic,
arisesFromGivens,
Implication(..), implicationPrototype, checkTelescopeSkol,
ImplicStatus(..), isInsolubleStatus, isSolvedStatus,
HasGivenEqs(..),
SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
bumpSubGoalDepth, subGoalDepthExceeded,
CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
ctLocTypeOrKind_maybe,
ctLocDepth, bumpCtLocDepth, isGivenLoc,
setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan,
pprCtLoc,
CtEvidence(..), TcEvDest(..),
mkKindLoc, toKindLoc, mkGivenLoc,
isWanted, isGiven, isDerived,
ctEvRole,
wrapType,
CtFlavour(..), ShadowInfo(..), ctFlavourContainsDerived, ctEvFlavour,
CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
eqCanRewrite, eqCanRewriteFR, eqMayRewriteFR,
eqCanDischargeFR,
pprEvVarTheta,
pprEvVars, pprEvVarWithType,
)
where
#include "HsVersions.h"
import GHC.Prelude
import {-# SOURCE #-} GHC.Tc.Types ( TcLclEnv, setLclEnvTcLevel, getLclEnvTcLevel
, setLclEnvLoc, getLclEnvLoc )
import GHC.Core.Predicate
import GHC.Core.Type
import GHC.Core.Coercion
import GHC.Core.Class
import GHC.Core.TyCon
import GHC.Types.Var
import GHC.Tc.Utils.TcType
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Origin
import GHC.Core
import GHC.Core.TyCo.Ppr
import GHC.Types.Name.Occurrence
import GHC.Utils.FV
import GHC.Types.Var.Set
import GHC.Driver.Session
import GHC.Types.Basic
import GHC.Utils.Outputable
import GHC.Types.SrcLoc
import GHC.Data.Bag
import GHC.Utils.Misc
import GHC.Utils.Panic
import Control.Monad ( msum )
import qualified Data.Semigroup ( (<>) )
import Data.Word ( Word8 )
import Data.List ( intersperse )
type Xi = TcType
type Cts = Bag Ct
data Ct
= CDictCan {
Ct -> CtEvidence
cc_ev :: CtEvidence,
Ct -> Class
cc_class :: Class,
Ct -> [Xi]
cc_tyargs :: [Xi],
Ct -> Bool
cc_pend_sc :: Bool
}
| CIrredCan {
cc_ev :: CtEvidence,
Ct -> CtIrredReason
cc_reason :: CtIrredReason
}
| CEqCan {
cc_ev :: CtEvidence,
Ct -> CanEqLHS
cc_lhs :: CanEqLHS,
Ct -> Xi
cc_rhs :: Xi,
Ct -> EqRel
cc_eq_rel :: EqRel
}
| CNonCanonical {
cc_ev :: CtEvidence
}
| CQuantCan QCInst
data CanEqLHS
= TyVarLHS TcTyVar
| TyFamLHS TyCon
[Xi]
instance Outputable CanEqLHS where
ppr :: CanEqLHS -> SDoc
ppr (TyVarLHS EvVar
tv) = forall a. Outputable a => a -> SDoc
ppr EvVar
tv
ppr (TyFamLHS TyCon
fam_tc [Xi]
fam_args) = forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Xi] -> Xi
mkTyConApp TyCon
fam_tc [Xi]
fam_args)
data QCInst
= QCI { QCInst -> CtEvidence
qci_ev :: CtEvidence
, QCInst -> [EvVar]
qci_tvs :: [TcTyVar]
, QCInst -> Xi
qci_pred :: TcPredType
, QCInst -> Bool
qci_pend_sc :: Bool
}
instance Outputable QCInst where
ppr :: QCInst -> SDoc
ppr (QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev }) = forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev
data Hole
= Hole { Hole -> HoleSort
hole_sort :: HoleSort
, Hole -> OccName
hole_occ :: OccName
, Hole -> Xi
hole_ty :: TcType
, Hole -> CtLoc
hole_loc :: CtLoc
}
data HoleSort = ExprHole HoleExprRef
| TypeHole
| ConstraintHole
instance Outputable Hole where
ppr :: Hole -> SDoc
ppr (Hole { hole_sort :: Hole -> HoleSort
hole_sort = ExprHole HoleExprRef
ref
, hole_occ :: Hole -> OccName
hole_occ = OccName
occ
, hole_ty :: Hole -> Xi
hole_ty = Xi
ty })
= SDoc -> SDoc
parens forall a b. (a -> b) -> a -> b
$ (SDoc -> SDoc
braces forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr OccName
occ SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr HoleExprRef
ref) SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Xi
ty
ppr (Hole { hole_sort :: Hole -> HoleSort
hole_sort = HoleSort
_other
, hole_occ :: Hole -> OccName
hole_occ = OccName
occ
, hole_ty :: Hole -> Xi
hole_ty = Xi
ty })
= SDoc -> SDoc
braces forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr OccName
occ SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr Xi
ty
instance Outputable HoleSort where
ppr :: HoleSort -> SDoc
ppr (ExprHole HoleExprRef
ref) = String -> SDoc
text String
"ExprHole:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr HoleExprRef
ref
ppr HoleSort
TypeHole = String -> SDoc
text String
"TypeHole"
ppr HoleSort
ConstraintHole = String -> SDoc
text String
"ConstraintHole"
data CtIrredReason
= IrredShapeReason
| HoleBlockerReason HoleSet
| NonCanonicalReason CheckTyEqResult
| ReprEqReason
| ShapeMismatchReason
| AbstractTyConReason
instance Outputable CtIrredReason where
ppr :: CtIrredReason -> SDoc
ppr CtIrredReason
IrredShapeReason = String -> SDoc
text String
"(irred)"
ppr (HoleBlockerReason HoleSet
holes) = SDoc -> SDoc
parens (String -> SDoc
text String
"blocked on" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr HoleSet
holes)
ppr (NonCanonicalReason CheckTyEqResult
cter) = forall a. Outputable a => a -> SDoc
ppr CheckTyEqResult
cter
ppr CtIrredReason
ReprEqReason = String -> SDoc
text String
"(repr)"
ppr CtIrredReason
ShapeMismatchReason = String -> SDoc
text String
"(shape)"
ppr CtIrredReason
AbstractTyConReason = String -> SDoc
text String
"(abstc)"
isInsolubleReason :: CtIrredReason -> Bool
isInsolubleReason :: CtIrredReason -> Bool
isInsolubleReason CtIrredReason
IrredShapeReason = Bool
False
isInsolubleReason (HoleBlockerReason {}) = Bool
False
isInsolubleReason (NonCanonicalReason CheckTyEqResult
cter) = CheckTyEqResult -> Bool
cterIsInsoluble CheckTyEqResult
cter
isInsolubleReason CtIrredReason
ReprEqReason = Bool
False
isInsolubleReason CtIrredReason
ShapeMismatchReason = Bool
True
isInsolubleReason CtIrredReason
AbstractTyConReason = Bool
True
newtype CheckTyEqResult = CTER Word8
cteOK :: CheckTyEqResult
cteOK :: CheckTyEqResult
cteOK = Word8 -> CheckTyEqResult
CTER forall a. Bits a => a
zeroBits
cterHasNoProblem :: CheckTyEqResult -> Bool
cterHasNoProblem :: CheckTyEqResult -> Bool
cterHasNoProblem (CTER Word8
0) = Bool
True
cterHasNoProblem CheckTyEqResult
_ = Bool
False
newtype CheckTyEqProblem = CTEP Word8
cteImpredicative, cteTypeFamily, cteHoleBlocker, cteInsolubleOccurs,
cteSolubleOccurs :: CheckTyEqProblem
cteImpredicative :: CheckTyEqProblem
cteImpredicative = Word8 -> CheckTyEqProblem
CTEP (forall a. Bits a => Int -> a
bit Int
0)
cteTypeFamily :: CheckTyEqProblem
cteTypeFamily = Word8 -> CheckTyEqProblem
CTEP (forall a. Bits a => Int -> a
bit Int
1)
cteHoleBlocker :: CheckTyEqProblem
cteHoleBlocker = Word8 -> CheckTyEqProblem
CTEP (forall a. Bits a => Int -> a
bit Int
2)
cteInsolubleOccurs :: CheckTyEqProblem
cteInsolubleOccurs = Word8 -> CheckTyEqProblem
CTEP (forall a. Bits a => Int -> a
bit Int
3)
cteSolubleOccurs :: CheckTyEqProblem
cteSolubleOccurs = Word8 -> CheckTyEqProblem
CTEP (forall a. Bits a => Int -> a
bit Int
4)
cteProblem :: CheckTyEqProblem -> CheckTyEqResult
cteProblem :: CheckTyEqProblem -> CheckTyEqResult
cteProblem (CTEP Word8
mask) = Word8 -> CheckTyEqResult
CTER Word8
mask
occurs_mask :: Word8
occurs_mask :: Word8
occurs_mask = Word8
insoluble_mask forall a. Bits a => a -> a -> a
.|. Word8
soluble_mask
where
CTEP Word8
insoluble_mask = CheckTyEqProblem
cteInsolubleOccurs
CTEP Word8
soluble_mask = CheckTyEqProblem
cteSolubleOccurs
cterHasProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
CTER Word8
bits cterHasProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasProblem` CTEP Word8
mask = (Word8
bits forall a. Bits a => a -> a -> a
.&. Word8
mask) forall a. Eq a => a -> a -> Bool
/= Word8
0
cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
CTER Word8
bits cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasOnlyProblem` CTEP Word8
mask = Word8
bits forall a. Eq a => a -> a -> Bool
== Word8
mask
cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
cterRemoveProblem (CTER Word8
bits) (CTEP Word8
mask) = Word8 -> CheckTyEqResult
CTER (Word8
bits forall a. Bits a => a -> a -> a
.&. forall a. Bits a => a -> a
complement Word8
mask)
cterHasOccursCheck :: CheckTyEqResult -> Bool
cterHasOccursCheck :: CheckTyEqResult -> Bool
cterHasOccursCheck (CTER Word8
bits) = (Word8
bits forall a. Bits a => a -> a -> a
.&. Word8
occurs_mask) forall a. Eq a => a -> a -> Bool
/= Word8
0
cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult
cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult
cterClearOccursCheck (CTER Word8
bits) = Word8 -> CheckTyEqResult
CTER (Word8
bits forall a. Bits a => a -> a -> a
.&. forall a. Bits a => a -> a
complement Word8
occurs_mask)
cterSetOccursCheckSoluble :: CheckTyEqResult -> CheckTyEqResult
cterSetOccursCheckSoluble :: CheckTyEqResult -> CheckTyEqResult
cterSetOccursCheckSoluble (CTER Word8
bits)
= Word8 -> CheckTyEqResult
CTER forall a b. (a -> b) -> a -> b
$ ((Word8
bits forall a. Bits a => a -> a -> a
.&. Word8
insoluble_mask) forall a. Bits a => a -> Int -> a
`shift` Int
1) forall a. Bits a => a -> a -> a
.|. (Word8
bits forall a. Bits a => a -> a -> a
.&. forall a. Bits a => a -> a
complement Word8
insoluble_mask)
where
CTEP Word8
insoluble_mask = CheckTyEqProblem
cteInsolubleOccurs
cterFromKind :: CheckTyEqResult -> CheckTyEqResult
cterFromKind :: CheckTyEqResult -> CheckTyEqResult
cterFromKind (CTER Word8
bits)
= Word8 -> CheckTyEqResult
CTER (Word8
bits forall a. Bits a => a -> a -> a
.&. Word8
occurs_mask)
cterIsInsoluble :: CheckTyEqResult -> Bool
cterIsInsoluble :: CheckTyEqResult -> Bool
cterIsInsoluble (CTER Word8
bits) = (Word8
bits forall a. Bits a => a -> a -> a
.&. Word8
mask) forall a. Eq a => a -> a -> Bool
/= Word8
0
where
mask :: Word8
mask = Word8
impredicative_mask forall a. Bits a => a -> a -> a
.|. Word8
insoluble_occurs_mask
CTEP Word8
impredicative_mask = CheckTyEqProblem
cteImpredicative
CTEP Word8
insoluble_occurs_mask = CheckTyEqProblem
cteInsolubleOccurs
instance Semigroup CheckTyEqResult where
CTER Word8
bits1 <> :: CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
<> CTER Word8
bits2 = Word8 -> CheckTyEqResult
CTER (Word8
bits1 forall a. Bits a => a -> a -> a
.|. Word8
bits2)
instance Monoid CheckTyEqResult where
mempty :: CheckTyEqResult
mempty = CheckTyEqResult
cteOK
instance Outputable CheckTyEqResult where
ppr :: CheckTyEqResult -> SDoc
ppr CheckTyEqResult
cter | CheckTyEqResult -> Bool
cterHasNoProblem CheckTyEqResult
cter = String -> SDoc
text String
"cteOK"
| Bool
otherwise
= SDoc -> SDoc
parens forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
fcat forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
intersperse SDoc
vbar forall a b. (a -> b) -> a -> b
$ [SDoc]
set_bits
where
all_bits :: [(CheckTyEqProblem, String)]
all_bits = [ (CheckTyEqProblem
cteImpredicative, String
"cteImpredicative")
, (CheckTyEqProblem
cteTypeFamily, String
"cteTypeFamily")
, (CheckTyEqProblem
cteHoleBlocker, String
"cteHoleBlocker")
, (CheckTyEqProblem
cteInsolubleOccurs, String
"cteInsolubleOccurs")
, (CheckTyEqProblem
cteSolubleOccurs, String
"cteSolubleOccurs") ]
set_bits :: [SDoc]
set_bits = [ String -> SDoc
text String
str
| (CheckTyEqProblem
bitmask, String
str) <- [(CheckTyEqProblem, String)]
all_bits
, CheckTyEqResult
cter CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasProblem` CheckTyEqProblem
bitmask ]
mkNonCanonical :: CtEvidence -> Ct
mkNonCanonical :: CtEvidence -> Ct
mkNonCanonical CtEvidence
ev = CNonCanonical { cc_ev :: CtEvidence
cc_ev = CtEvidence
ev }
mkNonCanonicalCt :: Ct -> Ct
mkNonCanonicalCt :: Ct -> Ct
mkNonCanonicalCt Ct
ct = CNonCanonical { cc_ev :: CtEvidence
cc_ev = Ct -> CtEvidence
cc_ev Ct
ct }
mkIrredCt :: CtIrredReason -> CtEvidence -> Ct
mkIrredCt :: CtIrredReason -> CtEvidence -> Ct
mkIrredCt CtIrredReason
reason CtEvidence
ev = CIrredCan { cc_ev :: CtEvidence
cc_ev = CtEvidence
ev, cc_reason :: CtIrredReason
cc_reason = CtIrredReason
reason }
mkGivens :: CtLoc -> [EvId] -> [Ct]
mkGivens :: CtLoc -> [EvVar] -> [Ct]
mkGivens CtLoc
loc [EvVar]
ev_ids
= forall a b. (a -> b) -> [a] -> [b]
map EvVar -> Ct
mk [EvVar]
ev_ids
where
mk :: EvVar -> Ct
mk EvVar
ev_id = CtEvidence -> Ct
mkNonCanonical (CtGiven { ctev_evar :: EvVar
ctev_evar = EvVar
ev_id
, ctev_pred :: Xi
ctev_pred = EvVar -> Xi
evVarPred EvVar
ev_id
, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc })
ctEvidence :: Ct -> CtEvidence
ctEvidence :: Ct -> CtEvidence
ctEvidence (CQuantCan (QCI { qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev })) = CtEvidence
ev
ctEvidence Ct
ct = Ct -> CtEvidence
cc_ev Ct
ct
ctLoc :: Ct -> CtLoc
ctLoc :: Ct -> CtLoc
ctLoc = CtEvidence -> CtLoc
ctEvLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence
setCtLoc :: Ct -> CtLoc -> Ct
setCtLoc :: Ct -> CtLoc -> Ct
setCtLoc Ct
ct CtLoc
loc = Ct
ct { cc_ev :: CtEvidence
cc_ev = (Ct -> CtEvidence
cc_ev Ct
ct) { ctev_loc :: CtLoc
ctev_loc = CtLoc
loc } }
ctOrigin :: Ct -> CtOrigin
ctOrigin :: Ct -> CtOrigin
ctOrigin = CtLoc -> CtOrigin
ctLocOrigin forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtLoc
ctLoc
ctPred :: Ct -> PredType
ctPred :: Ct -> Xi
ctPred Ct
ct = CtEvidence -> Xi
ctEvPred (Ct -> CtEvidence
ctEvidence Ct
ct)
ctEvId :: Ct -> EvVar
ctEvId :: Ct -> EvVar
ctEvId Ct
ct = CtEvidence -> EvVar
ctEvEvId (Ct -> CtEvidence
ctEvidence Ct
ct)
mkTcEqPredLikeEv :: CtEvidence -> TcType -> TcType -> TcType
mkTcEqPredLikeEv :: CtEvidence -> Xi -> Xi -> Xi
mkTcEqPredLikeEv CtEvidence
ev
= case Xi -> EqRel
predTypeEqRel Xi
pred of
EqRel
NomEq -> Xi -> Xi -> Xi
mkPrimEqPred
EqRel
ReprEq -> Xi -> Xi -> Xi
mkReprPrimEqPred
where
pred :: Xi
pred = CtEvidence -> Xi
ctEvPred CtEvidence
ev
ctFlavour :: Ct -> CtFlavour
ctFlavour :: Ct -> CtFlavour
ctFlavour = CtEvidence -> CtFlavour
ctEvFlavour forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence
ctEqRel :: Ct -> EqRel
ctEqRel :: Ct -> EqRel
ctEqRel = CtEvidence -> EqRel
ctEvEqRel forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence
instance Outputable Ct where
ppr :: Ct -> SDoc
ppr Ct
ct = forall a. Outputable a => a -> SDoc
ppr (Ct -> CtEvidence
ctEvidence Ct
ct) SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens SDoc
pp_sort
where
pp_sort :: SDoc
pp_sort = case Ct
ct of
CEqCan {} -> String -> SDoc
text String
"CEqCan"
CNonCanonical {} -> String -> SDoc
text String
"CNonCanonical"
CDictCan { cc_pend_sc :: Ct -> Bool
cc_pend_sc = Bool
pend_sc }
| Bool
pend_sc -> String -> SDoc
text String
"CDictCan(psc)"
| Bool
otherwise -> String -> SDoc
text String
"CDictCan"
CIrredCan { cc_reason :: Ct -> CtIrredReason
cc_reason = CtIrredReason
reason } -> String -> SDoc
text String
"CIrredCan" SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr CtIrredReason
reason
CQuantCan (QCI { qci_pend_sc :: QCInst -> Bool
qci_pend_sc = Bool
pend_sc })
| Bool
pend_sc -> String -> SDoc
text String
"CQuantCan(psc)"
| Bool
otherwise -> String -> SDoc
text String
"CQuantCan"
canEqLHS_maybe :: Xi -> Maybe CanEqLHS
canEqLHS_maybe :: Xi -> Maybe CanEqLHS
canEqLHS_maybe Xi
xi
| Just EvVar
tv <- Xi -> Maybe EvVar
tcGetTyVar_maybe Xi
xi
= forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ EvVar -> CanEqLHS
TyVarLHS EvVar
tv
| Just (TyCon
tc, [Xi]
args) <- HasCallStack => Xi -> Maybe (TyCon, [Xi])
tcSplitTyConApp_maybe Xi
xi
, TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
, [Xi]
args forall a. [a] -> Int -> Bool
`lengthIs` TyCon -> Int
tyConArity TyCon
tc
= forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ TyCon -> [Xi] -> CanEqLHS
TyFamLHS TyCon
tc [Xi]
args
| Bool
otherwise
= forall a. Maybe a
Nothing
canEqLHSType :: CanEqLHS -> TcType
canEqLHSType :: CanEqLHS -> Xi
canEqLHSType (TyVarLHS EvVar
tv) = EvVar -> Xi
mkTyVarTy EvVar
tv
canEqLHSType (TyFamLHS TyCon
fam_tc [Xi]
fam_args) = TyCon -> [Xi] -> Xi
mkTyConApp TyCon
fam_tc [Xi]
fam_args
canEqLHSKind :: CanEqLHS -> TcKind
canEqLHSKind :: CanEqLHS -> Xi
canEqLHSKind (TyVarLHS EvVar
tv) = EvVar -> Xi
tyVarKind EvVar
tv
canEqLHSKind (TyFamLHS TyCon
fam_tc [Xi]
fam_args) = HasDebugCallStack => Xi -> [Xi] -> Xi
piResultTys (TyCon -> Xi
tyConKind TyCon
fam_tc) [Xi]
fam_args
eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
eqCanEqLHS (TyVarLHS EvVar
tv1) (TyVarLHS EvVar
tv2) = EvVar
tv1 forall a. Eq a => a -> a -> Bool
== EvVar
tv2
eqCanEqLHS (TyFamLHS TyCon
fam_tc1 [Xi]
fam_args1) (TyFamLHS TyCon
fam_tc2 [Xi]
fam_args2)
= TyCon -> [Xi] -> TyCon -> [Xi] -> Bool
tcEqTyConApps TyCon
fam_tc1 [Xi]
fam_args1 TyCon
fam_tc2 [Xi]
fam_args2
eqCanEqLHS CanEqLHS
_ CanEqLHS
_ = Bool
False
tyCoVarsOfCt :: Ct -> TcTyCoVarSet
tyCoVarsOfCt :: Ct -> TcTyCoVarSet
tyCoVarsOfCt = FV -> TcTyCoVarSet
fvVarSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> FV
tyCoFVsOfCt
tyCoVarsOfCtList :: Ct -> [TcTyCoVar]
tyCoVarsOfCtList :: Ct -> [EvVar]
tyCoVarsOfCtList = FV -> [EvVar]
fvVarList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> FV
tyCoFVsOfCt
tyCoFVsOfCt :: Ct -> FV
tyCoFVsOfCt :: Ct -> FV
tyCoFVsOfCt Ct
ct = Xi -> FV
tyCoFVsOfType (Ct -> Xi
ctPred Ct
ct)
tyCoVarsOfCts :: Cts -> TcTyCoVarSet
tyCoVarsOfCts :: Cts -> TcTyCoVarSet
tyCoVarsOfCts = FV -> TcTyCoVarSet
fvVarSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cts -> FV
tyCoFVsOfCts
tyCoVarsOfCtsList :: Cts -> [TcTyCoVar]
tyCoVarsOfCtsList :: Cts -> [EvVar]
tyCoVarsOfCtsList = FV -> [EvVar]
fvVarList forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cts -> FV
tyCoFVsOfCts
tyCoFVsOfCts :: Cts -> FV
tyCoFVsOfCts :: Cts -> FV
tyCoFVsOfCts = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (FV -> FV -> FV
unionFV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> FV
tyCoFVsOfCt) FV
emptyFV
tyCoVarsOfWC :: WantedConstraints -> TyCoVarSet
tyCoVarsOfWC :: WantedConstraints -> TcTyCoVarSet
tyCoVarsOfWC = FV -> TcTyCoVarSet
fvVarSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. WantedConstraints -> FV
tyCoFVsOfWC
tyCoVarsOfWCList :: WantedConstraints -> [TyCoVar]
tyCoVarsOfWCList :: WantedConstraints -> [EvVar]
tyCoVarsOfWCList = FV -> [EvVar]
fvVarList forall b c a. (b -> c) -> (a -> b) -> a -> c
. WantedConstraints -> FV
tyCoFVsOfWC
tyCoFVsOfWC :: WantedConstraints -> FV
tyCoFVsOfWC :: WantedConstraints -> FV
tyCoFVsOfWC (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simple, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implic, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
holes })
= Cts -> FV
tyCoFVsOfCts Cts
simple FV -> FV -> FV
`unionFV`
forall a. (a -> FV) -> Bag a -> FV
tyCoFVsOfBag Implication -> FV
tyCoFVsOfImplic Bag Implication
implic FV -> FV -> FV
`unionFV`
forall a. (a -> FV) -> Bag a -> FV
tyCoFVsOfBag Hole -> FV
tyCoFVsOfHole Bag Hole
holes
tyCoFVsOfImplic :: Implication -> FV
tyCoFVsOfImplic :: Implication -> FV
tyCoFVsOfImplic (Implic { ic_skols :: Implication -> [EvVar]
ic_skols = [EvVar]
skols
, ic_given :: Implication -> [EvVar]
ic_given = [EvVar]
givens
, ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wanted })
| WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted
= FV
emptyFV
| Bool
otherwise
= [EvVar] -> FV -> FV
tyCoFVsVarBndrs [EvVar]
skols forall a b. (a -> b) -> a -> b
$
[EvVar] -> FV -> FV
tyCoFVsVarBndrs [EvVar]
givens forall a b. (a -> b) -> a -> b
$
WantedConstraints -> FV
tyCoFVsOfWC WantedConstraints
wanted
tyCoFVsOfHole :: Hole -> FV
tyCoFVsOfHole :: Hole -> FV
tyCoFVsOfHole (Hole { hole_ty :: Hole -> Xi
hole_ty = Xi
ty }) = Xi -> FV
tyCoFVsOfType Xi
ty
tyCoFVsOfBag :: (a -> FV) -> Bag a -> FV
tyCoFVsOfBag :: forall a. (a -> FV) -> Bag a -> FV
tyCoFVsOfBag a -> FV
tvs_of = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (FV -> FV -> FV
unionFV forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> FV
tvs_of) FV
emptyFV
dropDerivedWC :: WantedConstraints -> WantedConstraints
dropDerivedWC :: WantedConstraints -> WantedConstraints
dropDerivedWC wc :: WantedConstraints
wc@(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples })
= WantedConstraints
wc { wc_simple :: Cts
wc_simple = Cts -> Cts
dropDerivedSimples Cts
simples }
dropDerivedSimples :: Cts -> Cts
dropDerivedSimples :: Cts -> Cts
dropDerivedSimples Cts
simples = forall a b. (a -> Maybe b) -> Bag a -> Bag b
mapMaybeBag Ct -> Maybe Ct
dropDerivedCt Cts
simples
dropDerivedCt :: Ct -> Maybe Ct
dropDerivedCt :: Ct -> Maybe Ct
dropDerivedCt Ct
ct
= case CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev of
Wanted ShadowInfo
WOnly -> forall a. a -> Maybe a
Just (Ct
ct' { cc_ev :: CtEvidence
cc_ev = CtEvidence
ev_wd })
Wanted ShadowInfo
_ -> forall a. a -> Maybe a
Just Ct
ct'
CtFlavour
_ | Ct -> Bool
isDroppableCt Ct
ct -> forall a. Maybe a
Nothing
| Bool
otherwise -> forall a. a -> Maybe a
Just Ct
ct
where
ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
ct
ev_wd :: CtEvidence
ev_wd = CtEvidence
ev { ctev_nosh :: ShadowInfo
ctev_nosh = ShadowInfo
WDeriv }
ct' :: Ct
ct' = Ct -> Ct
setPendingScDict Ct
ct
isDroppableCt :: Ct -> Bool
isDroppableCt :: Ct -> Bool
isDroppableCt Ct
ct
= CtEvidence -> Bool
isDerived CtEvidence
ev Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
keep_deriv
where
ev :: CtEvidence
ev = Ct -> CtEvidence
ctEvidence Ct
ct
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
orig :: CtOrigin
orig = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc
keep_deriv :: Bool
keep_deriv
= case Ct
ct of
CIrredCan { cc_reason :: Ct -> CtIrredReason
cc_reason = CtIrredReason
reason } | CtIrredReason -> Bool
isInsolubleReason CtIrredReason
reason -> Bool -> Bool
keep_eq Bool
True
Ct
_ -> Bool -> Bool
keep_eq Bool
False
keep_eq :: Bool -> Bool
keep_eq Bool
definitely_insoluble
| CtOrigin -> Bool
isGivenOrigin CtOrigin
orig
= Bool
definitely_insoluble
| Bool
otherwise
= case CtOrigin
orig of
FunDepOrigin2 {} -> Bool
True
FunDepOrigin1 Xi
_ CtOrigin
orig1 RealSrcSpan
_ Xi
_ CtOrigin
orig2 RealSrcSpan
_
| Bool
g1 Bool -> Bool -> Bool
|| Bool
g2 -> Bool
True
| Bool
otherwise -> Bool
False
where
g1 :: Bool
g1 = CtOrigin -> Bool
isGivenOrigin CtOrigin
orig1
g2 :: Bool
g2 = CtOrigin -> Bool
isGivenOrigin CtOrigin
orig2
CtOrigin
_ -> Bool
False
arisesFromGivens :: Ct -> Bool
arisesFromGivens :: Ct -> Bool
arisesFromGivens Ct
ct
= case Ct -> CtEvidence
ctEvidence Ct
ct of
CtGiven {} -> Bool
True
CtWanted {} -> Bool
False
CtDerived { ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc } -> CtLoc -> Bool
isGivenLoc CtLoc
loc
isGivenLoc :: CtLoc -> Bool
isGivenLoc :: CtLoc -> Bool
isGivenLoc CtLoc
loc = CtOrigin -> Bool
isGivenOrigin (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc)
isWantedCt :: Ct -> Bool
isWantedCt :: Ct -> Bool
isWantedCt = CtEvidence -> Bool
isWanted forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence
isGivenCt :: Ct -> Bool
isGivenCt :: Ct -> Bool
isGivenCt = CtEvidence -> Bool
isGiven forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence
isDerivedCt :: Ct -> Bool
isDerivedCt :: Ct -> Bool
isDerivedCt = CtEvidence -> Bool
isDerived forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence
getUserTypeErrorMsg :: Ct -> Maybe Type
getUserTypeErrorMsg :: Ct -> Maybe Xi
getUserTypeErrorMsg Ct
ct = Xi -> Maybe Xi
findUserTypeError (Ct -> Xi
ctPred Ct
ct)
where
findUserTypeError :: Xi -> Maybe Xi
findUserTypeError Xi
t = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ( Xi -> Maybe Xi
userTypeError_maybe Xi
t
forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Xi -> Maybe Xi
findUserTypeError (Xi -> [Xi]
subTys Xi
t)
)
subTys :: Xi -> [Xi]
subTys Xi
t = case Xi -> (Xi, [Xi])
splitAppTys Xi
t of
(Xi
t,[]) ->
case HasDebugCallStack => Xi -> Maybe (TyCon, [Xi])
splitTyConApp_maybe Xi
t of
Maybe (TyCon, [Xi])
Nothing -> []
Just (TyCon
_,[Xi]
ts) -> [Xi]
ts
(Xi
t,[Xi]
ts) -> Xi
t forall a. a -> [a] -> [a]
: [Xi]
ts
isUserTypeErrorCt :: Ct -> Bool
isUserTypeErrorCt :: Ct -> Bool
isUserTypeErrorCt Ct
ct = case Ct -> Maybe Xi
getUserTypeErrorMsg Ct
ct of
Just Xi
_ -> Bool
True
Maybe Xi
_ -> Bool
False
isPendingScDict :: Ct -> Maybe Ct
isPendingScDict :: Ct -> Maybe Ct
isPendingScDict ct :: Ct
ct@(CDictCan { cc_pend_sc :: Ct -> Bool
cc_pend_sc = Bool
True })
= forall a. a -> Maybe a
Just (Ct
ct { cc_pend_sc :: Bool
cc_pend_sc = Bool
False })
isPendingScDict Ct
_ = forall a. Maybe a
Nothing
isPendingScInst :: QCInst -> Maybe QCInst
isPendingScInst :: QCInst -> Maybe QCInst
isPendingScInst qci :: QCInst
qci@(QCI { qci_pend_sc :: QCInst -> Bool
qci_pend_sc = Bool
True })
= forall a. a -> Maybe a
Just (QCInst
qci { qci_pend_sc :: Bool
qci_pend_sc = Bool
False })
isPendingScInst QCInst
_ = forall a. Maybe a
Nothing
setPendingScDict :: Ct -> Ct
setPendingScDict :: Ct -> Ct
setPendingScDict ct :: Ct
ct@(CDictCan { cc_pend_sc :: Ct -> Bool
cc_pend_sc = Bool
False })
= Ct
ct { cc_pend_sc :: Bool
cc_pend_sc = Bool
True }
setPendingScDict Ct
ct = Ct
ct
superClassesMightHelp :: WantedConstraints -> Bool
superClassesMightHelp :: WantedConstraints -> Bool
superClassesMightHelp (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics })
= forall a. (a -> Bool) -> Bag a -> Bool
anyBag Ct -> Bool
might_help_ct Cts
simples Bool -> Bool -> Bool
|| forall a. (a -> Bool) -> Bag a -> Bool
anyBag Implication -> Bool
might_help_implic Bag Implication
implics
where
might_help_implic :: Implication -> Bool
might_help_implic Implication
ic
| ImplicStatus
IC_Unsolved <- Implication -> ImplicStatus
ic_status Implication
ic = WantedConstraints -> Bool
superClassesMightHelp (Implication -> WantedConstraints
ic_wanted Implication
ic)
| Bool
otherwise = Bool
False
might_help_ct :: Ct -> Bool
might_help_ct Ct
ct = Ct -> Bool
isWantedCt Ct
ct Bool -> Bool -> Bool
&& Bool -> Bool
not (Ct -> Bool
is_ip Ct
ct)
is_ip :: Ct -> Bool
is_ip (CDictCan { cc_class :: Ct -> Class
cc_class = Class
cls }) = Class -> Bool
isIPClass Class
cls
is_ip Ct
_ = Bool
False
getPendingWantedScs :: Cts -> ([Ct], Cts)
getPendingWantedScs :: Cts -> ([Ct], Cts)
getPendingWantedScs Cts
simples
= forall acc x y.
(acc -> x -> (acc, y)) -> acc -> Bag x -> (acc, Bag y)
mapAccumBagL [Ct] -> Ct -> ([Ct], Ct)
get [] Cts
simples
where
get :: [Ct] -> Ct -> ([Ct], Ct)
get [Ct]
acc Ct
ct | Just Ct
ct' <- Ct -> Maybe Ct
isPendingScDict Ct
ct
= (Ct
ct'forall a. a -> [a] -> [a]
:[Ct]
acc, Ct
ct')
| Bool
otherwise
= ([Ct]
acc, Ct
ct)
singleCt :: Ct -> Cts
singleCt :: Ct -> Cts
singleCt = forall a. a -> Bag a
unitBag
andCts :: Cts -> Cts -> Cts
andCts :: Cts -> Cts -> Cts
andCts = forall a. Bag a -> Bag a -> Bag a
unionBags
listToCts :: [Ct] -> Cts
listToCts :: [Ct] -> Cts
listToCts = forall a. [a] -> Bag a
listToBag
ctsElts :: Cts -> [Ct]
ctsElts :: Cts -> [Ct]
ctsElts = forall a. Bag a -> [a]
bagToList
consCts :: Ct -> Cts -> Cts
consCts :: Ct -> Cts -> Cts
consCts = forall a. a -> Bag a -> Bag a
consBag
snocCts :: Cts -> Ct -> Cts
snocCts :: Cts -> Ct -> Cts
snocCts = forall a. Bag a -> a -> Bag a
snocBag
extendCtsList :: Cts -> [Ct] -> Cts
extendCtsList :: Cts -> [Ct] -> Cts
extendCtsList Cts
cts [Ct]
xs | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ct]
xs = Cts
cts
| Bool
otherwise = Cts
cts forall a. Bag a -> Bag a -> Bag a
`unionBags` forall a. [a] -> Bag a
listToBag [Ct]
xs
andManyCts :: [Cts] -> Cts
andManyCts :: [Cts] -> Cts
andManyCts = forall a. [Bag a] -> Bag a
unionManyBags
emptyCts :: Cts
emptyCts :: Cts
emptyCts = forall a. Bag a
emptyBag
isEmptyCts :: Cts -> Bool
isEmptyCts :: Cts -> Bool
isEmptyCts = forall a. Bag a -> Bool
isEmptyBag
pprCts :: Cts -> SDoc
pprCts :: Cts -> SDoc
pprCts Cts
cts = [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr (forall a. Bag a -> [a]
bagToList Cts
cts))
data WantedConstraints
= WC { WantedConstraints -> Cts
wc_simple :: Cts
, WantedConstraints -> Bag Implication
wc_impl :: Bag Implication
, WantedConstraints -> Bag Hole
wc_holes :: Bag Hole
}
emptyWC :: WantedConstraints
emptyWC :: WantedConstraints
emptyWC = WC { wc_simple :: Cts
wc_simple = forall a. Bag a
emptyBag
, wc_impl :: Bag Implication
wc_impl = forall a. Bag a
emptyBag
, wc_holes :: Bag Hole
wc_holes = forall a. Bag a
emptyBag }
mkSimpleWC :: [CtEvidence] -> WantedConstraints
mkSimpleWC :: [CtEvidence] -> WantedConstraints
mkSimpleWC [CtEvidence]
cts
= WantedConstraints
emptyWC { wc_simple :: Cts
wc_simple = forall a. [a] -> Bag a
listToBag (forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence]
cts) }
mkImplicWC :: Bag Implication -> WantedConstraints
mkImplicWC :: Bag Implication -> WantedConstraints
mkImplicWC Bag Implication
implic
= WantedConstraints
emptyWC { wc_impl :: Bag Implication
wc_impl = Bag Implication
implic }
isEmptyWC :: WantedConstraints -> Bool
isEmptyWC :: WantedConstraints -> Bool
isEmptyWC (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
f, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
i, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
holes })
= forall a. Bag a -> Bool
isEmptyBag Cts
f Bool -> Bool -> Bool
&& forall a. Bag a -> Bool
isEmptyBag Bag Implication
i Bool -> Bool -> Bool
&& forall a. Bag a -> Bool
isEmptyBag Bag Hole
holes
isSolvedWC :: WantedConstraints -> Bool
isSolvedWC :: WantedConstraints -> Bool
isSolvedWC WC {wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
wc_simple, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
wc_impl, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
holes} =
forall a. Bag a -> Bool
isEmptyBag Cts
wc_simple Bool -> Bool -> Bool
&& forall a. (a -> Bool) -> Bag a -> Bool
allBag (ImplicStatus -> Bool
isSolvedStatus forall b c a. (b -> c) -> (a -> b) -> a -> c
. Implication -> ImplicStatus
ic_status) Bag Implication
wc_impl Bool -> Bool -> Bool
&& forall a. Bag a -> Bool
isEmptyBag Bag Hole
holes
andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
andWC (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
f1, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
i1, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
h1 })
(WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
f2, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
i2, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
h2 })
= WC { wc_simple :: Cts
wc_simple = Cts
f1 forall a. Bag a -> Bag a -> Bag a
`unionBags` Cts
f2
, wc_impl :: Bag Implication
wc_impl = Bag Implication
i1 forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Implication
i2
, wc_holes :: Bag Hole
wc_holes = Bag Hole
h1 forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Hole
h2 }
unionsWC :: [WantedConstraints] -> WantedConstraints
unionsWC :: [WantedConstraints] -> WantedConstraints
unionsWC = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr WantedConstraints -> WantedConstraints -> WantedConstraints
andWC WantedConstraints
emptyWC
addSimples :: WantedConstraints -> Bag Ct -> WantedConstraints
addSimples :: WantedConstraints -> Cts -> WantedConstraints
addSimples WantedConstraints
wc Cts
cts
= WantedConstraints
wc { wc_simple :: Cts
wc_simple = WantedConstraints -> Cts
wc_simple WantedConstraints
wc forall a. Bag a -> Bag a -> Bag a
`unionBags` Cts
cts }
addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
addImplics WantedConstraints
wc Bag Implication
implic = WantedConstraints
wc { wc_impl :: Bag Implication
wc_impl = WantedConstraints -> Bag Implication
wc_impl WantedConstraints
wc forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Implication
implic }
addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints
addInsols :: WantedConstraints -> Cts -> WantedConstraints
addInsols WantedConstraints
wc Cts
cts
= WantedConstraints
wc { wc_simple :: Cts
wc_simple = WantedConstraints -> Cts
wc_simple WantedConstraints
wc forall a. Bag a -> Bag a -> Bag a
`unionBags` Cts
cts }
addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints
addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints
addHoles WantedConstraints
wc Bag Hole
holes
= WantedConstraints
wc { wc_holes :: Bag Hole
wc_holes = Bag Hole
holes forall a. Bag a -> Bag a -> Bag a
`unionBags` WantedConstraints -> Bag Hole
wc_holes WantedConstraints
wc }
dropMisleading :: WantedConstraints -> WantedConstraints
dropMisleading :: WantedConstraints -> WantedConstraints
dropMisleading (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
holes })
= WC { wc_simple :: Cts
wc_simple = forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
insolubleCt Cts
simples
, wc_impl :: Bag Implication
wc_impl = forall a b. (a -> b) -> Bag a -> Bag b
mapBag Implication -> Implication
drop_implic Bag Implication
implics
, wc_holes :: Bag Hole
wc_holes = forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Hole -> Bool
isOutOfScopeHole Bag Hole
holes }
where
drop_implic :: Implication -> Implication
drop_implic Implication
implic
= Implication
implic { ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints -> WantedConstraints
drop_wanted (Implication -> WantedConstraints
ic_wanted Implication
implic) }
drop_wanted :: WantedConstraints -> WantedConstraints
drop_wanted (WC { wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
holes })
= WC { wc_simple :: Cts
wc_simple = forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Ct -> Bool
keep_ct Cts
simples
, wc_impl :: Bag Implication
wc_impl = forall a b. (a -> b) -> Bag a -> Bag b
mapBag Implication -> Implication
drop_implic Bag Implication
implics
, wc_holes :: Bag Hole
wc_holes = forall a. (a -> Bool) -> Bag a -> Bag a
filterBag Hole -> Bool
isOutOfScopeHole Bag Hole
holes }
keep_ct :: Ct -> Bool
keep_ct Ct
ct = case Xi -> Pred
classifyPredType (Ct -> Xi
ctPred Ct
ct) of
ClassPred {} -> Bool
False
Pred
_ -> Bool
True
isSolvedStatus :: ImplicStatus -> Bool
isSolvedStatus :: ImplicStatus -> Bool
isSolvedStatus (IC_Solved {}) = Bool
True
isSolvedStatus ImplicStatus
_ = Bool
False
isInsolubleStatus :: ImplicStatus -> Bool
isInsolubleStatus :: ImplicStatus -> Bool
isInsolubleStatus ImplicStatus
IC_Insoluble = Bool
True
isInsolubleStatus ImplicStatus
IC_BadTelescope = Bool
True
isInsolubleStatus ImplicStatus
_ = Bool
False
insolubleImplic :: Implication -> Bool
insolubleImplic :: Implication -> Bool
insolubleImplic Implication
ic = ImplicStatus -> Bool
isInsolubleStatus (Implication -> ImplicStatus
ic_status Implication
ic)
insolubleWC :: WantedConstraints -> Bool
insolubleWC :: WantedConstraints -> Bool
insolubleWC (WC { wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
implics, wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
simples, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
holes })
= forall a. (a -> Bool) -> Bag a -> Bool
anyBag Ct -> Bool
insolubleCt Cts
simples
Bool -> Bool -> Bool
|| forall a. (a -> Bool) -> Bag a -> Bool
anyBag Implication -> Bool
insolubleImplic Bag Implication
implics
Bool -> Bool -> Bool
|| forall a. (a -> Bool) -> Bag a -> Bool
anyBag Hole -> Bool
isOutOfScopeHole Bag Hole
holes
insolubleCt :: Ct -> Bool
insolubleCt :: Ct -> Bool
insolubleCt Ct
ct
| Bool -> Bool
not (Ct -> Bool
insolubleEqCt Ct
ct) = Bool
False
| Ct -> Bool
arisesFromGivens Ct
ct = Bool
False
| Bool
otherwise = Bool
True
insolubleEqCt :: Ct -> Bool
insolubleEqCt :: Ct -> Bool
insolubleEqCt (CIrredCan { cc_reason :: Ct -> CtIrredReason
cc_reason = CtIrredReason
reason }) = CtIrredReason -> Bool
isInsolubleReason CtIrredReason
reason
insolubleEqCt Ct
_ = Bool
False
isOutOfScopeHole :: Hole -> Bool
isOutOfScopeHole :: Hole -> Bool
isOutOfScopeHole (Hole { hole_occ :: Hole -> OccName
hole_occ = OccName
occ }) = Bool -> Bool
not (OccName -> Bool
startsWithUnderscore OccName
occ)
instance Outputable WantedConstraints where
ppr :: WantedConstraints -> SDoc
ppr (WC {wc_simple :: WantedConstraints -> Cts
wc_simple = Cts
s, wc_impl :: WantedConstraints -> Bag Implication
wc_impl = Bag Implication
i, wc_holes :: WantedConstraints -> Bag Hole
wc_holes = Bag Hole
h})
= String -> SDoc
text String
"WC" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces ([SDoc] -> SDoc
vcat
[ forall a. Outputable a => SDoc -> Bag a -> SDoc
ppr_bag (String -> SDoc
text String
"wc_simple") Cts
s
, forall a. Outputable a => SDoc -> Bag a -> SDoc
ppr_bag (String -> SDoc
text String
"wc_impl") Bag Implication
i
, forall a. Outputable a => SDoc -> Bag a -> SDoc
ppr_bag (String -> SDoc
text String
"wc_holes") Bag Hole
h ])
ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc
ppr_bag :: forall a. Outputable a => SDoc -> Bag a -> SDoc
ppr_bag SDoc
doc Bag a
bag
| forall a. Bag a -> Bool
isEmptyBag Bag a
bag = SDoc
empty
| Bool
otherwise = SDoc -> Int -> SDoc -> SDoc
hang (SDoc
doc SDoc -> SDoc -> SDoc
<+> SDoc
equals)
Int
2 (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SDoc -> SDoc -> SDoc
($$) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
ppr) SDoc
empty Bag a
bag)
data Implication
= Implic {
Implication -> TcLevel
ic_tclvl :: TcLevel,
Implication -> [EvVar]
ic_skols :: [TcTyVar],
Implication -> SkolemInfo
ic_info :: SkolemInfo,
Implication -> [EvVar]
ic_given :: [EvVar],
Implication -> HasGivenEqs
ic_given_eqs :: HasGivenEqs,
Implication -> Bool
ic_warn_inaccessible :: Bool,
Implication -> TcLclEnv
ic_env :: TcLclEnv,
Implication -> WantedConstraints
ic_wanted :: WantedConstraints,
Implication -> EvBindsVar
ic_binds :: EvBindsVar,
Implication -> TcTyCoVarSet
ic_need_inner :: VarSet,
Implication -> TcTyCoVarSet
ic_need_outer :: VarSet,
Implication -> ImplicStatus
ic_status :: ImplicStatus
}
implicationPrototype :: Implication
implicationPrototype :: Implication
implicationPrototype
= Implic {
ic_tclvl :: TcLevel
ic_tclvl = forall a. String -> a
panic String
"newImplic:tclvl"
, ic_binds :: EvBindsVar
ic_binds = forall a. String -> a
panic String
"newImplic:binds"
, ic_info :: SkolemInfo
ic_info = forall a. String -> a
panic String
"newImplic:info"
, ic_env :: TcLclEnv
ic_env = forall a. String -> a
panic String
"newImplic:env"
, ic_warn_inaccessible :: Bool
ic_warn_inaccessible = forall a. String -> a
panic String
"newImplic:warn_inaccessible"
, ic_skols :: [EvVar]
ic_skols = []
, ic_given :: [EvVar]
ic_given = []
, ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
emptyWC
, ic_given_eqs :: HasGivenEqs
ic_given_eqs = HasGivenEqs
MaybeGivenEqs
, ic_status :: ImplicStatus
ic_status = ImplicStatus
IC_Unsolved
, ic_need_inner :: TcTyCoVarSet
ic_need_inner = TcTyCoVarSet
emptyVarSet
, ic_need_outer :: TcTyCoVarSet
ic_need_outer = TcTyCoVarSet
emptyVarSet }
data ImplicStatus
= IC_Solved
{ ImplicStatus -> [EvVar]
ics_dead :: [EvVar] }
| IC_Insoluble
| IC_BadTelescope
| IC_Unsolved
data HasGivenEqs
= NoGivenEqs
| LocalGivenEqs
| MaybeGivenEqs
deriving HasGivenEqs -> HasGivenEqs -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HasGivenEqs -> HasGivenEqs -> Bool
$c/= :: HasGivenEqs -> HasGivenEqs -> Bool
== :: HasGivenEqs -> HasGivenEqs -> Bool
$c== :: HasGivenEqs -> HasGivenEqs -> Bool
Eq
instance Outputable Implication where
ppr :: Implication -> SDoc
ppr (Implic { ic_tclvl :: Implication -> TcLevel
ic_tclvl = TcLevel
tclvl, ic_skols :: Implication -> [EvVar]
ic_skols = [EvVar]
skols
, ic_given :: Implication -> [EvVar]
ic_given = [EvVar]
given, ic_given_eqs :: Implication -> HasGivenEqs
ic_given_eqs = HasGivenEqs
given_eqs
, ic_wanted :: Implication -> WantedConstraints
ic_wanted = WantedConstraints
wanted, ic_status :: Implication -> ImplicStatus
ic_status = ImplicStatus
status
, ic_binds :: Implication -> EvBindsVar
ic_binds = EvBindsVar
binds
, ic_need_inner :: Implication -> TcTyCoVarSet
ic_need_inner = TcTyCoVarSet
need_in, ic_need_outer :: Implication -> TcTyCoVarSet
ic_need_outer = TcTyCoVarSet
need_out
, ic_info :: Implication -> SkolemInfo
ic_info = SkolemInfo
info })
= SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Implic" SDoc -> SDoc -> SDoc
<+> SDoc
lbrace)
Int
2 ([SDoc] -> SDoc
sep [ String -> SDoc
text String
"TcLevel =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl
, String -> SDoc
text String
"Skolems =" SDoc -> SDoc -> SDoc
<+> [EvVar] -> SDoc
pprTyVars [EvVar]
skols
, String -> SDoc
text String
"Given-eqs =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr HasGivenEqs
given_eqs
, String -> SDoc
text String
"Status =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr ImplicStatus
status
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Given =") Int
2 ([EvVar] -> SDoc
pprEvVars [EvVar]
given)
, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Wanted =") Int
2 (forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wanted)
, String -> SDoc
text String
"Binds =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr EvBindsVar
binds
, SDoc -> SDoc
whenPprDebug (String -> SDoc
text String
"Needed inner =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr TcTyCoVarSet
need_in)
, SDoc -> SDoc
whenPprDebug (String -> SDoc
text String
"Needed outer =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr TcTyCoVarSet
need_out)
, SkolemInfo -> SDoc
pprSkolInfo SkolemInfo
info ] SDoc -> SDoc -> SDoc
<+> SDoc
rbrace)
instance Outputable ImplicStatus where
ppr :: ImplicStatus -> SDoc
ppr ImplicStatus
IC_Insoluble = String -> SDoc
text String
"Insoluble"
ppr ImplicStatus
IC_BadTelescope = String -> SDoc
text String
"Bad telescope"
ppr ImplicStatus
IC_Unsolved = String -> SDoc
text String
"Unsolved"
ppr (IC_Solved { ics_dead :: ImplicStatus -> [EvVar]
ics_dead = [EvVar]
dead })
= String -> SDoc
text String
"Solved" SDoc -> SDoc -> SDoc
<+> (SDoc -> SDoc
braces (String -> SDoc
text String
"Dead givens =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [EvVar]
dead))
checkTelescopeSkol :: SkolemInfo -> Bool
checkTelescopeSkol :: SkolemInfo -> Bool
checkTelescopeSkol (ForAllSkol {}) = Bool
True
checkTelescopeSkol SkolemInfo
_ = Bool
False
instance Outputable HasGivenEqs where
ppr :: HasGivenEqs -> SDoc
ppr HasGivenEqs
NoGivenEqs = String -> SDoc
text String
"NoGivenEqs"
ppr HasGivenEqs
LocalGivenEqs = String -> SDoc
text String
"LocalGivenEqs"
ppr HasGivenEqs
MaybeGivenEqs = String -> SDoc
text String
"MaybeGivenEqs"
instance Semigroup HasGivenEqs where
HasGivenEqs
NoGivenEqs <> :: HasGivenEqs -> HasGivenEqs -> HasGivenEqs
<> HasGivenEqs
other = HasGivenEqs
other
HasGivenEqs
other <> HasGivenEqs
NoGivenEqs = HasGivenEqs
other
HasGivenEqs
MaybeGivenEqs <> HasGivenEqs
_other = HasGivenEqs
MaybeGivenEqs
HasGivenEqs
_other <> HasGivenEqs
MaybeGivenEqs = HasGivenEqs
MaybeGivenEqs
HasGivenEqs
LocalGivenEqs <> HasGivenEqs
LocalGivenEqs = HasGivenEqs
LocalGivenEqs
instance Monoid HasGivenEqs where
mempty :: HasGivenEqs
mempty = HasGivenEqs
NoGivenEqs
pprEvVars :: [EvVar] -> SDoc
pprEvVars :: [EvVar] -> SDoc
pprEvVars [EvVar]
ev_vars = [SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map EvVar -> SDoc
pprEvVarWithType [EvVar]
ev_vars)
pprEvVarTheta :: [EvVar] -> SDoc
pprEvVarTheta :: [EvVar] -> SDoc
pprEvVarTheta [EvVar]
ev_vars = [Xi] -> SDoc
pprTheta (forall a b. (a -> b) -> [a] -> [b]
map EvVar -> Xi
evVarPred [EvVar]
ev_vars)
pprEvVarWithType :: EvVar -> SDoc
pprEvVarWithType :: EvVar -> SDoc
pprEvVarWithType EvVar
v = forall a. Outputable a => a -> SDoc
ppr EvVar
v SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Xi -> SDoc
pprType (EvVar -> Xi
evVarPred EvVar
v)
wrapType :: Type -> [TyVar] -> [PredType] -> Type
wrapType :: Xi -> [EvVar] -> [Xi] -> Xi
wrapType Xi
ty [EvVar]
skols [Xi]
givens = [EvVar] -> Xi -> Xi
mkSpecForAllTys [EvVar]
skols forall a b. (a -> b) -> a -> b
$ [Xi] -> Xi -> Xi
mkPhiTy [Xi]
givens Xi
ty
data TcEvDest
= EvVarDest EvVar
| HoleDest CoercionHole
data CtEvidence
= CtGiven
{ CtEvidence -> Xi
ctev_pred :: TcPredType
, CtEvidence -> EvVar
ctev_evar :: EvVar
, CtEvidence -> CtLoc
ctev_loc :: CtLoc }
| CtWanted
{ ctev_pred :: TcPredType
, CtEvidence -> TcEvDest
ctev_dest :: TcEvDest
, CtEvidence -> ShadowInfo
ctev_nosh :: ShadowInfo
, ctev_loc :: CtLoc }
| CtDerived
{ ctev_pred :: TcPredType
, ctev_loc :: CtLoc }
ctEvPred :: CtEvidence -> TcPredType
ctEvPred :: CtEvidence -> Xi
ctEvPred = CtEvidence -> Xi
ctev_pred
ctEvLoc :: CtEvidence -> CtLoc
ctEvLoc :: CtEvidence -> CtLoc
ctEvLoc = CtEvidence -> CtLoc
ctev_loc
ctEvOrigin :: CtEvidence -> CtOrigin
ctEvOrigin :: CtEvidence -> CtOrigin
ctEvOrigin = CtLoc -> CtOrigin
ctLocOrigin forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> CtLoc
ctEvLoc
ctEvEqRel :: CtEvidence -> EqRel
ctEvEqRel :: CtEvidence -> EqRel
ctEvEqRel = Xi -> EqRel
predTypeEqRel forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> Xi
ctEvPred
ctEvRole :: CtEvidence -> Role
ctEvRole :: CtEvidence -> Role
ctEvRole = EqRel -> Role
eqRelRole forall b c a. (b -> c) -> (a -> b) -> a -> c
. CtEvidence -> EqRel
ctEvEqRel
ctEvTerm :: CtEvidence -> EvTerm
ctEvTerm :: CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev = EvExpr -> EvTerm
EvExpr (CtEvidence -> EvExpr
ctEvExpr CtEvidence
ev)
ctEvExpr :: CtEvidence -> EvExpr
ctEvExpr :: CtEvidence -> EvExpr
ctEvExpr ev :: CtEvidence
ev@(CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = HoleDest CoercionHole
_ })
= forall b. Coercion -> Expr b
Coercion forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => CtEvidence -> Coercion
ctEvCoercion CtEvidence
ev
ctEvExpr CtEvidence
ev = EvVar -> EvExpr
evId (CtEvidence -> EvVar
ctEvEvId CtEvidence
ev)
ctEvCoercion :: HasDebugCallStack => CtEvidence -> TcCoercion
ctEvCoercion :: HasDebugCallStack => CtEvidence -> Coercion
ctEvCoercion (CtGiven { ctev_evar :: CtEvidence -> EvVar
ctev_evar = EvVar
ev_id })
= EvVar -> Coercion
mkTcCoVarCo EvVar
ev_id
ctEvCoercion (CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest })
| HoleDest CoercionHole
hole <- TcEvDest
dest
=
CoercionHole -> Coercion
mkHoleCo CoercionHole
hole
ctEvCoercion CtEvidence
ev
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"ctEvCoercion" (forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)
ctEvEvId :: CtEvidence -> EvVar
ctEvEvId :: CtEvidence -> EvVar
ctEvEvId (CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = EvVarDest EvVar
ev }) = EvVar
ev
ctEvEvId (CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = HoleDest CoercionHole
h }) = CoercionHole -> EvVar
coHoleCoVar CoercionHole
h
ctEvEvId (CtGiven { ctev_evar :: CtEvidence -> EvVar
ctev_evar = EvVar
ev }) = EvVar
ev
ctEvEvId ctev :: CtEvidence
ctev@(CtDerived {}) = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"ctEvId:" (forall a. Outputable a => a -> SDoc
ppr CtEvidence
ctev)
instance Outputable TcEvDest where
ppr :: TcEvDest -> SDoc
ppr (HoleDest CoercionHole
h) = String -> SDoc
text String
"hole" SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr CoercionHole
h
ppr (EvVarDest EvVar
ev) = forall a. Outputable a => a -> SDoc
ppr EvVar
ev
instance Outputable CtEvidence where
ppr :: CtEvidence -> SDoc
ppr CtEvidence
ev = forall a. Outputable a => a -> SDoc
ppr (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev)
SDoc -> SDoc -> SDoc
<+> SDoc
pp_ev SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces (forall a. Outputable a => a -> SDoc
ppr (CtLoc -> SubGoalDepth
ctl_depth (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev)))
SDoc -> SDoc -> SDoc
<> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (CtEvidence -> Xi
ctEvPred CtEvidence
ev)
where
pp_ev :: SDoc
pp_ev = case CtEvidence
ev of
CtGiven { ctev_evar :: CtEvidence -> EvVar
ctev_evar = EvVar
v } -> forall a. Outputable a => a -> SDoc
ppr EvVar
v
CtWanted {ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
d } -> forall a. Outputable a => a -> SDoc
ppr TcEvDest
d
CtDerived {} -> String -> SDoc
text String
"_"
isWanted :: CtEvidence -> Bool
isWanted :: CtEvidence -> Bool
isWanted (CtWanted {}) = Bool
True
isWanted CtEvidence
_ = Bool
False
isGiven :: CtEvidence -> Bool
isGiven :: CtEvidence -> Bool
isGiven (CtGiven {}) = Bool
True
isGiven CtEvidence
_ = Bool
False
isDerived :: CtEvidence -> Bool
isDerived :: CtEvidence -> Bool
isDerived (CtDerived {}) = Bool
True
isDerived CtEvidence
_ = Bool
False
data CtFlavour
= Given
| Wanted ShadowInfo
| Derived
deriving CtFlavour -> CtFlavour -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CtFlavour -> CtFlavour -> Bool
$c/= :: CtFlavour -> CtFlavour -> Bool
== :: CtFlavour -> CtFlavour -> Bool
$c== :: CtFlavour -> CtFlavour -> Bool
Eq
data ShadowInfo
= WDeriv
| WOnly
deriving( ShadowInfo -> ShadowInfo -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ShadowInfo -> ShadowInfo -> Bool
$c/= :: ShadowInfo -> ShadowInfo -> Bool
== :: ShadowInfo -> ShadowInfo -> Bool
$c== :: ShadowInfo -> ShadowInfo -> Bool
Eq )
instance Outputable CtFlavour where
ppr :: CtFlavour -> SDoc
ppr CtFlavour
Given = String -> SDoc
text String
"[G]"
ppr (Wanted ShadowInfo
WDeriv) = String -> SDoc
text String
"[WD]"
ppr (Wanted ShadowInfo
WOnly) = String -> SDoc
text String
"[W]"
ppr CtFlavour
Derived = String -> SDoc
text String
"[D]"
ctFlavourContainsDerived :: CtFlavour -> Bool
ctFlavourContainsDerived :: CtFlavour -> Bool
ctFlavourContainsDerived (Wanted ShadowInfo
WDeriv) = Bool
True
ctFlavourContainsDerived CtFlavour
Derived = Bool
True
ctFlavourContainsDerived CtFlavour
_ = Bool
False
ctEvFlavour :: CtEvidence -> CtFlavour
ctEvFlavour :: CtEvidence -> CtFlavour
ctEvFlavour (CtWanted { ctev_nosh :: CtEvidence -> ShadowInfo
ctev_nosh = ShadowInfo
nosh }) = ShadowInfo -> CtFlavour
Wanted ShadowInfo
nosh
ctEvFlavour (CtGiven {}) = CtFlavour
Given
ctEvFlavour (CtDerived {}) = CtFlavour
Derived
type CtFlavourRole = (CtFlavour, EqRel)
ctEvFlavourRole :: CtEvidence -> CtFlavourRole
ctEvFlavourRole :: CtEvidence -> CtFlavourRole
ctEvFlavourRole CtEvidence
ev = (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, CtEvidence -> EqRel
ctEvEqRel CtEvidence
ev)
ctFlavourRole :: Ct -> CtFlavourRole
ctFlavourRole :: Ct -> CtFlavourRole
ctFlavourRole (CDictCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev })
= (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
NomEq)
ctFlavourRole (CEqCan { cc_ev :: Ct -> CtEvidence
cc_ev = CtEvidence
ev, cc_eq_rel :: Ct -> EqRel
cc_eq_rel = EqRel
eq_rel })
= (CtEvidence -> CtFlavour
ctEvFlavour CtEvidence
ev, EqRel
eq_rel)
ctFlavourRole Ct
ct
= CtEvidence -> CtFlavourRole
ctEvFlavourRole (Ct -> CtEvidence
ctEvidence Ct
ct)
eqCanRewrite :: EqRel -> EqRel -> Bool
eqCanRewrite :: EqRel -> EqRel -> Bool
eqCanRewrite EqRel
NomEq EqRel
_ = Bool
True
eqCanRewrite EqRel
ReprEq EqRel
ReprEq = Bool
True
eqCanRewrite EqRel
ReprEq EqRel
NomEq = Bool
False
eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
eqCanRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
eqCanRewriteFR (CtFlavour
Given, EqRel
r1) (CtFlavour
_, EqRel
r2) = EqRel -> EqRel -> Bool
eqCanRewrite EqRel
r1 EqRel
r2
eqCanRewriteFR (Wanted ShadowInfo
WDeriv, EqRel
NomEq) (CtFlavour
Derived, EqRel
NomEq) = Bool
True
eqCanRewriteFR (CtFlavour
Derived, EqRel
NomEq) (CtFlavour
Derived, EqRel
NomEq) = Bool
True
eqCanRewriteFR CtFlavourRole
_ CtFlavourRole
_ = Bool
False
eqMayRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
eqMayRewriteFR :: CtFlavourRole -> CtFlavourRole -> Bool
eqMayRewriteFR (Wanted ShadowInfo
WDeriv, EqRel
NomEq) (Wanted ShadowInfo
WDeriv, EqRel
NomEq) = Bool
True
eqMayRewriteFR (CtFlavour
Derived, EqRel
NomEq) (Wanted ShadowInfo
WDeriv, EqRel
NomEq) = Bool
True
eqMayRewriteFR CtFlavourRole
fr1 CtFlavourRole
fr2 = CtFlavourRole -> CtFlavourRole -> Bool
eqCanRewriteFR CtFlavourRole
fr1 CtFlavourRole
fr2
eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
eqCanDischargeFR :: CtFlavourRole -> CtFlavourRole -> Bool
eqCanDischargeFR (CtFlavour
f1,EqRel
r1) (CtFlavour
f2, EqRel
r2) = EqRel -> EqRel -> Bool
eqCanRewrite EqRel
r1 EqRel
r2
Bool -> Bool -> Bool
&& CtFlavour -> CtFlavour -> Bool
eqCanDischargeF CtFlavour
f1 CtFlavour
f2
eqCanDischargeF :: CtFlavour -> CtFlavour -> Bool
eqCanDischargeF :: CtFlavour -> CtFlavour -> Bool
eqCanDischargeF CtFlavour
Given CtFlavour
_ = Bool
True
eqCanDischargeF (Wanted ShadowInfo
_) (Wanted ShadowInfo
_) = Bool
True
eqCanDischargeF (Wanted ShadowInfo
WDeriv) CtFlavour
Derived = Bool
True
eqCanDischargeF CtFlavour
Derived CtFlavour
Derived = Bool
True
eqCanDischargeF CtFlavour
_ CtFlavour
_ = Bool
False
newtype SubGoalDepth = SubGoalDepth Int
deriving (SubGoalDepth -> SubGoalDepth -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SubGoalDepth -> SubGoalDepth -> Bool
$c/= :: SubGoalDepth -> SubGoalDepth -> Bool
== :: SubGoalDepth -> SubGoalDepth -> Bool
$c== :: SubGoalDepth -> SubGoalDepth -> Bool
Eq, Eq SubGoalDepth
SubGoalDepth -> SubGoalDepth -> Bool
SubGoalDepth -> SubGoalDepth -> Ordering
SubGoalDepth -> SubGoalDepth -> SubGoalDepth
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
$cmin :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
max :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
$cmax :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
>= :: SubGoalDepth -> SubGoalDepth -> Bool
$c>= :: SubGoalDepth -> SubGoalDepth -> Bool
> :: SubGoalDepth -> SubGoalDepth -> Bool
$c> :: SubGoalDepth -> SubGoalDepth -> Bool
<= :: SubGoalDepth -> SubGoalDepth -> Bool
$c<= :: SubGoalDepth -> SubGoalDepth -> Bool
< :: SubGoalDepth -> SubGoalDepth -> Bool
$c< :: SubGoalDepth -> SubGoalDepth -> Bool
compare :: SubGoalDepth -> SubGoalDepth -> Ordering
$ccompare :: SubGoalDepth -> SubGoalDepth -> Ordering
Ord, SubGoalDepth -> SDoc
forall a. (a -> SDoc) -> Outputable a
ppr :: SubGoalDepth -> SDoc
$cppr :: SubGoalDepth -> SDoc
Outputable)
initialSubGoalDepth :: SubGoalDepth
initialSubGoalDepth :: SubGoalDepth
initialSubGoalDepth = Int -> SubGoalDepth
SubGoalDepth Int
0
bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
bumpSubGoalDepth (SubGoalDepth Int
n) = Int -> SubGoalDepth
SubGoalDepth (Int
n forall a. Num a => a -> a -> a
+ Int
1)
maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
maxSubGoalDepth :: SubGoalDepth -> SubGoalDepth -> SubGoalDepth
maxSubGoalDepth (SubGoalDepth Int
n) (SubGoalDepth Int
m) = Int -> SubGoalDepth
SubGoalDepth (Int
n forall a. Ord a => a -> a -> a
`max` Int
m)
subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
subGoalDepthExceeded DynFlags
dflags (SubGoalDepth Int
d)
= Int -> IntWithInf
mkIntWithInf Int
d forall a. Ord a => a -> a -> Bool
> DynFlags -> IntWithInf
reductionDepth DynFlags
dflags
data CtLoc = CtLoc { CtLoc -> CtOrigin
ctl_origin :: CtOrigin
, CtLoc -> TcLclEnv
ctl_env :: TcLclEnv
, CtLoc -> Maybe TypeOrKind
ctl_t_or_k :: Maybe TypeOrKind
, CtLoc -> SubGoalDepth
ctl_depth :: !SubGoalDepth }
mkKindLoc :: TcType -> TcType
-> CtLoc -> CtLoc
mkKindLoc :: Xi -> Xi -> CtLoc -> CtLoc
mkKindLoc Xi
s1 Xi
s2 CtLoc
loc = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin (CtLoc -> CtLoc
toKindLoc CtLoc
loc)
(Xi -> Xi -> CtOrigin -> Maybe TypeOrKind -> CtOrigin
KindEqOrigin Xi
s1 Xi
s2 (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc)
(CtLoc -> Maybe TypeOrKind
ctLocTypeOrKind_maybe CtLoc
loc))
toKindLoc :: CtLoc -> CtLoc
toKindLoc :: CtLoc -> CtLoc
toKindLoc CtLoc
loc = CtLoc
loc { ctl_t_or_k :: Maybe TypeOrKind
ctl_t_or_k = forall a. a -> Maybe a
Just TypeOrKind
KindLevel }
mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc
mkGivenLoc :: TcLevel -> SkolemInfo -> TcLclEnv -> CtLoc
mkGivenLoc TcLevel
tclvl SkolemInfo
skol_info TcLclEnv
env
= CtLoc { ctl_origin :: CtOrigin
ctl_origin = SkolemInfo -> CtOrigin
GivenOrigin SkolemInfo
skol_info
, ctl_env :: TcLclEnv
ctl_env = TcLclEnv -> TcLevel -> TcLclEnv
setLclEnvTcLevel TcLclEnv
env TcLevel
tclvl
, ctl_t_or_k :: Maybe TypeOrKind
ctl_t_or_k = forall a. Maybe a
Nothing
, ctl_depth :: SubGoalDepth
ctl_depth = SubGoalDepth
initialSubGoalDepth }
ctLocEnv :: CtLoc -> TcLclEnv
ctLocEnv :: CtLoc -> TcLclEnv
ctLocEnv = CtLoc -> TcLclEnv
ctl_env
ctLocLevel :: CtLoc -> TcLevel
ctLocLevel :: CtLoc -> TcLevel
ctLocLevel CtLoc
loc = TcLclEnv -> TcLevel
getLclEnvTcLevel (CtLoc -> TcLclEnv
ctLocEnv CtLoc
loc)
ctLocDepth :: CtLoc -> SubGoalDepth
ctLocDepth :: CtLoc -> SubGoalDepth
ctLocDepth = CtLoc -> SubGoalDepth
ctl_depth
ctLocOrigin :: CtLoc -> CtOrigin
ctLocOrigin :: CtLoc -> CtOrigin
ctLocOrigin = CtLoc -> CtOrigin
ctl_origin
ctLocSpan :: CtLoc -> RealSrcSpan
ctLocSpan :: CtLoc -> RealSrcSpan
ctLocSpan (CtLoc { ctl_env :: CtLoc -> TcLclEnv
ctl_env = TcLclEnv
lcl}) = TcLclEnv -> RealSrcSpan
getLclEnvLoc TcLclEnv
lcl
ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind
ctLocTypeOrKind_maybe :: CtLoc -> Maybe TypeOrKind
ctLocTypeOrKind_maybe = CtLoc -> Maybe TypeOrKind
ctl_t_or_k
setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc
setCtLocSpan :: CtLoc -> RealSrcSpan -> CtLoc
setCtLocSpan ctl :: CtLoc
ctl@(CtLoc { ctl_env :: CtLoc -> TcLclEnv
ctl_env = TcLclEnv
lcl }) RealSrcSpan
loc = CtLoc -> TcLclEnv -> CtLoc
setCtLocEnv CtLoc
ctl (TcLclEnv -> RealSrcSpan -> TcLclEnv
setLclEnvLoc TcLclEnv
lcl RealSrcSpan
loc)
bumpCtLocDepth :: CtLoc -> CtLoc
bumpCtLocDepth :: CtLoc -> CtLoc
bumpCtLocDepth loc :: CtLoc
loc@(CtLoc { ctl_depth :: CtLoc -> SubGoalDepth
ctl_depth = SubGoalDepth
d }) = CtLoc
loc { ctl_depth :: SubGoalDepth
ctl_depth = SubGoalDepth -> SubGoalDepth
bumpSubGoalDepth SubGoalDepth
d }
setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
ctl CtOrigin
orig = CtLoc
ctl { ctl_origin :: CtOrigin
ctl_origin = CtOrigin
orig }
updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin ctl :: CtLoc
ctl@(CtLoc { ctl_origin :: CtLoc -> CtOrigin
ctl_origin = CtOrigin
orig }) CtOrigin -> CtOrigin
upd
= CtLoc
ctl { ctl_origin :: CtOrigin
ctl_origin = CtOrigin -> CtOrigin
upd CtOrigin
orig }
setCtLocEnv :: CtLoc -> TcLclEnv -> CtLoc
setCtLocEnv :: CtLoc -> TcLclEnv -> CtLoc
setCtLocEnv CtLoc
ctl TcLclEnv
env = CtLoc
ctl { ctl_env :: TcLclEnv
ctl_env = TcLclEnv
env }
pprCtLoc :: CtLoc -> SDoc
pprCtLoc :: CtLoc -> SDoc
pprCtLoc (CtLoc { ctl_origin :: CtLoc -> CtOrigin
ctl_origin = CtOrigin
o, ctl_env :: CtLoc -> TcLclEnv
ctl_env = TcLclEnv
lcl})
= [SDoc] -> SDoc
sep [ CtOrigin -> SDoc
pprCtOrigin CtOrigin
o
, String -> SDoc
text String
"at" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (TcLclEnv -> RealSrcSpan
getLclEnvLoc TcLclEnv
lcl)]