Do not discard insolubles in implications

Trac #14000 showed up two errors

* In TcRnTypes.dropInsolubles we dropped all implications, which
  might contain the very insolubles we wanted to keep.  This was
  an outright error, and is why the out-of-scope error was actually
  lost altogether in Trac #14000

* In TcSimplify.simplifyInfer, if there are definite (insoluble)
  errors, it's better to suppress the following ambiguity test,
  because the type may be bogus anyway.  See TcSimplify
  Note [Quantification with errors].  This fix seems a bit clunky,
  but it'll do for now.

7 files changed, 52 insertions, 20 deletions

diff --git a/testsuite/tests/parser/should_fail/T7848.hs b/testsuite/tests/parser/should_fail/T7848.hs
index 25f0af7ee0..920f28e8c9 100644
--- a/testsuite/tests/parser/should_fail/T7848.hs
+++ b/testsuite/tests/parser/should_fail/T7848.hs
@@ -8,4 +8,4 @@ x (+) ((&)@z) ((:&&) a b) (c :&& d) (e `A` f) (A g h) = y
         y _ = (&)
         {-# INLINE (&) #-}
         {-# SPECIALIZE (&) :: a #-}
-        (&) = x
+        (&) = 'c'
diff --git a/testsuite/tests/parser/should_fail/T7848.stderr b/testsuite/tests/parser/should_fail/T7848.stderr
index 95ac7374ef..413920dbe6 100644
--- a/testsuite/tests/parser/should_fail/T7848.stderr
+++ b/testsuite/tests/parser/should_fail/T7848.stderr
@@ -1,13 +1,7 @@
 
-T7848.hs:6:1: error:
-    • Occurs check: cannot construct the infinite type:
-        t ~ p0 -> p1 -> A -> A -> A -> A -> p2 -> t
-    • Relevant bindings include x :: t (bound at T7848.hs:6:1)
-
 T7848.hs:10:9: error:
-    • Couldn't match expected type ‘t’ with actual type ‘a’
-        because type variable ‘a’ would escape its scope
-      This (rigid, skolem) type variable is bound by
+    • Couldn't match expected type ‘Char’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
         the type signature for:
           (&) :: forall a. a
         at T7848.hs:10:9-35
@@ -20,5 +14,4 @@ T7848.hs:10:9: error:
                 y _ = (&)
                 {-# INLINE (&) #-}
                 {-# SPECIALIZE (&) :: a #-}
-                (&) = x
-    • Relevant bindings include x :: t (bound at T7848.hs:6:1)
+                (&) = 'c'
diff --git a/testsuite/tests/th/T5358.stderr b/testsuite/tests/th/T5358.stderr
index 4bfc53a78e..b698bc1004 100644
--- a/testsuite/tests/th/T5358.stderr
+++ b/testsuite/tests/th/T5358.stderr
@@ -1,4 +1,24 @@
 
+T5358.hs:10:13: error:
+    • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
+    • The function ‘T5358.t1’ is applied to one argument,
+      but its type ‘Int’ has none
+      In the first argument of ‘(==)’, namely ‘T5358.t1 x’
+      In the expression: T5358.t1 x == T5358.t2 x
+    • Relevant bindings include
+        x :: t (bound at T5358.hs:10:9)
+        T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
+
+T5358.hs:10:21: error:
+    • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’
+    • The function ‘T5358.t2’ is applied to one argument,
+      but its type ‘Int’ has none
+      In the second argument of ‘(==)’, namely ‘T5358.t2 x’
+      In the expression: T5358.t1 x == T5358.t2 x
+    • Relevant bindings include
+        x :: t (bound at T5358.hs:10:9)
+        T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1)
+
 T5358.hs:14:12: error:
     • Exception when trying to run compile-time code:
         runTest called error: forall (t_0 :: *) . t_0 -> GHC.Types.Bool
diff --git a/testsuite/tests/typecheck/should_fail/T14000.hs b/testsuite/tests/typecheck/should_fail/T14000.hs
new file mode 100644
index 0000000000..854a78b6ad
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T14000.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+module T14000 where
+
+class C a where
+    type T a
+    c :: a -> T a
+
+foo = c noSuchThing   -- noSuchThing is not in scope
diff --git a/testsuite/tests/typecheck/should_fail/T14000.stderr b/testsuite/tests/typecheck/should_fail/T14000.stderr
new file mode 100644
index 0000000000..8b51e37641
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T14000.stderr
@@ -0,0 +1,2 @@
+
+T14000.hs:8:9: error: Variable not in scope: noSuchThing
diff --git a/testsuite/tests/typecheck/should_fail/T8142.stderr b/testsuite/tests/typecheck/should_fail/T8142.stderr
index aec8b3b55c..25d60d1aff 100644
--- a/testsuite/tests/typecheck/should_fail/T8142.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8142.stderr
@@ -1,16 +1,24 @@
 
-T8142.hs:6:18: error:
-    • Couldn't match type ‘Nu g0’ with ‘Nu g’
-      Expected type: Nu ((,) a) -> Nu g
+T8142.hs:6:10: error:
+    • Couldn't match type ‘Nu ((,) a0)’ with ‘c -> f c’
+      Expected type: (c -> f c) -> c -> f c
         Actual type: Nu ((,) a0) -> Nu g0
-      NB: ‘Nu’ is a type function, and may not be injective
-      The type variable ‘g0’ is ambiguous
-    • In the ambiguity check for the inferred type for ‘h’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      When checking the inferred type
-        h :: forall a (g :: * -> *). Nu ((,) a) -> Nu g
+      The type variable ‘a0’ is ambiguous
+    • In the expression: h
       In an equation for ‘tracer’:
           tracer
             = h
             where
                 h = (\ (_, b) -> ((outI . fmap h) b)) . out
+    • Relevant bindings include
+        tracer :: (c -> f c) -> c -> f c (bound at T8142.hs:6:1)
+
+T8142.hs:6:57: error:
+    • Couldn't match type ‘Nu ((,) a)’ with ‘g (Nu ((,) a))’
+      Expected type: Nu ((,) a) -> (a, g (Nu ((,) a)))
+        Actual type: Nu ((,) a) -> (a, Nu ((,) a))
+    • In the second argument of ‘(.)’, namely ‘out’
+      In the expression: (\ (_, b) -> ((outI . fmap h) b)) . out
+      In an equation for ‘h’: h = (\ (_, b) -> ((outI . fmap h) b)) . out
+    • Relevant bindings include
+        h :: Nu ((,) a) -> Nu g (bound at T8142.hs:6:18)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 3d2a595648..e31c7eea7e 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -452,3 +452,4 @@ test('T13610', normal, compile_fail, [''])
 test('T11672', normal, compile_fail, [''])
 test('T13819', normal, compile_fail, [''])
 test('T11963', normal, compile_fail, [''])
+test('T14000', normal, compile_fail, [''])