约束的类型别名不与上下文共享相同的变量绑定行为

Question

我一直在玩,-XConstraintKinds以帮助缓解过于冗长的上下文,并在变量绑定方面发现了一个有趣的不一致:

{-# LANGUAGE
    TypeFamilies
  , ConstraintKinds
  , FlexibleContexts
  #-}

-- works
foo :: ( callTree ~ SomeTypeFunc output
       , OtherTypeFunc input ~ callTree
       ) => input -> output


type FooCtx input output =
  ( callTree ~ SomeTypeFunc output
  , OtherTypeFunc input ~ callTree
  )

-- doesn't work
foo' :: FooCtx input output =>
        input -> output

除了callTree进入顶级范围之外,还有解决方法吗？

Answer 1

没有真正的不一致,就是这样

1. 类型签名中的自由类型变量会forall自动添加量词,因此第一种情况实际上相当于

   foo :: forall callTree output input. ( callTree ~ SomeTypeFunc output
          , OtherTypeFunc input ~ callTree
          ) => input -> output
   

2. type声明右侧的所有自由类型变量必须是参数,不能包含任何不在范围内的变量.

这不是特定于约束种类,除了不能forall直接将量词应用于约束的不幸事实,这意味着我不知道使这种约束类型声明起作用的一般解决方法.

在您的特定示例中,( OtherTypeFunc input ~ SomeTypeFunc output )应该是等效的,但我假设您真的对一个更复杂的示例感兴趣,其中这样的重写不起作用.

我可以想到一种不同的解决方法,通过在约束的右侧包含值,以不同的方式将参数更改为类型声明:

{-# LANGUAGE TypeFamilies, ConstraintKinds, FlexibleContexts, RankNTypes #-}

type family OtherTypeFunc a
type family SomeTypeFunc a

type FooCtx input output value =
  forall callTree. ( callTree ~ SomeTypeFunc output
  , OtherTypeFunc input ~ callTree
  ) => value

-- This now works
foo' :: FooCtx input output ( input -> output )

foo' = undefined