Simply Typed Combinatory Logic?
Quick note, I allow parametric polymorphism (System F) in this system so that S, K and I can work over all types.

Notice that without pattern matching, we can't write an if no matter what we do. We have absolutely no operations on booleans. There is no way to distinguish True from False. Instead try

true : a -&gt; a -&gt; a
true = \t -&gt; \f -&gt; t

false : a -&gt; a -&gt; a
false = \t -&gt; \f -&gt; f


Let's let Bool = a -&gt; a -&gt; a for clarity.

 if : Bool -&gt; a -&gt; a -&gt; a
 if = \bool -&gt; \a -&gt; \b -&gt; bool a b


Now it's just a matter of compiling some lambda calculus expressions to combinators, which is pretty trivial.

if : Bool -&gt; a -&gt; a -&gt; a -- Or just Bool -&gt; Bool
if    = I

true : a -&gt; a -&gt; a
true  = K

false : a -&gt; a -&gt; a
false = K I