[isabelle-dev] Type variables without default sort

[Lars Noschinski]

Hi all,

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?

If this is not the case, would it be possible to just always infer at 
least the default case? 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.

   -- Lars