Prioritise equalities when solving, incl deriveds

We already prioritise equalities when solving, but
Trac #14723 showed that we were not doing so consistently
enough, and as a result the type checker could go into a loop.
Yikes.

See Note [Prioritise equalities] in TcSMonad.

Fixng this bug changed the solve order enough to demonstrate
a problem with fundeps: Trac #14745.

6 files changed, 126 insertions, 1 deletions

diff --git a/testsuite/tests/polykinds/T14723.hs b/testsuite/tests/polykinds/T14723.hs
new file mode 100644
index 0000000000..9b2f3bf75e
--- /dev/null
+++ b/testsuite/tests/polykinds/T14723.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T14723 () where
+
+import Data.Coerce( coerce )
+import Data.Kind (Type)
+import Data.Proxy (Proxy(..))
+import Data.String (fromString)
+import Data.Int (Int64)
+import GHC.Stack (HasCallStack)
+import GHC.TypeLits (Nat, Symbol)
+
+data JType = Iface Symbol
+
+data J (a :: JType)
+
+newIterator
+  :: IO (J ('Iface "java.util.Iterator"))
+newIterator = do
+    let tblPtr :: Int64
+        tblPtr = undefined
+    iterator <-
+         (qqMarker (Proxy :: Proxy "wuggle")
+                   (Proxy :: Proxy "waggle")
+                   (Proxy :: Proxy "tblPtr")
+                   (Proxy :: Proxy 106)
+                   (tblPtr, ())
+                   Proxy
+                   (undefined :: IO Int))
+    undefined
+
+class Coercible (a :: Type) where
+  type Ty a :: JType
+
+instance Coercible Int64 where
+  type Ty Int64 = Iface "Int64"
+instance Coercible Int where
+  type Ty Int = Iface "Int"
+
+class Coercibles xs (tys :: k) | xs -> tys
+instance Coercibles () ()
+instance (ty ~ Ty x, Coercible x, Coercibles xs tys) => Coercibles (x, xs) '(ty, tys)
+
+qqMarker
+  :: forall
+     -- k                -- the kind variable shows up in Core
+     (args_tys :: k)     -- JType's of arguments
+     tyres               -- JType of result
+     (input :: Symbol)   -- input string of the quasiquoter
+     (mname :: Symbol)   -- name of the method to generate
+     (antiqs :: Symbol)  -- antiquoted variables as a comma-separated list
+     (line :: Nat)       -- line number of the quasiquotation
+     args_tuple          -- uncoerced argument types
+     b.                  -- uncoerced result type
+     (tyres ~ Ty b, Coercibles args_tuple args_tys, Coercible b, HasCallStack)
+  => Proxy input
+  -> Proxy mname
+  -> Proxy antiqs
+  -> Proxy line
+  -> args_tuple
+  -> Proxy args_tys
+  -> IO b
+  -> IO b
+qqMarker = undefined
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index ba8b256217..79991a2cef 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -183,4 +183,5 @@ test('T14563', normal, compile_fail, [''])
 test('T14561', normal, compile_fail, [''])
 test('T14580', normal, compile_fail, [''])
 test('T14515', normal, compile, [''])
+test('T14723', normal, compile, [''])
 
diff --git a/testsuite/tests/typecheck/should_compile/T13651.hs b/testsuite/tests/typecheck/should_compile/T13651.hs
index 43ae633534..63bd88eb5c 100644
--- a/testsuite/tests/typecheck/should_compile/T13651.hs
+++ b/testsuite/tests/typecheck/should_compile/T13651.hs
@@ -12,3 +12,24 @@ foo :: (F cr cu ~ Bar h (Bar r u),
         F cu cs ~ Bar (Foo h) (Bar u s))
     => Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
 foo = undefined
+
+{-  Typechecking this program used to /just/ succeed in GHC 8.2,
+    (see Trac #14745 for why), but doesn't in 8.4.
+
+[G]  F cr cu ~ Bar h (Bar r u),
+     F cu cs ~ Bar (Foo h) (Bar u s))
+
+
+[W] F cr cu0 ~ Bar h (Bar r u)
+    --> (top-level fundeps)  cr ~ Bar h (Foo r)
+                             cu0 ~ Bar h (Foo u)
+        (local fundeps)      cu ~ cu0
+
+[W] F cu0 cs ~ Bar (Foo h) (Bar u s)
+    -->  (top-level fundeps)  cu0 ~ Bar (Foo h) (Foo u)
+                              cs  ~ Bar (Foo h) (Foo s)
+         (local fundeps)      cu0 ~ cu
+
+[W] F cr (Bar (Foo h) (Fo u)) ~ Bar h (Bar r u)
+
+-}
diff --git a/testsuite/tests/typecheck/should_compile/T13651.stderr b/testsuite/tests/typecheck/should_compile/T13651.stderr
new file mode 100644
index 0000000000..6b6c64302f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13651.stderr
@@ -0,0 +1,16 @@
+
+T13651.hs:11:8: error:
+    • Could not deduce: F cr (Bar (Foo h) (Foo u)) ~ Bar h (Bar r u)
+      from the context: (F cr cu ~ Bar h (Bar r u),
+                         F cu cs ~ Bar (Foo h) (Bar u s))
+        bound by the type signature for:
+                   foo :: forall cr cu h r u cs s.
+                          (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) =>
+                          Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
+        at T13651.hs:(11,8)-(13,65)
+    • In the ambiguity check for ‘foo’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature:
+        foo :: (F cr cu ~ Bar h (Bar r u),
+                F cu cs ~ Bar (Foo h) (Bar u s)) =>
+               Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs)
diff --git a/testsuite/tests/typecheck/should_compile/T13651a.hs b/testsuite/tests/typecheck/should_compile/T13651a.hs
new file mode 100644
index 0000000000..482231b6f2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13651a.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
+module T13651 where
+
+type family F r s = f | f -> r s
+
+type instance F (Bar h (Foo r)) (Bar h (Foo s)) = Bar h (Bar r s)
+
+data Bar s b
+data Foo a
+
+foo :: (F cr cu ~ Bar h (Bar r u),
+        F cu cs ~ Bar (Foo h) (Bar u s))
+    => Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> cu -> Foo (cr -> cs)
+    -- A variant of T13651 which fixes 'cu'
+    -- as well as the other type args
+foo = undefined
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 49df11b024..9e6898190d 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -561,7 +561,8 @@ test('T13594', normal, compile_fail, [''])
 test('T13603', normal, compile, [''])
 test('T13333', normal, compile, [''])
 test('T13585', [extra_files(['T13585.hs', 'T13585a.hs', 'T13585b.hs'])], run_command, ['$MAKE -s --no-print-directory T13585'])
-test('T13651', normal, compile, [''])
+test('T13651', normal, compile_fail, [''])
+test('T13651a', normal, compile, [''])
 test('T13680', normal, compile, [''])
 test('T13785', normal, compile, [''])
 test('T13804', normal, compile, [''])