Initial strict runtime check

.github/workflows/ci.yml

@@ -22,8 +22,8 @@ jobs:
     strategy:
       matrix:
         os: [ubuntu-latest]   # macOS-latest, windows-latest
-        cabal: [3.8]
-        ghc: [8.8.4, 8.10.7, 9.2.5, 9.4.3, 9.6.3]
+        cabal: [3.10.3]
+        ghc: [9.4.8, 9.6.6, 9.8.2, 9.10.1]
     steps:
     - uses: actions/checkout@v3
       if: github.event.action == 'opened' || github.event.action == 'synchronize' || github.event.ref == 'refs/heads/master'

CHANGELOG.md

@@ -4,6 +4,30 @@ Release notes for agda2hs v1.3
 Changes
 -------
 
+Changes to agda2hs:
+- Increased Agda base version to 2.7
+- Increased bounds to support GHC 9.8.4 and GHC 9.10.2
+- Re-implemented the canonicity check for instances to be simpler but more robust
+- Added {-# COMPILE AGDA2HS ... inline #-} pragma for marking definitions to be inlined during compilation to Haskell
+- Added {-# COMPILE AGDA2HS ... tuple #-} pragma for compiling record types in Agda to a tuple type in Haskell
+- Non-erased implicit arguments and instance arguments are now compiled to regular arguments in Haskell
+- Non-erased module parameters are now compiled to regular arguments in Haskell
+- Rank-N Haskell types are now supported
+- Added `agda2hs locate` command printing the path to the agda2hs prelude `.agda-lib` file
+
+Additions to the agda2hs Prelude:
+- New module `Haskell.Extra.Dec` for working with decidability proofs (compiled to `Bool`)
+- New module `Haskell.Extra.Refinement` for working with refinement types (compiled to the base type)
+- New module `Haskell.Extra.Erase` for working with erased types (compiled to `()`)
+- New module `Haskell.Extra.Sigma` for working with dependent pair types (compiled to tuples)
+- New module `Haskell.Extra.Loop` providing a safe `loop` function (using an erased fuel argument)
+- New module `Haskell.Extra.Delay` providing a `Delay` monad for non-termination (compiled to pure functions in Haskell)
+- New function `the` in `Haskell.Prim` for generating Haskell type annotations
+- Added properties to `Haskell.Law.Equality`: `subst`, `subst0`
+- Added properties to `Haskell.Law.Bool`: `ifFlip`, `ifTrueEqThen`, `ifFalseEqThen`
+- Added properties to `Haskell.Law.List`: `map-concatMap`, `map-<*>-recomp`, `concatMap-++-distr`
+- Added proofs that many of the instances defined in the prelude are lawful
+
 See https://github.com/agda/agda2hs/issues?q=milestone%3A1.3+is%3Apr for the full list of changes.
 
 Fixed issues

LICENSE

@@ -1,4 +1,4 @@
-Copyright 2023 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, and Henry Blanchette.
+Copyright 2024 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, and Jakob Naucke.
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
 

agda2hs.cabal

@@ -1,11 +1,11 @@
-cabal-version:       2.2
+cabal-version:       2.4
 name:                agda2hs
 version:             1.3
 license:             BSD-3-Clause
 license-file:        LICENSE
-author:              Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette
+author:              Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, and Jakob Naucke
 maintainer:          [email protected]
-copyright:           2023 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette
+copyright:           2024 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette, Viktor Csimma, Aleksander Wolska, Paul Bittner, Andreas Källberg, Bohdan Liesnikov, and Jakob Naucke
 category:            Language, Compiler
 build-type:          Simple
 synopsis:            Compiling Agda code to readable Haskell.
@@ -18,24 +18,14 @@ description:
 extra-doc-files:    CHANGELOG.md
                     README.md
 
+data-files: agda2hs.agda-lib
+            lib/**/*.agda
+
 source-repository head
   type:     git
   location: https://github.com/agda/agda2hs.git
 
-flag smuggler2
-  description: Rewrite sources to cleanup imports, and create explicit exports
-  default:     False
-  manual:      True
-
-common smuggler-options
-  if flag(smuggler2)
-    ghc-options: -fplugin=Smuggler2.Plugin
-                 -fplugin-opt=Smuggler2.Plugin:MinimiseImports
-                 -fplugin-opt=Smuggler2.Plugin:NoExportProcessing
-    build-depends: smuggler2 >= 0.3 && < 0.4
-
 executable agda2hs
-  import:              smuggler-options
   hs-source-dirs:      src
   main-is:             Main.hs
   other-modules:       Agda2Hs.AgdaUtils,
@@ -47,6 +37,7 @@ executable agda2hs
                        Agda2Hs.Compile.Name,
                        Agda2Hs.Compile.Postulate,
                        Agda2Hs.Compile.Record,
+                       Agda2Hs.Compile.RuntimeCheckUtils,
                        Agda2Hs.Compile.Term,
                        Agda2Hs.Compile.Type,
                        Agda2Hs.Compile.TypeDefinition,
@@ -60,12 +51,13 @@ executable agda2hs
                        AgdaInternals,
                        Paths_agda2hs
   autogen-modules:     Paths_agda2hs
-  build-depends:       base                 >= 4.13    && < 4.20,
+  build-depends:       base                 >= 4.13    && < 4.21,
                        Agda                 >= 2.7.0   && < 2.8.0,
                        bytestring           >= 0.11.5  && < 0.13,
                        containers           >= 0.6     && < 0.8,
                        unordered-containers >= 0.2.19  && < 0.3,
-                       mtl                  >= 2.2     && < 2.3 || >= 2.3.1,
+                       mtl                 (>= 2.2     && < 2.3)
+                                        || (>= 2.3.1   && < 2.4),
                        transformers         >= 0.6     && < 0.7,
                        monad-control        >= 1.0     && < 1.1,
                        directory            >= 1.2.6.2 && < 1.4,
@@ -75,7 +67,7 @@ executable agda2hs
                        text                 >= 2.0.2   && < 2.2,
                        deepseq              >= 1.4.4   && < 1.6,
                        yaml                 >= 0.11    && < 0.12,
-                       aeson                >= 2.2     && < 2.3,
+                       aeson                >= 2.0.3   && < 2.3,
   default-language:    Haskell2010
   default-extensions:  LambdaCase
                        RecordWildCards

docs/source/features.md

@@ -299,7 +299,7 @@ five = (id :: Natural -> Natural) 5
 (0-Quantity)=
 ## 0-Quantity Parameters
 
-Parameters can be annotated with a _quantity_ of either `0` or `ω` (the default quantity is `ω` if no quantity is explicitly annotated). Such parameters are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them.
+Parameters can be annotated with a _quantity_ of either `0` or `ω` (the default quantity is `ω` if no quantity is explicitly annotated). Parameters annotated with `0` are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them.
 
 Agda:
 ```agda

docs/source/introduction.md

@@ -15,7 +15,29 @@
   - you can navigate the library in [HTML format](https://agda.github.io/agda2hs/lib/),
     along with a comprehensive [test suite](https://agda.github.io/agda2hs/test/)
 
-### Installation
+### Installation with Cabal
+
+agda2hs is released [on Hackage](https://hackage.haskell.org/package/agda2hs),
+and can be installed with Cabal:
+
+```sh
+cabal install agda2hs
+```
+
+Once installed, the agda2hs prelude bundled with agda2hs
+can be registered in the Agda config using the `agda2hs locate` command:
+
+```sh
+agda2hs locate >> ~/.agda/libaries
+```
+
+Optionally, the agda2hs prelude can also be added as a default global import:
+
+```sh
+echo agda2hs >> ~/.agda/defaults
+```
+
+### Manual installation
 
 Let `DIR` be the directory in which you start running these shell commands.
 ```sh

flake.nix

@@ -20,14 +20,14 @@
             '';
             src = ./.;
           };
+        # options provides a way to jailbreak for packages that use agda2hs
         agda2hs-pkg = options:
           pkgs.haskellPackages.haskellSrc2nix {
             name = "agda2hs";
             src = ./.;
             extraCabal2nixOptions = options; #"--jailbreak"
         };
-        # jailbreaking here because otherwise aeson has to be overridden and that triggers recompilation of a lot of dependencies
-        agda2hs-hs = pkgs.haskellPackages.callPackage (agda2hs-pkg "--jailbreak") {};
+        agda2hs-hs = pkgs.haskellPackages.callPackage (agda2hs-pkg "") {};
         agda2hs-expr = import ./agda2hs.nix;
         agda2hs = pkgs.callPackage agda2hs-expr {
             inherit self;

lib/Haskell/Extra/Dec.agda

@@ -35,7 +35,8 @@ Dec : ∀ {ℓ} → @0 Set ℓ → Set ℓ
 Dec P = ∃ Bool (Reflects P)
 {-# COMPILE AGDA2HS Dec inline #-}
 
-mapDec : @0 (a → b)
+mapDec : {@0 a b : Set}
+       → @0 (a → b)
        → @0 (b → a)
        → Dec a → Dec b
 mapDec f g (True  ⟨ x ⟩) = True  ⟨ f x   ⟩

lib/Haskell/Extra/Dec/Instances.agda

@@ -0,0 +1,80 @@
+module Haskell.Extra.Dec.Instances where
+
+open import Haskell.Prelude
+open import Haskell.Prim
+open import Haskell.Extra.Dec
+open import Haskell.Extra.Refinement
+
+variable
+  ℓ' : Level
+  A : Set ℓ
+  B : A → Set ℓ'
+  x : A
+  xs : List A
+  p : Bool
+
+instance
+  decIsTrue : Dec (IsTrue p)
+  decIsTrue {False} = False ⟨ (λ ()) ⟩
+  decIsTrue {True} = True ⟨ IsTrue.itsTrue ⟩
+  -- could specify transparent but this is incompatible with the instance search result
+  {-# COMPILE AGDA2HS decIsTrue #-}
+
+  decIsFalse : Dec (IsFalse p)
+  decIsFalse {False} = True ⟨ IsFalse.itsFalse ⟩
+  decIsFalse {True} = False ⟨ (λ ()) ⟩
+  {-# COMPILE AGDA2HS decIsFalse #-}
+
+  decNonEmpty : {xs : List a} → Dec (NonEmpty xs)
+  decNonEmpty {xs = []} = False ⟨ (λ ()) ⟩
+  decNonEmpty {xs = _ ∷ _} = True ⟨ NonEmpty.itsNonEmpty ⟩
+  {-# COMPILE AGDA2HS decNonEmpty #-}
+
+allNoHead : (B x → ⊥) → All B (x ∷ xs) → ⊥
+allNoHead ni allCons = ni it
+
+allNoTail : (All B xs → ⊥) → All B (x ∷ xs) → ⊥
+allNoTail np allCons = np it
+
+interleaved mutual
+  instance
+    -- must name these variables explicitly or Agda2Hs gets confused
+    decAll : ∀ {a : Set ℓ} {B : a → Set ℓ'} {xs} ⦃ p : ∀ {x} → Dec (B x) ⦄ → Dec (All B xs)
+
+  decAllTail : ∀ {a : Set ℓ} {B : a → Set ℓ'} {@0 x} {@0 xs} ⦃ @0 i : B x ⦄ → Dec (All B xs) → Dec (All B (x ∷ xs))
+  decAllTail (False ⟨ p ⟩) = False ⟨ allNoTail p ⟩
+  decAllTail (True ⟨ p ⟩) = True ⟨ allCons ⦃ is = p ⦄ ⟩
+
+  decAllHead : ∀ {a : Set ℓ} {B : a → Set ℓ'} {@0 x} {xs} → ⦃ Dec (B x) ⦄ → ⦃ p : ∀ {x} → Dec (B x) ⦄ → Dec (All B (x ∷ xs))
+  decAllHead ⦃ False ⟨ i ⟩ ⦄ = False ⟨ allNoHead i ⟩
+  decAllHead ⦃ True ⟨ i ⟩ ⦄ = decAllTail ⦃ i = i ⦄ decAll
+
+  decAll {xs = []} = True ⟨ allNil ⟩
+  decAll {xs = x ∷ xs} = decAllHead
+
+  {-# COMPILE AGDA2HS decAll #-}
+  {-# COMPILE AGDA2HS decAllTail #-}
+  {-# COMPILE AGDA2HS decAllHead #-}
+
+anyNone : (B x → ⊥) → (Any B xs → ⊥) → Any B (x ∷ xs) → ⊥
+anyNone notHere _ anyHere = notHere it
+anyNone _ notThere anyThere = notThere it
+
+interleaved mutual
+  instance
+    decAny : ∀ {a : Set ℓ} {B : a → Set ℓ'} {xs} ⦃ p : ∀ {x} → Dec (B x) ⦄ → Dec (Any B xs)
+
+  decAnyTail : ∀ {a : Set ℓ} {B : a → Set ℓ'} {@0 x} {@0 xs} (@0 i : B x → ⊥) → Dec (Any B xs) → Dec (Any B (x ∷ xs))
+  decAnyTail i (False ⟨ p ⟩) = False ⟨ anyNone i p ⟩
+  decAnyTail _ (True ⟨ p ⟩) = True ⟨ anyThere ⦃ is = p ⦄ ⟩
+
+  decAnyHead : ∀ {a : Set ℓ} {B : a → Set ℓ'} {@0 x} {xs} → ⦃ Dec (B x) ⦄ → ⦃ p : ∀ {x} → Dec (B x) ⦄ → Dec (Any B (x ∷ xs))
+  decAnyHead ⦃ False ⟨ i ⟩ ⦄ = decAnyTail i decAny
+  decAnyHead ⦃ True ⟨ i ⟩ ⦄ = True ⟨ anyHere ⦃ i = i ⦄ ⟩
+
+  decAny {xs = []} = False ⟨ (λ ()) ⟩
+  decAny {xs = x ∷ xs} = decAnyHead
+
+  {-# COMPILE AGDA2HS decAny #-}
+  {-# COMPILE AGDA2HS decAnyTail #-}
+  {-# COMPILE AGDA2HS decAnyHead #-}