Fix error-message suppress on given equalities

I'd got the logic slightly wrong when reporting type errors
for insoluble 'given' equalities.  We suppress insoluble givens
under some circumstances (see Note [Given errors]), but we then
suppressed subsequent 'wanted' errors because the (suppressed)
'given' error "won".  Result: no errors at all :-(.

This patch fixes it and
 - Renames TcType.isTyVarUnderDatatype to the more
   perspicuous TcType.isInsolubleOccursCheck

In doing this I realise that I don't understand why we need
to keep the insolubles partitioned out separately at all...
but that is for another day.

10 files changed, 101 insertions, 27 deletions

diff --git a/testsuite/tests/ghci/scripts/Defer02.stderr b/testsuite/tests/ghci/scripts/Defer02.stderr
index 527a987d7d..5aa67f06c3 100644
--- a/testsuite/tests/ghci/scripts/Defer02.stderr
+++ b/testsuite/tests/ghci/scripts/Defer02.stderr
@@ -84,6 +84,11 @@ Defer01.hs:43:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In the expression: myOp 23
       In an equation for ‘j’: j = myOp 23
 
+Defer01.hs:47:7: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘Bool’ with actual type ‘Int’
+    • In the expression: x
+      In an equation for ‘k’: k x = x
+
 Defer01.hs:50:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match expected type ‘IO a0’
                   with actual type ‘Char -> IO ()’
diff --git a/testsuite/tests/indexed-types/should_fail/T2627b.stderr b/testsuite/tests/indexed-types/should_fail/T2627b.stderr
index 63f11b97f1..1a09bd8ef7 100644
--- a/testsuite/tests/indexed-types/should_fail/T2627b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2627b.stderr
@@ -1,9 +1,13 @@
 
 T2627b.hs:20:24: error:
-    • Occurs check: cannot construct the infinite type:
-        b0 ~ Dual (Dual b0)
+    • Couldn't match type ‘b0’ with ‘Dual (Dual b0)’
         arising from a use of ‘conn’
-      The type variable ‘b0’ is ambiguous
+        ‘b0’ is untouchable
+          inside the constraints: b ~ W e f
+          bound by a pattern with constructor:
+                     Wr :: forall e f. e -> Comm f -> Comm (W e f),
+                   in an equation for ‘conn’
+          at T2627b.hs:20:14-19
     • In the expression: conn undefined undefined
       In an equation for ‘conn’:
           conn (Rd k) (Wr a r) = conn undefined undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T5934.stderr b/testsuite/tests/indexed-types/should_fail/T5934.stderr
index 20b16b273b..e303e54f74 100644
--- a/testsuite/tests/indexed-types/should_fail/T5934.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5934.stderr
@@ -1,6 +1,20 @@
 
 T5934.hs:12:7: error:
-    • Couldn't match expected type ‘(forall s. GenST s) -> Int’
-                  with actual type ‘Integer’
+    • Cannot instantiate unification variable ‘a0’
+      with a type involving foralls: (forall s. GenST s) -> Int
+        GHC doesn't yet support impredicative polymorphism
+    • In the expression: 0
+      In an equation for ‘run’: run = 0
+
+T5934.hs:12:7: error:
+    • Ambiguous type variable ‘a0’ arising from the literal ‘0’
+      prevents the constraint ‘(Num a0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘a0’ should be.
+      These potential instances exist:
+        instance Num Integer -- Defined in ‘GHC.Num’
+        instance Num Double -- Defined in ‘GHC.Float’
+        instance Num Float -- Defined in ‘GHC.Float’
+        ...plus two others
+        (use -fprint-potential-instances to see them all)
     • In the expression: 0
       In an equation for ‘run’: run = 0
diff --git a/testsuite/tests/indexed-types/should_fail/T6123.stderr b/testsuite/tests/indexed-types/should_fail/T6123.stderr
index 0ae1a5e3c1..eafd27c454 100644
--- a/testsuite/tests/indexed-types/should_fail/T6123.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T6123.stderr
@@ -1,7 +1,6 @@
 
 T6123.hs:10:14: error:
-    • Occurs check: cannot construct the infinite type: a0 ~ Id a0
-        arising from a use of ‘cid’
+    • Couldn't match type ‘a0’ with ‘Id a0’ arising from a use of ‘cid’
       The type variable ‘a0’ is ambiguous
     • In the expression: cid undefined
       In an equation for ‘cundefined’: cundefined = cid undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T7354.stderr b/testsuite/tests/indexed-types/should_fail/T7354.stderr
index b7b70b8f4e..f4c3c0d37f 100644
--- a/testsuite/tests/indexed-types/should_fail/T7354.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7354.stderr
@@ -1,7 +1,8 @@
 
 T7354.hs:28:11: error:
-    • Occurs check: cannot construct the infinite type:
-        p ~ Base t (Prim [p] p)
+    • Couldn't match type ‘p’ with ‘Base t (Prim [p] p)’
+      ‘p’ is a rigid type variable bound by
+        the inferred type of foo :: Prim [p] p -> t at T7354.hs:28:1-13
       Expected type: Prim [p] p -> Base t (Prim [p] p)
         Actual type: Prim [p] p -> p
     • In the first argument of ‘ana’, namely ‘alg’
diff --git a/testsuite/tests/typecheck/should_compile/T12427a.stderr b/testsuite/tests/typecheck/should_compile/T12427a.stderr
index fc2aece398..05e926067f 100644
--- a/testsuite/tests/typecheck/should_compile/T12427a.stderr
+++ b/testsuite/tests/typecheck/should_compile/T12427a.stderr
@@ -2,15 +2,8 @@
 T12427a.hs:17:29: error:
     • Couldn't match expected type ‘p’
                   with actual type ‘(forall b. [b] -> [b]) -> Int’
-        ‘p’ is untouchable
-          inside the constraints: ()
-          bound by a pattern with constructor:
-                     T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T,
-                   in a case alternative
-          at T12427a.hs:17:19-24
       ‘p’ is a rigid type variable bound by
         the inferred type of h11 :: T -> p at T12427a.hs:17:1-29
-      Possible fix: add a type signature for ‘h11’
     • In the expression: v
       In a case alternative: T1 _ v -> v
       In the expression: case y of { T1 _ v -> v }
@@ -18,16 +11,8 @@ T12427a.hs:17:29: error:
         h11 :: T -> p (bound at T12427a.hs:17:1)
 
 T12427a.hs:28:6: error:
-    • Couldn't match expected type ‘p’
-                  with actual type ‘(forall b. [b] -> [b]) -> Int’
-        ‘p’ is untouchable
-          inside the constraints: ()
-          bound by a pattern with constructor:
-                     T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T,
-                   in a pattern binding
-          at T12427a.hs:28:1-7
-      ‘p’ is a rigid type variable bound by
-        the inferred type of x1 :: p at T12427a.hs:28:1-19
-      Possible fix: add a type signature for ‘x1’
+    • Cannot instantiate unification variable ‘p0’
+      with a type involving foralls: (forall b. [b] -> [b]) -> Int
+        GHC doesn't yet support impredicative polymorphism
     • In the pattern: T1 _ x1
       In a pattern binding: T1 _ x1 = undefined
diff --git a/testsuite/tests/typecheck/should_fail/T12589.stderr b/testsuite/tests/typecheck/should_fail/T12589.stderr
index a2587e2778..f77d6457b9 100644
--- a/testsuite/tests/typecheck/should_fail/T12589.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12589.stderr
@@ -1,2 +1,11 @@
 
 T12589.hs:13:3: error: Variable not in scope: (&) :: t0 -> t1 -> t
+
+T12589.hs:13:5: error:
+    • Cannot instantiate unification variable ‘t1’
+      with a type involving foralls:
+        (forall a. Bounded a => f0 a) -> h0 f0 xs0
+        GHC doesn't yet support impredicative polymorphism
+    • In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’
+      In the expression: (&) minBound hcpure (Proxy @Bounded)
+      In an equation for ‘a’: a = (&) minBound hcpure (Proxy @Bounded)
diff --git a/testsuite/tests/typecheck/should_fail/T13446.hs b/testsuite/tests/typecheck/should_fail/T13446.hs
new file mode 100644
index 0000000000..11a60776f6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13446.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{- # OPTIONS_GHC -fno-defer-type-errors #-}
+module T13446 where
+
+import Data.Coerce (Coercible)
+import GHC.Exts (Constraint)
+import GHC.TypeLits (Symbol)
+
+data Dict :: Constraint -> * where
+  Dict :: a => Dict a
+
+infixr 9 :-
+newtype a :- b = Sub (a => Dict b)
+instance a => Show (a :- b) where
+  showsPrec d (Sub Dict) = showParen (d > 10) $ showString "Sub Dict"
+
+class Lifting p f where
+  lifting :: p a :- p (f a)
+
+data Blah a = Blah
+
+newtype J (a :: JType) = J (Blah (J a))
+newtype JComparable a = JComparable (J (T (JTy a)))
+
+instance Lifting JReference JComparable where
+  lifting = Sub 'a'
+
+class (Coercible a (J (JTy a))) => JReference a where
+  type JTy a :: JType
+
+type T a
+  = 'Generic ('Iface "java.lang.Comparable") '[a]
+data JType = Class Symbol
+           | Generic JType [JType]
+           | Iface Symbol
+type JObject = J (Class "java.lang.Object")
+instance JReference JObject where
+  type JTy JObject = 'Class "java.lang.Object"
diff --git a/testsuite/tests/typecheck/should_fail/T13446.stderr b/testsuite/tests/typecheck/should_fail/T13446.stderr
new file mode 100644
index 0000000000..a0308f8be2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13446.stderr
@@ -0,0 +1,10 @@
+
+T13446.hs:34:17: error:
+    • Couldn't match expected type ‘Dict (JReference (JComparable a))’
+                  with actual type ‘Char’
+    • In the first argument of ‘Sub’, namely ‘'a'’
+      In the expression: Sub 'a'
+      In an equation for ‘lifting’: lifting = Sub 'a'
+    • Relevant bindings include
+        lifting :: JReference a :- JReference (JComparable a)
+          (bound at T13446.hs:34:3)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 13ea1d7a41..8fbe14111a 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -430,3 +430,4 @@ test('LevPolyBounded', normal, compile_fail, [''])
 test('T13292', normal, multimod_compile, ['T13292', '-v0 -fdefer-type-errors'])
 test('T13300', normal, compile_fail, [''])
 test('T12709', normal, compile_fail, [''])
+test('T13446', normal, compile_fail, [''])