diff --git a/asllib/aslspec/AST.ml b/asllib/aslspec/AST.ml
index f8776c4279..aafceb035c 100644
--- a/asllib/aslspec/AST.ml
+++ b/asllib/aslspec/AST.ml
@@ -2,13 +2,20 @@
     domain-specific language that defines the semantics-specification for ASL.
 *)
 
-exception SpecError of string
+type position = Lexing.position
+type source_location = { start_pos : position; end_pos : position }
+
+exception SpecError of { loc : source_location; msg : string }
+
+let missing_location =
+  let dummy_pos = Lexing.dummy_pos in
+  { start_pos = dummy_pos; end_pos = dummy_pos }
 
 (** Extends an error message and re-raises an exception. This is a temporary
     hack until the AST supports source locations. *)
-let stack_spec_error msg extra_msg =
+let stack_spec_error loc msg extra_msg =
   let full_msg = Printf.sprintf "%s\n%s" msg extra_msg in
-  raise (SpecError full_msg)
+  raise (SpecError { loc; msg = full_msg })
 
 (** Specifies a visual layout for a compound term. *)
 type layout =
@@ -101,17 +108,10 @@ module Attributes = struct
   include Map.Make (AttributeKey)
 
   type 'a map = 'a t
-  (** Shadows [Map.t] with a string-to-string map type. *)
+  (** Shadows [Map.t] with a dedicated map type. *)
 
   type nonrec t = attribute t
 
-  let check_definition_name name =
-    let () = assert (String.length name > 0) in
-    let id_regexp = Str.regexp "^[A-Za-z_']+$" in
-    if not (Str.string_match id_regexp name 0) then
-      let msg = Format.sprintf "illegal element-defining identifier: %s" name in
-      raise (SpecError msg)
-
   (** Shadows [of_list] by raising a [SpecError] exception on pairs containing
       the same key. *)
   let of_list pairs =
@@ -121,7 +121,7 @@ module Attributes = struct
           let msg =
             Format.sprintf "Duplicate attribute: '%s'" (AttributeKey.to_str k)
           in
-          raise (SpecError msg)
+          raise (SpecError { loc = missing_location; msg })
         else add k v acc_map)
       empty pairs
 
@@ -136,8 +136,8 @@ module Attributes = struct
     | Some _ -> assert false
     | _ -> None
 
-  (** [get_string key attrs] returns the string value for [key] in [attrs], or
-      [""] if not found. *)
+  (** [get_string_or_empty key attrs] returns the string value for [key] in
+      [attrs], or [""] if not found. *)
   let get_string_or_empty key attrs =
     match find_opt key attrs with
     | Some (StringAttribute s) -> s
@@ -200,31 +200,44 @@ module Term = struct
     | Option, Option -> true
     | _ -> false
 
-  (** Terms for constructing types out of other types, with [Label t] being the
+  (** Terms for constructing types out of other types, with [Label] being the
       leaf case.
 
-      In the context of a type definition, a [Label] variant defines a new label
-      \- a type representing just this single label. In other contexts, for
-      example a type variant appearing in the signature of a relation, this can
-      refer to a type defined elsewhere. *)
+      In the context of a type definition, a [Label] variant defines a new
+      label. That is, a type representing just this single label. In other
+      contexts, for example a type variant appearing in the signature of a
+      relation, this can refer to a type defined elsewhere. *)
   type t =
-    | Label of string
+    | Label of { loc : source_location; label : string }
         (** Either a set containing the single value named by the given string
             or a reference to a type with the given name. *)
-    | TypeOperator of { op : type_operator; term : opt_named_type_term }
+    | TypeOperator of {
+        loc : source_location;
+        op : type_operator;
+        term : opt_named_type_term;
+      }
         (** A set containing all types formed by applying the type operator [op]
             to the type given by [term]. *)
-    | Tuple of { label_opt : string option; args : opt_named_type_term list }
+    | Tuple of {
+        loc : source_location;
+        label_opt : string option;
+        args : opt_named_type_term list;
+      }
         (** A set containing all optionally-labelled tuples formed by the given
-            argunent terms. An unlabelled tuple containing a single term is a
+            argument terms. An unlabelled tuple containing a single term is a
             special case - its domain is the domain of that term; this serves to
             reference types defined elsewhere. *)
-    | Record of { label_opt : string option; fields : record_field list }
+    | Record of {
+        loc : source_location;
+        label_opt : string option;
+        fields : record_field list;
+      }
         (** A set containing all optionally-labelled records formed by the given
             fields. *)
-    | ConstantsSet of string list
-        (** A set containing all constants formed by the given names. *)
+    | ConstantsSet of { loc : source_location; labels : string list }
+        (** A set containing all constants formed by the given labels. *)
     | Function of {
+        loc : source_location;
         from_type : opt_named_type_term;
         to_type : opt_named_type_term;
         total : bool;
@@ -238,28 +251,49 @@ module Term = struct
   and opt_named_type_term = string option * t
   (** A term optionally associated with a variable name. *)
 
-  and record_field = { name : string; term : t; att : Attributes.t }
+  and record_field = {
+    loc : source_location;
+    name : string;
+    term : t;
+    att : Attributes.t;
+  }
   (** A field of a record type. *)
 
-  (** [make_type_operation op term] Constructs a type term in which [op] is
-      applied to [term]. *)
-  let make_type_operation op term = TypeOperator { op; term }
-
-  (** [make_tuple args] Constructs an unlabelled tuple for the tuple args
-      [args]. *)
-  let make_tuple args = Tuple { label_opt = None; args }
-
-  (** [make_labelled_tuple label args] Constructs a tuple labelled [label] and
-      tuple args [args]. *)
-  let make_labelled_tuple label args = Tuple { label_opt = Some label; args }
-
-  let make_record_field (name, term) attributes =
+  (** [loc_of term] returns the source location of [term]. *)
+  let loc_of term =
+    match term with
+    | Label { loc }
+    | TypeOperator { loc }
+    | Tuple { loc }
+    | Record { loc }
+    | Function { loc }
+    | ConstantsSet { loc } ->
+        loc
+
+  (** [make_label loc label] Constructs a label with the given location [loc]
+      and label [label]. *)
+  let make_label loc label = Label { loc; label }
+
+  (** [make_type_operation loc op term] constructs a type term in which [op] is
+      applied to [term] at source location [loc]. *)
+  let make_type_operation loc op term = TypeOperator { loc; op; term }
+
+  (** [make_tuple loc args] constructs an unlabelled tuple with arguments [args]
+      at source location [loc]. *)
+  let make_tuple loc args = Tuple { loc; label_opt = None; args }
+
+  (** [make_labelled_tuple loc label args] constructs a tuple labelled [label]
+      with arguments [args] at source location [loc]. *)
+  let make_labelled_tuple loc label args =
+    Tuple { loc; label_opt = Some label; args }
+
+  let make_record_field loc (name, term) attributes =
     let att = Attributes.of_list attributes in
-    { name; term; att }
+    { loc; name; term; att }
 
-  (** [make_record fields] Constructs an unlabelled record with fields [fields].
-  *)
-  let make_record fields = Record { label_opt = None; fields }
+  (** [make_record loc fields] constructs an unlabelled record with fields
+      [fields] at source location [loc]. *)
+  let make_record loc fields = Record { loc; label_opt = None; fields }
 
   let field_type { term } = term
   let field_name { name } = name
@@ -270,33 +304,50 @@ module Term = struct
   let record_field_prose_description { att } =
     Attributes.get_string_or_empty AttributeKey.Prose_Description att
 
-  (** [make_labelled_record label fields] Constructs a record labelled [label]
-      with fields [fields]. *)
-  let make_labelled_record label fields =
-    Record { label_opt = Some label; fields }
+  (** [make_labelled_record loc label fields] constructs a record labelled
+      [label] with fields [fields] at source location [loc]. *)
+  let make_labelled_record loc label fields =
+    Record { loc; label_opt = Some label; fields }
 end
 
 module Expr = struct
   (** A term that can be used to form a rule judgment. *)
   type t =
-    | Var of string
-    | FieldAccess of { base : t; field : string }
-    | ListIndex of { list_var : string; index : t }
+    | Var of { loc : source_location; id : string }
+    | FieldAccess of { loc : source_location; base : t; field : string }
+    | ListIndex of { loc : source_location; list_var : string; index : t }
         (** An expression indexing into the list variable [list_var] at position
             [index]. *)
-    | Record of { label_opt : string option; fields : (string * t) list }
-        (** A record construction expression. *)
-    | RecordUpdate of { record_expr : t; updates : (string * t) list }
+    | Record of {
+        loc : source_location;
+        label_opt : string option;
+        fields : (string * t) list;
+      }  (** A record construction expression. *)
+    | RecordUpdate of {
+        loc : source_location;
+        record_expr : t;
+        updates : (string * t) list;
+      }
         (** A record update expression that updates the fields given in
             [updates] of the record given by [record_expr]. *)
-    | UnresolvedApplication of { lhs : t; args : t list }
+    | UnresolvedApplication of { loc : source_location; lhs : t; args : t list }
         (** An application expression whose left-hand side has not yet been
             resolved. *)
-    | Tuple of { label_opt : string option; args : t list }
-    | Relation of { name : string; is_operator : bool; args : t list }
-    | Map of { lhs : t; args : t list }
+    | Tuple of {
+        loc : source_location;
+        label_opt : string option;
+        args : t list;
+      }
+    | Relation of {
+        loc : source_location;
+        name : string;
+        is_operator : bool;
+        args : t list;
+      }
+    | Map of { loc : source_location; lhs : t; args : t list }
         (** A map expression applies a function given by [lhs] to [args]. *)
     | Transition of {
+        loc : source_location;
         lhs : t;
         rhs : t;
         short_circuit : t list option;
@@ -307,8 +358,18 @@ module Expr = struct
       }
         (** A transition from the [lhs] configuration to the [rhs] configuration
             with optional alternatives. *)
-    | Indexed of { index : string; list_var : string; body : t }
-    | NamedExpr of { expr : t; name : string; same_name : bool }
+    | Indexed of {
+        loc : source_location;
+        index : string;
+        list_var : string;
+        body : t;
+      }
+    | NamedExpr of {
+        loc : source_location;
+        expr : t;
+        name : string;
+        same_name : bool;
+      }
         (** An (internally-)named expression. Used for giving names to
             sub-expressions appearing in the output configuration of an output
             judgment. Initially, all expressions are unnamed, names are assigned
@@ -316,39 +377,60 @@ module Expr = struct
             this expression is the same as the name of its sub-expression, which
             is used to determine whether to render the name in the output. *)
 
-  (** [make_var id] constructs a variable expression with identifier [id]. *)
-  let make_var id = Var id
-
-  (** [make_tuple args] constructs a tuple expression with the given arguments.
-  *)
-  let make_tuple args = Tuple { label_opt = None; args }
-
-  let make_labelled_tuple label args = Tuple { label_opt = Some label; args }
-  let make_opt_labelled_tuple label_opt args = Tuple { label_opt; args }
-
-  (** [make_application lhs args] constructs an application expression with
-      left-hand side [lhs] and argument expressions [args]. During rule
-      resolution, [lhs] is expected to resolve to either a relation name or a
-      tuple label. *)
-  let make_application lhs args = UnresolvedApplication { lhs; args }
-
-  (** [make_operator_application op_name args] constructs an application
-      expression representing the application of operator [op_name] to [args].
-  *)
-  let make_operator_application name args =
-    Relation { name; is_operator = true; args }
-
-  let make_record label_opt fields = Record { label_opt; fields }
-
-  let make_record_update record_expr updates =
-    RecordUpdate { record_expr; updates }
-
-  let make_list_index list_var index = ListIndex { list_var; index }
+  (** [loc_of expr] returns the source location of [expr]. *)
+  let loc_of = function
+    | Var { loc }
+    | FieldAccess { loc }
+    | ListIndex { loc }
+    | Record { loc }
+    | RecordUpdate { loc }
+    | UnresolvedApplication { loc }
+    | Tuple { loc }
+    | Relation { loc }
+    | Map { loc }
+    | Transition { loc }
+    | Indexed { loc }
+    | NamedExpr { loc } ->
+        loc
+
+  (** [make_var loc id] constructs a variable expression with identifier [id] at
+      source location [loc]. *)
+  let make_var loc id = Var { loc; id }
+
+  (** [make_tuple loc args] constructs a tuple expression with arguments [args]
+      at source location [loc]. *)
+  let make_tuple loc args = Tuple { loc; label_opt = None; args }
+
+  let make_labelled_tuple loc label args =
+    Tuple { loc; label_opt = Some label; args }
+
+  let make_opt_labelled_tuple loc label_opt args =
+    Tuple { loc; label_opt; args }
+
+  (** [make_application loc lhs args] constructs an application expression with
+      left-hand side [lhs] and argument expressions [args] at source location
+      [loc]. During rule resolution, [lhs] is expected to resolve to either a
+      relation name or a tuple label. *)
+  let make_application loc lhs args = UnresolvedApplication { loc; lhs; args }
+
+  (** [make_operator_application loc name args] constructs an application
+      expression representing the application of operator [name] to [args] at
+      source location [loc]. *)
+  let make_operator_application loc name args =
+    Relation { loc; name; is_operator = true; args }
+
+  let make_record loc label_opt fields = Record { loc; label_opt; fields }
+
+  let make_record_update loc record_expr updates =
+    RecordUpdate { loc; record_expr; updates }
+
+  let make_list_index loc list_var index = ListIndex { loc; list_var; index }
 end
 
 (** A datatype for a constant definition. *)
 module Constant : sig
   type t = {
+    loc : source_location;
     name : string;
     opt_type : Term.t option;
     opt_value_and_attributes : (Expr.t * Attributes.t) option;
@@ -356,6 +438,7 @@ module Constant : sig
   }
 
   val make :
+    source_location ->
     string ->
     Term.t option ->
     (Expr.t * attribute_pairs) option ->
@@ -370,6 +453,7 @@ module Constant : sig
   (** The layout for the value, if one exists. *)
 end = struct
   type t = {
+    loc : source_location;
     name : string;
     opt_type : Term.t option;
     opt_value_and_attributes : (Expr.t * Attributes.t) option;
@@ -380,13 +464,14 @@ end = struct
 
   open Attributes
 
-  let make name opt_type opt_value_and_attribute_pairs attributes =
+  let make loc name opt_type opt_value_and_attribute_pairs attributes =
     let opt_value_and_attributes =
       match opt_value_and_attribute_pairs with
       | Some (e, attr_pairs) -> Some (e, Attributes.of_list attr_pairs)
       | None -> None
     in
     {
+      loc;
       name;
       opt_type;
       opt_value_and_attributes;
@@ -409,7 +494,12 @@ end
 module TypeVariant : sig
   open Term
 
-  type t = { type_kind : type_kind; term : Term.t; att : Attributes.t }
+  type t = {
+    loc : source_location;
+    type_kind : type_kind;
+    term : Term.t;
+    att : Attributes.t;
+  }
 
   val make : type_kind -> Term.t -> attribute_pairs -> t
   val attributes_to_list : t -> attribute_pairs
@@ -420,10 +510,20 @@ module TypeVariant : sig
   (** The layout of the type term when rendered in the context of its containing
       type. *)
 end = struct
-  type t = { type_kind : Term.type_kind; term : Term.t; att : Attributes.t }
+  type t = {
+    loc : source_location;
+    type_kind : Term.type_kind;
+    term : Term.t;
+    att : Attributes.t;
+  }
 
   let make type_kind term attribute_pairs =
-    { type_kind; term; att = Attributes.of_list attribute_pairs }
+    {
+      loc = Term.loc_of term;
+      type_kind;
+      term;
+      att = Attributes.of_list attribute_pairs;
+    }
 
   open Attributes
 
@@ -442,6 +542,7 @@ end
 (** A datatype for a type definition. *)
 module Type : sig
   type t = {
+    loc : source_location;
     name : string;
     type_kind : Term.type_kind;
     variants : TypeVariant.t list;
@@ -449,7 +550,12 @@ module Type : sig
   }
 
   val make :
-    Term.type_kind -> string -> TypeVariant.t list -> attribute_pairs -> t
+    source_location ->
+    Term.type_kind ->
+    string ->
+    TypeVariant.t list ->
+    attribute_pairs ->
+    t
 
   val attributes_to_list : t -> attribute_pairs
   val prose_description : t -> string
@@ -460,13 +566,14 @@ module Type : sig
   (** The layout used when rendered as a stand-alone type definition. *)
 end = struct
   type t = {
+    loc : source_location;
     name : string;
     type_kind : Term.type_kind;
     variants : TypeVariant.t list;
     att : Attributes.t;
   }
 
-  let make type_kind name variants attribute_pairs =
+  let make loc type_kind name variants attribute_pairs =
     (* The [type_kind] of the variants is the [type_kind] given above. *)
     let variants_with_parent_type_kind =
       List.map
@@ -476,6 +583,7 @@ end = struct
         variants
     in
     {
+      loc;
       type_kind;
       name;
       variants = variants_with_parent_type_kind;
@@ -521,7 +629,7 @@ module Rule = struct
     | Cases of case list
 
   and case = { name : string; elements : rule_element list }
-  (** A sub-tree of judgments. *)
+  (** A named sub-tree of rule elements. *)
 
   type t = rule_element list
 
@@ -547,6 +655,7 @@ module Relation : sig
     | RelationCategory_Semantics
 
   type t = {
+    loc : source_location;
     name : string;
     parameters : string list;
         (** Type parameters. Currently, only available to operators. *)
@@ -562,6 +671,7 @@ module Relation : sig
   }
 
   val make :
+    source_location ->
     string ->
     relation_property ->
     relation_category option ->
@@ -572,6 +682,7 @@ module Relation : sig
     t
 
   val make_operator :
+    source_location ->
     string ->
     string list ->
     Term.opt_named_type_term list ->
@@ -610,6 +721,7 @@ end = struct
     | RelationCategory_Semantics
 
   type t = {
+    loc : source_location;
     name : string;
     parameters : string list;
     is_operator : bool;
@@ -622,8 +734,9 @@ end = struct
     rule_opt : Rule.t option;
   }
 
-  let make name property category input output attributes rule_opt =
+  let make loc name property category input output attributes rule_opt =
     {
+      loc;
       name;
       parameters = [];
       is_operator = false;
@@ -636,8 +749,10 @@ end = struct
       rule_opt;
     }
 
-  let make_operator name parameters input output_type is_variadic attributes =
+  let make_operator loc name parameters input output_type is_variadic attributes
+      =
     {
+      loc;
       name;
       parameters;
       is_operator = true;
@@ -696,12 +811,19 @@ module TypesRender : sig
   type type_subset_pointer = { type_name : string; variant_names : string list }
 
   type t = {
+    loc : source_location;
     name : string;
     pointers : type_subset_pointer list;
     att : Attributes.t;
   }
 
-  val make : string -> (string * string list) list -> attribute_pairs -> t
+  val make :
+    source_location ->
+    string ->
+    (string * string list) list ->
+    attribute_pairs ->
+    t
+
   val attributes_to_list : t -> attribute_pairs
 
   val lhs_hypertargets : t -> bool
@@ -711,13 +833,15 @@ end = struct
   type type_subset_pointer = { type_name : string; variant_names : string list }
 
   type t = {
+    loc : source_location;
     name : string;
     pointers : type_subset_pointer list;
     att : Attributes.t;
   }
 
-  let make name pointer_pairs attributes =
+  let make loc name pointer_pairs attributes =
     {
+      loc;
       name;
       pointers =
         List.map
@@ -733,18 +857,29 @@ end = struct
 end
 
 module RuleRender : sig
-  type t = { name : string; relation_name : string; path : string }
+  type t = {
+    loc : source_location;
+    name : string;
+    relation_name : string;
+    path : string;
+  }
 
-  val make : name:string -> relation_name:string -> string list -> t
+  val make :
+    source_location -> name:string -> relation_name:string -> string list -> t
 end = struct
-  type t = { name : string; relation_name : string; path : string }
+  type t = {
+    loc : source_location;
+    name : string;
+    relation_name : string;
+    path : string;
+  }
 
   (** [make ~name ~relation_name path] creates a rule render named [name], for
-      the relation [relation_name] with [path] acting as a filter on the cases
-      to render. Only cases whose predicates match the path are included (so an
+      the relation [relation_name] with [path] acting as a filter on the case
+      names to render. Only cases whose names match the path are included (so an
       empty path selects all cases). *)
-  let make ~name ~relation_name path =
-    { name; relation_name; path = Rule.join_case_names path }
+  let make loc ~name ~relation_name path =
+    { loc; name; relation_name; path = Rule.join_case_names path }
 end
 
 (** The top-level elements of a specification. *)
diff --git a/asllib/aslspec/ASTUtils.ml b/asllib/aslspec/ASTUtils.ml
index 7f6c441047..a312c38671 100644
--- a/asllib/aslspec/ASTUtils.ml
+++ b/asllib/aslspec/ASTUtils.ml
@@ -36,7 +36,7 @@ and vars_of_opt_named_type_terms opt_named_terms =
 
 let variant_to_label_opt { TypeVariant.term } =
   match term with
-  | Label label -> Some label
+  | Label { label } -> Some label
   | Tuple { label_opt } | Record { label_opt } -> label_opt
   | _ -> None
 
diff --git a/asllib/aslspec/PP.ml b/asllib/aslspec/PP.ml
index 84042f631f..b1386c8a08 100644
--- a/asllib/aslspec/PP.ml
+++ b/asllib/aslspec/PP.ml
@@ -53,7 +53,7 @@ let type_operator_to_token =
 let rec pp_type_term fmt =
   let open Term in
   function
-  | Label name -> pp_print_string fmt name
+  | Label { label } -> pp_print_string fmt label
   | TypeOperator { op; term } ->
       fprintf fmt "%s(%a)"
         (type_operator_to_token op |> tok_str)
@@ -65,10 +65,10 @@ let rec pp_type_term fmt =
   | Record { label_opt; fields } ->
       let label = Option.value label_opt ~default:"" in
       fprintf fmt "%s[%a]" label pp_record_fields fields
-  | ConstantsSet constants ->
+  | ConstantsSet { labels } ->
       fprintf fmt "%s(%a)" (tok_str CONSTANTS_SET)
         (pp_sep_list ~sep:"," pp_print_string)
-        constants
+        labels
   | Function { from_type; to_type; total } ->
       let keyword = if total then tok_str FUN else tok_str PARTIAL in
       fprintf fmt "%s %a -> %a" keyword pp_opt_named_type_term from_type
@@ -108,7 +108,7 @@ let pp_output_opt fmt is_output = if is_output then fprintf fmt "--@," else ()
 let rec pp_expr fmt =
   let open Expr in
   function
-  | Var name -> pp_print_string fmt name
+  | Var { id } -> pp_print_string fmt id
   | UnresolvedApplication { lhs; args } ->
       fprintf fmt "%a(%a)" pp_expr lhs (pp_comma_list pp_expr) args
   | Tuple { label_opt; args } ->
diff --git a/asllib/aslspec/SpecParser.mly b/asllib/aslspec/SpecParser.mly
index 733f5fe0f5..1d6ef5a579 100644
--- a/asllib/aslspec/SpecParser.mly
+++ b/asllib/aslspec/SpecParser.mly
@@ -2,27 +2,30 @@
 open AST
 open AST.AttributeKey
 
+(** Converts Menhir's [$sloc] pair into a [source_location] record. *)
+let loc (start_pos, end_pos) = { AST.start_pos; end_pos }
+
 (** Elements such as types, constants, and relations generate custom LaTeX macros.
     Since LaTeX macro names do not allow certain characters, such as numbers and apostrophes,
     we need to check that element-defining identifiers conform to those restrictions.
 *)
-let check_definition_name name =
+let check_definition_name loc name =
    let () = assert (String.length name > 0) in
    let id_regexp = Str.regexp "^[A-Za-z_']+$" in
    if not (Str.string_match id_regexp name 0) then
      let msg = Format.sprintf "illegal element-defining identifier: %s" name in
-     raise (SpecError msg)
+     raise (SpecError { loc; msg })
 
-let bool_of_string s =
+let bool_of_string loc s =
   match String.lowercase_ascii s with
   | "true" -> true
   | "false" -> false
   | _ ->
       let msg = Format.sprintf "expected boolean string (true/false), got: %s" s in
-      raise (SpecError msg)
+      raise (SpecError { loc; msg })
 
 (** Checks that the given string has balanced braces, which avoids LaTeX compilation errors. *)
-let check_balanced_braces s =
+let check_balanced_braces loc s =
   let rec scan i depth =
     if i >= String.length s then
       depth = 0
@@ -40,8 +43,8 @@ let check_balanced_braces s =
         scan (i + 1) new_depth
   in
   if not (scan 0 0) then
-    let msg = Format.sprintf "unbalanced braces in string: %s" s in
-    raise (SpecError msg)
+    let msg = Format.sprintf "unbalanced braces in: %s" s in
+    raise (SpecError {loc; msg })
 %}
 
 %type <AST.t> spec
@@ -166,9 +169,6 @@ let some(x) == ~ = x ; <Some>
    rules. *)
 let terminated_by(x, y) == terminated(y, x)
 
-(* Position annotation *)
-let annotated(x) == desc = x; { { desc; pos_start=$symbolstartpos; pos_end=$endpos } }
-
 (* ------------------------------------------------------------------------- *)
 (* Parameterized lists *)
 
@@ -222,25 +222,24 @@ let elem :=
 let type_kind := TYPEDEF; { Term.TypeKind_Generic }
     | AST; { Term.TypeKind_AST }
 
+let checked_identifier == id=IDENTIFIER; { check_definition_name (loc $sloc) id; id }
+
 let type_definition :=
-    | ~=type_kind; type_name=IDENTIFIER; ~=type_attributes; ~=type_variants_with_attributes;
-    {   check_definition_name type_name;
-        Elem_Type (Type.make type_kind type_name type_variants_with_attributes type_attributes) }
+    | ~=type_kind; type_name=checked_identifier; ~=type_attributes; ~=type_variants_with_attributes;
+    {   Elem_Type (Type.make (loc $sloc) type_kind type_name type_variants_with_attributes type_attributes) }
     | type_kind; type_name=IDENTIFIER; type_attributes; list1(type_variant_with_attributes);
     {   let msg = Format.sprintf "Definition of 'typedef %s' is missing '='" type_name in
-        raise (SpecError msg) }
+        raise (SpecError { loc = (loc $sloc); msg }) }
 
 let relation_definition :=
-    ~=relation_category; ~=relation_property; name=IDENTIFIER; input=plist0(opt_named_type_term); ARROW; output=type_variants;
+    ~=relation_category; ~=relation_property; name=checked_identifier; input=plist0(opt_named_type_term); ARROW; output=type_variants;
     ~=relation_attributes; ~=opt_relation_rule;
-    {   check_definition_name name;
-        Elem_Relation (Relation.make name relation_property relation_category input output relation_attributes opt_relation_rule) }
+    {   Elem_Relation (Relation.make (loc $sloc) name relation_property relation_category input output relation_attributes opt_relation_rule) }
 
 let operator_definition :=
-    ~=is_variadic; OPERATOR; name=IDENTIFIER; ~=parameters; input=plist0(opt_named_type_term); ARROW; output=type_term;
+    ~=is_variadic; OPERATOR; name=checked_identifier; ~=parameters; input=plist0(opt_named_type_term); ARROW; output=type_term;
     ~=operator_attributes;
-    {   check_definition_name name;
-        Elem_Relation (Relation.make_operator name parameters input output is_variadic operator_attributes) }
+    {   Elem_Relation (Relation.make_operator (loc $sloc) name parameters input output is_variadic operator_attributes) }
 
 let is_variadic :=
     | VARIADIC; { true }
@@ -250,9 +249,8 @@ let parameters :=
     | LBRACKET; params=tclist1(IDENTIFIER); RBRACKET; { params }
     | { [] }
 
-let constant_definition := CONSTANT; name=IDENTIFIER; ~=opt_type; att=type_attributes; ~=opt_value_and_attributes;
-    {   check_definition_name name;
-        Elem_Constant (Constant.make name opt_type opt_value_and_attributes att) }
+let constant_definition := CONSTANT; name=checked_identifier; ~=opt_type; att=type_attributes; ~=opt_value_and_attributes;
+    {   Elem_Constant (Constant.make (loc $sloc) name opt_type opt_value_and_attributes att) }
 
 let opt_type :=
     | { None }
@@ -285,13 +283,18 @@ let type_attribute :=
     | math_layout_attribute
     | short_circuit_macro_attribute
 
+let checked_template_attribute == template=STRING; {
+    check_balanced_braces (loc $sloc) template;
+    StringAttribute template
+}
+
 let prose_description_attribute ==
-    | PROSE_DESCRIPTION; EQ; template=STRING; {
-        check_balanced_braces template;
-        (Prose_Description, StringAttribute template) }
-    | template=STRING; {
-        check_balanced_braces template;
-        (Prose_Description, StringAttribute template) }
+    | PROSE_DESCRIPTION; EQ; template=checked_template_attribute; {
+        (Prose_Description, template)
+    }
+    | template=checked_template_attribute; {
+        (Prose_Description, template)
+    }
 
 let math_macro_attribute ==
     MATH_MACRO; EQ; macro=LATEX_MACRO; { (Math_Macro, MathMacroAttribute macro) }
@@ -319,20 +322,22 @@ let operator_attribute :=
     | operator_style_attribute
     | prose_application_attribute
 
+let bool_attribute_value == value=IDENTIFIER; { BoolAttribute (bool_of_string (loc $sloc) value) }
+
 let operator_style_attribute ==
-    | ASSOCIATIVE; EQ; value=IDENTIFIER; { (Associative, BoolAttribute (bool_of_string value)) }
-    | CUSTOM; EQ; value=IDENTIFIER; { (Custom, BoolAttribute (bool_of_string value)) }
-    | TYPECAST; EQ; value=IDENTIFIER; { (Typecast, BoolAttribute (bool_of_string value)) }
+    | ASSOCIATIVE; EQ; value=bool_attribute_value; { (Associative, value) }
+    | CUSTOM; EQ; value=bool_attribute_value; { (Custom, value) }
+    | TYPECAST; EQ; value=bool_attribute_value; { (Typecast, value) }
 
 let prose_application_attribute ==
-    PROSE_APPLICATION; EQ; template=STRING; {
-        check_balanced_braces template;
-        (Prose_Application, StringAttribute template) }
+    PROSE_APPLICATION; EQ; template=checked_template_attribute; {
+        (Prose_Application, template)
+    }
 
 let prose_transition_attribute ==
-    PROSE_TRANSITION; EQ; template=STRING; {
-        check_balanced_braces template;
-        (Prose_Transition, StringAttribute template) }
+    PROSE_TRANSITION; EQ; template=checked_template_attribute; {
+        (Prose_Transition, template)
+    }
 
 let type_variants_with_attributes :=
     | { [] }
@@ -350,19 +355,17 @@ let type_term_with_attributes := ~=type_term; ~=type_attributes;
     { TypeVariant.make TypeKind_Generic type_term type_attributes }
 
 let type_term :=
-    | name=IDENTIFIER; { check_definition_name name; Label name }
-    | op=type_operator; LPAR; ~=opt_named_type_term; RPAR; { Term.make_type_operation op opt_named_type_term }
-    | LPAR; args=tclist1(opt_named_type_term); RPAR; { Tuple {label_opt = None; args} }
-    | label=IDENTIFIER; LPAR; args=tclist1(opt_named_type_term); RPAR;
-    {   check_definition_name label;
-        Tuple {label_opt = Some label; args} }
-    | LBRACKET; fields=tclist1(record_field); RBRACKET; { Term.make_record fields }
-    | label=IDENTIFIER; LBRACKET; fields=tclist1(record_field); RBRACKET;
-    {   check_definition_name label;
-        Term.make_labelled_record label fields }
-    | CONSTANTS_SET; LPAR; constants=tclist1(IDENTIFIER); RPAR; { ConstantsSet constants }
-    | FUN; from_type=opt_named_type_term; ARROW; to_type=opt_named_type_term; { Function {from_type; to_type; total = true}}
-    | PARTIAL; from_type=opt_named_type_term; ARROW; to_type=opt_named_type_term; { Function {from_type; to_type; total = false}}
+    | name=checked_identifier; { Term.make_label (loc $sloc) name }
+    | op=type_operator; LPAR; ~=opt_named_type_term; RPAR; { Term.make_type_operation (loc $sloc) op opt_named_type_term }
+    | LPAR; args=tclist1(opt_named_type_term); RPAR; { Term.make_tuple (loc $sloc) args }
+    | label=checked_identifier; LPAR; args=tclist1(opt_named_type_term); RPAR;
+    {   Term.make_labelled_tuple (loc $sloc) label args }
+    | LBRACKET; fields=tclist1(record_field); RBRACKET; { Term.make_record (loc $sloc) fields }
+    | label=checked_identifier; LBRACKET; fields=tclist1(record_field); RBRACKET;
+    {   Term.make_labelled_record (loc $sloc) label fields }
+    | CONSTANTS_SET; LPAR; labels=tclist1(IDENTIFIER); RPAR; { ConstantsSet {loc=(loc $sloc); labels} }
+    | FUN; from_type=opt_named_type_term; ARROW; to_type=opt_named_type_term; { Function {loc=(loc $sloc); from_type; to_type; total = true}}
+    | PARTIAL; from_type=opt_named_type_term; ARROW; to_type=opt_named_type_term; { Function {loc=(loc $sloc); from_type; to_type; total = false}}
 
 let type_operator :=
     | POWERSET; { Powerset }
@@ -379,7 +382,7 @@ let opt_named_type_term ==
     | ~=type_term; { (None, type_term) }
 
 let record_field := ~=named_type_term; ~=type_attributes;
-    { Term.make_record_field named_type_term type_attributes }
+    { Term.make_record_field (loc $sloc) named_type_term type_attributes }
 
 let math_layout :=
     | IDENTIFIER; { Unspecified }
@@ -389,9 +392,8 @@ let math_layout :=
     | IDENTIFIER; LBRACKET; inner=clist0(math_layout); RBRACKET; { Vertical inner }
 
 let render_types :=
-    RENDER; name=IDENTIFIER; ~=render_types_attributes; EQ; pointers=clist1(type_subset_pointer);
-    {   check_definition_name name;
-        Elem_RenderTypes (TypesRender.make name pointers render_types_attributes) }
+    RENDER; name=checked_identifier; ~=render_types_attributes; EQ; pointers=clist1(type_subset_pointer);
+    {   Elem_RenderTypes (TypesRender.make (loc $sloc) name pointers render_types_attributes) }
 
 let type_subset_pointer :=
     | type_name=IDENTIFIER; LPAR; MINUS; RPAR; { (type_name, []) }
@@ -405,7 +407,7 @@ let render_types_attribute :=
     | lhs_hypertargets
 
 let lhs_hypertargets ==
-    | LHS_HYPERTARGETS; EQ; value=IDENTIFIER;{ (LHS_Hypertargets, BoolAttribute (bool_of_string value)) }
+    | LHS_HYPERTARGETS; EQ; value=bool_attribute_value; { (LHS_Hypertargets, value) }
 
 let opt_relation_rule := { None }
     | EQ; ~=rule; { Some rule }
@@ -427,35 +429,35 @@ let judgment :=
 
 let index_judgement :=
     | INDEX; LPAR; index=IDENTIFIER; COMMA; list_var=IDENTIFIER; COLON; body=transition_expr; RPAR;
-      { Expr.Indexed { index; list_var; body } }
+      { Expr.Indexed { loc=(loc $sloc); index; list_var; body } }
 
-let var_expr := id=IDENTIFIER; { Expr.make_var id }
+let var_expr := id=IDENTIFIER; { Expr.make_var (loc $sloc) id }
 
 let expr :=
     | var_expr
     | args=plist1(expr);
-      { Expr.make_tuple args }
+      { Expr.make_tuple (loc $sloc) args }
     | lhs=expr; args=plist0(expr);
-      { Expr.make_application lhs args }
+      { Expr.make_application (loc $sloc) lhs args }
     | base=expr; DOT; field=IDENTIFIER;
-      { Expr.FieldAccess { base; field } }
+      { Expr.FieldAccess { loc=(loc $sloc); base; field } }
     | list_var=IDENTIFIER; LBRACKET; index=expr; RBRACKET;
-      { Expr.make_list_index list_var index }
+      { Expr.make_list_index (loc $sloc) list_var index }
     | label_opt=ioption(IDENTIFIER); LBRACKET; fields=tclist1(field_and_value); RBRACKET;
-      { Expr.make_record label_opt fields }
+      { Expr.make_record (loc $sloc) label_opt fields }
     | base=expr; LPAR; fields=tclist1(field_and_value); RPAR;
-      { Expr.make_record_update base fields }
+      { Expr.make_record_update (loc $sloc) base fields }
     | lhs=expr; ~=infix_expr_operator; rhs=expr;
-      { Expr.make_operator_application infix_expr_operator [lhs; rhs] }
+      { Expr.make_operator_application (loc $sloc) infix_expr_operator [lhs; rhs] }
     | IF; cond=expr; THEN; then_branch=expr; ELSE; else_branch=expr;
-      { Expr.make_operator_application "if_then_else" [cond; then_branch; else_branch] }
+      { Expr.make_operator_application (loc $sloc) "if_then_else" [cond; then_branch; else_branch] }
     | cond_expr
 
 let cond_expr :=
     | COND; LPAR; cases=tclist1(cond_case); RPAR;
-      { Expr.make_operator_application "cond_op" cases }
+      { Expr.make_operator_application (loc $sloc) "cond_op" cases }
 let cond_case :=
-    | condition=expr; COLON; result=expr; { Expr.make_operator_application "cond_case" [condition; result] }
+    | condition=expr; COLON; result=expr; { Expr.make_operator_application (loc $sloc) "cond_case" [condition; result] }
 
 let maybe_output_expr ==
     | { false }
@@ -464,25 +466,25 @@ let maybe_output_expr ==
 let judgment_expr :=
     | transition_expr
     | LPAR; ~=transition_expr; RPAR;
-      { Expr.make_tuple [ transition_expr ] }
+      { Expr.make_tuple (loc $sloc) [ transition_expr ] }
     | index_judgement
     | LPAR; ~=index_judgement; RPAR;
-      { Expr.make_tuple [ index_judgement ] }
+      { Expr.make_tuple (loc $sloc) [ index_judgement ] }
 
 let transition_expr :=
     | lhs=expr; ARROW; rhs=transition_output_expr; ~=short_circuit;
-      { Expr.Transition { lhs; rhs; short_circuit } }
+      { Expr.Transition { loc=(loc $sloc); lhs; rhs; short_circuit } }
 
 let transition_output_expr :=
     | var_expr
     | args=plist1(transition_output_expr);
-      { Expr.make_tuple args }
-    | label=IDENTIFIER; args=plist1(transition_output_expr);
-      { Expr.make_application (Expr.make_var label) args }
+      { Expr.make_tuple (loc $sloc) args }
+    | label_as_var=var_expr; args=plist1(transition_output_expr);
+      { Expr.make_application (loc $sloc) label_as_var args }
     | list_var=IDENTIFIER; LBRACKET; index=transition_output_expr; RBRACKET;
-      { Expr.make_list_index list_var index }
+      { Expr.make_list_index (loc $sloc) list_var index }
     | lhs=transition_output_expr; ~=infix_expr_operator; rhs=transition_output_expr;
-      { Expr.make_operator_application infix_expr_operator [lhs; rhs] }
+      { Expr.make_operator_application (loc $sloc) infix_expr_operator [lhs; rhs] }
 
 let short_circuit :=
     | { None } (* Short-circuiting expressions will be inserted automatically. *)
@@ -492,10 +494,9 @@ let short_circuit :=
       { Some alternatives }
 
 let short_circuit_expr :=
-    | id=IDENTIFIER;
-      { Expr.make_var id }
-    | lhs=IDENTIFIER; args=plist0(IDENTIFIER);
-      { Expr.make_application (Expr.make_var lhs) (List.map Expr.make_var args) }
+    | var_expr
+    | lhs=var_expr; args=plist0(var_expr);
+      { Expr.make_application (loc $sloc) lhs args }
 
 let infix_expr_operator ==
     | COLON_EQ; { "assign" }
@@ -527,10 +528,10 @@ let judgment_attribute :=
     | math_layout_attribute
 
 let render_rule :=
-  | RENDER; RULE; name=IDENTIFIER; EQ; relation_name=IDENTIFIER; rule_name=pared(rule_name);
-    { check_definition_name name; Elem_RenderRule (RuleRender.make ~name ~relation_name rule_name) }
-  | RENDER; RULE; name=IDENTIFIER;
-    { check_definition_name name; Elem_RenderRule (RuleRender.make ~name ~relation_name:name []) }
+  | RENDER; RULE; name=checked_identifier; EQ; relation_name=IDENTIFIER; rule_name=pared(rule_name);
+    { Elem_RenderRule (RuleRender.make (loc $sloc) ~name ~relation_name rule_name) }
+  | RENDER; RULE; name=checked_identifier;
+    { Elem_RenderRule (RuleRender.make (loc $sloc) ~name ~relation_name:name []) }
     (** Stands for the entire rule for the given relation. *)
 
 let rule_name :=
diff --git a/asllib/aslspec/error.ml b/asllib/aslspec/error.ml
index f951308665..87291d5ae0 100644
--- a/asllib/aslspec/error.ml
+++ b/asllib/aslspec/error.ml
@@ -1,68 +1,87 @@
 open AST
+open ASTUtils
 
-let spec_error msg = raise (SpecError msg)
+(** [spec_error loc msg] raises a [SpecError] with a message [msg] and source
+    location [loc]. *)
+let spec_error loc msg = raise (SpecError { loc; msg })
+
+(** [spec_error loc msg] raises a [SpecError] with a message [msg] and source
+    location [loc]. *)
+let spec_error loc msg = spec_error loc msg
+
+(** [spec_error_loc_of_expr expr msg] raises a [SpecError] with a message [msg]
+    and the source location of [expr]. *)
+let spec_error_loc_of_expr expr msg =
+  let loc = Expr.loc_of expr in
+  spec_error loc msg
+
+(** [spec_error_loc_of_term term msg] raises a [SpecError] with a message [msg]
+    and the source location of [term]. *)
+let spec_error_loc_of_term term msg =
+  let loc = Term.loc_of term in
+  spec_error loc msg
 
 let bad_layout term layout ~consistent_layout =
-  spec_error
+  spec_error_loc_of_term term
   @@ Format.asprintf
        "layout %a is inconsistent with %a. Here's a consistent layout: %a"
        PP.pp_layout layout PP.pp_type_term term PP.pp_layout consistent_layout
 
-let undefined_reference id context =
-  spec_error @@ Format.asprintf "Undefined reference to '%s' in %s" id context
+let undefined_reference loc id context =
+  spec_error loc @@ Format.asprintf "Undefined reference to %s in %s" id context
 
-let undefined_element id =
-  spec_error @@ Format.asprintf "Encountered undefined element: %s" id
+let undefined_element loc id =
+  spec_error loc @@ Format.asprintf "Encountered undefined element: %s" id
 
-let duplicate_definition id =
-  spec_error @@ Format.asprintf "Duplicate definition of '%s'" id
+let duplicate_definition loc id =
+  spec_error loc @@ Format.asprintf "Duplicate definition of %s" id
 
-let unmatched_variables_in_template template unmatched_vars =
-  spec_error
+let unmatched_variables_in_template loc template unmatched_vars =
+  spec_error loc
   @@ Format.asprintf
-       "The prose template '%s' contains the following unmatched variables: %s"
+       "The prose template \"%s\" contains the following unmatched variables: \
+        %s"
        template
        (String.concat ", " unmatched_vars)
 
 let not_type_name_error relation_name term =
-  spec_error
+  spec_error_loc_of_term term
   @@ Format.asprintf
-       "In relation '%s', output type term '%a' is not a type name or a set of \
+       "In relation %s, output type term %a is not a type name or a set of \
         constants. All relation output types, except for the first one, must \
         be type names or a set of constants."
        relation_name PP.pp_type_term term
 
 let missing_short_circuit_attribute relation_name term type_name =
-  spec_error
+  spec_error_loc_of_term term
   @@ Format.asprintf
-       "In relation '%s', output type term '%a' references type '%s' which \
-        does not have a short-circuit macro defined. All relation output \
-        types, except for the first one, must reference types with \
-        short-circuit macros."
+       "In relation %s, output type term %a references type %s which does not \
+        have a short-circuit macro defined. All relation output types, except \
+        for the first one, must reference types with short-circuit macros."
        relation_name PP.pp_type_term term type_name
 
 let invalid_application_of_symbol_in_expr name expr =
-  spec_error
-  @@ Format.asprintf "Invalid application of symbol '%s' to expression %a" name
-       PP.pp_expr expr
+  spec_error_loc_of_expr expr
+    (Format.asprintf "Invalid application of symbol %s to expression %a" name
+       PP.pp_expr expr)
 
 let type_subsumption_failure sub super =
-  spec_error
+  spec_error_loc_of_term sub
   @@ Format.asprintf "Unable to determine that `%a` is subsumed by `%a`"
        PP.pp_type_term sub PP.pp_type_term super
 
 let argument_subsumption_failure sub super ~context_expr =
-  spec_error
-  @@ Format.asprintf "Unable to determine that `%a` is subsumed by `%a` in %a"
-       PP.pp_type_term sub PP.pp_type_term super PP.pp_expr context_expr
+  spec_error_loc_of_expr context_expr
+    (Format.asprintf "Unable to determine that `%a` is subsumed by `%a` in %a"
+       PP.pp_type_term sub PP.pp_type_term super PP.pp_expr context_expr)
 
-let non_constant_used_as_constant_set id =
-  spec_error
+let non_constant_used_as_constant_set context_term id =
+  spec_error_loc_of_term context_term
   @@ Format.asprintf
        "%s is used as a constant even though it is not defined as one" id
 
 let tuple_instantiation_length_failure term args label def_components =
-  spec_error
+  spec_error_loc_of_term term
   @@ Format.asprintf
        "The type term `%a` cannot be instantiated since it has %i type terms \
         and `%s` requires %i type terms"
@@ -70,85 +89,84 @@ let tuple_instantiation_length_failure term args label def_components =
        (List.length def_components)
 
 let tuple_instantiation_failure_not_labelled_tuple term label =
-  spec_error
+  spec_error_loc_of_term term
   @@ Format.asprintf
-       "The type term `%a` cannot be instantiated since '%s' is not a labelled \
+       "The type term `%a` cannot be instantiated since %s is not a labelled \
         tuple type"
        PP.pp_type_term term label
 
 let record_instantiation_failure_different_fields term def_term =
-  spec_error
+  spec_error_loc_of_term term
   @@ Format.asprintf
        "The type term `%a` cannot be instantiated since its list of fields is \
         different to those of %a"
        PP.pp_type_term term PP.pp_type_term def_term
 
 let record_instantiation_failure_not_labelled_record term label =
-  spec_error
+  spec_error_loc_of_term term
   @@ Format.asprintf
-       "The type term `%a` cannot be instantiated since '%s' is not a labelled \
+       "The type term `%a` cannot be instantiated since %s is not a labelled \
         record type"
        PP.pp_type_term term label
 
 let instantiation_failure_not_a_type term label =
-  spec_error
+  spec_error_loc_of_term term
   @@ Format.asprintf
-       "The type term `%a` cannot be instantiated since '%s' is not a type"
+       "The type term `%a` cannot be instantiated since %s is not a type"
        PP.pp_type_term term label
 
-let empty_rule relation_name =
-  spec_error
-  @@ Format.asprintf "The rule for relation '%s' is empty." relation_name
+let empty_rule { loc; Relation.name } =
+  spec_error loc @@ Format.asprintf "The rule for relation %s is empty." name
 
-let relation_argument_incorrect_naming relation_name term =
-  spec_error
+let relation_argument_incorrect_naming relation_name ((_, term) as arg) =
+  spec_error_loc_of_term term
   @@ Format.asprintf
-       "The term %a in relation '%s' does not provide a name for at least one \
-        of its sub-terms."
-       PP.pp_opt_named_type_term term relation_name
+       "The term %a in relation %s does not provide a name for at least one of \
+        its sub-terms."
+       PP.pp_opt_named_type_term arg relation_name
 
-let multiple_output_judgments relation_name rule_name_opt =
+let multiple_output_judgments { loc; Relation.name } rule_name_opt =
   let pp_name_opt fmt = function
     | Some name -> Format.fprintf fmt ": %s" name
     | None -> ()
   in
-  spec_error
+  spec_error loc
   @@ Format.asprintf
        "All but the last judgment in the rule for relation %s must be \
         non-output judgments%a"
-       relation_name pp_name_opt rule_name_opt
+       name pp_name_opt rule_name_opt
 
-let missing_output_judgment relation_name expanded_rule_name_opt =
-  spec_error
+let missing_output_judgment { loc; Relation.name } expanded_rule_name_opt =
+  spec_error loc
   @@ Format.asprintf
        "The rule for relation %s does not end with an output judgment in case \
         %s"
-       relation_name
+       name
        (Option.value ~default:"top-level" expanded_rule_name_opt)
 
 let illegal_lhs_application expr =
-  spec_error
+  spec_error_loc_of_expr expr
   @@ Format.asprintf
        "The left-hand side of an application must be a relation, type variant, \
-        or operator, but found expression %a"
+        or operator, but found %a"
        PP.pp_expr expr
 
 let invalid_number_of_arguments rel_name expr ~expected ~actual =
-  spec_error
+  spec_error_loc_of_expr expr
   @@ Format.asprintf
-       "The application of relation '%s' in expression %a has an invalid \
-        number of arguments: expected %d but found %d"
+       "The application of relation %s in expression %a has an invalid number \
+        of arguments: expected %d but found %d"
        rel_name PP.pp_expr expr expected actual
 
-let invalid_number_of_components label expr ~expected ~actual =
-  spec_error
+let invalid_number_of_components expr ~expected ~actual =
+  spec_error_loc_of_expr expr
   @@ Format.asprintf
-       "The application of tuple label '%s' in expression %a has an invalid \
-        number of args: expected %d but found %d"
-       label PP.pp_expr expr expected actual
+       "The labelled tuple %a has an invalid number of args: expected %d but \
+        found %d"
+       PP.pp_expr expr expected actual
 
 let invalid_record_field_names expr expr_field_names record_type_field_names =
-  spec_error
+  spec_error_loc_of_expr expr
   @@ Format.asprintf
        "The record expression %a has missing or invalid field names: expected \
         %s but found %s"
@@ -157,70 +175,66 @@ let invalid_record_field_names expr expr_field_names record_type_field_names =
        (String.concat ", " expr_field_names)
 
 let non_field id expr =
-  spec_error
-  @@ Format.asprintf
-       "The non-field identifier '%s' is used in expression %a as a field" id
+  spec_error_loc_of_expr expr
+  @@ Format.asprintf "The non-field identifier %s is used as a field in %a" id
        PP.pp_expr expr
 
 let undefined_variable_in_rule ~context_expr id =
-  spec_error
-  @@ Format.asprintf "The variable %s is used in %a before it is defined" id
-       PP.pp_expr context_expr
+  spec_error_loc_of_expr context_expr
+  @@ Format.asprintf "The variable %s is used before it is defined" id
 
 let redefined_variable_in_rule ~context_expr id =
-  spec_error
-  @@ Format.asprintf
-       "The variable %s is defined twice, the second time is in %a" id
-       PP.pp_expr context_expr
+  spec_error_loc_of_expr context_expr
+  @@ Format.asprintf "The variable %s is re-defined" id
 
 let undefined_field_in_record ~context_expr base_type field_id =
-  spec_error
-  @@ Format.asprintf "The field '%s' is not defined in the record type %a in %a"
+  spec_error_loc_of_expr context_expr
+  @@ Format.asprintf "The field %s is not defined in the record type %a in %a"
        field_id PP.pp_type_term base_type PP.pp_expr context_expr
 
 let invalid_list_index_type index_type ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf
        "The index type %a in %a is not a subtype of the natural numbers type \
         (N)"
        PP.pp_type_term index_type PP.pp_expr context_expr
 
 let invalid_list_base_type base_type ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf "The type %a in %a is not a list type" PP.pp_type_term
        base_type PP.pp_expr context_expr
 
 let invalid_number_of_arguments_for_map ~expected ~actual ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf
        "The map application in %a has an invalid number of arguments: expected \
         %d but found %d"
        PP.pp_expr context_expr expected actual
 
 let invalid_argument_type ~arg_expr ~actual_type ~formal_type ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf
        "The argument or field expression %a has type %a but expected to have a \
-        subtype of %a in %a"
+        subtype of %a"
        PP.pp_expr arg_expr PP.pp_type_term actual_type PP.pp_type_term
-       formal_type PP.pp_expr context_expr
+       formal_type
 
 let invalid_map_lhs_type lhs_type ~context_expr:expr =
-  spec_error
+  spec_error_loc_of_expr expr
   @@ Format.asprintf
        "The map application in %a has an invalid left-hand side type: expected \
         a function type but found %a"
        PP.pp_expr expr PP.pp_type_term lhs_type
 
 let invalid_labelled_type label ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf
-       "The label '%s' does not correspond to a labelled record or tuple in %a"
+       "The label %s does not correspond to a labelled record or tuple in %a"
        label PP.pp_expr context_expr
 
 let type_instantiation_length_failure formal_type arg_type ~expected_length
     ~actual_length =
-  spec_error
+  spec_error_loc_of_term arg_type
   @@ Format.asprintf
        "The type term `%a` cannot be instantiated with `%a` since they have \
         different numbers of arguments/fields: expected %d but found %d"
@@ -228,47 +242,46 @@ let type_instantiation_length_failure formal_type arg_type ~expected_length
        actual_length
 
 let type_operator_instantiation_failure ~relation_name formal_type arg_type =
-  spec_error
+  spec_error_loc_of_term arg_type
   @@ Format.asprintf
        "The type term `%a` cannot be instantiated with `%a` for operator `%s` \
         since there are incompatible argument types for it"
        PP.pp_type_term formal_type PP.pp_type_term arg_type relation_name
 
 let uninstantiated_parameter_in_relation param relation_name ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf
-       "The type parameter '%s' of relation '%s' could not be instantiated in \
-        %a"
+       "The type parameter %s of relation %s could not be instantiated in %a"
        param relation_name PP.pp_expr context_expr
 
-let parameter_type_unification_failure ~relation_name parameter_name term1 term2
-    =
-  spec_error
+let parameter_type_unification_failure loc ~relation_name parameter_name term1
+    term2 =
+  spec_error loc
   @@ Format.asprintf
-       "Could not unify types %a and %a for parameter '%s' of relation '%s'"
+       "Could not unify types %a and %a for parameter %s of relation %s"
        PP.pp_type_term term1 PP.pp_type_term term2 parameter_name relation_name
 
 let only_single_output_relations_supported name ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf
        "Only single output relations are supported outside of transition \
-        judgment: %s in %a"
+        judgments, and %s has more than one output in %a"
        name PP.pp_expr context_expr
 
 let only_relation_transitions_supported ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf
        "Only relation applications are supported on the left-hand side of \
         transitions in %a"
        PP.pp_expr context_expr
 
 let no_matching_output_type rhs ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf "No matching output type found for expression %a in %a"
        PP.pp_expr rhs PP.pp_expr context_expr
 
 let ambiguous_output_type rhs candidates ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf
        "Ambiguous output type for expression %a in %a. Possible candidates: %a"
        PP.pp_expr rhs PP.pp_expr context_expr
@@ -276,47 +289,48 @@ let ambiguous_output_type rhs candidates ~context_expr =
        candidates
 
 let invalid_indexed_body_type body_type ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf "The body type %a in %a is not the Boolean type"
        PP.pp_type_term body_type PP.pp_expr context_expr
 
 let cannot_apply_type_to_expr expr target_type =
-  spec_error
-  @@ Format.asprintf "Cannot apply type %a to expression %a" PP.pp_type_term
-       target_type PP.pp_expr expr
+  spec_error_loc_of_expr expr
+  @@ Format.asprintf "Cannot type %a as %a" PP.pp_expr expr PP.pp_type_term
+       target_type
 
 let judgment_not_boolean inferred_judgment_type judgment_expr =
-  spec_error
+  spec_error_loc_of_expr judgment_expr
   @@ Format.asprintf
-       "The type inferred for the judgment `%a` is %a, which is not Boolean"
+       "The type inferred for the judgment %a is %a, which is not the Boolean \
+        type"
        PP.pp_expr judgment_expr PP.pp_type_term inferred_judgment_type
 
 let output_type_mismatch output_judgment_type output_types output_expr =
-  spec_error
+  spec_error_loc_of_expr output_expr
   @@ Format.asprintf
-       "The type %a inferred for the output judgment `%a` does not match any \
-        of the output types %a"
+       "The type %a inferred for the output judgment %a does not match any of \
+        the output types %a"
        PP.pp_type_term output_judgment_type PP.pp_expr output_expr
        (PP.pp_sep_list ~sep:" | " PP.pp_type_term)
        output_types
 
 let record_update_expression_not_assignable expr =
-  spec_error
+  spec_error_loc_of_expr expr
   @@ Format.asprintf
-       "The record update expression `%a` cannot be used as an assignable \
+       "The record update expression %a cannot be used as an assignable \
         expression"
        PP.pp_expr expr
 
 let invalid_record_update_base_type base_type ~context_expr =
-  spec_error
+  spec_error_loc_of_expr context_expr
   @@ Format.asprintf "The base type %a in %a is not a record type"
        PP.pp_type_term base_type PP.pp_expr context_expr
 
-let missing_type_for_constant id =
-  spec_error @@ Format.asprintf "Missing type for constant '%s'" id
+let missing_type_for_constant loc id =
+  spec_error loc @@ Format.asprintf "Missing type for constant %s" id
 
-let missing_case_in_rule case_name relation_name case_path =
-  spec_error
+let missing_case_in_rule loc case_name relation_name case_path =
+  spec_error loc
   @@ Format.asprintf
-       "Case '%s' does not exist in rule for relation '%s' for path '%s'."
-       case_name relation_name case_path
+       "Case %s does not exist in rule for relation %s for path %s." case_name
+       relation_name case_path
diff --git a/asllib/aslspec/main.ml b/asllib/aslspec/main.ml
index 42f49b4afe..c3c7bc7556 100644
--- a/asllib/aslspec/main.ml
+++ b/asllib/aslspec/main.ml
@@ -112,6 +112,16 @@ let execute config =
   in
   ()
 
+let loc_to_gnu_error_format loc =
+  let open Lexing in
+  if loc == AST.missing_location then "Unknown location"
+  else
+    let start_pos = loc.AST.start_pos in
+    let filename = start_pos.pos_fname in
+    let line = start_pos.pos_lnum in
+    let column = start_pos.pos_cnum - start_pos.pos_bol + 1 in
+    Format.sprintf "%s:%d:%d" filename line column
+
 (** Main entry point. Runs aslspec for the command-line options. *)
 let () =
   let config = CLI.parse_args () in
@@ -127,8 +137,16 @@ let () =
       let error_type, msg =
         match error with
         | CLI.CLIError msg -> ("Usage Error", msg)
-        | Parsing.ParseError msg -> ("Syntax Error", msg)
-        | AST.SpecError msg -> ("Specification Error", msg)
+        | Parsing.ParseError { loc; msg } ->
+            let msg =
+              Format.sprintf "%s: %s" (loc_to_gnu_error_format loc) msg
+            in
+            ("Syntax Error", msg)
+        | AST.SpecError { loc; msg } ->
+            let msg =
+              Format.sprintf "%s: %s" (loc_to_gnu_error_format loc) msg
+            in
+            ("Specification Error", msg)
         | _ -> raise error
       in
       Format.eprintf "%s%s: %s%s\n" TextColor.red error_type msg
diff --git a/asllib/aslspec/parsing.ml b/asllib/aslspec/parsing.ml
index 440d6516d1..017418da5d 100644
--- a/asllib/aslspec/parsing.ml
+++ b/asllib/aslspec/parsing.ml
@@ -1,4 +1,4 @@
-exception ParseError of string
+exception ParseError of { loc : AST.source_location; msg : string }
 
 (** [pp_position] pretty-prints the position of the lexeme in the source file.
 *)
@@ -17,17 +17,27 @@ let parse_spec_from_lexbuf lexbuf filename =
       { pos_fname = filename; pos_lnum = 1; pos_bol = 0; pos_cnum = 0 }
   in
   try SpecParser.spec SpecLexer.token lexbuf with
-  | AST.SpecError msg ->
-      let msg = Format.asprintf "%s around %a" msg pp_position lexbuf in
-      raise (ParseError msg)
+  | AST.SpecError { loc; msg } -> raise (ParseError { loc; msg })
   | SpecParser.Error ->
       let msg = Format.asprintf "Syntax error at %a" pp_position lexbuf in
-      raise (ParseError msg)
+      let loc =
+        {
+          AST.start_pos = lexbuf.Lexing.lex_start_p;
+          end_pos = lexbuf.Lexing.lex_curr_p;
+        }
+      in
+      raise (ParseError { loc; msg })
   | SpecLexer.Error msg ->
       let msg =
         Format.asprintf "Lexical error at %a: %s" pp_position lexbuf msg
       in
-      raise (ParseError msg)
+      let loc =
+        {
+          AST.start_pos = lexbuf.Lexing.lex_start_p;
+          end_pos = lexbuf.Lexing.lex_curr_p;
+        }
+      in
+      raise (ParseError { loc; msg })
 
 let parse_spec_from_file filename =
   let file_channel = open_in_bin filename in
diff --git a/asllib/aslspec/parsing.mli b/asllib/aslspec/parsing.mli
index 99c4859a3e..39715073cb 100644
--- a/asllib/aslspec/parsing.mli
+++ b/asllib/aslspec/parsing.mli
@@ -1,6 +1,6 @@
 (** A module for parsing aslspec specifications. *)
 
-exception ParseError of string
+exception ParseError of { loc : AST.source_location; msg : string }
 
 val parse_spec_from_file : string -> AST.t
 (** [parse_spec_from_file filename] parses a specification from the file
diff --git a/asllib/aslspec/render.ml b/asllib/aslspec/render.ml
index 4cbbfecab4..dda2c580f0 100644
--- a/asllib/aslspec/render.ml
+++ b/asllib/aslspec/render.ml
@@ -89,13 +89,13 @@ module Make (S : SPEC_VALUE) = struct
   let rec pp_type_term fmt (type_term, layout) =
     let open Term in
     match type_term with
-    | Label name -> (
-        match get_short_circuit_macro name with
+    | Label { label } -> (
+        match get_short_circuit_macro label with
         | Some short_circuit_macro ->
             (* We like to render short-circuit expressions above type names that define them. *)
-            pp_overtext fmt pp_id_as_macro name pp_print_string
+            pp_overtext fmt pp_id_as_macro label pp_print_string
               short_circuit_macro
-        | None -> pp_id_as_macro fmt name)
+        | None -> pp_id_as_macro fmt label)
     | TypeOperator { op; term = sub_term } ->
         pp_type_operator fmt op pp_opt_named_type_term (sub_term, layout)
     | Tuple { label_opt = None; args = [ type_term ] } ->
@@ -113,11 +113,11 @@ module Make (S : SPEC_VALUE) = struct
         fprintf fmt "%a%a" pp_id_opt_as_macro label_opt
           (pp_fields pp_field_name pp_record_field_as_pair)
           (pp_record_fields_as_pairs, layout)
-    | ConstantsSet constant_names ->
+    | ConstantsSet { labels } ->
         let layout_contains_vertical = LayoutUtils.contains_vertical layout in
         pp_parenthesized Braces layout_contains_vertical
           (PP.pp_sep_list ~sep:", " pp_id_as_macro)
-          fmt constant_names
+          fmt labels
     | Function { from_type; to_type; total } ->
         let arrow_macro_name =
           if total then rightarrow_macro_name else partialto_macro_name
@@ -158,10 +158,11 @@ module Make (S : SPEC_VALUE) = struct
 
   (** Renders the mathematical formula for the relation signature [def] using
       [layout] and referencing elements in [S.spec]. *)
-  let pp_relation_math layout fmt { Relation.name; property; input; output } =
+  let pp_relation_math layout fmt
+      { Relation.name; property; input; output; loc } =
     (* Reuse the rendering for type terms. *)
     let input_as_labelled_tuple =
-      Term.Tuple { label_opt = Some name; args = input }
+      Term.Tuple { loc; label_opt = Some name; args = input }
     in
     let property_macro_name =
       match property with
@@ -295,16 +296,14 @@ module Make (S : SPEC_VALUE) = struct
 
   (** [pp_type_definition fmt def] renders the type definition [def] with the
       formatter [fmt]. *)
-  let pp_type_definition fmt ({ Type.name; variants } as def) =
+  let pp_type_definition fmt ({ Type.variants } as def) =
     match variants with
     | [] ->
         (* A basic type like `typedef A` *)
         pp_basic_type fmt def
-    | _ :: _ -> (
+    | _ :: _ ->
         (* A complex type like `typedef A = V1 | ... | Vk` *)
-        try pp_type_and_variants fmt (def, variants)
-        with SpecError e ->
-          stack_spec_error e (sprintf "While checking: %s" name))
+        pp_type_and_variants fmt (def, variants)
 
   (** [pp_type_definition_macro name fmt pp_value value] renders a wrapper
       around the rendering of a type definition for the type. The wrapper uses
@@ -393,17 +392,17 @@ module Make (S : SPEC_VALUE) = struct
     let short_circuit_macros_for_type_term type_term =
       let open Term in
       match type_term with
-      | Label id -> (
-          match Spec.defining_node_for_id S.spec id with
+      | Label { label } -> (
+          match Spec.defining_node_for_id S.spec label with
           | Node_Type typedef ->
               [
                 Type.short_circuit_macro typedef |> Option.get
                 (* get is ensured to succeed by [Spec.check_relations_outputs] *);
               ]
-          | Node_TypeVariant { term = Label id } -> [ get_or_gen_math_macro id ]
+          | Node_TypeVariant { term = Label { label } } ->
+              [ get_or_gen_math_macro label ]
           | _ -> assert false)
-      | ConstantsSet constant_names ->
-          List.map get_or_gen_math_macro constant_names
+      | ConstantsSet { labels } -> List.map get_or_gen_math_macro labels
       | _ -> assert false (* Checked in spec.ml *)
 
     (** [pp_expr fmt (expr, layout)] renders the expression [expr] with the
@@ -414,18 +413,18 @@ module Make (S : SPEC_VALUE) = struct
       | NamedExpr { expr = sub_expr; name; same_name } ->
           if same_name then pp_expr fmt (sub_expr, layout)
           else pp_overtext fmt pp_expr (sub_expr, layout) pp_var name
-      | Var name -> (
+      | Var { id } -> (
           (* Constants/labels should render via their macros.
           Plain variables should be rendered as text. *)
-          match Spec.defining_node_opt_for_id S.spec name with
+          match Spec.defining_node_opt_for_id S.spec id with
           | Some (Node_Constant _) | Some (Node_TypeVariant { term = Label _ })
             ->
-              pp_id_as_macro fmt name
+              pp_id_as_macro fmt id
           | Some (Node_Type _)
-          (* type names cannot be used as an expression so this case
-          corresponds to a variable that happens to share a name with a type. *)
+          (* type names cannot be used as expressions so this case
+             corresponds to a variable that happens to share a name with a type. *)
           | _ ->
-              pp_var fmt name)
+              pp_var fmt id)
       | Relation { name; is_operator; args } when is_operator ->
           (* operators often use custom macros, which might not mix well with arrays,
              so it's better to put them inside braces. *)
@@ -697,50 +696,52 @@ module Make (S : SPEC_VALUE) = struct
       match expr with
       | NamedExpr { expr = sub_expr } -> strip_names_from_expr sub_expr
       | Var name -> Var name
-      | ListIndex { list_var; index } ->
-          ListIndex { list_var; index = strip_names_from_expr index }
-      | Tuple { label_opt; args } ->
-          Tuple { label_opt; args = List.map strip_names_from_expr args }
-      | Record { label_opt; fields } ->
+      | ListIndex node ->
+          ListIndex { node with index = strip_names_from_expr node.index }
+      | Tuple node ->
+          Tuple { node with args = List.map strip_names_from_expr node.args }
+      | Record node ->
           Record
             {
-              label_opt;
+              node with
               fields =
                 List.map
                   (fun (field, field_expr) ->
                     (field, strip_names_from_expr field_expr))
-                  fields;
+                  node.fields;
             }
-      | RecordUpdate { record_expr; updates } ->
+      | RecordUpdate node ->
           RecordUpdate
             {
-              record_expr = strip_names_from_expr record_expr;
+              node with
+              record_expr = strip_names_from_expr node.record_expr;
               updates =
                 List.map
                   (fun (field, update_expr) ->
                     (field, strip_names_from_expr update_expr))
-                  updates;
+                  node.updates;
             }
-      | FieldAccess { base; field } ->
-          FieldAccess { base = strip_names_from_expr base; field }
-      | Map { lhs; args } ->
+      | FieldAccess node ->
+          FieldAccess { node with base = strip_names_from_expr node.base }
+      | Map node ->
           Map
             {
-              lhs = strip_names_from_expr lhs;
-              args = List.map strip_names_from_expr args;
+              node with
+              lhs = strip_names_from_expr node.lhs;
+              args = List.map strip_names_from_expr node.args;
             }
-      | Relation { name; is_operator; args } ->
-          Relation
-            { name; is_operator; args = List.map strip_names_from_expr args }
-      | Transition { lhs; rhs; short_circuit } ->
+      | Relation node ->
+          Relation { node with args = List.map strip_names_from_expr node.args }
+      | Transition node ->
           Transition
             {
-              lhs = strip_names_from_expr lhs;
-              rhs = strip_names_from_expr rhs;
-              short_circuit;
+              node with
+              lhs = strip_names_from_expr node.lhs;
+              rhs = strip_names_from_expr node.rhs;
+              short_circuit = node.short_circuit;
             }
-      | Indexed { index; list_var; body } ->
-          Indexed { index; list_var; body = strip_names_from_expr body }
+      | Indexed node ->
+          Indexed { node with body = strip_names_from_expr node.body }
       | UnresolvedApplication _ -> assert false
 
     (** [is_compound_expr expr] returns [true] if [expr] is considered compound
@@ -766,12 +767,12 @@ module Make (S : SPEC_VALUE) = struct
           let expr_prose = expr_to_prose stripped_sub_expr in
           Format.asprintf "%s (for the output variable %s)" expr_prose
             (var_to_prose name)
-      | Var name when String.equal name Spec.ignore_var ->
+      | Var { id } when String.equal id Spec.ignore_var ->
           "some arbitrary value"
-      | Var name -> (
+      | Var { id } -> (
           (* Constants/labels take their prose template from the prose_description attribute,
               while plain variables are rendered as text. *)
-          match Spec.defining_node_opt_for_id S.spec name with
+          match Spec.defining_node_opt_for_id S.spec id with
           | Some (Node_Constant def) ->
               let prose = Constant.prose_description def in
               prose_or_math prose expr
@@ -782,7 +783,7 @@ module Make (S : SPEC_VALUE) = struct
           (* type names cannot be used as an expression so this case
           corresponds to a variable that happens to share a name with a type. *)
           | _ ->
-              var_to_prose name)
+              var_to_prose id)
       | ListIndex { list_var; index = Var _ as index } ->
           (* An optimization of the prose for variable indices. *)
           Format.asprintf "%s[%s]" (var_to_prose list_var) (expr_to_prose index)
@@ -868,7 +869,9 @@ module Make (S : SPEC_VALUE) = struct
                 (List.map fst fields)
             in
             List.map
-              (fun field -> (field, Expr.Var Spec.ignore_var))
+              (fun field ->
+                (* Source locations are irrelevant during rendering. *)
+                (field, Expr.make_var missing_location Spec.ignore_var))
               unspecified_fields
           in
           let field_to_prose =
diff --git a/asllib/aslspec/spec.ml b/asllib/aslspec/spec.ml
index 5119801515..4c3adc7c9e 100644
--- a/asllib/aslspec/spec.ml
+++ b/asllib/aslspec/spec.ml
@@ -33,6 +33,14 @@ let definition_node_name = function
       name
   | Node_TypeVariant def -> Option.get (variant_to_label_opt def)
 
+let loc_of_definition_node = function
+  | Node_Type { Type.loc }
+  | Node_Relation { Relation.loc }
+  | Node_Constant { Constant.loc }
+  | Node_TypeVariant { TypeVariant.loc }
+  | Node_RecordField { Term.loc } ->
+      loc
+
 (** [pp_definition_node fmt node] pretty-prints the definition node [node]. *)
 let pp_definition_node fmt =
   let open PP in
@@ -103,11 +111,12 @@ let is_type_name id_to_defining_node id =
   | Some (Node_Type _) -> true
   | _ -> false
 
-(** [check_is_constant id_to_defining_node id] raises an error if [id] is not
-    defined as a constant directly or as a type variant with a label. *)
-let check_is_constant id_to_defining_node id =
+(** [check_is_constant context_term id_to_defining_node id] raises an error if
+    [id] is not defined as a constant directly or as a type variant with a
+    label. [context_term] is used for error reporting. *)
+let check_is_constant context_term id_to_defining_node id =
   if is_constant id_to_defining_node id then ()
-  else Error.non_constant_used_as_constant_set id
+  else Error.non_constant_used_as_constant_set context_term id
 
 (** Utility functions for handling layouts. *)
 module Layout = struct
@@ -117,13 +126,13 @@ module Layout = struct
       [ (r(a,b,c), (A,B,C)) ]. That is, a pair where the first component is a
       labelled tuple with the relation name and arguments and the second
       component is a tuple with all output terms. *)
-  let relation_to_tuple { Relation.name; input; output } =
+  let relation_to_tuple { Relation.name; input; output; loc } =
     let opt_named_output_terms = List.map (fun term -> (None, term)) output in
     let open Term in
-    make_tuple
+    make_tuple loc
       [
-        (None, make_labelled_tuple name input);
-        (None, make_tuple opt_named_output_terms);
+        (None, make_labelled_tuple loc name input);
+        (None, make_tuple loc opt_named_output_terms);
       ]
 
   let rec for_type_term term =
@@ -141,7 +150,8 @@ module Layout = struct
           in
           Vertical layout_per_field
         else Unspecified
-    | ConstantsSet names -> Horizontal (List.map (fun _ -> Unspecified) names)
+    | ConstantsSet { labels } ->
+        Horizontal (List.map (fun _ -> Unspecified) labels)
     | Function { from_type = _, from_term; to_type = _, to_term; _ } ->
         Horizontal [ for_type_term from_term; for_type_term to_term ]
 
@@ -205,9 +215,10 @@ let make_id_to_definition_node definition_nodes =
   List.fold_left
     (fun acc_map node ->
       let name = definition_node_name node in
+      let loc = loc_of_definition_node node in
       StringMap.update name
         (function
-          | Some _ -> Error.duplicate_definition name | None -> Some node)
+          | Some _ -> Error.duplicate_definition loc name | None -> Some node)
         acc_map)
     StringMap.empty definition_nodes
 
@@ -220,7 +231,7 @@ let make_variant_id_to_containing_type ast =
       List.fold_left
         (fun acc_map { TypeVariant.term } ->
           match term with
-          | Term.Label label
+          | Term.Label { label }
           | Term.Tuple { label_opt = Some label }
           | Term.Record { label_opt = Some label }
           (* Only labels, labelled tuples, and labelled records have
@@ -315,7 +326,7 @@ let defining_node_opt_for_id self id =
 let defining_node_for_id self id =
   match defining_node_opt_for_id self id with
   | Some def -> def
-  | None -> Error.undefined_element id
+  | None -> failwith ("Undefined element: " ^ id)
 
 let relation_for_id self id =
   match defining_node_for_id self id with
@@ -345,10 +356,10 @@ let elements self = self.ast
     relation definition, the parameters of the relation definition are added. *)
 let symbol_table_for_id id_to_defining_node id =
   match StringMap.find_opt id id_to_defining_node with
-  | Some (Node_Relation { Relation.parameters }) ->
+  | Some (Node_Relation { Relation.parameters; loc }) ->
       List.fold_left
         (fun curr_table param ->
-          let type_for_param = Type.make TypeKind_Generic param [] [] in
+          let type_for_param = Type.make loc TypeKind_Generic param [] [] in
           StringMap.add param (Node_Type type_for_param) curr_table)
         id_to_defining_node parameters
   | _ -> id_to_defining_node
@@ -380,69 +391,74 @@ module ResolveApplicationExpr = struct
     let open Expr in
     match expr with
     | Var _ | FieldAccess _ -> expr
-    | Tuple { label_opt; args } ->
-        let resolved_args = List.map resolve_in_context args in
-        Tuple { label_opt; args = resolved_args }
-    | Relation { is_operator = true; name; args } ->
+    | Tuple node ->
+        let resolved_args = List.map resolve_in_context node.args in
+        Tuple { node with args = resolved_args }
+    | Relation ({ is_operator = true; args; _ } as node) ->
         let resolved_args = List.map resolve_in_context args in
-        Relation { is_operator = true; name; args = resolved_args }
-    | ListIndex { list_var; index } ->
-        let resolved_index = resolve_in_context index in
-        ListIndex { list_var; index = resolved_index }
-    | Record { label_opt; fields } ->
+        Relation { node with args = resolved_args }
+    | ListIndex node ->
+        let resolved_index = resolve_in_context node.index in
+        ListIndex { node with index = resolved_index }
+    | Record node ->
         let resolved_fields =
           List.map
             (fun (field_name, field_expr) ->
               (field_name, resolve_in_context field_expr))
-            fields
+            node.fields
         in
-        Record { label_opt; fields = resolved_fields }
-    | RecordUpdate { record_expr; updates } ->
-        let resolved_record_expr = resolve_in_context record_expr in
+        Record { node with fields = resolved_fields }
+    | RecordUpdate node ->
+        let resolved_record_expr = resolve_in_context node.record_expr in
         let resolved_updates =
           List.map
             (fun (field_name, field_expr) ->
               (field_name, resolve_in_context field_expr))
-            updates
+            node.updates
         in
         RecordUpdate
-          { record_expr = resolved_record_expr; updates = resolved_updates }
-    | UnresolvedApplication { lhs; args } -> (
+          {
+            node with
+            record_expr = resolved_record_expr;
+            updates = resolved_updates;
+          }
+    | UnresolvedApplication { lhs; args; loc } -> (
         let resolved_args = List.map resolve_in_context args in
         match lhs with
-        | Var id -> (
+        | Var { loc; id } -> (
             match StringMap.find_opt id id_to_defining_node with
-            | Some (Node_Relation { Relation.is_operator; name }) ->
-                Relation { is_operator; name; args = resolved_args }
+            | Some (Node_Relation { Relation.is_operator; name; _ }) ->
+                Relation { loc; is_operator; name; args = resolved_args }
             | Some (Node_TypeVariant { term = Term.Tuple { label_opt } })
             | Some
                 (Node_Constant { opt_type = Some (Term.Tuple { label_opt }) })
               ->
-                Tuple { label_opt; args = resolved_args }
+                Tuple { loc; label_opt; args = resolved_args }
             | Some (Node_Constant { Constant.name })
             | Some (Node_Type { Type.name }) ->
                 Error.invalid_application_of_symbol_in_expr name expr
             | Some (Node_RecordField _) | Some (Node_TypeVariant _) | None ->
                 Error.illegal_lhs_application expr)
-        | _ -> Map { lhs = resolve_in_context lhs; args = resolved_args })
-    | Transition { lhs; rhs; short_circuit } ->
-        let resolved_lhs = resolve_in_context lhs in
-        let resolved_rhs = resolve_in_context rhs in
+        | _ -> Map { loc; lhs = resolve_in_context lhs; args = resolved_args })
+    | Transition node ->
+        let resolved_lhs = resolve_in_context node.lhs in
+        let resolved_rhs = resolve_in_context node.rhs in
         let resolved_short_circuit =
-          Option.map (List.map resolve_in_context) short_circuit
+          Option.map (List.map resolve_in_context) node.short_circuit
         in
         Transition
           {
+            node with
             lhs = resolved_lhs;
             rhs = resolved_rhs;
             short_circuit = resolved_short_circuit;
           }
-    | Indexed ({ body : Expr.t } as indexed_expr) ->
-        let resolved_body = resolve_in_context body in
-        Indexed { indexed_expr with body = resolved_body }
-    | NamedExpr ({ expr } as named_expr) ->
-        let resolved_expr = resolve_in_context expr in
-        NamedExpr { named_expr with expr = resolved_expr }
+    | Indexed node ->
+        let resolved_body = resolve_in_context node.body in
+        Indexed { node with body = resolved_body }
+    | NamedExpr node ->
+        let resolved_expr = resolve_in_context node.expr in
+        NamedExpr { node with expr = resolved_expr }
     | Relation _ | Map _ ->
         Format.kasprintf failwith "unexpected resolved expression: %a"
           PP.pp_expr expr
@@ -541,6 +557,7 @@ module ResolveRules = struct
           if is_output then
             Transition
               {
+                loc = Expr.loc_of expr;
                 lhs = conclusion_lhs;
                 rhs = expr;
                 short_circuit = Some [];
@@ -567,14 +584,14 @@ module ResolveRules = struct
   (** [lhs_of_conclusion def] returns an expression representing the LHS of the
       conclusion judgment for the relation definition [def]. This function
       assumes [relation_named_arguments_if_exists_rule] has been called. *)
-  let lhs_of_conclusion { Relation.name; is_operator; input } =
+  let lhs_of_conclusion { Relation.name; is_operator; input; loc } =
     (* Converts an optionally-named type term into a relation argument expression. *)
     let rec arg_of opt_named_term =
       match opt_named_term with
-      | Some name, _ -> Expr.Var name
-      | None, Term.Tuple { label_opt; args } ->
+      | Some id, term -> Expr.make_var (Term.loc_of term) id
+      | None, (Term.Tuple { label_opt; args } as term) ->
           let args = List.map arg_of args in
-          Expr.make_opt_labelled_tuple label_opt args
+          Expr.make_opt_labelled_tuple (Term.loc_of term) label_opt args
       | ( None,
           ( Term.Label _ | Term.Record _ | Term.TypeOperator _ | Term.Function _
           | Term.ConstantsSet _ ) ) ->
@@ -582,7 +599,7 @@ module ResolveRules = struct
             PP.pp_type_term (snd opt_named_term)
     in
     let named_args = List.map arg_of input in
-    Expr.Relation { name; is_operator; args = named_args }
+    Expr.Relation { loc; name; is_operator; args = named_args }
 
   (** In text, a list of [case] elements without non-[case] elements in between
       them are considered to be a single case element with multiple cases.
@@ -757,7 +774,7 @@ module ExpandRules = struct
       [ { name_opt = None; judgments = [] } ]
 end
 
-let filter_rule_for_path { Relation.name; rule_opt } path_str =
+let filter_rule_for_path { Relation.name; rule_opt; loc } path_str =
   assert (Option.is_some rule_opt);
   let open Rule in
   (* If path_str is empty, path should be empty as well. *)
@@ -765,7 +782,7 @@ let filter_rule_for_path { Relation.name; rule_opt } path_str =
   let rec filter_rule_elements rule_elements path =
     match (rule_elements, path) with
     | _, [] -> rule_elements
-    | [], _ -> Error.missing_case_in_rule path_str name path_str
+    | [], _ -> Error.missing_case_in_rule loc path_str name path_str
     | Rule.Judgment judgment :: rest, _ ->
         Rule.Judgment judgment :: filter_rule_elements rest path
     | Rule.Cases cases :: rest, case_name :: path_tail ->
@@ -773,7 +790,7 @@ let filter_rule_for_path { Relation.name; rule_opt } path_str =
           let find_case { name } = String.equal name case_name in
           match List.find_opt find_case cases with
           | Some { elements } -> elements
-          | None -> Error.missing_case_in_rule case_name name path_str
+          | None -> Error.missing_case_in_rule loc case_name name path_str
         in
         let filtered_case_elements =
           filter_rule_elements case_elements path_tail
@@ -806,10 +823,13 @@ module Check = struct
           List.iter2
             (fun { Term.term } cell -> check_layout term cell)
             fields cells
-    | ConstantsSet names, (Horizontal cells | Vertical cells) ->
-        if List.compare_lengths names cells <> 0 then
+    | ConstantsSet { loc; labels }, (Horizontal cells | Vertical cells) ->
+        if List.compare_lengths labels cells <> 0 then
           Error.bad_layout term layout ~consistent_layout
-        else List.iter2 (fun _ cell -> check_layout (Label "") cell) names cells
+        else
+          List.iter2
+            (fun _ cell -> check_layout (Label { loc; label = "" }) cell)
+            labels cells
     | ( Function { from_type = _, from_term; to_type = _, to_term; _ },
         (Horizontal cells | Vertical cells) ) ->
         if List.length cells <> 2 then
@@ -822,12 +842,13 @@ module Check = struct
       nodes in [spec] are structurally consistent with their type terms. *)
   let check_math_layout spec =
     let check_math_layout_for_definition_node node =
+      let loc = loc_of_definition_node node in
       let open Layout in
       match node with
       | Node_Type { Type.name } ->
-          check_layout (Label name) (math_layout_for_node node)
+          check_layout (Label { loc; label = name }) (math_layout_for_node node)
       | Node_Constant { Constant.name } ->
-          check_layout (Label name) (math_layout_for_node node)
+          check_layout (Label { loc; label = name }) (math_layout_for_node node)
       | Node_TypeVariant { TypeVariant.term } ->
           check_layout term (math_layout_for_node node)
       | Node_Relation def ->
@@ -841,7 +862,7 @@ module Check = struct
   let rec referenced_ids =
     let open Term in
     function
-    | Label id -> [ id ]
+    | Label { label } -> [ label ]
     | TypeOperator { term = _, t } -> referenced_ids t
     | Tuple { label_opt; args } -> (
         let component_ids =
@@ -858,7 +879,7 @@ module Check = struct
         match label_opt with
         | None -> fields_ids
         | Some label -> label :: fields_ids)
-    | ConstantsSet constant_names -> constant_names
+    | ConstantsSet { labels } -> labels
     | Function { from_type = _, from_term; to_type = _, to_term } ->
         referenced_ids from_term @ referenced_ids to_term
 
@@ -869,7 +890,9 @@ module Check = struct
       let referenced_ids_for_list = Utils.list_concat_map referenced_ids in
       let ids_referenced_by_elem =
         match elem with
-        | Elem_Constant _ -> []
+        | Elem_Constant { Constant.opt_type = Some c_term } ->
+            referenced_ids c_term
+        | Elem_Constant { Constant.opt_type = None } -> []
         | Elem_Type { Type.variants } ->
             referenced_ids_for_list
               (List.map (fun { TypeVariant.term } -> term) variants)
@@ -891,18 +914,18 @@ module Check = struct
       List.iter
         (fun id ->
           if not (StringMap.mem id id_to_defining_node) then
-            Error.undefined_reference id elem_name)
+            Error.undefined_reference missing_location id elem_name)
         ids_referenced_by_elem
     in
     List.iter (check_no_undefined_ids_in_elem id_to_defining_node) ast
 
-  (** [check_relations_outputs elems id_to_defining_node] checks that, for each
+  (** [check_relation_outputs elems id_to_defining_node] checks that, for each
       relation in [elems], the first output type term is arbitrary, and that all
       type terms following it are either type names or sets of constants.
       Furthermore, it checks that all type names used as alternative output type
       terms reference types with the [short_circuit_macro] attribute defined. If
       not, raises a [SpecError] describing the issue. *)
-  let check_relations_outputs { ast; id_to_defining_node } =
+  let check_relation_outputs { ast; id_to_defining_node } =
     let relations_defs =
       List.filter_map (function Elem_Relation def -> Some def | _ -> None) ast
     in
@@ -911,11 +934,12 @@ module Check = struct
       List.iter
         (fun term ->
           match term with
-          | Term.Label id -> (
-              match StringMap.find id id_to_defining_node with
+          | Term.Label { label } -> (
+              match StringMap.find label id_to_defining_node with
               | Node_Type typedef -> (
                   match Type.short_circuit_macro typedef with
-                  | None -> Error.missing_short_circuit_attribute name term id
+                  | None ->
+                      Error.missing_short_circuit_attribute name term label
                   | Some _ -> ())
               | _ -> Error.not_type_name_error name term)
           | Term.ConstantsSet _ -> ()
@@ -970,18 +994,14 @@ module Check = struct
       in
       let extra_vars = find_extra_vars_in_template template template_vars in
       if Utils.list_is_empty extra_vars then ()
-      else Error.unmatched_variables_in_template template extra_vars
+      else
+        Error.unmatched_variables_in_template missing_location template
+          extra_vars
 
     let rec check_prose_template_for_definition_node defining_node =
       let prose_description = prose_description_for_node defining_node in
       let vars = vars_of_node defining_node in
-      let () =
-        try check_extra_vars_in_prose_template prose_description vars
-        with SpecError e ->
-          stack_spec_error e
-            (Format.asprintf "While checking: %a" pp_definition_node
-               defining_node)
-      in
+      let () = check_extra_vars_in_prose_template prose_description vars in
       match defining_node with
       | Node_TypeVariant _ | Node_Constant _ | Node_RecordField _ -> ()
       | Node_Type { variants } ->
@@ -998,24 +1018,28 @@ module Check = struct
           let () =
             try
               check_extra_vars_in_prose_template prose_transition input_arg_vars
-            with SpecError e ->
-              stack_spec_error e
-                (Format.asprintf
-                   "While checking prose_transition for: %s. Recall that the \
-                    variables available for use in the prose_transition \
-                    template are only those of the input arguments. In this \
-                    case, those variables are: %s.\n\
-                    Hint: to refer to the outcomes you may use `|`"
-                   (definition_node_name defining_node)
-                   (String.concat ", " input_arg_vars))
+            with SpecError { loc; msg } ->
+              let extra_msg =
+                Format.asprintf
+                  "While checking prose_transition for: %s. Recall that the \
+                   variables available for use in the prose_transition \
+                   template are only those of the input arguments. In this \
+                   case, those variables are: %s.\n\
+                   Hint: to refer to the outcomes you may use `|`"
+                  (definition_node_name defining_node)
+                  (String.concat ", " input_arg_vars)
+              in
+              stack_spec_error loc msg extra_msg
           in
           let prose_application = Relation.prose_application def in
           try
             check_extra_vars_in_prose_template prose_application input_arg_vars
-          with SpecError e ->
-            stack_spec_error e
-              (Format.asprintf "While checking prose_application for: %s."
-                 (definition_node_name defining_node)))
+          with SpecError { loc; msg } ->
+            let extra_msg =
+              Format.asprintf "While checking prose_application for: %s."
+                (definition_node_name defining_node)
+            in
+            stack_spec_error loc msg extra_msg)
 
     let check spec =
       iter_defined_nodes spec check_prose_template_for_definition_node
@@ -1098,8 +1122,8 @@ module Check = struct
     let rec reduce_single_variant_type spec term =
       let open Term in
       match term with
-      | Label id -> (
-          match defining_node_opt_for_id spec id with
+      | Label { label } -> (
+          match defining_node_opt_for_id spec label with
           | Some
               (Node_Type
                  { Type.variants = [ { TypeVariant.term = variant_term } ]; _ })
@@ -1175,35 +1199,36 @@ module Check = struct
       let super = reduce_term spec super in
       let result =
         match (sub, super) with
-        | Label sub_id, _ when is_builtin_constant sub_id spec.bottom_constant
-          ->
+        | Label { label = sub_id }, _
+          when is_builtin_constant sub_id spec.bottom_constant ->
             (* The bottom constant is a subset of every type. *)
             true
-        | Label sub_id, Label super_id
-          when is_builtin_type sub_id spec.n_type
-               && is_builtin_type super_id spec.z_type ->
+        | Label { label = sub_label }, Label { label = super_label }
+          when is_builtin_type sub_label spec.n_type
+               && is_builtin_type super_label spec.z_type ->
             true
-        | Label sub_label, TypeOperator { op = List0 | List1 }
+        | Label { label = sub_label }, TypeOperator { op = List0 | List1 }
           when is_builtin_constant sub_label spec.empty_list ->
             (* The empty list is a subset of every list, since
                empty_list is universally quantified over all element types.
             *)
             true
-        | Label sub_label, TypeOperator { op = Powerset | Powerset_Finite }
+        | ( Label { label = sub_label },
+            TypeOperator { op = Powerset | Powerset_Finite } )
           when is_builtin_constant sub_label spec.empty_set ->
             (* The empty set is a subset of every set. *)
             true
-        | ( Label sub_label,
+        | ( Label { label = sub_label },
             TypeOperator { op = Option | Powerset | Powerset_Finite } )
           when is_builtin_constant sub_label spec.none_constant ->
             (* None is a subset of Option and also every set. *)
             true
-        | Label sub_label, ConstantsSet super_names ->
-            List.exists (String.equal sub_label) super_names
-        | _, Label super_label ->
+        | Label { label = sub_label }, ConstantsSet { labels = super_labels } ->
+            List.exists (String.equal sub_label) super_labels
+        | _, Label { label = super_label } ->
             let sub_is_label_case =
               match sub with
-              | Label sub_label ->
+              | Label { label = sub_label } ->
                   String.equal sub_label super_label
                   ||
                   (* The case where [sub_label] is a type name,
@@ -1252,8 +1277,9 @@ module Check = struct
             ((not sub_total) || super_total) (* sub_total implies super_total *)
             && subsumed_rec spec expanded_types super_from_term sub_from_term
             && subsumed_rec spec expanded_types sub_to_term super_to_term
-        | ConstantsSet sub_names, ConstantsSet super_names ->
-            List.for_all (fun name -> List.mem name super_names) sub_names
+        | ( ConstantsSet { labels = sub_labels },
+            ConstantsSet { labels = super_labels } ) ->
+            List.for_all (fun name -> List.mem name super_labels) sub_labels
         | _ ->
             (* false is safely conservative. *)
             false
@@ -1427,9 +1453,9 @@ module Check = struct
       | Function { from_type = _, from_term; to_type = _, to_term } ->
           check_well_formed id_to_defining_node from_term;
           check_well_formed id_to_defining_node to_term
-      | ConstantsSet labels ->
-          List.iter (check_is_constant id_to_defining_node) labels
-      | Label label -> (
+      | ConstantsSet { labels } ->
+          List.iter (check_is_constant term id_to_defining_node) labels
+      | Label { label } -> (
           let variant_def = StringMap.find label id_to_defining_node in
           match variant_def with
           | Node_Type _ | Node_TypeVariant { TypeVariant.term = Label _ } -> ()
@@ -1445,35 +1471,31 @@ module Check = struct
     let check ({ ast; id_to_defining_node } as spec) =
       List.iter
         (fun elem ->
-          try
-            match elem with
-            | Elem_RenderTypes _ | Elem_RenderRule _
-            | Elem_Constant { opt_type = None } ->
-                ()
-            | Elem_Constant { opt_type = Some type_term } ->
-                check_well_typed spec type_term
-            | Elem_Relation { name; input; output } ->
-                (* The check must be made in a symbol table that contains the relation parameters. *)
-                let spec =
-                  {
-                    spec with
-                    id_to_defining_node =
-                      symbol_table_for_id id_to_defining_node name;
-                  }
-                in
-                List.iter (fun (_, term) -> check_well_typed spec term) input;
-                List.iter (check_well_typed spec) output
-            | Elem_Type { Type.variants; _ } ->
-                List.iter
-                  (fun { TypeVariant.term } ->
-                    match term with
-                    | Label _ ->
-                        () (* A constant label definition is well-formed. *)
-                    | _ -> check_well_typed spec term)
-                  variants
-          with SpecError e ->
-            stack_spec_error e
-              (Format.asprintf "While checking: %s" (elem_name elem)))
+          match elem with
+          | Elem_RenderTypes _ | Elem_RenderRule _
+          | Elem_Constant { opt_type = None } ->
+              ()
+          | Elem_Constant { opt_type = Some type_term } ->
+              check_well_typed spec type_term
+          | Elem_Relation { name; input; output } ->
+              (* The check must be made in a symbol table that contains the relation parameters. *)
+              let spec =
+                {
+                  spec with
+                  id_to_defining_node =
+                    symbol_table_for_id id_to_defining_node name;
+                }
+              in
+              List.iter (fun (_, term) -> check_well_typed spec term) input;
+              List.iter (check_well_typed spec) output
+          | Elem_Type { Type.variants; _ } ->
+              List.iter
+                (fun { TypeVariant.term } ->
+                  match term with
+                  | Label _ ->
+                      () (* A constant label definition is well-formed. *)
+                  | _ -> check_well_typed spec term)
+                variants)
         ast
   end
 
@@ -1598,7 +1620,7 @@ module Check = struct
       in
       let use_def =
         match expr with
-        | Var id ->
+        | Var { id } ->
             vars_of_identifiers spec.id_to_defining_node [ id ]
             |> check_and_add_for_expr mode use_def
         | FieldAccess { base } -> (
@@ -1646,7 +1668,11 @@ module Check = struct
             let use_def = update_use_def_for_expr Use spec use_def lhs in
             update_use_def_for_expr Def spec use_def rhs
         | Relation
-            { is_operator = true; name; args = Var bound_var :: tail_args }
+            {
+              is_operator = true;
+              name;
+              args = Var { id = bound_var } :: tail_args;
+            }
           when is_quantifying_operator spec name ->
             update_use_def_with_bound_variable mode spec use_def tail_args
               ~context_expr:expr ~bound_var
@@ -1741,7 +1767,8 @@ module Check = struct
 
     (** [type_term_for_typedef def] returns the type term corresponding to the
         given type definition. *)
-    let type_term_for_typedef def = Term.Label def.Type.name
+    let type_term_for_typedef def =
+      Term.Label { loc = def.Type.loc; label = def.Type.name }
 
     (** [type_of_id spec type_env id] returns the type of [id] using [spec] to
         lookup the defining node for [id] if needed, and using [type_env] as a
@@ -1757,8 +1784,8 @@ module Check = struct
       match defining_node_opt_for_id spec id with
       | Some (Node_TypeVariant { TypeVariant.term }) -> term
       | Some (Node_Constant { Constant.opt_type = Some type_term }) -> type_term
-      | Some (Node_Constant { Constant.opt_type = None }) ->
-          Error.missing_type_for_constant id
+      | Some (Node_Constant { Constant.opt_type = None; loc }) ->
+          Error.missing_type_for_constant loc id
       | Some (Node_Relation _)
       | Some (Node_RecordField _)
       | Some (Node_Type _)
@@ -1808,12 +1835,12 @@ module Check = struct
             unify_structural_terms spec term1 term2
           in
           let get_variant_label = function
-            | Label id when StringMap.mem id spec.variant_id_to_containing_type
-              ->
-                Some id
-            | Tuple { label_opt = Some id; _ }
-            | Record { label_opt = Some id; _ } ->
-                Some id
+            | Label { label }
+              when StringMap.mem label spec.variant_id_to_containing_type ->
+                Some label
+            | Tuple { label_opt = Some label; _ }
+            | Record { label_opt = Some label; _ } ->
+                Some label
             | _ -> None
           in
           match structural_unification_result_opt with
@@ -1828,7 +1855,7 @@ module Check = struct
                     StringMap.find label2 spec.variant_id_to_containing_type
                   in
                   if String.equal container1 container2 then
-                    Some (Label container1)
+                    Some (Label { loc = loc_of term2; label = container1 })
                   else None
               | _ -> None)
       in
@@ -1845,11 +1872,13 @@ module Check = struct
         same internal structure. If successful, returns the unified term.
         Otherwise, returns [None]. *)
     and unify_structural_terms spec term1 term2 =
+      let loc = Term.loc_of term1 in
       if term1 == term2 then Some term1
       else
         let open Term in
         match (term1, term2) with
-        | Label id1, Label id2 when String.equal id1 id2 ->
+        | Label { label = id1 }, Label { label = id2 } when String.equal id1 id2
+          ->
             (* Here, we assume that the labels are not type names. *)
             Some term1
         | ( TypeOperator { op = op1; term = _, arg_term1 },
@@ -1858,7 +1887,8 @@ module Check = struct
             match unify_terms spec arg_term1 arg_term2 with
             | Some unified_arg_term ->
                 Some
-                  (TypeOperator { op = op1; term = (None, unified_arg_term) })
+                  (TypeOperator
+                     { loc; op = op1; term = (None, unified_arg_term) })
             | None -> None)
         | ( Tuple { label_opt = label1_opt; args = args1 },
             Tuple { label_opt = label2_opt; args = args2 } )
@@ -1869,6 +1899,7 @@ module Check = struct
                 Some
                   (Tuple
                      {
+                       loc;
                        label_opt = label1_opt;
                        args =
                          List.map2
@@ -1894,6 +1925,7 @@ module Check = struct
                 Some
                   (Record
                      {
+                       loc;
                        label_opt = label1_opt;
                        fields =
                          List.map2
@@ -1941,8 +1973,8 @@ module Check = struct
           @raise [SpecError]
             if [parameter_type] cannot be unified with an existing type for
             [parameter_name]. *)
-      let unify_parameter_type spec ~relation_name parameter_name parameter_type
-          type_env =
+      let unify_parameter_type spec loc ~relation_name parameter_name
+          parameter_type type_env =
         StringMap.update parameter_name
           (function
             | None -> Some parameter_type
@@ -1950,7 +1982,7 @@ module Check = struct
                 match unify_terms spec parameter_type existing_type with
                 | Some unified_type -> Some unified_type
                 | None ->
-                    Error.parameter_type_unification_failure ~relation_name
+                    Error.parameter_type_unification_failure loc ~relation_name
                       parameter_name existing_type parameter_type))
           type_env
 
@@ -1972,9 +2004,9 @@ module Check = struct
         let arg_type = reduce_term spec arg_type in
         let open Term in
         match (formal_type, arg_type) with
-        | Label formal_id, _ ->
+        | Label { label = formal_id; loc }, _ ->
             if is_parameter formal_id then
-              unify_parameter_type spec ~relation_name formal_id arg_type
+              unify_parameter_type spec loc ~relation_name formal_id arg_type
                 type_env
             else type_env
         | Tuple { args = formal_args }, Tuple { args = actual_args } ->
@@ -2036,19 +2068,19 @@ module Check = struct
       let rec substitute_type_parameters term parameter_env =
         let open Term in
         match term with
-        | Label id -> (
-            match StringMap.find_opt id parameter_env with
+        | Label { label } -> (
+            match StringMap.find_opt label parameter_env with
             | Some substituted_type -> substituted_type
             | None -> term)
-        | Tuple { label_opt; args } ->
+        | Tuple ({ args } as node) ->
             let substituted_args =
               List.map
                 (fun (name, sub_term) ->
                   (name, substitute_type_parameters sub_term parameter_env))
                 args
             in
-            Tuple { label_opt; args = substituted_args }
-        | Record { label_opt; fields } ->
+            Tuple { node with args = substituted_args }
+        | Record ({ fields } as node) ->
             let substituted_fields =
               List.map
                 (fun ({ term = field_term } as field) ->
@@ -2058,13 +2090,10 @@ module Check = struct
                   })
                 fields
             in
-            Record { label_opt; fields = substituted_fields }
+            Record { node with fields = substituted_fields }
         | Function
-            {
-              from_type = from_name, from_term;
-              to_type = to_name, to_term;
-              total;
-            } ->
+            ({ from_type = from_name, from_term; to_type = to_name, to_term } as
+             node) ->
             let substituted_from_term =
               substitute_type_parameters from_term parameter_env
             in
@@ -2073,15 +2102,16 @@ module Check = struct
             in
             Function
               {
+                node with
                 from_type = (from_name, substituted_from_term);
                 to_type = (to_name, substituted_to_term);
-                total;
               }
-        | TypeOperator { op; term = term_name, inner_term } ->
+        | TypeOperator ({ term = term_name, inner_term } as node) ->
             let substituted_inner_term =
               substitute_type_parameters inner_term parameter_env
             in
-            TypeOperator { op; term = (term_name, substituted_inner_term) }
+            TypeOperator
+              { node with term = (term_name, substituted_inner_term) }
         | ConstantsSet _ -> term
 
       (** [make_operator_formals_for_actual_num_of_args spec operator_name
@@ -2217,10 +2247,11 @@ module Check = struct
         let rec list_structured_terms_for_one_term spec term =
           let open Term in
           match term with
-          | Label id
-          | Term.Tuple { label_opt = None; args = [ (_, Term.Label id) ] }
-            when is_type_name spec.id_to_defining_node id -> (
-              match defining_node_for_id spec id with
+          | Label { label }
+          | Term.Tuple
+              { label_opt = None; args = [ (_, Term.Label { label }) ] }
+            when is_type_name spec.id_to_defining_node label -> (
+              match defining_node_for_id spec label with
               | Node_Type { Type.variants } ->
                   Utils.list_concat_map
                     (fun { TypeVariant.term = variant } ->
@@ -2325,8 +2356,8 @@ module Check = struct
       match base_type with
       | Term.Record { fields; _ } ->
           List.exists (fun { Term.name } -> String.equal name field_name) fields
-      | Term.Label id -> (
-          match defining_node_opt_for_id spec id with
+      | Term.Label { label } -> (
+          match defining_node_opt_for_id spec label with
           | Some (Node_Type { Type.variants; _ }) ->
               List.for_all
                 (fun { TypeVariant.term } ->
@@ -2344,10 +2375,10 @@ module Check = struct
       let open Expr in
       let t, tenv =
         match expr with
-        | Var id when is_ignore_var id ->
+        | Var { id } when is_ignore_var id ->
             (* If we type '_' with the bottom type, it will be subsumed by any other type. *)
             (spec.bottom_term, type_env)
-        | Var id ->
+        | Var { id } ->
             let id_type = type_of_id ~context_expr:expr spec type_env id in
             (id_type, type_env)
         | FieldAccess { base; field } ->
@@ -2379,7 +2410,7 @@ module Check = struct
                 (type_term_for_typedef spec.n_type)
             then (elem_type, type_env)
             else Error.invalid_list_index_type index_type ~context_expr:expr
-        | Record { label_opt; fields } ->
+        | Record { loc; label_opt; fields } ->
             (* All arguments must typecheck, and if the record is labelled,
                the inferred record type must be subsumed by the labelled record type. *)
             let fields =
@@ -2395,10 +2426,11 @@ module Check = struct
               let record_fields =
                 List.map2
                   (fun field_name field_type ->
-                    Term.make_record_field (field_name, field_type) [])
+                    let loc = Term.loc_of field_type in
+                    Term.make_record_field loc (field_name, field_type) [])
                   field_names field_types
               in
-              Term.Record { label_opt; fields = record_fields }
+              Term.Record { loc; label_opt; fields = record_fields }
             in
             let { TypeVariant.term = declared_type } =
               record_variant_for_expr spec expr
@@ -2448,7 +2480,7 @@ module Check = struct
                   ~context_expr:expr)
         | NamedExpr { expr = sub_expr } ->
             infer_type_in_env spec type_env sub_expr
-        | Tuple { label_opt; args } ->
+        | Tuple { loc; label_opt; args } ->
             (* All arguments must typecheck, and if the tuple is labelled,
                the inferred tuple type must be subsumed by the labelled tuple type. *)
             let arg_types, type_env = infer_type_list spec type_env args in
@@ -2456,7 +2488,7 @@ module Check = struct
               let anonymous_typed_args =
                 List.map (fun t -> (None, t)) arg_types
               in
-              Term.Tuple { label_opt; args = anonymous_typed_args }
+              Term.Tuple { loc; label_opt; args = anonymous_typed_args }
             in
             let () =
               match label_opt with
@@ -2481,17 +2513,18 @@ module Check = struct
             (* Mathematically, assignment expressions are just equalities so the
              resulting type is Boolean. *)
             (type_term_for_typedef spec.bool, type_env)
-        | Relation { is_operator = true; name; args = [ lhs; rhs ] }
+        | Relation { loc; is_operator = true; name; args = [ lhs; rhs ] }
           when is_builtin_relation name spec.reverse_assign ->
             (* Reduce to normal assignment by switching lhs and rhs. *)
             infer_type_in_env spec type_env
               (Relation
                  {
+                   loc;
                    is_operator = true;
                    name = spec.assign.name;
                    args = [ rhs; lhs ];
                  })
-        | Relation { name; args; is_operator = true } ->
+        | Relation { loc; name; args; is_operator = true } ->
             (* If the operator is quantifying, the type of the bound variable
                (first argument) cannot be inferred from the expression alone,
                since it's a newly introduced variable. Therefore, we first
@@ -2509,7 +2542,7 @@ module Check = struct
             let () =
               if false then
                 let instantiated_operator =
-                  Relation.make name RelationProperty_Function None
+                  Relation.make loc name RelationProperty_Function None
                     (List.map (fun t -> (None, t)) instantiated_arg_types)
                     [ instantiated_output_type ]
                     [] None
@@ -2679,7 +2712,7 @@ module Check = struct
         in
         let bound_variable_name, domain_term, type_env =
           match args with
-          | Var id :: domain_expr :: _ ->
+          | Var { id } :: domain_expr :: _ ->
               let domain_term, type_env =
                 infer_type_in_env spec type_env domain_expr
               in
@@ -2727,8 +2760,8 @@ module Check = struct
         match expr with NamedExpr { expr = sub_expr } -> sub_expr | _ -> expr
       in
       match (expr, target_type) with
-      | Var id, _ when is_ignore_var id -> type_env
-      | Var id, _ -> StringMap.add id target_type type_env
+      | Var { id }, _ when is_ignore_var id -> type_env
+      | Var { id }, _ -> StringMap.add id target_type type_env
       | ( Relation { name; args = [ arg ]; is_operator = true },
           Term.TypeOperator { op; term = _, op_arg_type } )
         when is_builtin_relation name spec.some_operator
@@ -2767,7 +2800,7 @@ module Check = struct
             (fun curr_env arg (_, target_arg_type) ->
               apply_type spec curr_env arg target_arg_type)
             type_env args target_args
-      | ListIndex { list_var; index }, _ ->
+      | ListIndex { loc; list_var; index }, _ ->
           let index_type, _ = infer_type_in_env spec type_env index in
           let () =
             if
@@ -2777,7 +2810,7 @@ module Check = struct
             else Error.invalid_list_index_type index_type ~context_expr:expr
           in
           let list_var_type =
-            Term.TypeOperator { op = List0; term = (None, target_type) }
+            Term.TypeOperator { loc; op = List0; term = (None, target_type) }
           in
           StringMap.add list_var list_var_type type_env
       | ( Expr.Record { fields = expr_fields; _ },
@@ -2873,17 +2906,14 @@ module Check = struct
 
         @raise [SpecError] if a type error is found during inference. *)
     let infer_type_for_judgment spec type_env expr =
-      try
-        let () =
-          if false then
-            Format.eprintf "--- Inferring types for judgment %a ---@."
-              PP.pp_expr expr
-          else ()
-        in
-        let judgment_type, updated_env = infer_type_in_env spec type_env expr in
-        (judgment_type, updated_env)
-      with SpecError err | Failure err ->
-        stack_spec_error err (Format.asprintf "In judgment %a" PP.pp_expr expr)
+      let () =
+        if false then
+          Format.eprintf "--- Inferring types for judgment %a ---@." PP.pp_expr
+            expr
+        else ()
+      in
+      let judgment_type, updated_env = infer_type_in_env spec type_env expr in
+      (judgment_type, updated_env)
 
     let check_and_infer relation spec expanded_rule =
       let () =
@@ -2946,20 +2976,19 @@ module Check = struct
         and that the last judgment, and only the last judgment, is an output
         judgment. If not, raises a [SpecError] describing the issue.
         [relation_name] is used when reporting errors. *)
-    let check_well_formed_expanded relation_name expanded_rule =
+    let check_well_formed_expanded relation expanded_rule =
       let open ExpandRules in
       (* Reverse the list to easily access the last judgment. *)
       match List.rev expanded_rule.judgments with
-      | [] -> Error.empty_rule relation_name
+      | [] -> Error.empty_rule relation
       | { expr = Transition _; is_output = true } :: prefix_rules ->
           List.iter
             (fun { Rule.is_output } ->
               if is_output then
-                Error.multiple_output_judgments relation_name
-                  expanded_rule.name_opt
+                Error.multiple_output_judgments relation expanded_rule.name_opt
               else ())
             prefix_rules
-      | _ -> Error.missing_output_judgment relation_name expanded_rule.name_opt
+      | _ -> Error.missing_output_judgment relation expanded_rule.name_opt
 
     (** [formals_of_relation id_to_defining_node rel_name] returns the list of
         formal arguments for the relation named [rel_name] using
@@ -3002,7 +3031,7 @@ module Check = struct
           | Some label ->
               let type_components = args_of_tuple id_to_defining_node label in
               if List.compare_lengths args type_components <> 0 then
-                Error.invalid_number_of_components label expr
+                Error.invalid_number_of_components expr
                   ~expected:(List.length type_components)
                   ~actual:(List.length args)
           | None -> ())
@@ -3060,26 +3089,18 @@ module Check = struct
       let () =
         List.iter
           (fun expanded_rule ->
-            try
-              let () =
-                check_well_formed_expanded relation.Relation.name expanded_rule
-              in
-              let open ExpandRules in
-              let () =
-                List.iter
-                  (fun { Rule.expr } -> check_expr_well_formed spec expr)
-                  expanded_rule.judgments
-              in
-              let () = UseDef.check_use_def relation spec expanded_rule in
-              let _discarded_type_env =
-                TypeInference.check_and_infer relation spec expanded_rule
-              in
-              ()
-            with SpecError err | Failure err ->
-              stack_spec_error err
-                (Format.asprintf "In rule for relation %s, case %s"
-                   relation.Relation.name
-                   (Option.value ~default:"top-level" expanded_rule.name_opt)))
+            let () = check_well_formed_expanded relation expanded_rule in
+            let open ExpandRules in
+            let () =
+              List.iter
+                (fun { Rule.expr } -> check_expr_well_formed spec expr)
+                expanded_rule.judgments
+            in
+            let () = UseDef.check_use_def relation spec expanded_rule in
+            let _discarded_type_env =
+              TypeInference.check_and_infer relation spec expanded_rule
+            in
+            ())
           expanded_rules
       in
       ()
@@ -3189,27 +3210,29 @@ module ExtendNames = struct
   (** [opt_extend] Wraps [expr] with a name if [opt_param_name] is [Some].
       Avoids naming a variable expression with its own name. *)
   let opt_extend spec expr opt_param_name =
+    let loc = Expr.loc_of expr in
     match (expr, opt_param_name) with
     | _, None -> expr
-    | Var v, Some name when String.equal v name ->
-        NamedExpr { expr; name; same_name = true }
+    | Var { id }, Some name when String.equal id name ->
+        NamedExpr { loc; expr; name; same_name = true }
         (* Avoid naming a variable with its own name. *)
     | ( Expr.Relation
-          { name = operator_name; is_operator = true; args = [ Var v ] },
+          { name = operator_name; is_operator = true; args = [ Var { id } ] },
         Some name ) ->
         let relation = relation_for_id spec operator_name in
-        if Relation.is_typecast_operator relation && String.equal v name then
+        if Relation.is_typecast_operator relation && String.equal id name then
           (* Typecasts render the input variable. If the input variable has the same name
              as the parameter, avoid naming it. *)
-          NamedExpr { expr; name; same_name = true }
-        else NamedExpr { expr; name; same_name = false }
-    | _, Some name -> NamedExpr { expr; name; same_name = false }
+          NamedExpr { loc; expr; name; same_name = true }
+        else NamedExpr { loc; expr; name; same_name = false }
+    | _, Some name -> NamedExpr { loc; expr; name; same_name = false }
 
   (** [extend_with_names type_term expr ] recursively transforms [expr] by
       adding names from [type_term] to sub-expressions of [expr]. Currently,
       only tuples (labelled or unlabelled) are supported, which is sufficient
       for most output configurations. *)
   let rec extend_with_names spec type_term expr =
+    let loc = Expr.loc_of expr in
     match (type_term, expr) with
     | Term.Tuple { label_opt = None; args = [ (opt_name, _) ] }, _ ->
         (* An unlabelled tuple with a single component serves as a named reference
@@ -3226,7 +3249,7 @@ module ExtendNames = struct
                  term %a since they have different number of args."
                 PP.pp_expr expr PP.pp_type_term type_term
             in
-            raise (SpecError msg)
+            Error.spec_error (Expr.loc_of expr) msg
           else ()
         in
         let extended_args =
@@ -3235,7 +3258,7 @@ module ExtendNames = struct
               opt_extend spec (extend_with_names spec arg_type arg) opt_name)
             term_components expr_components
         in
-        Expr.Tuple { label_opt = expr_label_opt; args = extended_args }
+        Expr.Tuple { loc; label_opt = expr_label_opt; args = extended_args }
     | _ -> expr
 
   (** [extend_rule_element output_type rule_element] extends output judgments in
@@ -3243,8 +3266,10 @@ module ExtendNames = struct
   let rec extend_rule_element spec output_types rule_element =
     match rule_element with
     | Judgment
-        ({ expr = Transition { lhs; rhs; short_circuit }; is_output = true } as
-         judgment) ->
+        ({
+           expr = Transition { loc; lhs; rhs; short_circuit };
+           is_output = true;
+         } as judgment) ->
         let output_type =
           match match_output_expr_to_term spec rhs output_types with
           | Some output_type -> output_type
@@ -3254,7 +3279,7 @@ module ExtendNames = struct
         in
         let extended_rhs = extend_with_names spec output_type rhs in
         let extended_expr =
-          Transition { lhs; rhs = extended_rhs; short_circuit }
+          Transition { loc; lhs; rhs = extended_rhs; short_circuit }
         in
         Judgment { judgment with expr = extended_expr }
     | Judgment _ -> rule_element
@@ -3312,16 +3337,15 @@ module ExtendConstantsWithTypes = struct
             in
             let init_type = Check.TypeInference.infer spec init_expr in
             init_type
-          with SpecError err ->
-            stack_spec_error err
-              (Format.asprintf
-                 "When inferring type for constant %s from its initialization \
-                  expression %a. Hint: you can explicitly specify the type of \
-                  the constant or reorder the constants."
-                 name PP.pp_expr init_expr))
+          with SpecError { loc; msg } ->
+            let extra_msg =
+              "Hint: you can explicitly specify the type of the constant or \
+               reorder the constants."
+            in
+            stack_spec_error loc msg extra_msg)
       | None, None ->
           (* A constant without a specified type has a type labeled by its name. *)
-          Label name
+          Label { loc = missing_location; label = name }
     in
     { def with Constant.opt_type = Some constant_type }
 
@@ -3373,20 +3397,22 @@ let add_default_rule_renders ({ ast } as spec) =
     List.filter_map
       (fun elem ->
         match elem with
-        | Elem_Relation { Relation.name; rule_opt = Some _ }
+        | Elem_Relation { Relation.name; loc; rule_opt = Some _ }
           when not (StringSet.mem name relations_with_rules) ->
-            let rule_render = RuleRender.make ~name ~relation_name:name [] in
+            let rule_render =
+              RuleRender.make loc ~name ~relation_name:name []
+            in
             Some (Elem_RenderRule rule_render)
         | _ -> None)
       ast
   in
   { spec with ast = ast @ generated_elems }
 
-(** [get_type id_to_defining_node name] retrieves the [Type.t] associated with
-    [name] in [id_to_defining_node].
+(** [get_builtin_type id_to_defining_node name] retrieves the [Type.t]
+    associated with [name] in [id_to_defining_node].
     @raise [SpecError]
       If [name] is not associated with a [Type.t] in [id_to_defining_node]. *)
-let get_type id_to_defining_node name =
+let get_builtin_type id_to_defining_node name =
   match StringMap.find name id_to_defining_node with
   | Node_Type def -> def
   | node ->
@@ -3395,14 +3421,14 @@ let get_type id_to_defining_node name =
           "%s must be a top-level type, but has been overridden with %a" name
           pp_definition_node node
       in
-      raise (SpecError msg)
+      Error.spec_error missing_location msg
 
-(** [get_constant id_to_defining_node name] retrieves the [Constant.t]
+(** [get_builtin_constant id_to_defining_node name] retrieves the [Constant.t]
     associated with [name] in [id_to_defining_node].
     @raise [SpecError]
       If [name] is not associated with a [Constant.t] in [id_to_defining_node].
 *)
-let get_constant id_to_defining_node name =
+let get_builtin_constant id_to_defining_node name =
   match StringMap.find name id_to_defining_node with
   | Node_Constant def -> def
   | node ->
@@ -3410,14 +3436,14 @@ let get_constant id_to_defining_node name =
         Format.asprintf "%s must be a constant, but has been overridden with %a"
           name pp_definition_node node
       in
-      raise (SpecError msg)
+      Error.spec_error missing_location msg
 
-(** [get_relation id_to_defining_node name] retrieves the [Relation.t]
+(** [get_builtin_relation id_to_defining_node name] retrieves the [Relation.t]
     associated with [name] in [id_to_defining_node].
     @raise [SpecError]
       If [name] is not associated with a [Relation.t] in [id_to_defining_node].
 *)
-let get_relation id_to_defining_node name =
+let get_builtin_relation id_to_defining_node name =
   match StringMap.find_opt name id_to_defining_node with
   | Some (Node_Relation def) when def.is_operator -> def
   | Some node ->
@@ -3426,10 +3452,10 @@ let get_relation id_to_defining_node name =
           "%s must be an operator, but has been overridden with %a" name
           pp_definition_node node
       in
-      raise (SpecError msg)
+      Error.spec_error missing_location msg
   | None ->
       let msg = Format.asprintf "Relation/operator %s is undefined." name in
-      raise (SpecError msg)
+      Error.spec_error missing_location msg
 
 (** [extend_ast_with_builtins ast id_to_defining_node] prepends to [ast] the AST
     elements from the built-in specification that are not already defined in
@@ -3454,24 +3480,24 @@ let make_spec_with_builtins ast =
   let id_to_defining_node = make_symbol_table ast in
   let ast = prepend_ast_with_builtins ast id_to_defining_node in
   let id_to_defining_node = make_symbol_table ast in
-  let get_constant = get_constant id_to_defining_node in
-  let get_type = get_type id_to_defining_node in
-  let get_relation = get_relation id_to_defining_node in
+  let get_builtin_constant = get_builtin_constant id_to_defining_node in
+  let get_builtin_type = get_builtin_type id_to_defining_node in
+  let get_builtin_relation = get_builtin_relation id_to_defining_node in
   {
     ast;
     id_to_defining_node;
-    bottom_constant = get_constant "bot";
-    bottom_term = Label "bot";
-    none_constant = get_constant "None";
-    empty_set = get_constant "empty_set";
-    empty_list = get_constant "empty_list";
-    bool = get_type "Bool";
-    n_type = get_type "N";
-    z_type = get_type "Z";
-    assign = get_relation "assign";
-    reverse_assign = get_relation "reverse_assign";
-    some_operator = get_relation "some";
-    cond_operator = get_relation "cond_op";
+    bottom_constant = get_builtin_constant "bot";
+    bottom_term = Label { loc = missing_location; label = "bot" };
+    none_constant = get_builtin_constant "None";
+    empty_set = get_builtin_constant "empty_set";
+    empty_list = get_builtin_constant "empty_list";
+    bool = get_builtin_type "Bool";
+    n_type = get_builtin_type "N";
+    z_type = get_builtin_type "Z";
+    assign = get_builtin_relation "assign";
+    reverse_assign = get_builtin_relation "reverse_assign";
+    some_operator = get_builtin_relation "some";
+    cond_operator = get_builtin_relation "cond_op";
     variant_id_to_containing_type = make_variant_id_to_containing_type ast;
     field_to_containing_variant = make_field_to_containing_variant ast;
   }
@@ -3479,7 +3505,7 @@ let make_spec_with_builtins ast =
 let from_ast ast =
   let spec = make_spec_with_builtins ast in
   let () = Check.check_no_undefined_ids spec in
-  let () = Check.check_relations_outputs spec in
+  let () = Check.check_relation_outputs spec in
   let () = Check.CheckTypeInstantiations.check spec in
   let () = Check.check_math_layout spec in
   let () = Check.CheckProseTemplates.check spec in
diff --git a/asllib/aslspec/spec.mli b/asllib/aslspec/spec.mli
index 8baf0885b1..645b669ad9 100644
--- a/asllib/aslspec/spec.mli
+++ b/asllib/aslspec/spec.mli
@@ -7,8 +7,8 @@ open AST
 val ignore_var : string
 
 (** Wraps AST nodes that define identifiers that may appear in type terms and
-    expression terms: types, constants, relations, labels, labelled tuples, and
-    labelled records. *)
+    expression terms: types, constants, relations, type variants, and record
+    fields. *)
 type definition_node =
   | Node_Type of Type.t
   | Node_Relation of Relation.t
@@ -23,8 +23,9 @@ val math_macro_opt_for_node : definition_node -> string option
 (** Utility functions for handling layouts. *)
 module Layout : sig
   val math_layout_for_node : definition_node -> layout
-  (** [math_layout_for_node node] returns the math layout for [node], or a
-      default layout based on its type term if no math layout is defined. *)
+  (** [math_layout_for_node node] returns the math layout for [node]. If none is
+      defined, a default layout is inferred for relation nodes, type variants,
+      and record fields; otherwise [Unspecified] is returned. *)
 
   val for_type_term : Term.t -> layout
   (** [for_type_term term] returns a full default layout for [term]. That is, a
@@ -46,7 +47,7 @@ val elements : t -> elem list
 
 val defining_node_for_id : t -> string -> definition_node
 (** [defining_node_for_id spec id] returns the defining node for [id] in [spec].
-    Raises [SpecError] if [id] is not defined. *)
+    Assumes that [id] is defined in [spec]. *)
 
 val defining_node_opt_for_id : t -> string -> definition_node option
 (** [defining_node_opt_for_id spec id] returns [Some node] if [id] is defined in
@@ -99,9 +100,8 @@ val filter_rule_for_path : Relation.t -> string -> Rule.t
 (** [filter_rule_for_path relation path_str] filters the rule given for
     [relation] to only include the cases along the path specified by [path_str].
     The path is a dot-separated, where each name corresponds to the name of the
-    case to take at each level of nesting. For example, "name1.name2" means ---
-    take the first case at the top level, and then the second case within that
-    case.
+    case to take at each level of nesting. For example, "name1.name2" means:
+    take case [name1] at the top level, and then case [name2] within it.
 
     @raise [SpecError]
       if [path_str] is not a valid path through the cases of the rule for
diff --git a/asllib/aslspec/tests.t/run.t b/asllib/aslspec/tests.t/run.t
index 5a2f36137a..91886c15bd 100644
--- a/asllib/aslspec/tests.t/run.t
+++ b/asllib/aslspec/tests.t/run.t
@@ -29,7 +29,7 @@
   >     \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c};
 
   $ aslspec type_name.bad
-  Syntax Error: illegal element-defining identifier: t2 around type_name.bad line 1 column 41
+  Syntax Error: type_name.bad:1:9: illegal element-defining identifier: t2
   [1]
 
 # Test that --pp generates legal output
@@ -41,45 +41,33 @@
   $ aslspec relations.spec --pp > tmp1.spec; aslspec tmp1.spec --pp > tmp2.spec; diff --ignore-all-space tmp1.spec tmp2.spec
 
   $ aslspec unmatched_prose_var.spec
-  Specification Error: The prose template 'transforms {a} to {b}' contains the following unmatched variables: {b}
-  While checking: relation transform_description_unmatched_b(a: A) -> A
-                  {
-                     prose_description = "transforms {a} to {b}",
-                     prose_application = "",
-                  };
+  Specification Error: Unknown location: The prose template "transforms {a} to {b}" contains the following unmatched variables: {b}
   [1]
 
 # Check that all type terms are well-formed
   $ aslspec instantiation_expansion.spec
   $ aslspec instantiation_labelled_tuple2.bad
-  Specification Error: The type term `L(O, A, B)` cannot be instantiated since it has 3 type terms and `L` requires 2 type terms
-  While checking: B
+  Specification Error: instantiation_labelled_tuple2.bad:9:8: The type term `L(O, A, B)` cannot be instantiated since it has 3 type terms and `L` requires 2 type terms
   [1]
   $ aslspec instantiation_labelled_tuple.bad
-  Specification Error: The type term `A(Int)` cannot be instantiated since 'A' is not a labelled tuple type
-  While checking: A
+  Specification Error: instantiation_labelled_tuple.bad:6:17: The type term `A(Int)` cannot be instantiated since A is not a labelled tuple type
   [1]
   $ aslspec instantiation_function.bad
-  Specification Error: Unable to determine that `fun O -> P` is subsumed by `fun P -> P`
-  While checking: Incorrect
+  Specification Error: instantiation_function.bad:9:25: Unable to determine that `fun O -> P` is subsumed by `fun P -> P`
   [1]
   $ aslspec instantiation_constant.bad
-  Specification Error: Int is used as a constant even though it is not defined as one
-  While checking: B
+  Specification Error: instantiation_constant.bad:3:18: Int is used as a constant even though it is not defined as one
   [1]
   $ aslspec instantiation_record.bad
-  Specification Error: The type term `A[f: Int]` cannot be instantiated since 'A' is not a labelled record type
-  While checking: A
+  Specification Error: instantiation_record.bad:6:17: The type term `A[f: Int]` cannot be instantiated since A is not a labelled record type
   [1]
   $ aslspec instantiation_label.bad
-  Specification Error: The type term `B` cannot be instantiated since 'B' is not a type
-  While checking: A
+  Specification Error: instantiation_label.bad:7:8: The type term `B` cannot be instantiated since B is not a type
   [1]
   $ aslspec instantiation_recursion.bad
-  Specification Error: Unable to determine that `B` is subsumed by `A`
-  While checking: B
+  Specification Error: instantiation_recursion.bad:9:11: Unable to determine that `B` is subsumed by `A`
   [1]
   $ aslspec relation_unnamed_arguments.bad
-  Specification Error: The term Num in relation 'unnamed_arg_has_rule' does not provide a name for at least one of its sub-terms.
+  Specification Error: relation_unnamed_arguments.bad:6:38: The term Num in relation unnamed_arg_has_rule does not provide a name for at least one of its sub-terms.
   [1]
   $ aslspec constants.spec
diff --git a/asllib/doc/.gitignore b/asllib/doc/.gitignore
index 51c5433ac7..64ea7f6c54 100644
--- a/asllib/doc/.gitignore
+++ b/asllib/doc/.gitignore
@@ -1,9 +1,5 @@
-ifempty.tex
-ifcode.tex
 comment.cut
-*Lines.tex
 generated_macros.tex
-generated_elements.tex
 *.bbl
 *.blg
 *.dvi
diff --git a/asllib/doc/ifcode.tex b/asllib/doc/ifcode.tex
new file mode 100644
index 0000000000..bc09244dd3
--- /dev/null
+++ b/asllib/doc/ifcode.tex
@@ -0,0 +1 @@
+\newif\ifcode\codefalse
diff --git a/asllib/doc/ifempty.tex b/asllib/doc/ifempty.tex
new file mode 100644
index 0000000000..6f393058c3
--- /dev/null
+++ b/asllib/doc/ifempty.tex
@@ -0,0 +1 @@
+\newif\ifempty\emptyfalse