@@ -1405,7 +1405,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
1405 -- Build the LHS as an "Infer", and pull out its type and
1405 -- Build the LHS as an "Infer", and pull out its type and
1406 -- pattern bindings
1406 -- pattern bindings
1407 i <- getIState
1407 i <- getIState
1408− let lhs = addImplPat i lhs_in
1408+ let lhs = addImplPat i (stripLinear i lhs_in)
1409 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
1409 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
1410 ((lhs', dlhs, []), _) <-
1410 ((lhs', dlhs, []), _) <-
1411 tclift $ elaborate ctxt (MN 0 "patLHS") infP []
1411 tclift $ elaborate ctxt (MN 0 "patLHS") infP []