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_given_eqs` field of the Implication). Note that we discard givens that have no equalities whatsoever, but we want to keep ones with only *local* equalities, as these may be helpful to the user in understanding what went wrong. 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_given_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 GHC.Tc.TyCl.PatSyn).
References 1
- Remove redundant provided dicts GHC.Tc.TyCl.PatSyn
Referenced by 3
- GHC.Tc.Errors call site
- GHC.Tc.Errors.Ppr call site
- HasGivenEqs GHC.Tc.Types.Constraint