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.holzensp...@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@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
signature.asc
Description: Digital signature
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users