Fix where under multiple cases

The names the locals were being applied to weren't being updated
properly, so applications of local functions inside case blocks were
sometimes given the wrong arguments. This is one of the few places where
it's hard to keep track of names in the type system! So naturally that'd
be where things go wrong I suppose...

src/Core/Env.idr

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

src/TTImp/Elab/App.idr

@@ -82,8 +82,9 @@ getVarType rigc nest env fc x
     = case lookup x (names nest) of
            Nothing => do (tm, ty) <- getNameType rigc env fc x
                          pure (tm, 0, ty)
-           Just (nestn, arglen, tmf) =>
+           Just (nestn, argns, tmf) =>
               do defs <- get Ctxt
+                 let arglen = length argns
                  let n' = maybe x id nestn
                  case !(lookupCtxtExact n' (gamma defs)) of
                       Nothing => throw (UndefinedName fc n')

src/TTImp/Elab/Case.idr

@@ -116,15 +116,24 @@ findScrutinee {vs = n' :: _} (b :: bs) (IVar loc' n)
     notLet _ = True
 findScrutinee _ _ = Nothing
 
-getNestData : (Name, (Maybe Name, Nat, a)) -> (Name, Maybe Name, Nat)
-getNestData (n, (mn, len, _)) = (n, mn, len)
+getNestData : (Name, (Maybe Name, List Name, a)) ->
+              (Name, Maybe Name, List Name)
+getNestData (n, (mn, enames, _)) = (n, mn, enames)
 
-bindCaseLocals : FC -> List (Name, Maybe Name, Nat) -> List Name -> RawImp -> RawImp
+bindCaseLocals : FC -> List (Name, Maybe Name, List Name) ->
+                 List (Name, Name)-> RawImp -> RawImp
 bindCaseLocals fc [] args rhs = rhs
-bindCaseLocals fc ((n, mn, len) :: rest) argns rhs
-    = ICaseLocal fc n (fromMaybe n mn)
-                 (take len argns)
+bindCaseLocals fc ((n, mn, envns) :: rest) argns rhs
+    = --trace ("Case local " ++ show (renvns ++ " from " ++ show argns) $
+        ICaseLocal fc n (fromMaybe n mn)
+                 (map getNameFrom (reverse envns))
                  (bindCaseLocals fc rest argns rhs)
+  where
+    getNameFrom : Name -> Name
+    getNameFrom n
+        = case lookup n argns of
+               Nothing => n
+               Just n' => n'
 
 export
 caseBlock : {vars : _} ->
@@ -198,6 +207,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
                            splitOn
 
          let alts' = map (updateClause casen splitOn nest env) alts
+         log 2 $ "Nested: " ++ show (map getNestData (names nest))
          log 2 $ "Generated alts: " ++ show alts'
          logTermNF 2 "Case application" env appTm
 
@@ -216,24 +226,25 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
                       else b in
               b' :: mkLocalEnv bs
 
-    getBindName : Int -> Name -> List Name -> Name
+    -- Return the original name in the environment, and what it needs to be
+    -- called in the case block. We need to mapping to build the ICaseLocal
+    -- so that it applies to the right original variable
+    getBindName : Int -> Name -> List Name -> (Name, Name)
     getBindName idx n@(UN un) vs
-       = if n `elem` vs then MN un idx else n
+       = if n `elem` vs then (n, MN un idx) else (n, n)
     getBindName idx n vs
-       = if n `elem` vs then MN "_cn" idx else n
+       = if n `elem` vs then (n, MN "_cn" idx) else (n, n)
 
-    -- Returns a list of names that nestednames should be applied to (skipping
-    -- the let bound ones) and a list of terms for the LHS of the case to be
-    -- applied to
-    addEnv : Int -> Env Term vs -> List Name -> (List Name, List RawImp)
+    -- Returns a list of names that nestednames should be applied to, mapped
+    -- to what the name has become in the case block, and a list of terms for
+    -- the LHS of the case to be applied to.
+    addEnv : Int -> Env Term vs -> List Name -> (List (Name, Name), List RawImp)
     addEnv idx [] used = ([], [])
     addEnv idx {vs = v :: vs} (b :: bs) used
         = let n = getBindName idx v used
-              (ns, rest) = addEnv (idx + 1) bs (n :: used)
-              ns' = case b of
-                         Let _ _ _ => ns
-                         _ => (n :: ns) in
-                   (ns', IAs fc UseLeft n (Implicit fc True) :: rest)
+              (ns, rest) = addEnv (idx + 1) bs (snd n :: used)
+              ns' = n :: ns in
+              (ns', IAs fc UseLeft (snd n) (Implicit fc True) :: rest)
 
     -- Replace a variable in the argument list; if the reference is to
     -- a variable kept in the outer environment (therefore not an argument
@@ -267,10 +278,10 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
 
     -- Get a name update for the LHS (so that if there's a nested data declaration
     -- the constructors are applied to the environment in the case block)
-    nestLHS : FC -> (Name, (Maybe Name, Nat, a)) -> (Name, RawImp)
-    nestLHS fc (n, (mn, len, t))
+    nestLHS : FC -> (Name, (Maybe Name, List Name, a)) -> (Name, RawImp)
+    nestLHS fc (n, (mn, ns, t))
         = (n, apply (IVar fc (fromMaybe n mn))
-                    (replicate len (Implicit fc False)))
+                    (map (const (Implicit fc False)) ns))
 
     applyNested : NestedNames vars -> RawImp -> RawImp
     applyNested nest lhs

src/TTImp/Elab/Local.idr

@@ -50,14 +50,14 @@ 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, Nat, FC -> NameType -> Term vars))
+               Core (Name, (Maybe Name, List Name, FC -> NameType -> Term vars))
     applyEnv outer inner
           = do ust <- get UST
                put UST (record { nextName $= (+1) } ust)
                let nestedName_in = Nested (outer, nextName ust) inner
                nestedName <- inCurrentNS nestedName_in
                n' <- addName nestedName
-               pure (inner, (Just nestedName, lengthNoLet env,
+               pure (inner, (Just nestedName, namesNoLet env,
                         \fc, nt => applyTo fc
                                (Ref fc nt (Resolved n')) env))
 
@@ -120,7 +120,9 @@ checkCaseLocal {vars} rig elabinfo nest env fc uname iname args sc expty
                          TCon t a _ _ _ _ _ _ => Ref fc (TyCon t a) iname
                          _ => Ref fc Func iname
          app <- getLocalTerm fc env name args
-         let nest' = record { names $= ((uname, (Just iname, length args,
+         log 5 $ "Updating case local " ++ show uname ++ " " ++ show args
+         logTermNF 10 "To" env app
+         let nest' = record { names $= ((uname, (Just iname, reverse args,
                                                 (\fc, nt => app))) :: ) }
                             nest
          check rig elabinfo nest' env sc expty

src/TTImp/ProcessDef.idr

@@ -314,10 +314,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, Nat, FC -> NameType -> Term vars))
+           Core (Name, (Maybe Name, List Name, FC -> NameType -> Term vars))
 applyEnv env withname
     = do n' <- resolveName withname
-         pure (withname, (Just withname, lengthNoLet env,
+         pure (withname, (Just withname, namesNoLet 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, Nat, FC -> NameType -> Term vs))
+               Core (Name, (Maybe Name, List Name, FC -> NameType -> Term vs))
     applyEnv env n
           = do n' <- resolveName n -- it'll be Resolved by expandAmbigName
-               pure (Resolved n', (Nothing, lengthNoLet env,
+               pure (Resolved n', (Nothing, namesNoLet env,
                         \fc, nt => applyTo fc
                                (Ref fc nt (Resolved n')) env))

src/TTImp/TTImp.idr

@@ -19,15 +19,15 @@ record NestedNames (vars : List Name) where
   -- 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,  -- new name if there is one
-                       Nat, -- length of the environment
+                       List Name, -- names used from the environment
                        FC -> NameType -> Term vars))
 
 export
 Weaken NestedNames where
   weaken (MkNested ns) = MkNested (map wknName ns)
     where
-      wknName : (Name, (Maybe Name, Nat, FC -> NameType -> Term vars)) ->
-                (Name, (Maybe Name, Nat, FC -> NameType -> Term (n :: vars)))
+      wknName : (Name, (Maybe Name, List Name, FC -> NameType -> Term vars)) ->
+                (Name, (Maybe Name, List Name, FC -> NameType -> Term (n :: vars)))
       wknName (n, (mn, len, rep)) = (n, (mn, len, \fc, nt => weaken (rep fc nt)))
 
 -- Unchecked terms, with implicit arguments

tests/Main.idr

@@ -80,7 +80,7 @@ idrisTests
        "record001", "record002",
        -- Miscellaneous regressions
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
-       "reg008", "reg009", "reg010", "reg011", "reg012", "reg013",
+       "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006",

tests/idris2/reg014/casecase.idr

@@ -0,0 +1,11 @@
+-- %logging 2
+test : List a -> Nat -> Nat
+test xs n
+    = case xs of
+           [] => Z
+           (y :: ys) => case n of
+                             Z => Z
+                             (S k) => calculate xs k
+  where
+    calculate : List a -> Nat -> Nat
+%logging 0

tests/idris2/reg014/expected

@@ -0,0 +1 @@
+1/1: Building casecase (casecase.idr)

tests/idris2/reg014/run

@@ -0,0 +1,3 @@
+$1 casecase.idr --check --debug-elab-check
+
+rm -rf build