Re: [GHC] #13780: Nightmarish pretty-printing of equality type in GHC 8.2 error message

2 Jul 2017

      #13780: Nightmarish pretty-printing of equality type in GHC 8.2 error message
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.2.1-rc2
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Another occurrence of this bug:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 module Foo where

 data family Sing (a :: k)

 data instance Sing (z :: Bool) =
     z ~ False => SFalse
   | z ~ True  => STrue
 }}}
 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind
 import Foo

 type family ElimBool (p :: Bool -> Type) (b :: Bool) (s :: Sing b)
                      (pFalse :: p False) (pTrue :: p True) :: p b where
   ElimBool _ _ SFalse pFalse _ = pFalse
   ElimBool _ _ STrue  _ pTrue  = pTrue
 }}}

 With GHC 8.0.2, you get this error:

 {{{
 GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/ryanglscott/.ghci
 [1 of 2] Compiling Foo              ( Foo.hs, interpreted )
 [2 of 2] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:11:16: error:
     • Expected kind ‘Sing _’, but ‘'SFalse’ has kind ‘Sing 'False’
     • In the third argument of ‘ElimBool’, namely ‘SFalse’
       In the type family declaration for ‘ElimBool’

 Bug.hs:12:16: error:
     • Expected kind ‘Sing _1’, but ‘'STrue’ has kind ‘Sing 'True’
     • In the third argument of ‘ElimBool’, namely ‘STrue’
       In the type family declaration for ‘ElimBool’
 }}}

 But with 8.2.1, you get this:

 {{{
 GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/ryanglscott/.ghci
 [1 of 2] Compiling Foo              ( Foo.hs, interpreted )
 [2 of 2] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:11:16: error:
     • Expected kind ‘Sing _’,
         but ‘'SFalse
                ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind
 ‘Sing
 'False’
     • In the third argument of ‘ElimBool’, namely ‘SFalse’
       In the type family declaration for ‘ElimBool’
    |
 11 |   ElimBool _ _ SFalse pFalse _ = pFalse
    |                ^^^^^^

 Bug.hs:12:16: error:
     • Expected kind ‘Sing _1’,
         but ‘'STrue
                ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind
 ‘Sing
 'True’
     • In the third argument of ‘ElimBool’, namely ‘STrue’
       In the type family declaration for ‘ElimBool’
    |
 12 |   ElimBool _ _ STrue  _ pTrue  = pTrue
    |                ^^^^^
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13780#comment:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler