[Agda] Implicit arguments

[effectfully]

Disclaimer: I'll desribe my intuition. I have no idea what the actual rules are.

1) Agda can infer `x' from (f x), if (not iff) there is no
pattern-matching in `f'. Agda can infer

  1.1) `A' and `n' from (Vec A n)
  1.2) `n' from (Fin (suc n)).
         It's always possible to infer `x' from (f x), if `f' is a
sequence of constructors.
  1.3) `m' from (Fin (n + m)), if `n' is known.
         It makes perfect sense, because `_+_' is not injective,
         and hence there are various ways to instantiate `n' and `m'.
         But after you have instantiated `n', (n + m) reduces to (suc
(suc ... m)), which is the 1.2 case.
         I.e. you have to explicitly pass arguments, if there is
pattern-matching on them (there is an exception, see below). Examples:

    postulate
      fancy₁ : ∀ n {m} -> Vec ℕ (n + m) -> Vec ℕ (m + n)

    test-fancy₁ : _
    test-fancy₁ = fancy₁ 2 (1 ∷ 2 ∷ 3 ∷ [])

    postulate
      fancy₂ : ∀ {n} m -> Vec ℕ (n + m) -> Vec ℕ (m + n)

    test-fancy₂ : Vec ℕ 3
    test-fancy₂ = fancy₂ 2 (1 ∷ 2 ∷ 3 ∷ [])

The second case works, because Agda looks at the type of `test-fancy₂'
and solves (m = 2, m + n = 3) => (n = 1).

A counter-example:

    postulate
      fancy₃ : ∀ {n} m -> Vec ℕ (n + m) -> ⊤

    fail-fancy₃ : ⊤
    fail-fancy₃ = fancy₃ 2 (1 ∷ 2 ∷ 3 ∷ [])

Agda can't infer `n' from (n + m), if `m' is known.

A little more complicated example:

    postulate
      fancy₄ : ∀ n {m p} -> Vec ℕ (n + m + p) -> Vec ℕ (n + m) -> ⊤

    test-fancy₄ : ⊤
    test-fancy₄ = fancy₄ 2 (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) (1 ∷ 2 ∷ 3 ∷ [])

(n = 2, n + m + p = 5, n + m = 3) => (n = 2, m = 1, p = 2)



  1.4) `f' is constructor-headed [1]. For example `Data.Product.N-ary' defines

    _^_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ
    A ^ 0           = Lift ⊤
    A ^ 1           = A
    A ^ suc (suc n) = A × A ^ suc n

It's not constructor-headed: if (A ^ n = ℕ × ℕ) you get two solutions:
  1) A = ℕ     , n = 2
  2) A = ℕ × ℕ , n = 1

But

    _^_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ
    A ^ 0       = Lift ⊤
    A ^ (suc n) = A × A ^ suc n

is constructor-headed, and Agda can infer both `A' and `n' from (A ^ n
= B), if `B' is known.

You can make the first definition constructor-headed by wrapping `A'
in the (A ^ 1) case in an additional datatype:

    record Wrap {α} (A : Set α) : Set α where
      constructor wrap
      field el : A

    _^_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ
    A ^ 0           = Lift ⊤
    A ^ 1           = Wrap A
    A ^ suc (suc n) = A × A ^ suc n

    test-wrap : _ ^ _
    test-wrap = 0 , 3 , 5 , wrap 9

2) Agda usually can't infer `f' from (f x)

    fun : {L : Set -> Set} -> L ℕ -> ⊤
    fun _ = _

    fail-fun : ⊤
    fail-fun = fun []

results in unresolved metas. But you can help she by limiting the
scope of search using instance arguments:

    record IsNatList (L : Set -> Set) : Set where
      field f : ⊤

    instance
      inst : IsNatList List
      inst = record { f = _ }

    fun-inst : {L : Set -> Set} {{_ : IsNatList L}} -> L ℕ -> ⊤
    fun-inst _ = _

    test-fun-inst : ⊤
    test-fun-inst = fun-inst []

No unresolved metas. Strangely this doesn't work if I omit the
pointless field in the `IsNatList' datatype.

3) Agda's definitional equality is beta-eta, so (proj₁ p , proj₂ p)
reduces to just `p' during typechecking. Using eta-rules Agda can
infer elements of records:

    auto-records : ⊤ × Lift {ℓ = Le.suc (Le.suc Le.zero)} ⊤
    auto-records = _

4) Sometimes Agda can infer more stuff in mutual blocks, but it's
black magic to me.

5) Have a look at [2] for more complicated cases.

[1] http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments
[2] http://www2.tcs.ifi.lmu.de/~abel/talkTLCA11.pdf