[isabelle-dev] Type arguments in datatype declarations

[Makarius]

On Mon, 27 Sep 2010, Florian Haftmann wrote:

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

My impression is that 'datatype' always had this tendency to require
the LHS type arguments to agree exactly, but Stefan should know what he 
had in mind originally.

I've made a quick test with Isabelle2008, Isabelle2009, Isabelle2009-1, 
Isabelle2009-2: all fail on the example above, but with different 
low-level exceptions.


 	Makarius