Error message displays redundant equality constraint
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:5-9
‘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.
Trac metadata
Trac field | Value |
---|---|
Version | 8.4.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |