[Agda] Suspicious Infirmity of Type Inferencer

[Vag Vagoff]

Why compiler compels me to type types and kinds in specified locations?
(marked by double parenthesis)

It is possible to enforce typechecker to do eta reduction while term 
normalization?
(so I could write I ≡ S K S instead of ∀ {x} I x ≡ S K S x)

module CombTest where

infix 8 _≡_ ; data _≡_ {A : Set} (a : A) : A → Set where ≡-refl : a ≡ a

K : ∀ {a b} → a → b → a
K x y = x
S : ∀ {a b c} → (a → b → c) → (a → b) → a → c
S x y z = x z (y z)
I : ∀ {a} → a → a
I x = x
B : ∀ {a b c : ((Set)) } → (b → c) → (a → b) → a → c -- [!]
B x y z = x (y z)
C : ∀ {a b c : ((Set)) } → (b → a → c) → a → b → c -- [!]
C x y z = x z y
W : ∀ {a b : ((Set)) } → (a → a → b) → a → b -- [!]
W x y = x y y

test-I₀ : ∀ {b a} {x : a} {y : a → b} → I x ≡ S K y x
test-I₀ = ≡-refl

test-I₁ : ∀ {a} {x : a} → I x ≡ S {_} { ((a → a)) } K K x  -- [!]
test-I₁ = ≡-refl

test-I₂ : ∀ {a} {x : a → a → a} → I x ≡ S K S x
test-I₂ = ≡-refl

test-B : ∀ {a b c} {x : b → c} {y : a → b} {z : a} → B x y z ≡ S (K S) K 
x y z
test-B = ≡-refl

test-C : ∀ {a b c} {x : b → a → c} {y : a} {z : b} → C x y z ≡ S (S (K 
(S (K S) K)) S) (K K) x y z
test-C = ≡-refl

test-W : ∀ {a b} {x : a → a → b} {y : a} → W x y ≡ S S (K I) x y
test-W = ≡-refl

test-W' : ∀ {a b} {x : a → a → b} {y : a} → W x y ≡ S S (K (S {_} { ((a 
→ a)) } K K)) x y -- [!]
test-W' = ≡-refl

test-S : ∀ {a b c} {x : a → b → c} {y : a → b} {z : a} → S x y z ≡ B (B 
(B W) C) (B B) x y z
test-S = ≡-refl