[GHC] #11513: Work out when GADT parameters should be specified

29 Jan 2016

      #11513: Work out when GADT parameters should be specified
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  TypeApplications                   |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Right now, there's not a clear specification of when GADT data constructor
 parameters should be specified, and what order they appear in. For
 example:

 {{{
 data G a where
   MkG :: b -> a -> G a
 }}}

 To my eye, we should get `MkG :: forall b a. b -> a -> G a`. But GHC now
 gives `MkG :: a {b}. b -> a -> G a`. At least two things are going on
 here:

 1. GHC puts all universals before existentials.

 2. There is an outright bug in `mkDataCon` that makes existentials act as
 inferred variables, but only for the representation type, not the wrapper
 type.

 You can witness (2) by noting that the `b` magically becomes specified if
 you put a strictness annotation (thereby necessitating the construction of
 a wrapper) anywhere.

 I'm not sure what to do about (1), from a design standpoint. Here are some
 thoughts.

 A. Having universals always come before existentials is convenient in
 pattern matching. When we have type application in patterns, you'll want
 to match only on existentials, never universals. So keeping the
 existentials together makes some sense. The universals will be omitted
 from the match entirely.

 B. FC absolutely requires that the universals come first. So if we allow
 the user to reorder the variables, that will necessitate creating a
 wrapper. Are there performance implications? That would be sad.

 C. We could tread a middle path, where if the user writes a `forall`, they
 get the order requested. Otherwise, they get universals first (whose order
 is taken from the ordering in the `data` declaration head) followed by
 existentials (whose order is taken from left-to-right first occurrence in
 the constructor type signature). But this is different than for functions,
 where we always use left-to-right ordering, even when lacking a `forall`.

 I tend to think that we should always just do what the user asks, but I'm
 worried about performance implications of this decision. It will make
 wrappers necessary for existential constructors that otherwise don't need
 them.

 Note that this whole debate is about only GADT constructors, not Haskell98
 ones. Haskell98 constructors will always have universals before
 existentials, because that's quite obvious from the way they're declared.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11513
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

GHC

tags

participants (1)