Ignore UseSide annotation in non-linear as-patterns (#2984)

Co-authored-by: Aleksei Volkov <volkov.aa@phystech.edu>

src/TTImp/ProcessDef.idr

@@ -285,10 +285,12 @@ findLinear top bound rig tm
       findLinArg : {vars : _} ->
                    RigCount -> NF [] -> List (Term vars) ->
                    Core (List (Name, RigCount))
-      findLinArg rig ty (As fc UseLeft _ p :: as)
-          = findLinArg rig ty (p :: as)
-      findLinArg rig ty (As fc UseRight p _ :: as)
-          = findLinArg rig ty (p :: as)
+      findLinArg rig ty@(NBind _ _ (Pi _ c _ _) _) (As fc u a p :: as)
+          = if isLinear c
+               then case u of
+                         UseLeft => findLinArg rig ty (p :: as)
+                         UseRight => findLinArg rig ty (a :: as)
+               else pure $ !(findLinArg rig ty [a]) ++ !(findLinArg rig ty (p :: as))
       findLinArg rig (NBind _ x (Pi _ c _ _) sc) (Local {name=a} fc _ idx prf :: as)
           = do defs <- get Ctxt
                let a = nameAt prf

tests/Main.idr

@@ -133,7 +133,8 @@ idrisTestsLinear = MkTestPool "Quantities" [] Nothing
        ["linear001", "linear002", "linear003", -- "linear004" -- disabled due to requiring linearity subtyping
         "linear005", "linear006", "linear007", "linear008",
         "linear009", "linear010", "linear011", "linear012",
-        "linear013", "linear014", "linear015", "linear016"]
+        "linear013", "linear014", "linear015", "linear016",
+        "linear017"]
 
 idrisTestsLiterate : TestPool
 idrisTestsLiterate = MkTestPool "Literate programming" [] Nothing

tests/idris2/linear017/As.idr

@@ -0,0 +1,13 @@
+-- Reduction of https://gist.github.com/AlgebraicWolf/0d921915d7aca032e35831c73c8d04f4
+
+-- See Discord discussion for further context:
+-- https://discord.com/channels/827106007712661524/954409815088721920/1108129142756606102
+
+data X : Nat -> Type where
+  IZ : X Z
+  IS : (0 n : _) -> X n -> X (S n)
+
+g : (m : Nat) -> X m -> Nat
+
+g (S m@(S m')) (IS .(S m') k) = g (S m') k
+g _ _ = 0

tests/idris2/linear017/expected

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

tests/idris2/linear017/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner --check As.idr
+
+rm -r build