[GHC] #8673: GHC could generate GADT record selectors in more cases

[GHC]

#8673: GHC could generate GADT record selectors in more cases
-------------------------------------+------------------------------------
        Reporter:  simonpj           |            Owner:
            Type:  feature request   |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.6.3
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Old description:

> Philip Holzenspies writes (in email to ghc-users):
> I was playing around with GADT-records again and ran into behaviour that
> I'm not sure is intentional. Given this program:
> {{{
> {-#LANGUAGE GADTs #-}
>
> data FooBar x a where
>    Foo :: { fooBar :: a } -> FooBar Char a
>    Bar :: { fooBar :: a } -> FooBar Bool a
> }}}
> GHC tells me this:
> {{{
> foo.hs:3:1:
>      Constructors Foo and Bar have a common field `fooBar',
>        but have different result types
>      In the data declaration for `FooBar'
> Failed, modules loaded: none.
> }}}
>
> The user guide does say (section 7.4.7): "However, for GADTs there is
> the following additional constraint: every constructor that has a field
> f must have the same result type (modulo alpha conversion)." So this
> behaviour is documented in the user guide. However, it seems reasonable
> that in the case above, where all the relevant variables are exposed in
> the result type of both constructors, this should be perfectly typeable.
> In other words, shouldn't GHC be able to derive a type that is simply:
> {{{
> fooBar :: FooBar x a -> a
> }}}
> ?
>
> Is this something that was simply never implemented, but could be, or is
> this not decidable or prohibitively computationally complex?

New description:

 Philip Holzenspies writes (in email to ghc-users): I was playing around
 with GADT-records again and ran into behaviour that I'm not sure is
 intentional. Given this program:
 {{{
 {-#LANGUAGE GADTs #-}

 data FooBar x a where
    Foo :: { fooBar :: a } -> FooBar Char a
    Bar :: { fooBar :: a } -> FooBar Bool a
 }}}
 GHC tells me this:
 {{{
 foo.hs:3:1:
      Constructors Foo and Bar have a common field `fooBar',
        but have different result types
      In the data declaration for `FooBar'
 Failed, modules loaded: none.
 }}}

 The user guide does say (section 7.4.7): "However, for GADTs there is the
 following additional constraint: every constructor that has a field f must
 have the same result type (modulo alpha conversion)." So this behaviour is
 documented in the user guide. However, it seems reasonable that in the
 case above, where all the relevant variables are exposed in the result
 type of both constructors, this should be perfectly typeable.

 In other words, shouldn't GHC be able to derive a type that is simply:
 {{{
 fooBar :: FooBar x a -> a
 }}}
 ?

 Is this something that was simply never implemented, but could be, or is
 this not decidable or prohibitively computationally complex?

--

Comment (by simonpj):

 Consider
 {{{
 data Bar a where
   B1 :: { x :: b } -> Bar [b]
   B2 :: { x :: b } -> Bar [b]
   B3 :: Bar a
 }}}
 Now we can define a perfectly good selector
 {{{
   x :: Bar [b] -> b
   x (B1 v) = v
   x (B2 v) = v
 }}}
 But this wouldn't work if the result types were different
 {{{
 data BadBar a where
   B1 :: { x :: b } -> Bar [b]
   B2 :: { x :: b } -> Bar b
   B3 :: Bar a
 }}}
 Now it's true that in your example the field mentions only *polymorphic*
 components, so there is a perfectly well-defined selector with the type
 you give.  Indeed, it could be a bit more complicated:
 {{{
 data FooBar x a where
   Foo :: { fooBar :: a } -> FooBar Char [a]
   Bar :: { fooBar :: a } -> FooBar Bool [a]
 }}}
 Then there is a reasonable selector with type
 {{{
   fooBar :: FooBar b [a] -> a
 }}}
 So what is the general rule? When exactly is there a well-defined selector
 type, and what is that type?  Notice that in the type of fooBar we had to
 generalise over the Char/Bool difference, but maintain the [a] part.
 Indeed it might all be part of one type:
 {{{
 data FooBar2 x where
   Foo2 :: { fooBar2 :: a } -> FooBar2 (Char, [a])
   Bar2 :: { fooBar2 :: a } -> FooBar2 (Bool, [a])
 }}}
 So now
 {{{
   fooBar2 :: FooBar2 (x, [a]) -> a
 }}}
 where we generalise part of the type.

 So, on reflection, there must be a more permissive rule than the one GHC
 currently implements.  If someone wants to figure out the general rule,
 express it formally, say what the user manual would say, we could discuss
 whether the cost benefit ratio is good enough to be worth implementing.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8673#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler