Bug in System F evaluation code

Describe the bug
I was attempting to implement the PairADT existential type in the System Fw project (from Ch30.2) to test typechecking. I manually implemented it with macros, but the System F parser confirms that the macro was writtern correctly:

TyAbs(TyAbs(Abs(TyVar(1), Abs(TyVar(0), TyAbs(Abs((TyVar(2)->(TyVar(1)->TyVar(0))), App(App(Var(0), Var(2)), Var(1))))))))

It is currently not properly typechecking, so I decided to debug, and see if I could typecheck it in System F.

repl: \X \Y \x: X. \y: Y. \R \p: X->Y->R. p x y

| 1 \X \Y \x: X. \y: Y. \R \p: X->Y->R. p x y
                                       ^~~^ --- Type mismatch in application
                                       ^^ --- Abstraction requires type TyVar(2)
                                         ^^ --- Value has a type of TyVar(1)

The term parses correctly, but does not typecheck. Moving the \R type abstraction outside allows it to typecheck however.

\X \Y \R \x: X. \y: Y. \p: X->Y->R. p x y

During debugging of this, I discovered a secondary bug lurking somewhere in the evaluator. The following expression properly typechecks, but gives a bogus substitution during evaluation:

repl: (\x: Nat. \Y \y: Nat->Y. y x) 10 [Nat] succ
    -: Nat
---> (((λTy (λ_:(Nat->TyVar(0)). (#0 #1))) [Nat]) Succ)
---> ((λ_:(Nat->Nat). (#0 #0)) Succ) <--- erroneous term variable shifting here
---> (Succ Succ)
===> (Succ Succ)

This should evaluate to 11 instead

After thinking about this for a couple minutes, I think this might be another issue due to how I track de Bruijn indices vs. how Pierce tracks them. In TaPL, both Term and Type level variables are tracked on the same stack/indexes, but I keep them separate. This is probably causing issues where he needs to downshift terms but I do not

Commenting out the visit_tyabs overloaded function in terms::visit seems to do the trick! We only bind type level variables here, so we don't actually need to bump the cutoff

types-and-programming-languages/system_f/src/terms/visit.rs

Lines 25 to 29 in 3eb7ff5

    
           fn visit_abs(&mut self, sp: &mut Span, ty: &mut Type, term: &mut Term) { 
        
               self.cutoff += 1; 
        
               self.visit(term); 
        
               self.cutoff -= 1; 
        
           }

Interesting to note that the evaluator appears to be substituting TyAbs/TyApp properly, but the typechecker is not

repl: (\X \Y \x: X. \y: Y. \R \p: X->Y->R. x) [Nat] [Bool] 10 true
  -: forall X.((Nat->(Bool->TyVar(0)))->Bool)
---> ((((λTy (λ_:Nat. (λ_:TyVar(0). (λTy (λ_:(Nat->(TyVar(1)->TyVar(0))). #2))))) [Bool]) 10) true)
---> (((λ_:Nat. (λ_:Bool. (λTy (λ_:(Nat->(Bool->TyVar(0))). #2)))) 10) true)
---> ((λ_:Bool. (λTy (λ_:(Nat->(Bool->TyVar(0))). 10))) true)
---> (λTy (λ_:(Nat->(Bool->TyVar(0))). 10))
===> (λTy (λ_:(Nat->(Bool->TyVar(0))). 10))

thread 'main' panicked at 'Type of term after evaluation is different than before!
1 forall X.((Nat->(Bool->TyVar(0)))->Bool)
2 forall X.((Nat->(Bool->TyVar(0)))->Nat)', system_f\src\main.rs:85:9

Note that the second term (after evaluation) is correct! Something going on once again with how we're keeping track of vars inside of the typing context

This is pretty much the minimal example:

(\X \x: X. \R \p: X->R. x) [Nat] 1

or

(\X \x: X. \R \p: X->R. p x) [Nat] 1 [Nat] succ

	fn visit_abs(&mut self, sp: &mut Span, ty: &mut Type, term: &mut Term) {
	self.cutoff += 1;
	self.visit(term);
	self.cutoff -= 1;
	}