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