[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Mon, 27 May 2013, Makarius wrote:

> The change ensures that variables with equal name are unified, in the 
> same manner as the types of Free or Const are unified, before doing the 
> real work of HO-unification.

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 {* toplevel_pp ["term"] "Proof_Display.pp_term Pure.thy" *}
declare [[show_types]]

typedecl nat
typedecl bool

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.


Note that the original implementation by Larry did try to unify the result 
types in any case, using the body_type function.  But that was assuming 
that the arity of the function type happens to coincide with the number of 
arguments in the term application.

This is why I introduced optional bounds to the function type traversal in 
envir.ML 7f3549a316f4.  Note that in 3b9c31867707 the type unification of 
the disagreement pair is done explicitly via unify_types_of, without 
taking the functions apart, but also see the modification of assignment 
where these bounds correspond to the number of actual arguments.


For the moment, I am not going to produce more changes.  Maybe Larry and 
Tobias also want to comment, as the authors of these modules from some 
decades ago.  Stefan is of course the proven expert who re-investigated 
quite a lot of that around 2000.


 	Makarius