这里有一个解决这个问题的方法。这个方法有点局限--在这种情况下适用，因为所讨论的特定程序只使用了Nat中的几个类型。它也是低效的。但它至少避免了使用像unsafeCoerce或OverlappingInstances这样的讨厌的东西。
GHC的困难在于处理FuncN类型族。要对apply函数的ConsN子句的右侧进行类型检查，GHC需要推导出FuncN (n + 1) ~ Double -> FuncN n。当特定类型（0，1，2...）替代了n，但无法推导出具有类型变量n的一般形式。
您可以考虑使用FuncN (n + 1) = Double -> FuncN n作为FuncN定义的第二个子句，但这是不允许的，因为操作符(+)不是构造函数：这是一个类型族，即使可以这样做，我也不认为会有什么帮助，因为GHC甚至不能排除FuncN的第一个子句适用于n + 1的可能性.
解决这个问题的技巧是生成类型相等的证据，以命题相等项FuncN (n + 1) :~: Double -> FuncN n的形式。我们为函数定义了一个类型别名，该函数将Nat中特定类型的代理Map到相应的证据上。

type FuncNProp n = Typeable n => Proxy n -> (FuncN (n + 1) :~: (Double -> FuncN n))

我们需要Typeable约束，这样才能使用eqT。
我还没有找到构造这种类型的全函数的方法，但这里有一个只包含0和1的方法，这是我们在这个特定程序中唯一需要的。

funcNProp :: forall n . FuncNProp n
funcNProp (proxy :: Proxy n) = case eqT @n @0
                                    of Just Refl -> Refl
                                       Nothing -> case eqT @n @1
                                                       of Just Refl -> Refl
                                                          Nothing -> error "Operators with arity greater than 2 not supported"

eqT测试允许GHC分别考虑0和1情况。返回的Refl值是GHC可以进行类型检查的证据，因为它可以推导出Nat中特定的单个类型的FuncN (n + 1) ~ Double -> FuncN n。
然后，我们更新apply的第二个子句，以使用此证据

apply f (ConsN x (xs :: ListN n' Double)) = case funcNProp (Proxy :: Proxy n' ) of Refl -> apply (f x) xs

...在ConsN模式子句中，我们还将n'与该类型匹配。使用该类型，我们构造一个代理传递给funcNProp，该代理生成对apply (f x) xs进行类型检查所需的证据。
以下是完整的计划：

{-#LANGUAGE FlexibleInstances
          , GADTs
          , DataKinds
          , TypeFamilies
          , TypeOperators
          , UndecidableInstances
          , ScopedTypeVariables
          , RankNTypes
          , TypeApplications
          , FlexibleContexts #-}

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

import GHC.TypeNats ( Nat, type (+), type (-) )
import Data.Typeable ( Typeable, Proxy(..), type (:~:)(..), eqT )

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

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

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

type FuncNProp n = Typeable n => Proxy n -> (FuncN (n + 1) :~: (Double -> FuncN n))

funcNProp :: forall n . FuncNProp n
funcNProp (proxy :: Proxy n) = case eqT @n @0
                                    of Just Refl -> Refl
                                       Nothing -> case eqT @n @1
                                                       of Just Refl -> Refl
                                                          Nothing -> error "Operators with arity greater than 2 not supported"

apply :: forall n . FuncN n -> ListN n Double -> Double
apply x EmptyN = x
apply f (ConsN x (xs :: ListN n' Double)) = case funcNProp (Proxy :: Proxy n' ) of Refl -> 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)

事实证明，还有另一种解决方案，只需添加一个仔细放置的约束。
如前所述，GHC的难点在于处理FuncN类型族。要对apply函数的ConsN子句的右侧进行类型检查，GHC需要推导出FuncN (n + 1) ~ Double -> FuncN n。当特定类型（0，1，2 ...）替代了n，但无法用类型变量n推导出一般形式。
解决方案是将该约束添加到ListN数据定义的ConsN子句中。也就是说，实际上，只承诺构造满足该属性的列表。由于该属性是一个同义反复，因此这不是一个限制，但是，更重要的是，如果所有ListN构造都是文字的（因此TypeNat是特定示例），GHC能够建立该属性，这是该特定程序的情况。
整个程序：

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

module Main where

import GHC.TypeNats ( Nat, type (+), type (-) )

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

data ListN n a where
    EmptyN :: ListN 0 a
    ConsN :: FuncN (n + 1) ~ (Double -> FuncN n) => a -> ListN n a -> ListN (n + 1) 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)

main :: IO ()
main = let subterm = Apply (OpTerm Sqrt) (ConsN (OpTerm Four) EmptyN)
           term = Apply (OpTerm Add) (ConsN subterm (ConsN (OpTerm Four) EmptyN))
       in print $ eval term