diff --git a/src/Compiler/LambdaLift.idr b/src/Compiler/LambdaLift.idr index 001c43e55f..46d6b5b347 100644 --- a/src/Compiler/LambdaLift.idr +++ b/src/Compiler/LambdaLift.idr @@ -368,10 +368,6 @@ mutual update Lifts { defs $= ((n, MkLFun (used us) bound scl') ::) } pure $ LUnderApp fc n (length bound) (allVars fc vars us) where - allPrfs : (vs : List Name) -> (unused : Vect (length vs) Bool) -> List (Var vs) - allPrfs [] _ = [] - allPrfs (v :: vs) (False::uvs) = MkVar First :: map weaken (allPrfs vs uvs) - allPrfs (v :: vs) (True::uvs) = map weaken (allPrfs vs uvs) -- apply to all the variables. 'First' will be first in the last, which -- is good, because the most recently bound name is the first argument to diff --git a/src/Core/TT/Var.idr b/src/Core/TT/Var.idr index 39009f63a4..3fa7ac959e 100644 --- a/src/Core/TT/Var.idr +++ b/src/Core/TT/Var.idr @@ -521,8 +521,8 @@ usedIsVar : usedIsVar (False :: bs) First = assert_total $ idris_crash "INTERNAL ERROR: Referenced variable marked as unused" usedIsVar (True :: bs) First = MkNVar First -usedIsVar (False :: bs) (Later p) = usedIsVar (bs) p -usedIsVar (True :: bs) (Later p) = later (usedIsVar (bs) p) +usedIsVar (False :: bs) (Later p) = usedIsVar bs p +usedIsVar (True :: bs) (Later p) = later (usedIsVar bs p) export usedNVar : (us : Used vars) -> NVar nm vars -> NVar nm (used us)