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