explicit implicit arguments

[GoogleCodeExporter]

This is on Development Agda of February 16, 2014.

Is this difficult to fix the checker with getting rid of applying in many
places things like

             \ {x} {y} -> f {x} {y}

?
This bites a programmer in a non-trivial way too.
For example (the code is not complete):

  ...
  IsOp₂homomorphism : (From c→ To) → Op₂ A → Op₂ B → Set (α ⊔ β=)
  IsOp₂homomorphism (f , _) _*_ _*'_ =
                                     {x y : A} → f (x * y) =b ((f x) *' (f y))

  foo : (g : C) → Op₂homomorphism _+_ _∙_
  foo g =  (cFromℤ , (\ {z} {u} → isH {z} {u}))
    where
    from = fromℤ g
    cong-from = cong₂-fromℤ {g = g}
    cFromℤ =  (from , cong-from)

    isH : IsOp₂homomorphism cFromℤ _+_ _∙_
    isH {z} {u} = fromℤ+homo g z u

  foo1 : C → Op₂homomorphism _+_ _∙_
  foo1 g =  homoFromℤ
            where
            homoFromℤ : Op₂homomorphism _+_ _∙_
            homoFromℤ = foo g

            cMap = proj₁ homoFromℤ

            is2homo :  IsOp₂homomorphism cMap _+_ _∙_
            is2homo =  \ {z} {u} → proj₂ homoFromℤ {z} {u}

The prefix "\ {z} {u} →"

occurs necessary not only in the line of "foo g"
but also in the line of "is2homo = ".

Sometimes it is difficult to debug, because there are too many possible sources
of "unsolved metas".

Original issue reported on code.google.com by `mech...@botik.ru` on 30 Mar 2014 at 7:39
* Merged into: #1079

[GoogleCodeExporter]

This is along the lines of issue #1079. Unfortunately, it is non-trivial to fix.

Original comment by andreas....@gmail.com on 2 Apr 2014 at 6:15

• Changed state: Duplicate
• Added labels: Conversion, HiddenArguments, Type-Enhancement