Re: [isabelle] Code generator forgets type constraint on literal integers
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.
On 21/08/14 16:21, Florian Haftmann wrote:
Ambiguous type variable `a0' in the constraints:
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and