[isabelle-dev] Type variables differing only in sort constraint

[Makarius]

On Thu, 27 May 2010, Florian Haftmann wrote:

> It is possible to enter type variables distinguished only by sort
> constraint on the Isar level:
>
> lemma
>  assumes "P TYPE('a::order)" and "Q TYPE('a::group_add)"
>  shows "R TYPE('a::power)"
> using assms proof -
>
> It is not clear to me whether this his always been possible that way or 
> slipped in due to some change.

While this is OK for the low-level inference kernel, the syntax layer is 
supposed to prevent such inconsistent constraints (both for type and term 
variables).

The above is accepted even in Isabelle2005, and nobody has noticed so far. 
When introducing the present check/uncheck infrastructure some years ago I 
did notice some internal oddities concerning sort constraints that are 
probably responsible for this effect.  Some weeks ago I actually managed 
to clear out some part of it (sort constraints for type specifications), 
but did not get to the bottom of the whole syntax stack.

After the next round of check/uncheck modernization it should work in the 
intended strict sense.


 	Makarius