GitLab

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