[Agda] Type Checking in Agda

[effectfully]

> Can any one elaborate the Type Checking(and inference ) Algorithm used by Agda, provide or some pointers for the same.

Agda is far too complex language, there can't be a single exhaustive
paper. Check these papers/posts first before you dive into
metavariables resolution, irrelevance, coinduction, sized typed,
instance arguments and whatever I forgot :

http://augustss.blogspot.dk/2007/10/simpler-easier-in-recent-paper-simply.html
http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/
(and the other parts)
https://github.com/sweirich/pi-forall
http://www.andres-loeh.de/PiSigma/PiSigma.pdf

> what approximations Agda uses to get a decidable type checker.
Type checking is decidable in intensional type theories, which Agda
is. It's type inference is undecidable.