<div dir="ltr"><div>The standard library could conceivably have separate files containing instances, e.g. Data.Nat.Instances would re-export Data.Nat.Literals.number as an instance. The fact that the standard library doesn't have instances is certainly one of the reasons I currently *don't* use it (and use Ulf's Prelude instead).<br></div><div><br></div><div>-- Jesper<br></div>
</div><br><div class="gmail_quote"><div dir="ltr">On Thu, Dec 6, 2018 at 7:09 AM Ulf Norell <<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">The Unit issue is due to Jesper's recent changes to instance arguments.<div>See <a href="https://github.com/agda/agda/pull/3419/commits/5c79dc03d1f3f4c2831c0a910387cdf41c57fb1f" target="_blank">https://github.com/agda/agda/pull/3419/commits/5c79dc03d1f3f4c2831c0a910387cdf41c57fb1f</a></div><div>for the documentation. Instance goals solved by unification still counts as </div><div>a missing instance if the solution isn't an instance.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">We are a bit reluctant to add instance declarations to the standard<br>library because they can't be hidden upon module import so users would<br>necessarily have them in scope even if they don't want them.</blockquote><div><br></div><div>Instances can be hidden on import as follows:</div><div><br></div><div><div> import Bar hiding (someInstance)</div><div> open Bar</div></div><div><br></div><div>If you write `open import Bar hiding (someInstance)` this desugars into</div><div><br></div><div> import Bar</div><div> open Bar hiding (someInstance)</div><div><br></div><div>which still leaves it in scope as `Bar.someInstance`</div><div><br></div><div>/ Ulf</div></div></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Dec 6, 2018 at 2:21 AM Guillaume Allais <<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I meant not importing anything unit-related.<br>
I don't get any error (using either 2.5.4.2 or 2.6.0-329b843) with:<br>
<br>
```<br>
open import Agda.Builtin.FromNat<br>
open import Data.Nat<br>
open import Data.Nat.Literals<br>
open import Data.Fin<br>
open import Data.Fin.Literals<br>
<br>
instance<br>
_ = Data.Nat.Literals.number<br>
_ = Data.Fin.Literals.number<br>
<br>
test-nat : ℕ<br>
test-nat = 3<br>
<br>
test-fin : Fin 7<br>
test-fin = 3<br>
```<br>
<br>
<br>
On 06/12/2018 01:58, Martin Stone Davis wrote:<br>
> Hi Guillaume,<br>
><br>
> I'm not sure what you meant by your remark that it's not necessary to import<br>
> Data.Unit. Did you just mean that it could be replaced with an import of<br>
> Agda.Builtin.Unit? If you meant that it could simply be removed, know that,<br>
> without that import, I get the following error in `test-nat`:<br>
><br>
> ```<br>
> No instance of type ;Agda.Builtin.Unit.⊤ was found in scope.<br>
> when checking that 3 is a valid argument to a function of type<br>
> {a : ;Agda.Primitive.Level} {A : Set a} ⦃ r : Number A ⦄ (n : ℕ)<br>
> ⦃ _ : r .Number.Constraint n ⦄ →<br>
> A<br>
> ```<br>
><br>
> -M<br>
><br>
><br>
> On 12/05/2018 12:04 PM, Guillaume Allais wrote:<br>
>> Hi Martin,<br>
>><br>
>> That looks like a reasonable module definition (with the side remark<br>
>> that it's not necessary to import Data.Unit).<br>
>><br>
>> We are a bit reluctant to add instance declarations to the standard<br>
>> library because they can't be hidden upon module import so users would<br>
>> necessarily have them in scope even if they don't want them.<br>
>><br>
>> As for the Data.Fin.Literals.number if we do need the natural number<br>
>> to be implicit for it to be usable directly as an instance, I think<br>
>> that should indeed be modified in the stdlib.<br>
>><br>
>> Cheers,<br>
>> -- <br>
>> gallais<br>
>><br>
>><br>
>> On 05/12/2018 06:31, Martin Stone Davis wrote:<br>
>>> To get both Nat and Fin literals using the standard library (latest development<br>
>>> versions, including Jesper's latest re: instance resolution), I write the<br>
>>> following:<br>
>>><br>
>>> ```agda<br>
>>> open import Agda.Builtin.FromNat<br>
>>> open import Data.Nat<br>
>>> open import Data.Nat.Literals<br>
>>> open import Data.Fin<br>
>>> open import Data.Fin.Literals<br>
>>> open import Data.Unit -- or Agda.Builtin.Unit<br>
>>><br>
>>> instance<br>
>>> _ = Data.Nat.Literals.number<br>
>>><br>
>>> _ : ∀ {n} → Number (Fin n)<br>
>>> _ = Data.Fin.Literals.number _<br>
>>><br>
>>> test-nat : ℕ<br>
>>> test-nat = 3<br>
>>><br>
>>> test-fin : Fin 7<br>
>>> test-fin = 3<br>
>>> ```<br>
>>><br>
>>> It's a bit annoying to need to import from Agda.Builtin.FromNat and from<br>
>>> Data.Unit, so I wonder if this is the recommended approach? Also, should<br>
>>> Data.Fin.Literals.number be updated to take a hidden argument (given that the<br>
>>> new instance resolution does not count explicit arguments as instance arguments<br>
>>> anymore)?<br>
>>><br>
>>> _______________________________________________<br>
>>> Agda mailing list<br>
>>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>