[isabelle-dev] auto raises a TYPE exception

Makarius makarius at sketis.net
Tue May 28 17:11:57 CEST 2013

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


   ?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 


More information about the isabelle-dev mailing list