[GHC] #15621: Error message involving type families points to wrong location

[GHC]

#15621: Error message involving type families points to wrong location
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
  (Type checker)                     |
           Keywords:  TypeFamilies   |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Poor/confusing
  Unknown/Multiple                   |  error message
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the following program:

 {{{#!hs
 {-# 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`:

 {{{#!hs
 {-# 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 ()
 }}}

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15621>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler