[Agda] Implicit arguments

[Peter Hancock]

On 12/04/2015 20:50, N. Raghavendra wrote:
> 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.

Me too. I often end up with scripts where there are masses of curly brackets
around arguments, by being too optimistic about what the type-checker will
infer.  Some general (not very helpful advice) is to use this feature only where
the type will be so blindingly obvious that you can infer it in your head.

On the other hand, it is often surprising what the type-checker *is* able to infer,
at least if your brain is as feeble as mine.  Then I sometimes find I need some
way to coax it into revealing the type.  What I have found is that using
let .. in ... structure on the right hand side of an equation, I can sometimes
get at the information what I want in a local definition.  I am sorry I cannot
be more explicit.

{I cannot refrain from adding that it baffles me that let { x1 = e1; ...} in e2
cannot occur *anywhere* an expression can occur.  It seems to make the language
less regular, and harder to use with confidence, that this is not the case.
No doubt there is some very good reason.}

I look forward to reading some proper answers to your question.

Peter