[isabelle-dev] HOL-Codegenerator_Test error

[Lars Hupel]

(Take the following with a grain of salt, it is the result of a cursory
investigation.)

As far as I can tell the current problem is a variation of §7.1.

Here's an excerpt from the error log:

[error] /tmp/foo/foo.scala:5687: ambiguous implicit values:
[error]  both method semiring_char_0_nat in object ROOT of type =>
ROOT.semiring_char_0[ROOT.nat]
[error]  and method semiring_div_nat in object ROOT of type =>
ROOT.semiring_div[ROOT.nat]
[error]  match expected type ROOT.power[ROOT.nat]
[error]                          less_eq_nat(power[nat](m,
nat_of_integer(BigInt(2))),
[error]                                                ^

The affected function is:

def sqrt(n: nat): nat =
  Max[nat](filter[nat](((m: nat) =>
                         less_eq_nat(power[nat](m,
nat_of_integer(BigInt(2))),
                                      n)),
                        seta[nat](upt(zero_nata, Suc(n)))))

As can be seen, it is not parameterized over types. There are actually
two legitimate ambiguous implicit values (with the inherent ambiguity
stemming from the export scheme of instances to Scala*).

The solution here might very well be to "close the diamond", but I fail
to understand how this compiled in the first place.

Cheers
Lars


* there is the possibility of improving the scheme to avoid the present
problem, but not the problem described in §7.1**
** if we want to fix §7.1 once and for all, the code generator needs to
disambiguate manually