[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Tue, 28 May 2013, Lawrence Paulson wrote:

> Historical note: when the original high-order unification code was 
> written, there was no user-level polymorphism. If my memory is correct, 
> the TVar constructor did not even exist.

This fits to my speculations when reading the code, and I've tried to 
take it into account.


> Any idea to unify types while at the same time identifying previously 
> distinct variables needs to be scrutinised with very great care. Better 
> to have an exception raised than to have unsound reasoning.

I agree with that, and I am ready to backout the change when we understand 
the overall situation better, and it turns out as too risky.


Just one note on your version of SIMPL0 (in 6228806b2605):

     (case (head_of t, head_of u) of
       (Var (_, T), Var (_, U)) =>
         let
           val T' = Envir.body_type env ~1 T and U' = Envir.body_type env ~1 U;
           val env = unify_types thy (T', U') env;
         in (env, dp :: flexflex, flexrigid) end

Here it looks like you are trying to unify the effective types of t and u, 
where the two Vars appear in the heads.  The arguments are treated 
specially later, so only the result types are taken into account 
(body_type).

This does not quite work if the results happen to be functions, maybe even 
of varying arity.  The unrestricted traversal of body_type does not know 
where to stop, just from looking at the type.  Thus it might unify too 
little, or produce somehow inconsistent type assignments later, maybe even 
malformed ones.


In my version 3b9c31867707 there is first unify_types_of for t and u 
outright, without any special cases, and unify_types for the types of the 
variables if they have equal names.  So it is similar to what you did 
before, but a bit more "thorough" as it is called in the changelog.

I did not dare to do the same in pattern.ML as well, since that works 
quite differently, and is more critical for performance as well.  I merely 
imitated Larry in doing some restricted body_type unification, in a 
homeopathic manner.


 	Makarius