Data.Functor.Nest to arbitrary depth

main.hs

{-#LANGUAGE DataKinds #-}
{-#LANGUAGE KindSignatures #-}
{-#LANGUAGE TypeFamilies #-}
{-#LANGUAGE TypeOperators #-}
{-#LANGUAGE UndecidableInstances #-}
{-#LANGUAGE ViewPatterns #-}

module Main where

import Data.Functor.Identity
import Data.Functor.Nested
import Data.Proxy
import GHC.TypeLits

-- | 'Depth 0' has a single @Identity@ constructor.
type family Depth (n :: Nat) where
  Depth 0 = Flat Identity
  Depth a = Nest (Depth (a-1)) Identity

nestToDepth0 :: a -> Nested (Depth 0) a
nestToDepth0 = Flat . Identity

nestToDepth1 :: a -> Nested (Depth 1) a
nestToDepth1 = Nest . Flat . Identity . Identity

test0 = nestToDepth0 ()
test1 = nestToDepth1 ()

-- How can I write the following?
nestToDepthN :: KnownNat (n :: Nat) => Proxy n -> a -> Nested (Depth n) a
nestToDepthN (natVal -> n)
  | n == 0 = nestToDepth0
  | n == 1 = nestToDepth1
  | otherwise = error "I don't know how to write this recursively yet"

-- main.hs:33:14:
--     Couldn't match type ‘Nest (Depth (1 - 1)) Identity’
--                   with ‘Flat Identity’
--     Expected type: a -> Nested (Depth n) a
--       Actual type: a -> Nested (Depth 1) a
--     In the expression: nestToDepth1
--     In an equation for ‘nestToDepthN’:
--         nestToDepthN (natVal -> n)
--           | n == 0 = nestToDepth0
--           | n == 1 = nestToDepth1
--           | otherwise
--           = error "I don't know how to write this recursively yet"

main :: IO ()
main = do
  print test0
  print test1