[isabelle] Solving a type class constraint



Hello,

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
consts
  P :: "'a::foo ⇒ bool"
  opt :: "'a option"

instantiation option :: (foo) foo
begin
  instance ..
end

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":

ML{*
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.)

Cheers
Lars




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