[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Tue May 28 14:11:31 CEST 2013
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)) =>
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
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
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
More information about the isabelle-dev