From 293306eaeefb6464969464473e21629a595fa3a2 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Mon, 23 Sep 2024 17:32:26 +0200
Subject: [PATCH 01/21] Lower version bound of aeson to 2.0.3

---
 agda2hs.cabal | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/agda2hs.cabal b/agda2hs.cabal
index b85576db..79828f8a 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -75,7 +75,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

From 148cbd280fc076db08a6f5308881fd0fd3d36163 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 24 Sep 2024 13:19:39 +0200
Subject: [PATCH 02/21] Add support for GHC 9.10.2

---
 agda2hs.cabal          | 2 +-
 src/Agda2Hs/Compile.hs | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/agda2hs.cabal b/agda2hs.cabal
index 79828f8a..8e0acc5f 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -60,7 +60,7 @@ 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,
diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs
index 2a2941e7..ddc5ec8c 100644
--- a/src/Agda2Hs/Compile.hs
+++ b/src/Agda2Hs/Compile.hs
@@ -14,6 +14,8 @@ import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Monad.Signature ( isInlineFun )
+import Agda.Utils.Impossible
+import Agda.Utils.List
 import Agda.Utils.Null
 import Agda.Utils.Monad ( whenM, anyM, when )
 
@@ -131,5 +133,5 @@ verifyOutput _ _ _ m ls = do
               Hs.RecDecl _ n _ -> n
           duplicateCons = filter ((> 1) . length) . group . sort  $ allCons
       when (length duplicateCons > 0) $
-        genericDocError =<< vcat (map (\x -> text $ "Cannot generate multiple constructors with the same identifier: " <> Hs.prettyPrint (head x)) duplicateCons)
+        genericDocError =<< vcat (map (\x -> text $ "Cannot generate multiple constructors with the same identifier: " <> Hs.prettyPrint (headWithDefault __IMPOSSIBLE__ x)) duplicateCons)
       return (length duplicateCons == 0)

From 429a9e3ef6e26928ea1ea5a82a2ad0ef386cb0f2 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 24 Sep 2024 13:19:57 +0200
Subject: [PATCH 03/21] Update GHC and Cabal versions for CI

---
 .github/workflows/ci.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 22bfd3a4..3017e2ec 100644
--- a/.github/workflows/ci.yml
+++ b/.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'

From aafa987c1728c56c1a59aba56dd58be8ecb4c047 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 24 Sep 2024 15:20:16 +0200
Subject: [PATCH 04/21] [ re #357 ] Generalize + simplify rule for compiling
 lambdas to partial type applications

---
 src/Agda2Hs/Compile/Type.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index 889c0f73..ecf58342 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -141,9 +141,9 @@ compileType t = do
          -- Rewrite `\x -> (a -> x)` to `(->) a`
          | Hs.TyFun _ a (Hs.TyVar _ y) <- body
          , y == x0 -> return $ Hs.TyApp () (Hs.TyCon () $ Hs.Special () $ Hs.FunCon ()) a
-         -- Rewrite `\x -> ((->) x)` to `(->)`
-         | Hs.TyApp _ (Hs.TyCon _ (Hs.Special _ (Hs.FunCon _))) (Hs.TyVar _ y) <- body
-         , y == x0 -> return $ Hs.TyCon () $ Hs.Special () $ Hs.FunCon ()
+         -- Rewrite `\x -> f x` to `f`
+         | Hs.TyApp _ f (Hs.TyVar _ y) <- body
+         , y == x0 -> return f
          | otherwise -> genericDocError =<< text "Not supported: type-level lambda" <+> prettyTCM t
 
     _ -> fail

From 80734767d3c1f73037e3d6246d3d2879b65e6801 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 24 Sep 2024 15:21:27 +0200
Subject: [PATCH 05/21] [ re #357 ] Erase type arguments of `mapDec`

The types a and b do not appear in Haskell code, so they should be marked as erased
---
 lib/Haskell/Extra/Dec.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/lib/Haskell/Extra/Dec.agda b/lib/Haskell/Extra/Dec.agda
index 5b2bd810..189ab353 100644
--- a/lib/Haskell/Extra/Dec.agda
+++ b/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   ⟩

From 3e7026157eb2ea3d1c74f558ee61dde05880638e Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 24 Sep 2024 16:33:05 +0200
Subject: [PATCH 06/21] Add change log for agda2hs 1.3

---
 CHANGELOG.md | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b1a82e51..79083de0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,29 @@ 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
+
+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

From a8a743ac764f6dd8ba8855caa0bc995940f55cec Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 24 Sep 2024 16:33:31 +0200
Subject: [PATCH 07/21] Add new contributors to the license file

---
 LICENSE | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LICENSE b/LICENSE
index 563d1232..b6fe7375 100644
--- a/LICENSE
+++ b/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:
 

From e461c05a75995c6f34379d011513b659e8bad0b1 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 24 Sep 2024 16:43:47 +0200
Subject: [PATCH 08/21] Remove (unmaintained) Smuggler tool from cabal file

---
 agda2hs.cabal | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/agda2hs.cabal b/agda2hs.cabal
index 8e0acc5f..262c2729 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -22,20 +22,7 @@ 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,

From d934308248be9bcfa12e65e419b1dbc6f0b436b8 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 24 Sep 2024 16:44:20 +0200
Subject: [PATCH 09/21] Add missing upper bound for mtl package

---
 agda2hs.cabal | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/agda2hs.cabal b/agda2hs.cabal
index 262c2729..679c91fa 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -52,7 +52,8 @@ executable agda2hs
                        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,

From 2b72ccb752accf2906c252c28839bbcae30d6f62 Mon Sep 17 00:00:00 2001
From: Bohdan <17168103+liesnikov@users.noreply.github.com>
Date: Tue, 24 Sep 2024 17:10:04 +0200
Subject: [PATCH 10/21] remove the jailbreak now that aeson bounds are relaxed

---
 flake.nix | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/flake.nix b/flake.nix
index 2c35db9e..3780f466 100644
--- a/flake.nix
+++ b/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;

From 770f209c3e1aa94ba9d34c1488379e83190d589d Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 24 Sep 2024 16:49:48 +0200
Subject: [PATCH 11/21] Update author list in agda2hs.cabal

---
 agda2hs.cabal | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/agda2hs.cabal b/agda2hs.cabal
index 679c91fa..93ac52bd 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -3,9 +3,9 @@ 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:          jesper@sikanda.be
-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.

From a5552b6f3d19a2c0a35a1778a00f8076d663de2b Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Wed, 25 Sep 2024 10:07:08 +0200
Subject: [PATCH 12/21] [ #308 ] Already fixed by new canonicity check, adding
 test case

---
 test/AllTests.agda      |  2 ++
 test/Issue308.agda      | 22 ++++++++++++++++++++++
 test/golden/AllTests.hs |  1 +
 test/golden/Issue308.hs | 11 +++++++++++
 4 files changed, 36 insertions(+)
 create mode 100644 test/Issue308.agda
 create mode 100644 test/golden/Issue308.hs

diff --git a/test/AllTests.agda b/test/AllTests.agda
index c62f9f24..721e2fd6 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -91,6 +91,7 @@ import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon
+import Issue308
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -179,4 +180,5 @@ import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon
+import Issue308
 #-}
diff --git a/test/Issue308.agda b/test/Issue308.agda
new file mode 100644
index 00000000..ddd05f40
--- /dev/null
+++ b/test/Issue308.agda
@@ -0,0 +1,22 @@
+open import Haskell.Prelude
+
+record Class (a : Set) : Set where
+  field
+    foo : a → a
+open Class {{...}} public
+{-# COMPILE AGDA2HS Class class #-}
+
+module M1 (@0 X : Set) where
+
+  instance
+    ClassInt : Class Int
+    ClassInt .foo = _+ 1
+  {-# COMPILE AGDA2HS ClassInt #-}
+
+module M2 (@0 X : Set) where
+
+  open M1 X
+
+  tester : Int
+  tester = foo 41
+  {-# COMPILE AGDA2HS tester #-}
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index f970e50c..0f7d8576 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -86,4 +86,5 @@ import ErasedPatternLambda
 import CustomTuples
 import ProjectionLike
 import FunCon
+import Issue308
 
diff --git a/test/golden/Issue308.hs b/test/golden/Issue308.hs
new file mode 100644
index 00000000..8dd7f11b
--- /dev/null
+++ b/test/golden/Issue308.hs
@@ -0,0 +1,11 @@
+module Issue308 where
+
+class Class a where
+    foo :: a -> a
+
+instance Class Int where
+    foo = (+ 1)
+
+tester :: Int
+tester = foo 41
+

From 0c087ab9affbc27e602464a628f58ee7bf9d434c Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Tue, 1 Oct 2024 11:15:57 +0200
Subject: [PATCH 13/21] [ fix #370 ] add locate command, data-files in cabal
 config

---
 agda2hs.cabal |  5 ++++-
 src/Main.hs   | 19 +++++++++++++------
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/agda2hs.cabal b/agda2hs.cabal
index 93ac52bd..7e177075 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -1,4 +1,4 @@
-cabal-version:       2.2
+cabal-version:       2.4
 name:                agda2hs
 version:             1.3
 license:             BSD-3-Clause
@@ -18,6 +18,9 @@ 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
diff --git a/src/Main.hs b/src/Main.hs
index c8642aec..3d4827e4 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -21,7 +21,7 @@ import Agda2Hs.Config ( checkConfig )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Render
 
-import Paths_agda2hs ( version )
+import Paths_agda2hs ( version, getDataFileName )
 
 
 -- | Agda2Hs default config
@@ -87,8 +87,15 @@ isInteractive = do
   return $ not $ null i
 
 main = do
-  -- Issue #201: disable backend when run in interactive mode
-  isInt <- isInteractive
-  if isInt
-    then runAgda [Backend backend{isEnabled = const False}]
-    else runAgda [Backend backend]
+  args <- getArgs
+
+  -- Issue #370: `agda2hs locate` will print out the path to the prelude agda-lib file
+  if args == ["locate"] then
+    putStrLn =<< getDataFileName "agda2hs.agda-lib"
+  else do
+    -- Issue #201: disable backend when run in interactive mode
+    isInt <- isInteractive
+
+    if isInt
+      then runAgda [Backend backend{isEnabled = const False}]
+      else runAgda [Backend backend]

From a686d8016419c4e0aa2193b9ea58316ba7fdb8ba Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Tue, 1 Oct 2024 11:32:26 +0200
Subject: [PATCH 14/21] update installation instructions

---
 docs/source/introduction.md | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/docs/source/introduction.md b/docs/source/introduction.md
index a81015ef..e5db0db5 100644
--- a/docs/source/introduction.md
+++ b/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

From 0412c42844b94d4d687d8bba3a29e7e815c93a2b Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Tue, 1 Oct 2024 11:41:24 +0200
Subject: [PATCH 15/21] update changelog

---
 CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 79083de0..92508833 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,7 @@ Changes to agda2hs:
 - 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`)

From afb539213772c88f45914b0fbc49df6917ad4701 Mon Sep 17 00:00:00 2001
From: anuyts <anuyts@users.noreply.github.com>
Date: Thu, 3 Oct 2024 12:42:46 +0200
Subject: [PATCH 16/21] Docs: tweak features.md

---
 docs/source/features.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/source/features.md b/docs/source/features.md
index d7675dd3..4b540cc1 100644
--- a/docs/source/features.md
+++ b/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

From 6a9885a72e9e23381dd83d81d0ddb762666423ea Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Tue, 10 Sep 2024 17:14:25 +0200
Subject: [PATCH 17/21] [ re #354 ] Do not check canonicity of erased instances

---
 src/Agda2Hs/Compile/Utils.hs | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index 9ff54f3f..a8bb62c7 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -267,10 +267,9 @@ checkInstance u = do
     checkInstanceElims = mapM_ checkInstanceElim
 
     checkInstanceElim :: Elim -> C ()
-    checkInstanceElim (Apply v) = case getHiding v of
-      Instance{} -> checkInstance $ unArg v
-      Hidden     -> return ()
-      NotHidden  -> return ()
+    checkInstanceElim (Apply v) =
+      when (isInstance v && usableQuantity v) $
+        checkInstance $ unArg v
     checkInstanceElim IApply{} = illegalInstance
     checkInstanceElim (Proj _ f) =
       unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance

From 62617a57a98a1a09b942f7fc8d14b383438de857 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Sun, 9 Jun 2024 12:36:20 +0200
Subject: [PATCH 18/21] [ fix #119 ] Throw an error when an unknown name
 appears in generated Haskell code

---
 src/Agda2Hs/Compile/ClassInstance.hs |  2 +-
 src/Agda2Hs/Compile/Name.hs          | 28 ++++++++++++++++++++++++++--
 src/Agda2Hs/Compile/Record.hs        | 12 +++++++++---
 src/Agda2Hs/Compile/Types.hs         |  2 ++
 src/Agda2Hs/Compile/Utils.hs         | 15 +++++++++++++++
 test/Delay.agda                      | 17 +++++++++++------
 test/Fail/Issue119.agda              | 13 +++++++++++++
 test/TypeOperatorImport.agda         |  8 +-------
 test/golden/Delay.hs                 | 11 ++++++++++-
 test/golden/Issue119.err             |  2 ++
 10 files changed, 90 insertions(+), 20 deletions(-)
 create mode 100644 test/Fail/Issue119.agda
 create mode 100644 test/golden/Issue119.err

diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs
index ee619d89..993b10e8 100644
--- a/src/Agda2Hs/Compile/ClassInstance.hs
+++ b/src/Agda2Hs/Compile/ClassInstance.hs
@@ -333,7 +333,7 @@ resolveStringName s = do
 lookupDefaultImplementations :: QName -> [Hs.Name ()] -> C [Definition]
 lookupDefaultImplementations recName fields = do
   let modName = qnameToMName recName
-      isField f _ = (`elem` fields) . unQual <$> compileQName f
+      isField f _ = (`elem` fields) <$> compileName (qnameName f)
   findDefinitions isField modName
 
 classMemberNames :: Definition -> C [Hs.Name ()]
diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs
index ed42dcbb..0e1f7cf0 100644
--- a/src/Agda2Hs/Compile/Name.hs
+++ b/src/Agda2Hs/Compile/Name.hs
@@ -31,8 +31,10 @@ import qualified Agda.Syntax.Common.Pretty as P
 import Agda.TypeChecking.Datatypes ( isDataOrRecordType )
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Records ( isRecordConstructor )
+import Agda.TypeChecking.Warnings ( warning )
 
 import qualified Agda.Utils.List1 as List1
+import Agda.Utils.Monad
 import Agda.Utils.Maybe ( isJust, isNothing, whenJust, fromMaybe, caseMaybeM )
 import Agda.Utils.Monad ( whenM )
 
@@ -102,11 +104,28 @@ compileQName f
       Just (r, def) | not (_recNamedCon def) -> r -- use record name for unnamed constructors
       _                                      -> f
     hf0 <- compileName (qnameName f)
-    (hf, mimpBuiltin) <- fromMaybe (hf0, Nothing) <$> isSpecialName f
+    special <- isSpecialName f
+    let (hf, mimpBuiltin) = fromMaybe (hf0, Nothing) special
+
     parent <- parentName f
     par <- traverse (compileName . qnameName) parent
     let mod0 = qnameModule $ fromMaybe f parent
     mod <- compileModuleName mod0
+
+    existsInHaskell <- orM
+      [ pure $ isJust special
+      , pure $ isPrimModule mod
+      , hasCompilePragma f
+      , isClassFunction f
+      , isWhereFunction f
+      , maybe (pure False) hasCompilePragma parent
+      ]
+
+    unless existsInHaskell $ do
+      reportSDoc "agda2hs.name" 20 $ text "DOES NOT EXIST IN HASKELL"
+      typeError $ CustomBackendError "agda2hs" $ P.text $
+        "Symbol " ++ Hs.prettyPrint hf ++ " is missing a COMPILE pragma or rewrite rule"
+
     currMod <- hsTopLevelModuleName <$> asks currModule
     let skipModule = mod == currMod
                   || isJust mimpBuiltin
@@ -185,7 +204,7 @@ compileQName f
 
     mkImport mod qual par hf maybeIsType
       -- make sure the Prelude is properly qualified
-      | any (`isPrefixOf` pp mod) primModules
+      | isPrimModule mod
       = if isQualified qual then
           let mod' = hsModuleName "Prelude"
           in (mod', Just (Import mod' qual Nothing hf maybeIsType))
@@ -193,6 +212,11 @@ compileQName f
       | otherwise
       = (mod, Just (Import mod qual par hf maybeIsType))
 
+isWhereFunction :: QName -> C Bool
+isWhereFunction f = do
+  whereMods <- asks whereModules
+  return $ any (qnameModule f `isLeChildModuleOf`) whereMods
+
 hsTopLevelModuleName :: TopLevelModuleName -> Hs.ModuleName ()
 hsTopLevelModuleName = hsModuleName . intercalate "." . map unpack
                      . List1.toList . moduleNameParts
diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs
index b82b0f4a..b7f6c180 100644
--- a/src/Agda2Hs/Compile/Record.hs
+++ b/src/Agda2Hs/Compile/Record.hs
@@ -16,7 +16,7 @@ import Agda.Syntax.Common ( Arg(unArg), defaultArg )
 import Agda.Syntax.Internal
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
-import Agda.TypeChecking.Pretty ( ($$), (<+>), text, vcat, prettyTCM )
+import Agda.TypeChecking.Pretty ( ($$), (<+>), text, vcat, prettyTCM, pretty, prettyList_ )
 import Agda.TypeChecking.Substitute ( TelV(TelV), Apply(apply) )
 import Agda.TypeChecking.Telescope
 
@@ -38,7 +38,10 @@ withMinRecord :: QName -> C a -> C a
 withMinRecord m = local $ \ e -> e { minRecordName = Just (qnameToMName m) }
 
 compileMinRecord :: [Hs.Name ()] -> QName -> C MinRecord
-compileMinRecord fieldNames m = do
+compileMinRecord fieldNames m = withMinRecord m $ do
+  reportSDoc "agda2hs.record.min" 20 $
+    text "Compiling minimal record" <+> pretty m <+>
+    text "with field names" <+> prettyList_ (map (text . pp) fieldNames)
   rdef <- getConstInfo m
   definedFields <- classMemberNames rdef
   let Record{recPars = npars, recTel = tel} = theDef rdef
@@ -48,9 +51,12 @@ compileMinRecord fieldNames m = do
   -- We can't simply compileFun here for two reasons:
   -- * it has an explicit dictionary argument
   -- * it's using the fields and definitions from the minimal record and not the parent record
-  compiled <- withMinRecord m $ addContext (defaultDom rtype) $ compileLocal $
+  compiled <- addContext (defaultDom rtype) $ compileLocal $
     fmap concat $ traverse (compileFun False) defaults
   let declMap = Map.fromList [ (definedName c, def) | def@(Hs.FunBind _ (c : _)) <- compiled ]
+  reportSDoc "agda2hs.record.min" 20 $
+    text "Done compiling minimal record" <+> pretty m <+>
+    text "defined fields: " <+> prettyList_ (map (text . pp) definedFields)
   return (definedFields, declMap)
 
 
diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs
index 2892a8ea..473c34c6 100644
--- a/src/Agda2Hs/Compile/Types.hs
+++ b/src/Agda2Hs/Compile/Types.hs
@@ -22,6 +22,7 @@ import qualified Language.Haskell.Exts.Comments as Hs
 import Agda.Compiler.Backend
 import Agda.Syntax.Position ( Range )
 import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName )
+import Agda.TypeChecking.Warnings ( MonadWarning )
 import Agda.Utils.Null
 import Agda.Utils.Impossible
 
@@ -174,6 +175,7 @@ instance MonadStConcreteNames C where
   runStConcreteNames m = rwsT $ \r s -> runStConcreteNames $ StateT $ \ns -> do
     ((x, ns'), s', w) <- runRWST (runStateT m ns) r s
     pure ((x, s', w), ns')
+instance MonadWarning C where
 instance IsString a => IsString (C a) where fromString = pure . fromString
 instance PureTCM C where
 instance Null a => Null (C a) where
diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index a8bb62c7..6d8ef53f 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -9,6 +9,7 @@ import Control.Monad.State ( put, modify )
 
 import Data.Maybe ( isJust )
 import qualified Data.Map as M
+import Data.List ( isPrefixOf )
 
 import qualified Language.Haskell.Exts as Hs
 
@@ -60,6 +61,8 @@ primModules =
   , "Haskell.Law"
   ]
 
+isPrimModule :: Hs.ModuleName () -> Bool
+isPrimModule mod = any (`isPrefixOf` pp mod) primModules
 
 concatUnzip :: [([a], [b])] -> ([a], [b])
 concatUnzip = (concat *** concat) . unzip
@@ -152,6 +155,18 @@ isErasedBaseType x = orM
   ]
   where b = El __DUMMY_SORT__ x
 
+hasCompilePragma :: QName -> C Bool
+hasCompilePragma q = processPragma q <&> \case
+  NoPragma{} -> False
+  InlinePragma{} -> True
+  DefaultPragma{} -> True
+  ClassPragma{} -> True
+  ExistingClassPragma{} -> True
+  UnboxPragma{} -> True
+  TransparentPragma{} -> True
+  NewTypePragma{} -> True
+  DerivePragma{} -> True
+
 -- Exploits the fact that the name of the record type and the name of the record module are the
 -- same, including the unique name ids.
 isClassFunction :: QName -> C Bool
diff --git a/test/Delay.agda b/test/Delay.agda
index b74ec943..3f07763f 100644
--- a/test/Delay.agda
+++ b/test/Delay.agda
@@ -8,16 +8,21 @@ open import Haskell.Extra.Delay
 open import Agda.Builtin.Size
 
 postulate
-  div : Int → Int → Int
-  mod : Int → Int → Int
+  div' : Int → Int → Int
+  mod' : Int → Int → Int
 
-even : Int → Bool
-even x = mod x 2 == 0
+{-# COMPILE AGDA2HS div' #-}
+{-# COMPILE AGDA2HS mod' #-}
+
+even' : Int → Bool
+even' x = mod' x 2 == 0
+
+{-# COMPILE AGDA2HS even' #-}
 
 collatz : ∀ {@0 j} → Int → Delay Int j
-collatz x = 
+collatz x =
   if x == 0 then now 0
-  else if even x then later (λ where .force → collatz (div x 2))
+  else if even' x then later (λ where .force → collatz (div' x 2))
   else later λ where .force → collatz (3 * x + 1)
 
 {-# COMPILE AGDA2HS collatz #-}
diff --git a/test/Fail/Issue119.agda b/test/Fail/Issue119.agda
new file mode 100644
index 00000000..70737ecc
--- /dev/null
+++ b/test/Fail/Issue119.agda
@@ -0,0 +1,13 @@
+module Fail.Issue119 where
+
+open import Haskell.Prelude
+
+aaa : Int
+aaa = 21
+
+-- Oops, forgot compile pragma for aaa
+
+bbb : Int
+bbb = aaa + aaa
+
+{-# COMPILE AGDA2HS bbb #-}
diff --git a/test/TypeOperatorImport.agda b/test/TypeOperatorImport.agda
index 42520d1a..0b6c5a70 100644
--- a/test/TypeOperatorImport.agda
+++ b/test/TypeOperatorImport.agda
@@ -2,15 +2,9 @@ module TypeOperatorImport where
 
 {-# FOREIGN AGDA2HS {-# LANGUAGE TypeOperators #-} #-}
 
-open import Agda.Builtin.Unit
-open import Agda.Builtin.Bool
-open import Haskell.Prelude using (_∘_)
+open import Haskell.Prelude hiding (_<_)
 open import TypeOperatorExport
 
-not : Bool → Bool
-not true  = false
-not false = true
-
 test1 : ⊤ < Bool
 test1 = tt
 {-# COMPILE AGDA2HS test1 #-}
diff --git a/test/golden/Delay.hs b/test/golden/Delay.hs
index 6eeaad90..88b21d48 100644
--- a/test/golden/Delay.hs
+++ b/test/golden/Delay.hs
@@ -1,7 +1,16 @@
 module Delay where
 
+div' :: Int -> Int -> Int
+div' = error "postulate: Int -> Int -> Int"
+
+mod' :: Int -> Int -> Int
+mod' = error "postulate: Int -> Int -> Int"
+
+even' :: Int -> Bool
+even' x = mod' x 2 == 0
+
 collatz :: Int -> Int
 collatz x
   = if x == 0 then 0 else
-      if even x then collatz (div x 2) else collatz (3 * x + 1)
+      if even' x then collatz (div' x 2) else collatz (3 * x + 1)
 
diff --git a/test/golden/Issue119.err b/test/golden/Issue119.err
new file mode 100644
index 00000000..3e956c4c
--- /dev/null
+++ b/test/golden/Issue119.err
@@ -0,0 +1,2 @@
+test/Fail/Issue119.agda:10,1-4
+agda2hs: Symbol aaa is missing a COMPILE pragma or rewrite rule

From e3d9ad67df3852402646663bce7b1eae977206e8 Mon Sep 17 00:00:00 2001
From: Jakob Naucke <jakob.naucke@posteo.de>
Date: Mon, 13 May 2024 18:43:18 +0200
Subject: [PATCH 19/21] Add OverloadedStrings to Record for simplicity

---
 src/Agda2Hs/Compile/Record.hs | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs
index b7f6c180..0e0fbafc 100644
--- a/src/Agda2Hs/Compile/Record.hs
+++ b/src/Agda2Hs/Compile/Record.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE OverloadedStrings #-}
 module Agda2Hs.Compile.Record where
 
 import Control.Monad ( unless, when )
@@ -88,7 +89,7 @@ compileMinRecords def sls = do
         | all (x ==) xs = return x
         | otherwise     = genericDocError =<< do
           text ("Conflicting default implementations for " ++ pp f ++ ":") $$
-            vcat [ text "-" <+> multilineText (pp d) | d <- nub (x : xs) ]
+            vcat [ "-" <+> multilineText (pp d) | d <- nub (x : xs) ]
   decls <- Map.traverseWithKey getUnique
          $ Map.unionsWith (<>) $ (map . fmap) (:| []) defaults
 
@@ -183,8 +184,8 @@ checkUnboxPragma def = do
   -- recRecursive can be used again after agda 2.6.4.2 is released
   -- see agda/agda#7042
   unless (all null recMutual) $ genericDocError
-    =<< text "Unboxed record" <+> prettyTCM (defName def)
-    <+> text "cannot be recursive"
+    =<< "Unboxed record" <+> prettyTCM (defName def)
+    <+> "cannot be recursive"
 
   TelV tel _ <- telViewUpTo recPars (defType def)
   addContext tel $ do
@@ -192,14 +193,14 @@ checkUnboxPragma def = do
     let fieldTel = recTel `apply` pars
     fields <- nonErasedFields fieldTel
     unless (length fields == 1) $ genericDocError
-      =<< text "Unboxed record" <+> prettyTCM (defName def)
-      <+> text "should have exactly one non-erased field"
+      =<< "Unboxed record" <+> prettyTCM (defName def)
+      <+> "should have exactly one non-erased field"
 
   where
     nonErasedFields :: Telescope -> C [String]
     nonErasedFields EmptyTel = return []
     nonErasedFields (ExtendTel a tel) = compileDom a >>= \case
       DODropped  -> underAbstraction a tel nonErasedFields
-      DOType -> genericDocError =<< text "Type field in unboxed record not supported"
-      DOInstance -> genericDocError =<< text "Instance field in unboxed record not supported"
+      DOType -> genericDocError =<< "Type field in unboxed record not supported"
+      DOInstance -> genericDocError =<< "Instance field in unboxed record not supported"
       DOTerm -> (absName tel:) <$> underAbstraction a tel nonErasedFields

From 2cb30b3c2f27293338c96dd1593c4c9867ef0d31 Mon Sep 17 00:00:00 2001
From: Jakob Naucke <jakob.naucke@posteo.de>
Date: Mon, 13 May 2024 18:49:11 +0200
Subject: [PATCH 20/21] Move resolveStringName to utils and make failable

for greater reuse
---
 src/Agda2Hs/Compile/ClassInstance.hs | 13 -------------
 src/Agda2Hs/Compile/Utils.hs         |  3 ++-
 2 files changed, 2 insertions(+), 14 deletions(-)

diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs
index 993b10e8..d780d266 100644
--- a/src/Agda2Hs/Compile/ClassInstance.hs
+++ b/src/Agda2Hs/Compile/ClassInstance.hs
@@ -14,14 +14,10 @@ import Language.Haskell.Exts.Extension as Hs
 import Agda.Compiler.Backend
 import Agda.Compiler.Common ( curDefs, sortDefs )
 
-import Agda.Interaction.BasicOps ( parseName )
-
 import Agda.Syntax.Common hiding ( Ranged )
 import Agda.Syntax.Internal
 import Agda.Syntax.Internal.Pattern ( patternToTerm )
-import Agda.Syntax.Position ( noRange )
 import Agda.Syntax.Scope.Base
-import Agda.Syntax.Scope.Monad ( resolveName )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
 import Agda.TypeChecking.Pretty
@@ -321,15 +317,6 @@ findDefinitions p m = do
   map snd <$> filterM (uncurry p) inMod
 
 
-resolveStringName :: String -> C QName
-resolveStringName s = do
-  cqname <- liftTCM $ parseName noRange s
-  rname  <- liftTCM $ resolveName cqname
-  case rname of
-    DefinedName _ aname _ -> return $ anameName aname
-    _ -> genericDocError =<< text ("Couldn't find " ++ s)
-
-
 lookupDefaultImplementations :: QName -> [Hs.Name ()] -> C [Definition]
 lookupDefaultImplementations recName fields = do
   let modName = qnameToMName recName
diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index 6d8ef53f..35f08a0d 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -14,13 +14,14 @@ import Data.List ( isPrefixOf )
 import qualified Language.Haskell.Exts as Hs
 
 import Agda.Compiler.Backend hiding ( Args )
+import Agda.Interaction.BasicOps ( parseName )
 
 import Agda.Syntax.Common
 import qualified Agda.Syntax.Concrete.Name as C
 import Agda.Syntax.Internal
 import Agda.Syntax.Position ( noRange )
 import Agda.Syntax.Scope.Base
-import Agda.Syntax.Scope.Monad ( bindVariable, freshConcreteName, isDatatypeModule )
+import Agda.Syntax.Scope.Monad ( bindVariable, freshConcreteName, isDatatypeModule, resolveName )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import qualified Agda.Syntax.Common.Pretty as P
 

From 205a5dfd0f7818158898db87307ca2c6f28334db Mon Sep 17 00:00:00 2001
From: Jakob Naucke <jakob.naucke@posteo.de>
Date: Wed, 10 Apr 2024 23:57:41 +0200
Subject: [PATCH 21/21] Initial strict runtime check

---
 agda2hs.cabal                                 |   1 +
 lib/Haskell/Extra/Dec/Instances.agda          |  80 +++++
 src/Agda2Hs/Compile.hs                        |  71 ++--
 src/Agda2Hs/Compile/Data.hs                   |  56 ++-
 src/Agda2Hs/Compile/Function.hs               |  34 +-
 src/Agda2Hs/Compile/Name.hs                   |  11 +-
 src/Agda2Hs/Compile/Record.hs                 |  71 +++-
 src/Agda2Hs/Compile/RuntimeCheckUtils.hs      | 339 ++++++++++++++++++
 src/Agda2Hs/Compile/Type.hs                   |   2 +-
 src/Agda2Hs/Compile/Types.hs                  |  25 +-
 src/Agda2Hs/Compile/Utils.hs                  |  39 +-
 src/Agda2Hs/HsUtils.hs                        |   3 +
 src/Agda2Hs/Render.hs                         |  51 ++-
 src/Main.hs                                   |   8 +-
 test/AllFailTests.agda                        |   2 +
 test/AllRuntimeCheckFailTests.agda            |   5 +
 test/AllRuntimeCheckTests.agda                |   5 +
 test/AllTests.agda                            |   4 +
 test/Fail/PostRtc.agda                        |   2 +
 test/Fail/RuntimeCheckArg.agda                |   7 +
 test/Fail/RuntimeCheckClass.agda              |  16 +
 test/Fail/RuntimeCheckGo.agda                 |   7 +
 test/Fail/RuntimeCheckInline.agda             |  11 +
 test/Fail/RuntimeCheckSc.agda                 |  11 +
 test/Fail/RuntimeCheckTransparent.agda        |  11 +
 test/Fail/RuntimeCheckTuple.agda              |  11 +
 test/Fail/RuntimeCheckUnboxed.agda            |  12 +
 test/Fail/RuntimeCheckUp.agda                 |   7 +
 test/Makefile                                 |  16 +-
 test/RuntimeCheckAutoImport.agda              |   7 +
 test/RuntimeCheckCallFeatures.agda            |   9 +
 test/RuntimeCheckFeatures.agda                |  87 +++++
 test/RuntimeCheckUseCases.agda                |  12 +
 test/golden/AllRuntimeCheckTests.hs           |   4 +
 test/golden/AllRuntimeCheckTests/PostRtc.hs   |   2 +
 test/golden/AllTests.hs                       |   4 +
 test/golden/PostRtc.err                       |   1 +
 test/golden/RuntimeCheckArg.err               |   2 +
 test/golden/RuntimeCheckAutoImport.hs         |  15 +
 test/golden/RuntimeCheckAutoImport/PostRtc.hs |   8 +
 test/golden/RuntimeCheckCallFeatures.hs       |   7 +
 .../RuntimeCheckCallFeatures/PostRtc.hs       |   8 +
 test/golden/RuntimeCheckClass.err             |   2 +
 test/golden/RuntimeCheckFeatures.hs           |  67 ++++
 test/golden/RuntimeCheckFeatures/PostRtc.hs   |  52 +++
 test/golden/RuntimeCheckGo.err                |   2 +
 test/golden/RuntimeCheckInline.err            |   2 +
 test/golden/RuntimeCheckSc.err                |   2 +
 test/golden/RuntimeCheckTransparent.err       |   2 +
 test/golden/RuntimeCheckTuple.err             |   2 +
 test/golden/RuntimeCheckUnboxed.err           |   2 +
 test/golden/RuntimeCheckUp.err                |   2 +
 test/golden/RuntimeCheckUseCases.hs           |  18 +
 test/golden/RuntimeCheckUseCases/PostRtc.hs   |  11 +
 54 files changed, 1148 insertions(+), 100 deletions(-)
 create mode 100644 lib/Haskell/Extra/Dec/Instances.agda
 create mode 100644 src/Agda2Hs/Compile/RuntimeCheckUtils.hs
 create mode 100644 test/AllRuntimeCheckFailTests.agda
 create mode 100644 test/AllRuntimeCheckTests.agda
 create mode 100644 test/Fail/PostRtc.agda
 create mode 100644 test/Fail/RuntimeCheckArg.agda
 create mode 100644 test/Fail/RuntimeCheckClass.agda
 create mode 100644 test/Fail/RuntimeCheckGo.agda
 create mode 100644 test/Fail/RuntimeCheckInline.agda
 create mode 100644 test/Fail/RuntimeCheckSc.agda
 create mode 100644 test/Fail/RuntimeCheckTransparent.agda
 create mode 100644 test/Fail/RuntimeCheckTuple.agda
 create mode 100644 test/Fail/RuntimeCheckUnboxed.agda
 create mode 100644 test/Fail/RuntimeCheckUp.agda
 create mode 100644 test/RuntimeCheckAutoImport.agda
 create mode 100644 test/RuntimeCheckCallFeatures.agda
 create mode 100644 test/RuntimeCheckFeatures.agda
 create mode 100644 test/RuntimeCheckUseCases.agda
 create mode 100644 test/golden/AllRuntimeCheckTests.hs
 create mode 100644 test/golden/AllRuntimeCheckTests/PostRtc.hs
 create mode 100644 test/golden/PostRtc.err
 create mode 100644 test/golden/RuntimeCheckArg.err
 create mode 100644 test/golden/RuntimeCheckAutoImport.hs
 create mode 100644 test/golden/RuntimeCheckAutoImport/PostRtc.hs
 create mode 100644 test/golden/RuntimeCheckCallFeatures.hs
 create mode 100644 test/golden/RuntimeCheckCallFeatures/PostRtc.hs
 create mode 100644 test/golden/RuntimeCheckClass.err
 create mode 100644 test/golden/RuntimeCheckFeatures.hs
 create mode 100644 test/golden/RuntimeCheckFeatures/PostRtc.hs
 create mode 100644 test/golden/RuntimeCheckGo.err
 create mode 100644 test/golden/RuntimeCheckInline.err
 create mode 100644 test/golden/RuntimeCheckSc.err
 create mode 100644 test/golden/RuntimeCheckTransparent.err
 create mode 100644 test/golden/RuntimeCheckTuple.err
 create mode 100644 test/golden/RuntimeCheckUnboxed.err
 create mode 100644 test/golden/RuntimeCheckUp.err
 create mode 100644 test/golden/RuntimeCheckUseCases.hs
 create mode 100644 test/golden/RuntimeCheckUseCases/PostRtc.hs

diff --git a/agda2hs.cabal b/agda2hs.cabal
index 7e177075..7e37dd64 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -37,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,
diff --git a/lib/Haskell/Extra/Dec/Instances.agda b/lib/Haskell/Extra/Dec/Instances.agda
new file mode 100644
index 00000000..564bcac8
--- /dev/null
+++ b/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 #-}
diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs
index ddc5ec8c..dafca2dc 100644
--- a/src/Agda2Hs/Compile.hs
+++ b/src/Agda2Hs/Compile.hs
@@ -25,16 +25,17 @@ import Agda2Hs.Compile.ClassInstance ( compileInstance )
 import Agda2Hs.Compile.Data ( compileData )
 import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlinePragma )
 import Agda2Hs.Compile.Postulate ( compilePostulate )
-import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma )
+import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma, checkTuplePragma )
+import Agda2Hs.Compile.RuntimeCheckUtils ( importDec )
 import Agda2Hs.Compile.Types
-import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension, primModules, isClassName )
+import Agda2Hs.Compile.Utils
 import Agda2Hs.Pragma
 import qualified Language.Haskell.Exts.Syntax as Hs
 import qualified Language.Haskell.Exts.Pretty as Hs
 
 
-initCompileEnv :: TopLevelModuleName -> SpecialRules -> CompileEnv
-initCompileEnv tlm rewrites = CompileEnv
+initCompileEnv :: TopLevelModuleName -> Bool -> SpecialRules -> CompileEnv
+initCompileEnv tlm rtc rewrites = CompileEnv
   { currModule        = tlm
   , minRecordName     = Nothing
   , isNestedInType    = False
@@ -42,6 +43,7 @@ initCompileEnv tlm rewrites = CompileEnv
   , compilingLocal    = False
   , whereModules      = []
   , copatternsEnabled = False
+  , rtc               = rtc
   , rewrites          = rewrites
   , writeImports      = True
   }
@@ -49,8 +51,8 @@ initCompileEnv tlm rewrites = CompileEnv
 initCompileState :: CompileState
 initCompileState = CompileState { lcaseUsed = 0 }
 
-runC :: TopLevelModuleName -> SpecialRules -> C a -> TCM (a, CompileOutput)
-runC tlm rewrites c = evalRWST c (initCompileEnv tlm rewrites) initCompileState
+runC :: TopLevelModuleName -> Bool -> SpecialRules -> C a -> TCM (a, CompileOutput)
+runC tlm rtc rewrites c = evalRWST c (initCompileEnv tlm rtc rewrites) initCompileState
 
 moduleSetup :: Options -> IsMain -> TopLevelModuleName -> Maybe FilePath -> TCM (Recompile ModuleEnv ModuleRes)
 moduleSetup _ _ m _ = do
@@ -66,20 +68,22 @@ moduleSetup _ _ m _ = do
 
 compile
   :: Options -> ModuleEnv -> IsMain -> Definition
-  -> TCM (CompiledDef, CompileOutput)
-compile opts tlm _ def =
+  -> TCM (RtcDefs, CompileOutput)
+compile opts tlm _ def = do
+  when rtc importDec
   withCurrentModule (qnameModule qname)
-    $ runC tlm (optRewrites opts)
+    $ runC tlm rtc (optRewrites opts)
     $ setCurrentRangeQ qname
     $ compileAndTag <* postCompile
   where
     qname = defName def
+    rtc = optRtc opts
 
     tag []   = []
     tag code = [(nameBindingSite $ qnameName qname, code)]
 
-    compileAndTag :: C CompiledDef
-    compileAndTag = tag <$> do
+    compileAndTag :: C RtcDefs
+    compileAndTag = (tag <$>) <$> do
       p <- processPragma qname
 
       reportSDoc "agda2hs.compile" 5  $ text "Compiling definition:" <+> prettyTCM qname
@@ -91,39 +95,42 @@ compile opts tlm _ def =
       reportSDoc "agda2hs.compile" 15  $ text "Is instance?" <+> prettyTCM isInstance
 
       case (p , theDef def) of
-        (NoPragma            , _         ) -> return []
-        (ExistingClassPragma , _         ) -> return []
-        (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxPragma def
-        (TransparentPragma   , Function{}) -> [] <$ checkTransparentPragma def
-        (InlinePragma        , Function{}) -> [] <$ checkInlinePragma def
-        (TuplePragma b       , Record{}  ) -> return []
-
-        (ClassPragma ms      , Record{}  ) -> pure <$> compileRecord (ToClass ms) def
-        (NewTypePragma ds    , Record{}  ) -> pure <$> compileRecord (ToRecord True ds) def
-        (NewTypePragma ds    , Datatype{}) -> compileData True ds def
-        (DefaultPragma ds    , Datatype{}) -> compileData False ds def
-        (DerivePragma s      , _         ) | isInstance -> pure <$> compileInstance (ToDerivation s) def
-        (DefaultPragma _     , Axiom{}   ) | isInstance -> pure <$> compileInstance (ToDerivation Nothing) def
-        (DefaultPragma _     , _         ) | isInstance -> pure <$> compileInstance ToDefinition def
-        (DefaultPragma _     , Axiom{}   ) -> compilePostulate def
-        (DefaultPragma _     , Function{}) -> compileFun True def
-        (DefaultPragma ds    , Record{}  ) -> pure <$> compileRecord (ToRecord False ds) def
-
-        _ -> genericDocError =<<  text "Don't know how to compile" <+> prettyTCM (defName def)
+        (NoPragma           , _          ) -> return $ WithRtc [] []
+        (ExistingClassPragma, _          ) -> return $ WithRtc [] []
+        (DefaultPragma _    , Function {}) | not isInstance -> compileFun True def
+        (NewTypePragma ds   , Datatype {}) -> compileData True ds def
+        (DefaultPragma ds   , Datatype {}) -> compileData False ds def
+        (ClassPragma ms     , Record {}  ) -> compileRecord (ToClass ms) def
+        (NewTypePragma ds   , Record {}  ) -> compileRecord (ToRecord True ds) def
+        (DefaultPragma ds   , Record {}  ) | not isInstance -> compileRecord (ToRecord False ds) def
+        -- ^ Names that may induce runtime checks or are safe to have none
+        _ -> do
+          tellNoErased $ prettyShow $ qnameName $ defName def
+          (`WithRtc` []) <$> case (p, theDef def) of
+            (UnboxPragma s    , Record {}  ) -> [] <$ checkUnboxPragma def
+            (TuplePragma b    , Record{}   ) -> [] <$ checkTuplePragma def
+            (TransparentPragma, Function {}) -> [] <$ checkTransparentPragma def
+            (InlinePragma     , Function {}) -> [] <$ checkInlinePragma def
+            (DerivePragma s   , _          ) | isInstance -> pure <$> compileInstance (ToDerivation s) def
+            (DefaultPragma _  , Axiom {}   ) | isInstance -> pure <$> compileInstance (ToDerivation Nothing) def
+            (DefaultPragma _  , _          ) | isInstance -> pure <$> compileInstance ToDefinition def
+            (DefaultPragma _  , Axiom {}   ) -> compilePostulate def
+            _ -> genericDocError =<< text "Don't know how to compile" <+> prettyTCM (defName def)
 
     postCompile :: C ()
     postCompile = whenM (gets $ lcaseUsed >>> (> 0)) $ tellExtension Hs.LambdaCase
 
 verifyOutput ::
   Options -> ModuleEnv -> IsMain -> TopLevelModuleName
-  -> [(CompiledDef, CompileOutput)] -> TCM Bool
+  -> [(RtcDefs, CompileOutput)] -> TCM Bool
 verifyOutput _ _ _ m ls = do
   reportSDoc "agda2hs.compile" 5 $ text "Checking generated output before rendering: " <+> prettyTCM m
   ensureUniqueConstructors
   where
     ensureUniqueConstructors = do
       let allCons = do
-            (r, _) <- ls
+            -- take from concat'd definitions and runtime checks
+            r <- ls >>= (\(WithRtc d r) -> d : [r]) . fst
             (_, a) <- r
             Hs.DataDecl _ _ _ _ cons _ <- a
             Hs.QualConDecl _ _ _ con <- cons
diff --git a/src/Agda2Hs/Compile/Data.hs b/src/Agda2Hs/Compile/Data.hs
index 3a544a0a..65486a5f 100644
--- a/src/Agda2Hs/Compile/Data.hs
+++ b/src/Agda2Hs/Compile/Data.hs
@@ -1,8 +1,9 @@
 module Agda2Hs.Compile.Data where
 
-import qualified Language.Haskell.Exts.Syntax as Hs
+import qualified Language.Haskell.Exts as Hs
 
 import Control.Monad ( when )
+import Data.List ( intercalate, partition )
 import Agda.Compiler.Backend
 import Agda.Syntax.Common
 import Agda.Syntax.Internal
@@ -14,11 +15,27 @@ import Agda.TypeChecking.Substitute
 import Agda.TypeChecking.Telescope
 
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
+import Agda.Utils.Monad ( ifNotM )
 
-import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds )
+import Agda2Hs.Compile.RuntimeCheckUtils
+import Agda2Hs.Compile.Type
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.HsUtils
+data DataRtcResult
+  = NoRtc
+  | DataNoneErased String
+  | DataUncheckable
+  | DataCheckable [Hs.Decl ()]
+
+concatRtc :: [DataRtcResult] -> ([String], [Hs.Decl ()])
+concatRtc [] = ([], [])
+concatRtc (res : ress) = case res of
+  DataNoneErased s -> (s : tlNoneErased, tlCheckable)
+  DataCheckable ds -> (tlNoneErased, ds ++ tlCheckable)
+  _ -> tl
+  where
+    tl@(tlNoneErased, tlCheckable) = concatRtc ress
 
 checkNewtype :: Hs.Name () -> [Hs.QualConDecl ()] -> C ()
 checkNewtype name cs = do
@@ -27,9 +44,10 @@ checkNewtype name cs = do
     (Hs.QualConDecl () _ _ (Hs.ConDecl () cName types):_) -> checkNewtypeCon cName types
     _ -> __IMPOSSIBLE__
 
-compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()]
+compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C RtcDecls
 compileData newtyp ds def = do
-  let d = hsName $ prettyShow $ qnameName $ defName def
+  let prettyName = prettyShow $ qnameName $ defName def
+      d = hsName prettyName
   checkValidTypeName d
   let Datatype{dataPars = n, dataIxs = numIxs, dataCons = cs} = theDef def
   TelV tel t <- telViewUpTo n (defType def)
@@ -38,14 +56,21 @@ compileData newtyp ds def = do
   let params = teleArgs tel
   addContext tel $ do
     binds <- compileTeleBinds tel
-    cs <- mapM (compileConstructor params) cs
-    let hd = foldl (Hs.DHApp ()) (Hs.DHead () d) binds
+    chkdCs <- mapM (compileConstructor params) cs
+    chks <- ifNotM (emitsRtc $ defName def) (return []) $ do
+      let (noneErased, chks) = concatRtc $ map snd chkdCs
+      -- Always export data type name
+      tellNoErased $ prettyName ++ "(" ++ intercalate ", " noneErased ++ ")"
+      return chks
+
+    let cs = map fst chkdCs
+        hd = foldl (Hs.DHApp ()) (Hs.DHead () d) binds
 
     let target = if newtyp then Hs.NewType () else Hs.DataType ()
 
     when newtyp (checkNewtype d cs)
 
-    return [Hs.DataDecl () target Nothing hd cs ds]
+    return $ WithRtc [Hs.DataDecl () target Nothing hd cs ds] chks
   where
     allIndicesErased :: Type -> C ()
     allIndicesErased t = reduce (unEl t) >>= \case
@@ -56,17 +81,28 @@ compileData newtyp ds def = do
         DomForall{}     -> genericDocError =<< text "Not supported: indexed datatypes"
       _ -> return ()
 
-compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ())
+compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl (), DataRtcResult)
 compileConstructor params c = do
   reportSDoc "agda2hs.data.con" 15 $ text "compileConstructor" <+> prettyTCM c
   reportSDoc "agda2hs.data.con" 20 $ text "  params = " <+> prettyTCM params
   ty <- (`piApplyM` params) . defType =<< getConstInfo c
   reportSDoc "agda2hs.data.con" 20 $ text "  ty = " <+> prettyTCM ty
   TelV tel _ <- telView ty
-  let conName = hsName $ prettyShow $ qnameName c
+  let conString = prettyShow $ qnameName c
+      conName = hsName conString
+  smartQName <- smartConstructor c True
+
   checkValidConName conName
   args <- compileConstructorArgs tel
-  return $ Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args
+  chk <- ifNotM (emitsRtc c) (return NoRtc) $ do
+    sig <- Hs.TypeSig () [hsName $ prettyShow $ qnameName smartQName] <$> compileType (unEl ty)
+    -- export constructor name when none erased, provide signature for smart constructor if it exists
+    checkRtc tel smartQName (hsVar conString) alternatingLevels >>= \case
+      NoneErased -> return $ DataNoneErased conString
+      Uncheckable -> return DataUncheckable
+      Checkable ds -> return $ DataCheckable $ sig : ds
+
+  return (Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args, chk)
 
 compileConstructorArgs :: Telescope -> C [Hs.Type ()]
 compileConstructorArgs EmptyTel = return []
diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs
index 3366837c..d725032e 100644
--- a/src/Agda2Hs/Compile/Function.hs
+++ b/src/Agda2Hs/Compile/Function.hs
@@ -24,7 +24,7 @@ import Agda.Syntax.Scope.Monad ( isDatatypeModule )
 
 import Agda.TypeChecking.Pretty
 import Agda.TypeChecking.Substitute
-import Agda.TypeChecking.Telescope ( telView, mustBePi, piApplyM )
+import Agda.TypeChecking.Telescope
 import Agda.TypeChecking.Sort ( ifIsSort )
 import Agda.TypeChecking.Datatypes ( getConType, isDataOrRecord )
 import Agda.TypeChecking.Records ( getDefType )
@@ -40,6 +40,7 @@ import Agda.Utils.Size ( Sized(size) )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
+import Agda2Hs.Compile.RuntimeCheckUtils
 import Agda2Hs.Compile.Term ( compileTerm, usableDom )
 import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileDomType )
 import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
@@ -97,7 +98,7 @@ compileLitNatPat = \case
 
 compileFun, compileFun'
   :: Bool -- ^ Whether the type signature shuuld also be generated
-  -> Definition -> C [Hs.Decl ()]
+  -> Definition -> C RtcDecls
 
 compileFun withSig def@Defn{..} =
   setCurrentRangeQ defName
@@ -115,7 +116,7 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
 
   ifM (endsInSort defType)
     -- if the function type ends in Sort, it's a type alias!
-    (ensureNoLocals err >> compileTypeDef x def)
+    ((`WithRtc` []) <$> (ensureNoLocals err >> compileTypeDef x def))
     -- otherwise, we have to compile clauses.
     $ do
     tel <- lookupSection m
@@ -159,7 +160,15 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
         =<< text "Functions defined with absurd patterns exclusively are not supported."
         <+> text "Use function `error` from the Haskell.Prelude instead."
 
-      return $ sig ++ [Hs.FunBind () cs]
+      let def = sig ++ [Hs.FunBind () cs]
+      chk <- ifNotM (emitsRtc defName) (return []) $ do
+        let typeTel = theTel $ telView' defType
+            success = hsVar $ prettyShow m ++ ".PostRtc." ++ prettyShow n
+        checkRtc typeTel defName success alternatingLevels >>= \case
+          NoneErased -> do tellNoErased $ prettyShow n; return []
+          Uncheckable -> return []
+          Checkable ds -> return $ sig ++ ds
+      return $ WithRtc def chk
   where
     Function{..} = theDef
     m = qnameModule defName
@@ -235,7 +244,7 @@ compileClause' curModule projName x ty c@Clause{..} = do
 
     let rhs = Hs.UnGuardedRhs () hsBody
         whereBinds | null whereDecls = Nothing
-                   | otherwise       = Just $ Hs.BDecls () (concat whereDecls)
+                   | otherwise       = Just $ Hs.BDecls () (concatMap defn whereDecls)
         match = case (x, ps) of
           (Hs.Symbol{}, p : q : ps) -> Hs.InfixMatch () p x (q : ps) rhs whereBinds
           _                         -> Hs.Match () x ps rhs whereBinds
@@ -373,13 +382,20 @@ withClauseLocals curModule c@Clause{..} k = do
 
 -- | Ensure a definition can be defined as transparent.
 checkTransparentPragma :: Definition -> C ()
-checkTransparentPragma def = compileFun False def >>= \case
+checkTransparentPragma def = do
+  whenM (andM [emitsRtc $ defName def, not <$> checkNoneErased tele alternatingLevels]) $ genericDocError =<<
+        "Cannot make function" <+> prettyTCM (defName def) <+> "transparent." <+>
+        "Transparent functions cannot have erased arguments with runtime checking."
+  compiledFun <- defn <$> compileFun False def
+  case compiledFun of
     [Hs.FunBind _ cls] ->
       mapM_ checkTransparentClause cls
     [Hs.TypeDecl _ hd b] ->
       checkTransparentTypeDef hd b
     _ -> __IMPOSSIBLE__
   where
+    tele = theTel $ telView' $ defType def
+
     checkTransparentClause :: Hs.Match () -> C ()
     checkTransparentClause = \case
       Hs.Match _ _ [p] (Hs.UnGuardedRhs _ e) _ | patToExp p == Just e -> return ()
@@ -396,8 +412,12 @@ checkTransparentPragma def = compileFun False def >>= \case
 
 -- | Ensure a definition can be defined as inline.
 checkInlinePragma :: Definition -> C ()
-checkInlinePragma def@Defn{defName = f} = do
+checkInlinePragma def@Defn{defName = f, defType = ty} = do
   let Function{funClauses = cs} = theDef def
+      typeTel = theTel $ telView' ty
+  whenM (andM [emitsRtc $ defName def, not <$> checkNoneErased typeTel alternatingLevels]) $ genericDocError =<<
+        "Cannot make function" <+> prettyTCM (defName def) <+> "inlinable." <+>
+        "Inline functions cannot have erased arguments with runtime checking."
   case filter (isJust . clauseBody) cs of
     [c] ->
       unlessM (allowedPats (namedClausePats c)) $ genericDocError =<<
diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs
index 0e1f7cf0..7f5beea2 100644
--- a/src/Agda2Hs/Compile/Name.hs
+++ b/src/Agda2Hs/Compile/Name.hs
@@ -36,7 +36,7 @@ import Agda.TypeChecking.Warnings ( warning )
 import qualified Agda.Utils.List1 as List1
 import Agda.Utils.Monad
 import Agda.Utils.Maybe ( isJust, isNothing, whenJust, fromMaybe, caseMaybeM )
-import Agda.Utils.Monad ( whenM )
+import Agda.Utils.Monad ( ifNotM, whenM )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Types
@@ -126,18 +126,21 @@ compileQName f
       typeError $ CustomBackendError "agda2hs" $ P.text $
         "Symbol " ++ Hs.prettyPrint hf ++ " is missing a COMPILE pragma or rewrite rule"
 
+    modRtc <- ifNotM (emitsRtc f) (return mod) $ case mod of
+      Hs.ModuleName () s -> do
+        return $ Hs.ModuleName () $ s ++ ".PostRtc"
     currMod <- hsTopLevelModuleName <$> asks currModule
     let skipModule = mod == currMod
                   || isJust mimpBuiltin
                   || prettyShow mod0 `elem` primMonadModules
     qual <- if | skipModule -> return Unqualified
-               | otherwise  -> getQualifier (fromMaybe f parent) mod
+               | otherwise  -> getQualifier (fromMaybe f parent) modRtc
     -- we only calculate this when dealing with type operators; usually that's where 'type' prefixes are needed in imports
     namespace <- (case hf of
           Hs.Symbol _ _ -> getNamespace f
           Hs.Ident  _ _ -> return (Hs.NoNamespace ()))
     let
-      (mod', mimp) = mkImport mod qual par hf namespace
+      (mod', mimp) = mkImport modRtc qual par hf namespace
       qf = qualify mod' hf qual
 
     -- add (possibly qualified) import
@@ -150,7 +153,7 @@ compileQName f
       ++ "\nhaskell name: " ++ Hs.prettyPrint hf
       ++ "\nparent name: " ++ prettyShow parent
       ++ "\nmod0: " ++ prettyShow mod0
-      ++ "\nmodule name: " ++ Hs.prettyPrint mod
+      ++ "\nmodule name: " ++ Hs.prettyPrint modRtc
       ++ "\ncurrent module: " ++ Hs.prettyPrint currMod
       ++ "\nqualifier: " ++ prettyShow (fmap (fmap pp) qual)
       ++ "\n(qualified) haskell name: " ++ pp qf
diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs
index 0e0fbafc..3e550688 100644
--- a/src/Agda2Hs/Compile/Record.hs
+++ b/src/Agda2Hs/Compile/Record.hs
@@ -4,7 +4,7 @@ module Agda2Hs.Compile.Record where
 import Control.Monad ( unless, when )
 import Control.Monad.Reader ( MonadReader(local) )
 
-import Data.List ( (\\), nub )
+import Data.List ( (\\), intercalate, nub )
 import Data.List.NonEmpty ( NonEmpty(..) )
 import Data.Map ( Map )
 import qualified Data.Map as Map
@@ -23,10 +23,12 @@ import Agda.TypeChecking.Telescope
 
 import Agda.Utils.Singleton
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
+import Agda.Utils.Monad ( andM, ifNotM, whenM )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.ClassInstance
 import Agda2Hs.Compile.Function ( compileFun )
+import Agda2Hs.Compile.RuntimeCheckUtils
 import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
@@ -53,7 +55,7 @@ compileMinRecord fieldNames m = withMinRecord m $ do
   -- * it has an explicit dictionary argument
   -- * it's using the fields and definitions from the minimal record and not the parent record
   compiled <- addContext (defaultDom rtype) $ compileLocal $
-    fmap concat $ traverse (compileFun False) defaults
+    concatMap defn <$> traverse (compileFun False) defaults
   let declMap = Map.fromList [ (definedName c, def) | def@(Hs.FunBind _ (c : _)) <- compiled ]
   reportSDoc "agda2hs.record.min" 20 $
     text "Done compiling minimal record" <+> pretty m <+>
@@ -97,7 +99,7 @@ compileMinRecords def sls = do
   return ([minPragma | not (null prims)] ++ Map.elems decls)
 
 
-compileRecord :: RecordTarget -> Definition -> C (Hs.Decl ())
+compileRecord :: RecordTarget -> Definition -> C RtcDecls
 compileRecord target def = do
   TelV tel _ <- telViewUpTo recPars (defType def)
   addContext tel $ do
@@ -107,24 +109,42 @@ compileRecord target def = do
     let fieldTel = snd $ splitTelescopeAt recPars recTel
     case target of
       ToClass ms -> do
-        (classConstraints, classDecls) <- compileRecFields classDecl recFields fieldTel
+        whenM (andM [emitsRtc $ defName def, not <$> checkNoneErased fieldTel recordLevels]) $ genericDocError =<<
+             "Cannot compile" <+> prettyTCM (defName def) <+> "to class." <+>
+             "Classes cannot have erased arguments with runtime checking."
+        (classConstraints, classDecls, _, _) <- compileRecFields classDecl recFields fieldTel
         let context = case classConstraints of
               []     -> Nothing
               [asst] -> Just (Hs.CxSingle () asst)
               assts  -> Just (Hs.CxTuple () assts)
         defaultDecls <- compileMinRecords def ms
-        return $ Hs.ClassDecl () context hd [] (Just (classDecls ++ map (Hs.ClsDecl ()) defaultDecls))
+        return $ WithRtc [Hs.ClassDecl () context hd [] (Just (classDecls ++ map (Hs.ClsDecl ()) defaultDecls))] []
       ToRecord newtyp ds -> do
+        smartQName <- smartConstructor (defName def) False
+
         checkValidConName cName
-        (constraints, fieldDecls) <- compileRecFields fieldDecl recFields fieldTel
+        (constraints, fieldDecls, fieldStrings, fieldTypes) <- compileRecFields fieldDecl recFields fieldTel
+
+        chk <- ifNotM (emitsRtc $ defName def) (return []) $ do
+          let scType = foldr (Hs.TyFun ()) (Hs.TyVar () $ Hs.Ident () rString) fieldTypes
+              sig = Hs.TypeSig () [hsName $ prettyShow $ qnameName smartQName] scType
+          (noneErasedCons, chk) <- checkRtc fieldTel smartQName (hsVar conString) recordLevels >>= \case
+            NoneErased -> return ([conString], [])
+            Uncheckable -> return ([], [])
+            Checkable ds -> return ([], sig : ds)
+          -- Always export record name and field names. Export constructor when it has no erased types.
+          tellNoErased $ rString ++ "(" ++ intercalate ", " (fieldStrings ++ noneErasedCons) ++ ")"
+          return chk
+
         when newtyp $ checkNewtypeCon cName fieldDecls
         let target = if newtyp then Hs.NewType () else Hs.DataType ()
-        compileDataRecord constraints fieldDecls target hd ds
-
+        (\c -> WithRtc [c] chk) <$> compileDataRecord constraints fieldDecls target hd ds
   where
-    rName = hsName $ prettyShow $ qnameName $ defName def
-    cName | recNamedCon = hsName $ prettyShow $ qnameName $ conName recConHead
-          | otherwise   = rName   -- Reuse record name for constructor if no given name
+    rString = prettyShow $ qnameName $ defName def
+    rName = hsName rString
+    conString | recNamedCon = prettyShow $ qnameName $ conName recConHead
+              | otherwise   = rString   -- Reuse record name for constructor if no given name
+    cName = hsName conString
 
     -- In Haskell, projections live in the same scope as the record type, so check here that the
     -- record module has been opened.
@@ -144,23 +164,24 @@ compileRecord target def = do
     fieldDecl n = Hs.FieldDecl () [n]
 
     compileRecFields :: (Hs.Name () -> Hs.Type () -> b)
-                     -> [Dom QName] -> Telescope -> C ([Hs.Asst ()], [b])
+                     -> [Dom QName] -> Telescope -> C ([Hs.Asst ()], [b], [String], [Hs.Type ()])
     compileRecFields decl ns tel = case (ns, tel) of
-      (_   , EmptyTel          ) -> return ([], [])
+      (_   , EmptyTel          ) -> return ([], [], [], [])
       (n:ns, ExtendTel dom tel') -> do
         hsDom <- compileDomType (absName tel') dom
-        (hsAssts, hsFields) <- underAbstraction dom tel' $ compileRecFields decl ns
+        (hsAssts, hsFields, fieldStrings, hsTypes) <- underAbstraction dom tel' $ compileRecFields decl ns
         case hsDom of
           DomType s hsA -> do
-            let fieldName = hsName $ prettyShow $ qnameName $ unDom n
+            let fieldString = prettyShow $ qnameName $ unDom n
+                fieldName = hsName fieldString
             fieldType <- addTyBang s hsA
             checkValidFunName fieldName
-            return (hsAssts, decl fieldName fieldType : hsFields)
+            return (hsAssts, decl fieldName fieldType : hsFields, fieldString : fieldStrings, hsA : hsTypes)
           DomConstraint hsA -> case target of
-            ToClass{} -> return (hsA : hsAssts , hsFields)
+            ToClass{} -> return (hsA : hsAssts, hsFields, fieldStrings, hsTypes)
             ToRecord{} -> genericError $
               "Not supported: record/class with constraint fields"
-          DomDropped -> return (hsAssts , hsFields)
+          DomDropped -> return (hsAssts, hsFields, fieldStrings, hsTypes)
           DomForall{} -> __IMPOSSIBLE__
       (_, _) -> __IMPOSSIBLE__
 
@@ -191,6 +212,9 @@ checkUnboxPragma def = do
   addContext tel $ do
     pars <- getContextArgs
     let fieldTel = recTel `apply` pars
+    whenM (andM [emitsRtc $ defName def, not <$> checkNoneErased fieldTel recordLevels]) $ genericDocError =<<
+          "Cannot make record" <+> prettyTCM (defName def) <+> "unboxed." <+>
+          "Unboxed records cannot have erased arguments in their fields with runtime checking."
     fields <- nonErasedFields fieldTel
     unless (length fields == 1) $ genericDocError
       =<< "Unboxed record" <+> prettyTCM (defName def)
@@ -204,3 +228,14 @@ checkUnboxPragma def = do
       DOType -> genericDocError =<< "Type field in unboxed record not supported"
       DOInstance -> genericDocError =<< "Instance field in unboxed record not supported"
       DOTerm -> (absName tel:) <$> underAbstraction a tel nonErasedFields
+
+checkTuplePragma :: Definition -> C ()
+checkTuplePragma def = do
+  let Record{..} = theDef def
+  TelV tel _ <- telViewUpTo recPars (defType def)
+  addContext tel $ do
+    pars <- getContextArgs
+    let fieldTel = recTel `apply` pars
+    whenM (andM [emitsRtc $ defName def, not <$> checkNoneErased fieldTel recordLevels]) $ genericDocError =<<
+          "Cannot compile record" <+> prettyTCM (defName def) <+> "as tuple." <+>
+          "Tuple records cannot have erased arguments in their fields with runtime checking."
diff --git a/src/Agda2Hs/Compile/RuntimeCheckUtils.hs b/src/Agda2Hs/Compile/RuntimeCheckUtils.hs
new file mode 100644
index 00000000..a167601a
--- /dev/null
+++ b/src/Agda2Hs/Compile/RuntimeCheckUtils.hs
@@ -0,0 +1,339 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Agda2Hs.Compile.RuntimeCheckUtils (importDec, checkNoneErased, smartConstructor, NestedLevel (Odd), alternatingLevels, recordLevels, RtcResult (..), checkRtc) where
+
+import Agda.Syntax.Common
+import Agda.Syntax.Common.Pretty (prettyShow)
+import qualified Agda.Syntax.Concrete as AC
+import Agda.Syntax.Concrete.Definitions (NiceEnv (NiceEnv), niceDeclarations, runNice)
+import qualified Agda.Syntax.Concrete.Name as AN
+import Agda.Syntax.Internal
+import Agda.Syntax.Position (noRange)
+import Agda.Syntax.Translation.ConcreteToAbstract (ToAbstract (toAbstract))
+import Agda.TypeChecking.InstanceArguments (findInstance)
+import Agda.TypeChecking.MetaVars (newInstanceMeta, newLevelMeta)
+import Agda.TypeChecking.Monad
+import Agda.TypeChecking.Pretty (PrettyTCM (prettyTCM), (<+>))
+import Agda.TypeChecking.Reduce (instantiate)
+import Agda.TypeChecking.Substitute (telView', theTel)
+import Agda.TypeChecking.Telescope (splitTelescopeAt)
+import Agda.Utils.Impossible (__IMPOSSIBLE__)
+import Agda.Utils.List (initLast)
+import qualified Agda.Utils.List1 as List1
+import Agda.Utils.Monad (allM, partitionM, unless)
+import Agda2Hs.Compile.Term (compileTerm)
+import Agda2Hs.Compile.Type (DomOutput (DODropped), compileDom)
+import Agda2Hs.Compile.Types (C)
+import Agda2Hs.Compile.Utils
+import Agda2Hs.HsUtils
+import Control.Monad.Except (catchError)
+import Control.Monad.State (StateT (StateT, runStateT))
+import Data.List (intersect)
+import Data.Map (empty)
+import Data.Maybe (catMaybes, fromJust, isJust)
+import Data.Tree (flatten, unfoldTree)
+import Data.Tuple (swap)
+import qualified Language.Haskell.Exts as Hs
+
+-- Import Haskell.Extra.Dec{,.Instances}
+-- based on Agda.Syntax.Translation.ConcreteToAbstract.importPrimitives
+importDec :: TCM ()
+importDec = do
+  let haskellExtra = AN.Qual (AC.simpleName "Haskell") . AN.Qual (AC.simpleName "Extra")
+      dec = AC.simpleName "Dec"
+      directives = ImportDirective noRange UseEverything [] [] Nothing
+      importDecl q = [AC.Import noRange (haskellExtra q) Nothing AC.DontOpen directives]
+      run ds = case fst $ runNice (NiceEnv True) $ niceDeclarations empty $ importDecl ds of
+        Left _ -> __IMPOSSIBLE__
+        Right ds -> toAbstract ds
+  run $ AC.QName dec
+  run $ AN.Qual dec $ AC.QName $ AC.simpleName "Instances"
+  return ()
+
+-- Retrieve constructor name and generated smart constructor qname.
+-- Takes extra argument whether one additional name should be stripped
+smartConstructor :: QName -> Bool -> C QName
+smartConstructor qname strip1 = do
+  checkNameConflict smartString
+  return smartQName
+  where
+    qnameList = qnameToList qname
+    -- data types need the name of the data type itself stripped
+    strip = if strip1 then 2 else 1
+    qualifier = List1.take (length qnameList - strip) qnameList
+    name = List1.last qnameList
+    smartString = "sc" ++ prettyShow name
+    smartName = mkName (nameBindingSite name) (nameId name) smartString
+    smartQName = qnameFromList $ List1.prependList qualifier $ smartName List1.:| []
+
+-- Only preconditions on odd levels of nesting should incur a check
+-- because only they can be violated from Haskell
+-- See Findler and Felleisen, Contracts for Higher-Order Functions, ICFP 2002
+data NestedLevel = Odd | Even
+
+-- Expected only to be used with infinite lists. Stream would be
+-- more faithful, but we use lists for dependency simplicity.
+whenOdd :: [NestedLevel] -> [a] -> [a]
+whenOdd (Odd : _) l = l
+whenOdd (Even : _) _ = []
+
+alternatingLevels :: [NestedLevel]
+alternatingLevels = cycle [Odd, Even]
+
+-- For records, both the fields and their types should be considered to be in odd position
+recordLevels :: [NestedLevel]
+recordLevels = Odd : alternatingLevels
+
+-- Runtime checks are not supported for certain pragmas.
+-- Check that the telescope has no erased types.
+checkNoneErased :: Telescope -> [NestedLevel] -> C Bool
+checkNoneErased tel ls = do
+  let doms = telToList tel
+  (erased, other) <- partitionM ((`checkTopOrDataErased` ls) . fst) $ zip doms $ map (domToTel . (snd <$>)) doms
+  (null erased &&) <$> allM other ((`checkNoneErased` ls) . snd)
+
+-- Check if a type is erased or contains an erased type within a data type or record.
+-- In this case, it should be checked.
+checkTopOrDataErased :: Dom (a, Type) -> [NestedLevel] -> C Bool
+checkTopOrDataErased d (_ : ls) = do
+  let domType = snd <$> d
+      unfold = unfoldTypes [unDom domType]
+      -- do not recurse into Pi at top level (that is still handled by caller),
+      -- but do at `Apply` levels below
+      tels = [domToTel t | Pi t _ <- map unArg unfold]
+      quantities = getQuantity d : map getQuantity unfold
+  domDropped <- (DODropped ==) <$> compileDom domType
+  (or (domDropped : [True | Quantity0 _ <- quantities]) ||) . not . and <$> mapM (`checkNoneErased` ls) tels
+
+-- External runtime check result
+data RtcResult
+  = NoneErased
+  | Uncheckable
+  | Checkable [Hs.Decl ()]
+
+-- Internal runtime check result
+data RtcResult'
+  = NoneErased'
+  | Uncheckable'
+  | -- The actual runtime check is assembled in the caller receiving an RtcResult',
+    -- because the logic at the top level is different, e.g. the declarations are
+    -- put in a `where` instead of being flattened.
+    Checkable'
+      { theirLhs :: [Hs.Pat ()],
+        theirChks :: [Hs.Exp ()],
+        theirRhs :: [Hs.Exp ()],
+        theirDecls :: [Hs.Decl ()]
+      }
+
+-- Check name induces no conflict
+checkNameConflict :: String -> C ()
+checkNameConflict s =
+  testResolveStringName s >>= \case
+    Just _ -> errorNameConflict s
+    Nothing -> return ()
+
+errorWhenConflicts :: [String] -> C ()
+errorWhenConflicts [] = pure ()
+errorWhenConflicts (c : _) = errorNameConflict c
+
+errorNameConflict :: String -> C ()
+errorNameConflict s =
+  genericDocError
+    =<< ("Illegal name" <+> prettyTCM s) <> ", conflicts with name generated for runtime checks."
+
+-- Create runtime check.
+-- Takes function name, lhs patterns, expressions for checks, expression on success,
+-- and optionally `where` binds
+createRtc :: Hs.Name () -> [Hs.Pat ()] -> [Hs.Exp ()] -> Hs.Exp () -> Maybe (Hs.Binds ()) -> Hs.Decl ()
+createRtc n args [] success = createRtc' n args $ Hs.UnGuardedRhs () success
+createRtc n args chks success =
+  createRtc' n args rhs
+  where
+    rhs = Hs.GuardedRhss () $ Hs.GuardedRhs () [Hs.Qualifier () andChks] success : notChks ++ [otherwiseChk]
+    andChks = foldr1 (\c -> Hs.InfixApp () c $ Hs.QVarOp () $ Hs.UnQual () $ Hs.Symbol () "&&") chks
+    chk2err chk =
+      let msg = "Runtime check failed: " ++ Hs.prettyPrint chk
+       in Hs.App () (hsVar "error") $ Hs.Lit () $ Hs.String () msg msg
+    errs = zip chks $ map chk2err chks
+    (nots, otherwise) = fromJust $ initLast errs
+    notChks = map (\(chk, err) -> Hs.GuardedRhs () [Hs.Qualifier () $ Hs.App () (hsVar "not") chk] err) nots
+    otherwiseChk = (\(_, err) -> Hs.GuardedRhs () [Hs.Qualifier () $ hsVar "otherwise"] err) otherwise
+
+createRtc' :: Hs.Name () -> [Hs.Pat ()] -> Hs.Rhs () -> Maybe (Hs.Binds ()) -> Hs.Decl ()
+createRtc' n args rhs binds = Hs.FunBind () [Hs.Match () n args rhs binds]
+
+{- Suffixes for `go` functions in the `where` declaration for nested
+erased arguments and `a` arguments for unnamed arguments.
+Example to show all cases:
+
+Turning
+
+tripleOdd : (((m : Nat) → @0 IsTrue (m > 0) → (((n : Nat) → @0 IsFalse (n < 1) → Nat) → Nat) → Nat) → Nat) → Nat
+
+into
+
+tripleOdd a0 = TripleOdd.PostRtc.tripleOdd (\ a1 -> a0 (go1 a1))
+  where
+    go1 up m a2
+      | decIsTrue (m > 0) = up m (\ a3 -> a2 (go0 a3))
+      | otherwise = error "Runtime check failed: decIsTrue (m > 0)"
+      where
+        go0 up n
+          | decIsFalse (n < 1) = up n
+          | otherwise = error "Runtime check failed: decIsFalse (n < 1)"
+
+has a tree of
+
+(((m : Nat) → @0 … → (((n : Nat) → @0 … → Nat) → Nat) → Nat) → Nat) → Nat ~ (0, 0)
+Reserve a0 for ((Nat → ((Nat → Nat) → Nat) → Nat) → Nat):
+  ((m : Nat) → @0 … → (((n : Nat) → @0 … → Nat) → Nat) → Nat) → Nat ~ (0, 1)
+Reserve a1 for (Nat → ((Nat → Nat) → Nat) → Nat):
+    (m : Nat) → @0 … → (((n : Nat) → @0 … → Nat) → Nat) → Nat ~ (0, 2)
+Reserve a2 for ((Nat → Nat) → Nat):
+      ((n : Nat) → @0 … → Nat) → Nat ~ (0, 3)
+Reserve a3 for (Nat → Nat):
+        (n : Nat) → @0 … → Nat ~ (0, 4)
+        ~ (0, 4), lhs = ["n"], chks = ["decIsFalse n < 1"], rhs = ["n"], decls = []
+Reserve go0 for (((Nat → Nat) → Nat) → Nat):
+      ~ (1, 4), lhs = ["a3"], chks = [], rhs = ["go0 a3"], decls = ["go0 up n = …"]
+Inline:
+    ~ (1, 4), lhs = ["m", "a2"], chks = ["decIsTrue (m > 0)"], rhs = ["m (\ a3 -> a2 (go0 a3))"], decls = ["go0 up n = …"]
+Reserve go1 for ((Nat → ((Nat → Nat) → Nat) → Nat) → Nat → ((Nat → Nat) → Nat) → Nat):
+  ~ (2, 4), lhs = ["a1"], chks = [], rhs = ["go1 a1"], decls = ["go1 up m a2 = …"]
+Inline:
+~ (2, 4), lhs = ["a0"], chks = [], rhs = ["(\ a1 -> a0 (go1 a1))"], decls = ["go1 up m a2 = …"]
+-}
+type NameIndices = (Int, Int)
+
+-- Creates a runtime check if necessary and possible, informing C accordingly.
+-- Takes telescope of type to check, name, level of nesting stream, and expression on success.
+checkRtc :: Telescope -> QName -> Hs.Exp () -> [NestedLevel] -> C RtcResult
+checkRtc tel name success lvls = do
+  (_, chk) <- checkRtc' (0, 0) tel lvls
+  case chk of
+    NoneErased' -> return NoneErased
+    Uncheckable' -> return Uncheckable
+    Checkable' {..} -> do
+      tellAllCheckable name
+      let rhs = eApp success theirRhs
+          chkName = hsName $ prettyShow $ qnameName name
+          chk = createRtc chkName theirLhs theirChks rhs $ if null theirDecls then Nothing else Just $ Hs.BDecls () theirDecls
+      return $ Checkable [chk]
+
+-- Recursively check for runtime checkability in nested types.
+-- Accumulates on name indices for `go` function and `a` argument.
+-- Takes telescope of type to check.
+checkRtc' :: NameIndices -> Telescope -> [NestedLevel] -> C (NameIndices, RtcResult')
+checkRtc' idcs tel lvls = do
+  -- Partition out arguments that are erased and at top level (those we will attempt to check)
+  (erased, call) <- partitionM ((`checkTopOrDataErased` lvls) . fst) $ zip doms telsUpTo
+  ourChks <- uncurry createGuardExp `mapM` whenOdd lvls erased
+  -- Recursively accumulate checks on arguments below top level
+  (belowIdcs, belowChks) <- mapAccumLM checkRtc'' idcs $ map (,lvls) call
+  (belowIdcs,)
+    <$> if not $ all isJust belowChks && all isJust ourChks
+      then return Uncheckable'
+      else -- all checkable or none erased
+        let (theirLhs, theirRhs, decls) = unzip3 $ catMaybes belowChks
+            theirDecls = concat decls
+            -- all checks below found an instance
+            theirChks = catMaybes ourChks
+         in if null theirDecls && null erased
+              then return NoneErased'
+              else return Checkable' {..}
+  where
+    doms = telToList tel
+    telsUpTo = map (\i -> fst $ splitTelescopeAt i tel) [0 ..]
+
+-- Check a single type for runtime checkability.
+-- Accumulates on name indices for `go` function and `a` argument.
+-- Takes domain of type and telescope up to that point for context.
+-- If checkable, returns lhs and rhs at that point plus declarations from checks below.
+checkRtc'' ::
+  NameIndices ->
+  ((Dom (ArgName, Type), Telescope), [NestedLevel]) ->
+  C (NameIndices, Maybe (Hs.Pat (), Hs.Exp (), [Hs.Decl ()]))
+checkRtc'' (goIdx, argIdx) ((d, tUpTo), _ : lvls) =
+  -- Mutual recursion with checkRtc'
+  addContext tUpTo (checkRtc' (goIdx, ourArgIdx) tAt lvls) >>= \case
+    (idcs, NoneErased') -> return (idcs, Just (ourLhs, argVar, []))
+    (idcs, Uncheckable') -> return (idcs, Nothing)
+    ((theirGoIdx, theirArgIdx), Checkable' {..}) -> do
+      let go = "go" ++ show theirGoIdx
+          conflicts = tAtNames `intersect` [go, arg, up]
+      errorWhenConflicts conflicts
+      let (ourGoIdx, ourRhs, ourRtc) =
+            if null theirChks
+              then -- inline if nothing to check at this level (consumes no `goIdx`)
+              -- e.g. `\ a3 -> a2 (go0 a3)`, continuing the example above `NameIndices`
+                (theirGoIdx, Hs.Lambda () theirLhs $ argVar `eApp` theirRhs, theirDecls)
+              else
+                let -- e.g. `up m a2`
+                    lhs = hsPat up : theirLhs
+                    -- e.g. `up m (\ a3 -> a2 (go0 a3))`
+                    rhs = hsVar up `eApp` theirRhs
+                    rtc = createRtc (hsName go) lhs theirChks rhs $ binds theirDecls
+                 in -- e.g. `go1 a1`
+                    (succ theirGoIdx, hsVar go `eApp` [argVar], [rtc])
+      return ((ourGoIdx, theirArgIdx), Just (ourLhs, ourRhs, ourRtc))
+  where
+    tAt = domToTel $ snd <$> d
+    tAtNames = map (fst . unDom) $ telToList tAt
+    name = fst $ unDom d
+    -- Use arg name if available, otherwise insert one (consumes one on `argIdx`)
+    (arg, ourArgIdx) = if name == "_" then ("a" ++ show argIdx, succ argIdx) else (name, argIdx)
+    ourLhs = hsPat arg
+    argVar = hsVar arg
+    up = "up"
+
+---- Small convenience functions
+
+-- Gather telescope from domain
+domToTel :: Dom Type -> Telescope
+domToTel = theTel . telView' . unDom
+
+-- Unfold data types and records from list of types
+unfoldTypes :: [Type] -> [Arg Term]
+unfoldTypes tys =
+  concat $
+    flatten $
+      ( \tes ->
+          let argss = [[a | Apply a <- es] | Def _ es <- tes]
+           in (concat argss, map (map unArg) argss)
+      )
+        `unfoldTree` map unEl tys
+
+-- Create binds from declarations except when empty
+binds :: [Hs.Decl ()] -> Maybe (Hs.Binds ())
+binds [] = Nothing
+binds decls = Just $ Hs.BDecls () decls
+
+-- Turn a type into its Dec version
+decify :: Type -> C Type
+decify t = do
+  dec <- resolveStringName "Haskell.Extra.Dec.Dec"
+  level <- liftTCM newLevelMeta
+  let vArg = defaultArg
+      hArg = setHiding Hidden . vArg
+  return $ t {unEl = Def dec $ map Apply [hArg $ Level level, vArg $ unEl t]}
+
+-- Failably find instances for decidable terms
+findDecInstances :: Type -> TCMT IO (Maybe Term)
+findDecInstances t =
+  do
+    (m, v) <- newInstanceMeta "" t
+    findInstance m Nothing
+    Just <$> instantiate v
+    `catchError` return (return Nothing)
+
+-- Create expression to be put in the guard
+createGuardExp :: Dom (a, Type) -> Telescope -> C (Maybe (Hs.Exp ()))
+createGuardExp dom telUpTo = addContext telUpTo $ do
+  dec <- decify $ snd $ unDom dom
+  liftTCM (findDecInstances dec) >>= traverse (compileTerm dec)
+
+-- from GHC.Utils.Monad
+mapAccumLM :: (Monad m, Traversable t) => (acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y)
+mapAccumLM f s = fmap swap . flip runStateT s . traverse f'
+  where
+    f' = StateT . (fmap . fmap) swap . flip f
diff --git a/src/Agda2Hs/Compile/Type.hs b/src/Agda2Hs/Compile/Type.hs
index ecf58342..e7dc518e 100644
--- a/src/Agda2Hs/Compile/Type.hs
+++ b/src/Agda2Hs/Compile/Type.hs
@@ -223,7 +223,7 @@ compileInlineType f args = do
     _                -> genericDocError =<< text "Could not reduce inline type alias " <+> prettyTCM f
 
 
-data DomOutput = DOInstance | DODropped | DOType | DOTerm
+data DomOutput = DOInstance | DODropped | DOType | DOTerm deriving Eq
 
 compileDom :: Dom Type -> C DomOutput
 compileDom a = do
diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs
index 473c34c6..f2683036 100644
--- a/src/Agda2Hs/Compile/Types.hs
+++ b/src/Agda2Hs/Compile/Types.hs
@@ -35,6 +35,18 @@ type Ranged a    = (Range, a)
 
 type Code = (Hs.Module Hs.SrcSpanInfo, [Hs.Comment])
 
+data WithRtc d = WithRtc {
+  defn :: d,
+  -- Runtime check
+  rtcDefn :: d
+}
+
+instance Functor WithRtc where
+  fmap f (WithRtc d r) = WithRtc (f d) (f r)
+
+type RtcDefs = WithRtc CompiledDef
+type RtcDecls = WithRtc [Hs.Decl ()]
+
 -- | Custom substitution for a given definition.
 data Rewrite = Rewrite
   { rewFrom   :: String
@@ -63,6 +75,7 @@ data Options = Options
   , optOutDir     :: Maybe FilePath
   , optConfigFile :: Maybe FilePath
   , optExtensions :: [Hs.Extension]
+  , optRtc        :: Bool
   , optRewrites   :: SpecialRules
   , optPrelude    :: PreludeOptions
   }
@@ -89,6 +102,8 @@ data CompileEnv = CompileEnv
   -- ^ the where-blocks currently in scope. Hack until Agda adds where-prominence
   , copatternsEnabled :: Bool
   -- ^ whether copatterns should be allowed when compiling patterns
+  , rtc :: Bool
+  -- ^ whether runtime checks should be emitted (uncheckable names are wrapped away)
   , rewrites :: SpecialRules
   -- ^ Special compilation rules.
   , writeImports :: Bool
@@ -126,14 +141,18 @@ data CompileOutput = CompileOutput
   -- ^ Haskell import statements.
   , haskellExtensions :: [Hs.KnownExtension]
   -- ^ Required language extensions.
+  , noErased :: [String]
+  -- ^ Names that can be exported as is wrt runtime checks because they have no erased arguments
+  , allCheckable :: [QName]
+  -- ^ Names that can be exported wrt runtime checks because all erased arguments are checkable
   }
 
 instance Semigroup CompileOutput where
-  CompileOutput imps exts <> CompileOutput imps' exts' =
-    CompileOutput (imps <> imps') (exts <> exts')
+  CompileOutput imps exts ers checks <> CompileOutput imps' exts' ers' checks' =
+    CompileOutput (imps <> imps') (exts <> exts') (ers <> ers') (checks <> checks')
 
 instance Monoid CompileOutput where
-  mempty = CompileOutput mempty mempty
+  mempty = CompileOutput mempty mempty mempty mempty
 
 -- | State used while compiling a single module.
 newtype CompileState = CompileState
diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index 35f08a0d..d8ce07a4 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -39,9 +39,11 @@ import Agda.TypeChecking.Substitute ( Subst, TelV(TelV), Apply(..) )
 import Agda.TypeChecking.Telescope ( telView )
 
 import Agda.Utils.Lens ( (<&>) )
+import qualified Agda.Utils.List1 as List1
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
 import Agda.Utils.Singleton
+import Agda.Utils.Tuple ( (-*-) )
 
 import AgdaInternals
 import Agda2Hs.AgdaUtils ( (~~) )
@@ -337,10 +339,16 @@ checkValidConName x = unless (validConName x) $ genericDocError =<< do
   text "Invalid name for Haskell constructor: " <+> text (Hs.prettyPrint x)
 
 tellImport :: Import -> C ()
-tellImport imp = tell $ CompileOutput [imp] []
+tellImport imp = tell $ CompileOutput [imp] [] [] []
 
 tellExtension :: Hs.KnownExtension -> C ()
-tellExtension pr = tell $ CompileOutput [] [pr]
+tellExtension pr = tell $ CompileOutput [] [pr] [] []
+
+tellNoErased :: String -> C ()
+tellNoErased er = tell $ CompileOutput [] [] [er] []
+
+tellAllCheckable :: QName -> C ()
+tellAllCheckable chk = tell $ CompileOutput [] [] [] [chk]
 
 tellUnboxedTuples :: Hs.Boxed -> C ()
 tellUnboxedTuples Hs.Boxed = return ()
@@ -372,7 +380,7 @@ checkFixityLevel name (Related lvl) =
                          <+> text "for operator"   <+> prettyTCM name
     else pure (Just (round lvl))
 
-maybePrependFixity :: QName -> Fixity -> C [Hs.Decl ()] -> C [Hs.Decl ()]
+maybePrependFixity :: QName -> Fixity -> C RtcDecls -> C RtcDecls
 maybePrependFixity n f comp | f /= noFixity = do
   hsLvl <- checkFixityLevel n (fixityLevel f)
   let x = hsName $ prettyShow $ qnameName n
@@ -380,7 +388,8 @@ maybePrependFixity n f comp | f /= noFixity = do
         NonAssoc   -> Hs.AssocNone ()
         LeftAssoc  -> Hs.AssocLeft ()
         RightAssoc -> Hs.AssocRight ()
-  (Hs.InfixDecl () hsAssoc hsLvl [Hs.VarOp () x]:) <$> comp
+  let head = (Hs.InfixDecl () hsAssoc hsLvl [Hs.VarOp () x]:)
+  (head <$>) <$> comp
 maybePrependFixity n f comp = comp
 
 
@@ -404,3 +413,25 @@ checkNoAsPatterns = \case
 
 noWriteImports :: C a -> C a
 noWriteImports = local $ \e -> e { writeImports = False }
+
+testResolveStringName :: String -> C (Maybe QName)
+testResolveStringName s = do
+  cqname <- liftTCM $ parseName noRange s
+  rname <- liftTCM $ resolveName cqname
+  case rname of
+    DefinedName _ aname _ -> return $ Just $ anameName aname
+    _ -> return Nothing
+
+resolveStringName :: String -> C QName
+resolveStringName s = do
+  testResolveStringName s >>= \case
+    Just aname -> return aname
+    Nothing -> genericDocError =<< text ("Couldn't find " ++ s)
+
+-- Check if runtime checks should be emitted, i.e. the feature is
+-- enabled and the name is not in the trusted computing base.
+-- This is not included in RuntimeCheckUtils.hs for dependency reasons.
+emitsRtc :: QName -> C Bool
+emitsRtc qname = do
+  topName <- prettyTCM $ List1.head $ mnameToList1 $ qnameModule qname
+  asks $ (show topName /= "Haskell" &&) . rtc
diff --git a/src/Agda2Hs/HsUtils.hs b/src/Agda2Hs/HsUtils.hs
index e09a5a8b..3835a6ef 100644
--- a/src/Agda2Hs/HsUtils.hs
+++ b/src/Agda2Hs/HsUtils.hs
@@ -78,6 +78,9 @@ extToName = Ident () . show
 hsModuleName :: String -> ModuleName ()
 hsModuleName = ModuleName ()
 
+hsPat :: String -> Pat ()
+hsPat = PVar () . hsName
+
 isOp :: QName () -> Bool
 isOp (UnQual _ Symbol{}) = True
 isOp (Special _ Cons{})  = True
diff --git a/src/Agda2Hs/Render.hs b/src/Agda2Hs/Render.hs
index 4cd979d2..220954b9 100644
--- a/src/Agda2Hs/Render.hs
+++ b/src/Agda2Hs/Render.hs
@@ -1,15 +1,17 @@
+{-# LANGUAGE OverloadedStrings #-}
+
 module Agda2Hs.Render where
 
-import Control.Monad ( unless )
+import Control.Monad ( when, unless )
 import Control.Monad.IO.Class ( MonadIO(liftIO) )
 
 import Data.Function ( on )
-import Data.List ( sortBy, nub )
+import Data.List ( intercalate, sortBy, nub )
 import Data.Maybe ( fromMaybe, isNothing )
 import Data.Set ( Set )
 import qualified Data.Set as Set
 
-import System.FilePath ( takeDirectory, (</>) )
+import System.FilePath ( takeDirectory, takeBaseName, joinPath, (</>) )
 import System.Directory ( createDirectoryIfMissing )
 
 import qualified Language.Haskell.Exts.SrcLoc as Hs
@@ -28,6 +30,7 @@ import Agda.Syntax.TopLevelModuleName
 import Agda.Syntax.Common.Pretty ( prettyShow )
 
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
+import qualified Agda.Utils.List1 as List1
 
 import Agda2Hs.Compile
 import Agda2Hs.Compile.Types
@@ -128,21 +131,25 @@ prettyShowImportDecl (Hs.ImportDecl _ m qual src safe mbPkg mbName mbSpecs) =
           (Hs.Ident  _ _)                     -> rest
 
 writeModule :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName
-            -> [(CompiledDef, CompileOutput)] -> TCM ModuleRes
+            -> [(RtcDefs, CompileOutput)] -> TCM ModuleRes
 writeModule opts _ isMain m outs = do
   code <- getForeignPragmas (optExtensions opts)
-  let mod  = prettyShow m
-      (cdefs, impss, extss) = unzip3 $ flip map outs $
-        \(cdef, CompileOutput imps exts) -> (cdef, imps, exts)
-      defs = concatMap defBlock cdefs ++ codeBlocks code
-      imps = concat impss
-      exts = concat extss
+  let mod = prettyShow m
+      defs = concatMap (defBlock . defn . fst) outs ++ codeBlocks code
+      chkdefs = concatMap (defBlock . rtcDefn . fst) outs
+      output = map snd outs
+      imps = concatMap imports output
+      exts = concatMap haskellExtensions output
+      safe = concatMap noErased output
+      chkd = map prettyShow $ concatMap allCheckable output
   unless (null code && null defs && isMain == NotMain) $ do
 
     let unlines' [] = []
         unlines' ss = unlines ss ++ "\n"
 
     let preOpts@PreludeOpts{..} = optPrelude opts
+        nameParts = rawModuleNameParts $ rawTopLevelModuleName m
+        rtc = optRtc opts && List1.head nameParts `notElem` ["Agda", "Haskell"]
 
     -- if the prelude is supposed to be implicit,
     -- or the prelude imports have been fixed in the config file,
@@ -163,15 +170,29 @@ writeModule opts _ isMain m outs = do
 
     -- The comments make it hard to generate and pretty print a full module
     hsFile <- moduleFileName opts m
-
-    let output = concat
+    when (rtc && "PostRtc" `elem` List1.toList nameParts) $ do
+      genericDocError =<< ("Illegal module name" <+> prettyTCM m)
+        <> ", conflicts with name generated for runtime checks."
+    let postFile = joinPath [takeDirectory hsFile, takeBaseName hsFile, "PostRtc.hs"]
+        renderedExps = intercalate ", " $ safe ++ chkd
+
+    -- "pre" runtime check output (_the_ output if RTC disabled)
+    let preOutput = concat
+          [ "module " ++ mod ++ " (" ++ renderedExps ++ ") where\n\n"
+          , autoImports
+          , "import " ++ mod ++ ".PostRtc\n\n"
+          , renderBlocks chkdefs
+          ]
+        output = concat
           [ renderLangExts exts
           , renderBlocks $ codePragmas code
-          , "module " ++ mod ++ " where\n\n"
+          , "module " ++ mod ++ (if rtc then ".PostRtc" else "") ++ " where\n\n"
           , autoImports
           , renderBlocks defs
           ]
 
     reportSLn "" 1 $ "Writing " ++ hsFile
-
-    liftIO $ ensureDirectory hsFile >> writeFile hsFile output
+    liftIO $ ensureDirectory hsFile >> writeFile hsFile (if rtc then preOutput else output)
+    when rtc $ do
+      reportSLn "" 1 $ "Writing " ++ postFile
+      liftIO $ ensureDirectory postFile >> writeFile postFile output
diff --git a/src/Main.hs b/src/Main.hs
index 3d4827e4..98f7b704 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -31,6 +31,7 @@ defaultOptions = Options
   , optOutDir     = Nothing
   , optConfigFile = Nothing
   , optExtensions = []
+  , optRtc        = False
   , optPrelude    = PreludeOpts False Nothing []
     -- by default the Prelude is imported explicitly
   , optRewrites   = defaultSpecialRules
@@ -49,8 +50,10 @@ configOpt src opts = return opts { optConfigFile = Just src }
 extensionOpt :: String -> Flag Options
 extensionOpt ext opts = return opts { optExtensions = Hs.parseExtension ext : optExtensions opts }
 
+rtcOpt :: Flag Options
+rtcOpt opts = return opts { optRtc = True }
 
-backend :: Backend' Options Options ModuleEnv ModuleRes (CompiledDef, CompileOutput)
+backend :: Backend' Options Options ModuleEnv ModuleRes (RtcDefs, CompileOutput)
 backend = Backend'
   { backendName           = "agda2hs"
   , backendVersion        = Just (showVersion version)
@@ -64,6 +67,9 @@ backend = Backend'
           "Write Haskell code to DIR. (default: project root)"
       , Option ['X'] [] (ReqArg extensionOpt "EXTENSION")
           "Enable Haskell language EXTENSION. Affects parsing of Haskell code in FOREIGN blocks."
+      , Option [] ["runtime-check"] (NoArg rtcOpt)
+          "Enable runtime checking of erased arguments. \
+          \Hides constructs with undecidable erased arguments away."
       , Option [] ["config"] (ReqArg configOpt "FILE")
           "Provide additional configuration to agda2hs with a YAML file."
       ]
diff --git a/test/AllFailTests.agda b/test/AllFailTests.agda
index 24deabc8..72fbbdf0 100644
--- a/test/AllFailTests.agda
+++ b/test/AllFailTests.agda
@@ -1,6 +1,8 @@
 {-# OPTIONS --guardedness #-}
 module AllFailTests where
 
+import AllRuntimeCheckFailTests
+
 import Fail.ClashingImport
 import Fail.Issue142
 import Fail.MatchOnDelay
diff --git a/test/AllRuntimeCheckFailTests.agda b/test/AllRuntimeCheckFailTests.agda
new file mode 100644
index 00000000..8ede18e7
--- /dev/null
+++ b/test/AllRuntimeCheckFailTests.agda
@@ -0,0 +1,5 @@
+module AllRuntimeCheckFailTests where
+
+import Fail.RuntimeCheckClass
+import Fail.RuntimeCheckInline
+import Fail.PostRtc.RuntimeCheckModuleName
diff --git a/test/AllRuntimeCheckTests.agda b/test/AllRuntimeCheckTests.agda
new file mode 100644
index 00000000..10ec318d
--- /dev/null
+++ b/test/AllRuntimeCheckTests.agda
@@ -0,0 +1,5 @@
+module AllRuntimeCheckTests where
+
+import RuntimeCheckCallFeatures
+import RuntimeCheckUseCases
+import RuntimeCheckAutoImport
diff --git a/test/AllTests.agda b/test/AllTests.agda
index 721e2fd6..2eca6e8d 100644
--- a/test/AllTests.agda
+++ b/test/AllTests.agda
@@ -181,4 +181,8 @@ import CustomTuples
 import ProjectionLike
 import FunCon
 import Issue308
+
+import RuntimeCheckCallFeatures
+import RuntimeCheckUseCases
+import RuntimeCheckAutoImport
 #-}
diff --git a/test/Fail/PostRtc.agda b/test/Fail/PostRtc.agda
new file mode 100644
index 00000000..9e0b48f9
--- /dev/null
+++ b/test/Fail/PostRtc.agda
@@ -0,0 +1,2 @@
+-- is an illegal module name in runtime checking
+module Fail.PostRtc where
diff --git a/test/Fail/RuntimeCheckArg.agda b/test/Fail/RuntimeCheckArg.agda
new file mode 100644
index 00000000..f3f8c9fe
--- /dev/null
+++ b/test/Fail/RuntimeCheckArg.agda
@@ -0,0 +1,7 @@
+module Fail.RuntimeCheckArg where
+
+open import Haskell.Prelude
+
+conflict : ((Nat → (a1 : Nat) → @0 IsTrue (a1 > 0) → Nat) → Nat) → Nat
+conflict _ = 0
+{-# COMPILE AGDA2HS conflict #-}
diff --git a/test/Fail/RuntimeCheckClass.agda b/test/Fail/RuntimeCheckClass.agda
new file mode 100644
index 00000000..2b299cb0
--- /dev/null
+++ b/test/Fail/RuntimeCheckClass.agda
@@ -0,0 +1,16 @@
+module Fail.RuntimeCheckClass where
+
+open import Haskell.Prelude
+
+record Class : Set where
+  field
+    theField : Nat
+open Class public
+{-# COMPILE AGDA2HS Class class #-}
+
+record NoClass : Set where
+  field
+    classFst : Nat
+    classSnd : ⦃@0 _ : IsTrue (classFst > 0)⦄ → Nat
+open NoClass public
+{-# COMPILE AGDA2HS NoClass class #-}
diff --git a/test/Fail/RuntimeCheckGo.agda b/test/Fail/RuntimeCheckGo.agda
new file mode 100644
index 00000000..25511450
--- /dev/null
+++ b/test/Fail/RuntimeCheckGo.agda
@@ -0,0 +1,7 @@
+module Fail.RuntimeCheckGo where
+
+open import Haskell.Prelude
+
+conflict : (((go0 : Nat) → @0 IsTrue (go0 > 0) → Nat) → Nat) → Nat
+conflict _ = 0
+{-# COMPILE AGDA2HS conflict #-}
diff --git a/test/Fail/RuntimeCheckInline.agda b/test/Fail/RuntimeCheckInline.agda
new file mode 100644
index 00000000..112bf373
--- /dev/null
+++ b/test/Fail/RuntimeCheckInline.agda
@@ -0,0 +1,11 @@
+module Fail.RuntimeCheckInline where
+
+open import Haskell.Prelude
+
+inlinable : Nat
+inlinable = 0
+{-# COMPILE AGDA2HS inlinable inline #-}
+
+notInlinable : (x : Nat) → ⦃@0 _ : IsTrue (x > 0)⦄ → Nat
+notInlinable _ = 0
+{-# COMPILE AGDA2HS notInlinable inline #-}
diff --git a/test/Fail/RuntimeCheckSc.agda b/test/Fail/RuntimeCheckSc.agda
new file mode 100644
index 00000000..c76a77b0
--- /dev/null
+++ b/test/Fail/RuntimeCheckSc.agda
@@ -0,0 +1,11 @@
+module Fail.RuntimeCheckSc where
+
+open import Haskell.Prelude
+
+data Dat : Set where
+  Conflict : ((x : Nat) ⦃@0 _ : IsTrue (x > 0)⦄ → Nat) → Dat
+{-# COMPILE AGDA2HS Dat #-}
+
+scConflict : Nat
+scConflict = 0
+{-# COMPILE AGDA2HS scConflict #-}
diff --git a/test/Fail/RuntimeCheckTransparent.agda b/test/Fail/RuntimeCheckTransparent.agda
new file mode 100644
index 00000000..cceb3574
--- /dev/null
+++ b/test/Fail/RuntimeCheckTransparent.agda
@@ -0,0 +1,11 @@
+module Fail.RuntimeCheckTransparent where
+
+open import Haskell.Prelude
+
+transparent : Nat → Nat
+transparent n = n
+{-# COMPILE AGDA2HS transparent transparent #-}
+
+noTransparent : (x : Nat) → ⦃@0 _ : IsTrue (x > 0)⦄ → Nat
+noTransparent n = n
+{-# COMPILE AGDA2HS noTransparent transparent #-}
diff --git a/test/Fail/RuntimeCheckTuple.agda b/test/Fail/RuntimeCheckTuple.agda
new file mode 100644
index 00000000..5b834347
--- /dev/null
+++ b/test/Fail/RuntimeCheckTuple.agda
@@ -0,0 +1,11 @@
+module Fail.RuntimeCheckTuple where
+
+open import Haskell.Prelude
+
+record CanTuple : Set where
+  field tupleField : Nat
+{-# COMPILE AGDA2HS CanTuple tuple #-}
+
+record CantTuple : Set where
+  field tupleField : (@0 _ : IsTrue Bool.true) → Nat
+{-# COMPILE AGDA2HS CantTuple tuple #-}
diff --git a/test/Fail/RuntimeCheckUnboxed.agda b/test/Fail/RuntimeCheckUnboxed.agda
new file mode 100644
index 00000000..c035e8cb
--- /dev/null
+++ b/test/Fail/RuntimeCheckUnboxed.agda
@@ -0,0 +1,12 @@
+module Fail.RuntimeCheckUnboxed where
+
+open import Haskell.Prelude
+
+record Unboxable : Set where
+  -- The erasure is in an evenly nested position, keeping the record unboxable.
+  field unboxField : (@0 _ : IsTrue Bool.true → Nat) → Nat
+{-# COMPILE AGDA2HS Unboxable unboxed #-}
+
+record NotUnboxable : Set where
+  field noUnboxField : (@0 _ : IsTrue Bool.true) → Nat
+{-# COMPILE AGDA2HS NotUnboxable unboxed #-}
diff --git a/test/Fail/RuntimeCheckUp.agda b/test/Fail/RuntimeCheckUp.agda
new file mode 100644
index 00000000..d68da756
--- /dev/null
+++ b/test/Fail/RuntimeCheckUp.agda
@@ -0,0 +1,7 @@
+module Fail.RuntimeCheckUp where
+
+open import Haskell.Prelude
+
+conflict : (((up : Nat) → @0 IsTrue (up > 0) → Nat) → Nat) → Nat
+conflict _ = 0
+{-# COMPILE AGDA2HS conflict #-}
diff --git a/test/Makefile b/test/Makefile
index ed87e47a..acfdc500 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -2,6 +2,7 @@ AGDA2HS=./agda2hs +RTS -M2G -RTS
 ROOT=$(shell cd ..; pwd)/
 MAIN=AllTests
 FAIL_MAIN=AllFailTests
+MAIN_RTC=AllRuntimeCheckTests
 
 .PHONY : default allTests print-fail fail compare golden \
 	html renderTranslations clean force-recompile
@@ -10,27 +11,32 @@ default : compare
 
 build/%.hs : %.agda *.agda Fail/*.agda Cubical/*.agda agda2hs
 	@echo == Compiling tests ==
-	$(AGDA2HS) $< -o build
+	(rtc=$$(echo $< | grep RuntimeCheck); $(AGDA2HS) $${rtc:+--runtime-check} $< -o build)
 
-allTests : build/$(MAIN).hs
+allTests : build/$(MAIN).hs build/$(MAIN_RTC).hs
 	@echo == Running ghc ==
-	@(cd build && ghc -fno-code $(MAIN).hs)
+	@(cd build && ghc -fno-code $(MAIN).hs && \
+	              ghc -fno-code $(rtc) $(MAIN_RTC).hs)
 
 print-fail :
 	@echo == Failing tests ==
+	mkdir -p build
 
 fail : print-fail $(patsubst Fail/%.agda,build/%.err,$(wildcard Fail/*.agda))
 
 build/%.err : Fail/%.agda agda2hs
 	@echo Compiling $<
-	@($(AGDA2HS) $< -o build -v0 && echo "UNEXPECTED SUCCESS" || true) | sed -e 's:'$(ROOT)'::g' > $@
+	@(rtc=$$(echo $< | grep -E '(RuntimeCheck|PostRtc)'); $(AGDA2HS) $${rtc:+--runtime-check} $< -o build -v0 \
+			&& echo "UNEXPECTED SUCCESS" || true) \
+		| sed -e 's:'$(ROOT)'::g' > $@
 
 compare : allTests fail
 	@echo == Comparing output ==
+	@cp -r build/Haskell golden
 	@diff -r build golden
 
 golden :
-	@cp build/*.hs build/Cubical/*.hs build/*.err golden
+	@cp -r build/* golden
 
 html : allTests fail html/index.html html/fail/index.html renderTranslations
 
diff --git a/test/RuntimeCheckAutoImport.agda b/test/RuntimeCheckAutoImport.agda
new file mode 100644
index 00000000..f3084d5d
--- /dev/null
+++ b/test/RuntimeCheckAutoImport.agda
@@ -0,0 +1,7 @@
+module RuntimeCheckAutoImport where
+
+open import Haskell.Prelude
+
+simpleFun : (x : Nat) ⦃@0 _ : IsTrue (x > 0)⦄ → Nat
+simpleFun _ = 0
+{-# COMPILE AGDA2HS simpleFun #-}
diff --git a/test/RuntimeCheckCallFeatures.agda b/test/RuntimeCheckCallFeatures.agda
new file mode 100644
index 00000000..d6fcd80b
--- /dev/null
+++ b/test/RuntimeCheckCallFeatures.agda
@@ -0,0 +1,9 @@
+{-# OPTIONS --sized-types #-}
+module RuntimeCheckCallFeatures where
+
+open import Haskell.Prelude
+open import RuntimeCheckFeatures
+
+externalFunCaller : Nat
+externalFunCaller = simpleFun 1
+{-# COMPILE AGDA2HS externalFunCaller #-}
diff --git a/test/RuntimeCheckFeatures.agda b/test/RuntimeCheckFeatures.agda
new file mode 100644
index 00000000..ddeaa14c
--- /dev/null
+++ b/test/RuntimeCheckFeatures.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --sized-types #-}
+module RuntimeCheckFeatures where
+
+open import Haskell.Prelude
+open import Haskell.Extra.Delay
+open import Haskell.Extra.Erase
+open import Haskell.Extra.Dec.Instances
+
+noneErasedFun : Nat → Nat
+noneErasedFun _ = 1
+{-# COMPILE AGDA2HS noneErasedFun #-}
+
+noDecInstance : ⦃ x : Nat ⦄ → @0 ⦃ HasResult x (now x) ⦄ → Nat
+noDecInstance = 0
+{-# COMPILE AGDA2HS noDecInstance #-}
+
+simpleFun : (x : Nat) → @0 ⦃ IsTrue (x > 0) ⦄ → Nat
+simpleFun _ = 0
+{-# COMPILE AGDA2HS simpleFun #-}
+
+simpleFunCaller : Nat
+simpleFunCaller = simpleFun 1
+{-# COMPILE AGDA2HS simpleFunCaller #-}
+
+-- Even precondition
+singleEven : ((x : Nat) → @0 IsTrue (x > 0) → Nat) → Nat
+singleEven _ = 0
+{-# COMPILE AGDA2HS singleEven #-}
+
+-- Double odd precondition with backreferencing and same-level nested checks
+doubleOdd : (x : Nat) → (((y : Nat) → @0 IsFalse (x < y) → Nat) → Nat) → (((y : Nat) → @0 IsFalse (x < y) → Nat) → Nat) → Nat
+doubleOdd _ _ _ = 0
+{-# COMPILE AGDA2HS doubleOdd #-}
+
+-- Triple odd precondition with multi-level checks
+tripleOdd : (((m : Nat) → @0 IsTrue (m > 0) → (((n : Nat) → @0 IsFalse (n < 1) → Nat) → Nat) → Nat) → Nat) → Nat
+tripleOdd _ = 0
+{-# COMPILE AGDA2HS tripleOdd #-}
+
+-- If you want to deconstruct in Haskell, you have to write deconstructors in Agda.
+-- Making the constructor available would enable bypassing the smart constructor.
+data Dat : Set where
+  Con : (x : Nat) → @0 IsTrue (x > 0) → Dat
+  NoneErasedCon : Nat → Dat
+{-# COMPILE AGDA2HS Dat #-}
+
+-- Term variables in type parameter not supported, so not showcased here
+record Rec : Set where
+  field
+    recFst : Nat
+    recSnd : @0 IsTrue (recFst > 0) → Nat
+open Rec public
+{-# COMPILE AGDA2HS Rec #-}
+
+record Newt : Set where
+  field
+    theField : (x : Nat) → @0 IsTrue (x > 0) → Nat
+open Newt public
+{-# COMPILE AGDA2HS Newt newtype #-}
+
+record NoneErasedNewt : Set where
+  field
+    noneErasedField : Nat
+open NoneErasedNewt public
+{-# COMPILE AGDA2HS NoneErasedNewt newtype #-}
+
+record ErasedField : Set where
+  field
+    erasedFst : Nat
+    @0 erasedSnd : IsTrue (erasedFst > 0)
+open ErasedField public
+{-# COMPILE AGDA2HS ErasedField #-}
+
+-- Should not be exported due to erased within
+listErased : (fs : List (((n : Nat) → @0 ⦃ IsFalse (n < 1) ⦄ → Nat) → Nat)) → Nat
+listErased _ = 0
+{-# COMPILE AGDA2HS listErased #-}
+
+-- Should not be exported due to erased (part of TCB)
+eraseTCB : (n : Nat) → @0 Erase (IsFalse (1 < n)) → Nat
+eraseTCB n iErased = 0
+{-# COMPILE AGDA2HS eraseTCB #-}
+
+-- Should be exported despite TCB record containing an erasure because erasure is not in a critical position
+fUnzip : {a b : Set} {f : Set → Set} → ⦃ Functor f ⦄ → f (a × b) → (f a × f b)
+fUnzip xs = (fmap fst xs , fmap snd xs)
+{-# COMPILE AGDA2HS fUnzip #-}
diff --git a/test/RuntimeCheckUseCases.agda b/test/RuntimeCheckUseCases.agda
new file mode 100644
index 00000000..0590787d
--- /dev/null
+++ b/test/RuntimeCheckUseCases.agda
@@ -0,0 +1,12 @@
+module RuntimeCheckUseCases where
+
+open import Haskell.Prelude
+open import Haskell.Extra.Dec.Instances
+
+subtractFromGreater : (x y : Nat) ⦃@0 _ : IsFalse (x < y)⦄ → Nat
+subtractFromGreater x y = x - y
+{-# COMPILE AGDA2HS subtractFromGreater #-}
+
+headOfNonEmpty : (xs : List Nat) ⦃@0 _ : NonEmpty xs ⦄ → Nat
+headOfNonEmpty (x ∷ _) = x
+{-# COMPILE AGDA2HS headOfNonEmpty #-}
diff --git a/test/golden/AllRuntimeCheckTests.hs b/test/golden/AllRuntimeCheckTests.hs
new file mode 100644
index 00000000..7973c927
--- /dev/null
+++ b/test/golden/AllRuntimeCheckTests.hs
@@ -0,0 +1,4 @@
+module AllRuntimeCheckTests () where
+
+import AllRuntimeCheckTests.PostRtc
+
diff --git a/test/golden/AllRuntimeCheckTests/PostRtc.hs b/test/golden/AllRuntimeCheckTests/PostRtc.hs
new file mode 100644
index 00000000..e5c33b35
--- /dev/null
+++ b/test/golden/AllRuntimeCheckTests/PostRtc.hs
@@ -0,0 +1,2 @@
+module AllRuntimeCheckTests.PostRtc where
+
diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs
index 0f7d8576..b649a506 100644
--- a/test/golden/AllTests.hs
+++ b/test/golden/AllTests.hs
@@ -88,3 +88,7 @@ import ProjectionLike
 import FunCon
 import Issue308
 
+import RuntimeCheckCallFeatures
+import RuntimeCheckUseCases
+import RuntimeCheckAutoImport
+
diff --git a/test/golden/PostRtc.err b/test/golden/PostRtc.err
new file mode 100644
index 00000000..701f8dc3
--- /dev/null
+++ b/test/golden/PostRtc.err
@@ -0,0 +1 @@
+Illegal module name Fail.PostRtc, conflicts with name generated for runtime checks.
diff --git a/test/golden/RuntimeCheckArg.err b/test/golden/RuntimeCheckArg.err
new file mode 100644
index 00000000..229d0abf
--- /dev/null
+++ b/test/golden/RuntimeCheckArg.err
@@ -0,0 +1,2 @@
+test/Fail/RuntimeCheckArg.agda:5,1-9
+Illegal name a1, conflicts with name generated for runtime checks.
diff --git a/test/golden/RuntimeCheckAutoImport.hs b/test/golden/RuntimeCheckAutoImport.hs
new file mode 100644
index 00000000..c0dd7f15
--- /dev/null
+++ b/test/golden/RuntimeCheckAutoImport.hs
@@ -0,0 +1,15 @@
+module RuntimeCheckAutoImport (RuntimeCheckAutoImport.simpleFun) where
+
+import qualified Haskell.Extra.Dec.Instances (decIsTrue)
+import Numeric.Natural (Natural)
+
+import RuntimeCheckAutoImport.PostRtc
+
+simpleFun :: Natural -> Natural
+simpleFun x
+  | Haskell.Extra.Dec.Instances.decIsTrue (x > 0) =
+    RuntimeCheckAutoImport.PostRtc.simpleFun x
+  | otherwise =
+    error
+      "Runtime check failed: Haskell.Extra.Dec.Instances.decIsTrue (x > 0)"
+
diff --git a/test/golden/RuntimeCheckAutoImport/PostRtc.hs b/test/golden/RuntimeCheckAutoImport/PostRtc.hs
new file mode 100644
index 00000000..8dbef56a
--- /dev/null
+++ b/test/golden/RuntimeCheckAutoImport/PostRtc.hs
@@ -0,0 +1,8 @@
+module RuntimeCheckAutoImport.PostRtc where
+
+import qualified Haskell.Extra.Dec.Instances (decIsTrue)
+import Numeric.Natural (Natural)
+
+simpleFun :: Natural -> Natural
+simpleFun _ = 0
+
diff --git a/test/golden/RuntimeCheckCallFeatures.hs b/test/golden/RuntimeCheckCallFeatures.hs
new file mode 100644
index 00000000..6e2cc9bb
--- /dev/null
+++ b/test/golden/RuntimeCheckCallFeatures.hs
@@ -0,0 +1,7 @@
+module RuntimeCheckCallFeatures (externalFunCaller) where
+
+import Numeric.Natural (Natural)
+import RuntimeCheckFeatures.PostRtc (simpleFun)
+
+import RuntimeCheckCallFeatures.PostRtc
+
diff --git a/test/golden/RuntimeCheckCallFeatures/PostRtc.hs b/test/golden/RuntimeCheckCallFeatures/PostRtc.hs
new file mode 100644
index 00000000..34bb9fa2
--- /dev/null
+++ b/test/golden/RuntimeCheckCallFeatures/PostRtc.hs
@@ -0,0 +1,8 @@
+module RuntimeCheckCallFeatures.PostRtc where
+
+import Numeric.Natural (Natural)
+import RuntimeCheckFeatures.PostRtc (simpleFun)
+
+externalFunCaller :: Natural
+externalFunCaller = simpleFun 1
+
diff --git a/test/golden/RuntimeCheckClass.err b/test/golden/RuntimeCheckClass.err
new file mode 100644
index 00000000..176bafa3
--- /dev/null
+++ b/test/golden/RuntimeCheckClass.err
@@ -0,0 +1,2 @@
+test/Fail/RuntimeCheckClass.agda:11,8-15
+Cannot compile NoClass to class. Classes cannot have erased arguments with runtime checking.
diff --git a/test/golden/RuntimeCheckFeatures.hs b/test/golden/RuntimeCheckFeatures.hs
new file mode 100644
index 00000000..45e77a6a
--- /dev/null
+++ b/test/golden/RuntimeCheckFeatures.hs
@@ -0,0 +1,67 @@
+module RuntimeCheckFeatures (noneErasedFun, simpleFunCaller, singleEven, Dat(NoneErasedCon), Rec(recFst, recSnd), Newt(theField), NoneErasedNewt(noneErasedField, NoneErasedNewt), ErasedField(erasedFst), fUnzip, RuntimeCheckFeatures.simpleFun, RuntimeCheckFeatures.doubleOdd, RuntimeCheckFeatures.tripleOdd, RuntimeCheckFeatures.scCon, RuntimeCheckFeatures.scRec, RuntimeCheckFeatures.scNewt, RuntimeCheckFeatures.scErasedField) where
+
+import Haskell.Extra.Dec.Instances (decIsFalse, decIsTrue)
+import Numeric.Natural (Natural)
+
+import RuntimeCheckFeatures.PostRtc
+
+simpleFun :: Natural -> Natural
+simpleFun x
+  | decIsTrue (x > 0) = RuntimeCheckFeatures.PostRtc.simpleFun x
+  | otherwise = error "Runtime check failed: decIsTrue (x > 0)"
+
+doubleOdd ::
+          Natural ->
+            ((Natural -> Natural) -> Natural) ->
+              ((Natural -> Natural) -> Natural) -> Natural
+doubleOdd x a0 a2
+  = RuntimeCheckFeatures.PostRtc.doubleOdd x (\ a1 -> a0 (go0 a1))
+      (\ a3 -> a2 (go1 a3))
+  where
+    go0 up y
+      | decIsFalse (x < y) = up y
+      | otherwise = error "Runtime check failed: decIsFalse (x < y)"
+    go1 up y
+      | decIsFalse (x < y) = up y
+      | otherwise = error "Runtime check failed: decIsFalse (x < y)"
+
+tripleOdd ::
+          ((Natural -> ((Natural -> Natural) -> Natural) -> Natural) ->
+             Natural)
+            -> Natural
+tripleOdd a0
+  = RuntimeCheckFeatures.PostRtc.tripleOdd (\ a1 -> a0 (go1 a1))
+  where
+    go1 up m a2
+      | decIsTrue (m > 0) = up m (\ a3 -> a2 (go0 a3))
+      | otherwise = error "Runtime check failed: decIsTrue (m > 0)"
+      where
+        go0 up n
+          | decIsFalse (n < 1) = up n
+          | otherwise = error "Runtime check failed: decIsFalse (n < 1)"
+
+scCon :: Natural -> Dat
+scCon x
+  | decIsTrue (x > 0) = Con x
+  | otherwise = error "Runtime check failed: decIsTrue (x > 0)"
+
+scRec :: Natural -> Natural -> Rec
+scRec recFst recSnd = Rec recFst (go0 recSnd)
+  where
+    go0 up
+      | decIsTrue (recFst > 0) = up
+      | otherwise = error "Runtime check failed: decIsTrue (recFst > 0)"
+
+scNewt :: (Natural -> Natural) -> Newt
+scNewt theField = Newt (go0 theField)
+  where
+    go0 up x
+      | decIsTrue (x > 0) = up x
+      | otherwise = error "Runtime check failed: decIsTrue (x > 0)"
+
+scErasedField :: Natural -> ErasedField
+scErasedField erasedFst
+  | decIsTrue (erasedFst > 0) = ErasedField erasedFst
+  | otherwise =
+    error "Runtime check failed: decIsTrue (erasedFst > 0)"
+
diff --git a/test/golden/RuntimeCheckFeatures/PostRtc.hs b/test/golden/RuntimeCheckFeatures/PostRtc.hs
new file mode 100644
index 00000000..05d1d619
--- /dev/null
+++ b/test/golden/RuntimeCheckFeatures/PostRtc.hs
@@ -0,0 +1,52 @@
+module RuntimeCheckFeatures.PostRtc where
+
+import Haskell.Extra.Dec.Instances (decIsFalse, decIsTrue)
+import Numeric.Natural (Natural)
+
+noneErasedFun :: Natural -> Natural
+noneErasedFun _ = 1
+
+noDecInstance :: Natural -> Natural
+noDecInstance x = 0
+
+simpleFun :: Natural -> Natural
+simpleFun _ = 0
+
+simpleFunCaller :: Natural
+simpleFunCaller = simpleFun 1
+
+singleEven :: (Natural -> Natural) -> Natural
+singleEven _ = 0
+
+doubleOdd ::
+          Natural ->
+            ((Natural -> Natural) -> Natural) ->
+              ((Natural -> Natural) -> Natural) -> Natural
+doubleOdd _ _ _ = 0
+
+tripleOdd ::
+          ((Natural -> ((Natural -> Natural) -> Natural) -> Natural) ->
+             Natural)
+            -> Natural
+tripleOdd _ = 0
+
+data Dat = Con Natural
+         | NoneErasedCon Natural
+
+data Rec = Rec{recFst :: Natural, recSnd :: Natural}
+
+newtype Newt = Newt{theField :: Natural -> Natural}
+
+newtype NoneErasedNewt = NoneErasedNewt{noneErasedField :: Natural}
+
+data ErasedField = ErasedField{erasedFst :: Natural}
+
+listErased :: [(Natural -> Natural) -> Natural] -> Natural
+listErased _ = 0
+
+eraseTCB :: Natural -> Natural
+eraseTCB n = 0
+
+fUnzip :: Functor f => f (a, b) -> (f a, f b)
+fUnzip xs = (fmap (\ r -> fst r) xs, fmap (\ r -> snd r) xs)
+
diff --git a/test/golden/RuntimeCheckGo.err b/test/golden/RuntimeCheckGo.err
new file mode 100644
index 00000000..8a45cf92
--- /dev/null
+++ b/test/golden/RuntimeCheckGo.err
@@ -0,0 +1,2 @@
+test/Fail/RuntimeCheckGo.agda:5,1-9
+Illegal name go0, conflicts with name generated for runtime checks.
diff --git a/test/golden/RuntimeCheckInline.err b/test/golden/RuntimeCheckInline.err
new file mode 100644
index 00000000..b5c7658a
--- /dev/null
+++ b/test/golden/RuntimeCheckInline.err
@@ -0,0 +1,2 @@
+test/Fail/RuntimeCheckInline.agda:9,1-13
+Cannot make function notInlinable inlinable. Inline functions cannot have erased arguments with runtime checking.
diff --git a/test/golden/RuntimeCheckSc.err b/test/golden/RuntimeCheckSc.err
new file mode 100644
index 00000000..db1452e0
--- /dev/null
+++ b/test/golden/RuntimeCheckSc.err
@@ -0,0 +1,2 @@
+test/Fail/RuntimeCheckSc.agda:5,6-9
+Illegal name scConflict, conflicts with name generated for runtime checks.
diff --git a/test/golden/RuntimeCheckTransparent.err b/test/golden/RuntimeCheckTransparent.err
new file mode 100644
index 00000000..3bd7640a
--- /dev/null
+++ b/test/golden/RuntimeCheckTransparent.err
@@ -0,0 +1,2 @@
+test/Fail/RuntimeCheckTransparent.agda:9,1-14
+Cannot make function noTransparent transparent. Transparent functions cannot have erased arguments with runtime checking.
diff --git a/test/golden/RuntimeCheckTuple.err b/test/golden/RuntimeCheckTuple.err
new file mode 100644
index 00000000..d837f8d8
--- /dev/null
+++ b/test/golden/RuntimeCheckTuple.err
@@ -0,0 +1,2 @@
+test/Fail/RuntimeCheckTuple.agda:9,8-17
+Cannot compile record CantTuple as tuple. Tuple records cannot have erased arguments in their fields with runtime checking.
diff --git a/test/golden/RuntimeCheckUnboxed.err b/test/golden/RuntimeCheckUnboxed.err
new file mode 100644
index 00000000..eae15e11
--- /dev/null
+++ b/test/golden/RuntimeCheckUnboxed.err
@@ -0,0 +1,2 @@
+test/Fail/RuntimeCheckUnboxed.agda:5,8-17
+Cannot make record Unboxable unboxed. Unboxed records cannot have erased arguments in their fields with runtime checking.
diff --git a/test/golden/RuntimeCheckUp.err b/test/golden/RuntimeCheckUp.err
new file mode 100644
index 00000000..f0e25078
--- /dev/null
+++ b/test/golden/RuntimeCheckUp.err
@@ -0,0 +1,2 @@
+test/Fail/RuntimeCheckUp.agda:5,1-9
+Illegal name up, conflicts with name generated for runtime checks.
diff --git a/test/golden/RuntimeCheckUseCases.hs b/test/golden/RuntimeCheckUseCases.hs
new file mode 100644
index 00000000..1e4df68d
--- /dev/null
+++ b/test/golden/RuntimeCheckUseCases.hs
@@ -0,0 +1,18 @@
+module RuntimeCheckUseCases (RuntimeCheckUseCases.subtractFromGreater, RuntimeCheckUseCases.headOfNonEmpty) where
+
+import Haskell.Extra.Dec.Instances (decIsFalse, decNonEmpty)
+import Numeric.Natural (Natural)
+
+import RuntimeCheckUseCases.PostRtc
+
+subtractFromGreater :: Natural -> Natural -> Natural
+subtractFromGreater x y
+  | decIsFalse (x < y) =
+    RuntimeCheckUseCases.PostRtc.subtractFromGreater x y
+  | otherwise = error "Runtime check failed: decIsFalse (x < y)"
+
+headOfNonEmpty :: [Natural] -> Natural
+headOfNonEmpty xs
+  | decNonEmpty xs = RuntimeCheckUseCases.PostRtc.headOfNonEmpty xs
+  | otherwise = error "Runtime check failed: decNonEmpty xs"
+
diff --git a/test/golden/RuntimeCheckUseCases/PostRtc.hs b/test/golden/RuntimeCheckUseCases/PostRtc.hs
new file mode 100644
index 00000000..b66e3ced
--- /dev/null
+++ b/test/golden/RuntimeCheckUseCases/PostRtc.hs
@@ -0,0 +1,11 @@
+module RuntimeCheckUseCases.PostRtc where
+
+import Haskell.Extra.Dec.Instances (decIsFalse, decNonEmpty)
+import Numeric.Natural (Natural)
+
+subtractFromGreater :: Natural -> Natural -> Natural
+subtractFromGreater x y = x - y
+
+headOfNonEmpty :: [Natural] -> Natural
+headOfNonEmpty (x : _) = x
+