https://stackoverflow.com/a/47300525/477476

NumFin.agda

open import Agda.Builtin.FromNat
open import Data.Fin

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Nat renaming (_≤?_ to _N≤?_)
open import Data.Unit

instance
  NumFin : ∀ {n} → Number (Fin n)
  Number.Constraint (NumFin {n}) k = True (suc k N≤? n)
  Number.fromNat NumFin m {{m<n}}= #_ m {m<n = m<n}

instance
  NumNat : Number ℕ
  Number.Constraint NumNat _ = ⊤
  Number.fromNat NumNat m = m

data I'mFinnish : Set where
  Mk : Fin 5 → I'mFinnish

foo : I'mFinnish
foo = Mk (# 3)

open import Data.Bool

-- This fails with
--     suc is not a constructor of the datatype Fin
--     when checking that the pattern suc (suc (suc zero)) has type Fin (fromNat 5)

bar′ : I'mFinnish → Bool
bar′ (Mk 3) = true
bar′ _      = false