Opened 7 weeks ago

Last modified 3 weeks ago

#13780 new bug

Nightmarish pretty-printing of equality type in GHC 8.2 error message

Reported by: RyanGlScott Owned by: goldfire
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.1-rc2
Keywords: TypeInType Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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:

{-# 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.

Change History (3)

comment:1 Changed 7 weeks ago by RyanGlScott

Cc: simonpj added

This was caused by either commit 77bb09270c70455bbd547470c4e995707d19f37d ( Re-add FunTy (big patch)) or e368f3265b80aeb337fbac3f6a70ee54ab14edfd (Major patch to introduce TyConBinder). I can't know for sure since commit 77bb09270c70455bbd547470c4e995707d19f37d doesn't build properly.

comment:2 Changed 7 weeks ago by simonpj

Owner: set to goldfire

I think this is another piece of fallout from the horrible uo_thing mess. We are printing a Type in a place where we should printing a HsType.

Richard is planning it investigate and simplify. c.f. #13601, and RichardAndSimon

comment:3 Changed 3 weeks ago by RyanGlScott

Another occurrence of this bug:

{-# 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
{-# 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
   |                ^^^^^
Note: See TracTickets for help on using tickets.