[Agda] Typeclasses again in release-candidate/master

[David Darais]

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