GADT records revisited

[Roman Cheplyaka]

I think this is intentional and conforms to the documentation. Your
constructors clearly have *different* result types, even though they
both can be instantiated from a single type scheme `FooBar x a`.

I'll leave it to others to comment on whether the generalization you
propose is reasonable and feasible.

Roman

* "Philip K.F. Hölzenspies" <p.k.f.holzenspies at utwente.nl> [2014-01-17 07:51:26+0100]
> Dear all,
> 
> 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?
> 
> Regards,
> Philip
> 
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: Digital signature
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140117/ea17e904/attachment.sig>