[isabelle-dev] Tweak Haskell output for future Haskell compatibility.

[Bertram Felgenhauer]

Dear Isabelle developers,

the Haskell code generator of Isabelle currently emits contexts for
data and newtype generates, e.g. (from CeTA):

  newtype (Linorder a) => Rbt a b = Rbt (Rbta a b);

The sole effect of such contexts is that the programmer must provide
a (Linorder a) context wherever Rbt a b is used, which is fairly uselss.
In the next version of the Haskell language definition (whenever that
will be), this feature will be removed.

  http://www.haskell.org/pipermail/haskell-prime/2011-January/003335.html
  http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts

Ghc currently requires a flag (-XDatatypeContexts) to compile code
using datatype contexts. In the latest release (7.4.1), this option
emits a warning:

    Warning: -XDatatypeContexts is deprecated: It was widely considered a
    misfeature, and has been removed from the Haskell language.

I propose, therefore, to omit these contexts in code generated by
Isabelle. This can safely wait until after the release, of course.
(patch attached)

Best regards,

Bertram
-------------- next part --------------
A non-text attachment was scrubbed...
Name: isabelle-haskell-no-data-contexts.patch
Type: text/x-diff
Size: 1069 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20120507/5c9bf12d/attachment.bin>