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

[Florian Haftmann]

Hi Clemens,

> 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

thanks for that hint.

The problem the class target faces is to determine the so called base
sort of the class specification, i.e. the sort that is inferred for the
type parameter 'a from the import *and* the fixes/assumes as given by
the user.  For this I cannot fix 'a in the first place.

I think I can circumvent this problem by adding a suitable plugin to the
term/type check phase.  Let's see…

Best,
	Florian

> 
> Clemens
> 
> 
> On 05 September, 2014 20:12 CEST, Florian Haftmann <florian.haftmann at 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.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
>  
>  
>  
>  
> 
> _______________________________________________
> 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: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140910/ee32f3cf/attachment.sig>