{-# LANGUAGE CPP #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
module GHC.HsToCore.Pmc.Solver (
Nabla, Nablas(..), initNablas,
lookupRefuts, lookupSolution,
PhiCt(..), PhiCts,
addPhiCtNablas,
addPhiCtsNablas,
isInhabited,
generateInhabitingPatterns
) where
#include "HsVersions.h"
import GHC.Prelude
import GHC.HsToCore.Pmc.Types
import GHC.HsToCore.Pmc.Utils (tracePm, mkPmId)
import GHC.Driver.Session
import GHC.Driver.Config
import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Monad (allM)
import GHC.Utils.Panic
import GHC.Data.Bag
import GHC.Types.CompleteMatch
import GHC.Types.Unique.Set
import GHC.Types.Unique.DSet
import GHC.Types.Unique.SDFM
import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Var (EvVar)
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Core
import GHC.Core.FVs (exprFreeVars)
import GHC.Core.Map.Expr
import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
import GHC.Core.Utils (exprType)
import GHC.Core.Make (mkListExpr, mkCharExpr)
import GHC.Types.Unique.Supply
import GHC.Data.FastString
import GHC.Types.SrcLoc
import GHC.Data.Maybe
import GHC.Core.ConLike
import GHC.Core.DataCon
import GHC.Core.PatSyn
import GHC.Core.TyCon
import GHC.Core.TyCon.RecWalk
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim (tYPETyCon)
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Subst (elemTCvSubst)
import GHC.Core.Type
import GHC.Tc.Solver (tcNormalise, tcCheckGivens, tcCheckWanteds)
import GHC.Core.Unify (tcMatchTy)
import GHC.Core.Coercion
import GHC.HsToCore.Monad hiding (foldlM)
import GHC.Tc.Instance.Family
import GHC.Core.FamInstEnv
import Control.Applicative ((<|>))
import Control.Monad (foldM, forM, guard, mzero, when, filterM)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State.Strict
import Data.Coerce
import Data.Either (partitionEithers)
import Data.Foldable (foldlM, minimumBy, toList)
import Data.Monoid (Any(..))
import Data.List (sortBy, find)
import qualified Data.List.NonEmpty as NE
import Data.Ord (comparing)
addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
addPhiCtsNablas Nablas
nablas PhiCts
cts = forall (m :: * -> *).
Monad m =>
(Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
liftNablasM (\Nabla
d -> Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
addPhiCts Nabla
d PhiCts
cts) Nablas
nablas
addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
nablas PhiCt
ct = Nablas -> PhiCts -> DsM Nablas
addPhiCtsNablas Nablas
nablas (forall a. a -> Bag a
unitBag PhiCt
ct)
liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
liftNablasM :: forall (m :: * -> *).
Monad m =>
(Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
liftNablasM Nabla -> m (Maybe Nabla)
f (MkNablas Bag Nabla
ds) = Bag Nabla -> Nablas
MkNablas forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bag (Maybe a) -> Bag a
catBagMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Nabla -> m (Maybe Nabla)
f Bag Nabla
ds)
isInhabited :: Nablas -> DsM Bool
isInhabited :: Nablas -> DsM Bool
isInhabited (MkNablas Bag Nabla
ds) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Bag Nabla
ds))
updRcm :: (CompleteMatch -> (Bool, CompleteMatch))
-> ResidualCompleteMatches -> (Maybe ResidualCompleteMatches)
updRcm :: (CompleteMatch -> (Bool, CompleteMatch))
-> ResidualCompleteMatches -> Maybe ResidualCompleteMatches
updRcm CompleteMatch -> (Bool, CompleteMatch)
f (RCM Maybe CompleteMatch
vanilla Maybe [CompleteMatch]
pragmas)
| Bool -> Bool
not Bool
any_change = forall a. Maybe a
Nothing
| Bool
otherwise = forall a. a -> Maybe a
Just (Maybe CompleteMatch
-> Maybe [CompleteMatch] -> ResidualCompleteMatches
RCM Maybe CompleteMatch
vanilla' Maybe [CompleteMatch]
pragmas')
where
f' :: CompleteMatch -> (Any, CompleteMatch)
f' :: CompleteMatch -> (Any, CompleteMatch)
f' = coerce :: forall a b. Coercible a b => a -> b
coerce CompleteMatch -> (Bool, CompleteMatch)
f
(Any
chgd, Maybe CompleteMatch
vanilla') = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompleteMatch -> (Any, CompleteMatch)
f' Maybe CompleteMatch
vanilla
(Any
chgds, Maybe [CompleteMatch]
pragmas') = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompleteMatch -> (Any, CompleteMatch)
f') Maybe [CompleteMatch]
pragmas
any_change :: Bool
any_change = Any -> Bool
getAny forall a b. (a -> b) -> a -> b
$ Any
chgd forall a. Monoid a => a -> a -> a
`mappend` Any
chgds
vanillaCompleteMatchTC :: TyCon -> Maybe CompleteMatch
vanillaCompleteMatchTC :: TyCon -> Maybe CompleteMatch
vanillaCompleteMatchTC TyCon
tc =
let
mb_dcs :: Maybe [DataCon]
mb_dcs | TyCon
tc forall a. Eq a => a -> a -> Bool
== TyCon
tYPETyCon = forall a. a -> Maybe a
Just []
| Bool
otherwise = TyCon -> Maybe [DataCon]
tyConDataCons_maybe TyCon
tc
in UniqDSet ConLike -> CompleteMatch
vanillaCompleteMatch forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Uniquable a => [a] -> UniqDSet a
mkUniqDSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map DataCon -> ConLike
RealDataCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [DataCon]
mb_dcs
addCompleteMatches :: ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches :: ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches (RCM Maybe CompleteMatch
v Maybe [CompleteMatch]
Nothing) = Maybe CompleteMatch
-> Maybe [CompleteMatch] -> ResidualCompleteMatches
RCM Maybe CompleteMatch
v forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DsM [CompleteMatch]
dsGetCompleteMatches
addCompleteMatches ResidualCompleteMatches
rcm = forall (f :: * -> *) a. Applicative f => a -> f a
pure ResidualCompleteMatches
rcm
addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addConLikeMatches (RealDataCon DataCon
dc) ResidualCompleteMatches
rcm = TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addTyConMatches (DataCon -> TyCon
dataConTyCon DataCon
dc) ResidualCompleteMatches
rcm
addConLikeMatches (PatSynCon PatSyn
_) ResidualCompleteMatches
rcm = ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches ResidualCompleteMatches
rcm
addTyConMatches :: TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addTyConMatches :: TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addTyConMatches TyCon
tc ResidualCompleteMatches
rcm = ResidualCompleteMatches -> ResidualCompleteMatches
add_tc_match forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches ResidualCompleteMatches
rcm
where
add_tc_match :: ResidualCompleteMatches -> ResidualCompleteMatches
add_tc_match ResidualCompleteMatches
rcm
= ResidualCompleteMatches
rcm{rcm_vanilla :: Maybe CompleteMatch
rcm_vanilla = ResidualCompleteMatches -> Maybe CompleteMatch
rcm_vanilla ResidualCompleteMatches
rcm forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TyCon -> Maybe CompleteMatch
vanillaCompleteMatchTC TyCon
tc}
markMatched :: PmAltCon -> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches)
markMatched :: PmAltCon
-> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches)
markMatched (PmAltLit PmLit
_) ResidualCompleteMatches
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
markMatched (PmAltConLike ConLike
cl) ResidualCompleteMatches
rcm = do
ResidualCompleteMatches
rcm' <- ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addConLikeMatches ConLike
cl ResidualCompleteMatches
rcm
let go :: CompleteMatch -> (Bool, CompleteMatch)
go CompleteMatch
cm = case forall a. Uniquable a => UniqDSet a -> a -> Maybe a
lookupUniqDSet (CompleteMatch -> UniqDSet ConLike
cmConLikes CompleteMatch
cm) ConLike
cl of
Maybe ConLike
Nothing -> (Bool
False, CompleteMatch
cm)
Just ConLike
_ -> (Bool
True, CompleteMatch
cm { cmConLikes :: UniqDSet ConLike
cmConLikes = forall a. Uniquable a => UniqDSet a -> a -> UniqDSet a
delOneFromUniqDSet (CompleteMatch -> UniqDSet ConLike
cmConLikes CompleteMatch
cm) ConLike
cl })
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (CompleteMatch -> (Bool, CompleteMatch))
-> ResidualCompleteMatches -> Maybe ResidualCompleteMatches
updRcm CompleteMatch -> (Bool, CompleteMatch)
go ResidualCompleteMatches
rcm'
data TopNormaliseTypeResult
= NormalisedByConstraints Type
| HadRedexes Type [(Type, DataCon, Type)] Type
tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts (NormalisedByConstraints Type
ty) = (Type
ty, [], Type
ty)
tntrGuts (HadRedexes Type
src_ty [(Type, DataCon, Type)]
ds Type
core_ty) = (Type
src_ty, [(Type, DataCon, Type)]
ds, Type
core_ty)
instance Outputable TopNormaliseTypeResult where
ppr :: TopNormaliseTypeResult -> SDoc
ppr (NormalisedByConstraints Type
ty) = String -> SDoc
text String
"NormalisedByConstraints" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
ty
ppr (HadRedexes Type
src_ty [(Type, DataCon, Type)]
ds Type
core_ty) = String -> SDoc
text String
"HadRedexes" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces SDoc
fields
where
fields :: SDoc
fields = [SDoc] -> SDoc
fsep (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma [ String -> SDoc
text String
"src_ty =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
src_ty
, String -> SDoc
text String
"newtype_dcs =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [(Type, DataCon, Type)]
ds
, String -> SDoc
text String
"core_ty =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
core_ty ])
pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType (TySt Int
_ InertSet
inert) Type
typ
= do FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
String -> SDoc -> DsM ()
tracePm String
"normalise" (forall a. Outputable a => a -> SDoc
ppr Type
typ)
Type
typ' <- forall a. TcM a -> DsM a
initTcDsForSolver forall a b. (a -> b) -> a -> b
$ InertSet -> Type -> TcM Type
tcNormalise InertSet
inert Type
typ
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case forall ev.
NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX (FamInstEnvs
-> NormaliseStepper
(ThetaType -> ThetaType,
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
stepper FamInstEnvs
env) forall {b} {c} {b} {c} {a} {a}.
(b -> c, b -> c) -> (a -> b, a -> b) -> (a -> c, a -> c)
comb Type
typ' of
Maybe
((ThetaType -> ThetaType,
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)]),
Type)
Nothing -> Type -> TopNormaliseTypeResult
NormalisedByConstraints Type
typ'
Just ((ThetaType -> ThetaType
ty_f,[(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tm_f), Type
ty) -> Type -> [(Type, DataCon, Type)] -> Type -> TopNormaliseTypeResult
HadRedexes Type
src_ty [(Type, DataCon, Type)]
newtype_dcs Type
core_ty
where
src_ty :: Type
src_ty = Type -> ThetaType -> Type
eq_src_ty Type
ty (Type
typ' forall a. a -> [a] -> [a]
: ThetaType -> ThetaType
ty_f [Type
ty])
newtype_dcs :: [(Type, DataCon, Type)]
newtype_dcs = [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tm_f []
core_ty :: Type
core_ty = Type
ty
where
eq_src_ty :: Type -> [Type] -> Type
eq_src_ty :: Type -> ThetaType -> Type
eq_src_ty Type
ty ThetaType
tys = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Type
ty forall a. a -> a
id (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Type -> Bool
is_closed_or_data_family ThetaType
tys)
is_closed_or_data_family :: Type -> Bool
is_closed_or_data_family :: Type -> Bool
is_closed_or_data_family Type
ty = Type -> Bool
pmIsClosedType Type
ty Bool -> Bool -> Bool
|| Type -> Bool
isDataFamilyAppType Type
ty
comb :: (b -> c, b -> c) -> (a -> b, a -> b) -> (a -> c, a -> c)
comb (b -> c
tyf1, b -> c
tmf1) (a -> b
tyf2, a -> b
tmf2) = (b -> c
tyf1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
tyf2, b -> c
tmf1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
tmf2)
stepper :: FamInstEnvs
-> NormaliseStepper
(ThetaType -> ThetaType,
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
stepper FamInstEnvs
env = NormaliseStepper
(ThetaType -> ThetaType,
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
newTypeStepper forall ev.
NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
`composeSteppers` forall a.
FamInstEnvs -> NormaliseStepper (ThetaType -> ThetaType, a -> a)
tyFamStepper FamInstEnvs
env
newTypeStepper :: NormaliseStepper ([Type] -> [Type],[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
newTypeStepper :: NormaliseStepper
(ThetaType -> ThetaType,
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
newTypeStepper RecTcChecker
rec_nts TyCon
tc ThetaType
tys
| Just (Type
ty', Coercion
_co) <- TyCon -> ThetaType -> Maybe (Type, Coercion)
instNewTyCon_maybe TyCon
tc ThetaType
tys
, let orig_ty :: Type
orig_ty = TyCon -> ThetaType -> Type
TyConApp TyCon
tc ThetaType
tys
= case RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_nts TyCon
tc of
Just RecTcChecker
rec_nts' -> let tyf :: ThetaType -> ThetaType
tyf = (Type
orig_tyforall a. a -> [a] -> [a]
:)
tmf :: [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tmf = ((Type
orig_ty, TyCon -> DataCon
tyConSingleDataCon TyCon
tc, Type
ty')forall a. a -> [a] -> [a]
:)
in forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts' Type
ty' (ThetaType -> ThetaType
tyf, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tmf)
Maybe RecTcChecker
Nothing -> forall ev. NormaliseStepResult ev
NS_Abort
| Bool
otherwise
= forall ev. NormaliseStepResult ev
NS_Done
tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
tyFamStepper :: forall a.
FamInstEnvs -> NormaliseStepper (ThetaType -> ThetaType, a -> a)
tyFamStepper FamInstEnvs
env RecTcChecker
rec_nts TyCon
tc ThetaType
tys
= case FamInstEnvs
-> TyCon -> ThetaType -> Maybe (Coercion, Type, MCoercion)
topReduceTyFamApp_maybe FamInstEnvs
env TyCon
tc ThetaType
tys of
Just (Coercion
_, Type
rhs, MCoercion
_) -> forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts Type
rhs ((Type
rhsforall a. a -> [a] -> [a]
:), forall a. a -> a
id)
Maybe (Coercion, Type, MCoercion)
_ -> forall ev. NormaliseStepResult ev
NS_Done
pmIsClosedType :: Type -> Bool
pmIsClosedType :: Type -> Bool
pmIsClosedType Type
ty
= case HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty of
Just (TyCon
tc, ThetaType
ty_args)
| TyCon -> Bool
is_algebraic_like TyCon
tc Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isFamilyTyCon TyCon
tc)
-> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
Maybe (TyCon, ThetaType)
_other -> Bool
False
where
is_algebraic_like :: TyCon -> Bool
is_algebraic_like :: TyCon -> Bool
is_algebraic_like TyCon
tc = TyCon -> Bool
isAlgTyCon TyCon
tc Bool -> Bool -> Bool
|| TyCon
tc forall a. Eq a => a -> a -> Bool
== TyCon
tYPETyCon
normaliseSourceTypeWHNF :: TyState -> Type -> DsM Type
normaliseSourceTypeWHNF :: TyState -> Type -> DsM Type
normaliseSourceTypeWHNF TyState
_ Type
ty | Type -> Bool
isSourceTypeInWHNF Type
ty = forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
normaliseSourceTypeWHNF TyState
ty_st Type
ty =
TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType TyState
ty_st Type
ty forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
NormalisedByConstraints Type
ty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
HadRedexes Type
ty [(Type, DataCon, Type)]
_ Type
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
isSourceTypeInWHNF :: Type -> Bool
isSourceTypeInWHNF :: Type -> Bool
isSourceTypeInWHNF Type
ty
| Just (TyCon
tc, ThetaType
_) <- HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty = Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc)
| Bool
otherwise = Bool
False
emptyRCM :: ResidualCompleteMatches
emptyRCM :: ResidualCompleteMatches
emptyRCM = Maybe CompleteMatch
-> Maybe [CompleteMatch] -> ResidualCompleteMatches
RCM forall a. Maybe a
Nothing forall a. Maybe a
Nothing
emptyVarInfo :: Id -> VarInfo
emptyVarInfo :: Id -> VarInfo
emptyVarInfo Id
x
= VI
{ vi_id :: Id
vi_id = Id
x
, vi_pos :: [PmAltConApp]
vi_pos = []
, vi_neg :: PmAltConSet
vi_neg = PmAltConSet
emptyPmAltConSet
, vi_bot :: BotInfo
vi_bot = BotInfo
MaybeBot
, vi_rcm :: ResidualCompleteMatches
vi_rcm = ResidualCompleteMatches
emptyRCM
}
lookupVarInfo :: TmState -> Id -> VarInfo
lookupVarInfo :: TmState -> Id -> VarInfo
lookupVarInfo (TmSt UniqSDFM Id VarInfo
env CoreMap Id
_ DIdSet
_) Id
x = forall a. a -> Maybe a -> a
fromMaybe (Id -> VarInfo
emptyVarInfo Id
x) (forall key ele.
Uniquable key =>
UniqSDFM key ele -> key -> Maybe ele
lookupUSDFM UniqSDFM Id VarInfo
env Id
x)
lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
lookupVarInfoNT TmState
ts Id
x = case TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x of
VI{ vi_pos :: VarInfo -> [PmAltConApp]
vi_pos = [PmAltConApp] -> Maybe Id
as_newtype -> Just Id
y } -> TmState -> Id -> (Id, VarInfo)
lookupVarInfoNT TmState
ts Id
y
VarInfo
res -> (Id
x, VarInfo
res)
where
as_newtype :: [PmAltConApp] -> Maybe Id
as_newtype = forall a. [a] -> Maybe a
listToMaybe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PmAltConApp -> Maybe Id
go
go :: PmAltConApp -> Maybe Id
go PACA{paca_con :: PmAltConApp -> PmAltCon
paca_con = PmAltConLike (RealDataCon DataCon
dc), paca_ids :: PmAltConApp -> [Id]
paca_ids = [Id
y]}
| DataCon -> Bool
isNewDataCon DataCon
dc = forall a. a -> Maybe a
Just Id
y
go PmAltConApp
_ = forall a. Maybe a
Nothing
trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
trvVarInfo :: forall (f :: * -> *) a.
Functor f =>
(VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
trvVarInfo VarInfo -> f (a, VarInfo)
f nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env} } Id
x
= (a, VarInfo) -> (a, Nabla)
set_vi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarInfo -> f (a, VarInfo)
f (TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x)
where
set_vi :: (a, VarInfo) -> (a, Nabla)
set_vi (a
a, VarInfo
vi') =
(a
a, Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts{ ts_facts :: UniqSDFM Id VarInfo
ts_facts = forall key ele.
Uniquable key =>
UniqSDFM key ele -> key -> ele -> UniqSDFM key ele
addToUSDFM UniqSDFM Id VarInfo
env (VarInfo -> Id
vi_id VarInfo
vi') VarInfo
vi' } })
lookupRefuts :: Nabla -> Id -> [PmAltCon]
lookupRefuts :: Nabla -> Id -> [PmAltCon]
lookupRefuts MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = TmState
ts } Id
x =
PmAltConSet -> [PmAltCon]
pmAltConSetElems forall a b. (a -> b) -> a -> b
$ VarInfo -> PmAltConSet
vi_neg forall a b. (a -> b) -> a -> b
$ TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x
isDataConSolution :: PmAltConApp -> Bool
isDataConSolution :: PmAltConApp -> Bool
isDataConSolution PACA{paca_con :: PmAltConApp -> PmAltCon
paca_con = PmAltConLike (RealDataCon DataCon
_)} = Bool
True
isDataConSolution PmAltConApp
_ = Bool
False
lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
lookupSolution Nabla
nabla Id
x = case VarInfo -> [PmAltConApp]
vi_pos (TmState -> Id -> VarInfo
lookupVarInfo (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x) of
[] -> forall a. Maybe a
Nothing
[PmAltConApp]
pos
| Just PmAltConApp
sol <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find PmAltConApp -> Bool
isDataConSolution [PmAltConApp]
pos -> forall a. a -> Maybe a
Just PmAltConApp
sol
| Bool
otherwise -> forall a. a -> Maybe a
Just (forall a. [a] -> a
head [PmAltConApp]
pos)
data PhiCt
= PhiTyCt !PredType
| PhiCoreCt !Id !CoreExpr
| PhiConCt !Id !PmAltCon ![TyVar] ![PredType] ![Id]
| PhiNotConCt !Id !PmAltCon
| PhiBotCt !Id
| PhiNotBotCt !Id
instance Outputable PhiCt where
ppr :: PhiCt -> SDoc
ppr (PhiTyCt Type
ty_ct) = forall a. Outputable a => a -> SDoc
ppr Type
ty_ct
ppr (PhiCoreCt Id
x CoreExpr
e) = forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr CoreExpr
e
ppr (PhiConCt Id
x PmAltCon
con [Id]
tvs ThetaType
dicts [Id]
args) =
[SDoc] -> SDoc
hsep (forall a. Outputable a => a -> SDoc
ppr PmAltCon
con forall a. a -> [a] -> [a]
: [SDoc]
pp_tvs forall a. [a] -> [a] -> [a]
++ [SDoc]
pp_dicts forall a. [a] -> [a] -> [a]
++ [SDoc]
pp_args) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"<-" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Id
x
where
pp_tvs :: [SDoc]
pp_tvs = forall a b. (a -> b) -> [a] -> [b]
map ((SDoc -> SDoc -> SDoc
<> Char -> SDoc
char Char
'@') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
ppr) [Id]
tvs
pp_dicts :: [SDoc]
pp_dicts = forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr ThetaType
dicts
pp_args :: [SDoc]
pp_args = forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
ppr [Id]
args
ppr (PhiNotConCt Id
x PmAltCon
con) = forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"≁" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr PmAltCon
con
ppr (PhiBotCt Id
x) = forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"~ ⊥"
ppr (PhiNotBotCt Id
x) = forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"≁ ⊥"
type PhiCts = Bag PhiCt
initFuel :: Int
initFuel :: Int
initFuel = Int
4
addPhiCts :: Nabla -> PhiCts -> DsM (Maybe Nabla)
addPhiCts :: Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
addPhiCts Nabla
nabla PhiCts
cts = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
let (ThetaType
ty_cts, [PhiCt]
tm_cts) = PhiCts -> (ThetaType, [PhiCt])
partitionPhiCts PhiCts
cts
Nabla
nabla' <- Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addTyCts Nabla
nabla (forall a. [a] -> Bag a
listToBag ThetaType
ty_cts)
Nabla
nabla'' <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Nabla -> PhiCt -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addPhiTmCt Nabla
nabla' (forall a. [a] -> Bag a
listToBag [PhiCt]
tm_cts)
Int
-> TyState -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
inhabitationTest Int
initFuel (Nabla -> TyState
nabla_ty_st Nabla
nabla) Nabla
nabla''
partitionPhiCts :: PhiCts -> ([PredType], [PhiCt])
partitionPhiCts :: PhiCts -> (ThetaType, [PhiCt])
partitionPhiCts = forall a b. [Either a b] -> ([a], [b])
partitionEithers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map PhiCt -> Either Type PhiCt
to_either forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
where
to_either :: PhiCt -> Either Type PhiCt
to_either (PhiTyCt Type
pred_ty) = forall a b. a -> Either a b
Left Type
pred_ty
to_either PhiCt
ct = forall a b. b -> Either a b
Right PhiCt
ct
addTyCts :: Nabla -> Bag PredType -> MaybeT DsM Nabla
addTyCts :: Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addTyCts nabla :: Nabla
nabla@MkNabla{ nabla_ty_st :: Nabla -> TyState
nabla_ty_st = TyState
ty_st } Bag Type
new_ty_cs = do
TyState
ty_st' <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TyState -> Bag Type -> DsM (Maybe TyState)
tyOracle TyState
ty_st Bag Type
new_ty_cs)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla{ nabla_ty_st :: TyState
nabla_ty_st = TyState
ty_st' }
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle :: TyState -> Bag Type -> DsM (Maybe TyState)
tyOracle ty_st :: TyState
ty_st@(TySt Int
n InertSet
inert) Bag Type
cts
| forall a. Bag a -> Bool
isEmptyBag Bag Type
cts
= forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just TyState
ty_st)
| Bool
otherwise
= do { Bag Id
evs <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Type -> DsM Id
nameTyCt Bag Type
cts
; String -> SDoc -> DsM ()
tracePm String
"tyOracle" (forall a. Outputable a => a -> SDoc
ppr Bag Type
cts SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr InertSet
inert)
; Maybe InertSet
mb_new_inert <- forall a. TcM a -> DsM a
initTcDsForSolver forall a b. (a -> b) -> a -> b
$ InertSet -> Bag Id -> TcM (Maybe InertSet)
tcCheckGivens InertSet
inert Bag Id
evs
; forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> InertSet -> TyState
TySt (Int
nforall a. Num a => a -> a -> a
+Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe InertSet
mb_new_inert) }
nameTyCt :: PredType -> DsM EvVar
nameTyCt :: Type -> DsM Id
nameTyCt Type
pred_ty = do
Unique
unique <- forall (m :: * -> *). MonadUnique m => m Unique
getUniqueM
let occname :: OccName
occname = FastString -> OccName
mkVarOccFS (String -> FastString
fsLit (String
"pm_"forall a. [a] -> [a] -> [a]
++forall a. Show a => a -> String
show Unique
unique))
idname :: Name
idname = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
unique OccName
occname SrcSpan
noSrcSpan
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> Type -> Id
mkLocalIdOrCoVar Name
idname Type
Many Type
pred_ty)
addPhiTmCt :: Nabla -> PhiCt -> MaybeT DsM Nabla
addPhiTmCt :: Nabla -> PhiCt -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addPhiTmCt Nabla
_ (PhiTyCt Type
ct) = forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"addPhiCt:TyCt" (forall a. Outputable a => a -> SDoc
ppr Type
ct)
addPhiTmCt Nabla
nabla (PhiCoreCt Id
x CoreExpr
e) = Nabla
-> Id -> CoreExpr -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addCoreCt Nabla
nabla Id
x CoreExpr
e
addPhiTmCt Nabla
nabla (PhiConCt Id
x PmAltCon
con [Id]
tvs ThetaType
dicts [Id]
args) = do
Nabla
nabla' <- Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addTyCts Nabla
nabla (forall a. [a] -> Bag a
listToBag ThetaType
dicts)
Nabla
nabla'' <- Nabla
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addConCt Nabla
nabla' Id
x PmAltCon
con [Id]
tvs [Id]
args
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt Nabla
nabla'' (PmAltCon -> [Id] -> [Id]
filterUnliftedFields PmAltCon
con [Id]
args)
addPhiTmCt Nabla
nabla (PhiNotConCt Id
x PmAltCon
con) = Nabla
-> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotConCt Nabla
nabla Id
x PmAltCon
con
addPhiTmCt Nabla
nabla (PhiBotCt Id
x) = Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addBotCt Nabla
nabla Id
x
addPhiTmCt Nabla
nabla (PhiNotBotCt Id
x) = Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt Nabla
nabla Id
x
filterUnliftedFields :: PmAltCon -> [Id] -> [Id]
filterUnliftedFields :: PmAltCon -> [Id] -> [Id]
filterUnliftedFields PmAltCon
con [Id]
args =
[ Id
arg | (Id
arg, HsImplBang
bang) <- forall a b. String -> [a] -> [b] -> [(a, b)]
zipEqual String
"addPhiCt" [Id]
args (PmAltCon -> [HsImplBang]
pmAltConImplBangs PmAltCon
con)
, HsImplBang -> Bool
isBanged HsImplBang
bang Bool -> Bool -> Bool
|| HasDebugCallStack => Type -> Bool
isUnliftedType (Id -> Type
idType Id
arg) ]
addBotCt :: Nabla -> Id -> MaybeT DsM Nabla
addBotCt :: Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addBotCt nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts=UniqSDFM Id VarInfo
env } } Id
x = do
let (Id
y, vi :: VarInfo
vi@VI { vi_bot :: VarInfo -> BotInfo
vi_bot = BotInfo
bot }) = TmState -> Id -> (Id, VarInfo)
lookupVarInfoNT (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x
case BotInfo
bot of
BotInfo
IsNotBot -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
BotInfo
IsBot -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla
BotInfo
MaybeBot ->
if HasDebugCallStack => Type -> Bool
isUnliftedType (Id -> Type
idType Id
x)
then forall (m :: * -> *) a. MonadPlus m => m a
mzero
else do
let vi' :: VarInfo
vi' = VarInfo
vi{ vi_bot :: BotInfo
vi_bot = BotInfo
IsBot }
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts{ts_facts :: UniqSDFM Id VarInfo
ts_facts = forall key ele.
Uniquable key =>
UniqSDFM key ele -> key -> ele -> UniqSDFM key ele
addToUSDFM UniqSDFM Id VarInfo
env Id
y VarInfo
vi' } }
addNotBotCt :: Nabla -> Id -> MaybeT DsM Nabla
addNotBotCt :: Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts=UniqSDFM Id VarInfo
env} } Id
x = do
let (Id
y, vi :: VarInfo
vi@VI { vi_bot :: VarInfo -> BotInfo
vi_bot = BotInfo
bot }) = TmState -> Id -> (Id, VarInfo)
lookupVarInfoNT (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x
case BotInfo
bot of
BotInfo
IsBot -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
BotInfo
IsNotBot -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla
BotInfo
MaybeBot -> do
let vi' :: VarInfo
vi' = VarInfo
vi{ vi_bot :: BotInfo
vi_bot = BotInfo
IsNotBot}
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Id -> Nabla -> Nabla
markDirty Id
y
forall a b. (a -> b) -> a -> b
$ Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts{ ts_facts :: UniqSDFM Id VarInfo
ts_facts = forall key ele.
Uniquable key =>
UniqSDFM key ele -> key -> ele -> UniqSDFM key ele
addToUSDFM UniqSDFM Id VarInfo
env Id
y VarInfo
vi' } }
addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla
addNotConCt :: Nabla
-> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotConCt Nabla
_ Id
_ (PmAltConLike (RealDataCon DataCon
dc))
| DataCon -> Bool
isNewDataCon DataCon
dc = forall (m :: * -> *) a. MonadPlus m => m a
mzero
addNotConCt Nabla
nabla Id
x PmAltCon
nalt = do
(Maybe Id
mb_mark_dirty, Nabla
nabla') <- forall (f :: * -> *) a.
Functor f =>
(VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
trvVarInfo VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo)
go Nabla
nabla Id
x
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case Maybe Id
mb_mark_dirty of
Just Id
x -> Id -> Nabla -> Nabla
markDirty Id
x Nabla
nabla'
Maybe Id
Nothing -> Nabla
nabla'
where
go :: VarInfo -> MaybeT DsM (Maybe Id, VarInfo)
go :: VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo)
go vi :: VarInfo
vi@(VI Id
x' [PmAltConApp]
pos PmAltConSet
neg BotInfo
_ ResidualCompleteMatches
rcm) = do
let contradicts :: PmAltCon -> PmAltConApp -> Bool
contradicts PmAltCon
nalt PmAltConApp
sol = PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon (PmAltConApp -> PmAltCon
paca_con PmAltConApp
sol) PmAltCon
nalt forall a. Eq a => a -> a -> Bool
== PmEquality
Equal
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PmAltCon -> PmAltConApp -> Bool
contradicts PmAltCon
nalt) [PmAltConApp]
pos))
let implies :: PmAltCon -> PmAltConApp -> Bool
implies PmAltCon
nalt PmAltConApp
sol = PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon (PmAltConApp -> PmAltCon
paca_con PmAltConApp
sol) PmAltCon
nalt forall a. Eq a => a -> a -> Bool
== PmEquality
Disjoint
let neg' :: PmAltConSet
neg'
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PmAltCon -> PmAltConApp -> Bool
implies PmAltCon
nalt) [PmAltConApp]
pos = PmAltConSet
neg
| PmAltCon -> Bool
hasRequiredTheta PmAltCon
nalt = PmAltConSet
neg
| Bool
otherwise = PmAltConSet -> PmAltCon -> PmAltConSet
extendPmAltConSet PmAltConSet
neg PmAltCon
nalt
MASSERT( isPmAltConMatchStrict nalt )
let vi' :: VarInfo
vi' = VarInfo
vi{ vi_neg :: PmAltConSet
vi_neg = PmAltConSet
neg', vi_bot :: BotInfo
vi_bot = BotInfo
IsNotBot }
Maybe ResidualCompleteMatches
mb_rcm' <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (PmAltCon
-> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches)
markMatched PmAltCon
nalt ResidualCompleteMatches
rcm)
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case Maybe ResidualCompleteMatches
mb_rcm' of
Just ResidualCompleteMatches
rcm' -> (forall a. a -> Maybe a
Just Id
x', VarInfo
vi'{ vi_rcm :: ResidualCompleteMatches
vi_rcm = ResidualCompleteMatches
rcm' })
Maybe ResidualCompleteMatches
Nothing -> (forall a. Maybe a
Nothing, VarInfo
vi')
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta (PmAltConLike ConLike
cl) = forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull ThetaType
req_theta
where
([Id]
_,[Id]
_,[EqSpec]
_,ThetaType
_,ThetaType
req_theta,[Scaled Type]
_,Type
_) = ConLike
-> ([Id], [Id], [EqSpec], ThetaType, ThetaType, [Scaled Type],
Type)
conLikeFullSig ConLike
cl
hasRequiredTheta PmAltCon
_ = Bool
False
addConCt :: Nabla -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Nabla
addConCt :: Nabla
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addConCt nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts=UniqSDFM Id VarInfo
env } } Id
x PmAltCon
alt [Id]
tvs [Id]
args = do
let vi :: VarInfo
vi@(VI Id
_ [PmAltConApp]
pos PmAltConSet
neg BotInfo
bot ResidualCompleteMatches
_) = TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (PmAltCon -> PmAltConSet -> Bool
elemPmAltConSet PmAltCon
alt PmAltConSet
neg))
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall a. Eq a => a -> a -> Bool
/= PmEquality
Disjoint) forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
alt forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltConApp -> PmAltCon
paca_con) [PmAltConApp]
pos)
case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((forall a. Eq a => a -> a -> Bool
== PmEquality
Equal) forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
alt forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltConApp -> PmAltCon
paca_con) [PmAltConApp]
pos of
Just (PACA PmAltCon
_con [Id]
other_tvs [Id]
other_args) -> do
let ty_cts :: [PhiCt]
ty_cts = ThetaType -> ThetaType -> [PhiCt]
equateTys (forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyVarTy [Id]
tvs) (forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyVarTy [Id]
other_tvs)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
args forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
other_args) forall a b. (a -> b) -> a -> b
$
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ String -> SDoc -> DsM ()
tracePm String
"error" (forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr PmAltCon
alt SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [Id]
args SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [Id]
other_args)
Nabla
nabla' <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
addPhiCts Nabla
nabla (forall a. [a] -> Bag a
listToBag [PhiCt]
ty_cts)
let add_var_ct :: Nabla -> (Id, Id) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
add_var_ct Nabla
nabla (Id
a, Id
b) = Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addVarCt Nabla
nabla Id
a Id
b
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Nabla -> (Id, Id) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
add_var_ct Nabla
nabla' forall a b. (a -> b) -> a -> b
$ forall a b. String -> [a] -> [b] -> [(a, b)]
zipEqual String
"addConCt" [Id]
args [Id]
other_args
Maybe PmAltConApp
Nothing -> do
let pos' :: [PmAltConApp]
pos' = PmAltCon -> [Id] -> [Id] -> PmAltConApp
PACA PmAltCon
alt [Id]
tvs [Id]
args forall a. a -> [a] -> [a]
: [PmAltConApp]
pos
let nabla_with :: BotInfo -> Nabla
nabla_with BotInfo
bot' =
Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts{ts_facts :: UniqSDFM Id VarInfo
ts_facts = forall key ele.
Uniquable key =>
UniqSDFM key ele -> key -> ele -> UniqSDFM key ele
addToUSDFM UniqSDFM Id VarInfo
env Id
x (VarInfo
vi{vi_pos :: [PmAltConApp]
vi_pos = [PmAltConApp]
pos', vi_bot :: BotInfo
vi_bot = BotInfo
bot'})} }
case (PmAltCon
alt, [Id]
args) of
(PmAltConLike (RealDataCon DataCon
dc), [Id
y]) | DataCon -> Bool
isNewDataCon DataCon
dc ->
case BotInfo
bot of
BotInfo
MaybeBot -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (BotInfo -> Nabla
nabla_with BotInfo
MaybeBot)
BotInfo
IsBot -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addBotCt (BotInfo -> Nabla
nabla_with BotInfo
MaybeBot) Id
y
BotInfo
IsNotBot -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt (BotInfo -> Nabla
nabla_with BotInfo
MaybeBot) Id
y
(PmAltCon, [Id])
_ -> ASSERT( isPmAltConMatchStrict alt )
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BotInfo -> Nabla
nabla_with BotInfo
IsNotBot)
equateTys :: [Type] -> [Type] -> [PhiCt]
equateTys :: ThetaType -> ThetaType -> [PhiCt]
equateTys ThetaType
ts ThetaType
us =
[ Type -> PhiCt
PhiTyCt (Type -> Type -> Type
mkPrimEqPred Type
t Type
u)
| (Type
t, Type
u) <- forall a b. String -> [a] -> [b] -> [(a, b)]
zipEqual String
"equateTys" ThetaType
ts ThetaType
us
, Bool -> Bool
not (Type -> Type -> Bool
eqType Type
t Type
u)
]
addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla
addVarCt :: Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addVarCt nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env } } Id
x Id
y =
case forall key ele.
Uniquable key =>
UniqSDFM key ele -> key -> key -> (Maybe ele, UniqSDFM key ele)
equateUSDFM UniqSDFM Id VarInfo
env Id
x Id
y of
(Maybe VarInfo
Nothing, UniqSDFM Id VarInfo
env') -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts{ ts_facts :: UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env' } })
(Just VarInfo
vi_x, UniqSDFM Id VarInfo
env') -> do
let nabla_equated :: Nabla
nabla_equated = Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts{ts_facts :: UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env'} }
let add_pos :: Nabla
-> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
add_pos Nabla
nabla (PACA PmAltCon
cl [Id]
tvs [Id]
args) = Nabla
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addConCt Nabla
nabla Id
y PmAltCon
cl [Id]
tvs [Id]
args
Nabla
nabla_pos <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Nabla
-> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
add_pos Nabla
nabla_equated (VarInfo -> [PmAltConApp]
vi_pos VarInfo
vi_x)
let add_neg :: Nabla -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
add_neg Nabla
nabla PmAltCon
nalt = Nabla
-> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotConCt Nabla
nabla Id
y PmAltCon
nalt
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Nabla -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
add_neg Nabla
nabla_pos (PmAltConSet -> [PmAltCon]
pmAltConSetElems (VarInfo -> PmAltConSet
vi_neg VarInfo
vi_x))
addCoreCt :: Nabla -> Id -> CoreExpr -> MaybeT DsM Nabla
addCoreCt :: Nabla
-> Id -> CoreExpr -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addCoreCt Nabla
nabla Id
x CoreExpr
e = do
SimpleOpts
simpl_opts <- DynFlags -> SimpleOpts
initSimpleOpts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
let e' :: CoreExpr
e' = HasDebugCallStack => SimpleOpts -> CoreExpr -> CoreExpr
simpleOptExpr SimpleOpts
simpl_opts CoreExpr
e
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x CoreExpr
e') Nabla
nabla
where
core_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
core_expr :: Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x (Cast CoreExpr
e Coercion
_co) = Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x CoreExpr
e
core_expr Id
x (Tick CoreTickish
_t CoreExpr
e) = Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x CoreExpr
e
core_expr Id
x CoreExpr
e
| Just (PmLit -> Maybe FastString
pmLitAsStringLit -> Just FastString
s) <- CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
e
, Type
expr_ty Type -> Type -> Bool
`eqType` Type
stringTy
= case FastString -> String
unpackFS FastString
s of
[] -> Id
-> InScopeSet
-> DataCon
-> [CoreExpr]
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
data_con_app Id
x InScopeSet
emptyInScopeSet DataCon
nilDataCon []
String
s' -> Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x (Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
charTy (forall a b. (a -> b) -> [a] -> [b]
map Char -> CoreExpr
mkCharExpr String
s'))
| Just PmLit
lit <- CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
e
= Id
-> PmLit
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_lit Id
x PmLit
lit
| Just (InScopeSet
in_scope, _empty_floats :: [FloatBind]
_empty_floats@[], DataCon
dc, ThetaType
_arg_tys, [CoreExpr]
args)
<- HasDebugCallStack =>
InScopeEnv
-> CoreExpr
-> Maybe (InScopeSet, [FloatBind], DataCon, ThetaType, [CoreExpr])
exprIsConApp_maybe InScopeEnv
in_scope_env CoreExpr
e
= Id
-> InScopeSet
-> DataCon
-> [CoreExpr]
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
data_con_app Id
x InScopeSet
in_scope DataCon
dc [CoreExpr]
args
| Var Id
y <- CoreExpr
e, Maybe DataCon
Nothing <- Id -> Maybe DataCon
isDataConId_maybe Id
x
= forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT (\Nabla
nabla -> Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addVarCt Nabla
nabla Id
x Id
y)
| Bool
otherwise
= Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
equate_with_similar_expr Id
x CoreExpr
e
where
expr_ty :: Type
expr_ty = CoreExpr -> Type
exprType CoreExpr
e
expr_in_scope :: InScopeSet
expr_in_scope = VarSet -> InScopeSet
mkInScopeSet (CoreExpr -> VarSet
exprFreeVars CoreExpr
e)
in_scope_env :: InScopeEnv
in_scope_env = (InScopeSet
expr_in_scope, forall a b. a -> b -> a
const Unfolding
NoUnfolding)
equate_with_similar_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
equate_with_similar_expr :: Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
equate_with_similar_expr Id
x CoreExpr
e = do
Id
rep <- forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT forall a b. (a -> b) -> a -> b
$ \Nabla
nabla -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nabla -> CoreExpr -> DsM (Id, Nabla)
representCoreExpr Nabla
nabla CoreExpr
e)
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT (\Nabla
nabla -> Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addVarCt Nabla
nabla Id
x Id
rep)
bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) Id
bind_expr :: CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
bind_expr CoreExpr
e = do
Id
x <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Type -> DsM Id
mkPmId (CoreExpr -> Type
exprType CoreExpr
e)))
Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x CoreExpr
e
forall (f :: * -> *) a. Applicative f => a -> f a
pure Id
x
data_con_app :: Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT DsM) ()
data_con_app :: Id
-> InScopeSet
-> DataCon
-> [CoreExpr]
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
data_con_app Id
x InScopeSet
in_scope DataCon
dc [CoreExpr]
args = do
let dc_ex_tvs :: [Id]
dc_ex_tvs = DataCon -> [Id]
dataConExTyCoVars DataCon
dc
arty :: Int
arty = DataCon -> Int
dataConSourceArity DataCon
dc
([CoreExpr]
ex_ty_args, [CoreExpr]
val_args) = forall b a. [b] -> [a] -> ([a], [a])
splitAtList [Id]
dc_ex_tvs [CoreExpr]
args
ex_tys :: ThetaType
ex_tys = forall a b. (a -> b) -> [a] -> [b]
map CoreExpr -> Type
exprToType [CoreExpr]
ex_ty_args
vis_args :: [CoreExpr]
vis_args = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
arty forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [CoreExpr]
val_args
UniqSupply
uniq_supply <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM
let (TCvSubst
_, [Id]
ex_tvs) = TCvSubst -> [Id] -> UniqSupply -> (TCvSubst, [Id])
cloneTyVarBndrs (InScopeSet -> TCvSubst
mkEmptyTCvSubst InScopeSet
in_scope) [Id]
dc_ex_tvs UniqSupply
uniq_supply
ty_cts :: [PhiCt]
ty_cts = ThetaType -> ThetaType -> [PhiCt]
equateTys (forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyVarTy [Id]
ex_tvs) ThetaType
ex_tys
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (DataCon -> Bool
isNewDataCon DataCon
dc)) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT forall a b. (a -> b) -> a -> b
$ \Nabla
nabla -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt Nabla
nabla Id
x
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT forall a b. (a -> b) -> a -> b
$ \Nabla
nabla -> forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
addPhiCts Nabla
nabla (forall a. [a] -> Bag a
listToBag [PhiCt]
ty_cts)
[Id]
arg_ids <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
bind_expr [CoreExpr]
vis_args
Id
-> PmAltCon
-> [Id]
-> [Id]
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_alt_con_app Id
x (ConLike -> PmAltCon
PmAltConLike (DataCon -> ConLike
RealDataCon DataCon
dc)) [Id]
ex_tvs [Id]
arg_ids
pm_lit :: Id -> PmLit -> StateT Nabla (MaybeT DsM) ()
pm_lit :: Id
-> PmLit
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_lit Id
x PmLit
lit = do
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT forall a b. (a -> b) -> a -> b
$ \Nabla
nabla -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt Nabla
nabla Id
x
Id
-> PmAltCon
-> [Id]
-> [Id]
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_alt_con_app Id
x (PmLit -> PmAltCon
PmAltLit PmLit
lit) [] []
pm_alt_con_app :: Id -> PmAltCon -> [TyVar] -> [Id] -> StateT Nabla (MaybeT DsM) ()
pm_alt_con_app :: Id
-> PmAltCon
-> [Id]
-> [Id]
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_alt_con_app Id
x PmAltCon
con [Id]
tvs [Id]
args = forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT forall a b. (a -> b) -> a -> b
$ \Nabla
nabla -> Nabla
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addConCt Nabla
nabla Id
x PmAltCon
con [Id]
tvs [Id]
args
representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
representCoreExpr nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ ts_reps :: TmState -> CoreMap Id
ts_reps = CoreMap Id
reps } } CoreExpr
e
| Just Id
rep <- forall a. CoreMap a -> CoreExpr -> Maybe a
lookupCoreMap CoreMap Id
reps CoreExpr
e = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id
rep, Nabla
nabla)
| Bool
otherwise = do
Id
rep <- Type -> DsM Id
mkPmId (CoreExpr -> Type
exprType CoreExpr
e)
let reps' :: CoreMap Id
reps' = forall a. CoreMap a -> CoreExpr -> a -> CoreMap a
extendCoreMap CoreMap Id
reps CoreExpr
e Id
rep
let nabla' :: Nabla
nabla' = Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts{ ts_reps :: CoreMap Id
ts_reps = CoreMap Id
reps' } }
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id
rep, Nabla
nabla')
modifyT :: Monad m => (s -> m s) -> StateT s m ()
modifyT :: forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT s -> m s
f = forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) ()) forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> m s
f
tyStateRefined :: TyState -> TyState -> Bool
tyStateRefined :: TyState -> TyState -> Bool
tyStateRefined TyState
a TyState
b = TyState -> Int
ty_st_n TyState
a forall a. Eq a => a -> a -> Bool
/= TyState -> Int
ty_st_n TyState
b
markDirty :: Id -> Nabla -> Nabla
markDirty :: Id -> Nabla -> Nabla
markDirty Id
x nabla :: Nabla
nabla@MkNabla{nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ts_dirty :: TmState -> DIdSet
ts_dirty = DIdSet
dirty} } =
Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts{ ts_dirty :: DIdSet
ts_dirty = DIdSet -> Id -> DIdSet
extendDVarSet DIdSet
dirty Id
x } }
traverseDirty :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
traverseDirty :: forall (m :: * -> *).
Monad m =>
(VarInfo -> m VarInfo) -> TmState -> m TmState
traverseDirty VarInfo -> m VarInfo
f ts :: TmState
ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env, ts_dirty :: TmState -> DIdSet
ts_dirty = DIdSet
dirty} =
[Id] -> UniqSDFM Id VarInfo -> m TmState
go (forall a. UniqDSet a -> [a]
uniqDSetToList DIdSet
dirty) UniqSDFM Id VarInfo
env
where
go :: [Id] -> UniqSDFM Id VarInfo -> m TmState
go [] UniqSDFM Id VarInfo
env = forall (f :: * -> *) a. Applicative f => a -> f a
pure TmState
ts{ts_facts :: UniqSDFM Id VarInfo
ts_facts=UniqSDFM Id VarInfo
env}
go (Id
x:[Id]
xs) !UniqSDFM Id VarInfo
env = do
VarInfo
vi' <- VarInfo -> m VarInfo
f (TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x)
[Id] -> UniqSDFM Id VarInfo -> m TmState
go [Id]
xs (forall key ele.
Uniquable key =>
UniqSDFM key ele -> key -> ele -> UniqSDFM key ele
addToUSDFM UniqSDFM Id VarInfo
env Id
x VarInfo
vi')
traverseAll :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
traverseAll :: forall (m :: * -> *).
Monad m =>
(VarInfo -> m VarInfo) -> TmState -> m TmState
traverseAll VarInfo -> m VarInfo
f ts :: TmState
ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env} = do
UniqSDFM Id VarInfo
env' <- forall key a b (f :: * -> *).
Applicative f =>
(a -> f b) -> UniqSDFM key a -> f (UniqSDFM key b)
traverseUSDFM VarInfo -> m VarInfo
f UniqSDFM Id VarInfo
env
forall (f :: * -> *) a. Applicative f => a -> f a
pure TmState
ts{ts_facts :: UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env'}
inhabitationTest :: Int -> TyState -> Nabla -> MaybeT DsM Nabla
inhabitationTest :: Int
-> TyState -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
inhabitationTest Int
0 TyState
_ Nabla
nabla = forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla
inhabitationTest Int
fuel TyState
old_ty_st nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = TmState
ts } = do
TmState
ts' <- if TyState -> TyState -> Bool
tyStateRefined TyState
old_ty_st (Nabla -> TyState
nabla_ty_st Nabla
nabla)
then forall (m :: * -> *).
Monad m =>
(VarInfo -> m VarInfo) -> TmState -> m TmState
traverseAll VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
test_one TmState
ts
else forall (m :: * -> *).
Monad m =>
(VarInfo -> m VarInfo) -> TmState -> m TmState
traverseDirty VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
test_one TmState
ts
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts'{ts_dirty :: DIdSet
ts_dirty=DIdSet
emptyDVarSet}}
where
nabla_not_dirty :: Nabla
nabla_not_dirty = Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts{ts_dirty :: DIdSet
ts_dirty=DIdSet
emptyDVarSet} }
test_one :: VarInfo -> MaybeT DsM VarInfo
test_one :: VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
test_one VarInfo
vi =
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TyState -> Nabla -> VarInfo -> DsM Bool
varNeedsTesting TyState
old_ty_st Nabla
nabla VarInfo
vi) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> do
Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instantiate (Int
fuelforall a. Num a => a -> a -> a
-Int
1) Nabla
nabla_not_dirty VarInfo
vi
Bool
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi
varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool
varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool
varNeedsTesting TyState
_ MkNabla{nabla_tm_st :: Nabla -> TmState
nabla_tm_st=TmState
tm_st} VarInfo
vi
| Id -> DIdSet -> Bool
elemDVarSet (VarInfo -> Id
vi_id VarInfo
vi) (TmState -> DIdSet
ts_dirty TmState
tm_st) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
varNeedsTesting TyState
_ Nabla
_ VarInfo
vi
| forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull (VarInfo -> [PmAltConApp]
vi_pos VarInfo
vi) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
varNeedsTesting TyState
old_ty_st MkNabla{nabla_ty_st :: Nabla -> TyState
nabla_ty_st=TyState
new_ty_st} VarInfo
_
| Bool -> Bool
not (TyState -> TyState -> Bool
tyStateRefined TyState
old_ty_st TyState
new_ty_st) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
varNeedsTesting TyState
old_ty_st MkNabla{nabla_ty_st :: Nabla -> TyState
nabla_ty_st=TyState
new_ty_st} VarInfo
vi = do
(Type
_, [(Type, DataCon, Type)]
_, Type
old_norm_ty) <- TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType TyState
old_ty_st (Id -> Type
idType forall a b. (a -> b) -> a -> b
$ VarInfo -> Id
vi_id VarInfo
vi)
(Type
_, [(Type, DataCon, Type)]
_, Type
new_norm_ty) <- TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType TyState
new_ty_st (Id -> Type
idType forall a b. (a -> b) -> a -> b
$ VarInfo -> Id
vi_id VarInfo
vi)
if Type
old_norm_ty Type -> Type -> Bool
`eqType` Type
new_norm_ty
then forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
else forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
instantiate :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
instantiate :: Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instantiate Int
fuel Nabla
nabla VarInfo
vi = Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instBot Int
fuel Nabla
nabla VarInfo
vi forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instCompleteSets Int
fuel Nabla
nabla VarInfo
vi
instBot :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
instBot :: Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instBot Int
_fuel Nabla
nabla VarInfo
vi = do
Nabla
_nabla' <- Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addBotCt Nabla
nabla (VarInfo -> Id
vi_id VarInfo
vi)
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi
addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
addNormalisedTypeMatches nabla :: Nabla
nabla@MkNabla{ nabla_ty_st :: Nabla -> TyState
nabla_ty_st = TyState
ty_st } Id
x
= forall (f :: * -> *) a.
Functor f =>
(VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
trvVarInfo VarInfo
-> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo)
add_matches Nabla
nabla Id
x
where
add_matches :: VarInfo
-> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo)
add_matches vi :: VarInfo
vi@VI{ vi_rcm :: VarInfo -> ResidualCompleteMatches
vi_rcm = ResidualCompleteMatches
rcm }
| ResidualCompleteMatches -> Bool
isRcmInitialised ResidualCompleteMatches
rcm = forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResidualCompleteMatches
rcm, VarInfo
vi)
add_matches vi :: VarInfo
vi@VI{ vi_rcm :: VarInfo -> ResidualCompleteMatches
vi_rcm = ResidualCompleteMatches
rcm } = do
Type
norm_res_ty <- TyState -> Type -> DsM Type
normaliseSourceTypeWHNF TyState
ty_st (Id -> Type
idType Id
x)
FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
ResidualCompleteMatches
rcm' <- case FamInstEnvs -> Type -> Maybe (TyCon, ThetaType, Coercion)
splitReprTyConApp_maybe FamInstEnvs
env Type
norm_res_ty of
Just (TyCon
rep_tc, ThetaType
_args, Coercion
_co) -> TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addTyConMatches TyCon
rep_tc ResidualCompleteMatches
rcm
Maybe (TyCon, ThetaType, Coercion)
Nothing -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches ResidualCompleteMatches
rcm
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResidualCompleteMatches
rcm', VarInfo
vi{ vi_rcm :: ResidualCompleteMatches
vi_rcm = ResidualCompleteMatches
rcm' })
splitReprTyConApp_maybe :: FamInstEnvs -> Type -> Maybe (TyCon, [Type], Coercion)
splitReprTyConApp_maybe :: FamInstEnvs -> Type -> Maybe (TyCon, ThetaType, Coercion)
splitReprTyConApp_maybe FamInstEnvs
env Type
ty =
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (FamInstEnvs -> TyCon -> ThetaType -> (TyCon, ThetaType, Coercion)
tcLookupDataFamInst FamInstEnvs
env) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty
instCompleteSets :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
instCompleteSets :: Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instCompleteSets Int
fuel Nabla
nabla VarInfo
vi = do
let x :: Id
x = VarInfo -> Id
vi_id VarInfo
vi
(ResidualCompleteMatches
rcm, Nabla
nabla) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
addNormalisedTypeMatches Nabla
nabla Id
x)
Nabla
nabla <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\Nabla
nabla CompleteMatch
cls -> Int
-> Nabla
-> Id
-> CompleteMatch
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
instCompleteSet Int
fuel Nabla
nabla Id
x CompleteMatch
cls) Nabla
nabla (ResidualCompleteMatches -> [CompleteMatch]
getRcm ResidualCompleteMatches
rcm)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TmState -> Id -> VarInfo
lookupVarInfo (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x)
anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool
anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool
anyConLikeSolution ConLike -> Bool
p = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PmAltCon -> Bool
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltConApp -> PmAltCon
paca_con)
where
go :: PmAltCon -> Bool
go (PmAltConLike ConLike
cl) = ConLike -> Bool
p ConLike
cl
go PmAltCon
_ = Bool
False
instCompleteSet :: Int -> Nabla -> Id -> CompleteMatch -> MaybeT DsM Nabla
instCompleteSet :: Int
-> Nabla
-> Id
-> CompleteMatch
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
instCompleteSet Int
fuel Nabla
nabla Id
x CompleteMatch
cs
| (ConLike -> Bool) -> [PmAltConApp] -> Bool
anyConLikeSolution (forall a. Uniquable a => a -> UniqDSet a -> Bool
`elementOfUniqDSet` (CompleteMatch -> UniqDSet ConLike
cmConLikes CompleteMatch
cs)) (VarInfo -> [PmAltConApp]
vi_pos VarInfo
vi)
= forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla
| Bool -> Bool
not (Type -> CompleteMatch -> Bool
completeMatchAppliesAtType (Id -> Type
varType Id
x) CompleteMatch
cs)
= forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla
| Bool
otherwise
= Nabla -> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
go Nabla
nabla (CompleteMatch -> [ConLike]
sorted_candidates CompleteMatch
cs)
where
vi :: VarInfo
vi = TmState -> Id -> VarInfo
lookupVarInfo (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x
sorted_candidates :: CompleteMatch -> [ConLike]
sorted_candidates :: CompleteMatch -> [ConLike]
sorted_candidates CompleteMatch
cm
| forall a. UniqDSet a -> Int
sizeUniqDSet UniqDSet ConLike
cs forall a. Ord a => a -> a -> Bool
<= Int
5 = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ConLike -> ConLike -> Ordering
compareConLikeTestability (forall a. UniqDSet a -> [a]
uniqDSetToList UniqDSet ConLike
cs)
| Bool
otherwise = forall a. UniqDSet a -> [a]
uniqDSetToList UniqDSet ConLike
cs
where cs :: UniqDSet ConLike
cs = CompleteMatch -> UniqDSet ConLike
cmConLikes CompleteMatch
cm
go :: Nabla -> [ConLike] -> MaybeT DsM Nabla
go :: Nabla -> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
go Nabla
_ [] = forall (m :: * -> *) a. MonadPlus m => m a
mzero
go Nabla
nabla (RealDataCon DataCon
dc:[ConLike]
_)
| DataCon -> Bool
isDataConTriviallyInhabited DataCon
dc
= forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla
go Nabla
nabla (ConLike
con:[ConLike]
cons) = do
let x :: Id
x = VarInfo -> Id
vi_id VarInfo
vi
let recur_not_con :: MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
recur_not_con = do
Nabla
nabla' <- Nabla
-> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotConCt Nabla
nabla Id
x (ConLike -> PmAltCon
PmAltConLike ConLike
con)
Nabla -> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
go Nabla
nabla' [ConLike]
cons
(Nabla
nabla forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Int
-> Nabla
-> Id
-> ConLike
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
instCon Int
fuel Nabla
nabla Id
x ConLike
con)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
recur_not_con
isDataConTriviallyInhabited :: DataCon -> Bool
isDataConTriviallyInhabited :: DataCon -> Bool
isDataConTriviallyInhabited DataCon
dc
| TyCon -> Bool
isTyConTriviallyInhabited (DataCon -> TyCon
dataConTyCon DataCon
dc) = Bool
True
isDataConTriviallyInhabited DataCon
dc =
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> ThetaType
dataConTheta DataCon
dc) Bool -> Bool -> Bool
&&
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> [HsImplBang]
dataConImplBangs DataCon
dc) Bool -> Bool -> Bool
&&
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> ThetaType
dataConUnliftedFieldTys DataCon
dc)
dataConUnliftedFieldTys :: DataCon -> [Type]
dataConUnliftedFieldTys :: DataCon -> ThetaType
dataConUnliftedFieldTys =
forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Bool
True) forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasDebugCallStack => Type -> Maybe Bool
isLiftedType_maybe) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Scaled a -> a
scaledThing forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> [Scaled Type]
dataConOrigArgTys
isTyConTriviallyInhabited :: TyCon -> Bool
isTyConTriviallyInhabited :: TyCon -> Bool
isTyConTriviallyInhabited TyCon
tc = forall a. Uniquable a => a -> UniqSet a -> Bool
elementOfUniqSet TyCon
tc UniqSet TyCon
triviallyInhabitedTyCons
triviallyInhabitedTyCons :: UniqSet TyCon
triviallyInhabitedTyCons :: UniqSet TyCon
triviallyInhabitedTyCons = forall a. Uniquable a => [a] -> UniqSet a
mkUniqSet [
TyCon
charTyCon, TyCon
doubleTyCon, TyCon
floatTyCon, TyCon
intTyCon, TyCon
wordTyCon, TyCon
word8TyCon
]
compareConLikeTestability :: ConLike -> ConLike -> Ordering
compareConLikeTestability :: ConLike -> ConLike -> Ordering
compareConLikeTestability PatSynCon{} ConLike
_ = Ordering
GT
compareConLikeTestability ConLike
_ PatSynCon{} = Ordering
GT
compareConLikeTestability (RealDataCon DataCon
a) (RealDataCon DataCon
b) = forall a. Monoid a => [a] -> a
mconcat
[ forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (forall a. [a] -> Int
fast_length forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> ThetaType
dataConTheta)
, forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing DataCon -> Int
unlifted_or_strict_fields
] DataCon
a DataCon
b
where
fast_length :: [a] -> Int
fast_length :: forall a. [a] -> Int
fast_length [a]
xs = forall a b. ([a] -> b) -> b -> [a] -> Int -> b
atLength forall (t :: * -> *) a. Foldable t => t a -> Int
length Int
6 [a]
xs Int
5
unlifted_or_strict_fields :: DataCon -> Int
unlifted_or_strict_fields :: DataCon -> Int
unlifted_or_strict_fields DataCon
dc = forall a. [a] -> Int
fast_length (DataCon -> [HsImplBang]
dataConImplBangs DataCon
dc)
forall a. Num a => a -> a -> a
+ forall a. [a] -> Int
fast_length (DataCon -> ThetaType
dataConUnliftedFieldTys DataCon
dc)
instCon :: Int -> Nabla -> Id -> ConLike -> MaybeT DsM Nabla
instCon :: Int
-> Nabla
-> Id
-> ConLike
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
instCon Int
fuel nabla :: Nabla
nabla@MkNabla{nabla_ty_st :: Nabla -> TyState
nabla_ty_st = TyState
ty_st} Id
x ConLike
con = forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ do
FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
let match_ty :: Type
match_ty = Id -> Type
idType Id
x
Type
norm_match_ty <- TyState -> Type -> DsM Type
normaliseSourceTypeWHNF TyState
ty_st Type
match_ty
Maybe TCvSubst
mb_sigma_univ <- FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe TCvSubst)
matchConLikeResTy FamInstEnvs
env TyState
ty_st Type
norm_match_ty ConLike
con
case Maybe TCvSubst
mb_sigma_univ of
Just TCvSubst
sigma_univ -> do
let ([Id]
_univ_tvs, [Id]
ex_tvs, [EqSpec]
eq_spec, ThetaType
thetas, ThetaType
_req_theta, [Scaled Type]
field_tys, Type
_con_res_ty)
= ConLike
-> ([Id], [Id], [EqSpec], ThetaType, ThetaType, [Scaled Type],
Type)
conLikeFullSig ConLike
con
(TCvSubst
sigma_ex, [Id]
_) <- TCvSubst -> [Id] -> UniqSupply -> (TCvSubst, [Id])
cloneTyVarBndrs TCvSubst
sigma_univ [Id]
ex_tvs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM
let gammas :: ThetaType
gammas = HasCallStack => TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
sigma_ex ([EqSpec] -> ThetaType
eqSpecPreds [EqSpec]
eq_spec forall a. [a] -> [a] -> [a]
++ ThetaType
thetas)
let field_tys' :: ThetaType
field_tys' = HasCallStack => TCvSubst -> ThetaType -> ThetaType
substTys TCvSubst
sigma_ex forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Scaled a -> a
scaledThing [Scaled Type]
field_tys
[Id]
arg_ids <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> DsM Id
mkPmId ThetaType
field_tys'
String -> SDoc -> DsM ()
tracePm String
"instCon" forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
[ forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
match_ty
, String -> SDoc
text String
"In WHNF:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Type -> Bool
isSourceTypeInWHNF Type
match_ty) SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
norm_match_ty
, forall a. Outputable a => a -> SDoc
ppr ConLike
con SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"... ->" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
_con_res_ty
, forall a. Outputable a => a -> SDoc
ppr (forall a b. (a -> b) -> [a] -> [b]
map (\Id
tv -> forall a. Outputable a => a -> SDoc
ppr Id
tv SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'↦' SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (TCvSubst -> Id -> Type
substTyVar TCvSubst
sigma_univ Id
tv)) [Id]
_univ_tvs)
, forall a. Outputable a => a -> SDoc
ppr ThetaType
gammas
, forall a. Outputable a => a -> SDoc
ppr (forall a b. (a -> b) -> [a] -> [b]
map (\Id
x -> forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Id -> Type
idType Id
x)) [Id]
arg_ids)
, forall a. Outputable a => a -> SDoc
ppr Int
fuel
]
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
let alt :: PmAltCon
alt = ConLike -> PmAltCon
PmAltConLike ConLike
con
Nabla
nabla' <- Nabla -> PhiCt -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addPhiTmCt Nabla
nabla (Id -> PmAltCon -> [Id] -> ThetaType -> [Id] -> PhiCt
PhiConCt Id
x PmAltCon
alt [Id]
ex_tvs ThetaType
gammas [Id]
arg_ids)
let branching_factor :: Int
branching_factor = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ PmAltCon -> [Id] -> [Id]
filterUnliftedFields PmAltCon
alt [Id]
arg_ids
let new_fuel :: Int
new_fuel
| Int
branching_factor forall a. Ord a => a -> a -> Bool
<= Int
1 = Int
fuel
| Bool
otherwise = forall a. Ord a => a -> a -> a
min Int
fuel Int
2
Int
-> TyState -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
inhabitationTest Int
new_fuel (Nabla -> TyState
nabla_ty_st Nabla
nabla) Nabla
nabla'
Maybe TCvSubst
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just Nabla
nabla)
matchConLikeResTy :: FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe TCvSubst)
matchConLikeResTy :: FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe TCvSubst)
matchConLikeResTy FamInstEnvs
env TyState
_ Type
ty (RealDataCon DataCon
dc) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ do
(TyCon
rep_tc, ThetaType
tc_args, Coercion
_co) <- FamInstEnvs -> Type -> Maybe (TyCon, ThetaType, Coercion)
splitReprTyConApp_maybe FamInstEnvs
env Type
ty
if TyCon
rep_tc forall a. Eq a => a -> a -> Bool
== DataCon -> TyCon
dataConTyCon DataCon
dc
then forall a. a -> Maybe a
Just (HasDebugCallStack => [Id] -> ThetaType -> TCvSubst
zipTCvSubst (DataCon -> [Id]
dataConUnivTyVars DataCon
dc) ThetaType
tc_args)
else forall a. Maybe a
Nothing
matchConLikeResTy FamInstEnvs
_ (TySt Int
_ InertSet
inert) Type
ty (PatSynCon PatSyn
ps) = forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ do
let ([Id]
univ_tvs,ThetaType
req_theta,[Id]
_,ThetaType
_,[Scaled Type]
_,Type
con_res_ty) = PatSyn -> ([Id], ThetaType, [Id], ThetaType, [Scaled Type], Type)
patSynSig PatSyn
ps
TCvSubst
subst <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Type -> Type -> Maybe TCvSubst
tcMatchTy Type
con_res_ty Type
ty
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Id -> TCvSubst -> Bool
`elemTCvSubst` TCvSubst
subst) [Id]
univ_tvs
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
req_theta
then forall (f :: * -> *) a. Applicative f => a -> f a
pure TCvSubst
subst
else do
let req_theta' :: ThetaType
req_theta' = HasCallStack => TCvSubst -> ThetaType -> ThetaType
substTys TCvSubst
subst ThetaType
req_theta
Bool
satisfiable <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. TcM a -> DsM a
initTcDsForSolver forall a b. (a -> b) -> a -> b
$ InertSet -> ThetaType -> TcM Bool
tcCheckWanteds InertSet
inert ThetaType
req_theta'
if Bool
satisfiable
then forall (f :: * -> *) a. Applicative f => a -> f a
pure TCvSubst
subst
else forall (m :: * -> *) a. MonadPlus m => m a
mzero
generateInhabitingPatterns :: [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns :: [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns [Id]
_ Int
0 Nabla
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
generateInhabitingPatterns [] Int
_ Nabla
nabla = forall (f :: * -> *) a. Applicative f => a -> f a
pure [Nabla
nabla]
generateInhabitingPatterns (Id
x:[Id]
xs) Int
n Nabla
nabla = do
String -> SDoc -> DsM ()
tracePm String
"generateInhabitingPatterns" (forall a. Outputable a => a -> SDoc
ppr Int
n SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Id
xforall a. a -> [a] -> [a]
:[Id]
xs) SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr Nabla
nabla)
let VI Id
_ [PmAltConApp]
pos PmAltConSet
neg BotInfo
_ ResidualCompleteMatches
_ = TmState -> Id -> VarInfo
lookupVarInfo (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x
case [PmAltConApp]
pos of
PmAltConApp
_:[PmAltConApp]
_ -> do
let arg_vas :: [Id]
arg_vas = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PmAltConApp -> [Id]
paca_ids [PmAltConApp]
pos
[Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns ([Id]
arg_vas forall a. [a] -> [a] -> [a]
++ [Id]
xs) Int
n Nabla
nabla
[]
| forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull [ PmLit
l | PmAltLit PmLit
l <- PmAltConSet -> [PmAltCon]
pmAltConSetElems PmAltConSet
neg ]
-> [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns [Id]
xs Int
n Nabla
nabla
[] -> Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
try_instantiate Id
x [Id]
xs Int
n Nabla
nabla
where
try_instantiate :: Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
try_instantiate :: Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
try_instantiate Id
x [Id]
xs Int
n Nabla
nabla = do
(Type
_src_ty, [(Type, DataCon, Type)]
dcs, Type
rep_ty) <- TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType (Nabla -> TyState
nabla_ty_st Nabla
nabla) (Id -> Type
idType Id
x)
Maybe (Id, Nabla)
mb_stuff <- forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ Id
-> Nabla
-> [(Type, DataCon, Type)]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)
instantiate_newtype_chain Id
x Nabla
nabla [(Type, DataCon, Type)]
dcs
case Maybe (Id, Nabla)
mb_stuff of
Maybe (Id, Nabla)
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Just (Id
y, Nabla
newty_nabla) -> do
let vi :: VarInfo
vi = TmState -> Id -> VarInfo
lookupVarInfo (Nabla -> TmState
nabla_tm_st Nabla
newty_nabla) Id
y
FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
ResidualCompleteMatches
rcm <- case FamInstEnvs -> Type -> Maybe (TyCon, ThetaType, Coercion)
splitReprTyConApp_maybe FamInstEnvs
env Type
rep_ty of
Just (TyCon
tc, ThetaType
_, Coercion
_) -> TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addTyConMatches TyCon
tc (VarInfo -> ResidualCompleteMatches
vi_rcm VarInfo
vi)
Maybe (TyCon, ThetaType, Coercion)
Nothing -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches (VarInfo -> ResidualCompleteMatches
vi_rcm VarInfo
vi)
[CompleteMatch]
clss <- TyState -> Type -> ResidualCompleteMatches -> DsM [CompleteMatch]
pickApplicableCompleteSets (Nabla -> TyState
nabla_ty_st Nabla
nabla) Type
rep_ty ResidualCompleteMatches
rcm
case forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty (forall a. UniqDSet a -> [a]
uniqDSetToList forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompleteMatch -> UniqDSet ConLike
cmConLikes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CompleteMatch]
clss) of
Maybe (NonEmpty [ConLike])
Nothing ->
[Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns [Id]
xs Int
n Nabla
newty_nabla
Just NonEmpty [ConLike]
clss -> do
NonEmpty [Nabla]
nablass' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM NonEmpty [ConLike]
clss (Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
instantiate_cons Id
y Type
rep_ty [Id]
xs Int
n Nabla
newty_nabla)
let nablas' :: [Nabla]
nablas' = forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall (t :: * -> *) a. Foldable t => t a -> Int
length) NonEmpty [Nabla]
nablass'
if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Nabla]
nablas' Bool -> Bool -> Bool
&& VarInfo -> BotInfo
vi_bot VarInfo
vi forall a. Eq a => a -> a -> Bool
/= BotInfo
IsNotBot
then [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns [Id]
xs Int
n Nabla
newty_nabla
else forall (f :: * -> *) a. Applicative f => a -> f a
pure [Nabla]
nablas'
instantiate_newtype_chain :: Id -> Nabla -> [(Type, DataCon, Type)] -> MaybeT DsM (Id, Nabla)
instantiate_newtype_chain :: Id
-> Nabla
-> [(Type, DataCon, Type)]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)
instantiate_newtype_chain Id
x Nabla
nabla [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id
x, Nabla
nabla)
instantiate_newtype_chain Id
x Nabla
nabla ((Type
_ty, DataCon
dc, Type
arg_ty):[(Type, DataCon, Type)]
dcs) = do
Id
y <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Type -> DsM Id
mkPmId Type
arg_ty
Nabla
nabla' <- Nabla
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addConCt Nabla
nabla Id
x (ConLike -> PmAltCon
PmAltConLike (DataCon -> ConLike
RealDataCon DataCon
dc)) [] [Id
y]
Id
-> Nabla
-> [(Type, DataCon, Type)]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)
instantiate_newtype_chain Id
y Nabla
nabla' [(Type, DataCon, Type)]
dcs
instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
instantiate_cons Id
_ Type
_ [Id]
_ Int
_ Nabla
_ [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
instantiate_cons Id
_ Type
_ [Id]
_ Int
0 Nabla
_ [ConLike]
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
instantiate_cons Id
_ Type
ty [Id]
xs Int
n Nabla
nabla [ConLike]
_
| forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TyCon -> Bool
isTyConTriviallyInhabited forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty) forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Bool
True
= [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns [Id]
xs Int
n Nabla
nabla
instantiate_cons Id
x Type
ty [Id]
xs Int
n Nabla
nabla (ConLike
cl:[ConLike]
cls) = do
Maybe Nabla
mb_nabla <- forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ Int
-> Nabla
-> Id
-> ConLike
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
instCon Int
4 Nabla
nabla Id
x ConLike
cl
String -> SDoc -> DsM ()
tracePm String
"instantiate_cons" ([SDoc] -> SDoc
vcat [ forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Id -> Type
idType Id
x)
, forall a. Outputable a => a -> SDoc
ppr Type
ty
, forall a. Outputable a => a -> SDoc
ppr ConLike
cl
, forall a. Outputable a => a -> SDoc
ppr Nabla
nabla
, forall a. Outputable a => a -> SDoc
ppr Maybe Nabla
mb_nabla
, forall a. Outputable a => a -> SDoc
ppr Int
n ])
[Nabla]
con_nablas <- case Maybe Nabla
mb_nabla of
Maybe Nabla
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Just Nabla
nabla' -> [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns [Id]
xs Int
n Nabla
nabla'
[Nabla]
other_cons_nablas <- Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
instantiate_cons Id
x Type
ty [Id]
xs (Int
n forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [Nabla]
con_nablas) Nabla
nabla [ConLike]
cls
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Nabla]
con_nablas forall a. [a] -> [a] -> [a]
++ [Nabla]
other_cons_nablas)
pickApplicableCompleteSets :: TyState -> Type -> ResidualCompleteMatches -> DsM [CompleteMatch]
pickApplicableCompleteSets :: TyState -> Type -> ResidualCompleteMatches -> DsM [CompleteMatch]
pickApplicableCompleteSets TyState
ty_st Type
ty ResidualCompleteMatches
rcm = do
let cl_res_ty_ok :: ConLike -> DsM Bool
cl_res_ty_ok :: ConLike -> DsM Bool
cl_res_ty_ok ConLike
cl = do
FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe TCvSubst)
matchConLikeResTy FamInstEnvs
env TyState
ty_st Type
ty ConLike
cl
let cm_applicable :: CompleteMatch -> DsM Bool
cm_applicable :: CompleteMatch -> DsM Bool
cm_applicable CompleteMatch
cm = do
Bool
cls_ok <- forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
allM ConLike -> DsM Bool
cl_res_ty_ok (forall a. UniqDSet a -> [a]
uniqDSetToList (CompleteMatch -> UniqDSet ConLike
cmConLikes CompleteMatch
cm))
let match_ty_ok :: Bool
match_ty_ok = Type -> CompleteMatch -> Bool
completeMatchAppliesAtType Type
ty CompleteMatch
cm
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
cls_ok Bool -> Bool -> Bool
&& Bool
match_ty_ok)
[CompleteMatch]
applicable_cms <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM CompleteMatch -> DsM Bool
cm_applicable (ResidualCompleteMatches -> [CompleteMatch]
getRcm ResidualCompleteMatches
rcm)
String -> SDoc -> DsM ()
tracePm String
"pickApplicableCompleteSets:" forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat
[ forall a. Outputable a => a -> SDoc
ppr Type
ty
, forall a. Outputable a => a -> SDoc
ppr ResidualCompleteMatches
rcm
, forall a. Outputable a => a -> SDoc
ppr [CompleteMatch]
applicable_cms
]
forall (m :: * -> *) a. Monad m => a -> m a
return [CompleteMatch]
applicable_cms