Re: [isabelle] Schematic type variable
There may be a mistake in your question, since I would expect y to be instantiated to q, not p. However, as a general rule, a type variable cannot be instantiated to a function type during higher-order unification. The reason for this restriction is that otherwise the search space would be unmanageable. I believe it is relaxed when the unification is essentially first-order.
On 19 Oct 2011, at 21:32, Steve Wong wrote:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and