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

5 files changed, 78 insertions, 36 deletions

diff --git a/compiler/basicTypes/VarEnv.hs b/compiler/basicTypes/VarEnv.hs
index c591ee452c..906434fddd 100644
--- a/compiler/basicTypes/VarEnv.hs
+++ b/compiler/basicTypes/VarEnv.hs
@@ -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
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 6bac122a32..5005abc04b 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -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
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 6205844c7d..8cd606613c 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -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
 
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 606e3c19e8..73541399f8 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -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
 
diff --git a/compiler/utils/UniqDFM.hs b/compiler/utils/UniqDFM.hs
index 9dfefa4bdb..4bd97ef2eb 100644
--- a/compiler/utils/UniqDFM.hs
+++ b/compiler/utils/UniqDFM.hs
@@ -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