[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.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- 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