Opened 12 days ago
Last modified 9 days ago
#15361 new bug
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):  
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 (5)
comment:1 followup: 2 Changed 12 days ago by
comment:2 Changed 12 days 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 12 days ago by
I find the second example more convincing than the first. I wonder how we do that...
comment:4 Changed 9 days 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?
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?