#3135.agda

module issue.#3135 where

-- latex \sqw
postulate
  A : Set
  □   : Set
  _□  : Set → Set
  ⟨_⟩ : Set → Set

--G : Set
--G = ? □

open import Agda.Builtin.Equality using (_≡_ ; refl)
_ : A □ ≡ A □
_ = refl

-- C-c C-l fails (version 2.6.1)
-- Don't know how to parse A □ ≡ A □. Could mean any one of:
--  (A □) ≡ (A □)
--  (A □) ≡ (A □)
--  (A □) ≡ (A □)
--  (A □) ≡ (A □)