Email Gateway (Aug 19 2022 at 15:28): Email Gateway (Aug 19 2022 at 15:28):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts of the code generator,
The code serialiser for Haskell forgets to print a type constraint on literal integers in
a polymorphic context that requires a type class instance. I have attached a minimal
example. The generated Haskell code does not compiler. Rather, it produces the following
error message.
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
How can I tell the code generator to print the type constraint for literal integers?
Andreas
Test.thy
Email Gateway (Aug 19 2022 at 15:31):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
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
signature.asc
Email Gateway (Aug 19 2022 at 15:32):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Apr 29 2024 at 20:15 UTC