[GHC] #16030: Poor pretty-printing of GADT constructors in GHCi

GHC ghc-devs at haskell.org
Tue Dec 11 17:33:31 UTC 2018


#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


More information about the ghc-tickets mailing list