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

[Tobias Nipkow]

This is an interesting issue. I would like to know if we need class constraints
for datatype parameters in the first place. I thought we had agreed at some
point (not on this list) to get rid of them, but we never did. Maybe there are
situations where you need them? The only one that comes to my mind is the
following: you define some type "('a::C) t" by a typedef and then make it into a
datatype by hand (via rep_datatype). Now you can use it inside a datatype
definition. Do we have a (conceivable) example of this situation?

Tobias

Am 07/05/2012 16:02, schrieb 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
> 
> 
> 
> This body part will be downloaded on demand.