[Agda] Re: Implicit arguments

[N. Raghavendra]

At 2015-04-13T08:13:08+02:00, Andreas Abel wrote:

> Boring, "obvious" type information tires the human reader out
> quickly. So it is necessary to omit it.  Ideally, Agda would exactly
> infer what we consider obvious...

Thanks for explaining the asymmetry in inferring n and m from n + m.

Another thing I wanted to say was that using implicit arguments
sometimes seems to result in a strange style of writing.  E.g., Agda
allows us to leave the arguments C and x implicit in the definition of
bool-ind below:

--8<---------------cut here---------------start------------->8---
open import Data.Bool
open import Data.Nat

bool-ind : ∀ {𝓁} {C : Bool → Set 𝓁} → C false → C true → {x : Bool} → C x
bool-ind cf ct {true} = ct
bool-ind cf ct {false} = cf

foo : _
foo = bool-ind {C = λ x → ℕ} 1 2

bar : ℕ
bar = foo {true}
--8<---------------cut here---------------end--------------->8---

However, whenever we apply bool-ind, we anyway have to provide Agda the
arguments C and x, that too in unwieldy braces.  It'd be nice if Agda
rejects the implicit declaration for the arguments C and x in such a
situation.

Cheers,
Raghu.

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