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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and