intToNat

IntToNat.hs

data Nat n where
  NZero :: Nat Zero
  NSucc :: forall n. Nat n -> Nat (Succ n)

intToNat :: Int -> forall n. Nat n
intToNat 0 = NZero
intToNat n = NSucc $ intToNat $ pred n

{-
    Couldn't match type ‘n’ with ‘Succ n0’
      ‘n’ is a rigid type variable bound by
          the type signature for intToNat :: Int -> Nat n at Main.hs:58:1
    Expected type: Nat n
      Actual type: Nat (Succ n0)
    In the expression: NSucc $ intToNat $ pred n
    In an equation for ‘intToNat’:
        intToNat n = NSucc $ intToNat $ pred n
-}