x！= y型のパターンp（y）がZ型であることをチェックするときのY型y

Question

x != y of type Y when checking that the pattern p(y) has type Zという形式の奇妙なエラーが発生します。なぜ、どのように私がこれを取得しているのか分かりませんし、問題を解決したいと思います。問題のインスタンスが続きます。ありがとうございました。

---

私はセット、

postulate A : Set 

やセットなどの要素を解釈する方法、そのセットのペアを使用して、その後

postulate F : A → Set 

を、と仮定しました

record B : Set where field s t : A 

パラメータ化された型を作成することができます：

data C : A → Set where MkC : (b : B) → F (B.s b) → C (B.t b) 

は、今私は、例えば、関数に

ABCF : ∀ a → (f : A → A) → C a → C (f a) 
ABCF t f e = {!!} 

を形成したいと私はC-c C-c を介して第3引数にパターンマッチングによってそうそしてそうすることが私に

を取得したいです b上

ABCF .(B.t b) f (MkC b x) = {!!} 

次に別C-c C-c、利回り

ABCF t f (MkC record { s = s ; t = .t } x) = ? 

しかしこのケーシングは、直ちにエラーが続く：t'と.tの交換

B.t b != t of type A 
when checking that the pattern MkC record { s = s ; t = .t } x has 
type C t 

はまた、これを解決しません。

このエラーの原因と解決方法を教えてください。

---

編集

としては、上記の問題はバグが原因である可能性があり、以下の答えが、何逆の例？

FCBA : ∀ {a} (f : A → A) → C (f a) → C a 
FCBA {a} f (MkC record { s = s ; t = .(f a) } x) = ? 

どうすればこの問題を解決できますか？エラーの原因となるもの

B.t b != f a of type A 
when checking that the pattern MkC record { s = s ; t = .(f a) } x 
has type C (f a) 

Answer 1

バグのようです。あなたが定期的に1とアクセスできないパターンを交換した場合、すべてが動作します：

ABCF : ∀ a → (f : A → A) → C a → C (f a) 
ABCF .t f (MkC record { s = s ; t = t } x) = {!!} 

しかし、それはC aから常にinferrableだからaとにかく、暗黙的でなければならないこと。そして、問題はありません。

ABCF : ∀ {a} → (f : A → A) → C a → C (f a) 
ABCF f (MkC record { s = s ; t = t } x) = {!!} 

---

あなたはパターンマッチが直接原因の種類があまりにも具体的であることに、あなたはそれを一般化することができますすることができない場合は、次の

open import Relation.Binary.PropositionalEquality 

FCBA : ∀ {a} (f : A → A) → C (f a) → C a 
FCBA {a} f c with f a | inspect f a | c 
... | .b | [ r ] | MkC record { s = s ; t = b } x = {!!} 

ここbにf aを一般化して覚えてそのf a ≡ b（この場合、そのような思い出しはおそらく有用ではありませんが、bが実際にはf aであることを忘れたくない場合に必要です）。これにより、cのパターンマッチは、以前のようにアクセスできないパターンと通常のパターンを入れ替えることができます。

しかし、これはトリックではありません - それは醜いハックです。おそらく、Agdaのメーリングリストで、このスワップが必要な理由とこれが意図された動作であるかどうかを尋ねるべきです。