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

Clemens Ballarin ballarin at in.tum.de
Thu Sep 4 11:56:56 CEST 2014

Is this a regression in the type inference of locale expressions, or has it always (i.e. since 2009) been like this?


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

More information about the isabelle-dev mailing list