[isabelle-dev] auto raises a TYPE exception

[Lawrence Paulson]

I don't quite understand your commentary, because the result of body_type can never be a function.

In general, polymorphism in higher-order unification never instantiates a type variable to a function type, for the reason you seem to hint at: because you wouldn't know when to stop. This is a source of incompleteness, but it has always been there.

Larry

On 28 May 2013, at 13:11, Makarius <makarius at sketis.net> wrote:

> 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