Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-27 19:53:50 -0800 (Thu, 27 Jan 2005)
Revision: 6518
Log message:

      Here is the plan:
         1. Make non-extensible typeclasses.
      
            define typeclass Ty1 =
               TyExp
             | KindExp
      
            Non-extensible means that it is illegal to extend the type
            afterwards.
      
               declare FooExp : Ty1
      
            The reason is because of negative type constraints (step 3).
      
         2. Add non-canonical types.
      
            define type TyElem{'a : Ty1} : Ty
            define type TyElem{TyExp} <--> Exp
            define type TyElem{KindExp} <--> TyExp
      
         3. Add limited dependent types.
      
            declare sequent { TyElem{'a} : ('a :> Ty1) >- Prop } : Prop
      
         4. Add dependent type checking.  This is undecidable *in general*
            but decidable if suitably restricted.
      

Changes	Path
+6 -3	metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.ml
+6 -3	metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.mli