如何让GHC从一个类型族约束推导另一个类型族约束

你遇到的问题是GHC无法自动识别两个类型族之间的逻辑蕴含关系——即LessGeneric t ~ 'True本应推出MoreGeneric t ~ 'True，但编译器无法自行完成这个推导。下面提供几种可行的解决思路：

方法一：用类型类层次结构编码蕴含关系 #

将类型族的逻辑转换为类型类的超类约束，让GHC通过类型类的层次自动推导约束：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}

import Data.Kind (Type)

-- 标记"属于MoreGeneric"的类型类
class IsMoreGeneric t where
instance IsMoreGeneric Int where
instance IsMoreGeneric Float where
instance IsMoreGeneric t where  -- 兜底实例，对应原类型族的默认分支

-- 让IsLessGeneric的超类是IsMoreGeneric，明确蕴含关系
class IsMoreGeneric t => IsLessGeneric t where
instance IsLessGeneric Float where
instance IsLessGeneric t where  -- 兜底实例

-- 改写函数签名，用类型类约束替代类型族等式
foo :: IsLessGeneric t => t -> ()
foo = bar

bar :: IsMoreGeneric t => t -> ()
bar = const ()

这里IsLessGeneric的实例必须满足IsMoreGeneric约束，因此当foo要求IsLessGeneric t时，GHC会自动推导出IsMoreGeneric t成立，顺利调用bar。

方法二：用辅助类型类封装蕴含规则 #

如果不想完全替换类型族，可以定义一个辅助类型类，专门编码LessGeneric t ~ 'True蕴含MoreGeneric t ~ 'True的规则：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind (Type)

type family MoreGeneric (t :: Type) :: Bool where
  MoreGeneric Int = 'True
  MoreGeneric Float = 'True
  MoreGeneric _ = 'False

type family LessGeneric (t :: Type) :: Bool where
  LessGeneric Float = 'True
  LessGeneric _ = 'False

-- 定义辅助类型类，封装蕴含逻辑
class (LessGeneric t ~ 'True) => LessGenericImpliesMoreGeneric t where
-- 针对Float实例，明确满足MoreGeneric约束
instance {-# OVERLAPPING #-} LessGenericImpliesMoreGeneric Float where
-- 兜底实例：只有当LessGeneric t为False时才匹配，避免冲突
instance {-# OVERLAPPABLE #-} (LessGeneric t ~ 'False) => LessGenericImpliesMoreGeneric t where

-- 使用辅助类型类作为约束
foo :: LessGenericImpliesMoreGeneric t => t -> ()
foo = bar

bar :: MoreGeneric t ~ 'True => t -> ()
bar = const ()

通过重叠实例，我们明确告诉GHC：当t是Float（即LessGeneric t ~ 'True）时，MoreGeneric t ~ 'True必然成立；其他类型要么不满足LessGeneric t ~ 'True，要么自动适配兜底规则。

方法三：直接修改类型族定义 #

如果可能，直接让LessGeneric的定义依赖MoreGeneric，从根源上明确蕴含关系：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind (Type)

type family MoreGeneric (t :: Type) :: Bool where
  MoreGeneric Int = 'True
  MoreGeneric Float = 'True
  MoreGeneric _ = 'False

-- 用MoreGeneric的结果约束LessGeneric的分支
type family LessGeneric (t :: Type) :: Bool where
  LessGeneric Float = 'True
  LessGeneric t = 'False

-- 定义组合约束，一次性表达两个条件
type LessGenericConstraint t = (LessGeneric t ~ 'True, MoreGeneric t ~ 'True)

foo :: LessGenericConstraint t => t -> ()
foo = bar

bar :: MoreGeneric t ~ 'True => t -> ()
bar = const ()

这种方式最直接，通过组合约束明确要求LessGeneric t ~ 'True时必须同时满足MoreGeneric t ~ 'True，让GHC无需额外推导。

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