[GHC] #16030: Poor pretty-printing of GADT constructors in GHCi
#16030: Poor pretty-printing of GADT constructors in GHCi -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I recently loaded this file into GHCi: {{{#!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Proxy data Foo1 (a :: k) where MkFoo1a :: Proxy a -> Int -> Foo1 a MkFoo1b :: { a :: Proxy a, b :: Int } -> Foo1 a data family Foo2 (a :: k) data instance Foo2 (a :: k) where MkFoo2a :: Proxy a -> Int -> Foo2 a MkFoo2b :: { c :: Proxy a, d :: Int} -> Foo2 a }}} And when I queried these datatypes with `:info`, I saw this: {{{ $ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs -fprint- explicit-kinds GHCi, version 8.7.20181129: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Ok, one module loaded. λ> :i Foo1 Foo2 type role Foo1 nominal phantom data Foo1 @k (a :: k) where MkFoo1a :: forall k (a :: k). (Proxy @{k} a) -> Int -> Foo1 k a MkFoo1b :: forall k (a :: k). {a :: Proxy @{k} a, b :: Int} -> Foo1 k a -- Defined at Bug.hs:8:1 data family Foo2 @k (a :: k) -- Defined at Bug.hs:12:1 data instance forall k (a :: k). Foo2 @k a where MkFoo2a :: forall k (a :: k). (Proxy @{k} a) -> Int -> Foo2 @k a MkFoo2b :: forall k (a :: k). {c :: Proxy @{k} a, d :: Int} -> Foo2 @k a -- Defined at Bug.hs:13:15 }}} Yuck. A couple of icky things to note here: * For some reason, the `Proxy @{k} a` field is needlessly parenthesized in `MkFoo1a` and `MkFoo2a`. This does //not// happen when record syntax is used, as demonstrated with `MkFoo1b` and `MkFoo2b`. * Even more strangely, despite the fact that `k` is a specified argument, we're pretty-printing the return type of `MkFoo1{a,b}` as `Foo k a`, not `Foo @k a`. This problem doesn't appear to happen for data family instances, since `MkFoo2{a,b}` don't have this issue. Patch incoming. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16030 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16030: Poor pretty-printing of GADT constructors in GHCi -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5440 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5440 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16030#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16030: Poor pretty-printing of GADT constructors in GHCi
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.7
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D5440
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Krzysztof Gogolewski
#16030: Poor pretty-printing of GADT constructors in GHCi -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5440 Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * status: patch => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16030#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16030: Poor pretty-printing of GADT constructors in GHCi -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5440 Wiki Page: | -------------------------------------+------------------------------------- Comment (by sheaf): Does this patch also add `@`s in the following situation? {{{#!hs data Foo (is :: [Type]) where AnyFoo :: Foo is type NilFoo = (AnyFoo :: Foo '[]) }}} `> :set -fprint-explicit-kinds`\\ `> :info NilFoo`\\ `type NilFoo = 'AnyFoo ('[] Type) :: Foo ('[] Type)` I've got code which uses a lot of different kinds, and `-fprint-explicit- kinds` helps me to understand why e.g. some type family applications are not computing (because of kind reasons), but I find the output quite hard to read because some types are passed as arguments where I would be expecting a type application. I would prefer the output to be: `type NilFoo = 'AnyFoo ('[] @Type) :: Foo ('[] @Type)` Let me know if that's reasonable. (I don't know what the visible kind application patch changes about this either.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16030#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16030: Poor pretty-printing of GADT constructors in GHCi -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5440 Wiki Page: | -------------------------------------+------------------------------------- Comment (by monoidal): Yes, GHC now outputs that kind. (Though you need -XNoStarIsType, otherwise you get `@*` instead of `@Type`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16030#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#16030: Poor pretty-printing of GADT constructors in GHCi -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.7 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5440 Wiki Page: | -------------------------------------+------------------------------------- Comment (by sheaf): Excellent, thank you. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16030#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC