Commit fffe3a25 authored by niteria's avatar niteria

Make inert_model and inert_eqs deterministic sets

The order inert_model and intert_eqs fold affects the order that the
typechecker looks at things. I've been able to experimentally confirm
that the order of equalities and the order of the model matter for
determinism. This is just a straigthforward replacement of
nondeterministic VarEnv for deterministic DVarEnv.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari, simonmar

Reviewed By: simonmar

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2232

GHC Trac Issues: #4012
parent 77ee3a92
......@@ -24,20 +24,23 @@ module VarEnv (
partitionVarEnv,
-- * Deterministic Var environments (maps)
DVarEnv, DIdEnv,
DVarEnv, DIdEnv, DTyVarEnv,
-- ** Manipulating these environments
emptyDVarEnv,
dVarEnvElts,
extendDVarEnv,
extendDVarEnv, extendDVarEnv_C,
lookupDVarEnv,
foldDVarEnv,
isEmptyDVarEnv, foldDVarEnv,
mapDVarEnv,
modifyDVarEnv,
alterDVarEnv,
plusDVarEnv_C,
unitDVarEnv,
delDVarEnv,
delDVarEnvList,
partitionDVarEnv,
anyDVarEnv,
-- * The InScopeSet type
InScopeSet,
......@@ -510,6 +513,7 @@ modifyVarEnv_Directly mangle_fn env key
type DVarEnv elt = UniqDFM elt
type DIdEnv elt = DVarEnv elt
type DTyVarEnv elt = DVarEnv elt
emptyDVarEnv :: DVarEnv a
emptyDVarEnv = emptyUDFM
......@@ -543,3 +547,21 @@ delDVarEnv = delFromUDFM
delDVarEnvList :: DVarEnv a -> [Var] -> DVarEnv a
delDVarEnvList = delListFromUDFM
isEmptyDVarEnv :: DVarEnv a -> Bool
isEmptyDVarEnv = isNullUDFM
extendDVarEnv_C :: (a -> a -> a) -> DVarEnv a -> Var -> a -> DVarEnv a
extendDVarEnv_C = addToUDFM_C
modifyDVarEnv :: (a -> a) -> DVarEnv a -> Var -> DVarEnv a
modifyDVarEnv mangle_fn env key
= case (lookupDVarEnv env key) of
Nothing -> env
Just xx -> extendDVarEnv env key (mangle_fn xx)
partitionDVarEnv :: (a -> Bool) -> DVarEnv a -> (DVarEnv a, DVarEnv a)
partitionDVarEnv = partitionUDFM
anyDVarEnv :: (a -> Bool) -> DVarEnv a -> Bool
anyDVarEnv = anyUDFM
......@@ -1324,7 +1324,7 @@ flatten_tyvar2 :: TcTyVar -> CtFlavourRole -> FlatM FlattenTvResult
flatten_tyvar2 tv fr@(flavour, eq_rel)
| Derived <- flavour -- For derived equalities, consult the inert_model (only)
= do { model <- liftTcS $ getInertModel
; case lookupVarEnv model tv of
; case lookupDVarEnv model tv of
Just (CTyEqCan { cc_rhs = rhs })
-> return (FTRFollowed rhs (pprPanic "flatten_tyvar2" (ppr tv $$ ppr rhs)))
-- Evidence is irrelevant for Derived contexts
......@@ -1332,7 +1332,7 @@ flatten_tyvar2 tv fr@(flavour, eq_rel)
| otherwise -- For non-derived equalities, consult the inert_eqs (only)
= do { ieqs <- liftTcS $ getInertEqs
; case lookupVarEnv ieqs tv of
; case lookupDVarEnv ieqs tv of
Just (ct:_) -- If the first doesn't work,
-- the subsequent ones won't either
| CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
......
......@@ -926,7 +926,7 @@ improveLocalFunEqs loc inerts fam_tc args fsk
lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType
-- See Note [lookupFlattenTyVar]
lookupFlattenTyVar model ftv
= case lookupVarEnv model ftv of
= case lookupDVarEnv model ftv of
Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs
_ -> mkTyVarTy ftv
......
......@@ -376,13 +376,13 @@ instance Outputable InertSet where
emptyInert :: InertSet
emptyInert
= IS { inert_cans = IC { inert_count = 0
, inert_eqs = emptyVarEnv
, inert_eqs = emptyDVarEnv
, inert_dicts = emptyDicts
, inert_safehask = emptyDicts
, inert_funeqs = emptyFunEqs
, inert_irreds = emptyCts
, inert_insols = emptyCts
, inert_model = emptyVarEnv }
, inert_model = emptyDVarEnv }
, inert_flat_cache = emptyExactFunEqs
, inert_solved_dicts = emptyDictMap }
......@@ -558,7 +558,7 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more
= IC { inert_model :: InertModel
-- See Note [inert_model: the inert model]
, inert_eqs :: TyVarEnv EqualCtList
, inert_eqs :: DTyVarEnv EqualCtList
-- See Note [inert_eqs: the inert equalities]
-- All Given/Wanted CTyEqCans; index is the LHS tyvar
......@@ -598,7 +598,7 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more
-- When non-zero, keep trying to solved
}
type InertModel = TyVarEnv Ct
type InertModel = DTyVarEnv Ct
-- If a -> ct, then ct is a
-- nominal, Derived, canonical CTyEqCan for [D] (a ~N rhs)
-- The index of the TyVarEnv is the 'a'
......@@ -1073,9 +1073,9 @@ instance Outputable InertCans where
, inert_safehask = safehask, inert_irreds = irreds
, inert_insols = insols, inert_count = count })
= braces $ vcat
[ ppUnless (isEmptyVarEnv eqs) $
[ ppUnless (isEmptyDVarEnv eqs) $
text "Equalities:"
<+> pprCts (foldVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
<+> pprCts (foldDVarEnv (\eqs rest -> listToBag eqs `andCts` rest) emptyCts eqs)
, ppUnless (isEmptyTcAppMap funeqs) $
text "Type-function equalities =" <+> pprCts (funEqsToBag funeqs)
, ppUnless (isEmptyTcAppMap dicts) $
......@@ -1086,8 +1086,8 @@ instance Outputable InertCans where
text "Irreds =" <+> pprCts irreds
, ppUnless (isEmptyCts insols) $
text "Insolubles =" <+> pprCts insols
, ppUnless (isEmptyVarEnv model) $
text "Model =" <+> pprCts (foldVarEnv consCts emptyCts model)
, ppUnless (isEmptyDVarEnv model) $
text "Model =" <+> pprCts (foldDVarEnv consCts emptyCts model)
, text "Unsolved goals =" <+> int count
]
......@@ -1223,7 +1223,7 @@ add_inert_eq ics@(IC { inert_count = n
| isDerived ev
= do { emitDerivedShadows ics tv
; return (ics { inert_model = extendVarEnv old_model tv ct }) }
; return (ics { inert_model = extendDVarEnv old_model tv ct }) }
| otherwise -- Given/Wanted Nominal equality [W] tv ~N ty
= do { emitNewDerived loc pred
......@@ -1311,7 +1311,7 @@ See Trac #11379 for a case of this.
modelCanRewrite :: InertModel -> TcTyCoVarSet -> Bool
-- See Note [Emitting shadow constraints]
-- True if there is any intersection between dom(model) and tvs
modelCanRewrite model tvs = not (disjointUFM model tvs)
modelCanRewrite model tvs = not (disjointUdfmUfm model tvs)
-- The low-level use of disjointUFM might e surprising.
-- InertModel = TyVarEnv Ct, and we want to see if its domain
-- is disjoint from that of a TcTyCoVarSet. So we drop down
......@@ -1409,7 +1409,7 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs
`andCts` insols_out)
, wl_implics = emptyBag }
(tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
(tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs
(feqs_out, feqs_in) = partitionFunEqs kick_out_fe funeqmap
(dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
(irs_out, irs_in) = partitionBag kick_out_ct irreds
......@@ -1436,12 +1436,12 @@ kickOutRewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs
&& new_tv `elemVarSet` tyCoVarsOfTypes tys)
kick_out_fe ct = pprPanic "kick_out_fe" (ppr ct)
kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList)
-> ([Ct], TyVarEnv EqualCtList)
kick_out_eqs :: EqualCtList -> ([Ct], DTyVarEnv EqualCtList)
-> ([Ct], DTyVarEnv EqualCtList)
kick_out_eqs eqs (acc_out, acc_in)
= (eqs_out ++ acc_out, case eqs_in of
[] -> acc_in
(eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
(eq1:_) -> extendDVarEnv acc_in (cc_tyvar eq1) eqs_in)
where
(eqs_in, eqs_out) = partition keep_eq eqs
......@@ -1493,9 +1493,9 @@ kickOutAfterUnification new_tv
kickOutModel :: TcTyVar -> InertCans -> (WorkList, InertCans)
kickOutModel new_tv ics@(IC { inert_model = model, inert_eqs = eqs })
= (foldVarEnv add emptyWorkList der_out, ics { inert_model = new_model })
= (foldDVarEnv add emptyWorkList der_out, ics { inert_model = new_model })
where
(der_out, new_model) = partitionVarEnv kick_out_der model
(der_out, new_model) = partitionDVarEnv kick_out_der model
kick_out_der :: Ct -> Bool
kick_out_der (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs })
......@@ -1669,7 +1669,7 @@ updInertIrreds :: (Cts -> Cts) -> TcS ()
updInertIrreds upd_fn
= updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
getInertEqs :: TcS (TyVarEnv EqualCtList)
getInertEqs :: TcS (DTyVarEnv EqualCtList)
getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) }
getInertModel :: TcS InertModel
......@@ -1682,7 +1682,7 @@ getInertGivens
= do { inerts <- getInertCans
; let all_cts = foldDicts (:) (inert_dicts inerts)
$ foldFunEqs (:) (inert_funeqs inerts)
$ concat (varEnvElts (inert_eqs inerts))
$ concat (dVarEnvElts (inert_eqs inerts))
; return (filter isGivenCt all_cts) }
getPendingScDicts :: TcS [Ct]
......@@ -1728,7 +1728,7 @@ getUnsolvedInerts
, inert_model = model } <- getInertCans
; keep_derived <- keepSolvingDeriveds
; let der_tv_eqs = foldVarEnv (add_der_eq keep_derived tv_eqs)
; let der_tv_eqs = foldDVarEnv (add_der_eq keep_derived tv_eqs)
emptyCts model
unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs der_tv_eqs
unsolved_fun_eqs = foldFunEqs add_if_unsolved fun_eqs emptyCts
......@@ -1761,10 +1761,10 @@ getUnsolvedInerts
is_unsolved ct = not (isGivenCt ct) -- Wanted or Derived
isInInertEqs :: TyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool
isInInertEqs :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> Bool
-- True if (a ~N ty) is in the inert set, in either Given or Wanted
isInInertEqs eqs tv rhs
= case lookupVarEnv eqs tv of
= case lookupDVarEnv eqs tv of
Nothing -> False
Just cts -> any (same_pred rhs) cts
where
......@@ -1784,7 +1784,7 @@ getNoGivenEqs tclvl skol_tvs
; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False iirreds
|| foldVarEnv ((||) . eqs_given_here local_fsks) False ieqs
|| anyDVarEnv (eqs_given_here local_fsks) ieqs
; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
; return (not has_given_eqs) }
......@@ -2039,19 +2039,19 @@ type EqualCtList = [Ct]
- Any number of Wanteds and/or Deriveds
-}
addTyEq :: TyVarEnv EqualCtList -> TcTyVar -> Ct -> TyVarEnv EqualCtList
addTyEq old_list tv it = extendVarEnv_C (\old_eqs _new_eqs -> it : old_eqs)
addTyEq :: DTyVarEnv EqualCtList -> TcTyVar -> Ct -> DTyVarEnv EqualCtList
addTyEq old_list tv it = extendDVarEnv_C (\old_eqs _new_eqs -> it : old_eqs)
old_list tv [it]
foldTyEqs :: (Ct -> b -> b) -> TyVarEnv EqualCtList -> b -> b
foldTyEqs :: (Ct -> b -> b) -> DTyVarEnv EqualCtList -> b -> b
foldTyEqs k eqs z
= foldVarEnv (\cts z -> foldr k z cts) z eqs
= foldDVarEnv (\cts z -> foldr k z cts) z eqs
findTyEqs :: InertCans -> TyVar -> EqualCtList
findTyEqs icans tv = lookupVarEnv (inert_eqs icans) tv `orElse` []
findTyEqs icans tv = lookupDVarEnv (inert_eqs icans) tv `orElse` []
delTyEq :: TyVarEnv EqualCtList -> TcTyVar -> TcType -> TyVarEnv EqualCtList
delTyEq m tv t = modifyVarEnv (filter (not . isThisOne)) m tv
delTyEq :: DTyVarEnv EqualCtList -> TcTyVar -> TcType -> DTyVarEnv EqualCtList
delTyEq m tv t = modifyDVarEnv (filter (not . isThisOne)) m tv
where isThisOne (CTyEqCan { cc_rhs = t1 }) = eqType t t1
isThisOne _ = False
......
......@@ -27,6 +27,7 @@ module UniqDFM (
emptyUDFM,
unitUDFM,
addToUDFM,
addToUDFM_C,
delFromUDFM,
delListFromUDFM,
adjustUDFM,
......@@ -43,10 +44,11 @@ module UniqDFM (
sizeUDFM,
intersectUDFM,
intersectsUDFM,
disjointUDFM,
disjointUDFM, disjointUdfmUfm,
minusUDFM,
udfmMinusUFM,
partitionUDFM,
anyUDFM,
udfmToList,
udfmToUfm,
......@@ -153,6 +155,18 @@ addToUDFM_Directly_C f (UDFM m i) u v =
where
tf (TaggedVal a j) (TaggedVal b _) = TaggedVal (f a b) j
addToUDFM_C
:: Uniquable key => (elt -> elt -> elt) -- old -> new -> result
-> UniqDFM elt -- old
-> key -> elt -- new
-> UniqDFM elt -- result
addToUDFM_C f (UDFM m i) k v =
UDFM (M.insertWith tf (getKey $ getUnique k) (TaggedVal v i) m) (i + 1)
where
tf (TaggedVal a j) (TaggedVal b _) = TaggedVal (f b a) j
-- Flip the arguments, just like
-- addToUFM_C does.
addListToUDFM_Directly :: UniqDFM elt -> [(Unique,elt)] -> UniqDFM elt
addListToUDFM_Directly = foldl (\m (k, v) -> addToUDFM_Directly m k v)
......@@ -267,6 +281,9 @@ intersectsUDFM x y = isNullUDFM (x `intersectUDFM` y)
disjointUDFM :: UniqDFM elt -> UniqDFM elt -> Bool
disjointUDFM (UDFM x _i) (UDFM y _j) = M.null (M.intersection x y)
disjointUdfmUfm :: UniqDFM elt -> UniqFM elt2 -> Bool
disjointUdfmUfm (UDFM x _i) y = M.null (M.intersection x (ufmToIntMap y))
minusUDFM :: UniqDFM elt1 -> UniqDFM elt2 -> UniqDFM elt1
minusUDFM (UDFM x i) (UDFM y _j) = UDFM (M.difference x y) i
-- M.difference returns a subset of a left set, so `i` is a good upper
......@@ -321,6 +338,9 @@ alterUDFM f (UDFM m i) k =
mapUDFM :: (elt1 -> elt2) -> UniqDFM elt1 -> UniqDFM elt2
mapUDFM f (UDFM m i) = UDFM (M.map (fmap f) m) i
anyUDFM :: (elt -> Bool) -> UniqDFM elt -> Bool
anyUDFM p (UDFM m _i) = M.fold ((||) . p . taggedFst) False m
instance Monoid (UniqDFM a) where
mempty = emptyUDFM
mappend = plusUDFM
......
T3330a.hs:19:34: error:
• Couldn't match type ‘s’ with ‘(->) (s0 ix0 -> ix1)’
‘s’ is a rigid type variable bound by
• Couldn't match type ‘ix’
with ‘r ix1 -> Writer [AnyF s] (r'0 ix1)’
‘ix’ is a rigid type variable bound by
the type signature for:
children :: forall (s :: * -> *) ix (r :: * -> *).
s ix -> PF s r ix -> [AnyF s]
......
T4174.hs:42:12: error:
• Couldn't match type ‘a’ with ‘SmStep
a’ is a rigid type variable bound by
• Couldn't match type ‘b’ with ‘RtsSpinLock
b’ is a rigid type variable bound by
the type signature for:
testcase :: forall (m :: * -> *) minor n t p a b.
Monad m =>
......
T4179.hs:26:16: error:
• Couldn't match type ‘A2 (x (A2 (FCon x) -> A3 (FCon x)))’
with ‘A2 (FCon x)’
• Couldn't match type ‘A3 (x (A2 (FCon x) -> A3 (FCon x)))’
with ‘A3 (FCon x)’
Expected type: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (FCon x) -> A3 (FCon x)
Actual type: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (x (A2 (FCon x) -> A3 (FCon x)))
-> A3 (x (A2 (FCon x) -> A3 (FCon x)))
NB: ‘A2’ is a type function, and may not be injective
NB: ‘A3’ is a type function, and may not be injective
• In the first argument of ‘foldDoC’, namely ‘op’
In the expression: foldDoC op
In an equation for ‘fCon’: fCon = foldDoC op
......
T9662.hs:47:8: error:
• Couldn't match type ‘k’ with ‘Int’
k’ is a rigid type variable bound by
• Couldn't match type ‘n’ with ‘Int’
n’ is a rigid type variable bound by
the type signature for:
test :: forall sh k m n.
Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
......
T9017.hs:8:7: error:
• Couldn't match kind ‘k’ with ‘*’
‘k’ is a rigid type variable bound by
• Couldn't match kind ‘k1’ with ‘*’
‘k1’ is a rigid type variable bound by
the type signature for:
foo :: forall k k1 (a :: k1 -> k -> *) (b :: k1) (m :: k1 -> k).
a b (m b)
......
T7869.hs:3:12: error:
• Couldn't match type ‘a’ with ‘a1’
because type variable ‘a1’ would escape its scope
• Couldn't match type ‘b’ with ‘b1’
because type variable ‘b1’ would escape its scope
This (rigid, skolem) type variable is bound by
an expression type signature:
[a1] -> b1
......@@ -11,6 +11,4 @@ T7869.hs:3:12: error:
• In the expression: f x
In the expression: (\ x -> f x) :: [a] -> b
In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b
• Relevant bindings include
x :: [a1] (bound at T7869.hs:3:7)
f :: [a] -> b (bound at T7869.hs:3:1)
• Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment