我可以让 GHC 推断出超过 GADT 模式匹配的约束吗？

Question

我想让 GHC 推断出超过 GADT 模式匹配的约束。例如，假设我有两个表达式，每个表达式都有一个推断约束：

f :: _ => a
g :: _ => a

（在我的用例中，这些推断的约束可能很大，因此手动将它们写出来是不可行的。）

然后假设我想根据布尔条件使用f 或g。天真地，我可以进行如下操作：

h1 :: _ => Bool -> a
h1 c = if c then f else g

假设我将推断的约束称为f ct_f 和g ct_g，那么GHC 将推断( ct_f, ct_g ) 的约束h1。

问题在于这是一个限制性很强的类型：如果布尔值是True，我不需要ct_g，相反，如果它是False，我不需要ct_f。所以我尝试使用标准机制来启用这种依赖约束：

data SBool (c :: Bool) where
  SFalse :: SBool False
  STrue  :: SBool True

h2 :: _ => SBool bool -> a
h2 = \case
  STrue  -> f
  SFalse -> g

但这不起作用，因为 GHC 的部分类型签名算法拒绝浮动约束超过 GADT 模式匹配。相反，我可以尝试明确地告诉 GHC 该怎么做：

ifC :: forall ct_t ct_f bool x. SBool bool -> ( ct_t => x ) -> ( ct_f => x ) -> ( If bool ct_t ct_f => x )
ifC STrue  a _ = a
ifC SFalse _ b = b

h3 :: _ => SBool bool -> a
h3 c = ifC c f g

这种方法也失败了，这一次是因为 GHC 认为 ifC 的类型签名不明确，即 GHC 需要用户显式传递类似的约束

h4 c = ifC @ct_f @ct_g c f g

不幸的是，我无法明确传递这些约束：我要求 GHC 推断它们，并且无法引用它们。例如，可以尝试将它们纳入如下范围：

h5 :: _ => SBool bool -> a
h5 c = 
  let
    f :: _ct_f => a
    f' = f
    g :: _ct_g => a
    g' = g
  in
    if_C @_ct_f @_ct_g c f' g'

但这是行不通的，因为 GHC 不支持命名通配符代替额外的约束（即使支持，它们也不会正确作用域）。

是否有其他方法可以让 GHC 推断：

h :: ( If bool ct_f ct_g ) => a

Answer 1

我用ImpredicativeTypes 稍微改进了代码。

type family GetBool a where
  GetBool (SBool True) = True 
  GetBool (SBool False) = False

data TF (a :: Constraint) x = TF x

class SIf a pt pf x where
  ifC' :: a -> TF pt x -> TF pf x -> (If (GetBool a) pt pf => x)

instance ((t => x) ~ (f => x)) => SIf (SBool True) t f x where
  ifC' _ (TF t) _ = t

instance ((t => x) ~ (f => x)) => SIf (SBool False) t f x where
  ifC' _ _ (TF f) = f

h3' :: _ => SBool bool -> a
h3' c = ifC' c f g

给它Num a 实例是有效的。

*Main> :t h3' 3
h3' 3
  :: (If (GetBool (SBool bool)) pt pf, SIf (SBool bool) pt pf a,
      Num (SBool bool)) =>
     a

let x = h3' f 现在也可以，但并不完美。我想我们做的是黑魔法......