Problem with TypeNats vs bespoke data statement

Question

I've been experimenting with an evalation function for a simple expression language, mainly as a way to familiarise myself with some Haskell extensions that I've not used before. The latest experiment is to use DataKinds and TypeFamilies to unify unary and binary operators. After some trouble, I made it work, but only if I represent the arity of the operators with a bespoke definition of the naturals:

data NatT = ZeroT | SuccT NatT

If I instead try to use TypeNats, the compiler fails to match the types. Below is the failing version. It's the second line of the apply function about which the compiler moans - the applications of f to a. The error is failure to match Double -> FuncN (n - 1) with FuncN n, (which is exactly the second line of the definition of FuncN). I can get different errors by using n+1 and n in place of n and n-1. I also tried declaring FuncN to be injective, but the compiler doesn't like that either.

This problem doesn't hugley surprise me and I'm content with the working version using NatT, but interested to see if it is possible to work around the problem while maintaining the use of TypeNats.

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

module FourFours
    ( NularyOp(..)
    , UnaryOp(..)
    , BinaryOp(..)
    , Term(..)
    , ListN(..)
    , eval
    ) where

import GHC.TypeNats

type family FuncN n where
    FuncN 0 = Double
    FuncN n = Double -> FuncN (n - 1)

data ListN n a where
    EmptyN :: ListN 0 a
    ConsN :: a -> ListN (n - 1) a -> ListN n a

instance Functor (ListN n) where
    fmap f EmptyN = EmptyN
    fmap f (ConsN a as) = ConsN (f a) (fmap f as)

apply :: FuncN n -> ListN n Double -> Double
apply x EmptyN = x
apply f (ConsN x xs) = apply (f x) xs

data NularyOp = Four | FortyFour | PointFour   deriving (Eq, Ord, Enum)
data UnaryOp = Sqrt                            deriving (Eq, Ord, Enum)
data BinaryOp = Add | Sub | Mul | Div | Pow    deriving (Eq, Ord, Enum)

class Op o where
    type Arity o :: Nat
    evalOp :: o -> FuncN (Arity o)

instance Op NularyOp where
    type Arity NularyOp = 0
    evalOp Four = 4
    evalOp FortyFour = 44
    evalOp PointFour = 0.4

instance Op UnaryOp where
    type Arity UnaryOp = 1
    evalOp Sqrt = sqrt

instance Op BinaryOp where
    type Arity BinaryOp = 2
    evalOp Add = (+)
    evalOp Sub = (-)
    evalOp Mul = (*)
    evalOp Div = (/)
    evalOp Pow = (**)

data Term n where
    OpTerm :: Op o => o -> Term (Arity o)
    Apply :: Term n -> ListN n (Term 0) -> Term 0


eval :: Term n -> FuncN n
eval (OpTerm o) = evalOp o
eval (Apply o ts) = apply (eval o) (fmap eval ts)