Haskell singletons库：case-of与let绑定模式匹配差异解析

我在学习singletons库时，手动为自定义List类型实现SingKind实例。发现toSing函数用case-of匹配SomeSing时能正常运行，但改用let绑定模式匹配就触发类型错误，提示类型变量会逃逸作用域，想搞懂两者的行为差异和失败原因。

自定义类型与实例定义 #

data List a = Nil | Cons a (List a)

data SList :: List a -> Type where
    SNil  :: SList 'Nil
    SCons :: Sing x -> SList xs -> SList ('Cons x xs)

type instance Sing = SList

instance SingKind k => SingKind (List k) where
    type Demote (List k) = List (Demote k)
    fromSing :: Sing (a :: List k) -> List (Demote k)
    toSing :: List (Demote k) -> SomeSing (List k)

可行的case-of实现 #

toSing (Cons x xs) = case toSing x of
    SomeSing singX -> case toSing xs of
        SomeSing singXs -> SomeSing $ SCons singX singXs

失败的let绑定实现 #

toSing (Cons x xs) =
    let SomeSing singX = toSing x
        SomeSing singXs = toSing xs
    in  SomeSing $ SCons singX singXs

错误信息 #

error:
    • Couldn't match type ‘x0’ with ‘a’
      Expected: Sing @k x0
        Actual: Sing @k1 a
    • because type variable ‘a’ would escape its scope
    This (rigid, skolem) type variable is bound by
      a pattern with constructor:
        SomeSing :: forall k (a :: k). Sing a -> SomeSing k,
      in a pattern binding
      at door.hs:169:13-26
    • In the pattern: SomeSing singX
      In a pattern binding: SomeSing singX = toSing x
      In the expression:
        let
          SomeSing singX = toSing x
          SomeSing singXs = toSing xs
        in SomeSing $ SCons singX singXs
    • Relevant bindings include
        singXs :: SList xs0 (bound at door.hs:170:22)
        xs :: List (Demote k1) (bound at door.hs:168:20)
        x :: Demote k1 (bound at door.hs:168:18)
        toSing :: List (Demote k1) -> SomeSing (List k1)
          (bound at door.hs:167:5)
    |
    |         let SomeSing singX = toSing x
    |                      ^^^^^

行为差异与失败原因 #

核心在于Haskell对case表达式和let绑定的类型变量作用域处理逻辑完全不同：

1. case表达式的类型上下文管理 #

当用case匹配SomeSing singX时，singX对应的隐藏类型变量（即SomeSing包装的Sing a中的a）会被严格限制在当前case分支的作用域内。编译器能完整追踪到这个类型变量和toSing x返回值的关联，后续在分支内用SCons组合singX和singXs时，能正确推导两者的类型依赖关系，不会出现类型逃逸。

2. let绑定的模式匹配问题 #

let绑定的模式匹配中，Haskell会把SomeSing singX里的隐藏类型变量标记为刚性skolem变量——这是一种不可被统一的局部类型变量，仅绑定在let的定义作用域内。当你在in部分尝试将singX和singXs组合成SCons并包装成SomeSing返回时，相当于试图把这些局部作用域的skolem变量暴露到外部作用域，破坏了类型变量的作用域边界，因此编译器触发“类型变量逃逸作用域”的错误。

本质原因 #

SomeSing是存在类型：它只承诺存在某个类型a使得内部是Sing a，但不会暴露具体的a。case匹配会在分支内部临时绑定这个隐藏类型，确保它只在分支内有效；而let绑定的模式匹配会试图将这个隐藏类型变量“提取”到外部，脱离了存在类型的原始上下文，导致编译器无法保证类型一致性。

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