GADT record syntax and contexts

[Philip K.F. Hölzenspies]

Dear GHCers,

Maybe this question is more for Haskell-cafe, but since it involves
language extensions as provided by GHC, it seems reasonable to post it
here.

The GHC user guide lists under 7.4 [1] the extensions to data types and
type synonyms. My question involves 7.4.5 (although the overlap with
7.4.6 is considerable; maybe the two should be merged). A property of
GADTs that I really appreciate is the fact that constructor contexts are
made available by pattern matching (I don't quite understand why normal
ADTs could do this, btw, but that's another question). The problem I
have now, though, is that there doesn't seem to be a syntax to combine
contexts and records in GADTs. Consider this program:

data ContTest a where
  A :: Show a => a -> ContTest a

data RecTest a where
  B { arg :: a } :: RecTest a

data RecContTest a where
  C { showable :: Show a => a } :: RecContTest a

a :: ContTest a -> String
a (A a) = show a

b :: Show a => RecTest a -> String
b = show . arg

c :: RecContTest a -> String
c (C { showable = x }) = show x

Both ContTest and RecTest work swimmingly (with functions a and b,
respectively). However, GHC complains that it can not deduce Show for
type a in function c. My definition of RecContTest is the only
syntactical form I could come up with that GHC accepts. Is there a
syntax for what I want here?

Regards,
Philip



PS. As a side-note. In section 7.4.5, the manual states that:

"At the moment, record updates are not yet possible with GADT-style
declarations, so support is limited to record construction, selection
and pattern matching."

However, if I add:

update org@(B {}) x = org { arg = x }

and evaluate "b $ update (B True) False" the response is "False" as one
would expect. Is this line in the user guide outdated, or is support for
updates unstable or partial?


[1]http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html