如何让GHC推断`Arrows (Domains func) (CoDomain func) ~ func`类型等式？

我完全懂你遇到的这个痛点——明明从逻辑上Arrows (Domains func) (CoDomain func)和func就是同一个类型，但GHC就是不认，核心原因就是它没法自动推断Domains、CoDomain和Arrows这几个类型族之间的单射关联。下面是几个实用的解决思路，你可以根据代码场景选择：

1. 用TypeFamilyDependencies给类型族加单射性声明 #

这是最直接的方案，通过GHC的TypeFamilyDependencies扩展，我们可以明确告诉GHC：每个func对应唯一的Domains func和CoDomain func；反过来，给定一组ds和cd，也只会对应唯一的Arrows ds cd。

修改类型族定义，加上依赖箭头|：

{-# LANGUAGE TypeFamilyDependencies #-}

-- 声明Domains是从func到ds的单射：知道ds就能反推func
type family Domains func = ds | ds -> func where
  -- 这里写你的Domains类型族分支定义

-- 同理给CoDomain加单射声明
type family CoDomain func = cd | cd -> func where
  -- 你的CoDomain分支定义

-- 关键：声明Arrows是从ds和cd到func的单射，知道func就能反推ds和cd
type family Arrows ds cd = func | func -> ds cd where
  -- 你的Arrows分支定义

加上这些声明后，GHC就能自动识别Arrows (Domains func) (CoDomain func) ~ func这个等式，你的curries调用应该就能顺利通过类型检查了。

2. 显式构造类型相等性证明（分情况处理） #

如果因为某些原因没法用TypeFamilyDependencies，那可以手动给GHC提供类型相等的证据，也就是你提到的对IsBase（或相关类型类/数据类型）分情况处理。

首先，定义一个证明函数，用来确认Arrows (Domains func) (CoDomain func)和func是相等的：

import Data.Type.Equality
import Data.Proxy

-- 这个函数返回类型相等的证据
arrowsDomainsCodomainEq :: forall func. Proxy func -> (Arrows (Domains func) (CoDomain func) :~: func)
arrowsDomainsCodomainEq p = case someBaseConstraint func of
  -- 根据你的IsBase或其他约束分情况匹配
  IsBaseCase1 -> Refl
  IsBaseCase2 -> Refl
  -- 每个分支返回Refl，GHC会在模式匹配时自动细化类型，承认等式成立

然后用这个证据转换curries的结果类型：

myCurriedFunc :: func
myCurriedFunc = case arrowsDomainsCodomainEq (Proxy :: Proxy func) of
  Refl -> curries (Proxy :: Proxy (Domains func)) (Proxy :: Proxy (CoDomain func)) undefined

当GHC看到Refl时，就会把Arrows ...的类型和func统一起来，自然就能通过检查了。

3. 调整curries的类型签名，直接关联func #

如果curries当前是分开接受Proxy (Domains func)和Proxy (CoDomain func)，可以把它改成直接接受Proxy func，内部自动推导对应的Domains和CoDomain：

curries' :: Proxy func -> func
curries' _ = curries (Proxy :: Proxy (Domains func)) (Proxy :: Proxy (CoDomain func)) undefined

之后直接调用curries' (Proxy :: Proxy func)即可——GHC会在处理curries'的类型时，借助类型族定义自动关联Domains func和CoDomain func，避免手动传递两个Proxy带来的类型推断问题。

4. 用TypeApplications显式指定类型参数 #

启用AllowAmbiguousTypes和TypeApplications扩展，直接告诉GHCcurries应该用的类型参数，帮它理清推导路径：

{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}

myCurriedFunc :: func
myCurriedFunc = curries @(Domains func) @(CoDomain func) Proxy Proxy undefined

不过这个方法通常需要配合前面的单射性声明或者类型相等证明，否则GHC可能还是没法把最终结果的类型和func统一起来。

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