Be less picky about reporing inaccessible code

Triggered by the discussion on Trac #12466, this patch
makes GHC less aggressive about reporting an error when
there are insoluble Givens.

Being so agressive was making some libraries fail to
compile, and is arguably wrong in at least some cases.
See the discussion on the ticket.

Several test now pass when they failed before; see
the files-modified list for this patch.

18 files changed, 151 insertions, 115 deletions

diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 4f1c5db00d..b27e073082 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -447,7 +447,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     -- type checking to get a Lint error later
     report1 = [ ("custom_error", is_user_type_error,
                                                   True, mkUserTypeErrorReporter)
-              , ("insoluble1",   is_given_eq,     True, mkGroupReporter mkEqErr)
+              , ("insoluble1",   is_given_eq,     True, mkGivenErrorReporter)
               , ("insoluble2",   utterly_wrong,   True, mkGroupReporter mkEqErr)
               , ("skolem eq1",   very_wrong,      True, mkSkolReporter)
               , ("skolem eq2",   skolem_eq,       True, mkSkolReporter)
@@ -579,6 +579,77 @@ mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
                             Nothing  -> pprPanic "mkUserTypeError" (ppr ct)
 
 
+mkGivenErrorReporter :: Reporter
+-- See Note [Given errors]
+mkGivenErrorReporter ctxt cts
+  | Just implic <- find_gadt_match (cec_encl ctxt)
+  = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
+       ; dflags <- getDynFlags
+       ; let ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (ic_env implic))
+                   -- For given constraints we overwrite the env (and hence src-loc)
+                  -- with one from the implication.  See Note [Inaccessible code]
+
+             inaccessible_msg = hang (text "Inaccessible code in")
+                                   2 (ppr (ic_info implic))
+             report = important inaccessible_msg `mappend`
+                      relevant_bindings binds_msg
+
+       ; err <- mkEqErr_help dflags ctxt report ct'
+                             Nothing ty1 ty2
+
+       ; traceTc "mkGivenErrorRporter" (ppr ct)
+       ; maybeReportError ctxt err }
+
+  | otherwise   -- Discard Given errors that don't come from
+                -- a pattern match; maybe we should warn instead?
+  = do { traceTc "mkGivenErrorRporter no" (ppr ct $$ ppr (cec_encl ctxt))
+       ; return () }
+  where
+    (ct : _ )  = cts    -- Never empty
+    (ty1, ty2) = getEqPredTys (ctPred ct)
+
+    find_gadt_match [] = Nothing
+    find_gadt_match (implic : implics)
+      | PatSkol {} <- ic_info implic
+      , not (ic_no_eqs implic)
+      = Just implic
+      | otherwise
+      = find_gadt_match implics
+
+{- Note [Given errors]
+~~~~~~~~~~~~~~~~~~~~~~
+Given constaints reprsent things for which we have (or will have)
+evidence, so they aren't errors.  But if a Given constraint is
+insoluble, this code is inaccessible, and we might want to at least
+warn about that.  A classic case is
+
+   data T a where
+     T1 :: T Int
+     T2 :: T a
+     T3 :: T Bool
+
+   f :: T Int -> Bool
+   f T1 = ...
+   f T2 = ...
+   f T3 = ...  -- We want to report this case as inaccessible
+
+We'd like to point out that the T3 match is inaccessible. It
+will have a Given constraint [G] Int ~ Bool.
+
+But we don't want to report ALL insoluble Given constraints.  See Trac
+#12466 for a long discussion on.  For example, if we aren't careful
+we'll complain about
+   f :: ((Int ~ Bool) => a -> a) -> Int
+which arguably is OK.  It's more debatable for
+   g :: (Int ~ Bool) => Int -> Int
+but it's tricky to distinguish these cases to we don't report
+either.
+
+The bottom line is this: find_gadt_match looks for an encosing
+pattern match which binds some equality constraints.  If we
+find one, we report the insoluble Given.
+-}
+
 mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
                              -- Make error message for a group
                 -> Reporter  -- Deal with lots of constraints
@@ -1170,17 +1241,8 @@ mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
 mkEqErr _ [] = panic "mkEqErr"
 
 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
-mkEqErr1 ctxt ct
-  | arisesFromGivens ct
-  = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
-       ; let (given_loc, given_msg) = mk_given (ctLoc ct) (cec_encl ctxt)
-       ; dflags <- getDynFlags
-       ; let report = important given_msg `mappend` relevant_bindings binds_msg
-       ; mkEqErr_help dflags ctxt report
-                      (setCtLoc ct given_loc) -- Note [Inaccessible code]
-                      Nothing ty1 ty2 }
-
-  | otherwise   -- Wanted or derived
+mkEqErr1 ctxt ct   -- Wanted or derived;
+                   -- givens handled in mkGivenErrorReporter
   = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
        ; rdr_env <- getGlobalRdrEnv
        ; fam_envs <- tcGetFamInstEnvs
@@ -1200,14 +1262,6 @@ mkEqErr1 ctxt ct
   where
     (ty1, ty2) = getEqPredTys (ctPred ct)
 
-    mk_given :: CtLoc -> [Implication] -> (CtLoc, SDoc)
-    -- For given constraints we overwrite the env (and hence src-loc)
-    -- with one from the implication.  See Note [Inaccessible code]
-    mk_given loc []           = (loc, empty)
-    mk_given loc (implic : _) = (setCtLocEnv loc (ic_env implic)
-                                , hang (text "Inaccessible code in")
-                                     2 (ppr (ic_info implic)))
-
        -- If the types in the error message are the same as the types
        -- we are unifying, don't add the extra expected/actual message
     mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 7da1939748..f6b72eb812 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -1774,19 +1774,23 @@ isInInertEqs eqs tv rhs
       , rhs `eqType` rhs2 = True
       | otherwise         = False
 
-getNoGivenEqs :: TcLevel     -- TcLevel of this implication
+getNoGivenEqs :: TcLevel          -- TcLevel of this implication
                -> [TcTyVar]       -- Skolems of this implication
+               -> Cts             -- Given insolubles from solveGivens
                -> TcS Bool        -- True <=> definitely no residual given equalities
 -- See Note [When does an implication have given equalities?]
-getNoGivenEqs tclvl skol_tvs
-  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds, inert_funeqs = funeqs })
+getNoGivenEqs tclvl skol_tvs given_insols
+  = do { inerts@(IC { inert_eqs = ieqs, inert_irreds = iirreds
+                    , inert_funeqs = funeqs })
              <- getInertCans
        ; let local_fsks = foldFunEqs add_fsk funeqs emptyVarSet
 
-             has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence)  False iirreds
+             has_given_eqs = foldrBag ((||) . ev_given_here . ctEvidence) False
+                                      (iirreds `unionBags` given_insols)
                           || anyDVarEnv (eqs_given_here local_fsks) ieqs
 
-       ; traceTcS "getNoGivenEqs" (vcat [ppr has_given_eqs, ppr inerts])
+       ; traceTcS "getNoGivenEqs" (vcat [ ppr has_given_eqs, ppr inerts
+                                        , ppr given_insols])
        ; return (not has_given_eqs) }
   where
     eqs_given_here :: VarSet -> EqualCtList -> Bool
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 6ebf9f1f85..d64bc08879 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -1254,7 +1254,7 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
                         -- we want to retain derived equalities so we can float
                         -- them out in floatEqualities
 
-                  ; no_eqs <- getNoGivenEqs tclvl skols
+                  ; no_eqs <- getNoGivenEqs tclvl skols given_insols
                         -- Call getNoGivenEqs /after/ solveWanteds, because
                         -- solveWanteds can augment the givens, via expandSuperClasses,
                         -- to reveal given superclass equalities
diff --git a/testsuite/tests/ghci/scripts/Defer02.script b/testsuite/tests/ghci/scripts/Defer02.script
index 3ff0bee911..732a1ce1b1 100755
--- a/testsuite/tests/ghci/scripts/Defer02.script
+++ b/testsuite/tests/ghci/scripts/Defer02.script
@@ -1,5 +1,8 @@
 -- Test -fwarn-type-errors
 -- This test shows how each error is printed at runtime
+-- Bizarrely Defer01.hs seems to be in typecheck/should_run
+--  I can't see how ghci finds it!
+
 :l Defer01
 t5624
 print a
diff --git a/testsuite/tests/ghci/scripts/Defer02.stderr b/testsuite/tests/ghci/scripts/Defer02.stderr
index f4830894b5..b9764c3b7b 100644
--- a/testsuite/tests/ghci/scripts/Defer02.stderr
+++ b/testsuite/tests/ghci/scripts/Defer02.stderr
@@ -41,8 +41,7 @@ Defer01.hs:31:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
       but its type ‘Char’ has none
       In the expression: e 'q'
       In an equation for ‘f’: f = e 'q'
-    • Relevant bindings include
-        f :: t (bound at Defer01.hs:31:1)
+    • Relevant bindings include f :: t (bound at Defer01.hs:31:1)
 
 Defer01.hs:34:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match expected type ‘Char’ with actual type ‘a’
@@ -55,8 +54,7 @@ Defer01.hs:34:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In an equation for ‘h’: h x = (x, 'c')
     • Relevant bindings include
         x :: a (bound at Defer01.hs:34:3)
-        h :: a -> (Char, Char)
-          (bound at Defer01.hs:34:1)
+        h :: a -> (Char, Char) (bound at Defer01.hs:34:1)
 
 Defer01.hs:39:17: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match expected type ‘Bool’ with actual type ‘T a’
@@ -86,26 +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:45:1: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    Couldn't match type ‘Int’ with ‘Bool’
-    Inaccessible code in
-      the type signature for:
-        k :: Int ~ Bool => Int -> Bool
-
-Defer01.hs:45:6: warning: [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘Int’ with ‘Bool’
-      Inaccessible code in
-        the type signature for:
-          k :: Int ~ Bool => Int -> Bool
-    • In the ambiguity check for ‘k’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature: k :: (Int ~ Bool) => Int -> Bool
-
-Defer01.hs:46:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+Defer01.hs:47:1: warning: [-Woverlapping-patterns (in -Wdefault)]
     Pattern match is redundant
     In an equation for ‘k’: k x = ...
 
-Defer01.hs:49:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
+Defer01.hs:50:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match expected type ‘IO a0’
                   with actual type ‘Char -> IO ()’
     • Probable cause: ‘putChar’ is applied to too few arguments
@@ -131,7 +114,7 @@ Defer01.hs:49:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In an equation for ‘b’: b x = x == x
 (deferred type error)
 
-<interactive>:7:11: error:
+<interactive>:10:11: error:
     • Couldn't match type ‘Bool’ with ‘Int’
       Expected type: C Int
         Actual type: C Bool
@@ -150,8 +133,7 @@ Defer01.hs:49:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
       but its type ‘Char’ has none
       In the expression: e 'q'
       In an equation for ‘f’: f = e 'q'
-    • Relevant bindings include
-        f :: t (bound at Defer01.hs:31:1)
+    • Relevant bindings include f :: t (bound at Defer01.hs:31:1)
 (deferred type error)
 *** Exception: Defer01.hs:34:8: error:
     • Couldn't match expected type ‘Char’ with actual type ‘a’
@@ -164,8 +146,7 @@ Defer01.hs:49:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In an equation for ‘h’: h x = (x, 'c')
     • Relevant bindings include
         x :: a (bound at Defer01.hs:34:3)
-        h :: a -> (Char, Char)
-          (bound at Defer01.hs:34:1)
+        h :: a -> (Char, Char) (bound at Defer01.hs:34:1)
 (deferred type error)
 *** Exception: Defer01.hs:39:17: error:
     • Couldn't match expected type ‘Bool’ with actual type ‘T a’
@@ -182,12 +163,12 @@ Defer01.hs:49:5: warning: [-Wdeferred-type-errors (in -Wdefault)]
       In an equation for ‘j’: j = myOp 23
 (deferred type error)
 
-<interactive>:13:8: error:
+<interactive>:16:8: error:
     • Couldn't match type ‘Int’ with ‘Bool’ arising from a use of ‘k’
     • In the first argument of ‘print’, namely ‘(k 2)’
       In the expression: print (k 2)
       In an equation for ‘it’: it = print (k 2)
-*** Exception: Defer01.hs:49:5: error:
+*** Exception: Defer01.hs:50:5: error:
     • Couldn't match expected type ‘IO a0’
                   with actual type ‘Char -> IO ()’
     • Probable cause: ‘putChar’ is applied to too few arguments
diff --git a/testsuite/tests/typecheck/should_compile/T12466.hs b/testsuite/tests/typecheck/should_compile/T12466.hs
new file mode 100644
index 0000000000..7940d99a59
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12466.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+module T12466 where
+
+class Foo a where
+  foo :: (a ~ Int => Int) -> a -> a
+  foo _ a2 = a2
+
+instance Foo Char
diff --git a/testsuite/tests/typecheck/should_compile/T12466a.hs b/testsuite/tests/typecheck/should_compile/T12466a.hs
new file mode 100644
index 0000000000..d0749e6b0a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T12466a.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module T12466a where
+
+import GHC.TypeLits (Nat)
+import Unsafe.Coerce (unsafeCoerce)
+
+data Dict a where
+  Dict :: a => Dict a
+
+newtype a :- b = Sub (a => Dict b)
+
+axiom :: forall a b. Dict (a ~ b)
+axiom = unsafeCoerce (Dict :: Dict (a ~ a))
+
+type Divides n m = n ~ Gcd n m
+type family Gcd :: Nat -> Nat -> Nat where
+
+dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)
+dividesGcd = Sub axiom
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index b9f452d15c..40d986a617 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -539,3 +539,5 @@ test('T12381', normal, compile, [''])
 test('T12082', normal, compile, [''])
 test('T10635', normal, compile, [''])
 test('T12170b', normal, compile, [''])
+test('T12466', normal, compile, [''])
+test('T12466a', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/FDsFromGivens.hs b/testsuite/tests/typecheck/should_fail/FDsFromGivens.hs
index 591c3bcca9..6e1b34d6c6 100644
--- a/testsuite/tests/typecheck/should_fail/FDsFromGivens.hs
+++ b/testsuite/tests/typecheck/should_fail/FDsFromGivens.hs
@@ -6,6 +6,7 @@ class C a b | a -> b where
    cop :: a -> b -> ()
 
 {- Failing, as it righteously should! It's inaccessible code -}
+-- But (c.f. test T5236) we no longer reject this (see Trac #12466)
 g1 :: (C Char [a], C Char Bool) => a -> ()
 g1 x = ()
 
diff --git a/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr b/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
index 5d137aa3d1..e69de29bb2 100644
--- a/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
+++ b/testsuite/tests/typecheck/should_fail/FDsFromGivens.stderr
@@ -1,19 +0,0 @@
-
-FDsFromGivens.hs:9:7: error:
-    • Couldn't match type ‘[a]’ with ‘Bool’
-        arising from a functional dependency between constraints:
-          ‘C Char Bool’
-            arising from the type signature for:
-                           g1 :: (C Char [a], C Char Bool) => a -> ()
-            at FDsFromGivens.hs:9:7-42
-          ‘C Char [a]’
-            arising from the type signature for:
-                           g1 :: (C Char [a], C Char Bool) => a -> ()
-            at FDsFromGivens.hs:9:7-42
-      Inaccessible code in
-        the type signature for:
-          g1 :: (C Char [a], C Char Bool) => a -> ()
-    • In the ambiguity check for ‘g1’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature:
-        g1 :: (C Char [a], C Char Bool) => a -> ()
diff --git a/testsuite/tests/typecheck/should_fail/T10715.hs b/testsuite/tests/typecheck/should_fail/T10715.hs
index 969abd5cf2..c48402ffd2 100644
--- a/testsuite/tests/typecheck/should_fail/T10715.hs
+++ b/testsuite/tests/typecheck/should_fail/T10715.hs
@@ -6,5 +6,11 @@ import Data.Ord ( Down )  -- convenient newtype
 
 data X a
 
+-- See Trac #10715 for a long discussion about whether
+-- this shoudl be accepted or not.
+--
+-- But in Trac #12466 we decided to accept contradictory
+-- type signatures, so definition is now accepeted even
+-- though you can never call it.
 doCoerce :: Coercible a (X a) => a -> X a
 doCoerce = coerce
diff --git a/testsuite/tests/typecheck/should_fail/T10715.stderr b/testsuite/tests/typecheck/should_fail/T10715.stderr
index 19bc1b9af3..e69de29bb2 100644
--- a/testsuite/tests/typecheck/should_fail/T10715.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10715.stderr
@@ -1,13 +0,0 @@
-
-T10715.hs:9:13: error:
-    • Couldn't match representation of type ‘a’ with that of ‘X a’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          doCoerce :: forall a. Coercible a (X a) => a -> X a
-        at T10715.hs:9:13-41
-      Inaccessible code in
-        the type signature for:
-          doCoerce :: Coercible a (X a) => a -> X a
-    • In the ambiguity check for ‘doCoerce’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature: doCoerce :: Coercible a (X a) => a -> X a
diff --git a/testsuite/tests/typecheck/should_fail/T5236.hs b/testsuite/tests/typecheck/should_fail/T5236.hs
index bbef9bb187..f32c06dcdb 100644
--- a/testsuite/tests/typecheck/should_fail/T5236.hs
+++ b/testsuite/tests/typecheck/should_fail/T5236.hs
@@ -10,6 +10,9 @@ class Id a b | a -> b, b -> a
 instance Id A A
 instance Id B B
 
+-- The fundeps mean that this type signature
+-- has a (derived) insoluble Given, A~B, but
+-- we now ignore that (Trac #12466)
 loop :: Id A B => Bool
 loop = True
 
diff --git a/testsuite/tests/typecheck/should_fail/T5236.stderr b/testsuite/tests/typecheck/should_fail/T5236.stderr
index 4a21aba79d..e69de29bb2 100644
--- a/testsuite/tests/typecheck/should_fail/T5236.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5236.stderr
@@ -1,15 +0,0 @@
-
-T5236.hs:13:9: error:
-    • Couldn't match type ‘B’ with ‘A’
-        arising from a functional dependency between:
-          constraint ‘Id A B’
-            arising from the type signature for:
-                           loop :: Id A B => Bool
-          instance ‘Id B B’ at T5236.hs:11:10-15
-      Inaccessible code in
-        the type signature for:
-          loop :: Id A B => Bool
-    • In the ambiguity check for ‘loop’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature:
-        loop :: Id A B => Bool
diff --git a/testsuite/tests/typecheck/should_fail/T8392a.hs b/testsuite/tests/typecheck/should_fail/T8392a.hs
index 6f47b4e331..2ae23380a2 100644
--- a/testsuite/tests/typecheck/should_fail/T8392a.hs
+++ b/testsuite/tests/typecheck/should_fail/T8392a.hs
@@ -2,6 +2,8 @@
 module T8392a where
 
 -- Should complain even with AllowAmbiguousTypes
-
+--
+-- But (Trac #12466) we now don't complain about
+-- contradictory signatures
 foo :: (Int ~ Bool) => a -> a
 foo x = x
diff --git a/testsuite/tests/typecheck/should_fail/T8392a.stderr b/testsuite/tests/typecheck/should_fail/T8392a.stderr
index df53c22bda..e69de29bb2 100644
--- a/testsuite/tests/typecheck/should_fail/T8392a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8392a.stderr
@@ -1,9 +0,0 @@
-
-T8392a.hs:6:8: error:
-    • Couldn't match type ‘Int’ with ‘Bool’
-      Inaccessible code in
-        the type signature for:
-          foo :: Int ~ Bool => a -> a
-    • In the ambiguity check for ‘foo’
-      In the type signature:
-        foo :: (Int ~ Bool) => a -> a
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index eda6a9f23d..62734f861c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -253,7 +253,7 @@ test('SilentParametersOverlapping', normal, compile, [''])
 test('FailDueToGivenOverlapping', normal, compile_fail, [''])
 test('LongWayOverlapping', normal, compile_fail, [''])
 test('T5051', normal, compile, [''])
-test('T5236',normal,compile_fail,[''])
+test('T5236',normal,compile,[''])
 test('T5246',normal,compile_fail,[''])
 test('T5300',normal,compile_fail,[''])
 test('T5095',normal,compile_fail,[''])
@@ -287,7 +287,7 @@ test('T6018fail', extra_clean([ 'T6018fail.hi' , 'T6018fail.o'
 test('T6018failclosed', normal, compile_fail, [''])
 test('T6018failclosed2', normal, compile_fail, [''])
 test('T6078', normal, compile_fail, [''])
-test('FDsFromGivens', normal, compile_fail, [''])
+test('FDsFromGivens', normal, compile, [''])
 test('FDsFromGivens2', normal, compile_fail, [''])
 test('T7019', normal, compile_fail,[''])
 test('T7019a', normal, compile_fail,[''])
@@ -335,7 +335,7 @@ test('TcCoercibleFail', [when(compiler_debugged(), skip)], compile_fail, [''])
 test('TcCoercibleFail2', [], compile_fail, [''])
 test('TcCoercibleFail3', [], compile_fail, [''])
 test('T8306', normal, compile_fail, [''])
-test('T8392a', normal, compile_fail, [''])
+test('T8392a', normal, compile, [''])
 test('T8428', normal, compile_fail, [''])
 test('T8450', normal, compile_fail, [''])
 test('T8514', normal, compile_fail, [''])
@@ -389,7 +389,7 @@ test('ExpandSynsFail3', normal, compile_fail, ['-fprint-expanded-synonyms'])
 test('ExpandSynsFail4', normal, compile_fail, ['-fprint-expanded-synonyms'])
 test('T10698', expect_broken(10698), compile_fail, [''])
 test('T10836', normal, compile_fail, [''])
-test('T10715', normal, compile_fail, [''])
+test('T10715', normal, compile, [''])
 test('T10715b', normal, compile_fail, [''])
 test('T10971b', normal, compile_fail, [''])
 test('T10971d', extra_clean(['T10971c.hi', 'T10971c.o']), multimod_compile_fail, ['T10971d','-v0'])
diff --git a/testsuite/tests/typecheck/should_run/Defer01.hs b/testsuite/tests/typecheck/should_run/Defer01.hs
index f6c69dcfa7..135fd837ca 100644
--- a/testsuite/tests/typecheck/should_run/Defer01.hs
+++ b/testsuite/tests/typecheck/should_run/Defer01.hs
@@ -42,6 +42,7 @@ class MyClass a where myOp :: a -> String
 
 j = myOp 23 -- Two errors, should not combine them
 
+-- No longer reported as an error: Trac #12466
 k :: (Int ~ Bool) => Int -> Bool
 k x = x