Agda の演算子の構文によるエラー

中置演算子を定義できる言語はいろいろあって面白いんですが、Agda の自由度はかなり高い。

　　C [ f ≈ g ] = Category._≈_ C f g
　　infix　4 _[_≈_]

で圏Cでの等号定義できる。これを使うと複数の圏の演算を混ざるとか平気でできます。三項演算子だ。しかも二項演算子を三項に拡張してる。

この _ のところに変数が来るわけだな。 この記法は圏論でも使われてたりします。
さらに syntax というのがあるらしいが、まだ使ってません。

equality 自体も _≡_ という二項演算子で

　　data : Set } :　(x y : A) → Set　where
　　　refl　: {x : A} → x ≡ x

なんですが、これを x ≡_ みたいに使える。

　　x ≡_ = λ y → x ≡ y

(x ≡_) y が x ≡ y になるわけなので正しく curry 化されてるわけ。 なのだが、

　　_≡_ x　と _≡ x と x ≡_

と三種類書ける。どれも構文エラーにならない。 　　_≡_ x　と x ≡_ は同じ。

x ≡ y と　y ≡ x は同じなので、どれでも良いと思ったし、動いてたんですが、昨日、突然、

　　annot instantiate the metavariable _491 to solution section
　　since it contains the variable section
　　which is not in scope of the metavariable
　　when checking that the inferred type of an application

というわけわかエラーが。いやなにいってるんだかわらないんですが。でも、いろいろ削ってだめなところを抜き出したら

　　_≡ x と x ≡_ との違いだった

どっちかに統一すれば解決。なくなく 60 箇所くらい修正する羽目に。いや、Emacs の Keyboard macro でできるわけなんだが...

　　x ≡_ = λ y → x ≡ y
　　_≡ x = λ y → y ≡ x

なので、確かに違う。しかも通る場合がある。しかし、結局は通るはず。しかし、エラーは出る。なるほどわけわかりません。

いや、混ぜた自分が謎でもあるのだが...