[isabelle-dev] Additional type variable(s) in specification

[John Matthews]

> 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  
this:

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  
messages.

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.

-john



-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2205 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101202/5f915369/attachment.bin>