[Agda] using literals and the standard library

[Martin Stone Davis]

I replicated your results with 2.6.0-329b843, but that's prior to 
Jesper's "no-overlapping-instances" update. The failure w/o importing 
Data.Unit occurs in the latest from the master branch (ed8a6aa).


On 12/05/2018 05:20 PM, Guillaume Allais wrote:
> I meant not importing anything unit-related.
> I don't get any error (using either 2.5.4.2 or 2.6.0-329b843) with:
>
> ```
> open import Agda.Builtin.FromNat
> open import Data.Nat
> open import Data.Nat.Literals
> open import Data.Fin
> open import Data.Fin.Literals
>
> instance
>    _ = Data.Nat.Literals.number
>    _ = Data.Fin.Literals.number
>
> test-nat : ℕ
> test-nat = 3
>
> test-fin : Fin 7
> test-fin = 3
> ```
>
>
> On 06/12/2018 01:58, Martin Stone Davis wrote:
>> Hi Guillaume,
>>
>> I'm not sure what you meant by your remark that it's not necessary to import
>> Data.Unit. Did you just mean that it could be replaced with an import of
>> Agda.Builtin.Unit? If you meant that it could simply be removed, know that,
>> without that import, I get the following error in `test-nat`:
>>
>> ```
>> No instance of type ;Agda.Builtin.Unit.⊤ was found in scope.
>> when checking that 3 is a valid argument to a function of type
>> {a : ;Agda.Primitive.Level} {A : Set a} ⦃ r : Number A ⦄ (n : ℕ)
>> ⦃ _ : r .Number.Constraint n ⦄ →
>> A
>> ```
>>
>> -M
>>
>>
>> On 12/05/2018 12:04 PM, Guillaume Allais wrote:
>>> Hi Martin,
>>>
>>> That looks like a reasonable module definition (with the side remark
>>> that it's not necessary to import Data.Unit).
>>>
>>> We are a bit reluctant to add instance declarations to the standard
>>> library because they can't be hidden upon module import so users would
>>> necessarily have them in scope even if they don't want them.
>>>
>>> As for the Data.Fin.Literals.number if we do need the natural number
>>> to be implicit for it to be usable directly as an instance, I think
>>> that should indeed be modified in the stdlib.
>>>
>>> Cheers,
>>> -- 
>>> gallais
>>>
>>>
>>> On 05/12/2018 06:31, Martin Stone Davis wrote:
>>>> To get both Nat and Fin literals using the standard library (latest development
>>>> versions, including Jesper's latest re: instance resolution), I write the
>>>> following:
>>>>
>>>> ```agda
>>>> open import Agda.Builtin.FromNat
>>>> open import Data.Nat
>>>> open import Data.Nat.Literals
>>>> open import Data.Fin
>>>> open import Data.Fin.Literals
>>>> open import Data.Unit -- or Agda.Builtin.Unit
>>>>
>>>> instance
>>>>     _ = Data.Nat.Literals.number
>>>>
>>>>     _ : ∀ {n} → Number (Fin n)
>>>>     _ = Data.Fin.Literals.number _
>>>>
>>>> test-nat : ℕ
>>>> test-nat = 3
>>>>
>>>> test-fin : Fin 7
>>>> test-fin = 3
>>>> ```
>>>>
>>>> It's a bit annoying to need to import from Agda.Builtin.FromNat and from
>>>> Data.Unit, so I wonder if this is the recommended approach? Also, should
>>>> Data.Fin.Literals.number be updated to take a hidden argument (given that the
>>>> new instance resolution does not count explicit arguments as instance arguments
>>>> anymore)?
>>>>
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda at lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>