Better error reporting for inaccessible code

This patch fixes Trac #15558.  There turned out to be
two distinct problems

* In TcExpr.tc_poly_expr_nc we had

    tc_poly_expr_nc (L loc expr) res_ty
      = do { traceTc "tcPolyExprNC" (ppr res_ty)
           ; (wrap, expr')
               <- tcSkolemiseET GenSigCtxt res_ty $ \ res_ty ->
                  setSrcSpan loc $
                    -- NB: setSrcSpan *after* skolemising,
                    -- so we get better skolem locations
                  tcExpr expr res_ty

  Putting the setSrcSpan inside the tcSkolemise means that
  the location on the Implication constraint is the /call/
  to the function rather than the /argument/ to the call,
  and that is really quite wrong.

  I don't know what Richard's comment NB means -- I moved the
  setSrcSpan outside, and the "binding site" info in error
  messages actually improved.

  The reason I found this is that it affects the span reported
  for Trac #15558.

* In TcErrors.mkGivenErrorReporter we carefully munge the location
  for an insoluble Given constraint (Note [Inaccessible code]).
  But the 'implic' passed in wasn't necesarily the immediately-
  enclosing implication -- but for location-munging purposes
  it jolly well should be.

  Solution: use the innermost implication. This actually
  simplifies the code -- no need to pass an implication in to
  mkGivenErrorReporter.

9 files changed, 58 insertions, 30 deletions

diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 06b660f193..87b853f42e 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -614,25 +614,28 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
     is_irred _ (IrredPred {}) = True
     is_irred _ _              = False
 
-    given_eq_spec = case find_gadt_match (cec_encl ctxt) of
-       Just imp -> ("insoluble1a", is_given_eq, True,  mkGivenErrorReporter imp)
-       Nothing  -> ("insoluble1b", is_given_eq, False, ignoreErrorReporter)
-                  -- False means don't suppress subsequent errors
-                  -- Reason: we don't report all given errors
-                  --         (see mkGivenErrorReporter), and we should only suppress
-                  --         subsequent errors if we actually report this one!
-                  --         Trac #13446 is an example
-
-    find_gadt_match [] = Nothing
-    find_gadt_match (implic : implics)
+    given_eq_spec  -- See Note [Given errors]
+      | has_gadt_match (cec_encl ctxt)
+      = ("insoluble1a", is_given_eq, True,  mkGivenErrorReporter)
+      | otherwise
+      = ("insoluble1b", is_given_eq, False, ignoreErrorReporter)
+          -- False means don't suppress subsequent errors
+          -- Reason: we don't report all given errors
+          --         (see mkGivenErrorReporter), and we should only suppress
+          --         subsequent errors if we actually report this one!
+          --         Trac #13446 is an example
+
+    -- See Note [Given errors]
+    has_gadt_match [] = False
+    has_gadt_match (implic : implics)
       | PatSkol {} <- ic_info implic
       , not (ic_no_eqs implic)
       , wopt Opt_WarnInaccessibleCode (implicDynFlags implic)
           -- Don't bother doing this if -Winaccessible-code isn't enabled.
           -- See Note [Avoid -Winaccessible-code when deriving] in TcInstDcls.
-      = Just implic
+      = True
       | otherwise
-      = find_gadt_match implics
+      = has_gadt_match implics
 
 ---------------
 isSkolemTy :: TcLevel -> Type -> Bool
@@ -701,14 +704,17 @@ mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
                             Nothing  -> pprPanic "mkUserTypeError" (ppr ct)
 
 
-mkGivenErrorReporter :: Implication -> Reporter
+mkGivenErrorReporter :: Reporter
 -- See Note [Given errors]
-mkGivenErrorReporter implic ctxt cts
+mkGivenErrorReporter ctxt cts
   = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
        ; dflags <- getDynFlags
-       ; let ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (implicLclEnv implic))
+       ; let (implic:_) = cec_encl ctxt
+                 -- Always non-empty when mkGivenErrorReporter is called
+             ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (implicLclEnv implic))
                    -- For given constraints we overwrite the env (and hence src-loc)
-                  -- with one from the implication.  See Note [Inaccessible code]
+                   -- with one from the immediately-enclosing implication.
+                   -- See Note [Inaccessible code]
 
              inaccessible_msg = hang (text "Inaccessible code in")
                                    2 (ppr (ic_info implic))
@@ -761,7 +767,7 @@ which arguably is OK.  It's more debatable for
 but it's tricky to distinguish these cases so we don't report
 either.
 
-The bottom line is this: find_gadt_match looks for an enclosing
+The bottom line is this: has_gadt_match looks for an enclosing
 pattern match which binds some equality constraints.  If we
 find one, we report the insoluble Given.
 -}
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 30b46c74bd..b70276da7e 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -110,12 +110,10 @@ tc_poly_expr expr res_ty
     do { traceTc "tcPolyExpr" (ppr res_ty); tc_poly_expr_nc expr res_ty }
 
 tc_poly_expr_nc (L loc expr) res_ty
-  = do { traceTc "tcPolyExprNC" (ppr res_ty)
+  = setSrcSpan loc $
+    do { traceTc "tcPolyExprNC" (ppr res_ty)
        ; (wrap, expr')
            <- tcSkolemiseET GenSigCtxt res_ty $ \ res_ty ->
-              setSrcSpan loc $
-                -- NB: setSrcSpan *after* skolemising, so we get better
-                -- skolem locations
               tcExpr expr res_ty
        ; return $ L loc (mkHsWrap wrap expr') }
 
diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr
index 3f5eb9825a..8ece51029b 100644
--- a/testsuite/tests/dependent/should_fail/T14066d.stderr
+++ b/testsuite/tests/dependent/should_fail/T14066d.stderr
@@ -4,7 +4,7 @@ T14066d.hs:11:35: error:
       ‘b1’ is a rigid type variable bound by
         a type expected by the context:
           forall c b1 (a :: c). (Proxy a, Proxy c, b1)
-        at T14066d.hs:11:33-35
+        at T14066d.hs:11:35
       ‘b’ is a rigid type variable bound by
         the type signature for:
           f :: forall b. b -> (Proxy Maybe, ())
diff --git a/testsuite/tests/gadt/T15558.hs b/testsuite/tests/gadt/T15558.hs
new file mode 100644
index 0000000000..91dff3f956
--- /dev/null
+++ b/testsuite/tests/gadt/T15558.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+module T15558 where
+
+data T a where
+  MkT :: T Int
+
+data Foo a = MkFoo ((a ~ Bool) => ())
+
+f :: T a -> Foo a
+f MkT = MkFoo ()
+
+-- g :: Foo Int
+-- g = f MkT
diff --git a/testsuite/tests/gadt/T15558.stderr b/testsuite/tests/gadt/T15558.stderr
new file mode 100644
index 0000000000..ee70f0373b
--- /dev/null
+++ b/testsuite/tests/gadt/T15558.stderr
@@ -0,0 +1,9 @@
+
+T15558.hs:11:15: warning: [-Winaccessible-code (in -Wdefault)]
+    • Couldn't match type ‘Int’ with ‘Bool’
+      Inaccessible code in
+        a type expected by the context:
+          (a ~ Bool) => ()
+    • In the first argument of ‘MkFoo’, namely ‘()’
+      In the expression: MkFoo ()
+      In an equation for ‘f’: f MkT = MkFoo ()
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index 27210312c3..395cce8c12 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -118,3 +118,4 @@ test('T14320', normal, compile, [''])
 test('T14719', normal, compile_fail, ['-fdiagnostics-show-caret'])
 test('T14808', normal, compile, [''])
 test('T15009', normal, compile, [''])
+test('T15558', normal, compile, [''])
diff --git a/testsuite/tests/polykinds/T7594.stderr b/testsuite/tests/polykinds/T7594.stderr
index 1b4b9017f7..5632e97707 100644
--- a/testsuite/tests/polykinds/T7594.stderr
+++ b/testsuite/tests/polykinds/T7594.stderr
@@ -5,7 +5,7 @@ T7594.hs:37:12: error:
           inside the constraints: (:&:) c0 Real a
           bound by a type expected by the context:
                      forall a. (:&:) c0 Real a => a -> b
-          at T7594.hs:37:8-19
+          at T7594.hs:37:12-16
       ‘b’ is a rigid type variable bound by
         the inferred type of bar2 :: b
         at T7594.hs:37:1-19
diff --git a/testsuite/tests/typecheck/should_fail/tcfail068.stderr b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
index 4318021213..299fc7b8a7 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail068.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
@@ -4,7 +4,7 @@ tcfail068.hs:14:9: error:
       ‘s1’ is a rigid type variable bound by
         a type expected by the context:
           forall s1. GHC.ST.ST s1 (IndTree s a)
-        at tcfail068.hs:(13,9)-(14,31)
+        at tcfail068.hs:(13,15)-(14,31)
       ‘s’ is a rigid type variable bound by
         the type signature for:
           itgen :: forall a s.
@@ -27,7 +27,7 @@ tcfail068.hs:19:9: error:
       ‘s1’ is a rigid type variable bound by
         a type expected by the context:
           forall s1. GHC.ST.ST s1 (IndTree s a)
-        at tcfail068.hs:(18,9)-(21,19)
+        at tcfail068.hs:(18,15)-(21,19)
       ‘s’ is a rigid type variable bound by
         the type signature for:
           itiap :: forall a s.
@@ -58,7 +58,7 @@ tcfail068.hs:24:36: error:
       ‘s1’ is a rigid type variable bound by
         a type expected by the context:
           forall s1. GHC.ST.ST s1 (IndTree s a)
-        at tcfail068.hs:24:29-46
+        at tcfail068.hs:24:35-46
       ‘s’ is a rigid type variable bound by
         the type signature for:
           itrap :: forall a s.
@@ -95,7 +95,7 @@ tcfail068.hs:36:46: error:
       ‘s1’ is a rigid type variable bound by
         a type expected by the context:
           forall s1. GHC.ST.ST s1 (c, IndTree s b)
-        at tcfail068.hs:36:40-63
+        at tcfail068.hs:36:45-63
       ‘s’ is a rigid type variable bound by
         the type signature for:
           itrapstate :: forall b a c s.
diff --git a/testsuite/tests/typecheck/should_fail/tcfail076.stderr b/testsuite/tests/typecheck/should_fail/tcfail076.stderr
index d4368a4cf5..52fcebb927 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail076.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail076.stderr
@@ -4,11 +4,11 @@ tcfail076.hs:18:82: error:
       ‘res1’ is a rigid type variable bound by
         a type expected by the context:
           forall res1. (b -> m res1) -> m res1
-        at tcfail076.hs:18:64-88
+        at tcfail076.hs:18:71-88
       ‘res’ is a rigid type variable bound by
         a type expected by the context:
           forall res. (a -> m res) -> m res
-        at tcfail076.hs:18:28-96
+        at tcfail076.hs:18:35-96
       Expected type: m res1
         Actual type: m res
     • In the expression: cont a