[Agda] Implicit arguments

[N. Raghavendra]

When defining a function or a dependent type, I'm often unsure about
which parameters can be declared as implicit.  How do I know whether the
system can infer a particular argument from the types of other
arguments?  Until now, I have been just guessing, and it hasn't been
satisfactory.  Can people describe some method of finding out which
parameters to assume as implicit?

Thanks and cheers,
Raghu.

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/