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



Hi Florian,

Thanks for looking into this and the hint about defining constants for the literals. Playing with this a little bit further, I found out that it suffices to define one identity function on integer and apply it to all problematic integer literals.

Best,
Andreas

On 21/08/14 16:21, Florian Haftmann wrote:
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,
	Florian






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