> 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
Class_Clash.thy
Description: application/extension-thy
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
