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

[Makarius]

On Tue, 8 May 2012, Tobias Nipkow wrote:

> 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.

The expert(s) on code generation should comment on that, most notably 
Florian.

When he made his first round on the renewed codegenerator, we changed a 
few things at the bottom of the logic to get sort constraints out of the 
way.  As a consequence, primitive consts and corresponding definitional 
axioms have become free from sort constraints, but the results are 
presented to the user with constraints as expected.


 	Makarius