<div dir="ltr">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<div><br></div><div>record Default (A : Set) : Set where</div><div> field default : A</div><div><br></div><div>open Default {{...}}</div><div><br></div><div>instance</div><div> DefaultNat : Default Nat</div><div> DefaultNat = 0</div><div><br></div><div>-- Here we don't want the type of x to be inferred to be Nat just because we haven't</div><div>-- (yet) added more instances of Default.</div><div>x : _</div><div>x = default</div><div><br></div><div>/ Ulf</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jul 7, 2015 at 5:33 AM, effectfully <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">open import Relation.Binary.PropositionalEquality<br>
open import Data.Nat<br>
open import Data.Fin<br>
<br>
instance<br>
fz : Fin 1<br>
fz = zero<br>
<br>
z : ∀ {n} {{_ : Fin n}} -> ℕ<br>
z = 0<br>
<br>
yellow : z ≡ 0<br>
yellow = refl<br>
<br>
ok : z {1} ≡ 0<br>
ok = refl<br>
<br>
----<br>
<br>
The instance is not picked in `yellow'. Agda can't find the instance<br>
even in this case:<br>
<br>
----<br>
<br>
record R (n m : ℕ) : Set where<br>
<br>
instance<br>
r : R 0 1<br>
r = _<br>
<br>
z' : ∀ {m} {{_ : R 0 m}} -> ℕ<br>
z' = 0<br>
<br>
yellow' : z' ≡ 0<br>
yellow' = refl<br>
<br>
ok' : z' {1} ≡ 0<br>
ok' = refl<br>
<br>
----<br>
<br>
Should I report this as a bug, or is this a known limitation?<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>