[isabelle-dev] Type arguments in datatype declarations

[Florian Haftmann]

The following datatype specification succeeds as expected

datatype ('a, 'b) foo = Nihil | Bar "('a, 'b) bar"
  and ('a, 'b) bar = Foo "('a, 'b) foo"

whereas the following logically equivalent, but differently written
specification fails with a low-level exception in size.ML:

datatype ('a, 'b) foo = Nihil | Bar "('b, 'a) bar"
  and ('b, 'a) bar = Foo "('a, 'b) foo"

I have always assumed gracefully that for mutual datatype specifications
the names of arguments must be strictly the same, and many recent
extensions to the datatype package also do.  Have specifications like
the second ever been intended to succeed?  If yes, the issue could be
solved by consolidating specifications silently before processing.  If
no, a user-level error message should be reported.

My personal preference is the second, but there might be different opinions.

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

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: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20100927/b26b0298/attachment.sig>