[ fix ] case spliting under implicit/auto parameter

[dunhamsteve]

Description

This fixes #2331. When calculating the cases, the case splitting code was inserting _ for all of the local environment arguments, regardless of whether they are explicit or not. This works for functions in where clauses where these arguments are always explicit, but not for parameter blocks if they have implicit or auto arguments. The fix will only return _ for the explicit positions.

Included test case from #2331, which now splits:

parameters {auto _ : ()}
  f : Nat -> Nat
  f m = ?a

as

parameters {auto _ : ()}
  f : Nat -> Nat
  f 0 = ?a_0
  f (S k) = ?a_1

An alternative approach would return arguments for implicit positions too:

diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr
index e74131455..3f4e60bcb 100644
--- a/src/TTImp/Interactive/CaseSplit.idr
+++ b/src/TTImp/Interactive/CaseSplit.idr
@@ -196,8 +196,11 @@ newLHS : {auto c : Ref Ctxt Defs} ->
          RawImp -> Core RawImp
 newLHS fc envlen allvars var con tm
     = do let (f, args) = getFnArgs tm []
-         let keep = map (const (Explicit fc (Implicit fc True)))
-                        (take envlen args)
+         let keep = map (\case
+                            (Explicit fc' t) => Explicit fc (Implicit fc' True)
+                            (Auto fc' t) => Auto fc' (Implicit fc' True)
+                            (Named fc' n t) => Named fc' n (Implicit fc' True))
+                        (take envlen args)
          let ups = drop envlen args
          ups' <- traverse (update allvars var con) ups
          pure $ apply f (keep ++ ups')