GADT records revisited

[Philip K.F. Hölzenspies]

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

Re: 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.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