Isabelle: Wellsortedness error

Question

What is the Wellsortedness error in Isabelle.

I encountered a trouble such as:

How can I solve it?

Answer 1

The value command internally uses the code generator for evaluation and the code generator raises the wellsortedness errors. In the above case, Isabelle's type checker infers a type with a type variable for the term mirror Typ, namely 'a tree where the type variable 'a has sort type. Since a 'a tree may contain values of 'a, the code generator also tries to generate code for pretty-printing 'a tree, which is implemented in the type class term_of. This fails however because the inferred type for 'a is type and not term_of, and that is the reason for the well-sortedness error.

The simplest way to avoid the error is to give a monomorphic type explicitly. For example,

value "mirror Tip :: nat tree"

should work.