Is there a convenient way to construct larger type level Peano numbers using mono-traversable?

Question

The mono-traversable package uses type level Peano numbers for MinLen. I can construct them using chained Succs:

toMinLen [1,2,3] :: Maybe (MinLen (Succ (Succ Zero)) [Int])

but this quickly gets out of hand:

toMinLen [1,2,3] :: Maybe (MinLen (Succ (Succ (Succ (Succ (Succ Zero))))) [Int])

Is there a convenient way to construct larger Peano numbers? I see GHC has a TypeLiterals extension but I'm not sure if I can use it here. Alternatively, I can make synonyms like:

type One = Succ Zero
type Two = Succ One

and so on; does something like that already exist somewhere?

Answer 1

TypeLits is perfectly good for type-level numerals. Also, it's easy to use it only for syntactic sugar and leave the underlying library-specific implementation unchanged.

{-# LANGUAGE
  UndecidableInstances, TypeFamilies,
  DataKinds, TypeOperators #-}

import qualified GHC.TypeLits as TL

data Nat = Zero | Succ Nat

newtype MinLen (n :: Nat) a = MinLen a

We have to define a type family that converts a literal to the number type:

type family Lit (n :: TL.Nat) :: Nat where
  Lit 0 = Zero
  Lit n = Succ (Lit (n TL.- 1))

Now you can use Lit n whenever you need a Nat literal. In GHCi:

>:kind! MinLen (Lit 3)
MinLen (Lit 3) :: * -> *
= MinLen ('Succ ('Succ ('Succ 'Zero)))