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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
