[ProofPower] Re: Type-check bug?

[Roger Bishop Jones]

On Tuesday 21 September 2004  2:49 am, you Steve Brackin:
> After Roger Jones figured out that my problem came from type
> variables, I started trying to solve it by taking the first
> course he suggested, namely stating a more specific goal that
> explicitly mentions all the type variables;  that's what
> worked for me in HOL90.  I went back to my Z theory, intending
> to modify all my schema definitions so that every schema
> explicitly names every type variable that it uses.  This gave
> me another surprise, though, a "contains type variables not
> found in type of constants to be defined" error.  After
> sanitizing and pruning, I got it down to the following:
>
> new_theory "test";
> set_flag ("z_type_check_only", false);
> %SZS% S1 [TV1, TV2]
> %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH% %BV% x1: TV1;
> %BV% x2: %bbP% TV2
> ^
> %SZS% S2 [TV1, TV2]
> %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH% %BV% x3: %bbP% S1
> ^
> %SZS% S3 [TV1, TV2]
> %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH% %BV% x4: %bbP% S2
>
> So how does one tell pp that S3 depends on TV1 and TV2 but on
> no other type variables?

Type inference should give the most general type consistent
with the information available.
The type ambiguity arises primarily from the use of generic
entities without explicit instantiation or other use
from which inference can be made.
If there is nothing which constrains the type of the actual
generic parameters then they will be should be given a new type
variable.
That's my understanding of the situation, but I don't understand
why you don't get an error on S2, so maybe Rob can comment on
that.

To fix the problem you can explicitly instantiate the uses
of the generic schemas, e.g.:

> %SZS% S3 [TV1, TV2]
> %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH% %BV% x4: %bbP% 
S2[TV1, TV2]

Though these messages about type variables sound rather
ProofPower specific, they do correspond to real problems
of ambiguity in your specification.
You should be aware also when using implicit instantiation
of generics, that even if ProofPower can infer the type
it has no way of inferring the set.
It will always use the universe over the inferred type,
and this is unlikely to give the desired effect in this kind
of specification.

Roger Jones