diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr
index 189df4273..d775148ec 100644
--- a/src/TTImp/ProcessDef.idr
+++ b/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
diff --git a/tests/Main.idr b/tests/Main.idr
index 3180b6da1..1c4692e83 100644
--- a/tests/Main.idr
+++ b/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
diff --git a/tests/idris2/linear017/As.idr b/tests/idris2/linear017/As.idr
new file mode 100644
index 000000000..eba40c303
--- /dev/null
+++ b/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
diff --git a/tests/idris2/linear017/expected b/tests/idris2/linear017/expected
new file mode 100644
index 000000000..b1f7dad97
--- /dev/null
+++ b/tests/idris2/linear017/expected
@@ -0,0 +1 @@
+1/1: Building As (As.idr)
diff --git a/tests/idris2/linear017/run b/tests/idris2/linear017/run
new file mode 100644
index 000000000..4b4d889dd
--- /dev/null
+++ b/tests/idris2/linear017/run
@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner --check As.idr
+
+rm -r build