[isabelle-dev] auto raises a TYPE exception

[Makarius]

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