diff --git a/CHANGELOG.md b/CHANGELOG.md
index 68f1d8bb6..bd4b87129 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,12 @@
 # Changelog
 
+## 2026-07-06
+
+### Candid 0.10.32
+
+* Non-breaking changes:
+  + A service reference now decodes where a `principal` is expected: `service <actortype>` is a subtype of `principal` (spec addition: `service <: principal`, modelled analogously to `nat <: int`). The subtype checker and the deserializer accept a service reference at type `principal`; the two share an identical wire encoding, so the coercion is the identity on the reference. The reverse (a `principal` at a `service` type) remains rejected.
+
 ## 2026-07-03
 
 ### ic_principal 0.1.5
diff --git a/Cargo.lock b/Cargo.lock
index 408799824..119688fd0 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -209,13 +209,13 @@ dependencies = [
 
 [[package]]
 name = "candid"
-version = "0.10.31"
+version = "0.10.32"
 dependencies = [
  "anyhow",
  "bincode",
  "binread",
  "byteorder",
- "candid_derive 0.10.31",
+ "candid_derive 0.10.32",
  "candid_parser 0.4.0",
  "hex",
  "ic_principal 0.1.5",
@@ -247,7 +247,7 @@ dependencies = [
 
 [[package]]
 name = "candid_derive"
-version = "0.10.31"
+version = "0.10.32"
 dependencies = [
  "lazy_static",
  "proc-macro2 1.0.86",
@@ -280,7 +280,7 @@ version = "0.4.0"
 dependencies = [
  "anyhow",
  "arbitrary",
- "candid 0.10.31",
+ "candid 0.10.32",
  "codespan-reporting",
  "console",
  "convert_case",
diff --git a/coq/MiniCandid.v b/coq/MiniCandid.v
index 61bfc58d4..16ec632a2 100644
--- a/coq/MiniCandid.v
+++ b/coq/MiniCandid.v
@@ -35,6 +35,8 @@ CoInductive T :=
   | NullT : T
   | OptT : T -> T
   | FuncT : T -> T -> T
+  | ServiceT : T
+  | PrincipalT : T
   | VoidT : T
   | ReservedT : T
   .
@@ -54,6 +56,8 @@ Inductive V :=
   | NullV : V
   | SomeV : V -> V
   | FuncV : RefV -> V
+  | ServiceV : RefV -> V
+  | PrincipalV : RefV -> V
   | ReservedV : V
   .
 (**
@@ -91,6 +95,12 @@ Inductive HasType : V -> T -> Prop :=
   | FuncHT:
     case funcHT,
     forall rv t1 t2, FuncV rv :: FuncT t1 t2
+  | ServiceHT:
+    case serviceHT,
+    forall rv, ServiceV rv :: ServiceT
+  | PrincipalHT:
+    case principalHT,
+    forall rv, PrincipalV rv :: PrincipalT
   | ReservedHT:
     case reservedHT,
     ReservedV :: ReservedT
@@ -105,6 +115,9 @@ CoInductive Subtype : T -> T -> Prop :=
   | NatIntST :
     case natIntST,
     NatT <: IntT
+  | ServicePrincipalST :
+    case servicePrincipalST,
+    ServiceT <: PrincipalT
   | OptST :
     case optST,
     forall t1 t2,
@@ -179,6 +192,9 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V :=
   | IntV n, IntT, IntT => IntV n
   | NatV n, NatT, IntT => IntV (Z.of_nat n)
   | FuncV r, FuncT ta1 tr1, FuncT ta2 tr2 => FuncV r
+  | ServiceV r, ServiceT, ServiceT => ServiceV r
+  | PrincipalV r, PrincipalT, PrincipalT => PrincipalV r
+  | ServiceV r, ServiceT, PrincipalT => PrincipalV r
 
   | SomeV v, OptT t1, OptT t2 =>
     if t1 <:? t2
@@ -195,6 +211,9 @@ Function coerce (t1 : T) (t2 : T) (v1 : V) : V :=
   | FuncV r, FuncT ta1 tr1, OptT (FuncT ta2 tr2) =>
     if ta2 <:? ta1
     then if tr1 <:? tr2 then SomeV (FuncV r) else NullV else NullV
+  | ServiceV r, ServiceT, OptT ServiceT => SomeV (ServiceV r)
+  | PrincipalV r, PrincipalT, OptT PrincipalT => SomeV (PrincipalV r)
+  | ServiceV r, ServiceT, OptT PrincipalT => SomeV (PrincipalV r)
 
   | v, t, ReservedT => ReservedV
 
@@ -237,6 +256,16 @@ Proof.
       destruct (t3 <:? t2_2); try reflexivity.
       contradict HNotST; named_constructor; assumption.
   }
+  [serviceHT]: {
+    destruct (ServiceT <:? t2) as [HST | HNotST].
+    - inversion HST; subst; clear HST; simpl; reflexivity.
+    - destruct t2; try reflexivity; contradict HNotST; named_constructor.
+  }
+  [principalHT]: {
+    destruct (PrincipalT <:? t2) as [HST | HNotST].
+    - inversion HST; subst; clear HST; simpl; reflexivity.
+    - destruct t2; try reflexivity; contradict HNotST; named_constructor.
+  }
 Qed.
 
 Lemma coerce_reservedT:
@@ -254,6 +283,9 @@ Lemma coerce_nice_ind:
   (case natC, forall n, P NatT NatT (NatV n) (NatV n)) ->
   (case intC, forall n, P IntT IntT (IntV n) (IntV n)) ->
   (case natIntC, forall n, P NatT IntT (NatV n) (IntV (Z.of_nat n))) ->
+  (case serviceC, forall r, P ServiceT ServiceT (ServiceV r) (ServiceV r)) ->
+  (case principalC, forall r, P PrincipalT PrincipalT (PrincipalV r) (PrincipalV r)) ->
+  (case servicePrincipalC, forall r, P ServiceT PrincipalT (ServiceV r) (PrincipalV r)) ->
   (case nullC, P NullT NullT NullV NullV) ->
   (case nullOptC, forall t, P NullT (OptT t) NullV NullV) ->
   (case optNullC, forall t1 t2, P (OptT t1) (OptT t2) NullV NullV) ->
@@ -293,7 +325,7 @@ Lemma coerce_nice_ind:
   (forall t1 t2 v1, t1 <: t2 -> v1 :: t1 -> P t1 t2 v1 (coerce t1 t2 v1)).
 Proof.
   intros P.
-  intros NatC IntC NatIntC NullC NullOptC OptNullC OptSomeC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC FuncC ReservedC.
+  intros NatC IntC NatIntC ServiceC PrincipalC ServicePrincipalC NullC NullOptC OptNullC OptSomeC OpportunisticOptC ReservedOptC ConstituentOptC OpportunisticConstituentOptC FuncC ReservedC.
   intros t1 t2 v1 HST HHT.
   revert t2 HST.
   induction HHT; name_cases.
@@ -319,6 +351,8 @@ Proof.
           - contradict n0. named_constructor.
           - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
           - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
     }
     [reservedST]: { apply ReservedC; clear_names. named_constructor. }
   }
@@ -338,6 +372,8 @@ Proof.
           - contradict n0. named_constructor.
           - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
           - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
     }
     [reservedST]: { apply ReservedC; clear_names. named_constructor. }
   }
@@ -370,6 +406,8 @@ Proof.
                ++ apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
             ** apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
           - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
     }
     [funcST]: { apply FuncC; clear_names; assumption. }
     [reservedST]: { apply ReservedC; clear_names. named_constructor. }
@@ -405,13 +443,57 @@ Proof.
     }
     [reservedST]: { apply ReservedC; clear_names. named_constructor; assumption. }
   }
-  [reservedHT]: { 
+  [reservedHT]: {
     intros.
     inversion HST; subst; clear HST; name_cases.
     [reflST]: { apply ReservedC; clear_names. named_constructor. }
     [optST]: { apply ReservedOptC; clear_names. }
     [reservedST]: { apply ReservedC; clear_names.  named_constructor. }
   }
+  [serviceHT]: {
+    intros.
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: { apply ServiceC; clear_names. }
+    [servicePrincipalST]: { apply ServicePrincipalC; clear_names. }
+    [optST]: {
+      destruct (is_opt_like_type t0) eqn:His_opt_like.
+      * destruct t0; inversion His_opt_like; simpl; clear His_opt_like;
+        apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+      * destruct (subtyping_decidable ServiceT t0) as [s | Hn].
+        + destruct t0; inversion s; subst; clear s; inversion His_opt_like; clear His_opt_like.
+          - apply ConstituentOptC; clear_names; simpl; intuition; named_constructor.
+          - apply ConstituentOptC; clear_names; simpl; intuition; named_constructor.
+        + destruct t0; inversion His_opt_like; clear His_opt_like.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - contradict Hn. named_constructor.
+          - contradict Hn. named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+    }
+    [reservedST]: { apply ReservedC; clear_names. named_constructor. }
+  }
+  [principalHT]: {
+    intros.
+    inversion HST; subst; clear HST; name_cases.
+    [reflST]: { apply PrincipalC; clear_names. }
+    [optST]: {
+      destruct (is_opt_like_type t0) eqn:His_opt_like.
+      * destruct t0; inversion His_opt_like; simpl; clear His_opt_like;
+        apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+      * destruct (subtyping_decidable PrincipalT t0) as [s | Hn].
+        + destruct t0; inversion s; subst; clear s; inversion His_opt_like; clear His_opt_like.
+          - apply ConstituentOptC; clear_names; simpl; intuition; named_constructor.
+        + destruct t0; inversion His_opt_like; clear His_opt_like.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+          - contradict Hn. named_constructor.
+          - apply OpportunisticConstituentOptC; clear_names; simpl; intuition named_constructor.
+    }
+    [reservedST]: { apply ReservedC; clear_names. named_constructor. }
+  }
 Qed.
 
 (**
@@ -737,6 +819,10 @@ CoInductive UpToNull : V -> V -> Prop :=
     SomeV v1 ~~ SomeV v2
   | FuncUT:
     forall r, FuncV r ~~ FuncV r
+  | ServiceUT:
+    forall r, ServiceV r ~~ ServiceV r
+  | PrincipalUT:
+    forall r, PrincipalV r ~~ PrincipalV r
   | ReservedUT:
     ReservedV ~~ ReservedV
 where "v1 ~~ v2" := (UpToNull v1 v2).
diff --git a/coq/nix/default.nix b/coq/nix/default.nix
index 46aac3f19..f7a010f75 100644
--- a/coq/nix/default.nix
+++ b/coq/nix/default.nix
@@ -1,22 +1,29 @@
 {}:
 let
-  sources =  import ./sources.nix;
-
   subpath = import ./gitSource.nix;
 
+  # Re-pinned to a modern nixpkgs that provides coq_8_18.
+  #
+  # The previous niv pin (nixos-20.09) no longer evaluates on current nix, and
+  # the default `coq` is now Rocq 9.x, which renamed the stdlib namespace
+  # (Coq.* -> Stdlib.*) and relocated FunInd — both of which these proofs use.
+  # coq_8_18 is the newest coq that still accepts them unchanged.
+  nixpkgs = fetchTarball {
+    url = "https://github.com/NixOS/nixpkgs/archive/e8273b29fe1390ec8d4603f2477357555291432e.tar.gz";
+    sha256 = "1k8idy9ka87c7gjb9aiqrcx4l9kwblv8fs4pwf0byjivsmbjfdhi";
+  };
+
   overlays = [
     (pkgs: super: { local = {
-      # Fetch niv from nix/sources.json, newer than nixpkgs
-      niv = (import sources.niv {}).niv;
-
       # the main product: building the theories
       theories = pkgs.stdenv.mkDerivation {
         name = "candid-coq";
         src = subpath ./..;
         buildInputs = [
           pkgs.dune_2
-          pkgs.coq
-          pkgs.ocaml
+          pkgs.coq_8_18
+          pkgs.coq_8_18.ocaml
+          pkgs.coq_8_18.ocamlPackages.findlib
         ];
         buildPhase = ''
           dune build --display=short
@@ -31,24 +38,8 @@ let
         inputsFrom = [
           pkgs.local.theories
         ];
-        propagatedBuildInputs = [
-          pkgs.niv
-        ];
-
-        # This helps with using GUI programs like coqide
-        LOCALE_ARCHIVE = pkgs.stdenv.lib.optionalString pkgs.stdenv.isLinux "${pkgs.glibcLocales}/lib/locale/locale-archive";
-
-        # allow building this as a derivation, so that CI can biuld and cache
-        # the dependencies of shell
-        phases = ["installPhase" "fixupPhase"];
-        installPhase = ''
-          mkdir $out
-        '';
-        preferLocalBuild = true;
-        allowSubstitutes = true;
       };
     };})
   ];
 
-in import sources.nixpkgs { inherit overlays; }
-
+in import nixpkgs { inherit overlays; }
diff --git a/coq/nix/sources.json b/coq/nix/sources.json
deleted file mode 100644
index f5e79a22f..000000000
--- a/coq/nix/sources.json
+++ /dev/null
@@ -1,26 +0,0 @@
-{
-    "niv": {
-        "branch": "master",
-        "description": "Easy dependency management for Nix projects",
-        "homepage": "https://github.com/nmattia/niv",
-        "owner": "nmattia",
-        "repo": "niv",
-        "rev": "ba57d5a29b4e0f2085917010380ef3ddc3cf380f",
-        "sha256": "1kpsvc53x821cmjg1khvp1nz7906gczq8mp83664cr15h94sh8i4",
-        "type": "tarball",
-        "url": "https://github.com/nmattia/niv/archive/ba57d5a29b4e0f2085917010380ef3ddc3cf380f.tar.gz",
-        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
-    },
-    "nixpkgs": {
-        "branch": "nixos-20.09",
-        "description": "Nix Packages collection",
-        "homepage": "",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "ae47c79479a086e96e2977c61e538881913c0c08",
-        "sha256": "1yaa02zdbmd4j5lrhbynk5xdv6dkfhajlbsf5fkhx73hj9knmfgn",
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/ae47c79479a086e96e2977c61e538881913c0c08.tar.gz",
-        "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
-    }
-}
diff --git a/coq/nix/sources.nix b/coq/nix/sources.nix
deleted file mode 100644
index 1938409dd..000000000
--- a/coq/nix/sources.nix
+++ /dev/null
@@ -1,174 +0,0 @@
-# This file has been generated by Niv.
-
-let
-
-  #
-  # The fetchers. fetch_<type> fetches specs of type <type>.
-  #
-
-  fetch_file = pkgs: name: spec:
-    let
-      name' = sanitizeName name + "-src";
-    in
-      if spec.builtin or true then
-        builtins_fetchurl { inherit (spec) url sha256; name = name'; }
-      else
-        pkgs.fetchurl { inherit (spec) url sha256; name = name'; };
-
-  fetch_tarball = pkgs: name: spec:
-    let
-      name' = sanitizeName name + "-src";
-    in
-      if spec.builtin or true then
-        builtins_fetchTarball { name = name'; inherit (spec) url sha256; }
-      else
-        pkgs.fetchzip { name = name'; inherit (spec) url sha256; };
-
-  fetch_git = name: spec:
-    let
-      ref =
-        if spec ? ref then spec.ref else
-          if spec ? branch then "refs/heads/${spec.branch}" else
-            if spec ? tag then "refs/tags/${spec.tag}" else
-              abort "In git source '${name}': Please specify `ref`, `tag` or `branch`!";
-    in
-      builtins.fetchGit { url = spec.repo; inherit (spec) rev; inherit ref; };
-
-  fetch_local = spec: spec.path;
-
-  fetch_builtin-tarball = name: throw
-    ''[${name}] The niv type "builtin-tarball" is deprecated. You should instead use `builtin = true`.
-        $ niv modify ${name} -a type=tarball -a builtin=true'';
-
-  fetch_builtin-url = name: throw
-    ''[${name}] The niv type "builtin-url" will soon be deprecated. You should instead use `builtin = true`.
-        $ niv modify ${name} -a type=file -a builtin=true'';
-
-  #
-  # Various helpers
-  #
-
-  # https://github.com/NixOS/nixpkgs/pull/83241/files#diff-c6f540a4f3bfa4b0e8b6bafd4cd54e8bR695
-  sanitizeName = name:
-    (
-      concatMapStrings (s: if builtins.isList s then "-" else s)
-        (
-          builtins.split "[^[:alnum:]+._?=-]+"
-            ((x: builtins.elemAt (builtins.match "\\.*(.*)" x) 0) name)
-        )
-    );
-
-  # The set of packages used when specs are fetched using non-builtins.
-  mkPkgs = sources: system:
-    let
-      sourcesNixpkgs =
-        import (builtins_fetchTarball { inherit (sources.nixpkgs) url sha256; }) { inherit system; };
-      hasNixpkgsPath = builtins.any (x: x.prefix == "nixpkgs") builtins.nixPath;
-      hasThisAsNixpkgsPath = <nixpkgs> == ./.;
-    in
-      if builtins.hasAttr "nixpkgs" sources
-      then sourcesNixpkgs
-      else if hasNixpkgsPath && ! hasThisAsNixpkgsPath then
-        import <nixpkgs> {}
-      else
-        abort
-          ''
-            Please specify either <nixpkgs> (through -I or NIX_PATH=nixpkgs=...) or
-            add a package called "nixpkgs" to your sources.json.
-          '';
-
-  # The actual fetching function.
-  fetch = pkgs: name: spec:
-
-    if ! builtins.hasAttr "type" spec then
-      abort "ERROR: niv spec ${name} does not have a 'type' attribute"
-    else if spec.type == "file" then fetch_file pkgs name spec
-    else if spec.type == "tarball" then fetch_tarball pkgs name spec
-    else if spec.type == "git" then fetch_git name spec
-    else if spec.type == "local" then fetch_local spec
-    else if spec.type == "builtin-tarball" then fetch_builtin-tarball name
-    else if spec.type == "builtin-url" then fetch_builtin-url name
-    else
-      abort "ERROR: niv spec ${name} has unknown type ${builtins.toJSON spec.type}";
-
-  # If the environment variable NIV_OVERRIDE_${name} is set, then use
-  # the path directly as opposed to the fetched source.
-  replace = name: drv:
-    let
-      saneName = stringAsChars (c: if isNull (builtins.match "[a-zA-Z0-9]" c) then "_" else c) name;
-      ersatz = builtins.getEnv "NIV_OVERRIDE_${saneName}";
-    in
-      if ersatz == "" then drv else
-        # this turns the string into an actual Nix path (for both absolute and
-        # relative paths)
-        if builtins.substring 0 1 ersatz == "/" then /. + ersatz else /. + builtins.getEnv "PWD" + "/${ersatz}";
-
-  # Ports of functions for older nix versions
-
-  # a Nix version of mapAttrs if the built-in doesn't exist
-  mapAttrs = builtins.mapAttrs or (
-    f: set: with builtins;
-    listToAttrs (map (attr: { name = attr; value = f attr set.${attr}; }) (attrNames set))
-  );
-
-  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/lists.nix#L295
-  range = first: last: if first > last then [] else builtins.genList (n: first + n) (last - first + 1);
-
-  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L257
-  stringToCharacters = s: map (p: builtins.substring p 1 s) (range 0 (builtins.stringLength s - 1));
-
-  # https://github.com/NixOS/nixpkgs/blob/0258808f5744ca980b9a1f24fe0b1e6f0fecee9c/lib/strings.nix#L269
-  stringAsChars = f: s: concatStrings (map f (stringToCharacters s));
-  concatMapStrings = f: list: concatStrings (map f list);
-  concatStrings = builtins.concatStringsSep "";
-
-  # https://github.com/NixOS/nixpkgs/blob/8a9f58a375c401b96da862d969f66429def1d118/lib/attrsets.nix#L331
-  optionalAttrs = cond: as: if cond then as else {};
-
-  # fetchTarball version that is compatible between all the versions of Nix
-  builtins_fetchTarball = { url, name ? null, sha256 }@attrs:
-    let
-      inherit (builtins) lessThan nixVersion fetchTarball;
-    in
-      if lessThan nixVersion "1.12" then
-        fetchTarball ({ inherit url; } // (optionalAttrs (!isNull name) { inherit name; }))
-      else
-        fetchTarball attrs;
-
-  # fetchurl version that is compatible between all the versions of Nix
-  builtins_fetchurl = { url, name ? null, sha256 }@attrs:
-    let
-      inherit (builtins) lessThan nixVersion fetchurl;
-    in
-      if lessThan nixVersion "1.12" then
-        fetchurl ({ inherit url; } // (optionalAttrs (!isNull name) { inherit name; }))
-      else
-        fetchurl attrs;
-
-  # Create the final "sources" from the config
-  mkSources = config:
-    mapAttrs (
-      name: spec:
-        if builtins.hasAttr "outPath" spec
-        then abort
-          "The values in sources.json should not have an 'outPath' attribute"
-        else
-          spec // { outPath = replace name (fetch config.pkgs name spec); }
-    ) config.sources;
-
-  # The "config" used by the fetchers
-  mkConfig =
-    { sourcesFile ? if builtins.pathExists ./sources.json then ./sources.json else null
-    , sources ? if isNull sourcesFile then {} else builtins.fromJSON (builtins.readFile sourcesFile)
-    , system ? builtins.currentSystem
-    , pkgs ? mkPkgs sources system
-    }: rec {
-      # The sources, i.e. the attribute set of spec name to spec
-      inherit sources;
-
-      # The "pkgs" (evaluated nixpkgs) to use for e.g. non-builtin fetchers
-      inherit pkgs;
-    };
-
-in
-mkSources (mkConfig {}) // { __functor = _: settings: mkSources (mkConfig settings); }
diff --git a/rust/bench/Cargo.lock b/rust/bench/Cargo.lock
index cd46b269f..94fa1007e 100644
--- a/rust/bench/Cargo.lock
+++ b/rust/bench/Cargo.lock
@@ -156,7 +156,7 @@ dependencies = [
 
 [[package]]
 name = "candid"
-version = "0.10.31"
+version = "0.10.32"
 dependencies = [
  "anyhow",
  "binread",
@@ -177,7 +177,7 @@ dependencies = [
 
 [[package]]
 name = "candid_derive"
-version = "0.10.31"
+version = "0.10.32"
 dependencies = [
  "lazy_static",
  "proc-macro2",
diff --git a/rust/candid/Cargo.toml b/rust/candid/Cargo.toml
index 583b646fb..47fbdc432 100644
--- a/rust/candid/Cargo.toml
+++ b/rust/candid/Cargo.toml
@@ -1,7 +1,7 @@
 [package]
 name = "candid"
 # sync with the version in `candid_derive/Cargo.toml`
-version = "0.10.31"
+version = "0.10.32"
 edition = "2021"
 rust-version.workspace = true
 authors = ["DFINITY Team"]
@@ -16,7 +16,7 @@ keywords = ["internet-computer", "idl", "candid", "dfinity"]
 include = ["src", "Cargo.toml", "LICENSE", "README.md"]
 
 [dependencies]
-candid_derive = { path = "../candid_derive", version = "=0.10.31" }
+candid_derive = { path = "../candid_derive", version = "=0.10.32" }
 ic_principal = { path = "../ic_principal", version = "0.1.0" }
 binread = { version = "2.2", features = ["debug_template"] }
 byteorder = "1.5.0"
diff --git a/rust/candid/src/de.rs b/rust/candid/src/de.rs
index f18a334be..1fdd72137 100644
--- a/rust/candid/src/de.rs
+++ b/rust/candid/src/de.rs
@@ -618,8 +618,20 @@ impl<'de> Deserializer<'de> {
         V: Visitor<'de>,
     {
         self.unroll_type()?;
+        // Dispatched only when the expected type is `principal`. Accept exactly
+        // the two wire types that share the `PrincipalBytes` encoding: `principal`
+        // (reflexive) and `service <actortype>` (spec: `service <: principal`), so
+        // a service reference decodes as its principal. We match the wire type
+        // directly rather than calling `check_subtype()`: the general subtype
+        // relation also admits `empty` (bottom) `<: principal`, which would let a
+        // payload declare wire type `empty` yet be decoded as a principal from
+        // arbitrary trailing bytes. Matching also avoids the subtype-check
+        // overhead on this common decoding path.
         check!(
-            *self.expect_type == TypeInner::Principal && *self.wire_type == TypeInner::Principal,
+            matches!(
+                self.wire_type.as_ref(),
+                TypeInner::Principal | TypeInner::Service(_)
+            ),
             "principal"
         );
         let mut bytes = vec![2u8];
diff --git a/rust/candid/src/types/subtype.rs b/rust/candid/src/types/subtype.rs
index bf3027aff..8072f18a4 100644
--- a/rust/candid/src/types/subtype.rs
+++ b/rust/candid/src/types/subtype.rs
@@ -272,6 +272,10 @@ fn subtype_collect_(
         (_, Reserved) => (),
         (Empty, _) => (),
         (Nat, Int) => (),
+        // A service reference is represented by its canister's principal, so any
+        // service type is a subtype of `principal` (spec: `service <: principal`),
+        // unconditionally — like `Nat <: Int`.
+        (Service(_), Principal) => (),
         (Vec(ty1), Vec(ty2)) => {
             subtype_collect_(report, gamma, env, ty1, ty2, depth, path, errors, is_input);
         }
@@ -555,6 +559,7 @@ fn subtype_(
         (_, Reserved) => Ok(()),
         (Empty, _) => Ok(()),
         (Nat, Int) => Ok(()),
+        (Service(_), Principal) => Ok(()),
         (Vec(ty1), Vec(ty2)) => subtype_(report, gamma, env, ty1, ty2, depth),
         (Null, Opt(_)) => Ok(()),
         (Opt(ty1), Opt(ty2)) if subtype_(report, gamma, env, ty1, ty2, depth).is_ok() => Ok(()),
diff --git a/rust/candid_derive/Cargo.toml b/rust/candid_derive/Cargo.toml
index 4f2f4ec5e..1237b6d69 100644
--- a/rust/candid_derive/Cargo.toml
+++ b/rust/candid_derive/Cargo.toml
@@ -1,7 +1,7 @@
 [package]
 name = "candid_derive"
 # sync with the version in `candid/Cargo.toml`
-version = "0.10.31"
+version = "0.10.32"
 edition = "2021"
 rust-version.workspace = true
 authors = ["DFINITY Team"]
diff --git a/spec/Candid.md b/spec/Candid.md
index baa2d93bb..d88794216 100644
--- a/spec/Candid.md
+++ b/spec/Candid.md
@@ -756,6 +756,14 @@ An exception are integers, which can be specialised to natural numbers:
 nat <: int
 ```
 
+Similarly, a principal can be specialised to any service reference:
+
+```
+
+--------------------------------
+service <actortype> <: principal
+```
+
 Additional rules apply to `empty` and `reserved`, which makes these a bottom resp. top type:
 ```
 
@@ -921,6 +929,12 @@ Values of type `nat` coerce at type `int`:
 <nat> : nat ~> <nat> : int
 ```
 
+A service reference coerces at type `principal` (both share the same value form, so this is the identity on the value):
+```
+---------------------------------------------------------------------
+service <text> : service <actortype> ~> principal <text> : principal
+```
+
 Coercion into `reserved` is the constant map (this is arbitrarily using `null` as “the” value of `reserved`):
 ```
 --------------------------
diff --git a/test/reference.test.did b/test/reference.test.did
index 51ff72ea4..99ea82b33 100644
--- a/test/reference.test.did
+++ b/test/reference.test.did
@@ -26,6 +26,27 @@ assert blob "DIDL\02\6a\01\71\01\7d\00\69\01\03foo\00\01\01\01\03\ca\ff\ee"
 assert blob "DIDL\02\6a\01\71\01\7d\00\69\02\03foo\00\04foo\32\00\01\01\01\03\ca\ff\ee"
   == "(service \"w7x7r-cok77-xa\")" : (service { foo : (text) -> (nat); foo2 : (text) -> (nat) }) "service";
 
+// service <: principal: a service reference value decodes at type `principal`
+// (identical wire encoding). The reverse (a principal at `service {}`) is rejected above.
+assert blob "DIDL\01\69\00\01\00\01\03\ca\ff\ee" == "(principal \"w7x7r-cok77-xa\")" : (principal) "service {} value decodes at principal";
+assert blob "DIDL\02\6a\01\71\01\7d\00\69\01\03foo\00\01\01\01\03\ca\ff\ee"
+  == "(principal \"w7x7r-cok77-xa\")" : (principal) "service {foo} value decodes at principal";
+// ...but `empty` (bottom) must NOT be accepted as a principal wire type: although
+// `empty <: principal` holds, an `empty`-typed value carries no bytes, so admitting
+// it would let a payload declare wire type `empty` yet be decoded as a principal
+// from arbitrary trailing bytes. Same trailing bytes as the `\68` principal above.
+assert blob "DIDL\00\01\6f\01\03\ca\ff\ee" !: (principal) "principal: reject empty (bottom) wire type";
+// A recursive service type (its method returns the service itself) still decodes
+// at `principal`: the wire type unrolls to a `service` head and only the
+// PrincipalBytes are read from the value stream.
+assert blob "DIDL\02\69\01\01m\01\6a\00\01\01\00\01\00\01\03\ca\ff\ee"
+  == "(principal \"w7x7r-cok77-xa\")" : (principal) "recursive service value decodes at principal";
+// Only `principal`/`service` wire types coerce to `principal`; other reference and
+// aggregate wire types are rejected (they do not share the PrincipalBytes encoding).
+assert blob "DIDL\01\6a\00\00\00\01\00\01\01\03\ca\ff\ee\01\61" !: (principal) "principal: reject func wire type";
+assert blob "DIDL\01\6c\00\01\00"                               !: (principal) "principal: reject record wire type";
+assert blob "DIDL\01\6e\7d\01\00\00"                            !: (principal) "principal: reject opt wire type";
+
 assert blob "DIDL\02\6a\01\71\01\7d\00\69\03\03foo\00\04foo\32\00\01\01\01\03\ca\ff\ee" !: (service { foo : (text) -> (nat); foo2 : (text) -> (nat) }) "service: too long";
 assert blob "DIDL\02\6a\01\71\01\7d\00\69\01\03foo\00\04foo\32\00\01\01\01\03\ca\ff\ee" !: (service { foo : (text) -> (nat); foo2 : (text) -> (nat) }) "service: too short";
 assert blob "DIDL\02\6a\01\71\01\7d\00\69\02\04foo\32\00\03foo\00\01\01\01\03\ca\ff\ee" !: (service { foo : (text) -> (nat); foo2 : (text) -> (nat) }) "service: unsorted";
diff --git a/test/subtypes.test.did b/test/subtypes.test.did
index cd92605a8..e22f42f18 100644
--- a/test/subtypes.test.did
+++ b/test/subtypes.test.did
@@ -157,6 +157,19 @@ assert blob "DIDL\02\6a\00\01\01\00\6d\01\01\00\01\01\00\01m"
 assert blob "DIDL\03\6a\00\01\01\00\6d\02\6d\02\01\00\01\01\00\01m"
    == "(opt func \"aaaaa-aa\".m)" : (opt func () -> (Vec)) "vec {µ vec} <: (µ vec)";
 
+// service references: every service type is a subtype of `principal`
+// (spec: `service <actortype> <: principal`), but not vice versa.
+assert blob "DIDL\02\6a\00\01\01\00\69\00\01\00\01\01\00\01m"
+   == "(opt func \"aaaaa-aa\".m)" : (opt func () -> (principal)) "service {} <: principal";
+assert blob "DIDL\03\6a\00\01\01\00\69\01\01m\02\6a\00\00\00\01\00\01\01\00\01m"
+   == "(opt func \"aaaaa-aa\".m)" : (opt func () -> (principal)) "service {m:()->()} <: principal";
+assert blob "DIDL\01\6a\00\01\68\00\01\00\01\01\00\01m"
+   == "(null)" : (opt func () -> (service {})) "principal </: service {}";
+// a recursive (µ) service type is still <: principal (Var-alias chain resolves to
+// the service head, which is unconditionally a subtype of principal)
+assert blob "DIDL\03\6a\00\01\01\00\69\01\01m\02\6a\00\01\01\00\01\00\01\01\00\01m"
+   == "(opt func \"aaaaa-aa\".m)" : (opt func () -> (principal)) "(µ service) <: principal";
+
 // future types
 // This uses 0x67 for the “future type”; bump (well, decrement) once that
 // becomes a concrete future type