# [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.*