[Agda] Proposed Agda feature: non-canonical implicit arguments

[Nils Anders Danielsson]

On 2011-04-01 16:32, Andreas Abel wrote:
> In your paper you are addressing the question of a logic programming
> engine to find instances and proofs.  Indeed, I think such an engine
> would be useful if it sensibly restricted (no recursion) and also only
> succeeds if there is a *unique* instance.  In case of proofs (see the
> irrelevance feature) uniqueness is not important, but surely in case of
> inferred programs (as it is with unification now).

I agree that instances should only be inferred if they are unique
(except in irrelevant contexts).

At the moment Agda has some support for /closed/ type-classes via
universes. Quick example:

   open import Data.Bool as Bool using (Bool)
   open import Data.Nat as Nat using (ℕ)
   open import Relation.Binary
   open import Relation.Binary.PropositionalEquality
   open import Relation.Nullary

   data Eq : Set where
     bool nat : Eq

   El : Eq → Set
   El bool = Bool
   El nat  = ℕ

   _≟_ : {a : Eq} → Decidable (_≡_ {A = El a})
   _≟_ {bool} = Bool._≟_
   _≟_ {nat}  = Nat._≟_

   example : Dec (5 ≡ 3)
   example = 5 ≟ 3

Note that the "instance" is inferred automatically on the last line.
However, this inference mechanism, which Ulf came up with to support
this use of universes, is rather syntactic and brittle:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments

-- 
/NAD