add borrowing test

src/main/scala/qualfsub/TypeCheck.scala

@@ -393,7 +393,7 @@ def checkSubtypeOverlap(T: QType, S: QType)(using Γ: TEnv): Unit =
   val QType(t2, q2) = S
   if (t1.isSubtype(t2)) {
     val sq1 = q1.sat
-    val sq2 = q2.sat
+    val sq2 = q2.sat // FIXME: should not compute saturated sat here
     if (sq1.isSubqual(sq2)) ()
     else throw NonOverlap(sq2 - Fresh(), sq1 \ sq2)
   } else throw NotSubtype(t1, t2)()

src/test/scala/diamond/Diamond.scala

@@ -406,4 +406,28 @@ class DiamondTest extends AnyFunSuite {
       (TForall("𝐹#2","A","a",TTop^ ◆,
         TFun("𝑓#3","x",TVar("A")^"a",TVar("A")^"x")^"a")^()))
   }
+
+  test("borrowing") {
+    val p1 = """
+      def borrow[A^a <: Top^<>, B^b <: Top^<>](x: A^a, block: ((A^a) => B^b)^<>) = { block(x) };
+      val x = Ref 42;
+      borrow[Ref[Int]^x, Int](x, (y: Ref[Int]^x) => { !y }) // allowed
+    """
+    assert(parseAndCheck(p1) == (TNum^()))
+
+    val p2 = """
+      def borrow[A^a <: Top^<>, B^b <: Top^<>](x: A^a, block: ((A^a) => B^b)^<>) = { block(x) };
+      val x = Ref 42;
+      borrow[Ref[Int]^x, Int](x, (y: Ref[Int]^x) => { !x }) // not allowed
+    """
+    intercept[NonOverlap] { parseAndCheck(p2) }
+
+    val p3 = """
+      def borrow[A^a <: Top^<>, B^b <: Top^<>](x: A^a, block: ((A^a) => B^b)^<>) = { block(x) };
+      val x = Ref 42;
+      val z = x;
+      borrow[Ref[Int]^x, Int](x, (y: Ref[Int]^x) => { !z }) // not allowed
+    """
+    intercept[NonOverlap] { parseAndCheck(p3) }
+  }
 }