[isabelle-dev] [isabelle] Code generator forgets type constraint on literal integers

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sat Sep 20 15:34:48 CEST 2014

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

See now http://isabelle.in.tum.de/reports/Isabelle/rev/d0d3c30806b4

This solution is simply to annotate any numeral any Haskell with an
explicit type constraints, since numerals in Haskell are always polymorphic.

> this seem to be an instance of the »type class variables in
> contravariant position« issue; it has been resolved in general by Lukas
> Bulwahn.

This suspicion is wrong, see above.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140920/b814c772/attachment.asc>

More information about the isabelle-dev mailing list