[isabelle-dev] [isabelle] Code generator forgets type constraint on literal integers
andreas.lochbihler at inf.ethz.ch
Mon Sep 22 10:56:38 CEST 2014
Thanks, Florian. Now I can drop my workarounds.
On 20/09/14 15:34, Florian Haftmann wrote:
>>> 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
> This suspicion is wrong, see above.
More information about the isabelle-dev