[ fix ] Handle PLet in setLinear

Author: spcfox

CHANGELOG_NEXT.md

@@ -36,6 +36,7 @@ should target this file (`CHANGELOG_NEXT`).
   typically happens when a numeric literal or an ambiguous name appears in an
   `impossible` clause.
 * Do not inline `Core.sequence`, because it is recursively defined.
+* Fixed incorrect argument multiplicity when using an as-pattern (#3687).
 
 ### Building/Packaging changes
 

src/TTImp/ProcessDef.idr

@@ -310,14 +310,17 @@ findLinear top bound rig tm
       findLinArg _ _ [] = pure []
 
 setLinear : List (Name, RigCount) -> Term vars -> Term vars
-setLinear vs (Bind fc x b@(PVar {}) sc)
-    = case lookup x vs of
-           Just c' => Bind fc x (setMultiplicity b c') (setLinear vs sc)
-           _ => Bind fc x b (setLinear vs sc)
-setLinear vs (Bind fc x b@(PVTy {}) sc)
-    = case lookup x vs of
-           Just c' => Bind fc x (setMultiplicity b c') (setLinear vs sc)
-           _ => Bind fc x b (setLinear vs sc)
+setLinear vs (Bind fc x b sc)
+    = do let b' = case guard (isPatternBinder b) *> lookup x vs of
+                       Just c' => setMultiplicity b c'
+                       Nothing => b
+         Bind fc x b' (setLinear vs sc)
+  where
+    isPatternBinder : Binder a -> Bool
+    isPatternBinder (PVar {}) = True
+    isPatternBinder (PVTy {}) = True
+    isPatternBinder (PLet {}) = True
+    isPatternBinder _ = False
 setLinear vs tm = tm
 
 -- Combining multiplicities on LHS:

tests/idris2/linear/linear018/Issue3687.idr

@@ -0,0 +1,5 @@
+data X : Nat -> Type where
+  XS : X (S n)
+
+f : () -> (n : Nat) -> X n -> Nat
+f b@() .(S m) XS = ?hole

tests/idris2/linear/linear018/expected

@@ -0,0 +1,7 @@
+1/1: Building Issue3687 (Issue3687.idr)
+Main>    b : ()
+ 0 m : Nat
+------------------------------
+hole : Nat
+Main> 
+Bye for now!

tests/idris2/linear/linear018/input

@@ -0,0 +1 @@
+:t hole

tests/idris2/linear/linear018/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+idris2 Issue3687.idr < input