feat: Update linearity checker to use new diagnostics

examples/demo.ipynb

@@ -306,13 +306,18 @@
      "name": "stderr",
      "output_type": "stream",
      "text": [
-      "Guppy compilation failed. Error in file <In [9]>:6\n",
+      "Error: Linearity violation (at <In [9]>:6:10)\n",
+      "  | \n",
+      "4 | @guppy(bad_module)\n",
+      "5 | def bad(q: qubit @owned) -> qubit:\n",
+      "6 |     cx(q, q)\n",
+      "  |           ^ Variable `q` with linear type `qubit` cannot be borrowed\n",
+      "  |             ...\n",
+      "  | \n",
+      "6 |     cx(q, q)\n",
+      "  |        - since it was already borrowed here\n",
       "\n",
-      "4:    @guppy(bad_module)\n",
-      "5:    def bad(q: qubit @owned) -> qubit:\n",
-      "6:        cx(q, q)\n",
-      "                ^\n",
-      "GuppyError: Variable `q` with linear type `qubit` was already used (at 6:7)\n"
+      "Guppy compilation failed due to 1 previous error\n"
      ]
     }
    ],
@@ -350,13 +355,16 @@
      "name": "stderr",
      "output_type": "stream",
      "text": [
-      "Guppy compilation failed. Error in file <In [10]>:7\n",
+      "Error: Linearity violation (at <In [10]>:7:7)\n",
+      "  | \n",
+      "5 | def bad(q: qubit @owned) -> qubit:\n",
+      "6 |     tmp = qubit()\n",
+      "7 |     cx(tmp, q)\n",
+      "  |        ^^^ Variable `tmp` with linear type `qubit` is leaked\n",
+      "\n",
+      "Help: Make sure that `tmp` is consumed or returned to avoid the leak\n",
       "\n",
-      "5:    def bad(q: qubit @owned) -> qubit:\n",
-      "6:        tmp = qubit()\n",
-      "7:        cx(tmp, q)\n",
-      "             ^^^\n",
-      "GuppyError: Variable `tmp` with linear type `qubit` is not used on all control-flow paths\n"
+      "Guppy compilation failed due to 1 previous error\n"
      ]
     }
    ],

guppylang/checker/cfg_checker.py

@@ -60,7 +60,7 @@ def __init__(self, input_tys: list[Type], output_ty: Type) -> None:
 
 
 def check_cfg(
-    cfg: CFG, inputs: Row[Variable], return_ty: Type, globals: Globals
+    cfg: CFG, inputs: Row[Variable], return_ty: Type, func_name: str, globals: Globals
 ) -> CheckedCFG[Place]:
     """Type checks a control-flow graph.
 
@@ -126,7 +126,7 @@ def check_cfg(
     # Finally, run the linearity check
     from guppylang.checker.linearity_checker import check_cfg_linearity
 
-    linearity_checked_cfg = check_cfg_linearity(checked_cfg, globals)
+    linearity_checked_cfg = check_cfg_linearity(checked_cfg, func_name, globals)
 
     return linearity_checked_cfg
 

guppylang/checker/core.py

@@ -85,6 +85,11 @@ def id(self) -> "Variable.Id":
         """The unique `PlaceId` identifier for this place."""
         return Variable.Id(self.name)
 
+    @cached_property
+    def root(self) -> "Variable":
+        """The root variable of this place."""
+        return self
+
     @property
     def describe(self) -> str:
         """A human-readable description of this place for error messages."""
@@ -123,6 +128,11 @@ def id(self) -> "FieldAccess.Id":
         """The unique `PlaceId` identifier for this place."""
         return FieldAccess.Id(self.parent.id, self.field.name)
 
+    @cached_property
+    def root(self) -> "Variable":
+        """The root variable of this place."""
+        return self.parent.root
+
     @property
     def ty(self) -> Type:
         """The type of this place."""
@@ -182,6 +192,11 @@ def defined_at(self) -> AstNode | None:
         """Optional location where this place was last assigned to."""
         return self.parent.defined_at
 
+    @cached_property
+    def root(self) -> "Variable":
+        """The root variable of this place."""
+        return self.parent.root
+
     @property
     def describe(self) -> str:
         """A human-readable description of this place for error messages."""

guppylang/checker/errors/linearity.py

@@ -0,0 +1,259 @@
+"""Collection of error messages emitted during linearity checking."""
+
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import TYPE_CHECKING, ClassVar
+
+from guppylang.diagnostic import Error, Help, Note
+
+if TYPE_CHECKING:
+    from guppylang.checker.core import (
+        Place,
+        Variable,
+    )
+    from guppylang.checker.linearity_checker import UseKind
+    from guppylang.definition.struct import StructField
+    from guppylang.tys.ty import (
+        StructType,
+        Type,
+    )
+
+
+@dataclass(frozen=True)
+class AlreadyUsedError(Error):
+    title: ClassVar[str] = "Linearity violation"
+    span_label: ClassVar[str] = (
+        "{place.describe} with linear type `{place.ty}` cannot be {kind.subjunctive} "
+        "..."
+    )
+    place: Place
+    kind: UseKind
+
+    @dataclass(frozen=True)
+    class PrevUse(Note):
+        span_label: ClassVar[str] = "since it was already {prev_kind.subjunctive} here"
+        prev_kind: UseKind
+
+
+@dataclass(frozen=True)
+class ComprAlreadyUsedError(Error):
+    title: ClassVar[str] = "Linearity violation"
+    span_label: ClassVar[str] = (
+        "{place.describe} with linear type `{place.ty}` would be {kind.subjunctive} "
+        "multiple times when evaluating this comprehension"
+    )
+    place: Place
+    kind: UseKind
+
+    @dataclass(frozen=True)
+    class PrevUse(Note):
+        span_label: ClassVar[str] = "since it was already {prev_kind.subjunctive} here"
+        prev_kind: UseKind
+
+
+@dataclass(frozen=True)
+class PlaceNotUsedError(Error):
+    title: ClassVar[str] = "Linearity violation"
+    place: Place
+
+    @property
+    def rendered_span_label(self) -> str:
+        s = f"{self.place.describe} with linear type `{self.place.ty}` "
+        match self.children:
+            case [PlaceNotUsedError.Branch(), *_]:
+                return s + "may be leaked ..."
+            case _:
+                return s + "is leaked"
+
+    @dataclass(frozen=True)
+    class Branch(Note):
+        span_label: ClassVar[str] = "if this expression is `{truth_value}`"
+        truth_value: bool
+
+    @dataclass(frozen=True)
+    class Fix(Help):
+        message: ClassVar[str] = (
+            "Make sure that `{place}` is consumed or returned to avoid the leak"
+        )
+
+
+@dataclass(frozen=True)
+class UnnamedExprNotUsedError(Error):
+    title: ClassVar[str] = "Linearity violation"
+    span_label: ClassVar[str] = "Expression with linear type `{ty}` is leaked"
+    ty: Type
+
+    @dataclass(frozen=True)
+    class Fix(Help):
+        message: ClassVar[str] = "Consider assigning this value to a local variable"
+
+
+@dataclass(frozen=True)
+class UnnamedFieldNotUsedError(Error):
+    title: ClassVar[str] = "Linearity violation"
+    span_label: ClassVar[str] = (
+        "Linear field `{field.name}` of expression with type `{struct_ty}` is leaked"
+    )
+    field: StructField
+    struct_ty: StructType
+
+    @dataclass(frozen=True)
+    class Fix(Help):
+        message: ClassVar[str] = (
+            "Consider assigning this value to a local variable before accessing the "
+            "field `{used_field.name}`"
+        )
+        used_field: StructField
+
+
+@dataclass(frozen=True)
+class UnnamedSubscriptNotUsedError(Error):
+    title: ClassVar[str] = "Linearity violation"
+    span_label: ClassVar[str] = (
+        "Linear items of expression with type `{container_ty}` are leaked ..."
+    )
+    container_ty: Type
+
+    @dataclass(frozen=True)
+    class SubscriptHint(Note):
+        span_label: ClassVar[str] = "since only this subscript is used"
+
+    @dataclass(frozen=True)
+    class Fix(Help):
+        message: ClassVar[str] = (
+            "Consider assigning this value to a local variable before subscripting it"
+        )
+
+
+@dataclass(frozen=True)
+class NotOwnedError(Error):
+    title: ClassVar[str] = "Not owned"
+    place: Place
+    kind: UseKind
+    is_call_arg: bool
+    func_name: str | None
+    calling_func_name: str
+
+    @property
+    def rendered_span_label(self) -> str:
+        if self.is_call_arg:
+            f = f"Function `{self.func_name}`" if self.func_name else "Function"
+            return (
+                f"{f} wants to take ownership of this argument, but "
+                f"`{self.calling_func_name}` doesn't own `{self.place}`"
+            )
+        return (
+            f"Cannot {self.kind.indicative} `{self.place}` since "
+            f"`{self.calling_func_name}` doesn't own it"
+        )
+
+    @dataclass(frozen=True)
+    class MakeOwned(Help):
+        span_label: ClassVar[str] = (
+            "Argument `{place.root.name}` is only borrowed. Consider taking ownership: "
+            "`{place.root.name}: {place.root.ty} @owned`"
+        )
+
+
+@dataclass(frozen=True)
+class MoveOutOfSubscriptError(Error):
+    title: ClassVar[str] = "Subscript {kind.subjunctive}"
+    span_label: ClassVar[str] = (
+        "Cannot {kind.indicative} a subscript of `{parent}` with linear type "
+        "`{parent.ty}`"
+    )
+    kind: UseKind
+    parent: Place
+
+    @dataclass(frozen=True)
+    class Explanation(Note):
+        message: ClassVar[str] = (
+            "Subscripts on linear types are only allowed to be borrowed, not "
+            "{kind.subjunctive}"
+        )
+
+
+@dataclass(frozen=True)
+class BorrowShadowedError(Error):
+    title: ClassVar[str] = "Borrow shadowed"
+    span_label: ClassVar[str] = "Assignment shadows borrowed argument `{place}`"
+    place: Place
+
+    @dataclass(frozen=True)
+    class Rename(Help):
+        message: ClassVar[str] = "Consider assigning to a different name"
+
+
+@dataclass(frozen=True)
+class BorrowSubPlaceUsedError(Error):
+    title: ClassVar[str] = "Linearity violation"
+    span_label: ClassVar[str] = (
+        "Borrowed argument {borrowed_var} cannot be returned to the caller ..."
+    )
+    borrowed_var: Variable
+    sub_place: Place
+
+    @dataclass(frozen=True)
+    class PrevUse(Note):
+        span_label: ClassVar[str] = (
+            "since `{sub_place}` with linear type `{sub_place.ty}` was already "
+            "{kind.subjunctive} here"
+        )
+        kind: UseKind
+
+    @dataclass(frozen=True)
+    class Fix(Help):
+        message: ClassVar[str] = (
+            "Consider writing a value back into `{sub_place}` before returning"
+        )
+
+
+@dataclass(frozen=True)
+class DropAfterCallError(Error):
+    title: ClassVar[str] = "Linearity violation"
+    span_label: ClassVar[str] = (
+        "Value with linear type `{ty}` would be leaked after {func} returns"
+    )
+    ty: Type
+    func_name: str | None
+
+    @property
+    def func(self) -> str:
+        return f"`{self.func_name}`" if self.func_name else "the function"
+
+    @dataclass(frozen=True)
+    class Assign(Help):
+        message: ClassVar[str] = (
+            "Consider assigning the value to a local variable before passing it to "
+            "{func}"
+        )
+
+
+@dataclass(frozen=True)
+class LinearCaptureError(Error):
+    title: ClassVar[str] = "Linearity violation"
+    span_label: ClassVar[str] = (
+        "{var.describe} with linear type {var.ty} cannot be used here since `{var}` is "
+        "captured from an outer scope"
+    )
+    var: Variable
+
+    @dataclass(frozen=True)
+    class DefinedHere(Note):
+        span_label: ClassVar[str] = "`{var}` defined here"
+
+
+@dataclass(frozen=True)
+class LinearPartialApplyError(Error):
+    title: ClassVar[str] = "Linearity violation"
+    span_label: ClassVar[str] = (
+        "This expression implicitly constructs a closure that captures a linear value"
+    )
+
+    @dataclass(frozen=True)
+    class Captured(Note):
+        span_label: ClassVar[str] = (
+            "This expression with linear type `{ty}` is implicitly captured"
+        )
+        ty: Type

guppylang/checker/expr_checker.py

@@ -586,7 +586,10 @@ def visit_Subscript(self, node: ast.Subscript) -> tuple[ast.expr, Type]:
             # other indices after this one has been projected out (e.g. `f()[0]` makes
             # you loose access to all elements besides 0).
             expr = SubscriptAccessAndDrop(
-                item=item, item_expr=item_expr, getitem_expr=getitem_expr
+                item=item,
+                item_expr=item_expr,
+                getitem_expr=getitem_expr,
+                original_expr=node,
             )
         return with_loc(node, expr), result_ty
 

guppylang/checker/func_checker.py

@@ -36,7 +36,7 @@ def check_global_func_def(
         Variable(x, inp.ty, loc, inp.flags)
         for x, inp, loc in zip(ty.input_names, ty.inputs, args, strict=True)
     ]
-    return check_cfg(cfg, inputs, ty.output, globals)
+    return check_cfg(cfg, inputs, ty.output, func_def.name, globals)
 
 
 def check_nested_func_def(
@@ -102,7 +102,7 @@ def check_nested_func_def(
             # Otherwise, we treat it like a local name
             inputs.append(Variable(func_def.name, func_def.ty, func_def))
 
-    checked_cfg = check_cfg(cfg, inputs, func_ty.output, globals)
+    checked_cfg = check_cfg(cfg, inputs, func_ty.output, func_def.name, globals)
     checked_def = CheckedNestedFunctionDef(
         def_id,
         checked_cfg,