[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?

I did not check this yet, but it is very likely that this has been
undetected since ever.  I will figure out…

	Florian

> 
> Clemens
> 
>  
> 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: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140904/25fd0aa9/attachment.sig>