diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index ecb404289a3ede815b3e97f1cfacfe85a999ddd9..c044cdedaf78d9657ce05aca82d7ebc3407ac2fd 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 0000000000000000000000000000000000000000..53ae965e21952e44c20ba0c620e387cc553f7f8e --- /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 0000000000000000000000000000000000000000..93b01742ffa982f163d084cffecc195d503d0664 --- /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 decc6adabaaf58faa39b8d1ce15704ad561bd37b..573a532f10eb3ad994f508e21aa5227a610f8b4d 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 9a042ec22f95f85ae3bb3dbc3572092b1afae170..72023d247e223e5e8ff173e2f6f97493ce8c3ece 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, [''])