Dear Simon and fellow GHCers, Thank you for having a look at this. I've inlined my response with your message.
| data RecContTest a where | C { showable :: Show a => a } :: RecContTest a
This definitely isn't going to work: it declares the 'showable' field to be a function that *requires* a Show context, not one that *provides* a Show context.
Absolutely. Like I said, I committed the sin of hacking until GHC stopped complaining. At some point, I turned off the semantics in my head ;)
The problem is mainly to find a decent syntax -- and that problem made me simply omit it altogether. Probably the most plausible possibilities are
(A) data RecContTest a where Show a => C { showable :: Show a => a } :: RecContTest a
(B) data RecContTest a where C :: Show a => { showable :: Show a => a } -> RecContTest a
I presume there's a little copy-paste mishap going on here and that you mean: (A) data RecContTest a where Show a => C { showable :: a } :: RecContTest a (B) data RecContTest a where C :: Show a => { showable :: a } -> RecContTest a
The latter (B) looks best to me. I dislike (A) because part of the type (the "Show a =>") occurs before the constructor name C, and part appears after. On the other hand, (B) has something that looks vaguely like a type { x::ty, y::ty } -> ty but that's not really valid type syntax. (Mind you, the ! marks in a constructor signature aren't part of valid types either, so maybe it's not so bad to have a special form in constructor declarations.)
I'm afraid I'm not too well informed with regards to type syntax, but another reason to prefer B over A is that it looks much more like a normal function declaration. When I explain GADTs and their syntax to people that haven't used them before, I usually start off by saying that constructors are simply functions. With GADTs, the declarations of the constructors look exactly like those of functions, but you don't have to worry about providing a binding.
But if we were going to adopt (B), then even when there is no class context we should really say
(B) data RecTest a where B :: { arg :: a } -> RecTest a
rather than the current syntax which is
(A) data RecTest a where B { arg :: a } :: RecTest a
[Note the different placement of the double colon and arrow in (B).]
Again, B is much more in-sync with "normal GADTs" (i.e. non-record syntax) and with the perspective of constructors-as-functions I mentioned above. The record parts of B don't seem to be function-like, but it is how I would define functions on extensible records (regardless of the current status of different implementations / alternatives). To me, this foo :: { bar :: Bool, tutu :: Int } -> String means that foo is a function on any record that contains at least the fields bar and tutu of the mentioned types.
My take on this (B) looks nicer, but it would represent a breaking change But perhaps not many people use record-style syntax + GADT-style syntax And better to make breaking changes sooner than later
One very important reason for me to use GADTs nowadays, is that they provide contexts in pattern matches. If normal ADTs were to do the same, I would use far less GADTs. Record syntax just makes sense when you stick more than three arguments in a constructor. Having said that, *every* ADT seems to be a record in GHC: data FooBar = Foo Int Int | Bar Char isFoo Foo {} = True isFoo _ = False Rounding up; B has my strong preference over A. I don't know whether very strong alternatives will present themselves, but B seems quite nice in general. Regards, Philip