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

[Andreas Lochbihler]

Thanks, Florian. Now I can drop my workarounds.

Andreas

On 20/09/14 15:34, Florian Haftmann wrote:
>>> 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
>