Kill non-deterministic foldUFM in TrieMap and TcAppMap

Summary:
foldUFM introduces unnecessary non-determinism that actually
leads to different generated code as explained in
Note [TrieMap determinism].

As we're switching from UniqFM to UniqDFM here you might be
concerned about performance. There's nothing that ./validate
detects. nofib reports no change in Compile Allocations, but
Compile Time got better on some tests and worse on some,
yielding this summary:

        -1 s.d.                -----            -3.8%
        +1 s.d.                -----            +5.4%
        Average                -----            +0.7%

This is not a fair comparison as the order of Uniques
changes what GHC is actually doing. One benefit from making
this deterministic is also that it will make the
performance results more stable.

Full nofib results: P108

Test Plan: ./validate, nofib

Reviewers: goldfire, simonpj, simonmar, austin, bgamari

Reviewed By: simonpj

Subscribers: thomie

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

GHC Trac Issues: #4012

20 files changed, 222 insertions, 120 deletions

diff --git a/compiler/basicTypes/NameEnv.hs b/compiler/basicTypes/NameEnv.hs
index d9ad35945b..674323d290 100644
--- a/compiler/basicTypes/NameEnv.hs
+++ b/compiler/basicTypes/NameEnv.hs
@@ -21,6 +21,12 @@ module NameEnv (
         lookupNameEnv, lookupNameEnv_NF, delFromNameEnv, delListFromNameEnv,
         elemNameEnv, mapNameEnv, disjointNameEnv,
 
+        DNameEnv,
+
+        emptyDNameEnv,
+        lookupDNameEnv,
+        mapDNameEnv,
+        alterDNameEnv,
         -- ** Dependency analysis
         depAnal
     ) where
@@ -31,6 +37,7 @@ import Digraph
 import Name
 import Unique
 import UniqFM
+import UniqDFM
 import Maybes
 
 {-
@@ -116,3 +123,20 @@ anyNameEnv f x          = foldUFM ((||) . f) False x
 disjointNameEnv x y     = isNullUFM (intersectUFM x y)
 
 lookupNameEnv_NF env n = expectJust "lookupNameEnv_NF" (lookupNameEnv env n)
+
+-- Deterministic NameEnv
+-- See Note [Deterministic UniqFM] in UniqDFM for explanation why we need
+-- DNameEnv.
+type DNameEnv a = UniqDFM a
+
+emptyDNameEnv :: DNameEnv a
+emptyDNameEnv = emptyUDFM
+
+lookupDNameEnv :: DNameEnv a -> Name -> Maybe a
+lookupDNameEnv = lookupUDFM
+
+mapDNameEnv :: (a -> b) -> DNameEnv a -> DNameEnv b
+mapDNameEnv = mapUDFM
+
+alterDNameEnv :: (Maybe a -> Maybe a) -> DNameEnv a -> Name -> DNameEnv a
+alterDNameEnv = alterUDFM
diff --git a/compiler/basicTypes/VarEnv.hs b/compiler/basicTypes/VarEnv.hs
index bd59e15253..917946f56e 100644
--- a/compiler/basicTypes/VarEnv.hs
+++ b/compiler/basicTypes/VarEnv.hs
@@ -31,6 +31,8 @@ module VarEnv (
         extendDVarEnv,
         lookupDVarEnv,
         foldDVarEnv,
+        mapDVarEnv,
+        alterDVarEnv,
 
         -- * The InScopeSet type
         InScopeSet,
@@ -514,3 +516,9 @@ lookupDVarEnv = lookupUDFM
 
 foldDVarEnv :: (a -> b -> b) -> b -> DVarEnv a -> b
 foldDVarEnv = foldUDFM
+
+mapDVarEnv :: (a -> b) -> DVarEnv a -> DVarEnv b
+mapDVarEnv = mapUDFM
+
+alterDVarEnv :: (Maybe a -> Maybe a) -> DVarEnv a -> Var -> DVarEnv a
+alterDVarEnv = alterUDFM
diff --git a/compiler/coreSyn/TrieMap.hs b/compiler/coreSyn/TrieMap.hs
index 2b23b256cb..fbff260055 100644
--- a/compiler/coreSyn/TrieMap.hs
+++ b/compiler/coreSyn/TrieMap.hs
@@ -25,7 +25,7 @@ import Name
 import Type
 import TyCoRep
 import Var
-import UniqFM
+import UniqDFM
 import Unique( Unique )
 import FastString(FastString)
 
@@ -129,13 +129,81 @@ instance Ord k => TrieMap (Map.Map k) where
   foldTM k m z = Map.fold k z m
   mapTM f m = Map.map f m
 
-instance TrieMap UniqFM where
-  type Key UniqFM = Unique
-  emptyTM = emptyUFM
-  lookupTM k m = lookupUFM m k
-  alterTM k f m = alterUFM f m k
-  foldTM k m z = foldUFM k z m
-  mapTM f m = mapUFM f m
+
+{-
+Note [foldTM determinism]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+We want foldTM to be deterministic, which is why we have an instance of
+TrieMap for UniqDFM, but not for UniqFM. Here's an example of some things that
+go wrong if foldTM is nondeterministic. Consider:
+
+  f a b = return (a <> b)
+
+Depending on the order that the typechecker generates constraints you
+get either:
+
+  f :: (Monad m, Monoid a) => a -> a -> m a
+
+or:
+
+  f :: (Monoid a, Monad m) => a -> a -> m a
+
+The generated code will be different after desugaring as the dictionaries
+will be bound in different orders, leading to potential ABI incompatibility.
+
+One way to solve this would be to notice that the typeclasses could be
+sorted alphabetically.
+
+Unfortunately that doesn't quite work with this example:
+
+  f a b = let x = a <> a; y = b <> b in x
+
+where you infer:
+
+  f :: (Monoid m, Monoid m1) => m1 -> m -> m1
+
+or:
+
+  f :: (Monoid m1, Monoid m) => m1 -> m -> m1
+
+Here you could decide to take the order of the type variables in the type
+according to depth first traversal and use it to order the constraints.
+
+The real trouble starts when the user enables incoherent instances and
+the compiler has to make an arbitrary choice. Consider:
+
+  class T a b where
+    go :: a -> b -> String
+
+  instance (Show b) => T Int b where
+    go a b = show a ++ show b
+
+  instance (Show a) => T a Bool where
+    go a b = show a ++ show b
+
+  f = go 10 True
+
+GHC is free to choose either dictionary to implement f, but for the sake of
+determinism we'd like it to be consistent when compiling the same sources
+with the same flags.
+
+inert_dicts :: DictMap is implemented with a TrieMap. In getUnsolvedInerts it
+gets converted to a bag of (Wanted) Cts using a fold. Then in
+solve_simple_wanteds it's merged with other WantedConstraints. We want the
+conversion to a bag to be deterministic. For that purpose we use UniqDFM
+instead of UniqFM to implement the TrieMap.
+
+See Note [Deterministic UniqFM] in UniqDFM for more details on how it's made
+deterministic.
+-}
+
+instance TrieMap UniqDFM where
+  type Key UniqDFM = Unique
+  emptyTM = emptyUDFM
+  lookupTM k m = lookupUDFM m k
+  alterTM k f m = alterUDFM f m k
+  foldTM k m z = foldUDFM k z m
+  mapTM f m = mapUDFM f m
 
 {-
 ************************************************************************
@@ -227,11 +295,11 @@ foldMaybe k (Just a) b = k a b
 ************************************************************************
 -}
 
-lkNamed :: NamedThing n => n -> NameEnv a -> Maybe a
-lkNamed n env = lookupNameEnv env (getName n)
+lkDNamed :: NamedThing n => n -> DNameEnv a -> Maybe a
+lkDNamed n env = lookupDNameEnv env (getName n)
 
-xtNamed :: NamedThing n => n -> XT a -> NameEnv a -> NameEnv a
-xtNamed tc f m = alterNameEnv f m (getName tc)
+xtDNamed :: NamedThing n => n -> XT a -> DNameEnv a -> DNameEnv a
+xtDNamed tc f m = alterDNameEnv f m (getName tc)
 
 ------------------------
 type LiteralMap  a = Map.Map Literal a
@@ -598,13 +666,13 @@ xtTickish = alterTM
 ------------------------
 data AltMap a   -- A single alternative
   = AM { am_deflt :: CoreMapG a
-       , am_data  :: NameEnv (CoreMapG a)
+       , am_data  :: DNameEnv (CoreMapG a)
        , am_lit   :: LiteralMap (CoreMapG a) }
 
 instance TrieMap AltMap where
    type Key AltMap = CoreAlt
    emptyTM  = AM { am_deflt = emptyTM
-                 , am_data = emptyNameEnv
+                 , am_data = emptyDNameEnv
                  , am_lit  = emptyLiteralMap }
    lookupTM = lkA emptyCME
    alterTM  = xtA emptyCME
@@ -625,13 +693,13 @@ instance Eq (DeBruijn CoreAlt) where
 mapA :: (a->b) -> AltMap a -> AltMap b
 mapA f (AM { am_deflt = adeflt, am_data = adata, am_lit = alit })
   = AM { am_deflt = mapTM f adeflt
-       , am_data = mapNameEnv (mapTM f) adata
+       , am_data = mapTM (mapTM f) adata
        , am_lit = mapTM (mapTM f) alit }
 
 lkA :: CmEnv -> CoreAlt -> AltMap a -> Maybe a
 lkA env (DEFAULT,    _, rhs)  = am_deflt >.> lkG (D env rhs)
 lkA env (LitAlt lit, _, rhs)  = am_lit >.> lkLit lit >=> lkG (D env rhs)
-lkA env (DataAlt dc, bs, rhs) = am_data >.> lkNamed dc
+lkA env (DataAlt dc, bs, rhs) = am_data >.> lkDNamed dc
                                         >=> lkG (D (extendCMEs env bs) rhs)
 
 xtA :: CmEnv -> CoreAlt -> XT a -> AltMap a -> AltMap a
@@ -640,7 +708,7 @@ xtA env (DEFAULT, _, rhs)    f m =
 xtA env (LitAlt l, _, rhs)   f m =
     m { am_lit   = am_lit m   |> xtLit l |>> xtG (D env rhs) f }
 xtA env (DataAlt d, bs, rhs) f m =
-    m { am_data  = am_data m  |> xtNamed d
+    m { am_data  = am_data m  |> xtDNamed d
                              |>> xtG (D (extendCMEs env bs) rhs) f }
 
 fdA :: (a -> b -> b) -> AltMap a -> b -> b
@@ -713,7 +781,7 @@ type TypeMapG = GenMap TypeMapX
 data TypeMapX a
   = TM { tm_var    :: VarMap a
        , tm_app    :: TypeMapG (TypeMapG a)
-       , tm_tycon  :: NameEnv a
+       , tm_tycon  :: DNameEnv a
        , tm_forall :: TypeMapG (BndrMap a) -- See Note [Binders]
        , tm_tylit  :: TyLitMap a
        , tm_coerce :: Maybe a
@@ -775,7 +843,7 @@ instance Outputable a => Outputable (TypeMapG a) where
 emptyT :: TypeMapX a
 emptyT = TM { tm_var  = emptyTM
             , tm_app  = EmptyMap
-            , tm_tycon  = emptyNameEnv
+            , tm_tycon  = emptyDNameEnv
             , tm_forall = EmptyMap
             , tm_tylit  = emptyTyLitMap
             , tm_coerce = Nothing }
@@ -786,7 +854,7 @@ mapT f (TM { tm_var  = tvar, tm_app = tapp, tm_tycon = ttycon
            , tm_coerce = tcoerce })
   = TM { tm_var    = mapTM f tvar
        , tm_app    = mapTM (mapTM f) tapp
-       , tm_tycon  = mapNameEnv f ttycon
+       , tm_tycon  = mapTM f ttycon
        , tm_forall = mapTM (mapTM f) tforall
        , tm_tylit  = mapTM f tlit
        , tm_coerce = fmap f tcoerce }
@@ -799,7 +867,7 @@ lkT (D env ty) m = go ty m
     go (TyVarTy v)                 = tm_var    >.> lkVar env v
     go (AppTy t1 t2)               = tm_app    >.> lkG (D env t1)
                                                >=> lkG (D env t2)
-    go (TyConApp tc [])            = tm_tycon  >.> lkNamed tc
+    go (TyConApp tc [])            = tm_tycon  >.> lkDNamed tc
     go ty@(TyConApp _ (_:_))       = pprPanic "lkT TyConApp" (ppr ty)
     go (LitTy l)                   = tm_tylit  >.> lkTyLit l
     go (ForAllTy (Named tv _) ty)  = tm_forall >.> lkG (D (extendCME env tv) ty)
@@ -815,7 +883,7 @@ xtT (D env ty) f m | Just ty' <- trieMapView ty = xtT (D env ty') f m
 xtT (D env (TyVarTy v))       f m = m { tm_var    = tm_var m |> xtVar env v f }
 xtT (D env (AppTy t1 t2))     f m = m { tm_app    = tm_app m |> xtG (D env t1)
                                                             |>> xtG (D env t2) f }
-xtT (D _   (TyConApp tc []))  f m = m { tm_tycon  = tm_tycon m |> xtNamed tc f }
+xtT (D _   (TyConApp tc []))  f m = m { tm_tycon  = tm_tycon m |> xtDNamed tc f }
 xtT (D _   (LitTy l))         f m = m { tm_tylit  = tm_tylit m |> xtTyLit l f }
 xtT (D env (CastTy t _))      f m = xtT (D env t) f m
 xtT (D _   (CoercionTy {}))   f m = m { tm_coerce = tm_coerce m |> f }
@@ -988,11 +1056,11 @@ xtBndr env v f = xtG (D env (varType v)) f
 
 --------- Variable occurrence -------------
 data VarMap a = VM { vm_bvar   :: BoundVarMap a  -- Bound variable
-                   , vm_fvar   :: VarEnv a }      -- Free variable
+                   , vm_fvar   :: DVarEnv a }      -- Free variable
 
 instance TrieMap VarMap where
    type Key VarMap = Var
-   emptyTM  = VM { vm_bvar = IntMap.empty, vm_fvar = emptyVarEnv }
+   emptyTM  = VM { vm_bvar = IntMap.empty, vm_fvar = emptyDVarEnv }
    lookupTM = lkVar emptyCME
    alterTM  = xtVar emptyCME
    foldTM   = fdVar
@@ -1000,24 +1068,24 @@ instance TrieMap VarMap where
 
 mapVar :: (a->b) -> VarMap a -> VarMap b
 mapVar f (VM { vm_bvar = bv, vm_fvar = fv })
-  = VM { vm_bvar = mapTM f bv, vm_fvar = mapVarEnv f fv }
+  = VM { vm_bvar = mapTM f bv, vm_fvar = mapTM f fv }
 
 lkVar :: CmEnv -> Var -> VarMap a -> Maybe a
 lkVar env v
   | Just bv <- lookupCME env v = vm_bvar >.> lookupTM bv
-  | otherwise                  = vm_fvar >.> lkFreeVar v
+  | otherwise                  = vm_fvar >.> lkDFreeVar v
 
 xtVar :: CmEnv -> Var -> XT a -> VarMap a -> VarMap a
 xtVar env v f m
-  | Just bv <- lookupCME env v = m { vm_bvar = vm_bvar m |> xtInt bv f }
-  | otherwise                  = m { vm_fvar = vm_fvar m |> xtFreeVar v f }
+  | Just bv <- lookupCME env v = m { vm_bvar = vm_bvar m |> alterTM bv f }
+  | otherwise                  = m { vm_fvar = vm_fvar m |> xtDFreeVar v f }
 
 fdVar :: (a -> b -> b) -> VarMap a -> b -> b
 fdVar k m = foldTM k (vm_bvar m)
           . foldTM k (vm_fvar m)
 
-lkFreeVar :: Var -> VarEnv a -> Maybe a
-lkFreeVar var env = lookupVarEnv env var
+lkDFreeVar :: Var -> DVarEnv a -> Maybe a
+lkDFreeVar var env = lookupDVarEnv env var
 
-xtFreeVar :: Var -> XT a -> VarEnv a -> VarEnv a
-xtFreeVar v f m = alterVarEnv f m v
+xtDFreeVar :: Var -> XT a -> DVarEnv a -> DVarEnv a
+xtDFreeVar v f m = alterDVarEnv f m v
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 65595c691f..88f2f870e1 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -149,6 +149,7 @@ import TcRnTypes
 
 import Unique
 import UniqFM
+import UniqDFM
 import Maybes
 
 import StaticFlags( opt_PprStyle_Debug )
@@ -2071,37 +2072,38 @@ not match the requsted info exactly!
 
 -}
 
-type TcAppMap a = UniqFM (ListMap LooseTypeMap a)
+type TcAppMap a = UniqDFM (ListMap LooseTypeMap a)
     -- Indexed by tycon then the arg types, using "loose" matching, where
     -- we don't require kind equality. This allows, for example, (a |> co)
     -- to match (a).
     -- See Note [Use loose types in inert set]
-    -- Used for types and classes; hence UniqFM
+    -- Used for types and classes; hence UniqDFM
+    -- See Note [foldTM determinism] for why we use UniqDFM here
 
 isEmptyTcAppMap :: TcAppMap a -> Bool
-isEmptyTcAppMap m = isNullUFM m
+isEmptyTcAppMap m = isNullUDFM m
 
 emptyTcAppMap :: TcAppMap a
-emptyTcAppMap = emptyUFM
+emptyTcAppMap = emptyUDFM
 
 findTcApp :: TcAppMap a -> Unique -> [Type] -> Maybe a
-findTcApp m u tys = do { tys_map <- lookupUFM m u
+findTcApp m u tys = do { tys_map <- lookupUDFM m u
                        ; lookupTM tys tys_map }
 
 delTcApp :: TcAppMap a -> Unique -> [Type] -> TcAppMap a
-delTcApp m cls tys = adjustUFM (deleteTM tys) m cls
+delTcApp m cls tys = adjustUDFM (deleteTM tys) m cls
 
 insertTcApp :: TcAppMap a -> Unique -> [Type] -> a -> TcAppMap a
-insertTcApp m cls tys ct = alterUFM alter_tm m cls
+insertTcApp m cls tys ct = alterUDFM alter_tm m cls
   where
     alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
 
 -- mapTcApp :: (a->b) -> TcAppMap a -> TcAppMap b
--- mapTcApp f = mapUFM (mapTM f)
+-- mapTcApp f = mapUDFM (mapTM f)
 
 filterTcAppMap :: (Ct -> Bool) -> TcAppMap Ct -> TcAppMap Ct
 filterTcAppMap f m
-  = mapUFM do_tm m
+  = mapUDFM do_tm m
   where
     do_tm tm = foldTM insert_mb tm emptyTM
     insert_mb ct tm
@@ -2117,7 +2119,7 @@ tcAppMapToBag :: TcAppMap a -> Bag a
 tcAppMapToBag m = foldTcAppMap consBag m emptyBag
 
 foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
-foldTcAppMap k m z = foldUFM (foldTM k) z m
+foldTcAppMap k m z = foldUDFM (foldTM k) z m
 
 
 {- *********************************************************************
@@ -2139,7 +2141,7 @@ findDict m cls tys = findTcApp m (getUnique cls) tys
 
 findDictsByClass :: DictMap a -> Class -> Bag a
 findDictsByClass m cls
-  | Just tm <- lookupUFM m cls = foldTM consBag tm emptyBag
+  | Just tm <- lookupUDFM m cls = foldTM consBag tm emptyBag
   | otherwise                  = emptyBag
 
 delDict :: DictMap a -> Class -> [Type] -> DictMap a
@@ -2150,7 +2152,7 @@ addDict m cls tys item = insertTcApp m (getUnique cls) tys item
 
 addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
 addDictsByClass m cls items
-  = addToUFM m cls (foldrBag add emptyTM items)
+  = addToUDFM m cls (foldrBag add emptyTM items)
   where
     add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
     add ct _ = pprPanic "addDictsByClass" (ppr ct)
@@ -2203,7 +2205,7 @@ findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
 -- We use this to check for derived interactions with built-in type-function
 -- constructors.
 findFunEqsByTyCon m tc
-  | Just tm <- lookupUFM m tc = foldTM (:) tm []
+  | Just tm <- lookupUDFM m tc = foldTM (:) tm []
   | otherwise                 = []
 
 foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
diff --git a/testsuite/tests/ado/ado004.stderr b/testsuite/tests/ado/ado004.stderr
index 6a39e6d142..8f5a816612 100644
--- a/testsuite/tests/ado/ado004.stderr
+++ b/testsuite/tests/ado/ado004.stderr
@@ -3,11 +3,11 @@ TYPE SIGNATURES
     forall (f :: * -> *). Applicative f => (Int -> f Int) -> f Int
   test2 ::
     forall t b (f :: * -> *).
-    (Applicative f, Num t, Num b) =>
+    (Num b, Num t, Applicative f) =>
     (t -> f b) -> f b
   test2a ::
     forall t b (f :: * -> *).
-    (Num t, Num b, Functor f) =>
+    (Num b, Num t, Functor f) =>
     (t -> f b) -> f b
   test2b ::
     forall (m :: * -> *) a t. (Num t, Monad m) => (t -> a) -> m a
diff --git a/testsuite/tests/ghc-api/apirecomp001/apirecomp001.stderr b/testsuite/tests/ghc-api/apirecomp001/apirecomp001.stderr
index 80b94dca4b..52385104cf 100644
--- a/testsuite/tests/ghc-api/apirecomp001/apirecomp001.stderr
+++ b/testsuite/tests/ghc-api/apirecomp001/apirecomp001.stderr
@@ -3,14 +3,14 @@ B.hs:4:1: warning: [-Wmissing-signatures]
     Top-level binding with no type signature:
       answer_to_live_the_universe_and_everything :: Int
 
-B.hs:5:12: warning: [-Wtype-defaults]
+B.hs:5:13: warning: [-Wtype-defaults]
     • Defaulting the following constraints to type ‘Integer’
+        (Num a0) arising from the literal ‘1’ at B.hs:5:13
         (Enum a0)
           arising from the arithmetic sequence ‘1 .. 23 * 2’ at B.hs:5:12-20
-        (Num a0) arising from the literal ‘1’ at B.hs:5:13
-    • In the first argument of ‘length’, namely ‘[1 .. 23 * 2]’
+    • In the expression: 1
+      In the first argument of ‘length’, namely ‘[1 .. 23 * 2]’
       In the first argument of ‘(-)’, namely ‘length [1 .. 23 * 2]’
-      In the expression: length [1 .. 23 * 2] - 4
 
 A.hs:7:1: warning: [-Wmissing-signatures]
     Top-level binding with no type signature: main :: IO ()
@@ -19,14 +19,14 @@ B.hs:4:1: warning: [-Wmissing-signatures]
     Top-level binding with no type signature:
       answer_to_live_the_universe_and_everything :: Int
 
-B.hs:5:12: warning: [-Wtype-defaults]
+B.hs:5:13: warning: [-Wtype-defaults]
     • Defaulting the following constraints to type ‘Integer’
+        (Num a0) arising from the literal ‘1’ at B.hs:5:13
         (Enum a0)
           arising from the arithmetic sequence ‘1 .. 23 * 2’ at B.hs:5:12-20
-        (Num a0) arising from the literal ‘1’ at B.hs:5:13
-    • In the first argument of ‘length’, namely ‘[1 .. 23 * 2]’
+    • In the expression: 1
+      In the first argument of ‘length’, namely ‘[1 .. 23 * 2]’
       In the first argument of ‘(-)’, namely ‘length [1 .. 23 * 2]’
-      In the expression: length [1 .. 23 * 2] - 4
 
 A.hs:7:1: warning: [-Wmissing-signatures]
     Top-level binding with no type signature: main :: IO ()
diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr
index bedb722475..a3489d23bd 100644
--- a/testsuite/tests/indexed-types/should_compile/T3017.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr
@@ -4,7 +4,7 @@ TYPE SIGNATURES
   emptyL :: forall a. ListColl a
   insert :: forall c. Coll c => Elem c -> c -> c
   test2 ::
-    forall t t1 c. (Elem c ~ (t, t1), Coll c, Num t1, Num t) => c -> c
+    forall t t1 c. (Elem c ~ (t, t1), Coll c, Num t, Num t1) => c -> c
 TYPE CONSTRUCTORS
   class Coll c where
     type family Elem c :: * open
diff --git a/testsuite/tests/parser/should_compile/T2245.stderr b/testsuite/tests/parser/should_compile/T2245.stderr
index 7a4e868c9f..c2bc8da935 100644
--- a/testsuite/tests/parser/should_compile/T2245.stderr
+++ b/testsuite/tests/parser/should_compile/T2245.stderr
@@ -11,12 +11,12 @@ T2245.hs:5:10: warning: [-Wmissing-methods (in -Wdefault)]
         ‘fromRational’ and (either ‘recip’ or ‘/’)
     • In the instance declaration for ‘Fractional T’
 
-T2245.hs:7:29: warning: [-Wtype-defaults (in -Wall)]
+T2245.hs:7:27: warning: [-Wtype-defaults (in -Wall)]
     • Defaulting the following constraints to type ‘T’
+        (Ord a0) arising from an operator section at T2245.hs:7:27-33
         (Fractional a0)
           arising from the literal ‘1e400’ at T2245.hs:7:29-33
-        (Ord a0) arising from an operator section at T2245.hs:7:27-33
         (Read a0) arising from a use of ‘read’ at T2245.hs:7:38-41
-    • In the second argument of ‘(<)’, namely ‘1e400’
-      In the first argument of ‘(.)’, namely ‘(< 1e400)’
+    • In the first argument of ‘(.)’, namely ‘(< 1e400)’
       In the second argument of ‘(.)’, namely ‘(< 1e400) . read’
+      In the second argument of ‘($)’, namely ‘show . (< 1e400) . read’
diff --git a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr
index 0f0d6f91b2..83c22b61af 100644
--- a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints1.stderr
@@ -1,6 +1,6 @@
 TYPE SIGNATURES
-  arbitCs1 :: forall a. (Show a, Eq a, Enum a) => a -> String
-  arbitCs2 :: forall a. (Show a, Eq a, Enum a) => a -> String
+  arbitCs1 :: forall a. (Eq a, Enum a, Show a) => a -> String
+  arbitCs2 :: forall a. (Show a, Enum a, Eq a) => a -> String
   arbitCs3 :: forall a. (Show a, Enum a, Eq a) => a -> String
   arbitCs4 :: forall a. (Eq a, Show a, Enum a) => a -> String
   arbitCs5 :: forall a. (Eq a, Enum a, Show a) => a -> String
@@ -8,4 +8,4 @@ TYPE CONSTRUCTORS
 COERCION AXIOMS
 Dependent modules: []
 Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
-                     integer-gmp-1.0.0.0]
+                     integer-gmp-1.0.0.1]
diff --git a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
index ee31ed289c..5893c7ba55 100644
--- a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
@@ -39,7 +39,7 @@ TYPE SIGNATURES
   atan2 :: forall a. RealFloat a => a -> a -> a
   atanh :: forall a. Floating a => a -> a
   break :: forall a. (a -> Bool) -> [a] -> ([a], [a])
-  ceiling :: forall b a. (RealFrac a, Integral b) => a -> b
+  ceiling :: forall b a. (Integral b, RealFrac a) => a -> b
   compare :: forall a. Ord a => a -> a -> Ordering
   concat :: forall (t :: * -> *) a. P.Foldable t => t [a] -> [a]
   concatMap ::
@@ -56,7 +56,7 @@ TYPE SIGNATURES
   dropWhile :: forall a. (a -> Bool) -> [a] -> [a]
   either :: forall b c a. (a -> c) -> (b -> c) -> Either a b -> c
   elem ::
-    forall (t :: * -> *) a. (P.Foldable t, Eq a) => a -> t a -> Bool
+    forall (t :: * -> *) a. (Eq a, P.Foldable t) => a -> t a -> Bool
   encodeFloat :: forall a. RealFloat a => Integer -> Int -> a
   enumFrom :: forall a. Enum a => a -> [a]
   enumFromThen :: forall a. Enum a => a -> a -> [a]
@@ -72,7 +72,7 @@ TYPE SIGNATURES
   floatDigits :: forall a. RealFloat a => a -> Int
   floatRadix :: forall a. RealFloat a => a -> Integer
   floatRange :: forall a. RealFloat a => a -> (Int, Int)
-  floor :: forall b a. (RealFrac a, Integral b) => a -> b
+  floor :: forall b a. (Integral b, RealFrac a) => a -> b
   fmap ::
     forall (f :: * -> *) b a. Functor f => (a -> b) -> f a -> f b
   foldl ::
@@ -118,26 +118,26 @@ TYPE SIGNATURES
   map :: forall b a. (a -> b) -> [a] -> [b]
   mapM ::
     forall (t :: * -> *) (m :: * -> *) b a.
-    (P.Traversable t, Monad m) =>
+    (Monad m, P.Traversable t) =>
     (a -> m b) -> t a -> m (t b)
   mapM_ ::
     forall (t :: * -> *) (m :: * -> *) b a.
-    (P.Foldable t, Monad m) =>
+    (Monad m, P.Foldable t) =>
     (a -> m b) -> t a -> m ()
   max :: forall a. Ord a => a -> a -> a
   maxBound :: forall t. Bounded t => t
   maximum ::
-    forall (t :: * -> *) a. (P.Foldable t, Ord a) => t a -> a
+    forall (t :: * -> *) a. (Ord a, P.Foldable t) => t a -> a
   maybe :: forall a b. b -> (a -> b) -> Maybe a -> b
   min :: forall a. Ord a => a -> a -> a
   minBound :: forall t. Bounded t => t
   minimum ::
-    forall (t :: * -> *) a. (P.Foldable t, Ord a) => t a -> a
+    forall (t :: * -> *) a. (Ord a, P.Foldable t) => t a -> a
   mod :: forall a. Integral a => a -> a -> a
   negate :: forall a. Num a => a -> a
   not :: Bool -> Bool
   notElem ::
-    forall (t :: * -> *) a. (P.Foldable t, Eq a) => a -> t a -> Bool
+    forall (t :: * -> *) a. (Eq a, P.Foldable t) => a -> t a -> Bool
   null :: forall (t :: * -> *) a. P.Foldable t => t a -> Bool
   odd :: forall a. Integral a => a -> Bool
   or :: forall (t :: * -> *). P.Foldable t => t Bool -> Bool
@@ -146,9 +146,9 @@ TYPE SIGNATURES
   pred :: forall a. Enum a => a -> a
   print :: forall a. Show a => a -> IO ()
   product ::
-    forall (t :: * -> *) a. (P.Foldable t, Num a) => t a -> a
+    forall (t :: * -> *) a. (Num a, P.Foldable t) => t a -> a
   properFraction ::
-    forall b a. (RealFrac a, Integral b) => a -> (b, a)
+    forall b a. (Integral b, RealFrac a) => a -> (b, a)
   putChar :: Char -> IO ()
   putStr :: String -> IO ()
   putStrLn :: String -> IO ()
@@ -162,14 +162,14 @@ TYPE SIGNATURES
   readParen :: forall a. Bool -> ReadS a -> ReadS a
   reads :: forall a. Read a => ReadS a
   readsPrec :: forall a. Read a => Int -> ReadS a
-  realToFrac :: forall b a. (Real a, Fractional b) => a -> b
+  realToFrac :: forall b a. (Fractional b, Real a) => a -> b
   recip :: forall a. Fractional a => a -> a
   rem :: forall a. Integral a => a -> a -> a
   repeat :: forall a. a -> [a]
   replicate :: forall a. Int -> a -> [a]
   return :: forall (m :: * -> *) a. Monad m => a -> m a
   reverse :: forall a. [a] -> [a]
-  round :: forall b a. (RealFrac a, Integral b) => a -> b
+  round :: forall b a. (Integral b, RealFrac a) => a -> b
   scaleFloat :: forall a. RealFloat a => Int -> a -> a
   scanl :: forall a b. (b -> a -> b) -> b -> [a] -> [b]
   scanl1 :: forall a. (a -> a -> a) -> [a] -> [a]
@@ -178,11 +178,11 @@ TYPE SIGNATURES
   seq :: forall b a. a -> b -> b
   sequence ::
     forall (t :: * -> *) (m :: * -> *) a.
-    (P.Traversable t, Monad m) =>
+    (Monad m, P.Traversable t) =>
     t (m a) -> m (t a)
   sequence_ ::
     forall (t :: * -> *) (m :: * -> *) a.
-    (P.Foldable t, Monad m) =>
+    (Monad m, P.Foldable t) =>
     t (m a) -> m ()
   show :: forall a. Show a => a -> String
   showChar :: Char -> ShowS
@@ -201,7 +201,7 @@ TYPE SIGNATURES
   sqrt :: forall a. Floating a => a -> a
   subtract :: forall a. Num a => a -> a -> a
   succ :: forall a. Enum a => a -> a
-  sum :: forall (t :: * -> *) a. (P.Foldable t, Num a) => t a -> a
+  sum :: forall (t :: * -> *) a. (Num a, P.Foldable t) => t a -> a
   tail :: forall a. [a] -> [a]
   take :: forall a. Int -> [a] -> [a]
   takeWhile :: forall a. (a -> Bool) -> [a] -> [a]
@@ -210,7 +210,7 @@ TYPE SIGNATURES
   toEnum :: forall a. Enum a => Int -> a
   toInteger :: forall a. Integral a => a -> Integer
   toRational :: forall a. Real a => a -> Rational
-  truncate :: forall b a. (RealFrac a, Integral b) => a -> b
+  truncate :: forall b a. (Integral b, RealFrac a) => a -> b
   uncurry :: forall c b a. (a -> b -> c) -> (a, b) -> c
   undefined :: forall t. t
   unlines :: [String] -> String
diff --git a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
index b5268acb60..6d22293cb9 100644
--- a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
@@ -10,7 +10,7 @@ Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
 WarningWildcardInstantiations.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
     • Found type wildcard ‘_a’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
-               the inferred type of foo :: (Show a, Enum a) => a -> String
+               the inferred type of foo :: (Enum a, Show a) => a -> String
                at WarningWildcardInstantiations.hs:6:1
     • In the type signature:
         foo :: (Show _a, _) => _a -> _
diff --git a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
index 30efb8fc14..2df15443c9 100644
--- a/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/InstantiatedNamedWildcardsInConstraints.stderr
@@ -2,7 +2,7 @@
 InstantiatedNamedWildcardsInConstraints.hs:4:14: error:
     • Found type wildcard ‘_a’ standing for ‘b’
       Where: ‘b’ is a rigid type variable bound by
-               the inferred type of foo :: (Show b, Enum b) => b -> (String, b)
+               the inferred type of foo :: (Enum b, Show b) => b -> (String, b)
                at InstantiatedNamedWildcardsInConstraints.hs:4:8
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
index 63058a9781..7e0b5ace3e 100644
--- a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
@@ -2,7 +2,7 @@
 WildcardInstantiations.hs:5:14: error:
     • Found type wildcard ‘_a’ standing for ‘a’
       Where: ‘a’ is a rigid type variable bound by
-               the inferred type of foo :: (Show a, Enum a) => a -> String
+               the inferred type of foo :: (Enum a, Show a) => a -> String
                at WildcardInstantiations.hs:6:1
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
diff --git a/testsuite/tests/rebindable/rebindable6.stderr b/testsuite/tests/rebindable/rebindable6.stderr
index 8d2ea09928..8667f318bf 100644
--- a/testsuite/tests/rebindable/rebindable6.stderr
+++ b/testsuite/tests/rebindable/rebindable6.stderr
@@ -25,15 +25,18 @@ rebindable6.hs:110:17: error:
                    return b }
 
 rebindable6.hs:111:17: error:
-    • Ambiguous type variable ‘t1’ arising from a do statement
-                                   with the failable pattern ‘Just (b :: b)’
-      prevents the constraint ‘(HasFail
-                                  ([Prelude.Char] -> t1))’ from being solved.
+    • Ambiguous type variables ‘t0’, ‘t1’ arising from a do statement
+      prevents the constraint ‘(HasBind
+                                  (IO (Maybe b) -> (Maybe b -> t1) -> t0))’ from being solved.
         (maybe you haven't applied a function to enough arguments?)
-      Probable fix: use a type annotation to specify what ‘t1’ should be.
+      Relevant bindings include
+        g :: IO (Maybe b) (bound at rebindable6.hs:108:19)
+        test_do :: IO a -> IO (Maybe b) -> IO b
+          (bound at rebindable6.hs:108:9)
+      Probable fix: use a type annotation to specify what ‘t0’, ‘t1’ should be.
       These potential instance exist:
-        instance HasFail (String -> IO a)
-          -- Defined at rebindable6.hs:61:18
+        instance HasBind (IO a -> (a -> IO b) -> IO b)
+          -- Defined at rebindable6.hs:51:18
     • In a stmt of a 'do' block: Just (b :: b) <- g
       In the expression:
         do { f;
diff --git a/testsuite/tests/typecheck/should_compile/T10971a.stderr b/testsuite/tests/typecheck/should_compile/T10971a.stderr
index 72c675aa8c..bfcc3ff846 100644
--- a/testsuite/tests/typecheck/should_compile/T10971a.stderr
+++ b/testsuite/tests/typecheck/should_compile/T10971a.stderr
@@ -32,11 +32,11 @@ T10971a.hs:9:6: warning: [-Wname-shadowing (in -Wall)]
     This binding for ‘f’ shadows the existing binding
       defined at T10971a.hs:7:1
 
-T10971a.hs:9:31: warning: [-Wtype-defaults (in -Wall)]
+T10971a.hs:9:14: warning: [-Wtype-defaults (in -Wall)]
     • Defaulting the following constraints to type ‘[]’
-        (Foldable t0) arising from a use of ‘length’ at T10971a.hs:9:31-38
         (Traversable t0)
           arising from a use of ‘fmapDefault’ at T10971a.hs:9:14-28
-    • In the expression: length x
+        (Foldable t0) arising from a use of ‘length’ at T10971a.hs:9:31-38
+    • In the expression: fmapDefault f x
       In the expression: (fmapDefault f x, length x)
       In the expression: \ f x -> (fmapDefault f x, length x)
diff --git a/testsuite/tests/typecheck/should_fail/T5300.stderr b/testsuite/tests/typecheck/should_fail/T5300.stderr
index f751249677..589da0a5c4 100644
--- a/testsuite/tests/typecheck/should_fail/T5300.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5300.stderr
@@ -12,13 +12,13 @@ T5300.hs:11:7: error:
         f1 :: (Monad m, C1 a b c) => a -> StateT (T b) m a
 
 T5300.hs:14:7: error:
-    • Could not deduce (C2 a2 b2 c20)
+    • Could not deduce (C1 a1 b1 c10)
       from the context: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2)
         bound by the type signature for:
                    f2 :: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
                          a1 -> StateT (T b2) m a2
         at T5300.hs:14:7-69
-      The type variable ‘c20’ is ambiguous
+      The type variable ‘c10’ is ambiguous
     • In the ambiguity check for ‘f2’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature:
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index c95dc53d1c..62385ea1df 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -1,23 +1,22 @@
 
 T5853.hs:15:46: error:
-    • Could not deduce: Subst t (Elem t2) ~ t2
+    • Could not deduce: Subst (Subst t2 t) t1 ~ Subst t2 t1
         arising from a use of ‘<$>’
-      from the context: (F t1,
-                         Elem t1 ~ Elem t1,
+      from the context: (F t2,
                          Elem t2 ~ Elem t2,
-                         Subst t1 (Elem t2) ~ t2,
-                         Subst t2 (Elem t1) ~ t1,
-                         F t,
-                         Elem t ~ Elem t,
-                         Elem t1 ~ Elem t1,
-                         Subst t (Elem t1) ~ t1,
-                         Subst t1 (Elem t) ~ t)
+                         Elem (Subst t2 t1) ~ t1,
+                         Subst t2 t1 ~ Subst t2 t1,
+                         Subst (Subst t2 t1) (Elem t2) ~ t2,
+                         F (Subst t2 t),
+                         Elem (Subst t2 t) ~ t,
+                         Elem t2 ~ Elem t2,
+                         Subst (Subst t2 t) (Elem t2) ~ t2,
+                         Subst t2 t ~ Subst t2 t)
         bound by the RULE "map/map" at T5853.hs:15:2-57
-      ‘t2’ is a rigid type variable bound by
-        the RULE "map/map" at T5853.hs:15:2
+      NB: ‘Subst’ is a type function, and may not be injective
     • In the expression: (f . g) <$> xs
       When checking the transformation rule "map/map"
     • Relevant bindings include
-        f :: Elem t1 -> Elem t2 (bound at T5853.hs:15:19)
-        g :: Elem t -> Elem t1 (bound at T5853.hs:15:21)
-        xs :: t (bound at T5853.hs:15:23)
+        f :: Elem t2 -> t1 (bound at T5853.hs:15:19)
+        g :: t -> Elem t2 (bound at T5853.hs:15:21)
+        xs :: Subst t2 t (bound at T5853.hs:15:23)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail171.stderr b/testsuite/tests/typecheck/should_fail/tcfail171.stderr
index 4c1068b652..076a3394d4 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail171.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail171.stderr
@@ -1,8 +1,8 @@
 
 tcfail171.hs:9:10: error:
-    • No instance for (PrintfType b) arising from a use of ‘printf’
+    • No instance for (PrintfArg a) arising from a use of ‘printf’
       Possible fix:
-        add (PrintfType b) to the context of
+        add (PrintfArg a) to the context of
           the type signature for:
             phex :: a -> b
     • In the expression: printf "0x%x" x
diff --git a/testsuite/tests/typecheck/should_fail/tcfail204.stderr b/testsuite/tests/typecheck/should_fail/tcfail204.stderr
index f3326faf0e..a3e8eec3d6 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail204.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail204.stderr
@@ -1,12 +1,11 @@
 
-tcfail204.hs:10:15: warning: [-Wtype-defaults (in -Wall)]
+tcfail204.hs:10:7: warning: [-Wtype-defaults (in -Wall)]
     • Defaulting the following constraints to type ‘Double’
-        (Fractional a0)
-          arising from the literal ‘6.3’ at tcfail204.hs:10:15-17
         (RealFrac a0)
           arising from a use of ‘ceiling’ at tcfail204.hs:10:7-17
-    • In the first argument of ‘ceiling’, namely ‘6.3’
-      In the expression: ceiling 6.3
+        (Fractional a0)
+          arising from the literal ‘6.3’ at tcfail204.hs:10:15-17
+    • In the expression: ceiling 6.3
       In an equation for ‘foo’: foo = ceiling 6.3
 
 <no location info>: error: 
diff --git a/testsuite/tests/warnings/should_compile/PluralS.stderr b/testsuite/tests/warnings/should_compile/PluralS.stderr
index 4cffc15a1f..b1ceab6762 100644
--- a/testsuite/tests/warnings/should_compile/PluralS.stderr
+++ b/testsuite/tests/warnings/should_compile/PluralS.stderr
@@ -6,12 +6,11 @@ PluralS.hs:15:17: warning: [-Wtype-defaults (in -Wall)]
       In the expression: 123 `seq` ()
       In an equation for ‘defaultingNum’: defaultingNum = 123 `seq` ()
 
-PluralS.hs:17:29: warning: [-Wtype-defaults (in -Wall)]
+PluralS.hs:17:24: warning: [-Wtype-defaults (in -Wall)]
     • Defaulting the following constraints to type ‘Integer’
-        (Num a0) arising from the literal ‘123’ at PluralS.hs:17:29-31
         (Show a0) arising from a use of ‘show’ at PluralS.hs:17:24-31
-    • In the first argument of ‘show’, namely ‘123’
-      In the expression: show 123
+        (Num a0) arising from the literal ‘123’ at PluralS.hs:17:29-31
+    • In the expression: show 123
       In an equation for ‘defaultingNumAndShow’:
           defaultingNumAndShow = show 123