Count argument position in parameter blocks

We need to know where we are so that we know if we're at an
erasable/detaggable argument position

src/Core/Binary.idr

@@ -221,7 +221,7 @@ readTTCFile modns as b
 --            coreLift $ putStrLn $ "Read " ++ show (length guesses) ++ " guesses"
 --            constraints <- the (Core (List (Int, Constraint))) $ fromBuf b
 --            coreLift $ putStrLn $ "Read " ++ show (length constraints) ++ " constraints"
-           defs <- logTime "Definitions" $ fromBuf b
+           defs <- logTime ("Definitions " ++ show modns) $ fromBuf b
            uholes <- fromBuf b
            autohs <- fromBuf b
            typehs <- fromBuf b

src/Core/Env.idr

@@ -17,6 +17,12 @@ length : Env tm xs -> Nat
 length [] = 0
 length (_ :: xs) = S (length xs)
 
+export
+lengthNoLet : Env tm xs -> Nat
+lengthNoLet [] = 0
+lengthNoLet (Let _ _ _ :: xs) = lengthNoLet xs
+lengthNoLet (_ :: xs) = S (lengthNoLet xs)
+
 public export
 data IsDefined : Name -> List Name -> Type where
   MkIsDefined : {idx : Nat} -> RigCount -> .(IsVar n idx vars) ->

src/TTImp/Elab/App.idr

@@ -77,11 +77,12 @@ getVarType : {vars : _} ->
              {auto e : Ref EST (EState vars)} ->
              RigCount -> NestedNames vars -> Env Term vars ->
              FC -> Name ->
-             Core (Term vars, Glued vars)
+             Core (Term vars, Nat, Glued vars)
 getVarType rigc nest env fc x
     = case lookup x (names nest) of
-           Nothing => getNameType rigc env fc x
+           Nothing => do (tm, ty) <- getNameType rigc env fc x
-           Just (nestn, tmf) =>
+                         pure (tm, 0, ty)
+           Just (nestn, arglen, tmf) =>
               do defs <- get Ctxt
                  let n' = maybe x id nestn
                  case !(lookupCtxtExact n' (gamma defs)) of
@@ -98,7 +99,7 @@ getVarType rigc nest env fc x
                              do checkVisibleNS fc (fullname ndef) (visibility ndef)
                                 logTerm 10 ("Type of " ++ show n') tyenv
                                 logTerm 10 ("Expands to") tm
-                                pure (tm, gnf env tyenv)
+                                pure (tm, arglen, gnf env tyenv)
     where
       useVars : List (Term vars) -> Term vars -> Term vars
       useVars [] sc = sc
@@ -524,7 +525,7 @@ checkApp rig elabinfo nest env fc (IApp fc' fn arg) expargs impargs exp
 checkApp rig elabinfo nest env fc (IImplicitApp fc' fn nm arg) expargs impargs exp
    = checkApp rig elabinfo nest env fc' fn expargs ((nm, arg) :: impargs) exp
 checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
-   = do (ntm, nty_in) <- getVarType rig nest env fc n
+   = do (ntm, arglen, nty_in) <- getVarType rig nest env fc n
         nty <- getNF nty_in
         elabinfo <- updateElabInfo (elabMode elabinfo) n expargs elabinfo
         logC 10 (do defs <- get Ctxt
@@ -539,7 +540,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
                           " to " ++ show expargs ++ "\n\tFunction type " ++
                           (show !(toFullNames fnty)) ++ "\n\tExpected app type "
                                 ++ show exptyt))
-        checkAppWith rig elabinfo nest env fc ntm nty (Just n, 0) expargs impargs False exp
+        checkAppWith rig elabinfo nest env fc ntm nty (Just n, arglen) expargs impargs False exp
   where
     isPrimName : List Name -> Name -> Bool
     isPrimName [] fn = False

src/TTImp/Elab/Case.idr

@@ -317,7 +317,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
 
          let alts' = map (updateClause casen splitOn env smaller) alts
          log 2 $ "Generated alts: " ++ show alts'
-         let nest' = record { names $= ((Resolved cidx, (Nothing,
+         let nest' = record { names $= ((Resolved cidx, (Nothing, length pre_env,
                                   (\fc, nt => applyToFull fc caseRef pre_env))) ::) }
                             nest
          processDecl [InCase] nest' pre_env (IDef fc casen alts')

src/TTImp/Elab/Local.idr

@@ -49,11 +49,11 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
              else b :: dropLinear bs
 
     applyEnv : {auto c : Ref Ctxt Defs} -> Int -> Name ->
-               Core (Name, (Maybe Name, FC -> NameType -> Term vars))
+               Core (Name, (Maybe Name, Nat, FC -> NameType -> Term vars))
     applyEnv outer inner
           = do let nestedName = Nested outer inner
                n' <- addName nestedName
-               pure (inner, (Just nestedName,
+               pure (inner, (Just nestedName, lengthNoLet env,
                         \fc, nt => applyTo fc
                                (Ref fc nt (Resolved n')) env))
 

src/TTImp/ProcessDef.idr

@@ -309,10 +309,10 @@ hasEmptyPat defs env _ = pure False
 -- For checking with blocks as nested names
 applyEnv : {auto c : Ref Ctxt Defs} ->
            Env Term vars -> Name ->
-           Core (Name, (Maybe Name, FC -> NameType -> Term vars))
+           Core (Name, (Maybe Name, Nat, FC -> NameType -> Term vars))
 applyEnv env withname
     = do n' <- resolveName withname
-         pure (withname, (Just withname,
+         pure (withname, (Just withname, lengthNoLet env,
                   \fc, nt => applyTo fc
                          (Ref fc nt (Resolved n')) env))
 

src/TTImp/ProcessParams.idr

@@ -57,9 +57,9 @@ processParams {vars} {c} {m} {u} nest env fc ps ds
        = IPi fc RigW Explicit (Just n) ty (mkParamTy ps)
 
     applyEnv : Env Term vs -> Name ->
-               Core (Name, (Maybe Name, FC -> NameType -> Term vs))
+               Core (Name, (Maybe Name, Nat, FC -> NameType -> Term vs))
     applyEnv env n
           = do n' <- resolveName n -- it'll be Resolved by expandAmbigName
-               pure (Resolved n', (Nothing,
+               pure (Resolved n', (Nothing, lengthNoLet env,
                         \fc, nt => applyTo fc
                                (Ref fc nt (Resolved n')) env))

src/TTImp/TTImp.idr

@@ -18,15 +18,17 @@ record NestedNames (vars : List Name) where
   -- applied to its enclosing environment
   -- Takes the location and name type, because we don't know them until we
   -- elaborate the name at the point of use
-  names : List (Name, (Maybe Name, FC -> NameType -> Term vars))
+  names : List (Name, (Maybe Name,  -- new name if there is one
+                       Nat, -- length of the environment
+                       FC -> NameType -> Term vars))
 
 export
 Weaken NestedNames where
   weaken (MkNested ns) = MkNested (map wknName ns)
     where
-      wknName : (Name, (Maybe Name, FC -> NameType -> Term vars)) ->
+      wknName : (Name, (Maybe Name, Nat, FC -> NameType -> Term vars)) ->
-                (Name, (Maybe Name, FC -> NameType -> Term (n :: vars)))
+                (Name, (Maybe Name, Nat, FC -> NameType -> Term (n :: vars)))
-      wknName (n, (mn, rep)) = (n, (mn, \fc, nt => weaken (rep fc nt)))
+      wknName (n, (mn, len, rep)) = (n, (mn, len, \fc, nt => weaken (rep fc nt)))
 
 -- Unchecked terms, with implicit arguments
 -- This is the raw, elaboratable form.