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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Sep 4 09:21:42 CEST 2014

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

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.



PGP available:
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Class_Clash.thy
Type: application/x-extension-thy
Size: 1762 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140904/73cadba6/attachment.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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140904/73cadba6/attachment.asc>

More information about the isabelle-dev mailing list