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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
