[commit: ghc] master: Suppress redundant givens during error reporting (c552fee)
git at git.haskell.org
git at git.haskell.org
Sun Aug 12 16:49:34 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/c552feea127d8ed8cbf4994a157c4bbe254b96c3/ghc
>---------------------------------------------------------------
commit c552feea127d8ed8cbf4994a157c4bbe254b96c3
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date: Sun Aug 12 17:27:27 2018 +0200
Suppress redundant givens during error reporting
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
>---------------------------------------------------------------
c552feea127d8ed8cbf4994a157c4bbe254b96c3
compiler/typecheck/TcErrors.hs | 44 +++++++++++++++++++++-
testsuite/tests/typecheck/should_fail/T15361.hs | 20 ++++++++++
.../tests/typecheck/should_fail/T15361.stderr | 36 ++++++++++++++++++
testsuite/tests/typecheck/should_fail/T5853.stderr | 2 +-
testsuite/tests/typecheck/should_fail/all.T | 1 +
5 files changed, 100 insertions(+), 3 deletions(-)
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index ecb4042..c044cde 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -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
index 0000000..53ae965
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15361.hs
@@ -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
index 0000000..93b0174
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15361.stderr
@@ -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
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index decc6ad..573a532 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -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)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 9a042ec..72023d2 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -475,4 +475,5 @@ test('T14904a', normal, compile_fail, [''])
test('T14904b', normal, compile_fail, [''])
test('T15067', normal, compile_fail, [''])
test('T15330', normal, compile_fail, [''])
+test('T15361', normal, compile_fail, [''])
test('T15438', normal, compile_fail, [''])
More information about the ghc-commits
mailing list