Try reflection again

nix/agda.nix

@@ -26,6 +26,35 @@ rec {
     '';
   });
 
+  agda-stdlib-classes = agda-packages.mkDerivation {
+    pname = "agda-stdlib-classes";
+    version = "2.0";
+    src = pkgs.fetchFromGitHub {
+      repo = "agda-stdlib-classes";
+      owner = "omelkonian";
+      rev = "28df278381c94a25c54f6819524cd9f8cb99f092";
+      sha256 = "sha256-TdPJ3K4jyAIQgX1sUrqd0QeA72n2mkBVzlg8WfrqWWY=";
+    };
+    meta = { };
+    libraryFile = "agda-stdlib-classes.agda-lib";
+    everythingFile = "standard-library-classes.agda";
+    buildInputs = [ agda-stdlib ];
+  };
+
+  agda-stdlib-meta = agda-packages.mkDerivation {
+    pname = "agda-stdlib-meta";
+    version = "2.1.1";
+    src = pkgs.fetchFromGitHub {
+      repo = "stdlib-meta";
+      owner = "omelkonian";
+      rev = "v2.1.1";
+      sha256 = "qOoThYMG0dzjKvwmzzVZmGcerfb++MApbaGRzLEq3/4=";
+    };
+    meta = { };
+    libraryFile = "agda-stdlib-meta.agda-lib";
+    everythingFile = "Main.agda";
+    buildInputs = [ agda-stdlib agda-stdlib-classes ];
+  };
 
   # We want to keep control of which version of Agda we use, so we supply our own and override
   # the one from nixpkgs.
@@ -119,7 +148,8 @@ rec {
   };
 
 
-  agda-with-stdlib = agda-packages.agda.withPackages [ agda-stdlib ];
+  agda-with-stdlib =
+    agda-packages.agda.withPackages [ agda-stdlib agda-stdlib-classes agda-stdlib-meta ];
 
 
   agda-project = pkgs.haskell-nix.hackage-project {

plutus-metatheory/Plutus.agda-lib

@@ -1,2 +1,2 @@
-depend: standard-library
+depend: standard-library, standard-library-classes, standard-library-meta
 include: src

plutus-metatheory/src/VerifiedCompilation.lagda.md

@@ -60,6 +60,7 @@ import Relation.Binary as Binary using (Decidable)
 import Relation.Unary as Unary using (Decidable)
 import Agda.Builtin.Int
 import Relation.Nary as Nary using (Decidable)
+
 ```
 
 ## Compiler optimisation traces
@@ -186,3 +187,49 @@ runCertifier : List (SimplifierTag × Untyped × Untyped) → Maybe Proof
 runCertifier rawInput with traverseEitherList (toWellScoped {⊥}) rawInput
 ... | inj₁ _ = nothing
 ... | inj₂ inputTrace = just (proof (isTrace? inputTrace))
+
+open import Tactic.Derive.Show
+import Data.List.Base as L
+import Agda.Builtin.Sigma as S
+open import Class.MonadTC.Instances
+open import Tactic.Defaults
+open import Relation.Nullary using (Reflects)
+open import Data.Bool.Base using (Bool)
+open import Class.Show.Core
+open import Agda.Primitive using (Level)
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
+open import Relation.Binary.Core using (REL)
+
+variable
+  l : Level
+  l' : Level
+  l'' : Level
+  A : Set l
+  B : Set l'
+  X : Set
+
+instance 
+  Show-Neg : Show (A → ⊥)
+  Show-Neg = ?
+
+instance
+  Show-Pointwise : {xs : L.List A} {ys : L.List B} {r : REL A B l''} {{ _ : Show A }} → Show (Pointwise r xs ys)
+  Show-Pointwise = ?
+
+unquoteDecl
+    Show-Dec
+    Show-Trace
+    Show-Reflects
+    Show-Bool
+    Show-Transformation
+    Show-Translation
+  =
+    derive-Show 
+      ( (quote Dec S., Show-Dec)
+      L.∷ (quote Trace S., Show-Trace)
+      L.∷ (quote Reflects S., Show-Reflects)
+      L.∷ (quote Bool S., Show-Bool)
+      L.∷ (quote Transformation S., Show-Transformation)
+      L.∷ (quote Translation S., Show-Translation)
+      L.∷ L.[]
+      )