Haskell中GADT的Functor实例实现，unliftExprF类型检查失败问题

错误根因 #

你写的unliftExprF本身在类型逻辑上不成立：
ExprF a的构造子Fmap封装了两个值：类型为x -> a的转换函数，和类型为Expr x的原始表达式。你要返回的Expr a和内部的Expr x是完全不同的类型，你没有对转换函数做任何处理就直接返回内部的Expr x，当然无法通过类型检查。
更深层的逻辑问题是：经过fmap转换后的ExprF a的参数a可以是任意类型（比如你可以把Expr Int通过fmap show转成ExprF String），但你的Expr GADT仅支持Int和Bool两种类型的取值，天然就不可能把任意ExprF a转回Expr a。

解决方案 #

方案1：保留现有结构，调整unlift逻辑 #

你已经实现了Reval类型类和eval函数，完全可以通过「先求值、应用转换函数、再重新构造Expr」的方式实现类型安全的unlift，只需要给函数加上Reval a约束即可：

unliftExprF :: Reval a => ExprF a -> Expr a
unliftExprF (Fmap f e) = reval $ f $ eval e

如果你不需要拿到Expr实例，只是要对ExprF求值，可以直接实现ExprF的求值函数，完全不需要unlift：

evalF :: Eq a => ExprF a -> a
evalF (Fmap f e) = f $ eval e

方案2：直接实现带约束的Functor（需要ConstraintKinds扩展） #

如果你不想用ExprF中间层，可以按照《The Constrained-Monad Problem》的思路实现带约束的Functor类，代码如下：

{-# LANGUAGE GADTs, ConstraintKinds, KindSignatures, TypeFamilies #-}
import GHC.Exts (Constraint)

-- 带约束的Functor类
class CFunctor (f :: * -> *) where
  type C f a :: Constraint
  cfmap :: (C f a, C f b) => (a -> b) -> f a -> f b

-- 给Expr实现CFunctor实例，约束类型必须是Reval的实例
instance CFunctor Expr where
  type C Expr a = (Eq a, Reval a)
  cfmap f e = reval $ f $ eval e

内容的提问来源于stack exchange，提问作者Dragno