[isabelle] Solving a type class constraint


I'm trying to produce well-sorted terms in Isabelle/ML. Basically, I have a predicate "P" of type "'a" with some sort constraint, and I want to apply it to some polymorphic constant. Consider this small Isar snippet:

class foo
  P :: "'a::foo ⇒ bool"
  opt :: "'a option"

instantiation option :: (foo) foo
  instance ..

declare [[show_sorts]]

ML_val{* @{term "P opt"} *}

As is obvious from the output, type inference instantiates P's type to

  'a∷foo option ⇒ bool

The important bit here is that it slapped a "foo" constraint on the type variable.

However, it is not obvious to me how to do the same thing in ML. I mean, it's trivial to construct a well-typed term for "P opt":

fun mk_P t = Const (@{const_name P}, fastype_of t --> @{typ bool}) $ t;
  val t = mk_P @{term opt};
  val ct = cterm_of @{theory} t;

... but the sort constraint is missing on the instantiated type of "P".

A very "hackish" approximation for this problem is to go through "fastype_of t" and replace all sort constraints by "[foo]", because I can (sort of) assume that all my instantiations for "foo" only require "foo" for the type variables. I feel that there ought to be a better solution, though.

Why do I even need well-sorted terms? I have rules which look like this:

  P x ⟹ P (Some x)

and I cannot apply them unless the sorts line up.

(In my formalization, the type constructor is not "option", but "fun", but the idea is the same.)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.