[Agda] Typeclasses again in release-candidate/master

[Ulf Norell]

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.

/ Ulf

On Sat, Feb 20, 2016 at 7:01 AM, David Darais <darais at cs.umd.edu> wrote:

> Hello again,
>
> Sorry to keep pestering about typeclasses, but here is another example
> from my
> codebase which doesn't typecheck in both 2.5.0.20160213 and master, and
> used to
> typecheck in 2.4.2.5.
>
> > open import Agda.Primitive
> >
> > record Order {ℓ} ℓ' (A : Set ℓ) : Set (ℓ ⊔ lsuc ℓ') where
> >   field
> >     _≤_ : A → A → Set ℓ'
> > open Order {{...}} public
> >
> > data ℕ : Set where
> >   Zero : ℕ
> >   Succ : ℕ → ℕ
> >
> > data _≤ⁿ_ : ℕ → ℕ → Set where
> >   Zero : ∀ {n} → Zero ≤ⁿ n
> >   Succ : ∀ {n₁ n₂} → n₁ ≤ⁿ n₂ → Succ n₁ ≤ⁿ Succ n₂
> >
> > instance
> >   Order[ℕ] : Order lzero ℕ
> >   Order[ℕ] = record { _≤_ = _≤ⁿ_ }
> >
> > subtract : ∀ (n₁ n₂ : ℕ) → n₂ ≤ n₁ → ℕ
> > subtract n₁ n P = {!!}
>
> The issues is that Agda is not able to resolve the use of `≤` in
> `subtract`,
> leaving `n₂ ≤ n₁` highlighted in yellow (unresolved metas). Shouldn't this
> be a
> clear case where Agda picks the `Order[ℕ]` instance?
>
> Thanks,
> David
> _______________________________________________
> 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/20160220/861b1cf7/attachment.html