From c13e87adbcca71be79fe2760383391a2bb80cf0a Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Thu, 15 Jun 2023 20:56:05 +0100
Subject: [PATCH 01/10] Flatten a CPS to an accumulator

---
 src/Compiler/Checking/PostInferenceChecks.fs | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Compiler/Checking/PostInferenceChecks.fs b/src/Compiler/Checking/PostInferenceChecks.fs
index 145c7e0799c..481973c8432 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fs
+++ b/src/Compiler/Checking/PostInferenceChecks.fs
@@ -975,12 +975,12 @@ and CheckCallWithReceiver cenv env m returnTy args ctxts ctxt =
                 limitArgs
         CheckCallLimitArgs cenv env m returnTy limitArgs ctxt
 
-and CheckExprLinear (cenv: cenv) (env: env) expr (ctxt: PermitByRefExpr) (contf : Limit -> Limit) =    
+and CheckExprLinear (cenv: cenv) (env: env) expr (ctxt: PermitByRefExpr) (acc : Limit) : Limit =
     match expr with
     | Expr.Sequential (e1, e2, NormalSeq, _) -> 
         CheckExprNoByrefs cenv env e1
         // tailcall
-        CheckExprLinear cenv env e2 ctxt contf
+        CheckExprLinear cenv env e2 ctxt acc
 
     | Expr.Let (TBind(v, _bindRhs, _) as bind, body, _, _) ->
         let isByRef = isByrefTy cenv.g v.Type
@@ -995,27 +995,27 @@ and CheckExprLinear (cenv: cenv) (env: env) expr (ctxt: PermitByRefExpr) (contf
         BindVal cenv env v
         LimitVal cenv v { limit with scope = if isByRef then limit.scope else env.returnScope }
         // tailcall
-        CheckExprLinear cenv env body ctxt contf 
+        CheckExprLinear cenv env body ctxt acc
 
     | LinearOpExpr (_op, tyargs, argsHead, argLast, m) ->
         CheckTypeInstNoByrefs cenv env m tyargs
         argsHead |> List.iter (CheckExprNoByrefs cenv env) 
         // tailcall
-        CheckExprLinear cenv env argLast PermitByRefExpr.No (fun _ -> contf NoLimit)
+        CheckExprLinear cenv env argLast PermitByRefExpr.No NoLimit
 
     | LinearMatchExpr (_spMatch, _exprm, dtree, tg1, e2, m, ty) ->
         CheckTypeNoInnerByrefs cenv env m ty 
         CheckDecisionTree cenv env dtree
         let lim1 = CheckDecisionTreeTarget cenv env ctxt tg1
         // tailcall
-        CheckExprLinear cenv env e2 ctxt (fun lim2 -> contf (CombineLimits [ lim1; lim2 ]))
+        CheckExprLinear cenv env e2 ctxt (CombineTwoLimits lim1 acc)
 
     | Expr.DebugPoint (_, innerExpr) -> 
-        CheckExprLinear cenv env innerExpr ctxt contf
+        CheckExprLinear cenv env innerExpr ctxt acc
 
     | _ -> 
         // not a linear expression
-        contf (CheckExpr cenv env expr ctxt)
+        CheckExpr cenv env expr ctxt
 
 /// Check a resumable code expression (the body of a ResumableCode delegate or
 /// the body of the MoveNextMethod for a state machine)
@@ -1143,7 +1143,7 @@ and CheckExpr (cenv: cenv) (env: env) origExpr (ctxt: PermitByRefExpr) : Limit =
     | Expr.Let _ 
     | Expr.Sequential (_, _, NormalSeq, _)
     | Expr.DebugPoint _ -> 
-        CheckExprLinear cenv env expr ctxt id
+        CheckExprLinear cenv env expr ctxt NoLimit
 
     | Expr.Sequential (e1, e2, ThenDoSeq, _) -> 
         CheckExprNoByrefs cenv env e1

From 2096185825e8c8c3a20d0769a4e8167e546bfd4e Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Fri, 16 Jun 2023 19:10:37 +0100
Subject: [PATCH 02/10] Expose members for test

---
 src/Compiler/Checking/PostInferenceChecks.fs  | 131 +++++++++---------
 src/Compiler/Checking/PostInferenceChecks.fsi |  16 +++
 2 files changed, 83 insertions(+), 64 deletions(-)

diff --git a/src/Compiler/Checking/PostInferenceChecks.fs b/src/Compiler/Checking/PostInferenceChecks.fs
index 481973c8432..b95c276ca61 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fs
+++ b/src/Compiler/Checking/PostInferenceChecks.fs
@@ -124,71 +124,74 @@ let BindTypars g env (tps: Typar list) =
 let BindArgVals env (vs: Val list) = 
     { env with argVals = ValMap.OfList (List.map (fun v -> (v, ())) vs) }
 
-/// Limit flags represent a type(s) returned from checking an expression(s) that is interesting to impose rules on.
-[<Flags>]
-type LimitFlags =
-    | None                          = 0b00000
-    | ByRef                         = 0b00001
-    | ByRefOfSpanLike               = 0b00011
-    | ByRefOfStackReferringSpanLike = 0b00101
-    | SpanLike                      = 0b01000
-    | StackReferringSpanLike        = 0b10000
-
-[<Struct>]
-type Limit =
-    {
-        scope: int
-        flags: LimitFlags
-    }
-
-    member this.IsLocal = this.scope >= 1
-
-/// Check if the limit has the target limit.
-let inline HasLimitFlag targetLimit (limit: Limit) =
-    limit.flags &&& targetLimit = targetLimit
-
-let NoLimit = { scope = 0; flags = LimitFlags.None }
-
-// Combining two limits will result in both limit flags merged.
-// If none of the limits are limited by a by-ref or a stack referring span-like
-//   the scope will be 0.
-let CombineTwoLimits limit1 limit2 = 
-    let isByRef1 = HasLimitFlag LimitFlags.ByRef limit1
-    let isByRef2 = HasLimitFlag LimitFlags.ByRef limit2
-    let isStackSpan1 = HasLimitFlag LimitFlags.StackReferringSpanLike limit1
-    let isStackSpan2 = HasLimitFlag LimitFlags.StackReferringSpanLike limit2
-    let isLimited1 = isByRef1 || isStackSpan1
-    let isLimited2 = isByRef2 || isStackSpan2
-
-    // A limit that has a stack referring span-like but not a by-ref, 
-    //   we force the scope to 1. This is to handle call sites
-    //   that return a by-ref and have stack referring span-likes as arguments.
-    //   This is to ensure we can only prevent out of scope at the method level rather than visibility.
-    let limit1 =
-        if isStackSpan1 && not isByRef1 then
-            { limit1 with scope = 1 }
-        else
-            limit1
+[<AutoOpen>]
+module Limit =
+
+    /// Limit flags represent a type(s) returned from checking an expression(s) that is interesting to impose rules on.
+    [<Flags>]
+    type LimitFlags =
+        | None                          = 0b00000
+        | ByRef                         = 0b00001
+        | ByRefOfSpanLike               = 0b00011
+        | ByRefOfStackReferringSpanLike = 0b00101
+        | SpanLike                      = 0b01000
+        | StackReferringSpanLike        = 0b10000
+
+    [<Struct>]
+    type Limit =
+        {
+            scope: int
+            flags: LimitFlags
+        }
+
+        member this.IsLocal = this.scope >= 1
+
+    /// Check if the limit has the target limit.
+    let inline HasLimitFlag targetLimit (limit: Limit) =
+        limit.flags &&& targetLimit = targetLimit
+
+    let NoLimit = { scope = 0; flags = LimitFlags.None }
+
+    // Combining two limits will result in both limit flags merged.
+    // If none of the limits are limited by a by-ref or a stack referring span-like
+    //   the scope will be 0.
+    let CombineTwoLimits limit1 limit2 =
+        let isByRef1 = HasLimitFlag LimitFlags.ByRef limit1
+        let isByRef2 = HasLimitFlag LimitFlags.ByRef limit2
+        let isStackSpan1 = HasLimitFlag LimitFlags.StackReferringSpanLike limit1
+        let isStackSpan2 = HasLimitFlag LimitFlags.StackReferringSpanLike limit2
+        let isLimited1 = isByRef1 || isStackSpan1
+        let isLimited2 = isByRef2 || isStackSpan2
+
+        // A limit that has a stack referring span-like but not a by-ref,
+        //   we force the scope to 1. This is to handle call sites
+        //   that return a by-ref and have stack referring span-likes as arguments.
+        //   This is to ensure we can only prevent out of scope at the method level rather than visibility.
+        let limit1 =
+            if isStackSpan1 && not isByRef1 then
+                { limit1 with scope = 1 }
+            else
+                limit1
 
-    let limit2 =
-        if isStackSpan2 && not isByRef2 then
-            { limit2 with scope = 1 }
-        else
-            limit2
-
-    match isLimited1, isLimited2 with
-    | false, false ->
-        { scope = 0; flags = limit1.flags ||| limit2.flags }
-    | true, true ->
-        { scope = Math.Max(limit1.scope, limit2.scope); flags = limit1.flags ||| limit2.flags }
-    | true, false ->
-        { limit1 with flags = limit1.flags ||| limit2.flags }
-    | false, true ->
-        { limit2 with flags = limit1.flags ||| limit2.flags }
-
-let CombineLimits limits =
-    (NoLimit, limits)
-    ||> List.fold CombineTwoLimits
+        let limit2 =
+            if isStackSpan2 && not isByRef2 then
+                { limit2 with scope = 1 }
+            else
+                limit2
+
+        match isLimited1, isLimited2 with
+        | false, false ->
+            { scope = 0; flags = limit1.flags ||| limit2.flags }
+        | true, true ->
+            { scope = Math.Max(limit1.scope, limit2.scope); flags = limit1.flags ||| limit2.flags }
+        | true, false ->
+            { limit1 with flags = limit1.flags ||| limit2.flags }
+        | false, true ->
+            { limit2 with flags = limit1.flags ||| limit2.flags }
+
+    let CombineLimits limits =
+        (NoLimit, limits)
+        ||> List.fold CombineTwoLimits
 
 type cenv = 
     { boundVals: Dictionary<Stamp, int> // really a hash set
diff --git a/src/Compiler/Checking/PostInferenceChecks.fsi b/src/Compiler/Checking/PostInferenceChecks.fsi
index 6e289af71c8..41e321ef4f4 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fsi
+++ b/src/Compiler/Checking/PostInferenceChecks.fsi
@@ -26,3 +26,19 @@ val CheckImplFile:
     (bool * bool) *
     isInternalTestSpanStackReferring: bool ->
         bool * StampMap<AnonRecdTypeInfo>
+
+module Limit =
+    [<System.Flags>]
+    type LimitFlags =
+        | None = 0b00000
+        | ByRef = 0b00001
+        | ByRefOfSpanLike = 0b00011
+        | ByRefOfStackReferringSpanLike = 0b00101
+        | SpanLike = 0b01000
+        | StackReferringSpanLike = 0b10000
+
+    [<Struct>]
+    type Limit = { scope: int; flags: LimitFlags }
+
+    val NoLimit: Limit
+    val CombineTwoLimits: Limit -> Limit -> Limit

From cc4f8e7e7ad906557aa4c025ac5af825c4777b39 Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Fri, 16 Jun 2023 20:02:18 +0100
Subject: [PATCH 03/10] Add docstrings

---
 src/Compiler/Checking/PostInferenceChecks.fs  |  3 +--
 src/Compiler/Checking/PostInferenceChecks.fsi | 25 ++++++++++++++++++-
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/Compiler/Checking/PostInferenceChecks.fs b/src/Compiler/Checking/PostInferenceChecks.fs
index b95c276ca61..8a25053d967 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fs
+++ b/src/Compiler/Checking/PostInferenceChecks.fs
@@ -127,7 +127,6 @@ let BindArgVals env (vs: Val list) =
 [<AutoOpen>]
 module Limit =
 
-    /// Limit flags represent a type(s) returned from checking an expression(s) that is interesting to impose rules on.
     [<Flags>]
     type LimitFlags =
         | None                          = 0b00000
@@ -1768,7 +1767,7 @@ and CheckLambdas isTop (memberVal: Val option) cenv env inlined valReprInfo alwa
         let freesOpt = CheckEscapes cenv memInfo.IsSome m syntacticArgs body
 
         //  no reraise under lambda expression
-        CheckNoReraise cenv freesOpt body 
+        CheckNoReraise cenv freesOpt body
 
         // Check the body of the lambda
         if isTop && not g.compilingFSharpCore && isByrefLikeTy g m bodyTy then
diff --git a/src/Compiler/Checking/PostInferenceChecks.fsi b/src/Compiler/Checking/PostInferenceChecks.fsi
index 41e321ef4f4..f02fcaa1cee 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fsi
+++ b/src/Compiler/Checking/PostInferenceChecks.fsi
@@ -27,6 +27,8 @@ val CheckImplFile:
     isInternalTestSpanStackReferring: bool ->
         bool * StampMap<AnonRecdTypeInfo>
 
+/// It's unlikely you want to use this module except within
+/// PostInferenceChecks. It's exposed to allow testing.
 module Limit =
     [<System.Flags>]
     type LimitFlags =
@@ -37,8 +39,29 @@ module Limit =
         | SpanLike = 0b01000
         | StackReferringSpanLike = 0b10000
 
+    /// A "limit" here is some combination of restrictions on a Val.
     [<Struct>]
-    type Limit = { scope: int; flags: LimitFlags }
+    type Limit =
+        {
+            /// The scope of this Limit, i.e. "to which scope can a Val safely escape?".
+            /// Some values are not allowed to escape their scope.
+            /// For example, a top-level function is allowed to return a byref type, but inner functions are not.
+            /// This `scope` field is the information that lets us track that.
+            /// (Recall that in general scopes are counted starting from 0 indicating the top-level scope, and
+            /// increasing by 1 essentially for every nested `let`-binding, method, or module.)
+            ///
+            /// Some specific values which are often used:
+            /// * the value 0 is used in NoLimit, since it indicates "this Val can safely escape to all scopes";
+            /// * the value 1 is a "top-level local scope", allowing us to express the restriction "this cannot appear
+            ///   at the top level" (for example, `let x = &y` cannot appear at the top level).
+            scope: int
+            /// The combinations of limits which apply.
+            flags: LimitFlags
+        }
 
+    /// Indicates that no limit applies to some Val. It can appear at the top level or within a `let`-binding,
+    /// and the Val does not have any byref- or span-related restrictions.
     val NoLimit: Limit
+
+    /// Construct a Limit which expresses "this Val must obey the first Limit and the second Limit simultaneously".
     val CombineTwoLimits: Limit -> Limit -> Limit

From ee574f5f3071f014ab5f290d9379a25d38fab86d Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Sat, 17 Jun 2023 14:18:40 +0100
Subject: [PATCH 04/10] Add tests of the properties I claimed in the PR

---
 src/Compiler/Checking/PostInferenceChecks.fsi |  2 +-
 .../FSharp.Compiler.UnitTests.fsproj          |  1 +
 .../PostInferenceChecksTests.fs               | 84 +++++++++++++++++++
 3 files changed, 86 insertions(+), 1 deletion(-)
 create mode 100644 tests/FSharp.Compiler.UnitTests/PostInferenceChecksTests.fs

diff --git a/src/Compiler/Checking/PostInferenceChecks.fsi b/src/Compiler/Checking/PostInferenceChecks.fsi
index f02fcaa1cee..eabfeba77db 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fsi
+++ b/src/Compiler/Checking/PostInferenceChecks.fsi
@@ -51,7 +51,7 @@ module Limit =
             /// increasing by 1 essentially for every nested `let`-binding, method, or module.)
             ///
             /// Some specific values which are often used:
-            /// * the value 0 is used in NoLimit, since it indicates "this Val can safely escape to all scopes";
+            /// * the value 0 is used in NoLimit and other situations which don't limit where the Val can escape;
             /// * the value 1 is a "top-level local scope", allowing us to express the restriction "this cannot appear
             ///   at the top level" (for example, `let x = &y` cannot appear at the top level).
             scope: int
diff --git a/tests/FSharp.Compiler.UnitTests/FSharp.Compiler.UnitTests.fsproj b/tests/FSharp.Compiler.UnitTests/FSharp.Compiler.UnitTests.fsproj
index a1b239c1141..828f5b08c75 100644
--- a/tests/FSharp.Compiler.UnitTests/FSharp.Compiler.UnitTests.fsproj
+++ b/tests/FSharp.Compiler.UnitTests/FSharp.Compiler.UnitTests.fsproj
@@ -27,6 +27,7 @@
     <Compile Include="BuildGraphTests.fs" />
     <Compile Include="FsiTests.fs" />
     <Compile Include="AssemblySigningAttributes.fs" />
+    <Compile Include="PostInferenceChecksTests.fs" />
     <Compile Include="..\..\tests\service\FsUnit.fs">
       <Link>CompilerService\FsUnit.fs</Link>
     </Compile>
diff --git a/tests/FSharp.Compiler.UnitTests/PostInferenceChecksTests.fs b/tests/FSharp.Compiler.UnitTests/PostInferenceChecksTests.fs
new file mode 100644
index 00000000000..3c4fcddf8ba
--- /dev/null
+++ b/tests/FSharp.Compiler.UnitTests/PostInferenceChecksTests.fs
@@ -0,0 +1,84 @@
+namespace FSharp.Compiler.ComponentTests.Checking
+
+open System
+open Xunit
+open FSharp.Compiler.PostTypeCheckSemanticChecks.Limit
+
+module PostInferenceChecksTests =
+
+    [<Literal>]
+    let internal NUM_TESTS = 10_000
+
+    let genNat (rng : Random) : int =
+        let i = rng.Next ()
+        if i = Int32.MinValue then
+            0
+        else
+            abs i
+
+    let internal possibleLimitFlags = LimitFlags.GetValues<LimitFlags> ()
+
+    let internal genLimitFlags (rng : Random) : LimitFlags =
+        Seq.init (genNat rng % 10 + 1) (fun _ -> possibleLimitFlags[genNat rng % possibleLimitFlags.Length])
+        |> Seq.reduce (|||)
+
+    let internal generateLimit (rng : Random) : Limit =
+        { scope = genNat rng
+          flags = genLimitFlags rng }
+
+    let createSeed () =
+        DateTime.UtcNow.Ticks % int64 Int32.MaxValue
+        |> int
+
+    [<Fact>]
+    let ``NoLimit is almost a zero for CombineTwoLimits`` () =
+        let seed = createSeed ()
+        let rng = Random seed
+
+        for count in 0..NUM_TESTS - 1 do
+            try
+                let original = generateLimit rng
+                let after = CombineTwoLimits original NoLimit
+                Assert.StrictEqual (after.flags, original.flags)
+                if original.scope <> after.scope then
+                    // See docs on the `scope` field for the conditions under which
+                    // these special values are used.
+                    Assert.InRange (after.scope, 0, 1)
+            with
+            | exc ->
+                let exc = AggregateException ($"Failed with seed %i{seed}, count %i{count}", exc)
+                raise exc
+
+    [<Fact>]
+    let ``CombineTwoLimits is commutative`` () =
+        let seed = createSeed ()
+        let rng = Random seed
+
+        for count in 0..NUM_TESTS - 1 do
+            try
+                let x = generateLimit rng
+                let y = generateLimit rng
+                Assert.StrictEqual (CombineTwoLimits x y, CombineTwoLimits y x)
+            with
+            | exc ->
+                let exc = AggregateException ($"Failed with seed %i{seed}, count %i{count}", exc)
+                raise exc
+
+    [<Fact>]
+    let ``CombineTwoLimits is associative`` () =
+        let seed = createSeed ()
+        let rng = Random seed
+
+        for count in 0..NUM_TESTS - 1 do
+            try
+                let x = generateLimit rng
+                let y = generateLimit rng
+                let z = generateLimit rng
+
+                let lhs = CombineTwoLimits (CombineTwoLimits x y) z
+                let rhs = CombineTwoLimits x (CombineTwoLimits y z)
+                Assert.StrictEqual (lhs, rhs)
+            with
+            | exc ->
+                let exc = AggregateException ($"Failed with seed %i{seed}, %i{count}", exc)
+                raise exc

From 028cfa8ac6c4730c0ef63c578b0c52a5fc960bb7 Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Tue, 4 Jul 2023 22:56:42 +0100
Subject: [PATCH 05/10] Fix base case

---
 src/Compiler/Checking/PostInferenceChecks.fs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Compiler/Checking/PostInferenceChecks.fs b/src/Compiler/Checking/PostInferenceChecks.fs
index 8a25053d967..25c8fa7c15a 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fs
+++ b/src/Compiler/Checking/PostInferenceChecks.fs
@@ -1003,7 +1003,7 @@ and CheckExprLinear (cenv: cenv) (env: env) expr (ctxt: PermitByRefExpr) (acc :
         CheckTypeInstNoByrefs cenv env m tyargs
         argsHead |> List.iter (CheckExprNoByrefs cenv env) 
         // tailcall
-        CheckExprLinear cenv env argLast PermitByRefExpr.No NoLimit
+        CheckExprLinear cenv env argLast PermitByRefExpr.No acc
 
     | LinearMatchExpr (_spMatch, _exprm, dtree, tg1, e2, m, ty) ->
         CheckTypeNoInnerByrefs cenv env m ty 

From 0fa4cfd4d6bd9035d9016fa74bab6fda09a16779 Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Tue, 4 Jul 2023 23:24:22 +0100
Subject: [PATCH 06/10] Apparently I'm breaking the law

---
 tests/FSharp.Compiler.UnitTests/PostInferenceChecksTests.fs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/tests/FSharp.Compiler.UnitTests/PostInferenceChecksTests.fs b/tests/FSharp.Compiler.UnitTests/PostInferenceChecksTests.fs
index 3c4fcddf8ba..01d6bb5a3f6 100644
--- a/tests/FSharp.Compiler.UnitTests/PostInferenceChecksTests.fs
+++ b/tests/FSharp.Compiler.UnitTests/PostInferenceChecksTests.fs
@@ -16,7 +16,10 @@ module PostInferenceChecksTests =
         else
             abs i
 
-    let internal possibleLimitFlags = LimitFlags.GetValues<LimitFlags> ()
+    let internal possibleLimitFlags =
+        Enum.GetValues typeof<LimitFlags>
+        |> Seq.cast<LimitFlags>
+        |> Array.ofSeq
 
     let internal genLimitFlags (rng : Random) : LimitFlags =
         Seq.init (genNat rng % 10 + 1) (fun _ -> possibleLimitFlags[genNat rng % possibleLimitFlags.Length])

From fb282c9243b095bda88efb26b4e47caf888c2570 Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Mon, 21 Aug 2023 21:28:38 +0100
Subject: [PATCH 07/10] Restore comment that got lost

---
 src/Compiler/Checking/PostInferenceChecks.fsi | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Compiler/Checking/PostInferenceChecks.fsi b/src/Compiler/Checking/PostInferenceChecks.fsi
index eabfeba77db..5ed4bb61fe8 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fsi
+++ b/src/Compiler/Checking/PostInferenceChecks.fsi
@@ -64,4 +64,5 @@ module Limit =
     val NoLimit: Limit
 
     /// Construct a Limit which expresses "this Val must obey the first Limit and the second Limit simultaneously".
+    //// If none of the limits are limited by a by-ref or a stack referring span-like, the scope will be 0.
     val CombineTwoLimits: Limit -> Limit -> Limit

From e37836fd3acc4ac06b3f891f52865642192b4061 Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Mon, 21 Aug 2023 21:57:43 +0100
Subject: [PATCH 08/10] Get rid of one call

---
 src/Compiler/Checking/PostInferenceChecks.fs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Compiler/Checking/PostInferenceChecks.fs b/src/Compiler/Checking/PostInferenceChecks.fs
index 1722e766c87..173cc3f9d25 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fs
+++ b/src/Compiler/Checking/PostInferenceChecks.fs
@@ -1012,9 +1012,7 @@ and CheckExprLinear (cenv: cenv) (env: env) expr (ctxt: PermitByRefExpr) (acc :
     | Expr.DebugPoint (_, innerExpr) ->
         CheckExprLinear cenv env innerExpr ctxt acc
 
-    | _ ->
-        // not a linear expression
-        CheckExpr cenv env expr ctxt
+    | _ -> failwith "unreachable: it was the caller's responsibility to ensure we were in one of the above cases"
 
 /// Check a resumable code expression (the body of a ResumableCode delegate or
 /// the body of the MoveNextMethod for a state machine)

From 7d3fc81b50adbd072dc9b715201f348880094201 Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Mon, 21 Aug 2023 22:04:09 +0100
Subject: [PATCH 09/10] Revert "Get rid of one call"

This reverts commit e37836fd3acc4ac06b3f891f52865642192b4061.
---
 src/Compiler/Checking/PostInferenceChecks.fs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Compiler/Checking/PostInferenceChecks.fs b/src/Compiler/Checking/PostInferenceChecks.fs
index 173cc3f9d25..1722e766c87 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fs
+++ b/src/Compiler/Checking/PostInferenceChecks.fs
@@ -1012,7 +1012,9 @@ and CheckExprLinear (cenv: cenv) (env: env) expr (ctxt: PermitByRefExpr) (acc :
     | Expr.DebugPoint (_, innerExpr) ->
         CheckExprLinear cenv env innerExpr ctxt acc
 
-    | _ -> failwith "unreachable: it was the caller's responsibility to ensure we were in one of the above cases"
+    | _ ->
+        // not a linear expression
+        CheckExpr cenv env expr ctxt
 
 /// Check a resumable code expression (the body of a ResumableCode delegate or
 /// the body of the MoveNextMethod for a state machine)

From 5115d924418eb0a6c84fe949c835c0cf1dc8f0c9 Mon Sep 17 00:00:00 2001
From: Smaug123 <patrick+github@patrickstevens.co.uk>
Date: Mon, 21 Aug 2023 22:30:37 +0100
Subject: [PATCH 10/10] Revert change

---
 src/Compiler/Checking/PostInferenceChecks.fs | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/Compiler/Checking/PostInferenceChecks.fs b/src/Compiler/Checking/PostInferenceChecks.fs
index 1722e766c87..67128182ace 100644
--- a/src/Compiler/Checking/PostInferenceChecks.fs
+++ b/src/Compiler/Checking/PostInferenceChecks.fs
@@ -974,12 +974,12 @@ and CheckCallWithReceiver cenv env m returnTy args ctxts ctxt =
                 limitArgs
         CheckCallLimitArgs cenv env m returnTy limitArgs ctxt
 
-and CheckExprLinear (cenv: cenv) (env: env) expr (ctxt: PermitByRefExpr) (acc : Limit) : Limit =
+and CheckExprLinear (cenv: cenv) (env: env) expr (ctxt: PermitByRefExpr) (contf : Limit -> Limit) : Limit =
     match expr with
     | Expr.Sequential (e1, e2, NormalSeq, _) ->
         CheckExprNoByrefs cenv env e1
         // tailcall
-        CheckExprLinear cenv env e2 ctxt acc
+        CheckExprLinear cenv env e2 ctxt contf
 
     | Expr.Let (TBind(v, _bindRhs, _) as bind, body, _, _) ->
         let isByRef = isByrefTy cenv.g v.Type
@@ -994,27 +994,28 @@ and CheckExprLinear (cenv: cenv) (env: env) expr (ctxt: PermitByRefExpr) (acc :
         BindVal cenv env v
         LimitVal cenv v { limit with scope = if isByRef then limit.scope else env.returnScope }
         // tailcall
-        CheckExprLinear cenv env body ctxt acc
+        CheckExprLinear cenv env body ctxt contf
 
     | LinearOpExpr (_op, tyargs, argsHead, argLast, m) ->
         CheckTypeInstNoByrefs cenv env m tyargs
         argsHead |> List.iter (CheckExprNoByrefs cenv env)
         // tailcall
-        CheckExprLinear cenv env argLast PermitByRefExpr.No acc
+        CheckExprLinear cenv env argLast PermitByRefExpr.No (fun _ -> contf NoLimit)
 
     | LinearMatchExpr (_spMatch, _exprm, dtree, tg1, e2, m, ty) ->
         CheckTypeNoInnerByrefs cenv env m ty
         CheckDecisionTree cenv env dtree
         let lim1 = CheckDecisionTreeTarget cenv env ctxt tg1
         // tailcall
-        CheckExprLinear cenv env e2 ctxt (CombineTwoLimits lim1 acc)
+        CheckExprLinear cenv env e2 ctxt (fun lim2 -> contf (CombineTwoLimits lim1 lim2))
 
     | Expr.DebugPoint (_, innerExpr) ->
-        CheckExprLinear cenv env innerExpr ctxt acc
+        CheckExprLinear cenv env innerExpr ctxt contf
 
     | _ ->
         // not a linear expression
         CheckExpr cenv env expr ctxt
+        |> contf
 
 /// Check a resumable code expression (the body of a ResumableCode delegate or
 /// the body of the MoveNextMethod for a state machine)
@@ -1142,7 +1143,7 @@ and CheckExpr (cenv: cenv) (env: env) origExpr (ctxt: PermitByRefExpr) : Limit =
     | Expr.Let _
     | Expr.Sequential (_, _, NormalSeq, _)
     | Expr.DebugPoint _ ->
-        CheckExprLinear cenv env expr ctxt NoLimit
+        CheckExprLinear cenv env expr ctxt id
 
     | Expr.Sequential (e1, e2, ThenDoSeq, _) ->
         CheckExprNoByrefs cenv env e1
