[isabelle-dev] Additional type variable(s) in specification
matthews at galois.com
Thu Dec 2 21:06:39 CET 2010
> What you specify is a type constraint for the main body of the
> specification text. There can be a mismatch of what the system
> infers as most general type and what you've had in mind. There can
> be also surprises due to type abbreviations.
> Which situation did you have exactly?
I don't have the original sources at hand, but it was something like
consts my_overloaded_const :: "(int * 'a)"
definition foo :: "int ⇒ int" where
"foo x = x + fst my_overloaded_const"
But what Isabelle gives back is
foo :: 'a itself ⇒ int ⇒ int
which is neither a generalization nor a specialization of the type
signature we gave it. Originally this was part of some automatically-
generated Isabelle theories, so we didn't see any of the warning
Instead, Isabelle started giving us (what we thought were) strange
type errors when we started using the constant in theories that
inherited from the automatically generated theory.
We figured out what was going on and fixed the translator, but it
would have saved us time and confusion if Isabelle had stopped and
given us an error when we tried to define foo.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 2205 bytes
Desc: not available
More information about the isabelle-dev