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

2 Jun 2017


      #13780: Nightmarish pretty-printing of equality type in GHC 8.2 error message
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1-rc2
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 I originally spotted this in
 https://ghc.haskell.org/trac/ghc/ticket/12102#comment:1, but I happened to
 stumble upon it again recently in a separate context, so I though it
 deserved its own ticket. Here's some code which does not typecheck:

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

 data family Sing (a :: k)

 data Foo a = a ~ Bool => MkFoo
 data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
 }}}

 In GHC 8.0.1 and 8.0.2, the error message you'd get from this program was
 reasonable enough:

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

 Bug.hs:9:40: error:
     • Expected kind ‘Foo a’, but ‘'MkFoo’ has kind ‘Foo Bool’
     • In the second argument of ‘~’, namely ‘MkFoo’
       In the definition of data constructor ‘SMkFoo’
       In the data instance declaration for ‘Sing’
 }}}

 But in GHC 8.2.1 and HEAD, it's hair-raisingly bad:

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

 Bug.hs:9:40: error:
     • Expected kind ‘Foo a’,
         but ‘'MkFoo
                ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind
 ‘Foo Bool’
     • In the second argument of ‘~’, namely ‘MkFoo’
       In the definition of data constructor ‘SMkFoo’
       In the data instance declaration for ‘Sing’
   |
 9 | data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
   |                                        ^^^^^
 }}}

 **WAT.**

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