summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/deSugar/Check.hs7
-rw-r--r--compiler/deSugar/PmOracle.hs171
-rw-r--r--compiler/deSugar/PmTypes.hs33
-rw-r--r--compiler/types/TyCoRep.hs6
-rw-r--r--compiler/utils/Bag.hs6
5 files changed, 124 insertions, 99 deletions
diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index 4808b56eae..be2fb76bf0 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -51,9 +51,11 @@ import PatSyn
import HscTypes (CompleteMatch(..))
import BasicTypes (Boxity(..))
import Var (EvVar)
-
+import Coercion
+import TcEvidence
import {-# SOURCE #-} DsExpr (dsExpr, dsLExpr)
import MatchLit (dsLit, dsOverLit)
+import IOEnv
import DsMonad
import Bag
import TyCoRep
@@ -66,9 +68,6 @@ import Data.List (find)
import Control.Monad (forM, when, forM_)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Maybe
-import Coercion
-import TcEvidence
-import IOEnv
import qualified Data.Semigroup as Semi
{-
diff --git a/compiler/deSugar/PmOracle.hs b/compiler/deSugar/PmOracle.hs
index b321a8f9d1..ef90d8d2d8 100644
--- a/compiler/deSugar/PmOracle.hs
+++ b/compiler/deSugar/PmOracle.hs
@@ -64,15 +64,16 @@ import TysPrim (tYPETyCon)
import TyCoRep
import Type
import TcSimplify (tcNormalise, tcCheckSatisfiability)
+import TcType (evVarPred)
import Unify (tcMatchTy)
-import TcRnTypes (pprEvVarWithType, completeMatchConLikes)
+import TcRnTypes (completeMatchConLikes)
import Coercion
import MonadUtils hiding (foldlM)
import DsMonad hiding (foldlM)
import FamInst
import FamInstEnv
-import Control.Monad (zipWithM, guard, mzero)
+import Control.Monad (guard, mzero)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State.Strict
import Data.Bifunctor (second)
@@ -147,21 +148,11 @@ getUnmatchedConstructor (PM _tc ms)
---------------------------------------------------
-- * Instantiating constructors, types and evidence
-newEvVar :: Name -> Type -> EvVar
-newEvVar name ty = mkLocalId name ty
-
-nameType :: String -> Type -> DsM EvVar
-nameType name ty = do
- unique <- getUniqueM
- let occname = mkVarOccFS (fsLit (name++"_"++show unique))
- idname = mkInternalName unique occname noSrcSpan
- return (newEvVar idname ty)
-
-- | Instantiate a 'ConLike' given its universal type arguments. Instantiates
-- existential and term binders with fresh variables of appropriate type.
-- Also returns instantiated evidence variables from the match and the types of
-- strict constructor fields.
-mkOneConFull :: [Type] -> ConLike -> DsM ([Id], [EvVar], [Type], [TyVar])
+mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type], [TyVar])
-- * 'con' K is a ConLike
-- - In the case of DataCons and most PatSynCons, these
-- are associated with a particular TyCon T
@@ -197,23 +188,21 @@ mkOneConFull arg_tys con = do
vars <- mapM mkPmId field_tys'
-- All constraints bound by the constructor (alpha-renamed), these are added
-- to the type oracle
- let theta_cs = substTheta subst (eqSpecPreds eq_spec ++ thetas)
- theta_ev_vars <- mapM (nameType "pm") theta_cs
+ let ty_cs = map TyCt (substTheta subst (eqSpecPreds eq_spec ++ thetas))
-- Figure out the types of strict constructor fields
let arg_is_banged = map isBanged $ conLikeImplBangs con
strict_arg_tys = filterByList arg_is_banged field_tys'
- return (vars, theta_ev_vars, strict_arg_tys, ex_tvs')
+ return (vars, listToBag ty_cs, strict_arg_tys, ex_tvs')
-equateTyVars :: [TyVar] -> [TyVar] -> DsM [EvVar]
+equateTyVars :: [TyVar] -> [TyVar] -> Bag TyCt
equateTyVars ex_tvs1 ex_tvs2
= ASSERT(ex_tvs1 `equalLength` ex_tvs2)
- catMaybes <$> zipWithM mb_to_evvar ex_tvs1 ex_tvs2
+ listToBag $ catMaybes $ zipWith mb_to_evvar ex_tvs1 ex_tvs2
where
mb_to_evvar tv1 tv2
- | tv1 == tv2 = pure Nothing
- | otherwise = Just <$> to_evvar tv1 tv2
- to_evvar tv1 tv2 = nameType "pmConCon" $
- mkPrimEqPred (mkTyVarTy tv1) (mkTyVarTy tv2)
+ | tv1 == tv2 = Nothing
+ | otherwise = Just (to_evvar tv1 tv2)
+ to_evvar tv1 tv2 = TyCt $ mkPrimEqPred (mkTyVarTy tv1) (mkTyVarTy tv2)
-------------------------
-- * Pattern match oracle
@@ -287,8 +276,8 @@ instance Monoid SatisfiabilityCheck where
pmIsSatisfiable
:: Delta -- ^ The ambient term and type constraints
-- (known to be satisfiable).
- -> Bag TmCt -- ^ The new term constraints.
- -> Bag EvVar -- ^ The new type constraints.
+ -> Bag TmCt -- ^ The new term constraints.
+ -> Bag TyCt -- ^ The new type constraints.
-> [Type] -- ^ The strict argument types.
-> DsM (Maybe Delta)
-- ^ @'Just' delta@ if the constraints (@delta@) are
@@ -346,7 +335,7 @@ instance Outputable TopNormaliseTypeResult where
, text "newtype_dcs =" <+> ppr ds
, text "core_ty =" <+> ppr core_ty ])
-pmTopNormaliseType :: Bag EvVar -> Type -> DsM TopNormaliseTypeResult
+pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
-- ^ Get rid of *outermost* (or toplevel)
-- * type function redex
-- * data family redex
@@ -362,12 +351,12 @@ pmTopNormaliseType :: Bag EvVar -> Type -> DsM TopNormaliseTypeResult
-- NB: Normalisation can potentially change kinds, if the head of the type
-- is a type family with a variable result kind. I (Richard E) can't think
-- of a way to cause trouble here, though.
-pmTopNormaliseType ty_cs typ
+pmTopNormaliseType (TySt inert) typ
= do env <- dsGetFamInstEnvs
-- Before proceeding, we chuck typ into the constraint solver, in case
-- solving for given equalities may reduce typ some. See
-- "Wrinkle: local equalities" in Note [Type normalisation for EmptyCase].
- (_, mb_typ') <- initTcDsForSolver $ tcNormalise ty_cs typ
+ (_, mb_typ') <- initTcDsForSolver $ tcNormalise inert typ
-- If tcNormalise didn't manage to simplify the type, continue anyway.
-- We might be able to reduce type applications nonetheless!
let typ' = fromMaybe typ mb_typ'
@@ -538,31 +527,51 @@ equalities (such as i ~ Int) that may be in scope.
----------------
-- * Type oracle
+-- | Wraps a 'PredType', which is a constraint type.
+newtype TyCt = TyCt PredType
+
+instance Outputable TyCt where
+ ppr (TyCt pred_ty) = ppr pred_ty
+
+-- | Allocates a fresh 'EvVar' name for 'PredTyCt's, or simply returns the
+-- wrapped 'EvVar' for 'EvVarTyCt's.
+nameTyCt :: TyCt -> DsM EvVar
+nameTyCt (TyCt pred_ty) = do
+ unique <- getUniqueM
+ let occname = mkVarOccFS (fsLit ("pm_"++show unique))
+ idname = mkInternalName unique occname noSrcSpan
+ return (mkLocalId idname pred_ty)
+
-- | Check whether a set of type constraints is satisfiable.
-tyOracle :: Bag EvVar -> DsM Bool
-tyOracle evs
- = do { ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability evs
+tyOracle :: TyState -> Bag TyCt -> DsM (Maybe TyState)
+tyOracle (TySt inert) cts
+ = do { evs <- traverse nameTyCt cts
+ ; let new_inert = inert `unionBags` evs
+ ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability new_inert
; case res of
- Just sat -> return sat
- Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
+ -- Note how this implicitly gives all former PredTyCts a name, so
+ -- that we don't needlessly re-allocate them every time!
+ Just True -> return (Just (TySt new_inert))
+ Just False -> return Nothing
+ Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) }
-- | A 'SatisfiabilityCheck' based on new type-level constraints.
-- Returns a new 'Delta' if the new constraints are compatible with existing
-- ones. Doesn't bother calling out to the type oracle if the bag of new type
-- constraints was empty. Will only recheck 'PossibleMatches' in the term oracle
-- for emptiness if the first argument is 'True'.
-tyIsSatisfiable :: Bool -> Bag EvVar -> SatisfiabilityCheck
+tyIsSatisfiable :: Bool -> Bag TyCt -> SatisfiabilityCheck
tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta -> do
- tracePm "tyIsSatisfiable" (ppr (fmap pprEvVarWithType new_ty_cs))
- let ty_cs = new_ty_cs `unionBags` delta_ty_cs delta
- let delta' = delta{ delta_ty_cs = ty_cs }
+ tracePm "tyIsSatisfiable" (ppr new_ty_cs)
if isEmptyBag new_ty_cs
then pure (Just delta)
- else tyOracle ty_cs >>= \case
- False -> pure Nothing
- True
- | recheck_complete_sets -> ensureAllPossibleMatchesInhabited delta'
- | otherwise -> pure (Just delta')
+ else tyOracle (delta_ty_st delta) new_ty_cs >>= \case
+ Nothing -> pure Nothing
+ Just ty_st' -> do
+ let delta' = delta{ delta_ty_st = ty_st' }
+ if recheck_complete_sets
+ then ensureAllPossibleMatchesInhabited delta'
+ else pure (Just delta')
{- *********************************************************************
@@ -696,13 +705,13 @@ emptyVarInfo x = VI (idType x) [] [] NoPM 0
lookupVarInfo :: TmState -> Id -> VarInfo
-- (lookupVarInfo tms x) tells what we know about 'x'
-lookupVarInfo (TS env) x = fromMaybe (emptyVarInfo x) (lookupSDIE env x)
+lookupVarInfo (TmSt env) x = fromMaybe (emptyVarInfo x) (lookupSDIE env x)
-initPossibleMatches :: Bag EvVar -> VarInfo -> DsM VarInfo
-initPossibleMatches ty_cs vi@VI{ vi_ty = ty, vi_cache = NoPM } = do
+initPossibleMatches :: TyState -> VarInfo -> DsM VarInfo
+initPossibleMatches ty_st vi@VI{ vi_ty = ty, vi_cache = NoPM } = do
-- New evidence might lead to refined info on ty, in turn leading to discovery
-- of a COMPLETE set.
- res <- pmTopNormaliseType ty_cs ty
+ res <- pmTopNormaliseType ty_st ty
let ty' = normalisedSourceType res
mb_pm <- initIM ty'
-- tracePm "initPossibleMatches" (ppr vi $$ ppr ty' $$ ppr res $$ ppr mb_pm)
@@ -715,8 +724,8 @@ initPossibleMatches _ vi = pure vi
-- to initialise the 'vi_cache' component if it was 'NoPM' through
-- 'initPossibleMatches'.
initLookupVarInfo :: Delta -> Id -> DsM VarInfo
-initLookupVarInfo MkDelta{ delta_tm_cs = ts, delta_ty_cs = ty_cs } x
- = initPossibleMatches ty_cs (lookupVarInfo ts x)
+initLookupVarInfo MkDelta{ delta_tm_st = ts, delta_ty_st = ty_st } x
+ = initPossibleMatches ty_st (lookupVarInfo ts x)
------------------------------------------------
-- * Exported utility functions querying 'Delta'
@@ -724,7 +733,7 @@ initLookupVarInfo MkDelta{ delta_tm_cs = ts, delta_ty_cs = ty_cs } x
-- | Check whether a constraint (x ~ BOT) can succeed,
-- given the resulting state of the term oracle.
canDiverge :: Delta -> Id -> Bool
-canDiverge MkDelta{ delta_tm_cs = ts } x
+canDiverge MkDelta{ delta_tm_st = ts } x
-- If the variable seems not evaluated, there is a possibility for
-- constraint x ~ BOT to be satisfiable. That's the case when we haven't found
-- a solution (i.e. some equivalent literal or constructor) for it yet.
@@ -739,7 +748,7 @@ canDiverge MkDelta{ delta_tm_cs = ts } x
lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon]
-- Unfortunately we need the extra bit of polymorphism and the unfortunate
-- duplication of lookupVarInfo here.
-lookupRefuts MkDelta{ delta_tm_cs = ts@(TS (SDIE env)) } k =
+lookupRefuts MkDelta{ delta_tm_st = ts@(TmSt (SDIE env)) } k =
case lookupUDFM env k of
Nothing -> []
Just (Indirect y) -> vi_neg (lookupVarInfo ts y)
@@ -752,7 +761,7 @@ isDataConSolution _ = False
-- @lookupSolution delta x@ picks a single solution ('vi_pos') of @x@ from
-- possibly many, preferring 'RealDataCon' solutions whenever possible.
lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [Id])
-lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_cs delta) x) of
+lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_st delta) x) of
[] -> Nothing
pos
| Just sol <- find isDataConSolution pos -> Just sol
@@ -763,7 +772,7 @@ lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_cs delta) x) of
-- is always less or equal to @length (lookupSolution delta x)@!
lookupNumberOfRefinements :: Delta -> Id -> Int
lookupNumberOfRefinements delta x
- = vi_n_refines (lookupVarInfo (delta_tm_cs delta) x)
+ = vi_n_refines (lookupVarInfo (delta_tm_st delta) x)
-------------------------------
-- * Adding facts to the oracle
@@ -781,7 +790,7 @@ instance Outputable TmCt where
-- | Add type equalities to 'Delta'.
addTypeEvidence :: Delta -> Bag EvVar -> DsM (Maybe Delta)
addTypeEvidence delta dicts
- = runSatisfiabilityCheck delta (tyIsSatisfiable True dicts)
+ = runSatisfiabilityCheck delta (tyIsSatisfiable True (TyCt . evVarPred <$> dicts))
-- | Tries to equate two representatives in 'Delta'.
-- See Note [TmState invariants].
@@ -794,7 +803,7 @@ addTmCt delta ct = runMaybeT $ case ct of
-- 'Delta' and return @Nothing@ if that leads to a contradiction.
-- See Note [TmState invariants].
addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta)
-addRefutableAltCon delta@MkDelta{ delta_tm_cs = TS env } x nalt = runMaybeT $ do
+addRefutableAltCon delta@MkDelta{ delta_tm_st = TmSt env } x nalt = runMaybeT $ do
vi@(VI _ pos neg pm _) <- lift (initLookupVarInfo delta x)
-- 1. Bail out quickly when nalt contradicts a solution
let contradicts nalt (cl, _args) = eqPmAltCon cl nalt == Equal
@@ -813,7 +822,7 @@ addRefutableAltCon delta@MkDelta{ delta_tm_cs = TS env } x nalt = runMaybeT $ do
PmAltConLike cl
-> MaybeT (ensureInhabited delta vi_ext{ vi_cache = markMatched cl pm })
_ -> pure vi_ext
- pure delta{ delta_tm_cs = TS (setEntrySDIE env x vi') }
+ pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi') }
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta (PmAltConLike cl) = notNull req_theta
@@ -915,13 +924,13 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo
case guessConLikeUnivTyArgsFromResTy env (vi_ty vi) con of
Nothing -> pure True -- be conservative about this
Just arg_tys -> do
- (_vars, ev_vars, strict_arg_tys, _ex_tyvars) <- mkOneConFull arg_tys con
+ (_vars, ty_cs, strict_arg_tys, _ex_tyvars) <- mkOneConFull arg_tys con
-- No need to run the term oracle compared to pmIsSatisfiable
fmap isJust <$> runSatisfiabilityCheck delta $ mconcat
-- Important to pass False to tyIsSatisfiable here, so that we won't
-- recursively call ensureAllPossibleMatchesInhabited, leading to an
-- endless recursion.
- [ tyIsSatisfiable False (listToBag ev_vars)
+ [ tyIsSatisfiable False ty_cs
, tysAreNonVoid initRecTc strict_arg_tys
]
@@ -930,10 +939,10 @@ ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This wo
-- This check is necessary after having matched on a GADT con to weed out
-- impossible matches.
ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta)
-ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_cs = TS env }
+ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_st = TmSt env }
= runMaybeT (set_tm_cs_env delta <$> traverseSDIE go env)
where
- set_tm_cs_env delta env = delta{ delta_tm_cs = TS env }
+ set_tm_cs_env delta env = delta{ delta_tm_st = TmSt env }
go vi = MaybeT (ensureInhabited delta vi)
-- | @refineToAltCon delta x con arg_tys ex_tyvars@ instantiates @con@ at
@@ -957,15 +966,15 @@ refineToAltCon delta x alt@(PmAltConLike con) arg_tys ex_tvs1 = do
-- [ex1, ex2].
-- Return Nothing if such a match is contradictory with delta.
- (arg_vars, theta_ev_vars, strict_arg_tys, ex_tvs2) <- mkOneConFull arg_tys con
+ (arg_vars, theta_ty_cs, strict_arg_tys, ex_tvs2) <- mkOneConFull arg_tys con
-- If we have identical constructors but different existential
-- tyvars, then generate extra equality constraints to ensure the
-- existential tyvars.
-- See Note [Coverage checking and existential tyvars].
- ex_ev_vars <- equateTyVars ex_tvs1 ex_tvs2
+ let ex_ty_cs = equateTyVars ex_tvs1 ex_tvs2
- let new_ty_cs = listToBag theta_ev_vars `unionBags` listToBag ex_ev_vars
+ let new_ty_cs = theta_ty_cs `unionBags` ex_ty_cs
let new_tm_cs = unitBag (TmVarCon x alt arg_vars)
-- Now check satifiability
@@ -982,8 +991,8 @@ refineToAltCon delta x alt@(PmAltConLike con) arg_tys ex_tvs1 = do
-- | This is the only place that actualy increments 'vi_n_refines'.
markRefined :: Delta -> Id -> Delta
-markRefined delta@MkDelta{ delta_tm_cs = ts@(TS env) } x
- = delta{ delta_tm_cs = TS env' }
+markRefined delta@MkDelta{ delta_tm_st = ts@(TmSt env) } x
+ = delta{ delta_tm_st = TmSt env' }
where
vi = lookupVarInfo ts x
env' = setEntrySDIE env x vi{ vi_n_refines = vi_n_refines vi + 1 }
@@ -1114,7 +1123,7 @@ arises in the first place!
--
-- See Note [TmState invariants].
addVarVarCt :: Delta -> (Id, Id) -> MaybeT DsM Delta
-addVarVarCt delta@MkDelta{ delta_tm_cs = TS env } (x, y)
+addVarVarCt delta@MkDelta{ delta_tm_st = TmSt env } (x, y)
-- It's important that we never @equate@ two variables of the same equivalence
-- class, otherwise we might get cyclic substitutions.
-- Cf. 'extendSubstAndSolve' and
@@ -1122,7 +1131,7 @@ addVarVarCt delta@MkDelta{ delta_tm_cs = TS env } (x, y)
| sameRepresentativeSDIE env x y = pure delta
| otherwise = equate delta x y
--- | @equate ts@(TS env) x y@ merges the equivalence classes of @x@ and @y@ by
+-- | @equate ts@(TmSt env) x y@ merges the equivalence classes of @x@ and @y@ by
-- adding an indirection to the environment.
-- Makes sure that the positive and negative facts of @x@ and @y@ are
-- compatible.
@@ -1130,11 +1139,11 @@ addVarVarCt delta@MkDelta{ delta_tm_cs = TS env } (x, y)
--
-- See Note [TmState invariants].
equate :: Delta -> Id -> Id -> MaybeT DsM Delta
-equate delta@MkDelta{ delta_tm_cs = TS env } x y
+equate delta@MkDelta{ delta_tm_st = TmSt env } x y
= ASSERT( not (sameRepresentativeSDIE env x y) )
case (lookupSDIE env x, lookupSDIE env y) of
- (Nothing, _) -> pure (delta{ delta_tm_cs = TS (setIndirectSDIE env x y) })
- (_, Nothing) -> pure (delta{ delta_tm_cs = TS (setIndirectSDIE env y x) })
+ (Nothing, _) -> pure (delta{ delta_tm_st = TmSt (setIndirectSDIE env x y) })
+ (_, Nothing) -> pure (delta{ delta_tm_st = TmSt (setIndirectSDIE env y x) })
-- Merge the info we have for x into the info for y
(Just vi_x, Just vi_y) -> do
-- This assert will probably trigger at some point...
@@ -1145,7 +1154,7 @@ equate delta@MkDelta{ delta_tm_cs = TS env } x y
-- Then sum up the refinement counters
let vi_y' = vi_y{ vi_n_refines = vi_n_refines vi_x + vi_n_refines vi_y }
let env_refs = setEntrySDIE env_ind y vi_y'
- let delta_refs = delta{ delta_tm_cs = TS env_refs }
+ let delta_refs = delta{ delta_tm_st = TmSt env_refs }
-- and then gradually merge every positive fact we have on x into y
let add_fact delta (cl, args) = addVarConCt delta y cl args
delta_pos <- foldlM add_fact delta_refs (vi_pos vi_x)
@@ -1162,7 +1171,7 @@ equate delta@MkDelta{ delta_tm_cs = TS env } x y
--
-- See Note [TmState invariants].
addVarConCt :: Delta -> Id -> PmAltCon -> [Id] -> MaybeT DsM Delta
-addVarConCt delta@MkDelta{ delta_tm_cs = TS env } x alt args = do
+addVarConCt delta@MkDelta{ delta_tm_st = TmSt env } x alt args = do
VI ty pos neg cache n <- lift (initLookupVarInfo delta x)
-- First try to refute with a negative fact
guard (all ((/= Equal) . eqPmAltCon alt) neg)
@@ -1180,7 +1189,7 @@ addVarConCt delta@MkDelta{ delta_tm_cs = TS env } x alt args = do
-- the new solution)
let neg' = filter ((== PossiblyOverlap) . eqPmAltCon alt) neg
let pos' = (alt,args):pos
- pure delta{ delta_tm_cs = TS (setEntrySDIE env x (VI ty pos' neg' cache n))}
+ pure delta{ delta_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg' cache n))}
----------------------------------------
-- * Enumerating inhabitation candidates
@@ -1194,7 +1203,7 @@ addVarConCt delta@MkDelta{ delta_tm_cs = TS env } x alt args = do
data InhabitationCandidate =
InhabitationCandidate
{ ic_tm_cs :: Bag TmCt
- , ic_ty_cs :: Bag EvVar
+ , ic_ty_cs :: Bag TyCt
, ic_strict_arg_tys :: [Type]
}
@@ -1210,10 +1219,10 @@ mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate
mkInhabitationCandidate x dc = do
let cl = RealDataCon dc
let tc_args = tyConAppArgs (idType x)
- (arg_vars, ev_vars, strict_arg_tys, _ex_tyvars) <- mkOneConFull tc_args cl
+ (arg_vars, ty_cs, strict_arg_tys, _ex_tyvars) <- mkOneConFull tc_args cl
pure InhabitationCandidate
{ ic_tm_cs = unitBag (TmVarCon x (PmAltConLike cl) arg_vars)
- , ic_ty_cs = listToBag ev_vars
+ , ic_ty_cs = ty_cs
, ic_strict_arg_tys = strict_arg_tys
}
@@ -1225,8 +1234,8 @@ mkInhabitationCandidate x dc = do
-- See also Note [Checking EmptyCase Expressions]
inhabitationCandidates :: Delta -> Type
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
-inhabitationCandidates MkDelta{ delta_ty_cs = ty_cs } ty = do
- pmTopNormaliseType ty_cs ty >>= \case
+inhabitationCandidates MkDelta{ delta_ty_st = ty_st } ty = do
+ pmTopNormaliseType ty_st ty >>= \case
NoChange _ -> alts_to_check ty ty []
NormalisedByConstraints ty' -> alts_to_check ty' ty' []
HadRedexes src_ty dcs core_ty -> alts_to_check src_ty core_ty dcs
@@ -1338,7 +1347,7 @@ tysAreNonVoid rec_env strict_arg_tys = SC $ \delta -> do
-- @Note [Strict argument type constraints]@.
checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> DsM Bool
checkAllNonVoid rec_ts amb_cs strict_arg_tys = do
- let definitely_inhabited = definitelyInhabitedType (delta_ty_cs amb_cs)
+ let definitely_inhabited = definitelyInhabitedType (delta_ty_st amb_cs)
tys_to_check <- filterOutM definitely_inhabited strict_arg_tys
let rec_max_bound | tys_to_check `lengthExceeds` 1
= 1
@@ -1398,9 +1407,9 @@ nonVoid rec_ts amb_cs strict_arg_ty = do
-- 2. @C@ has no strict argument types.
--
-- See the @Note [Strict argument type constraints]@.
-definitelyInhabitedType :: Bag EvVar -> Type -> DsM Bool
-definitelyInhabitedType ty_cs ty = do
- res <- pmTopNormaliseType ty_cs ty
+definitelyInhabitedType :: TyState -> Type -> DsM Bool
+definitelyInhabitedType ty_st ty = do
+ res <- pmTopNormaliseType ty_st ty
pure $ case res of
HadRedexes _ cons _ -> any meets_criteria cons
_ -> False
@@ -1610,7 +1619,7 @@ provideEvidenceForEquation = go init_ts
let (_,ex_tvs,_,_,_,_,_) = conLikeFullSig cl
-- we might need to freshen ex_tvs. Not sure
-- We may need to reduce type famlies/synonyms in x's type first
- res <- pmTopNormaliseType (delta_ty_cs delta) (idType x)
+ res <- pmTopNormaliseType (delta_ty_st delta) (idType x)
let res_ty = normalisedSourceType res
env <- dsGetFamInstEnvs
case guessConLikeUnivTyArgsFromResTy env res_ty cl of
diff --git a/compiler/deSugar/PmTypes.hs b/compiler/deSugar/PmTypes.hs
index fc97f636a7..0e0f91839d 100644
--- a/compiler/deSugar/PmTypes.hs
+++ b/compiler/deSugar/PmTypes.hs
@@ -29,7 +29,7 @@ module PmTypes (
setIndirectSDIE, setEntrySDIE, traverseSDIE,
-- * The pattern match oracle
- VarInfo(..), TmState(..), Delta(..), initDelta,
+ VarInfo(..), TmState(..), TyState(..), Delta(..), initDelta
) where
#include "HsVersions.h"
@@ -57,7 +57,7 @@ import CoreUtils (exprType)
import PrelNames
import TysWiredIn
import TysPrim
-import TcRnTypes (pprEvVarWithType)
+import TcType (evVarPred)
import Numeric (fromRat)
import Data.Foldable (find)
@@ -441,7 +441,7 @@ instance Outputable a => Outputable (SharedDIdEnv a) where
-- equal, thus represent the same set of values.
--
-- See Note [TmState invariants].
-newtype TmState = TS (SharedDIdEnv VarInfo)
+newtype TmState = TmSt (SharedDIdEnv VarInfo)
-- Deterministic so that we generate deterministic error messages
-- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
@@ -498,7 +498,7 @@ data VarInfo
-- | Not user-facing.
instance Outputable TmState where
- ppr (TS state) = ppr state
+ ppr (TmSt state) = ppr state
-- | Not user-facing.
instance Outputable VarInfo where
@@ -507,23 +507,34 @@ instance Outputable VarInfo where
-- | Initial state of the oracle.
initTmState :: TmState
-initTmState = TS emptySDIE
+initTmState = TmSt emptySDIE
+
+-- | The type oracle state. A poor man's inert set: The invariant is that all
+-- constraints in there are mutually compatible.
+newtype TyState = TySt (Bag EvVar)
+
+-- | Not user-facing.
+instance Outputable TyState where
+ ppr (TySt evs)
+ = braces $ hcat $ punctuate comma $ map (ppr . evVarPred) $ bagToList evs
+
+initTyState :: TyState
+initTyState = TySt emptyBag
-- | Term and type constraints to accompany each value vector abstraction.
-- For efficiency, we store the term oracle state instead of the term
-- constraints.
-data Delta = MkDelta { delta_ty_cs :: Bag EvVar -- Type oracle; things like a~Int
- , delta_tm_cs :: TmState } -- Term oracle; things like x~Nothing
+data Delta = MkDelta { delta_ty_st :: TyState -- Type oracle; things like a~Int
+ , delta_tm_st :: TmState } -- Term oracle; things like x~Nothing
-- | An initial delta that is always satisfiable
initDelta :: Delta
-initDelta = MkDelta emptyBag initTmState
+initDelta = MkDelta initTyState initTmState
instance Outputable Delta where
ppr delta = vcat [
-- intentionally formatted this way enable the dev to comment in only
-- the info she needs
- ppr (delta_tm_cs delta),
- ppr (pprEvVarWithType <$> delta_ty_cs delta)
- --ppr (delta_ty_cs delta)
+ ppr (delta_tm_st delta),
+ ppr (delta_ty_st delta)
]
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 51ad630372..065efcd417 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -860,12 +860,12 @@ see Note [Required quantifiers in the type of a term] in TcExpr.
********************************************************************** -}
--- | A type of the form @p@ of kind @Constraint@ represents a value whose type is
+-- | A type of the form @p@ of constraint kind represents a value whose type is
-- the Haskell predicate @p@, where a predicate is what occurs before
-- the @=>@ in a Haskell type.
--
--- We use 'PredType' as documentation to mark those types that we guarantee to have
--- this kind.
+-- We use 'PredType' as documentation to mark those types that we guarantee to
+-- have this kind.
--
-- It can be expanded into its representation, but:
--
diff --git a/compiler/utils/Bag.hs b/compiler/utils/Bag.hs
index be46640920..e1eea48000 100644
--- a/compiler/utils/Bag.hs
+++ b/compiler/utils/Bag.hs
@@ -327,3 +327,9 @@ instance Foldable.Foldable Bag where
foldl' k z (UnitBag x) = k z x
foldl' k z (TwoBags b1 b2) = let r1 = foldl' k z b1 in seq r1 $ foldl' k r1 b2
foldl' k z (ListBag xs) = foldl' k z xs
+
+instance Traversable Bag where
+ traverse _ EmptyBag = pure EmptyBag
+ traverse f (UnitBag x) = UnitBag <$> f x
+ traverse f (TwoBags b1 b2) = TwoBags <$> traverse f b1 <*> traverse f b2
+ traverse f (ListBag xs) = ListBag <$> traverse f xs
View Lorry Controller Status