[isabelle-dev] Type variables without default sort

[Makarius]

On Wed, 29 Jun 2011, Lars Noschinski wrote:

> every once in a while, I manage to create a goal state which contains 
> type variables with the empty sort (for example in "f x = 0", x is of 
> type "'b :: {}", if there are no additional constraints on f. Some tools 
> don't like this (e.g. metis omits a warning, SMT fails altogether) and 
> it always takes me a while to find out, what went wrong.
>
> From an user perspective, this behaviour is a bit puzzling, because it 
> only occurs if a type variable is invented by Isabelle (explicitly 
> mentioned type variables always get the default sort). So I wonder why 
> the default sort is not added for invented type variables. Are there 
> certain situations where type variables with empty sort are needed?

This is an ancient issue, and recurrent source of certain insider jokes.

First of all, this is not the "empty sort", but the empty intersection of 
type classes i.e. the "full sort".  Officially it is called the "top 
sort".

Apart from the "default sort", the "base sort" of the object logic is also 
significant.  Mixing all that up can lead to very odd situations.  I have 
occasionally compared this with the "Zone" of Strugatsky / Tarkovsky, 
although the situation has greatly improved internally in the past few 
years.


In general I count the surprise for the user of this (correct) behaviour 
of type inference as an instance of the general problem of types that turn 
out more general than anticipated.


> Otherwise some kind of warning (similar to the one emitted if a fresh 
> type variable is invented for a fix-ed variable) might be useful. Tobias 
> suggested that such a "warning" could also be done in a similar way like 
> for numerals, by adding an "::'a::{}" annotation in the output.

This inlined annotation from many years ago was already a slight 
improvement over direct warnings on the output channel (which are mostly 
ignored by users).

Since output of terms is more and more replaced by immediate source markup 
now, one could start thinking of a good visual metaphor for type 
inference.  So the question is how to present feedback directly in the 
place where the user is producing text, not in occasional printout by the 
prover in the background.


 	Makarius