Error message involving type families points to wrong location
Consider the following program:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
b = Refl
in ()
This doesn't typecheck, which isn't surprising, since F Int
doesn't equal F Bool
in the definition of b
. What //is// surprising is where the error message points to:
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Int
Actual type: F Bool :~: F Bool
NB: ‘F’ is a non-injective type family
• In the expression: Refl
In an equation for ‘a’: a = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
|
12 | a = Refl
| ^^^^
This claims that the error message arises from the definition of a
, which is completely wrong! As evidence, if you comment out b
, then the program typechecks again.
Another interesting facet of this bug is that if you comment out a
:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Type.Equality
type family F a
f :: ()
f =
let {- a :: F Int :~: F Int
a = Refl -}
b :: F Int :~: F Bool
b = Refl
in ()
Then the error message will actually point to b
this time:
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Bool :~: F Bool
NB: ‘F’ is a non-injective type family
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
b :: F Int :~: F Bool
b = Refl
in ()
|
15 | b = Refl
| ^^^^
The use of type families appears to be important to triggering this bug, since I can't observe this behavior without the use of F
.
This is a regression that was introduced at some point between GHC 8.0.2 and 8.2.2, since 8.2.2 gives the incorrect error message shown above, while 8.0.2 points to the right location:
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:11: error:
• Couldn't match type ‘F Int’ with ‘F Bool’
Expected type: F Int :~: F Bool
Actual type: F Int :~: F Int
NB: ‘F’ is a type function, and may not be injective
• In the expression: Refl
In an equation for ‘b’: b = Refl
In the expression:
let
a :: F Int :~: F Int
a = Refl
b :: F Int :~: F Bool
....
in ()
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 |