[ #4067 ] Added another test case.refs/pull/4263/headissue4067

3 files changed, 44 insertions, 0 deletions

diff --git a/test/interaction/Issue4067-2.agda b/test/interaction/Issue4067-2.agda
new file mode 100644
index 0000000..ff8dde9
--- /dev/null
+++ b/test/interaction/Issue4067-2.agda
@@ -0,0 +1,37 @@
+{-# OPTIONS --cubical #-}
+
+open import Agda.Builtin.Cubical.Path
+
+postulate
+  trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+
+infix  -1 finally
+infixr -2 _≡⟨⟩_
+
+_≡⟨⟩_ : {A : Set} (x {y} : A) → x ≡ y → x ≡ y
+_ ≡⟨⟩ x≡y = x≡y
+
+finally : {A : Set} (x y : A) → x ≡ y → x ≡ y
+finally _ _ x≡y = x≡y
+
+syntax finally x y x≡y = x ≡⟨ x≡y ⟩∎ y ∎
+
+⟨_⟩ : {A : Set} → A → A
+⟨ x ⟩ = x
+
+{-# NOINLINE ⟨_⟩ #-}
+
+record R (F : Set → Set) : Set₁ where
+  field
+    p : {A : Set} {x : F A} → x ≡ x
+
+open R ⦃ … ⦄ public
+
+test :
+  {F : Set → Set} ⦃ r : R F ⦄ {A : Set} {x₁ x₂ : F A}
+  (p₁ p₂ : x₁ ≡ x₂) (assumption : p₁ ≡ p₂) →
+  trans p p₁ ≡ trans p p₂
+test p₁ p₂ assumption =
+  trans p p₁      ≡⟨⟩
+  trans p ⟨ p₁ ⟩  ≡⟨ ? ⟩∎  -- The goal type should contain ⟨_⟩.
+  trans p p₂      ∎
diff --git a/test/interaction/Issue4067-2.in b/test/interaction/Issue4067-2.in
new file mode 100644
index 0000000..3d2c5bf
--- /dev/null
+++ b/test/interaction/Issue4067-2.in
@@ -0,0 +1 @@
+top_command (cmd_load currentFile [])
diff --git a/test/interaction/Issue4067-2.out b/test/interaction/Issue4067-2.out
new file mode 100644
index 0000000..ab5bb0f
--- /dev/null
+++ b/test/interaction/Issue4067-2.out
@@ -0,0 +1,6 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : trans (R.p r) ⟨ p₁ ⟩ ≡ trans (R.p r) p₂ " nil)
+((last . 1) . (agda2-goals-action '(0)))