Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-08 00:04:25 -0800 (Tue, 08 Feb 2005)
Revision: 6629
Log message:
I overlooked free type variables in the environment during existential
quantification in rules and rewrites. This fixes it. However, note
that rewrites like the following don't typecheck.
prim_rw add_sub_one :
('a in int) -->
'a <--> (('a +@ 1) -@ 1)
The rewrite is quite sensible in Itt, but problematic because it
applies to any term in the system (including display forms
for example). The quick solution is to add the constraint.
prim_rw add_sub_one ('a :> Term) :
('a in int) -->
'a <--> (('a +@ 1) -@ 1)
This is a bit suboptimal, but rewrites like this are very rare,
and the extra alpha-equality adds only O(1) overhead.