This is what I expected. Type inference of locale expressions is inherently heuristic and probably you are hitting this. (This could be verified further with a stack trace). For more background, see also this earlier message: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-February/003821.html
Clemens On 05 September, 2014 20:12 CEST, Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de> wrote: > > Is this a regression in the type inference of locale expressions, or has it > > always (i.e. since 2009) been like this? > > Using the attached retrofitted theory, the same behaviour occurs: > > > $ /opt/Isabelle2009/Isabelle2009/bin/isabelle tty > >> val it = () : unit > > val commit = fn : unit -> bool > > Welcome to Isabelle/HOL (Isabelle2009: April 2009) > >> theory Foo imports Class_Clash begin > > Loading theory "Class_Clash" > > parameters > > f :: "'a => 'a => 'a" > > constants > > F :: "'a => 'a => 'a" > > parameters > > f :: "'a => 'a => 'a" > > constants > > F :: "'a => 'a => 'a" > > "plus" > > :: "'a => 'a => 'a" > > "inf" > > :: "'b => 'b => 'b" > > "plus" > > :: "'a => 'a => 'a" > > "inf" > > :: "'a => 'a => 'a" > > "plus" > > :: "'a => 'a => 'a" > > "inf" > > :: "'a => 'a => 'a" > > *** Type unification failed > > *** Type error in application: Incompatible operand type > > *** > > *** Operator: op = inf :: ('b => 'b => 'b) => bool > > *** Operand: plus :: 'a => 'a => 'a > > *** > > *** At command "locale" (line 64 of "/data/tum/drawer/thy/Class_Clash.thy"). > >> Error - Database is not opened for writing. > >> val it = () : unit > > There is strong evidence that it has always been like this. > > Shall I just chance my luck and dive into the sources? > > Cheers, > Florian > > > > > > On 04 September, 2014 09:21 CEST, Florian Haftmann > > <florian.haftm...@informatik.tu-muenchen.de> wrote: > > > >> At d6a2e3567f95, I am currently analysing a problem with type inference > >> in locale expressions: when leaving types implicit, imported parameters > >> are given disjoint types despite they could be unified, and are so if > >> given explicit type annotations. The problem occurs if the imported > >> locales themselves have dependencies on other locales containing a > >> definition. > >> > >> The reason why this is really annyoing is that it breaks certain class>> > >> specifications to typecheck and currently effectively prevents me from>> > >> adding such a simple thing as product over lists. > >> > >> See attached theory for quite minimal examples. > >> > >> I will have to investigate this further. > >> > >> Florian > >> > >> -- > >> > >> PGP available: > >> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > > > > > > > > > > > > _______________________________________________ > > isabelle-dev mailing list > > isabelle-...@in.tum.de > > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev