[isabelle-dev] auto raises a TYPE exception

[Lawrence Paulson]

the disagreement pairs should be fully eta-expanded by this point, though I haven't looked at the code recently. That would imply that the body_type cannot be a function type.

Larry

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

> On Tue, 28 May 2013, Lawrence Paulson wrote:
> 
>> 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.
> 
> The function type could have been there already from the start, e.g.:
> 
>  ?x i j k :: ?'a => ?'b
> 
> for
> 
>  ?x :: U => V => W => ?'a => ?'b
> 
> where i :: U, j :: V, k :: W in the term context.
> 
> In that case, the unrestricted body_type would merely take ?'b into account of the unification problem, not the remaining ?'a => ?'b.
> 
> 
> It is just a habit of mine to watch out for such incidents -- we used to have them in many situations in the past when traversing ==> of the logic. And of course, such doubts are no disproof of anything, just critical observations.
> 
> 
> 	Makarius