<div dir="ltr">It's the same principle in play here. Agda refuses to proceed with the instance search since there is an unsolved and unconstrained level meta.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Feb 20, 2016 at 7:01 AM, David Darais <span dir="ltr"><<a href="mailto:darais@cs.umd.edu" target="_blank">darais@cs.umd.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello again,<br>
<br>
Sorry to keep pestering about typeclasses, but here is another example from my<br>
codebase which doesn't typecheck in both 2.5.0.20160213 and master, and used to<br>
typecheck in 2.4.2.5.<br>
<br>
> open import Agda.Primitive<br>
><br>
> record Order {ℓ} ℓ' (A : Set ℓ) : Set (ℓ ⊔ lsuc ℓ') where<br>
> field<br>
> _≤_ : A → A → Set ℓ'<br>
> open Order {{...}} public<br>
><br>
> data ℕ : Set where<br>
> Zero : ℕ<br>
> Succ : ℕ → ℕ<br>
><br>
> data _≤ⁿ_ : ℕ → ℕ → Set where<br>
> Zero : ∀ {n} → Zero ≤ⁿ n<br>
> Succ : ∀ {n₁ n₂} → n₁ ≤ⁿ n₂ → Succ n₁ ≤ⁿ Succ n₂<br>
><br>
> instance<br>
> Order[ℕ] : Order lzero ℕ<br>
> Order[ℕ] = record { _≤_ = _≤ⁿ_ }<br>
><br>
> subtract : ∀ (n₁ n₂ : ℕ) → n₂ ≤ n₁ → ℕ<br>
> subtract n₁ n P = {!!}<br>
<br>
The issues is that Agda is not able to resolve the use of `≤` in `subtract`,<br>
leaving `n₂ ≤ n₁` highlighted in yellow (unresolved metas). Shouldn't this be a<br>
clear case where Agda picks the `Order[ℕ]` instance?<br>
<br>
Thanks,<br>
David<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>