NOTE: application transformation of function with implicit

Recently, I'm working on a theorem prover, and implementing implicit parameters. This brings a hard problem for me, and the idea get from type theory elaboration implementation should be recorded for myself! So here is the idea, the following definition is classic equality, type part.

(def (= {A : Type}
	[a b : A])
  : Type
  #:postulate)

In my theorem prover, one can write

(= T t t)
# or
(= t t)

It's clear that the second one is the point and usually we write down. So how to type check it? The idea is generating a fresh meta for it:

(= ?T t t)

Then unification should work!