Agda 2.6.4 migration

.github/workflows/build.yml

@@ -34,7 +34,7 @@ jobs:
           nix_path: nixpkgs=channel:nixos-unstable
           extra_nix_config: |
             trusted-public-keys = hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY=
-            substituters = https://cache.nixos.org/
+            substituters = https://cache.iog.io https://cache.nixos.org/
 
       - name: Restore store
         id: cache-store-restore

default.nix

@@ -16,8 +16,8 @@ let
     src = fetchFromGitHub {
       repo = "agda-stdlib";
       owner = "input-output-hk";
-      rev = "bdfab77b179c937856c49d72321ca26e2a27d568";
-      sha256 = "+PMZjmMK5xz+3Va7RN1ErtQghzpUlzsc9JBUoL+iasc=";
+      rev = "cb72ba52dfbd4f83d1034e352eb88550a3e1f681";
+      sha256 = "+OByLIWv+pdHvWt41hniE4oeo2DJZewRyYYmNXvCix0=";
     };
   });
 
@@ -27,8 +27,8 @@ let
     src = fetchFromGitHub {
       repo = "stdlib-meta";
       owner = "input-output-hk";
-      rev = "897555aefd77c83e88492255641da3bcc4879461";
-      sha256 = "EIKcLjGdnI/6nSCI18v7kPxoojAWsz8O5d9wwol2M0w=";
+      rev = "f434542c4baf667805161eeb35e5ec772233e180";
+      sha256 = "e+gb3z+cTFW4QS0c/SQqnNVBxf9hGHKOZa/vSMkHDvw=";
     };
     meta = { };
     libraryFile = "stdlib-meta.agda-lib";

nix/sources.json

@@ -5,10 +5,10 @@
         "homepage": "",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "8276a165b9fa3db1a7a4f29ee29b680e0799b9dc",
-        "sha256": "1157f8p4lvywglcb8spwk2qwcnzs6000cqyx5s9bnkj6zmwjpqwx",
+        "rev": "caf1c4efda9aac9b6b8437d4c8c89c927dcaebee",
+        "sha256": "1v5cgnbxickfsck8jiwbmhkjbkw0iy09lam0g04jwg2yw0llqxj2",
         "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/8276a165b9fa3db1a7a4f29ee29b680e0799b9dc.tar.gz",
+        "url": "https://github.com/NixOS/nixpkgs/archive/caf1c4efda9aac9b6b8437d4c8c89c927dcaebee.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
     },
     "nixpkgs": {

nix/sources.nix

@@ -10,49 +10,50 @@ let
     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'; };
+    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; };
+    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
+        spec.ref or (
           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`!";
-      submodules = if spec ? submodules then spec.submodules else false;
+          if spec ? tag then "refs/tags/${spec.tag}" else
+          abort "In git source '${name}': Please specify `ref`, `tag` or `branch`!"
+        );
+      submodules = spec.submodules or false;
       submoduleArg =
         let
           nixSupportsSubmodules = builtins.compareVersions builtins.nixVersion "2.4" >= 0;
           emptyArgWithWarning =
-            if submodules == true
+            if submodules
             then
               builtins.trace
                 (
                   "The niv input \"${name}\" uses submodules "
                   + "but your nix's (${builtins.nixVersion}) builtins.fetchGit "
                   + "does not support them"
                 )
-                {}
-            else {};
+                { }
+            else { };
         in
-          if nixSupportsSubmodules
-          then { inherit submodules; }
-          else emptyArgWithWarning;
+        if nixSupportsSubmodules
+        then { inherit submodules; }
+        else emptyArgWithWarning;
     in
-      builtins.fetchGit
-        ({ url = spec.repo; inherit (spec) rev; inherit ref; } // submoduleArg);
+    builtins.fetchGit
+      ({ url = spec.repo; inherit (spec) rev; inherit ref; } // submoduleArg);
 
   fetch_local = spec: spec.path;
 
@@ -86,16 +87,16 @@ let
       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.
-          '';
+    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:
@@ -115,13 +116,13 @@ let
   # 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;
+      saneName = stringAsChars (c: if (builtins.match "[a-zA-Z0-9]" c) == null 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}";
+    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
 
@@ -132,7 +133,7 @@ let
   );
 
   # 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);
+  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));
@@ -143,43 +144,46 @@ let
   concatStrings = builtins.concatStringsSep "";
 
   # https://github.com/NixOS/nixpkgs/blob/8a9f58a375c401b96da862d969f66429def1d118/lib/attrsets.nix#L331
-  optionalAttrs = cond: as: if cond then as else {};
+  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;
+    if lessThan nixVersion "1.12" then
+      fetchTarball ({ inherit url; } // (optionalAttrs (name != null) { 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;
+    if lessThan nixVersion "1.12" then
+      fetchurl ({ inherit url; } // (optionalAttrs (name != null) { 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;
+    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)
+    , sources ? if sourcesFile == null then { } else builtins.fromJSON (builtins.readFile sourcesFile)
     , system ? builtins.currentSystem
     , pkgs ? mkPkgs sources system
     }: rec {
@@ -191,4 +195,4 @@ let
     };
 
 in
-mkSources (mkConfig {}) // { __functor = _: settings: mkSources (mkConfig settings); }
+mkSources (mkConfig { }) // { __functor = _: settings: mkSources (mkConfig settings); }

src/Ledger/Epoch.agda

@@ -29,8 +29,8 @@ record EpochStructure : Set₁ where
     preoEpoch = hasPreorderFromStrictPartialOrder {_<_ = _<_ on firstSlot}
       record
         { isEquivalence = isEquivalence
-        ; irrefl = λ where refl → <-irrefl refl
-        ; trans  = <-trans
+        ; irrefl = λ where refl → <-irrefl {A = Slot} refl
+        ; trans  = <-trans {A = Slot}
         ; <-resp-≈ = (λ where refl → id) , (λ where refl → id)
         }
 

src/Ledger/Gov.lagda

@@ -154,9 +154,9 @@ instance
       (yesᵈ (wf , dep) , noᵈ notNewComm) → just (_ , GOV-Propose wf dep λ isNewComm → ⊥-elim (notNewComm (_ , _ , _ , isNewComm)))
       _ → nothing
   Computational-GOV' .completeness (⟦ _ , _ , pparams ⟧ᵗ , k) s (inj₁ record { gid = aid ; role = role }) s' (GOV-Vote mem cV)
-    with lookupActionId pparams role aid s | "agda#6868"
-  ... | noᵈ ¬p | _ = ⊥-elim (¬p (⤖⇒ (fromRelated Any↔) .to (_ , ∈-fromList .from mem , refl , cV)))
-  ... | yesᵈ p | _ with ⤖⇒ (fromRelated Any↔) .from p
+    with lookupActionId pparams role aid s
+  ... | noᵈ ¬p = ⊥-elim (¬p (⤖⇒ (fromRelated Any↔) .to (_ , ∈-fromList .from mem , refl , cV)))
+  ... | yesᵈ p with ⤖⇒ (fromRelated Any↔) .from p
   ...   | (_ , mem , refl , cV) = refl
   Computational-GOV' .completeness (⟦ _ , epoch , pparams ⟧ᵗ , k) s (inj₂ record { action = a ; deposit = d }) s' (GOV-Propose wf dep newOk)
     with ¿ actionWellFormed a ≡ true × d ≡ pparams .PParams.govActionDeposit ¿ | isNewCommittee a

src/Ledger/PPUp/Properties.agda

@@ -44,7 +44,7 @@ instance
   Computational-PPUP .completeness Γ _ (just up) _ _ | PPUpdateCurrent p₁ p₂ p₃ p₄
     rewrite dec-yes ¿ Current-Property Γ up ¿ (p₁ , p₂ , p₃ , p₄) .proj₂ = refl
   Computational-PPUP .completeness Γ _ (just up) _ _ | PPUpdateFuture p₁ p₂ p₃ p₄
-    with ¿ Current-Property Γ up ¿ | ¿ Future-Property Γ up ¿ | "agda#6868"
-  ... | yes (_ , _ , ¬p₃ , _) | _ | _ = ⊥-elim $ <⇒¬>⊎≈ ¬p₃ (≤⇔<∨≈ .Equivalence.to p₃)
-  ... | no _ | yes p | _ = refl
-  ... | no _ | no ¬p | _ = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄))
+    with ¿ Current-Property Γ up ¿ | ¿ Future-Property Γ up ¿
+  ... | yes (_ , _ , ¬p₃ , _) | _ = ⊥-elim $ <⇒¬>⊎≈ {A = Slot} ¬p₃ (≤⇔<∨≈ .Equivalence.to p₃)
+  ... | no _ | yes p = refl
+  ... | no _ | no ¬p = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄))

src/Ledger/Utxo.lagda

@@ -30,7 +30,7 @@ instance
   _ = ExUnit-CommutativeMonoid
 
   HasCoin-Map : ∀ {A} → ⦃ DecEq A ⦄ → HasCoin (A ⇀ Coin)
-  HasCoin-Map .getCoin s = Σᵐᵛ[ x ← s ᶠᵐ ] x
+  HasCoin-Map .getCoin s = indexedSumᵐᵛ ⦃ +-0-commutativeMonoid ⦄ id (s ᶠᵐ)
 
 isPhaseTwoScriptAddress : Tx → Addr → Bool
 isPhaseTwoScriptAddress tx a
@@ -42,7 +42,7 @@ isPhaseTwoScriptAddress tx a
 ... | just s  = isP2Script s
 
 totExUnits : Tx → ExUnits
-totExUnits tx = Σᵐ[ x ← tx .wits .txrdmrs ᶠᵐ ] (x .proj₂ .proj₂)
+totExUnits tx = indexedSumᵐ ⦃ ExUnit-CommutativeMonoid ⦄ (λ x → x .proj₂ .proj₂) (tx .wits .txrdmrs ᶠᵐ)
   where open Tx; open TxWitnesses
 
 -- utxoEntrySizeWithoutVal = 27 words (8 bytes)
@@ -79,7 +79,7 @@ module _ (let open Tx; open TxBody) where
   outs tx = mapKeys (tx .txid ,_) (tx .txouts)
 
   balance : UTxO → Value
-  balance utxo = Σᵐᵛ[ x ← utxo ᶠᵐ ] getValue x
+  balance utxo = indexedSumᵐᵛ ⦃ Value-CommutativeMonoid ⦄ getValue (utxo ᶠᵐ)
 
   cbalance : UTxO → Coin
   cbalance utxo = coin (balance utxo)