Opened 4 months ago
Closed 3 months ago
#15361 closed bug (fixed)
Error message displays redundant equality constraint
Reported by:  RyanGlScott  Owned by:  

Priority:  normal  Milestone:  8.6.1 
Component:  Compiler (Type checker)  Version:  8.4.3 
Keywords:  TypeInType  Cc:  
Operating System:  Unknown/Multiple  Architecture:  Unknown/Multiple 
Type of failure:  Poor/confusing error message  Test Case:  
Blocked By:  Blocking:  
Related Tickets:  #14394  Differential Rev(s):  Phab:D5002 
Wiki Page: 
Description
When compiling this program:
{# LANGUAGE GADTs #} {# LANGUAGE KindSignatures #} {# LANGUAGE RankNTypes #} {# LANGUAGE TypeOperators #} module Bug where import Data.Kind import Data.Type.Equality foo :: forall (a :: Type) (b :: Type) (c :: Type). a :~~: b > a :~~: c foo HRefl = HRefl
GHC complains thus:
$ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:12: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 Bug.hs:12:59 ‘a’ is a rigid type variable bound by the type signature for: foo :: forall a b c. (a :~~: b) > a :~~: c at Bug.hs:(10,1)(11,27) ‘c’ is a rigid type variable bound by the type signature for: foo :: forall a b c. (a :~~: b) > a :~~: c at Bug.hs:(10,1)(11,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 Bug.hs:12:1)  12  foo HRefl = HRefl  ^^^^^
That * ~ *
constraint is entirely redundant.
Change History (13)
comment:1 followup: 2 Changed 4 months ago by
comment:2 Changed 4 months ago by
Replying to goldfire:
Do you propose that GHC not mention givens that are implied by other givens?
Certainly not, and moreover, GHC already does not mention redundant implied givens in certain situations. In this code:
{# LANGUAGE GADTs #} {# LANGUAGE TypeOperators #} import Data.Type.Equality data Goo a where MkGoo :: (Ord a, a ~ Bool) => a > Goo a goo :: Goo a > a :~: b goo MkGoo{} = Refl
Bug.hs:10:15: error: • Could not deduce: b ~ Bool from the context: (Ord a, a ~ Bool) bound by a pattern with constructor: MkGoo :: forall a. (Ord a, a ~ Bool) => a > Goo a, in an equation for ‘goo’ at Bug.hs:10:511 ‘b’ is a rigid type variable bound by the type signature for: goo :: forall a b. Goo a > a :~: b at Bug.hs:9:123 Expected type: a :~: b Actual type: a :~: a • In the expression: Refl In an equation for ‘goo’: goo MkGoo {} = Refl • Relevant bindings include goo :: Goo a > a :~: b (bound at Bug.hs:10:1)  10  goo MkGoo{} = Refl  ^^^^
GHC does not bother warning about an Eq a
constraint being in the context bound by the MkGoo
pattern match, even though it is implied by Ord a
.
Moreover, in this code:
{# LANGUAGE GADTs #} {# LANGUAGE TypeOperators #} import Data.Type.Equality hoo :: Int :~: Int > a :~: b > a :~: c hoo Refl Refl = Refl
Bug.hs:7:17: error: • Could not deduce: a ~ c from the context: b ~ a bound by a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in an equation for ‘hoo’ at Bug.hs:7:1013 ‘a’ is a rigid type variable bound by the type signature for: hoo :: forall a b c. (Int :~: Int) > (a :~: b) > a :~: c at Bug.hs:6:140 ‘c’ is a rigid type variable bound by the type signature for: hoo :: forall a b c. (Int :~: Int) > (a :~: b) > a :~: c at Bug.hs:6:140 Expected type: a :~: c Actual type: a :~: a • In the expression: Refl In an equation for ‘hoo’: hoo Refl Refl = Refl • Relevant bindings include hoo :: (Int :~: Int) > (a :~: b) > a :~: c (bound at Bug.hs:7:1)  7  hoo Refl Refl = Refl  ^^^^
GHC does not warn about an Int ~ Int
constraint, even though we "put it there" by matching on a value of type Int :~: Int
.
comment:3 Changed 4 months ago by
I find the second example more convincing than the first. I wonder how we do that...
comment:4 Changed 4 months ago by
We can fix this issue with the following patch:

compiler/typecheck/TcErrors.hs
diff git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 95dc152..1098b1f 100644
a b pp_givens givens 1821 1821 where 1822 1822 ppr_given herald (Implic { ic_given = gs, ic_info = skol_info 1823 1823 , ic_env = env }) 1824 = hang (herald <+> pprEvVarTheta gs)1824 = hang (herald <+> pprEvVarTheta (mkMinimalBySCs evVarPred gs)) 1825 1825 2 (sep [ text "bound by" <+> ppr skol_info 1826 1826 , text "at" <+> ppr (tcl_loc env) ]) 1827 1827
(Where pp_givens
is the function that prints out the stuff after from the context:
.) Does this sound like a reasonable approach?
comment:6 Changed 4 months ago by
Differential Rev(s):  → Phab:D5002 

Status:  new → patch 
In that case, I'll go for that approach. See Phab:D5002.
comment:7 followup: 8 Changed 4 months ago by
I was puzzled about why redundant givens are sometimes reported and sometimes not. Here's the deal
 For each implication GHC figures out, during constraint solving, whether the implication binds any equalities. This is used to guide equality floatout, and is recorded in the implication in the
ic_no_eqs
field.
 The "whether binds any equalities" test is performed on the canonicalised, inert givens, in
TcSMonad.getNoGivenEqs
. SeeNote [When does an implication have given equalities?]
.
 If an implication binds
* ~ *
only (call it situation (A)), we'll discard that Given, and mark the implication asic_no_eqs = True
.
 But if an implication binds
* ~ *
anda ~ b
, situation (B), theic_no_eqs
field will be setFalse
.
 When reporting an equality error, we report givens only from implications with
ic_no_eqs
=False
. That makes sense. But it'll discard situation (A), and keep situation (B).
 For the implications we keep, we report all original, userwritten givens. Hence the reported
* ~ *
.
So that explain the behavior you see. For example for hoo
in comment:2, the Int :~: Int
binds no equalities because when Int ~ Int
is solved we get nothing. So it is not reported.
I suppose, therefore, that the solution you suggest is no unreasonable, provided you write Note to explain. In particular
mkMinimalBySCs
happens to eliminate reflexive equalities, as well as superclasses. (Why? See Note [Remove redundant provided dicts]in
TcPatSyn`.
 Explain how a given
* ~ *
can arise.
comment:8 Changed 4 months ago by
Replying to simonpj:
I suppose, therefore, that the solution you suggest is no unreasonable, provided you write Note to explain.
Sure thing. I've updated Phab:D5002.
comment:11 Changed 3 months ago by
Status:  patch → merge 

comment:12 Changed 3 months ago by
Milestone:  8.8.1 → 8.6.1 

This was marked as merge, but not milestoned properly.
comment:13 Changed 3 months ago by
Resolution:  → fixed 

Status:  merge → closed 
Merged in 89ad5fed345d54ed73ecb3057346f3ef81864c8c.
But you put it there, by matching on heterogeneous equality on types all of kind
Type
. Do you propose that GHC not mention givens that are implied by other givens?