[isabelle-dev] Problem with type inference in locale expressions

[Florian Haftmann]

> 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.haftmann at 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-dev at 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Class_Clash.thy
Type: application/x-extension-thy
Size: 1708 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140905/f2eba8f3/attachment-0002.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140905/f2eba8f3/attachment.sig>