[isabelle-dev] auto raises a TYPE exception

[Stefan Berghofer]

On 05/27/2013 07:54 PM, Makarius wrote:
> Here is another example for Isabelle/Pure, without schematic variables with different types.  It may be be tried before/after my change 3b9c31867707 from today:
>
> [...]
>
> ML {*
>    val read = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_schematic @{context});
>    val a = read "a :: nat => bool";
>    val x = read "?x :: ?'b";
> *}
>
> ML {* Seq.list_of (Unify.hounifiers (@{theory}, Envir.empty 15, [(a, x)])); *}
> ML {* Seq.list_of (Unify.unifiers (@{theory}, Envir.empty 15, [(a, x)])); *}
> ML {* Pattern.unify @{theory} (a, x) (Envir.empty 15); *}
>
> Before the change, Unify.hounifiers crashes; after the change it is able to work out the type instantiation correctly.  Pattern.unify is still not quite there, neither before nor after the change.

Hi Markus,

there is a comment at the beginning of unify.ML saying that

   Types as well as terms are unified.  The outermost functions assume
   the terms to be unified already have the same type.  In resolution,
   this is assured because both have type "prop".

So it is the expected behaviour that the unification functions cannot cope with
the above example, since it does not satisfy this precondition.

Greetings,
Stefan