Suppress redundant givens during error reporting
authorRyan Scott <ryan.gl.scott@gmail.com>
Sun, 12 Aug 2018 15:27:27 +0000 (17:27 +0200)
committerBen Gamari <ben@smart-cactus.org>
Thu, 23 Aug 2018 22:50:23 +0000 (18:50 -0400)
Summary:
When GHC reports that it cannot solve a constraint in error
messages, it often reports what given constraints it has in scope.
Unfortunately, sometimes redundant constraints (like `* ~ *`,
from  #15361) can sneak in. The fix is simple: blast away these
redundant constraints using `mkMinimalBySCs`.

Test Plan: make test TEST=T15361

Reviewers: simonpj, bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15361

Differential Revision: https://phabricator.haskell.org/D5002

(cherry picked from commit c552feea127d8ed8cbf4994a157c4bbe254b96c3)

compiler/typecheck/TcErrors.hs
testsuite/tests/typecheck/should_fail/T15361.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T15361.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_fail/T5853.stderr
testsuite/tests/typecheck/should_fail/all.T

index 1528a49..1b86756 100644 (file)
@@ -1809,7 +1809,8 @@ misMatchOrCND ctxt ct oriented ty1 ty2
     eq_pred = ctEvPred ev
     orig    = ctEvOrigin ev
     givens  = [ given | given <- getUserGivens ctxt, not (ic_no_eqs given)]
-              -- Keep only UserGivens that have some equalities
+              -- Keep only UserGivens that have some equalities.
+              -- See Note [Suppress redundant givens during error reporting]
 
 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
 couldNotDeduce givens (wanteds, orig)
@@ -1824,10 +1825,49 @@ pp_givens givens
                  : map (ppr_given (text "or from:")) gs
     where
        ppr_given herald implic@(Implic { ic_given = gs, ic_info = skol_info })
-           = hang (herald <+> pprEvVarTheta gs)
+           = hang (herald <+> pprEvVarTheta (mkMinimalBySCs evVarPred gs))
+             -- See Note [Suppress redundant givens during error reporting]
+             -- for why we use mkMinimalBySCs above.
                 2 (sep [ text "bound by" <+> ppr skol_info
                        , text "at" <+> ppr (tcl_loc (implicLclEnv implic)) ])
 
+{-
+Note [Suppress redundant givens during error reporting]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When GHC is unable to solve a constraint and prints out an error message, it
+will print out what given constraints are in scope to provide some context to
+the programmer. But we shouldn't print out /every/ given, since some of them
+are not terribly helpful to diagnose type errors. Consider this example:
+
+  foo :: Int :~: Int -> a :~: b -> a :~: c
+  foo Refl Refl = Refl
+
+When reporting that GHC can't solve (a ~ c), there are two givens in scope:
+(Int ~ Int) and (a ~ b). But (Int ~ Int) is trivially soluble (i.e.,
+redundant), so it's not terribly useful to report it in an error message.
+To accomplish this, we discard any Implications that do not bind any
+equalities by filtering the `givens` selected in `misMatchOrCND` (based on
+the `ic_no_eqs` field of the Implication).
+
+But this is not enough to avoid all redundant givens! Consider this example,
+from #15361:
+
+  goo :: forall (a :: Type) (b :: Type) (c :: Type).
+         a :~~: b -> a :~~: c
+  goo HRefl = HRefl
+
+Matching on HRefl brings the /single/ given (* ~ *, a ~ b) into scope.
+The (* ~ *) part arises due the kinds of (:~~:) being unified. More
+importantly, (* ~ *) is redundant, so we'd like not to report it. However,
+the Implication (* ~ *, a ~ b) /does/ bind an equality (as reported by its
+ic_no_eqs field), so the test above will keep it wholesale.
+
+To refine this given, we apply mkMinimalBySCs on it to extract just the (a ~ b)
+part. This works because mkMinimalBySCs eliminates reflexive equalities in
+addition to superclasses (see Note [Remove redundant provided dicts]
+in TcPatSyn).
+-}
+
 extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
 -- Add on extra info about skolem constants
 -- NB: The types themselves are already tidied
diff --git a/testsuite/tests/typecheck/should_fail/T15361.hs b/testsuite/tests/typecheck/should_fail/T15361.hs
new file mode 100644 (file)
index 0000000..53ae965
--- /dev/null
@@ -0,0 +1,20 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+module T15361 where
+
+import Data.Kind
+import Data.Type.Equality
+
+-- Don't report (* ~ *) here
+foo :: forall (a :: Type) (b :: Type) (c :: Type).
+       a :~~: b -> a :~~: c
+foo HRefl = HRefl
+
+data Chumbawamba :: Type -> Type where
+  IGetKnockedDown :: (Eq a, Ord a) => a -> Chumbawamba a
+
+-- Don't report (Eq a) here
+goo :: Chumbawamba a -> String
+goo (IGetKnockedDown x) = show x
diff --git a/testsuite/tests/typecheck/should_fail/T15361.stderr b/testsuite/tests/typecheck/should_fail/T15361.stderr
new file mode 100644 (file)
index 0000000..93b0174
--- /dev/null
@@ -0,0 +1,36 @@
+
+T15361.hs:13:13: error:
+    • Could not deduce: a ~ c
+      from the context: b ~ a
+        bound by a pattern with constructor:
+                   HRefl :: forall k1 (a :: k1). a :~~: a,
+                 in an equation for ‘foo’
+        at T15361.hs:13:5-9
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall a b c. (a :~~: b) -> a :~~: c
+        at T15361.hs:(11,1)-(12,27)
+      ‘c’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall a b c. (a :~~: b) -> a :~~: c
+        at T15361.hs:(11,1)-(12,27)
+      Expected type: a :~~: c
+        Actual type: a :~~: a
+    • In the expression: HRefl
+      In an equation for ‘foo’: foo HRefl = HRefl
+    • Relevant bindings include
+        foo :: (a :~~: b) -> a :~~: c (bound at T15361.hs:13:1)
+
+T15361.hs:20:27: error:
+    • Could not deduce (Show a) arising from a use of ‘show’
+      from the context: Ord a
+        bound by a pattern with constructor:
+                   IGetKnockedDown :: forall a. (Eq a, Ord a) => a -> Chumbawamba a,
+                 in an equation for ‘goo’
+        at T15361.hs:20:6-22
+      Possible fix:
+        add (Show a) to the context of
+          the type signature for:
+            goo :: forall a. Chumbawamba a -> String
+    • In the expression: show x
+      In an equation for ‘goo’: goo (IGetKnockedDown x) = show x
index decc6ad..573a532 100644 (file)
@@ -2,7 +2,7 @@
 T5853.hs:15:46: error:
     • Could not deduce: Subst (Subst fa a) b ~ Subst fa b
         arising from a use of ‘<$>’
-      from the context: (F fa, Elem fa ~ Elem fa, Elem (Subst fa b) ~ b,
+      from the context: (F fa, Elem (Subst fa b) ~ b,
                          Subst fa b ~ Subst fa b, Subst (Subst fa b) (Elem fa) ~ fa,
                          F (Subst fa a), Elem (Subst fa a) ~ a, Elem fa ~ Elem fa,
                          Subst (Subst fa a) (Elem fa) ~ fa, Subst fa a ~ Subst fa a)
index e2d6b71..434c79c 100644 (file)
@@ -474,4 +474,5 @@ test('T14884', normal, compile_fail, [''])
 test('T14904a', normal, compile_fail, [''])
 test('T14904b', normal, compile_fail, [''])
 test('T15067', normal, compile_fail, [''])
+test('T15361', normal, compile_fail, [''])
 test('T15527', normal, compile_fail, [''])