https://twitter.com/KazutakaMatsuda/status/804334181467627520

C.agda

module C where

import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl)

data C {A : Set} : Set where
  c : (a : A) → C

------ ケース1
-- OK
f₁ : {A : Set} {a b : A} -> c a ≡ c b → a ≡ b
f₁ {A} {a} {.a} refl = refl
--
-- λでなく普通に関数
--

------ ケース2
-- NG
-- f₂ : {A : Set} {a b : A} -> c a ≡ c b → a ≡ b
-- f₂ = (λ { refl → refl })
--
-- aとbをreflのパターンマッチで同じ(名前)にしたいけど，
-- λ外で縛られた変数であるため，reflのマッチ自体ができない
--

------ ケース3
-- OK
f₃ : {A : Set} (a b : A) -> c a ≡ c b → a ≡ b
f₃ = λ { x .x refl -> refl }
--
-- λ内で縛れる(依存性が解決できる)ようにしてやるとできる．
--

------ ケース4
-- NG
-- f₄ : {A : Set} (a b : A) -> c a ≡ c b → a ≡ b
-- f₄ a b = (λ { x .x refl → refl }) a b
--
-- 変数に束縛してλに与えてしまうと，
-- その束縛した変数から別の値を作ること等が可能になり，
-- λの中からみた2変数と≡の変数の依存が正当なものかわからなくなるのでダメ．
-- たとえば，
--
-- f₅ : {A : Set} (a b : A) -> c a ≡ c b → a ≡ b
-- f₅ a b = (λ { x .x refl → refl }) a a
--
-- でも同じワカリマセンが出る．
--