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 noninjective 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 noninjective 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 