{-# LANGUAGE MultiWayIf #-}
module GHC.Tc.Solver.Dict (
solveDict, solveDictNC,
checkInstanceOK,
matchLocalInst, chooseInstance,
makeSuperClasses, mkStrictSuperClasses,
solveCallStack
) where
import GHC.Prelude
import GHC.Tc.Errors.Types
import GHC.Tc.Instance.FunDeps
import GHC.Tc.Instance.Class( safeOverlap, matchEqualityInst )
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.CtLoc
import GHC.Tc.Types.Origin
import GHC.Tc.Types.EvTerm( evCallStack )
import GHC.Tc.Solver.InertSet
import GHC.Tc.Solver.Monad
import GHC.Tc.Solver.Types
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Unify( uType )
import GHC.Hs.Type( HsIPName(..) )
import GHC.Core
import GHC.Core.Type
import GHC.Core.InstEnv ( DFunInstType, ClsInst(..) )
import GHC.Core.Class
import GHC.Core.Predicate
import GHC.Core.Multiplicity ( scaledThing )
import GHC.Core.Unify ( ruleMatchTyKiX )
import GHC.Types.Name
import GHC.Types.Name.Set
import GHC.Types.Var
import GHC.Types.Id( mkTemplateLocals )
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Utils.Monad ( concatMapM, foldlM )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Misc
import GHC.Unit.Module
import GHC.Data.Bag
import GHC.Driver.DynFlags
import qualified GHC.LanguageExtensions as LangExt
import Data.Maybe ( listToMaybe, mapMaybe, isJust )
import Data.Void( Void )
import Control.Monad.Trans.Maybe( MaybeT, runMaybeT )
import Control.Monad.Trans.Class( lift )
import Control.Monad
solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Void
solveDictNC :: CtEvidence -> Class -> [Type] -> SolverStage Void
solveDictNC CtEvidence
ev Class
cls [Type]
tys
= do { TcS () -> SolverStage ()
forall a. TcS a -> SolverStage a
simpleStage (TcS () -> SolverStage ()) -> TcS () -> SolverStage ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcS ()
traceTcS String
"solveDictNC" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev)
; dict_ct <- CtEvidence -> Class -> [Type] -> SolverStage DictCt
canDictCt CtEvidence
ev Class
cls [Type]
tys
; solveDict dict_ct }
solveDict :: DictCt -> SolverStage Void
solveDict :: DictCt -> SolverStage Void
solveDict dict_ct :: DictCt
dict_ct@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys })
| Class -> Bool
isEqualityClass Class
cls
= CtEvidence -> Class -> [Type] -> SolverStage Void
solveEqualityDict CtEvidence
ev Class
cls [Type]
tys
| Bool
otherwise
= Bool -> SDoc -> SolverStage Void -> SolverStage Void
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (HasDebugCallStack => CtEvidence -> Role
CtEvidence -> Role
ctEvRewriteRole CtEvidence
ev Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal) (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys) (SolverStage Void -> SolverStage Void)
-> SolverStage Void -> SolverStage Void
forall a b. (a -> b) -> a -> b
$
do { TcS () -> SolverStage ()
forall a. TcS a -> SolverStage a
simpleStage (TcS () -> SolverStage ()) -> TcS () -> SolverStage ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcS ()
traceTcS String
"solveDict" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_ct)
; DictCt -> SolverStage ()
tryInertDicts DictCt
dict_ct
; DictCt -> SolverStage ()
tryInstances DictCt
dict_ct
; DictCt -> SolverStage ()
doLocalFunDepImprovement DictCt
dict_ct
; DictCt -> SolverStage ()
doTopFunDepImprovement DictCt
dict_ct
; TcS () -> SolverStage ()
forall a. TcS a -> SolverStage a
simpleStage (DictCt -> TcS ()
updInertDicts DictCt
dict_ct)
; CtEvidence -> String -> SolverStage Void
forall a. CtEvidence -> String -> SolverStage a
stopWithStage (DictCt -> CtEvidence
dictCtEvidence DictCt
dict_ct) String
"Kept inert DictCt" }
updInertDicts :: DictCt -> TcS ()
updInertDicts :: DictCt -> TcS ()
updInertDicts dict_ct :: DictCt
dict_ct@(DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys })
= do { String -> SDoc -> TcS ()
traceTcS String
"Adding inert dict" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_ct SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
; if | CtEvidence -> Bool
isGiven CtEvidence
ev, Just (Type
str_ty, Type
_) <- Class -> [Type] -> Maybe (Type, Type)
isIPPred_maybe Class
cls [Type]
tys
->
(InertSet -> InertSet) -> TcS ()
updInertSet ((InertSet -> InertSet) -> TcS ())
-> (InertSet -> InertSet) -> TcS ()
forall a b. (a -> b) -> a -> b
$ \ inerts :: InertSet
inerts@(IS { inert_cans :: InertSet -> InertCans
inert_cans = InertCans
ics, inert_solved_dicts :: InertSet -> DictMap DictCt
inert_solved_dicts = DictMap DictCt
solved }) ->
InertSet
inerts { inert_cans = updDicts (filterDicts (not_ip_for str_ty)) ics
, inert_solved_dicts = filterDicts (not_ip_for str_ty) solved }
| Bool
otherwise
-> () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
; (InertCans -> InertCans) -> TcS ()
updInertCans ((DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
updDicts (DictCt -> DictMap DictCt -> DictMap DictCt
addDict DictCt
dict_ct)) }
where
not_ip_for :: Type -> DictCt -> Bool
not_ip_for :: Type -> DictCt -> Bool
not_ip_for Type
str_ty (DictCt { di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys })
= Bool -> Bool
not (Type -> Class -> [Type] -> Bool
mentionsIP Type
str_ty Class
cls [Type]
tys)
canDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt
canDictCt :: CtEvidence -> Class -> [Type] -> SolverStage DictCt
canDictCt CtEvidence
ev Class
cls [Type]
tys
| CtEvidence -> Bool
isGiven CtEvidence
ev
= TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue DictCt) -> SolverStage DictCt)
-> TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a b. (a -> b) -> a -> b
$
do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys
; emitWork (listToBag sc_cts)
; continueWith (DictCt { di_ev = ev, di_cls = cls
, di_tys = tys, di_pend_sc = doNotExpand }) }
| CtWanted { ctev_rewriters :: CtEvidence -> RewriterSet
ctev_rewriters = RewriterSet
rewriters } <- CtEvidence
ev
, Just FastString
ip_name <- Class -> [Type] -> Maybe FastString
isCallStackPred Class
cls [Type]
tys
, CtOrigin -> Bool
isPushCallStackOrigin CtOrigin
orig
= TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue DictCt) -> SolverStage DictCt)
-> TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a b. (a -> b) -> a -> b
$
do {
let new_loc :: CtLoc
new_loc = CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
loc (HsIPName -> CtOrigin
IPOccOrigin (FastString -> HsIPName
HsIPName FastString
ip_name))
; new_ev <- CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedEvVarNC CtLoc
new_loc RewriterSet
rewriters Type
pred
; let ev_cs = FastString -> RealSrcSpan -> EvExpr -> EvCallStack
EvCsPushCall (CtOrigin -> FastString
callStackOriginFS CtOrigin
orig)
(CtLoc -> RealSrcSpan
ctLocSpan CtLoc
loc) (HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr CtEvidence
new_ev)
; solveCallStack ev ev_cs
; continueWith (DictCt { di_ev = new_ev, di_cls = cls
, di_tys = tys, di_pend_sc = doNotExpand }) }
| Bool
otherwise
= TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue DictCt) -> SolverStage DictCt)
-> TcS (StopOrContinue DictCt) -> SolverStage DictCt
forall a b. (a -> b) -> a -> b
$
do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; let fuel | Class -> Bool
classHasSCs Class
cls = DynFlags -> ScDepth
wantedsFuel DynFlags
dflags
| Bool
otherwise = ScDepth
doNotExpand
; continueWith (DictCt { di_ev = ev, di_cls = cls
, di_tys = tys, di_pend_sc = fuel }) }
where
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
orig :: CtOrigin
orig = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc
pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
solveCallStack CtEvidence
ev EvCallStack
ev_cs
= do { cs_tm <- EvCallStack -> TcS EvExpr
forall (m :: * -> *).
(MonadThings m, HasModule m, HasDynFlags m) =>
EvCallStack -> m EvExpr
evCallStack EvCallStack
ev_cs
; let ev_tm = EvExpr -> TcCoercion -> EvTerm
mkEvCast EvExpr
cs_tm (Type -> TcCoercion
wrapIP (CtEvidence -> Type
ctEvPred CtEvidence
ev))
; setEvBindIfWanted ev EvCanonical ev_tm }
solveEqualityDict :: CtEvidence -> Class -> [Type] -> SolverStage Void
solveEqualityDict :: CtEvidence -> Class -> [Type] -> SolverStage Void
solveEqualityDict CtEvidence
ev Class
cls [Type]
tys
| CtWanted { ctev_dest :: CtEvidence -> TcEvDest
ctev_dest = TcEvDest
dest } <- CtEvidence
ev
= TcS (StopOrContinue Void) -> SolverStage Void
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue Void) -> SolverStage Void)
-> TcS (StopOrContinue Void) -> SolverStage Void
forall a b. (a -> b) -> a -> b
$
do { let (DataCon
data_con, Role
role, Type
t1, Type
t2) = Class -> [Type] -> (DataCon, Role, Type, Type)
matchEqualityInst Class
cls [Type]
tys
; (co, _, _) <- CtEvidence
-> Role
-> (UnifyEnv -> TcM TcCoercion)
-> TcS (TcCoercion, Cts, [EvVar])
forall a.
CtEvidence -> Role -> (UnifyEnv -> TcM a) -> TcS (a, Cts, [EvVar])
wrapUnifierTcS CtEvidence
ev Role
role ((UnifyEnv -> TcM TcCoercion) -> TcS (TcCoercion, Cts, [EvVar]))
-> (UnifyEnv -> TcM TcCoercion) -> TcS (TcCoercion, Cts, [EvVar])
forall a b. (a -> b) -> a -> b
$ \UnifyEnv
uenv ->
UnifyEnv -> Type -> Type -> TcM TcCoercion
uType UnifyEnv
uenv Type
t1 Type
t2
; setWantedEvTerm dest EvCanonical $
evDataConApp data_con tys [Coercion co]
; stopWith ev "Solved wanted lifted equality" }
| CtGiven { ctev_evar :: CtEvidence -> EvVar
ctev_evar = EvVar
ev_id, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc } <- CtEvidence
ev
, [EvVar
sel_id] <- Class -> [EvVar]
classSCSelIds Class
cls
= TcS (StopOrContinue Void) -> SolverStage Void
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue Void) -> SolverStage Void)
-> TcS (StopOrContinue Void) -> SolverStage Void
forall a b. (a -> b) -> a -> b
$
do { let sc_pred :: Type
sc_pred = EvVar -> [Type] -> Type
classMethodInstTy EvVar
sel_id [Type]
tys
ev_expr :: EvTerm
ev_expr = EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$ EvVar -> EvExpr
forall b. EvVar -> Expr b
Var EvVar
sel_id EvExpr -> [Type] -> EvExpr
forall b. Expr b -> [Type] -> Expr b
`mkTyApps` [Type]
tys EvExpr -> EvExpr -> EvExpr
forall b. Expr b -> Expr b -> Expr b
`App` EvVar -> EvExpr
evId EvVar
ev_id
; given_ev <- CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
loc (Type
sc_pred, EvTerm
ev_expr)
; startAgainWith (mkNonCanonical given_ev) }
| Bool
otherwise
= String -> SDoc -> SolverStage Void
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"solveEqualityDict" (Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls)
tryInertDicts :: DictCt -> SolverStage ()
tryInertDicts :: DictCt -> SolverStage ()
tryInertDicts DictCt
dict_ct
= TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$ do { inerts <- TcS InertCans
getInertCans
; try_inert_dicts inerts dict_ct }
try_inert_dicts :: InertCans -> DictCt -> TcS (StopOrContinue ())
try_inert_dicts :: InertCans -> DictCt -> TcS (StopOrContinue ())
try_inert_dicts InertCans
inerts dict_w :: DictCt
dict_w@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev_w, di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys })
| Just DictCt
dict_i <- InertCans -> CtLoc -> Class -> [Type] -> Maybe DictCt
lookupInertDict InertCans
inerts (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w) Class
cls [Type]
tys
, let ev_i :: CtEvidence
ev_i = DictCt -> CtEvidence
dictCtEvidence DictCt
dict_i
loc_i :: CtLoc
loc_i = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_i
loc_w :: CtLoc
loc_w = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w
=
do {
dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; short_cut_worked <- shortCutSolver dflags ev_w ev_i
; if short_cut_worked
then stopWith ev_w "interactDict/solved from instance"
else if prohibitedSuperClassSolve loc_i loc_w
then continueWith ()
else
do {
; case solveOneFromTheOther (CDictCan dict_i) (CDictCan dict_w) of
InteractResult
KeepInert -> do { String -> SDoc -> TcS ()
traceTcS String
"lookupInertDict:KeepInert" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_w)
; CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev_w CanonicalEvidence
EvCanonical (CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev_i)
; StopOrContinue () -> TcS (StopOrContinue ())
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (StopOrContinue () -> TcS (StopOrContinue ()))
-> StopOrContinue () -> TcS (StopOrContinue ())
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc -> StopOrContinue ()
forall a. CtEvidence -> SDoc -> StopOrContinue a
Stop CtEvidence
ev_w (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Dict equal" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_w) }
InteractResult
KeepWork -> do { String -> SDoc -> TcS ()
traceTcS String
"lookupInertDict:KeepWork" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_w)
; CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev_i CanonicalEvidence
EvCanonical (CtEvidence -> EvTerm
ctEvTerm CtEvidence
ev_w)
; (InertCans -> InertCans) -> TcS ()
updInertCans ((DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
updDicts ((DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans)
-> (DictMap DictCt -> DictMap DictCt) -> InertCans -> InertCans
forall a b. (a -> b) -> a -> b
$ DictCt -> DictMap DictCt -> DictMap DictCt
forall a. DictCt -> DictMap a -> DictMap a
delDict DictCt
dict_w)
; () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith () } } }
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"tryInertDicts:no" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_w SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
; () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith () }
shortCutSolver :: DynFlags
-> CtEvidence
-> CtEvidence
-> TcS Bool
shortCutSolver :: DynFlags -> CtEvidence -> CtEvidence -> TcS Bool
shortCutSolver DynFlags
dflags CtEvidence
ev_w CtEvidence
ev_i
| CtEvidence -> Bool
isWanted CtEvidence
ev_w
, CtEvidence -> Bool
isGiven CtEvidence
ev_i
, Bool -> Bool
not (Type -> Bool
isIPLikePred (CtEvidence -> Type
ctEvPred CtEvidence
ev_w))
, Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.IncoherentInstances DynFlags
dflags)
, GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_SolveConstantDicts DynFlags
dflags
= do { ev_binds_var <- TcS EvBindsVar
getTcEvBindsVar
; ev_binds <- assertPpr (not (isCoEvBindsVar ev_binds_var )) (ppr ev_w) $
getTcEvBindsMap ev_binds_var
; solved_dicts <- getSolvedDicts
; mb_stuff <- runMaybeT $
try_solve_from_instance (ev_binds, solved_dicts) ev_w
; case mb_stuff of
Maybe (EvBindMap, DictMap DictCt)
Nothing -> Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just (EvBindMap
ev_binds', DictMap DictCt
solved_dicts')
-> do { EvBindsVar -> EvBindMap -> TcS ()
setTcEvBindsMap EvBindsVar
ev_binds_var EvBindMap
ev_binds'
; DictMap DictCt -> TcS ()
setSolvedDicts DictMap DictCt
solved_dicts'
; Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True } }
| Bool
otherwise
= Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
where
loc_w :: CtLoc
loc_w = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev_w
try_solve_from_instance
:: (EvBindMap, DictMap DictCt) -> CtEvidence
-> MaybeT TcS (EvBindMap, DictMap DictCt)
try_solve_from_instance :: (EvBindMap, DictMap DictCt)
-> CtEvidence -> MaybeT TcS (EvBindMap, DictMap DictCt)
try_solve_from_instance (EvBindMap
ev_binds, DictMap DictCt
solved_dicts) CtEvidence
ev
| let pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
ev
, ClassPred Class
cls [Type]
tys <- Type -> Pred
classifyPredType Type
pred
= do { inst_res <- TcS ClsInstResult -> MaybeT TcS ClsInstResult
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcS ClsInstResult -> MaybeT TcS ClsInstResult)
-> TcS ClsInstResult -> MaybeT TcS ClsInstResult
forall a b. (a -> b) -> a -> b
$ DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS ClsInstResult
matchGlobalInst DynFlags
dflags Bool
True Class
cls [Type]
tys CtLoc
loc_w
; lift $ warn_custom_warn_instance inst_res loc_w
; case inst_res of
OneInst { cir_new_theta :: ClsInstResult -> [Type]
cir_new_theta = [Type]
preds
, cir_mk_ev :: ClsInstResult -> [EvExpr] -> EvTerm
cir_mk_ev = [EvExpr] -> EvTerm
mk_ev
, cir_canonical :: ClsInstResult -> CanonicalEvidence
cir_canonical = CanonicalEvidence
canonical
, cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what }
| InstanceWhat -> Bool
safeOverlap InstanceWhat
what
, (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isTyFamFree [Type]
preds
-> do { let dict_ct :: DictCt
dict_ct = DictCt { di_ev :: CtEvidence
di_ev = CtEvidence
ev, di_cls :: Class
di_cls = Class
cls
, di_tys :: [Type]
di_tys = [Type]
tys, di_pend_sc :: ScDepth
di_pend_sc = ScDepth
doNotExpand }
solved_dicts' :: DictMap DictCt
solved_dicts' = DictCt -> DictMap DictCt -> DictMap DictCt
addSolvedDict DictCt
dict_ct DictMap DictCt
solved_dicts
; TcS () -> MaybeT TcS ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcS () -> MaybeT TcS ()) -> TcS () -> MaybeT TcS ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcS ()
traceTcS String
"shortCutSolver: found instance" ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
preds)
; loc' <- TcS CtLoc -> MaybeT TcS CtLoc
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcS CtLoc -> MaybeT TcS CtLoc) -> TcS CtLoc -> MaybeT TcS CtLoc
forall a b. (a -> b) -> a -> b
$ CtLoc -> InstanceWhat -> Type -> TcS CtLoc
checkInstanceOK (CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev) InstanceWhat
what Type
pred
; lift $ checkReductionDepth loc' pred
; evc_vs <- mapM (new_wanted_cached ev loc' solved_dicts') preds
; let ev_tm = [EvExpr] -> EvTerm
mk_ev ((MaybeNew -> EvExpr) -> [MaybeNew] -> [EvExpr]
forall a b. (a -> b) -> [a] -> [b]
map MaybeNew -> EvExpr
getEvExpr [MaybeNew]
evc_vs)
ev_binds' = EvBindMap -> EvBind -> EvBindMap
extendEvBinds EvBindMap
ev_binds (EvBind -> EvBindMap) -> EvBind -> EvBindMap
forall a b. (a -> b) -> a -> b
$
EvVar -> CanonicalEvidence -> EvTerm -> EvBind
mkWantedEvBind (CtEvidence -> EvVar
ctEvEvId CtEvidence
ev) CanonicalEvidence
canonical EvTerm
ev_tm
; foldlM try_solve_from_instance (ev_binds', solved_dicts') $
freshGoals evc_vs }
ClsInstResult
_ -> MaybeT TcS (EvBindMap, DictMap DictCt)
forall a. MaybeT TcS a
forall (m :: * -> *) a. MonadPlus m => m a
mzero }
| Bool
otherwise
= MaybeT TcS (EvBindMap, DictMap DictCt)
forall a. MaybeT TcS a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
new_wanted_cached :: CtEvidence -> CtLoc
-> DictMap DictCt -> TcPredType -> MaybeT TcS MaybeNew
new_wanted_cached :: CtEvidence
-> CtLoc -> DictMap DictCt -> Type -> MaybeT TcS MaybeNew
new_wanted_cached CtEvidence
ev_w CtLoc
loc DictMap DictCt
cache Type
pty
| ClassPred Class
cls [Type]
tys <- Type -> Pred
classifyPredType Type
pty
= TcS MaybeNew -> MaybeT TcS MaybeNew
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcS MaybeNew -> MaybeT TcS MaybeNew)
-> TcS MaybeNew -> MaybeT TcS MaybeNew
forall a b. (a -> b) -> a -> b
$ case DictMap DictCt -> CtLoc -> Class -> [Type] -> Maybe DictCt
forall a. DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
findDict DictMap DictCt
cache CtLoc
loc_w Class
cls [Type]
tys of
Just DictCt
dict_ct -> MaybeNew -> TcS MaybeNew
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return (MaybeNew -> TcS MaybeNew) -> MaybeNew -> TcS MaybeNew
forall a b. (a -> b) -> a -> b
$ EvExpr -> MaybeNew
Cached (HasDebugCallStack => CtEvidence -> EvExpr
CtEvidence -> EvExpr
ctEvExpr (DictCt -> CtEvidence
dictCtEvidence DictCt
dict_ct))
Maybe DictCt
Nothing -> CtEvidence -> MaybeNew
Fresh (CtEvidence -> MaybeNew) -> TcS CtEvidence -> TcS MaybeNew
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedNC CtLoc
loc (CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev_w) Type
pty
| Bool
otherwise = MaybeT TcS MaybeNew
forall a. MaybeT TcS a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
tryInstances :: DictCt -> SolverStage ()
tryInstances :: DictCt -> SolverStage ()
tryInstances DictCt
dict_ct
= TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$ do { inerts <- TcS InertSet
getInertSet
; try_instances inerts dict_ct }
try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ())
try_instances :: InertSet -> DictCt -> TcS (StopOrContinue ())
try_instances InertSet
inerts work_item :: DictCt
work_item@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_cls :: DictCt -> Class
di_cls = Class
cls
, di_tys :: DictCt -> [Type]
di_tys = [Type]
xis })
| CtEvidence -> Bool
isGiven CtEvidence
ev
= () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith ()
| Just CtEvidence
solved_ev <- InertSet -> CtLoc -> Class -> [Type] -> Maybe CtEvidence
lookupSolvedDict InertSet
inerts CtLoc
dict_loc Class
cls [Type]
xis
= do { CtEvidence -> CanonicalEvidence -> EvTerm -> TcS ()
setEvBindIfWanted CtEvidence
ev CanonicalEvidence
EvCanonical (CtEvidence -> EvTerm
ctEvTerm CtEvidence
solved_ev)
; CtEvidence -> String -> TcS (StopOrContinue ())
forall a. CtEvidence -> String -> TcS (StopOrContinue a)
stopWith CtEvidence
ev String
"Dict/Top (cached)" }
| Bool
otherwise
= do { dflags <- TcS DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
; case lkup_res of
OneInst { cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what }
-> do { InstanceWhat -> DictCt -> TcS ()
insertSafeOverlapFailureTcS InstanceWhat
what DictCt
work_item
; InstanceWhat -> DictCt -> TcS ()
updSolvedDicts InstanceWhat
what DictCt
work_item
; CtEvidence -> ClsInstResult -> TcS (StopOrContinue ())
forall a. CtEvidence -> ClsInstResult -> TcS (StopOrContinue a)
chooseInstance CtEvidence
ev ClsInstResult
lkup_res }
ClsInstResult
_ ->
() -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith () }
where
dict_loc :: CtLoc
dict_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
chooseInstance :: CtEvidence -> ClsInstResult -> TcS (StopOrContinue a)
chooseInstance :: forall a. CtEvidence -> ClsInstResult -> TcS (StopOrContinue a)
chooseInstance CtEvidence
work_item
(OneInst { cir_new_theta :: ClsInstResult -> [Type]
cir_new_theta = [Type]
theta
, cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what
, cir_mk_ev :: ClsInstResult -> [EvExpr] -> EvTerm
cir_mk_ev = [EvExpr] -> EvTerm
mk_ev
, cir_canonical :: ClsInstResult -> CanonicalEvidence
cir_canonical = CanonicalEvidence
canonical })
= do { String -> SDoc -> TcS ()
traceTcS String
"doTopReact/found instance for" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
work_item
; deeper_loc <- CtLoc -> InstanceWhat -> Type -> TcS CtLoc
checkInstanceOK CtLoc
loc InstanceWhat
what Type
pred
; checkReductionDepth deeper_loc pred
; assertPprM (getTcEvBindsVar >>= return . not . isCoEvBindsVar)
(ppr work_item)
; evc_vars <- mapM (newWanted deeper_loc (ctEvRewriters work_item)) theta
; setEvBindIfWanted work_item canonical (mk_ev (map getEvExpr evc_vars))
; emitWorkNC (freshGoals evc_vars)
; stopWith work_item "Dict/Top (solved wanted)" }
where
pred :: Type
pred = CtEvidence -> Type
ctEvPred CtEvidence
work_item
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
work_item
chooseInstance CtEvidence
work_item ClsInstResult
lookup_res
= String -> SDoc -> TcS (StopOrContinue a)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"chooseInstance" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
work_item SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ ClsInstResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInstResult
lookup_res)
checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
checkInstanceOK :: CtLoc -> InstanceWhat -> Type -> TcS CtLoc
checkInstanceOK CtLoc
loc InstanceWhat
what Type
pred
= do { CtLoc -> InstanceWhat -> Type -> TcS ()
checkWellStagedDFun CtLoc
loc InstanceWhat
what Type
pred
; CtLoc -> TcS CtLoc
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return CtLoc
deeper_loc }
where
deeper_loc :: CtLoc
deeper_loc = CtLoc -> CtLoc
zap_origin (CtLoc -> CtLoc
bumpCtLocDepth CtLoc
loc)
origin :: CtOrigin
origin = CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc
zap_origin :: CtLoc -> CtLoc
zap_origin CtLoc
loc
| ScOrigin ClsInstOrQC
what NakedScFlag
_ <- CtOrigin
origin
= CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin CtLoc
loc (ClsInstOrQC -> NakedScFlag -> CtOrigin
ScOrigin ClsInstOrQC
what NakedScFlag
NotNakedSc)
| Bool
otherwise
= CtLoc
loc
matchClassInst :: DynFlags -> InertSet
-> Class -> [Type]
-> CtLoc -> TcS ClsInstResult
matchClassInst :: DynFlags
-> InertSet -> Class -> [Type] -> CtLoc -> TcS ClsInstResult
matchClassInst DynFlags
dflags InertSet
inerts Class
clas [Type]
tys CtLoc
loc
| Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.IncoherentInstances DynFlags
dflags)
, Bool -> Bool
not (Class -> Bool
isCTupleClass Class
clas)
, Bool -> Bool
not (InertSet -> CtLoc -> Class -> [Type] -> Bool
noMatchableGivenDicts InertSet
inerts CtLoc
loc Class
clas [Type]
tys)
= do { String -> SDoc -> TcS ()
traceTcS String
"Delaying instance application" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Work item:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Class -> [Type] -> SDoc
pprClassPred Class
clas [Type]
tys ]
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NotSure }
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"matchClassInst" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"pred =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'{'
; local_res <- Type -> CtLoc -> TcS ClsInstResult
matchLocalInst Type
pred CtLoc
loc
; case local_res of
OneInst {} ->
do { String -> SDoc -> TcS ()
traceTcS String
"} matchClassInst local match" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ ClsInstResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInstResult
local_res
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
local_res }
ClsInstResult
NotSure ->
do { String -> SDoc -> TcS ()
traceTcS String
"} matchClassInst local not sure" SDoc
forall doc. IsOutput doc => doc
empty
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
local_res }
ClsInstResult
NoInstance
-> do { global_res <- DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS ClsInstResult
matchGlobalInst DynFlags
dflags Bool
False Class
clas [Type]
tys CtLoc
loc
; warn_custom_warn_instance global_res loc
; traceTcS "} matchClassInst global result" $ ppr global_res
; return global_res } }
where
pred :: Type
pred = Class -> [Type] -> Type
mkClassPred Class
clas [Type]
tys
warn_custom_warn_instance :: ClsInstResult -> CtLoc -> TcS ()
warn_custom_warn_instance :: ClsInstResult -> CtLoc -> TcS ()
warn_custom_warn_instance (OneInst{ cir_what :: ClsInstResult -> InstanceWhat
cir_what = InstanceWhat
what }) CtLoc
ct_loc
| TopLevInstance{ iw_dfun_id :: InstanceWhat -> EvVar
iw_dfun_id = EvVar
dfun, iw_warn :: InstanceWhat -> Maybe (WarningTxt GhcRn)
iw_warn = Just WarningTxt GhcRn
warn } <- InstanceWhat
what = do
let mod :: Module
mod = HasDebugCallStack => Name -> Module
Name -> Module
nameModule (Name -> Module) -> Name -> Module
forall a b. (a -> b) -> a -> b
$ EvVar -> Name
forall a. NamedThing a => a -> Name
getName EvVar
dfun
this_mod <- TcS Module
forall (m :: * -> *). HasModule m => m Module
getModule
when (this_mod /= mod)
$ ctLocWarnTcS ct_loc
$ TcRnPragmaWarning
{ pragma_warning_info = PragmaWarningInstance dfun (ctl_origin ct_loc)
, pragma_warning_msg = warn }
warn_custom_warn_instance ClsInstResult
_ CtLoc
_ = () -> TcS ()
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
matchLocalInst :: Type -> CtLoc -> TcS ClsInstResult
matchLocalInst Type
pred CtLoc
loc
= do { inerts@(IS { inert_cans = ics }) <- TcS InertSet
getInertSet
; case match_local_inst inerts (inert_insts ics) of
{ ([], []) -> do { String -> SDoc -> TcS ()
traceTcS String
"No local instance for" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NoInstance }
; ([(CtEvidence, [DFunInstType])]
matches, [(CtEvidence, [DFunInstType])]
unifs) ->
do { matches <- ((CtEvidence, [DFunInstType]) -> TcS InstDFun)
-> [(CtEvidence, [DFunInstType])] -> TcS [InstDFun]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (CtEvidence, [DFunInstType]) -> TcS InstDFun
mk_instDFun [(CtEvidence, [DFunInstType])]
matches
; unifs <- mapM mk_instDFun unifs
; case dominatingMatch matches of
{ Just (EvVar
dfun_id, [Type]
tys, [Type]
theta)
| (InstDFun -> Bool) -> [InstDFun] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (([Type]
theta [Type] -> [Type] -> Bool
`impliedBySCs`) ([Type] -> Bool) -> (InstDFun -> [Type]) -> InstDFun -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InstDFun -> [Type]
forall a b c. (a, b, c) -> c
thdOf3) [InstDFun]
unifs
->
do { let result :: ClsInstResult
result = OneInst { cir_new_theta :: [Type]
cir_new_theta = [Type]
theta
, cir_mk_ev :: [EvExpr] -> EvTerm
cir_mk_ev = EvVar -> [Type] -> [EvExpr] -> EvTerm
evDFunApp EvVar
dfun_id [Type]
tys
, cir_canonical :: CanonicalEvidence
cir_canonical = CanonicalEvidence
EvCanonical
, cir_what :: InstanceWhat
cir_what = InstanceWhat
LocalInstance }
; String -> SDoc -> TcS ()
traceTcS String
"Best local instance found:" (SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"pred:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"result:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ClsInstResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr ClsInstResult
result
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"matches:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
matches
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"unifs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
unifs ]
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
result }
; Maybe InstDFun
mb_best ->
do { String -> SDoc -> TcS ()
traceTcS String
"Multiple local instances; not committing to any"
(SDoc -> TcS ()) -> SDoc -> TcS ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"pred:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"matches:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
matches
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"unifs:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [InstDFun] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [InstDFun]
unifs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"best_match:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Maybe InstDFun -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe InstDFun
mb_best ]
; ClsInstResult -> TcS ClsInstResult
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return ClsInstResult
NotSure }}}}}
where
pred_tv_set :: TyCoVarSet
pred_tv_set = Type -> TyCoVarSet
tyCoVarsOfType Type
pred
mk_instDFun :: (CtEvidence, [DFunInstType]) -> TcS InstDFun
mk_instDFun :: (CtEvidence, [DFunInstType]) -> TcS InstDFun
mk_instDFun (CtEvidence
ev, [DFunInstType]
tys) =
let dfun_id :: EvVar
dfun_id = CtEvidence -> EvVar
ctEvEvId CtEvidence
ev
in do { (tys, theta) <- EvVar -> [DFunInstType] -> TcS ([Type], [Type])
instDFunType (CtEvidence -> EvVar
ctEvEvId CtEvidence
ev) [DFunInstType]
tys
; return (dfun_id, tys, theta) }
match_local_inst :: InertSet
-> [QCInst]
-> ( [(CtEvidence, [DFunInstType])]
, [(CtEvidence, [DFunInstType])] )
match_local_inst :: InertSet
-> [QCInst]
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
match_local_inst InertSet
_inerts []
= ([], [])
match_local_inst InertSet
inerts (qci :: QCInst
qci@(QCI { qci_tvs :: QCInst -> [EvVar]
qci_tvs = [EvVar]
qtvs
, qci_pred :: QCInst -> Type
qci_pred = Type
qpred
, qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
qev })
:[QCInst]
qcis)
| let in_scope :: InScopeSet
in_scope = TyCoVarSet -> InScopeSet
mkInScopeSet (TyCoVarSet
qtv_set TyCoVarSet -> TyCoVarSet -> TyCoVarSet
`unionVarSet` TyCoVarSet
pred_tv_set)
, Just TvSubstEnv
tv_subst <- TyCoVarSet
-> RnEnv2 -> TvSubstEnv -> Type -> Type -> Maybe TvSubstEnv
ruleMatchTyKiX TyCoVarSet
qtv_set (InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
in_scope)
TvSubstEnv
emptyTvSubstEnv Type
qpred Type
pred
, let match :: (CtEvidence, [DFunInstType])
match = (CtEvidence
qev, (EvVar -> DFunInstType) -> [EvVar] -> [DFunInstType]
forall a b. (a -> b) -> [a] -> [b]
map (TvSubstEnv -> EvVar -> DFunInstType
forall a. VarEnv a -> EvVar -> Maybe a
lookupVarEnv TvSubstEnv
tv_subst) [EvVar]
qtvs)
= ((CtEvidence, [DFunInstType])
match(CtEvidence, [DFunInstType])
-> [(CtEvidence, [DFunInstType])] -> [(CtEvidence, [DFunInstType])]
forall a. a -> [a] -> [a]
:[(CtEvidence, [DFunInstType])]
matches, [(CtEvidence, [DFunInstType])]
unifs)
| Bool
otherwise
= Bool
-> SDoc
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCoVarSet -> TyCoVarSet -> Bool
disjointVarSet TyCoVarSet
qtv_set (Type -> TyCoVarSet
tyCoVarsOfType Type
pred))
(QCInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr QCInst
qci SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred)
([(CtEvidence, [DFunInstType])]
matches, Maybe (CtEvidence, [DFunInstType])
this_unif Maybe (CtEvidence, [DFunInstType])
-> [(CtEvidence, [DFunInstType])] -> [(CtEvidence, [DFunInstType])]
forall {a}. Maybe a -> [a] -> [a]
`combine` [(CtEvidence, [DFunInstType])]
unifs)
where
qloc :: CtLoc
qloc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
qev
qtv_set :: TyCoVarSet
qtv_set = [EvVar] -> TyCoVarSet
mkVarSet [EvVar]
qtvs
([(CtEvidence, [DFunInstType])]
matches, [(CtEvidence, [DFunInstType])]
unifs) = InertSet
-> [QCInst]
-> ([(CtEvidence, [DFunInstType])], [(CtEvidence, [DFunInstType])])
match_local_inst InertSet
inerts [QCInst]
qcis
this_unif :: Maybe (CtEvidence, [DFunInstType])
this_unif
| Just Subst
subst <- InertSet -> Type -> CtLoc -> Type -> CtLoc -> Maybe Subst
mightEqualLater InertSet
inerts Type
qpred CtLoc
qloc Type
pred CtLoc
loc
= (CtEvidence, [DFunInstType]) -> Maybe (CtEvidence, [DFunInstType])
forall a. a -> Maybe a
Just (CtEvidence
qev, (EvVar -> DFunInstType) -> [EvVar] -> [DFunInstType]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> EvVar -> DFunInstType
lookupTyVar Subst
subst) [EvVar]
qtvs)
| Bool
otherwise
= Maybe (CtEvidence, [DFunInstType])
forall a. Maybe a
Nothing
combine :: Maybe a -> [a] -> [a]
combine Maybe a
Nothing [a]
us = [a]
us
combine (Just a
u) [a]
us = a
u a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
us
type InstDFun = (DFunId, [TcType], TcThetaType)
dominatingMatch :: [InstDFun] -> Maybe InstDFun
dominatingMatch :: [InstDFun] -> Maybe InstDFun
dominatingMatch [InstDFun]
matches =
[InstDFun] -> Maybe InstDFun
forall a. [a] -> Maybe a
listToMaybe ([InstDFun] -> Maybe InstDFun) -> [InstDFun] -> Maybe InstDFun
forall a b. (a -> b) -> a -> b
$ ((InstDFun, [InstDFun]) -> Maybe InstDFun)
-> [(InstDFun, [InstDFun])] -> [InstDFun]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((InstDFun -> [InstDFun] -> Maybe InstDFun)
-> (InstDFun, [InstDFun]) -> Maybe InstDFun
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry InstDFun -> [InstDFun] -> Maybe InstDFun
go) ([InstDFun] -> [(InstDFun, [InstDFun])]
forall a. [a] -> [(a, [a])]
holes [InstDFun]
matches)
where
go :: InstDFun -> [InstDFun] -> Maybe InstDFun
go :: InstDFun -> [InstDFun] -> Maybe InstDFun
go InstDFun
this [] = InstDFun -> Maybe InstDFun
forall a. a -> Maybe a
Just InstDFun
this
go this :: InstDFun
this@(EvVar
_,[Type]
_,[Type]
this_theta) ((EvVar
_,[Type]
_,[Type]
other_theta):[InstDFun]
others)
| [Type]
this_theta [Type] -> [Type] -> Bool
`impliedBySCs` [Type]
other_theta
= InstDFun -> [InstDFun] -> Maybe InstDFun
go InstDFun
this [InstDFun]
others
| Bool
otherwise
= Maybe InstDFun
forall a. Maybe a
Nothing
impliedBySCs :: TcThetaType -> TcThetaType -> Bool
impliedBySCs :: [Type] -> [Type] -> Bool
impliedBySCs [Type]
c1 [Type]
c2 = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
in_c2 [Type]
c1
where
in_c2 :: TcPredType -> Bool
in_c2 :: Type -> Bool
in_c2 Type
pred = (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Type
pred HasDebugCallStack => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType`) [Type]
c2_expanded
c2_expanded :: [TcPredType]
c2_expanded :: [Type]
c2_expanded = [ Type
q | Type
p <- [Type]
c2, Type
q <- Type
p Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: Type -> [Type]
transSuperClasses Type
p ]
doLocalFunDepImprovement :: DictCt -> SolverStage ()
doLocalFunDepImprovement :: DictCt -> SolverStage ()
doLocalFunDepImprovement dict_ct :: DictCt
dict_ct@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
work_ev, di_cls :: DictCt -> Class
di_cls = Class
cls })
= TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$
do { inerts <- TcS InertCans
getInertCans
; imp <- foldlM add_fds False (findDictsByClass (inert_dicts inerts) cls)
; if imp then startAgainWith (CDictCan dict_ct)
else continueWith () }
where
work_pred :: Type
work_pred = CtEvidence -> Type
ctEvPred CtEvidence
work_ev
work_loc :: CtLoc
work_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
work_ev
add_fds :: Bool -> DictCt -> TcS Bool
add_fds :: Bool -> DictCt -> TcS Bool
add_fds Bool
so_far (DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
inert_ev })
| CtEvidence -> Bool
isGiven CtEvidence
work_ev Bool -> Bool -> Bool
&& CtEvidence -> Bool
isGiven CtEvidence
inert_ev
= Bool -> TcS Bool
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
so_far
| Bool
otherwise
= do { String -> SDoc -> TcS ()
traceTcS String
"doLocalFunDepImprovement" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat
[ CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
work_ev
, CtLoc -> SDoc
pprCtLoc CtLoc
work_loc, Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> Bool
isGivenLoc CtLoc
work_loc)
, CtLoc -> SDoc
pprCtLoc CtLoc
inert_loc, Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> Bool
isGivenLoc CtLoc
inert_loc)
, CtLoc -> SDoc
pprCtLoc CtLoc
derived_loc, Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> Bool
isGivenLoc CtLoc
derived_loc) ])
; unifs <- CtEvidence -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool
emitFunDepWanteds CtEvidence
work_ev ([FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool)
-> [FunDepEqn (CtLoc, RewriterSet)] -> TcS Bool
forall a b. (a -> b) -> a -> b
$
(CtLoc, RewriterSet)
-> Type -> Type -> [FunDepEqn (CtLoc, RewriterSet)]
forall loc. loc -> Type -> Type -> [FunDepEqn loc]
improveFromAnother (CtLoc
derived_loc, RewriterSet
inert_rewriters)
Type
inert_pred Type
work_pred
; return (so_far || unifs)
}
where
inert_pred :: Type
inert_pred = CtEvidence -> Type
ctEvPred CtEvidence
inert_ev
inert_loc :: CtLoc
inert_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
inert_ev
inert_rewriters :: RewriterSet
inert_rewriters = CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
inert_ev
derived_loc :: CtLoc
derived_loc = CtLoc
work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth`
ctl_depth inert_loc
, ctl_origin = FunDepOrigin1 work_pred
(ctLocOrigin work_loc)
(ctLocSpan work_loc)
inert_pred
(ctLocOrigin inert_loc)
(ctLocSpan inert_loc) }
doTopFunDepImprovement :: DictCt -> SolverStage ()
doTopFunDepImprovement :: DictCt -> SolverStage ()
doTopFunDepImprovement dict_ct :: DictCt
dict_ct@(DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
xis })
| CtEvidence -> Bool
isGiven CtEvidence
ev
= TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$ () -> TcS (StopOrContinue ())
forall a. a -> TcS (StopOrContinue a)
continueWith ()
| Bool
otherwise
= TcS (StopOrContinue ()) -> SolverStage ()
forall a. TcS (StopOrContinue a) -> SolverStage a
Stage (TcS (StopOrContinue ()) -> SolverStage ())
-> TcS (StopOrContinue ()) -> SolverStage ()
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcS ()
traceTcS String
"try_fundeps" (DictCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr DictCt
dict_ct)
; instEnvs <- TcS InstEnvs
getInstEnvs
; let fundep_eqns = InstEnvs
-> (ClsInst -> (CtLoc, RewriterSet))
-> Class
-> [Type]
-> [FunDepEqn (CtLoc, RewriterSet)]
forall loc.
InstEnvs -> (ClsInst -> loc) -> Class -> [Type] -> [FunDepEqn loc]
improveFromInstEnv InstEnvs
instEnvs ClsInst -> (CtLoc, RewriterSet)
mk_ct_loc Class
cls [Type]
xis
; imp <- emitFunDepWanteds ev fundep_eqns
; if imp then startAgainWith (CDictCan dict_ct)
else continueWith () }
where
dict_pred :: Type
dict_pred = Class -> [Type] -> Type
mkClassPred Class
cls [Type]
xis
dict_loc :: CtLoc
dict_loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev
dict_origin :: CtOrigin
dict_origin = CtLoc -> CtOrigin
ctLocOrigin CtLoc
dict_loc
mk_ct_loc :: ClsInst
-> (CtLoc, RewriterSet)
mk_ct_loc :: ClsInst -> (CtLoc, RewriterSet)
mk_ct_loc ClsInst
ispec
= ( CtLoc
dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
inst_pred inst_loc }
, RewriterSet
emptyRewriterSet )
where
inst_pred :: Type
inst_pred = Class -> [Type] -> Type
mkClassPred Class
cls (ClsInst -> [Type]
is_tys ClsInst
ispec)
inst_loc :: SrcSpan
inst_loc = EvVar -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan (ClsInst -> EvVar
is_dfun ClsInst
ispec)
makeSuperClasses :: [Ct] -> TcS [Ct]
makeSuperClasses :: [Ct] -> TcS [Ct]
makeSuperClasses [Ct]
cts = (Ct -> TcS [Ct]) -> [Ct] -> TcS [Ct]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM Ct -> TcS [Ct]
go [Ct]
cts
where
go :: Ct -> TcS [Ct]
go (CDictCan (DictCt { di_ev :: DictCt -> CtEvidence
di_ev = CtEvidence
ev, di_cls :: DictCt -> Class
di_cls = Class
cls, di_tys :: DictCt -> [Type]
di_tys = [Type]
tys, di_pend_sc :: DictCt -> ScDepth
di_pend_sc = ScDepth
fuel }))
= ScDepth -> TcS [Ct] -> TcS [Ct]
forall a. ScDepth -> a -> a
assertFuelPreconditionStrict ScDepth
fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
ScDepth
-> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses ScDepth
fuel CtEvidence
ev [] [] Class
cls [Type]
tys
go (CQuantCan (QCI { qci_pred :: QCInst -> Type
qci_pred = Type
pred, qci_ev :: QCInst -> CtEvidence
qci_ev = CtEvidence
ev, qci_pend_sc :: QCInst -> ScDepth
qci_pend_sc = ScDepth
fuel }))
= Bool -> SDoc -> TcS [Ct] -> TcS [Ct]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Type -> Bool
isClassPred Type
pred) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred) (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
ScDepth -> TcS [Ct] -> TcS [Ct]
forall a. ScDepth -> a -> a
assertFuelPreconditionStrict ScDepth
fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
ScDepth
-> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses ScDepth
fuel CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
where
([EvVar]
tvs, [Type]
theta, Class
cls, [Type]
tys) = Type -> ([EvVar], [Type], Class, [Type])
tcSplitDFunTy (CtEvidence -> Type
ctEvPred CtEvidence
ev)
go Ct
ct = String -> SDoc -> TcS [Ct]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"makeSuperClasses" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)
mkStrictSuperClasses
:: ExpansionFuel -> CtEvidence
-> [TyVar] -> ThetaType
-> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses :: ScDepth
-> CtEvidence -> [EvVar] -> [Type] -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses ScDepth
fuel CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
= ScDepth
-> NameSet
-> CtEvidence
-> [EvVar]
-> [Type]
-> Class
-> [Type]
-> TcS [Ct]
mk_strict_superclasses (ScDepth -> ScDepth
consumeFuel ScDepth
fuel) (Name -> NameSet
unitNameSet (Class -> Name
className Class
cls))
CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
mk_strict_superclasses :: ExpansionFuel -> NameSet -> CtEvidence
-> [TyVar] -> ThetaType
-> Class -> [Type] -> TcS [Ct]
mk_strict_superclasses :: ScDepth
-> NameSet
-> CtEvidence
-> [EvVar]
-> [Type]
-> Class
-> [Type]
-> TcS [Ct]
mk_strict_superclasses ScDepth
_ NameSet
_ CtEvidence
_ [EvVar]
_ [Type]
_ Class
cls [Type]
_
| Class -> Bool
isEqualityClass Class
cls
= [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mk_strict_superclasses ScDepth
fuel NameSet
rec_clss
ev :: CtEvidence
ev@(CtGiven { ctev_evar :: CtEvidence -> EvVar
ctev_evar = EvVar
evar, ctev_loc :: CtEvidence -> CtLoc
ctev_loc = CtLoc
loc })
[EvVar]
tvs [Type]
theta Class
cls [Type]
tys
=
do { String -> SDoc -> TcS ()
traceTcS String
"mk_strict" (CtEvidence -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtEvidence
ev SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CtOrigin -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CtLoc -> CtOrigin
ctLocOrigin CtLoc
loc))
; (EvVar -> TcS [Ct]) -> [EvVar] -> TcS [Ct]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM EvVar -> TcS [Ct]
do_one_given (Class -> [EvVar]
classSCSelIds Class
cls) }
where
dict_ids :: [EvVar]
dict_ids = [Type] -> [EvVar]
mkTemplateLocals [Type]
theta
this_size :: PatersonSize
this_size = Class -> [Type] -> PatersonSize
pSizeClassPred Class
cls [Type]
tys
do_one_given :: EvVar -> TcS [Ct]
do_one_given EvVar
sel_id
| HasDebugCallStack => Type -> Bool
Type -> Bool
isUnliftedType Type
sc_pred
, Bool -> Bool
not ([EvVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EvVar]
tvs Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta)
=
[Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise
= do { given_ev <- CtLoc -> (Type, EvTerm) -> TcS CtEvidence
newGivenEvVar CtLoc
sc_loc ((Type, EvTerm) -> TcS CtEvidence)
-> (Type, EvTerm) -> TcS CtEvidence
forall a b. (a -> b) -> a -> b
$
EvVar -> Type -> (Type, EvTerm)
mk_given_desc EvVar
sel_id Type
sc_pred
; assertFuelPrecondition fuel $
mk_superclasses fuel rec_clss given_ev tvs theta sc_pred }
where
sc_pred :: Type
sc_pred = EvVar -> [Type] -> Type
classMethodInstTy EvVar
sel_id [Type]
tys
mk_given_desc :: Id -> PredType -> (PredType, EvTerm)
mk_given_desc :: EvVar -> Type -> (Type, EvTerm)
mk_given_desc EvVar
sel_id Type
sc_pred
= (Type
swizzled_pred, EvTerm
swizzled_evterm)
where
([EvVar]
sc_tvs, Type
sc_rho) = Type -> ([EvVar], Type)
splitForAllTyCoVars Type
sc_pred
([Scaled Type]
sc_theta, Type
sc_inner_pred) = Type -> ([Scaled Type], Type)
splitFunTys Type
sc_rho
all_tvs :: [EvVar]
all_tvs = [EvVar]
tvs [EvVar] -> [EvVar] -> [EvVar]
forall a. [a] -> [a] -> [a]
`chkAppend` [EvVar]
sc_tvs
all_theta :: [Type]
all_theta = [Type]
theta [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
`chkAppend` ((Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
sc_theta)
swizzled_pred :: Type
swizzled_pred = [EvVar] -> [Type] -> Type -> Type
HasDebugCallStack => [EvVar] -> [Type] -> Type -> Type
mkInfSigmaTy [EvVar]
all_tvs [Type]
all_theta Type
sc_inner_pred
swizzled_evterm :: EvTerm
swizzled_evterm = EvExpr -> EvTerm
EvExpr (EvExpr -> EvTerm) -> EvExpr -> EvTerm
forall a b. (a -> b) -> a -> b
$
[EvVar] -> EvExpr -> EvExpr
forall b. [b] -> Expr b -> Expr b
mkLams [EvVar]
all_tvs (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$
[EvVar] -> EvExpr -> EvExpr
forall b. [b] -> Expr b -> Expr b
mkLams [EvVar]
dict_ids (EvExpr -> EvExpr) -> EvExpr -> EvExpr
forall a b. (a -> b) -> a -> b
$
EvVar -> EvExpr
forall b. EvVar -> Expr b
Var EvVar
sel_id
EvExpr -> [Type] -> EvExpr
forall b. Expr b -> [Type] -> Expr b
`mkTyApps` [Type]
tys
EvExpr -> EvExpr -> EvExpr
forall b. Expr b -> Expr b -> Expr b
`App` (EvVar -> EvExpr
evId EvVar
evar EvExpr -> [EvVar] -> EvExpr
forall b. Expr b -> [EvVar] -> Expr b
`mkVarApps` ([EvVar]
tvs [EvVar] -> [EvVar] -> [EvVar]
forall a. [a] -> [a] -> [a]
++ [EvVar]
dict_ids))
EvExpr -> [EvVar] -> EvExpr
forall b. Expr b -> [EvVar] -> Expr b
`mkVarApps` [EvVar]
sc_tvs
sc_loc :: CtLoc
sc_loc | Class -> Bool
isCTupleClass Class
cls = CtLoc
loc
| Bool
otherwise = CtLoc
loc { ctl_origin = mk_sc_origin (ctLocOrigin loc) }
mk_sc_origin :: CtOrigin -> CtOrigin
mk_sc_origin :: CtOrigin -> CtOrigin
mk_sc_origin (GivenSCOrigin SkolemInfoAnon
skol_info ScDepth
sc_depth Bool
already_blocked)
= SkolemInfoAnon -> ScDepth -> Bool -> CtOrigin
GivenSCOrigin SkolemInfoAnon
skol_info (ScDepth
sc_depth ScDepth -> ScDepth -> ScDepth
forall a. Num a => a -> a -> a
+ ScDepth
1)
(Bool
already_blocked Bool -> Bool -> Bool
|| SkolemInfoAnon -> Bool
newly_blocked SkolemInfoAnon
skol_info)
mk_sc_origin (GivenOrigin SkolemInfoAnon
skol_info)
=
SkolemInfoAnon -> ScDepth -> Bool -> CtOrigin
GivenSCOrigin SkolemInfoAnon
skol_info ScDepth
1 (SkolemInfoAnon -> Bool
newly_blocked SkolemInfoAnon
skol_info)
mk_sc_origin CtOrigin
other_orig = String -> SDoc -> CtOrigin
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"Given constraint without given origin" (SDoc -> CtOrigin) -> SDoc -> CtOrigin
forall a b. (a -> b) -> a -> b
$
EvVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr EvVar
evar SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ CtOrigin -> SDoc
forall a. Outputable a => a -> SDoc
ppr CtOrigin
other_orig
newly_blocked :: SkolemInfoAnon -> Bool
newly_blocked (InstSkol ClsInstOrQC
_ PatersonSize
head_size) = Maybe PatersonCondFailure -> Bool
forall a. Maybe a -> Bool
isJust (PatersonSize
this_size PatersonSize -> PatersonSize -> Maybe PatersonCondFailure
`ltPatersonSize` PatersonSize
head_size)
newly_blocked SkolemInfoAnon
_ = Bool
False
mk_strict_superclasses ScDepth
fuel NameSet
rec_clss CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
| (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
noFreeVarsOfType [Type]
tys
= [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise
= Bool -> SDoc -> TcS [Ct] -> TcS [Ct]
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ([EvVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EvVar]
tvs Bool -> Bool -> Bool
&& [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta) ([EvVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [EvVar]
tvs SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
theta) (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
(Type -> TcS [Ct]) -> [Type] -> TcS [Ct]
forall (m :: * -> *) (f :: * -> *) a b.
(Monad m, Traversable f) =>
(a -> m [b]) -> f a -> m [b]
concatMapM Type -> TcS [Ct]
do_one (Class -> [Type] -> [Type]
immSuperClasses Class
cls [Type]
tys)
where
loc :: CtLoc
loc = CtEvidence -> CtLoc
ctEvLoc CtEvidence
ev CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
`updateCtLocOrigin` Type -> CtOrigin -> CtOrigin
WantedSuperclassOrigin (CtEvidence -> Type
ctEvPred CtEvidence
ev)
do_one :: Type -> TcS [Ct]
do_one Type
sc_pred
= do { String -> SDoc -> TcS ()
traceTcS String
"mk_strict_superclasses Wanted" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
sc_pred)
; sc_ev <- CtLoc -> RewriterSet -> Type -> TcS CtEvidence
newWantedNC CtLoc
loc (CtEvidence -> RewriterSet
ctEvRewriters CtEvidence
ev) Type
sc_pred
; mk_superclasses fuel rec_clss sc_ev [] [] sc_pred }
mk_superclasses :: ExpansionFuel -> NameSet -> CtEvidence
-> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
mk_superclasses :: ScDepth
-> NameSet -> CtEvidence -> [EvVar] -> [Type] -> Type -> TcS [Ct]
mk_superclasses ScDepth
fuel NameSet
rec_clss CtEvidence
ev [EvVar]
tvs [Type]
theta Type
pred
| ClassPred Class
cls [Type]
tys <- Type -> Pred
classifyPredType Type
pred
= ScDepth -> TcS [Ct] -> TcS [Ct]
forall a. ScDepth -> a -> a
assertFuelPrecondition ScDepth
fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
ScDepth
-> NameSet
-> CtEvidence
-> [EvVar]
-> [Type]
-> Class
-> [Type]
-> TcS [Ct]
mk_superclasses_of ScDepth
fuel NameSet
rec_clss CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
| Bool
otherwise
= [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [CtEvidence -> Ct
mkNonCanonical CtEvidence
ev]
mk_superclasses_of :: ExpansionFuel -> NameSet -> CtEvidence
-> [TyVar] -> ThetaType -> Class -> [Type]
-> TcS [Ct]
mk_superclasses_of :: ScDepth
-> NameSet
-> CtEvidence
-> [EvVar]
-> [Type]
-> Class
-> [Type]
-> TcS [Ct]
mk_superclasses_of ScDepth
fuel NameSet
rec_clss CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
| Bool
loop_found = do { String -> SDoc -> TcS ()
traceTcS String
"mk_superclasses_of: loop" (Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys)
; ScDepth -> TcS [Ct] -> TcS [Ct]
forall a. ScDepth -> a -> a
assertFuelPrecondition ScDepth
fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$ [Ct] -> TcS [Ct]
forall a. a -> TcS a
forall (m :: * -> *) a. Monad m => a -> m a
return [ScDepth -> Ct
mk_this_ct ScDepth
fuel] }
| Bool
otherwise = do { String -> SDoc -> TcS ()
traceTcS String
"mk_superclasses_of" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
cls SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
tys
, Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Class -> Bool
isCTupleClass Class
cls)
, NameSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr NameSet
rec_clss
])
; sc_cts <- ScDepth -> TcS [Ct] -> TcS [Ct]
forall a. ScDepth -> a -> a
assertFuelPrecondition ScDepth
fuel (TcS [Ct] -> TcS [Ct]) -> TcS [Ct] -> TcS [Ct]
forall a b. (a -> b) -> a -> b
$
ScDepth
-> NameSet
-> CtEvidence
-> [EvVar]
-> [Type]
-> Class
-> [Type]
-> TcS [Ct]
mk_strict_superclasses ScDepth
fuel NameSet
rec_clss' CtEvidence
ev [EvVar]
tvs [Type]
theta Class
cls [Type]
tys
; return (mk_this_ct doNotExpand : sc_cts) }
where
cls_nm :: Name
cls_nm = Class -> Name
className Class
cls
loop_found :: Bool
loop_found = Bool -> Bool
not (Class -> Bool
isCTupleClass Class
cls) Bool -> Bool -> Bool
&& Name
cls_nm Name -> NameSet -> Bool
`elemNameSet` NameSet
rec_clss
rec_clss' :: NameSet
rec_clss' = NameSet
rec_clss NameSet -> Name -> NameSet
`extendNameSet` Name
cls_nm
mk_this_ct :: ExpansionFuel -> Ct
mk_this_ct :: ScDepth -> Ct
mk_this_ct ScDepth
fuel | [EvVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [EvVar]
tvs, [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
theta
= DictCt -> Ct
CDictCan (DictCt { di_ev :: CtEvidence
di_ev = CtEvidence
ev, di_cls :: Class
di_cls = Class
cls
, di_tys :: [Type]
di_tys = [Type]
tys, di_pend_sc :: ScDepth
di_pend_sc = ScDepth
fuel })
| Bool
otherwise
= QCInst -> Ct
CQuantCan (QCI { qci_tvs :: [EvVar]
qci_tvs = [EvVar]
tvs, qci_pred :: Type
qci_pred = Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys
, qci_ev :: CtEvidence
qci_ev = CtEvidence
ev, qci_pend_sc :: ScDepth
qci_pend_sc = ScDepth
fuel })