[GHC] #8673: GHC could generate GADT record selectors in more cases
GHC
ghc-devs at haskell.org
Fri Jan 17 08:05:48 UTC 2014
#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
Keywords: | Operating System: Unknown/Multiple
Architecture: Unknown/Multiple | Type of failure: None/Unknown
Difficulty: Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: |
------------------------------------+-------------------------------------
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?
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8673>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list