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

[Tobias Nipkow]

Am 08/05/2012 14:44, schrieb Makarius:
> So apart from the observation that the foundational kernel does not require sort
> constraints (apart from HOL.type of course), were there any reasons against them?

They are not allowed in Haskell anymore, so why do we allow them (and complicate
the code generation for Haskell in the future)? That was the starting point.

That the kernel does not require sort constraints is not the point. Even if it
did, you would still not need sort constraints in datatypes because their
construction does not involve any sorts. You could always (I think) define an
unconstrained datatype, even if its intended usage is in a constrained setting.

I now see that there are certain extra-logical uses and accept that some people
just like to explicitly constrain the usage of a datatype.

Now that the machinery works smoothly, I would not suggest to remove it.

Tobias