[Agda] Agda can't find an obvious instance.

[Ulf Norell]

This is the intended behaviour. Metavariables are not resolved based on
which instances exist, since this leads to unpredictable behaviour and
brittle code. For instance

record Default (A : Set) : Set where
  field default : A

open Default {{...}}

instance
  DefaultNat : Default Nat
  DefaultNat = 0

-- Here we don't want the type of x to be inferred to be Nat just because
we haven't
-- (yet) added more instances of Default.
x : _
x = default

/ Ulf


On Tue, Jul 7, 2015 at 5:33 AM, effectfully <effectfully at gmail.com> wrote:

> open import Relation.Binary.PropositionalEquality
> open import Data.Nat
> open import Data.Fin
>
> instance
>   fz : Fin 1
>   fz = zero
>
> z : ∀ {n} {{_ : Fin n}} -> ℕ
> z = 0
>
> yellow : z ≡ 0
> yellow = refl
>
> ok : z {1} ≡ 0
> ok = refl
>
> ----
>
> The instance is not picked in `yellow'. Agda can't find the instance
> even in this case:
>
> ----
>
> record R (n m : ℕ) : Set where
>
> instance
>   r : R 0 1
>   r = _
>
> z' : ∀ {m} {{_ : R 0 m}} -> ℕ
> z' = 0
>
> yellow' : z' ≡ 0
> yellow' = refl
>
> ok' : z' {1} ≡ 0
> ok' = refl
>
> ----
>
> Should I report this as a bug, or is this a known limitation?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150707/44f77a1b/attachment.html