[GHC] #13780: Nightmarish pretty-printing of equality type in GHC 8.2 error message
#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
#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 (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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: simonpj (added) Comment: 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13780#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: (none) => goldfire Comment: 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 [wiki:RichardAndSimon] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13780#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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): This appears to be fixed in GHC HEAD. I need to figure out which commit did the deed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13780#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: #13819 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #13819 Comment: These were fixed in c2417b87ff59c92fbfa8eceeff2a0d6152b11a47 (Fix #13819 by refactoring TypeEqOrigin.uo_thing). TODO: Add regression tests. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13780#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13780: Nightmarish pretty-printing of equality type in GHC 8.2 error message -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: patch 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: #13819 | Differential Rev(s): Phab:D3794 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D3794 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13780#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13780: Nightmarish pretty-printing of equality type in GHC 8.2 error message
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: goldfire
Type: bug | Status: patch
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: #13819 | Differential Rev(s): Phab:D3794
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#13780: Nightmarish pretty-printing of equality type in GHC 8.2 error message -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1-rc2 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Poor/confusing | Test Case: error message | dependent/should_fail/T13780a, | dependent/should_fail/T13780c Blocked By: | Blocking: Related Tickets: #13819 | Differential Rev(s): Phab:D3794 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => closed * testcase: => dependent/should_fail/T13780a, dependent/should_fail/T13780c * resolution: => fixed * milestone: => 8.4.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13780#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC