[isabelle-dev] HOL-Codegenerator_Test error

Lars Hupel hupel at in.tum.de
Tue Jan 12 11:27:22 CET 2016

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

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 =>
[error]  and method semiring_div_nat in object ROOT of type =>
[error]  match expected type ROOT.power[ROOT.nat]
[error]                          less_eq_nat(power[nat](m,
[error]                                                ^

The affected function is:

def sqrt(n: nat): nat =
  Max[nat](filter[nat](((m: nat) =>
                        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.


* 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

More information about the isabelle-dev mailing list