[isabelle-dev] Type arguments in datatype declarations

[Stefan Berghofer]

Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

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

Hi Florian,

this is a perfectly legal datatype and therefore should be handled by
the datatype package without prior "consolidation" or whatever, but
I think this case has just been overlooked when reimplementing the
definition of the size functions using the new infrastructure for
datatype interpretations. I'll try to find out what exactly goes wrong.

Greetings,
Stefan