[isabelle] Schematic type variable


I'm experimenting with matching a pattern containing schematic type
variables and it'd be great if someone could clarify the following:

1) match "?x (?y::?'a)" against "(p::(nat=>nat) => nat) q"

ML {*
val trm = @{term "(p::(nat\<Rightarrow>nat) \<Rightarrow> nat) q "};
val pat = @{cpat "?x (?y::?'a)"} |> term_of;
val mtchs = Unify.matchers @{theory} [(pat,trm)] |> Seq.list_of;

Unsurprisingly, I get a substitution with ?y::nat=>nat := q.

2) match "?x (?y::?'a) against "(p::nat=>nat) q"

Here, I don't get a substitution where ?y is instantiated to the function
p::nat=>nat. Why can't ?'a be instantiated to nat=>nat like in 1)? I get
that substitution when ?y::?'a=>?'b though.

Any help will be appreciated.


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