Commit c552feea authored by Ryan Scott's avatar Ryan Scott Committed by Krzysztof Gogolewski

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
parent f7f9820e
...@@ -1809,7 +1809,8 @@ misMatchOrCND ctxt ct oriented ty1 ty2 ...@@ -1809,7 +1809,8 @@ misMatchOrCND ctxt ct oriented ty1 ty2
eq_pred = ctEvPred ev eq_pred = ctEvPred ev
orig = ctEvOrigin ev orig = ctEvOrigin ev
givens = [ given | given <- getUserGivens ctxt, not (ic_no_eqs given)] 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 :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
couldNotDeduce givens (wanteds, orig) couldNotDeduce givens (wanteds, orig)
...@@ -1824,10 +1825,49 @@ pp_givens givens ...@@ -1824,10 +1825,49 @@ pp_givens givens
: map (ppr_given (text "or from:")) gs : map (ppr_given (text "or from:")) gs
where where
ppr_given herald implic@(Implic { ic_given = gs, ic_info = skol_info }) 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 2 (sep [ text "bound by" <+> ppr skol_info
, text "at" <+> ppr (tcl_loc (implicLclEnv implic)) ]) , 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 extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
-- Add on extra info about skolem constants -- Add on extra info about skolem constants
-- NB: The types themselves are already tidied -- NB: The types themselves are already tidied
......
{-# 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
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
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
T5853.hs:15:46: error: T5853.hs:15:46: error:
• Could not deduce: Subst (Subst fa a) b ~ Subst fa b • Could not deduce: Subst (Subst fa a) b ~ Subst fa b
arising from a use of ‘<$>’ 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, 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, 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) Subst (Subst fa a) (Elem fa) ~ fa, Subst fa a ~ Subst fa a)
......
...@@ -475,4 +475,5 @@ test('T14904a', normal, compile_fail, ['']) ...@@ -475,4 +475,5 @@ test('T14904a', normal, compile_fail, [''])
test('T14904b', normal, compile_fail, ['']) test('T14904b', normal, compile_fail, [''])
test('T15067', normal, compile_fail, ['']) test('T15067', normal, compile_fail, [''])
test('T15330', normal, compile_fail, ['']) test('T15330', normal, compile_fail, [''])
test('T15361', normal, compile_fail, [''])
test('T15438', normal, compile_fail, ['']) test('T15438', normal, compile_fail, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment