[Agda] using literals and the standard library

[Martin Stone Davis]

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)?

[Guillaume Allais]

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

To get both Nat and Fin literals using the standard library (latest development
versions, including Jesper's latest re: instance resolution), I write the
```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
https://lists.chalmers.se/mailman/listinfo/agda

[Martin Stone Davis]

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

Post by Guillaume Allais
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

To get both Nat and Fin literals using the standard library (latest development
versions, including Jesper's latest re: instance resolution), I write the
```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
https://lists.chalmers.se/mailman/listinfo/agda

[Guillaume Allais]

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
```

Post by Martin Stone Davis
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,
```
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

Post by Guillaume Allais
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

To get both Nat and Fin literals using the standard library (latest development
versions, including Jesper's latest re: instance resolution), I write the
```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
https://lists.chalmers.se/mailman/listinfo/agda

[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).

Post by Guillaume Allais
I meant not importing anything unit-related.
```
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
```

Post by Martin Stone Davis
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,
```
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

Post by Guillaume Allais
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

To get both Nat and Fin literals using the standard library (latest development
versions, including Jesper's latest re: instance resolution), I write the
```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
https://lists.chalmers.se/mailman/listinfo/agda