Here is how we can use this API to define a `Show`

instance for singleton types:

instance Show (Nat n) where showsPrec p n = showsPrec p (natToInteger n)

A more interesting example is to define a function which maps integers into singleton types:

integerToMaybeNat :: TypeNat n => Integer -> Maybe (Nat n) integerToMaybeNat x = check nat where check y = if x == natToInteger y then Just y else Nothing

The implementation of `integerToMaybeNat`

is a little subtle: by using
the helper function `check`

, we ensure that the two occurrences of
`nat`

(aka `y`

) both have the same type, namely `Nat n`

. There are other
ways to achieve the same, for example, by using scoped type variables,
and providing explicit type signatures.

Now, we can use `integerToNat`

to provide a `Read`

instance for singleton types:

instance TypeNat n => Read (Nat n) where readsPrec p x = do (x,xs) <- readsPrec p x case integerToMaybeNat x of Just n -> [(n,xs)] Nothing -> []