[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 <krz.gogolewski@…>): In [changeset:"9d9e35574a92773d872efd58a67339a9e054a9f1/ghc" 9d9e3557/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="9d9e35574a92773d872efd58a67339a9e054a9f1" Fix #16030 by refactoring IfaceSyn's treatment of GADT constructors Summary: GHCi's `:info` command was pretty-printined GADT constructors suboptimally in the following ways: 1. Sometimes, fields were parenthesized when they did not need it, e.g., ```lang=haskell data Foo a where MkFoo :: (Maybe a) -> Foo a ``` I fixed this by refactoring some code in `pprIfaceConDecl` to be a little smarter with respect to GADT syntax. See `pprFieldArgTy` and `pprArgTy`. 2. With `-fprint-explicit-kinds` enabled, there would be times when specified arguments would be printed without a leading `@` in GADT return types, e.g., ```lang=haskell data Bar @k (a :: k) where MkBar :: Bar k a ``` It turns out that `ppr_tc_app`, the function which pretty-prints these return types, was not using the proper machinery to print out the arguments, which caused the visibilities to be forgotten entirely. I refactored `ppr_tc_app` to do this correctly. Test Plan: make test TEST=T16030 Reviewers: goldfire, bgamari, simonpj Reviewed By: simonpj Subscribers: simonpj, rwbarton, carter GHC Trac Issues: #16030 Differential Revision: https://phabricator.haskell.org/D5440 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16030#comment:2> 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: | -------------------------------------+------------------------------------- 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