Make inert_model and inert_eqs deterministic sets
authorBartosz Nitka <niteria@gmail.com>
Tue, 17 May 2016 12:45:43 +0000 (05:45 -0700)
committerBartosz Nitka <niteria@gmail.com>
Mon, 25 Jul 2016 14:38:55 +0000 (07:38 -0700)
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

(cherry picked from commit fffe3a25adab41d44943ed1be0191cf570d3e154)

compiler/basicTypes/VarEnv.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcSMonad.hs
compiler/utils/UniqDFM.hs
testsuite/tests/indexed-types/should_fail/T3330a.stderr
testsuite/tests/indexed-types/should_fail/T4174.stderr
testsuite/tests/indexed-types/should_fail/T4179.stderr
testsuite/tests/indexed-types/should_fail/T9662.stderr
testsuite/tests/polykinds/T9017.stderr
testsuite/tests/typecheck/should_fail/T7869.stderr

index f06b736..27343d0 100644 (file)
@@ -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,
@@ -507,6 +510,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
@@ -540,3 +544,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
index 76eda37..ec0d838 100644 (file)
@@ -1312,7 +1312,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
@@ -1320,7 +1320,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
index ca5d912..398f21d 100644 (file)
@@ -923,7 +923,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
 
index 4387ab3..27b929f 100644 (file)
@@ -369,13 +369,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 }
 
@@ -551,7 +551,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
 
@@ -591,7 +591,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'
@@ -1066,9 +1066,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) $
@@ -1079,8 +1079,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
       ]
 
@@ -1216,7 +1216,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
@@ -1304,7 +1304,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
@@ -1402,7 +1402,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
@@ -1429,12 +1429,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
 
@@ -1486,9 +1486,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 })
@@ -1662,7 +1662,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
@@ -1675,7 +1675,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]
@@ -1721,7 +1721,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
@@ -1754,10 +1754,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
@@ -1777,7 +1777,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) }
@@ -2032,19 +2032,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
 
index e70b983..1da108e 100644 (file)
@@ -28,6 +28,7 @@ module UniqDFM (
         emptyUDFM,
         unitUDFM,
         addToUDFM,
+        addToUDFM_C,
         delFromUDFM,
         delListFromUDFM,
         adjustUDFM,
@@ -44,10 +45,11 @@ module UniqDFM (
         sizeUDFM,
         intersectUDFM,
         intersectsUDFM,
-        disjointUDFM,
+        disjointUDFM, disjointUdfmUfm,
         minusUDFM,
         udfmMinusUFM,
         partitionUDFM,
+        anyUDFM,
 
         udfmToList,
         udfmToUfm,
@@ -157,6 +159,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)
 
@@ -271,6 +285,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
@@ -325,6 +342,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
index c90ea43..0950875 100644 (file)
@@ -1,7 +1,8 @@
 
 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]
index 2b0524f..c932530 100644 (file)
@@ -1,7 +1,7 @@
 
 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 =>
index 516bdf3..91244c4 100644 (file)
@@ -1,13 +1,13 @@
 
 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
index efa3a73..04ba4f4 100644 (file)
@@ -1,7 +1,7 @@
 
 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)
index 4a2473a..b52000e 100644 (file)
@@ -1,7 +1,7 @@
 
 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)
index f906a95..4490292 100644 (file)
@@ -1,7 +1,7 @@
 
 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)