[Agda] using literals and the standard library

[Ulf Norell]

The Unit issue is due to Jesper's recent changes to instance arguments.
See
https://github.com/agda/agda/pull/3419/commits/5c79dc03d1f3f4c2831c0a910387cdf41c57fb1f
for the documentation. Instance goals solved by unification still counts as
a missing instance if the solution isn't an instance.

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.


Instances can be hidden on import as follows:

  import Bar hiding (someInstance)
  open Bar

If you write `open import Bar hiding (someInstance)` this desugars into

  import Bar
  open Bar hiding (someInstance)

which still leaves it in scope as `Bar.someInstance`

/ Ulf

On Thu, Dec 6, 2018 at 2:21 AM Guillaume Allais <
guillaume.allais at ens-lyon.org> 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
> >
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181206/3f0c7a4d/attachment.html>