[Agda] Typeclasses again in release-candidate/master

[Andrea Vezzosi]

Oh, sorry, I didn't mean to imply it would work in Agda.

On Sat, Feb 20, 2016 at 7:30 PM, David Darais <darais at cs.umd.edu> wrote:
> 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
>>>
>