Re: [isabelle] Code generator forgets type constraint on literal integers

Hi Andreas,

> Generated_Code.hs:29:14:
>     Ambiguous type variable `a0' in the constraints:
>       (Prelude.Num a0)
>         arising from the literal `42' at Generated_Code.hs:29:14-15
>       (Foo a0) arising from a use of `bar' at Generated_Code.hs:29:10-12
>     Probable fix: add a type signature that fixes these type variable(s)
>     In the first argument of `bar', namely `42'
>     In the expression: bar 42
>     In an equation for `foobar': foobar = bar 42

this seem to be an instance of the »type class variables in
contravariant position« issue; it has been resolved in general by Lukas
Bulwahn, but, alas, these annotations are not printed for custom
serializations.  I will have a look at this and refine it accordingly.

Until, then, you can help yourself by an auxiliary definition:

definition aux where "aux = (42 :: integer)"
definition foobar where "foobar = bar (42 :: integer)"
lemma [code]: "foobar = bar aux" by (simp add: foobar_def aux_def)

This works unless you have a considerable number of literals in critical
positions (but even then workarounds are possible using auxiliary
constants, the preprocessor and custom serialization).

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.