Re: [isabelle] type error



On Thu, 18 Nov 2010, Viorel Preoteasa wrote:


On 11/18/2010 4:13 PM, Lawrence Paulson wrote:
The following warning should alert you to the problem:

### Additional type variable(s) in specification of disjunctive: 'd
Thank you for your answer. I have figured it out myself finally. I had this
problem before, but I forgot about it.


For more information, switch on “show types" and you can locate the occurrence of 'd

Test.disjunctive_def:
   disjunctive TYPE(?'d) (?R::?'a =>  ?'b =>  ?'c) =
   (ALL P::?'d =>  ?'a =>  ?'b. (?R .. SUP P) = SUP (%w::?'d. ?R .. P w))

An implicit type parameter has been generated in order to ensure that this definition is sound. Probably you should make the right hand side of your definition more specific.

Wouldn't be better is Isabelle would give an error already when
defining something which depends on an additional type variable?

This problem of "hidden polymorphism" is notorious since very early versions of Gordon-style HOL. After several years of spurious crashes in Isabelle, we are now in the state where the infrastructure is able to treat it robustly in most situations, despite remaining surprises as experienced above.

The deeper problem here is that it depends on the context of a specification if a locally fixed type variable is really "polymorphic" and thus leads to extra TYPE arguments, or not. In general it is not an error.

Warnings are traditionally hardly visible in Proof General interaction. This is about to improve very soon in the editor view.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.