[Agda] Some problems with K-S basis

[v0id_NULL]

Dear list,
Help me, please. I try to deal with combinatory logic via Agda, but I have
some problems with defining of K-combinator. If I define K and S
combinators like this

K : {a b : _} → {A : Set a} → {B : Set b} → A → B → A
K x _ = x

S : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → (A → B → C) →
(A → B) → A → C
S x y z = x z (y z)

this leads to that Agda can not solve some constrains in this definition of
I-combinator

I : {ℓ : _} → {A : Set ℓ} → A → A
I = S K K

Agda needs in prompt of this implicit argument
I = S K (K {_} {_} {_} {?})
but I don't know how to do this, because it doesn't matter (the second
explicit argument of K is discarded by definition).

But if I define K-combinaor like this

K : {a : _} → {A : Set a} → A → {b : _} → {B : Set b} → B → A
K x _ = x

this leads to that Agda fails to type-check this definition of I-combinator

I : {ℓ : _} → {A : Set ℓ} → A → A
I = S K K

with report containing: "...because this would result in an invalid use of
Setω..."

How I must to define S-K basis, enough right to define complex combinators
with applicative by like (K K), (S (K S) K) and so on?

Generaly, tell me, please, is it good idea to implement something like
combinatory logic via Agda?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170724/a6d584c6/attachment.html>