[Agda] Typeclasses again in release-candidate/master

[David Darais]

I tested this idea and it fails to convince Agda to resolve the instance.

I have a large codebase with instances like this, so if you have any more ideas
please let me know.

Thanks,
David

> open import Agda.Primitive
> 
> data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
>   refl : x ≡ x
> 
> {-# BUILTIN EQUALITY _≡_ #-}
> {-# BUILTIN REFL refl #-}
> 
> 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[ℕ] : ∀ {ℓ} {{E : ℓ ≡ lzero}} → Order ℓ ℕ
>   Order[ℕ] {{refl}} = record { _≤_ = _≤ⁿ_ }
> 
> subtract : ∀ (n₁ n₂ : ℕ) → n₂ ≤ n₁ → ℕ
> subtract n₁ n₂ P = {!!}

> On Feb 20, 2016, at 11:55 AM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
> 
> In Haskell you would hack this sort of thing with an equality
> constraint, so that the instance matches any level, including metas,
> but then the constraint solver sets the level to lzero:
> 
> instance (l ~ lzero) => Order l ℕ where { ... }
> 
> 
> 
> 
> 
> 
> 
> On Sat, Feb 20, 2016 at 9:05 AM, Ulf Norell <ulf.norell at gmail.com> wrote:
>> Yes that might be something to consider.
>> 
>> / Ulf
>> 
>> On Sat, Feb 20, 2016 at 8:33 AM, effectfully <effectfully at gmail.com> wrote:
>>> 
>>> Ulf Norell, would it make sense to give a special treatment for level
>>> metas wrt instance search? Records are very often parameterized by
>>> levels and it doesn't feel good to choose between universe
>>> polymorphism and instance search.
>> 
>> 
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>