Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-06 15:21:43 -0800 (Sun, 06 Feb 2005)
Revision: 6607
Log message:
Typechecking is now stricter.
-- For rules and rewrites, the goal types are existentially quantified.
-- Rewrites are type-invariant. For example, the following will fail.
declare typeclass A
declare typeclass B -> A
declare foo : A
declare bar : B
prim_rw bad : foo <--> bar
This is rejected because the (bar --> foo) rewrite is bogus.
At this point, the type system is basically sound, apart from
rule and rewrite arguments, and assuming the implementation is
correct. Let's merge.