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

[Florian Haftmann]

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