From a9ef4fadc563ad2c9ec6aa611547481b330fe9d6 Mon Sep 17 00:00:00 2001
From: Pavel Turyansky <pavel.turyansky@kaspersky.com>
Date: Sat, 4 May 2024 12:47:48 +0000
Subject: [PATCH] downstream fix, see agda/agda#7247

---
 src/Reflection/AST/Definition.agda | 35 ++++++++++++++++++------------
 src/Reflection/AST/Show.agda       |  3 ++-
 2 files changed, 23 insertions(+), 15 deletions(-)

diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 3f06fef070..8b6da0f4e6 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -8,6 +8,7 @@
 
 module Reflection.AST.Definition where
 
+import Data.Bool.Properties as Bool                    using (_≟_)
 import Data.List.Properties as List                    using (≡-dec)
 import Data.Nat.Properties as ℕ                        using (_≟_)
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
@@ -56,8 +57,14 @@ record′-injective₂ refl = refl
 record′-injective : ∀ {c c′ fs fs′} → record′ c fs ≡ record′ c′ fs′ → c ≡ c′ × fs ≡ fs′
 record′-injective = < record′-injective₁ , record′-injective₂ >
 
-constructor′-injective : ∀ {c c′} → constructor′ c ≡ constructor′ c′ → c ≡ c′
-constructor′-injective refl = refl
+constructor′-injective₁ : ∀ {c c′ e e′} → constructor′ c e ≡ constructor′ c′ e′ → c ≡ c′
+constructor′-injective₁ refl = refl
+
+constructor′-injective₂ : ∀ {c c′ e e′} → constructor′ c e ≡ constructor′ c′ e′ → e ≡ e′
+constructor′-injective₂ refl = refl
+
+constructor′-injective : ∀ {c c′ e e′} → constructor′ c e ≡ constructor′ c′ e′ → c ≡ c′ × e ≡ e′
+constructor′-injective = < constructor′-injective₁ , constructor′-injective₂ >
 
 infix 4 _≟_
 
@@ -70,39 +77,39 @@ data-type pars cs ≟ data-type pars′ cs′ =
 record′ c fs      ≟ record′ c′ fs′      =
   map′ (uncurry (cong₂ record′)) record′-injective
            (c Name.≟ c′ ×-dec List.≡-dec (Arg.≡-dec Name._≟_) fs fs′)
-constructor′ d    ≟ constructor′ d′     =
-  map′ (cong constructor′) constructor′-injective (d Name.≟ d′)
+constructor′ d e  ≟ constructor′ d′ e′  =
+  map′ (uncurry (cong₂ constructor′)) constructor′-injective (d Name.≟ d′ ×-dec e Bool.≟ e′)
 axiom             ≟ axiom               = yes refl
 primitive′        ≟ primitive′          = yes refl
 
 -- antidiagonal
 function cs ≟ data-type pars cs₁ = no (λ ())
 function cs ≟ record′ c fs = no (λ ())
-function cs ≟ constructor′ d = no (λ ())
+function cs ≟ constructor′ d e = no (λ ())
 function cs ≟ axiom = no (λ ())
 function cs ≟ primitive′ = no (λ ())
 data-type pars cs ≟ function cs₁ = no (λ ())
 data-type pars cs ≟ record′ c fs = no (λ ())
-data-type pars cs ≟ constructor′ d = no (λ ())
+data-type pars cs ≟ constructor′ d e = no (λ ())
 data-type pars cs ≟ axiom = no (λ ())
 data-type pars cs ≟ primitive′ = no (λ ())
 record′ c fs ≟ function cs = no (λ ())
 record′ c fs ≟ data-type pars cs = no (λ ())
-record′ c fs ≟ constructor′ d = no (λ ())
+record′ c fs ≟ constructor′ d e = no (λ ())
 record′ c fs ≟ axiom = no (λ ())
 record′ c fs ≟ primitive′ = no (λ ())
-constructor′ d ≟ function cs = no (λ ())
-constructor′ d ≟ data-type pars cs = no (λ ())
-constructor′ d ≟ record′ c fs = no (λ ())
-constructor′ d ≟ axiom = no (λ ())
-constructor′ d ≟ primitive′ = no (λ ())
+constructor′ d e ≟ function cs = no (λ ())
+constructor′ d e ≟ data-type pars cs = no (λ ())
+constructor′ d e ≟ record′ c fs = no (λ ())
+constructor′ d e ≟ axiom = no (λ ())
+constructor′ d e ≟ primitive′ = no (λ ())
 axiom ≟ function cs = no (λ ())
 axiom ≟ data-type pars cs = no (λ ())
 axiom ≟ record′ c fs = no (λ ())
-axiom ≟ constructor′ d = no (λ ())
+axiom ≟ constructor′ d e = no (λ ())
 axiom ≟ primitive′ = no (λ ())
 primitive′ ≟ function cs = no (λ ())
 primitive′ ≟ data-type pars cs = no (λ ())
 primitive′ ≟ record′ c fs = no (λ ())
-primitive′ ≟ constructor′ d = no (λ ())
+primitive′ ≟ constructor′ d e = no (λ ())
 primitive′ ≟ axiom = no (λ ())
diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda
index 5d748e089b..9d9855709e 100644
--- a/src/Reflection/AST/Show.agda
+++ b/src/Reflection/AST/Show.agda
@@ -11,6 +11,7 @@
 
 module Reflection.AST.Show where
 
+import Data.Bool.Show as Bool
 import Data.Char.Base as Char
 import Data.Float.Base as Float
 open import Data.List.Base hiding (_++_; intersperse)
@@ -144,6 +145,6 @@ showDefinition (data-type pars cs) =
  "datatype" <+> ℕ.show pars <+> braces (intersperse ", " (map showName cs))
 showDefinition (record′ c fs)      =
  "record" <+> showName c <+> braces (intersperse ", " (map (showName ∘′ unArg) fs))
-showDefinition (constructor′ d)    = "constructor" <+> showName d
+showDefinition (constructor′ d e)  = "constructor" <+> showName d <+> Bool.show e
 showDefinition axiom               = "axiom"
 showDefinition primitive′          = "primitive"