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

[Florian Haftmann]

See now http://isabelle.in.tum.de/reports/Isabelle/rev/7f990b3d5189
which seems to do the job.  There a still dark corners wrt. to base sort
inference which maybe one day will lift its ugly head but for the moment
it is OK.

	Florian

On 10.09.2014 10:35, Florian Haftmann wrote:
> 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
>>
> 
> 
> 
> _______________________________________________
> 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/20140911/c6dd06f8/attachment.sig>