为什么删除空约束会导致编译器错误？答案

【问题标题】：Why does removing an empty constraint cause a compiler error?为什么删除空约束会导致编译器错误？
【发布时间】：2021-11-08 14:41:35
【问题描述】：

我观察到一些我不太理解的行为。这是一个 MWE

{-# Language PatternSynonyms, GADTs #-}
module Test where

data Succ a
data Zero

data Vec n a where
  EmptyVec :: Vec Zero a
  (:+) :: a -> Vec n a -> Vec (Succ n) a

newtype Comp f g a = Comp (f (g a))

pattern CEv :: () => (n ~ Zero) => Comp (Vec n) g a
pattern CEv = Comp EmptyVec

t :: Comp (Vec m) (Vec n) r -> Bool
t (Comp (_ :+ _)) = True
t CEv = False

这编译。但是我们可能会注意到CEv 有两个约束，() => 和(n ~ Zero) =>。由于其中一个是空的，因此删除它不会有任何危害吗？好吧，如果我们删除它 t 就会中断。

pattern CEv :: (n ~ Zero) => Comp (Vec n) g a
pattern CEv = Comp EmptyVec


/XXXXXXX/src/Test.hs:18:3: error:
    • Couldn't match type ‘m’ with ‘Zero’ arising from a pattern
      ‘m’ is a rigid type variable bound by
        the type signature for:
          t :: forall m n r. Comp (Vec m) (Vec n) r -> Bool
        at src/Test.hs:16:1-35
    • In the pattern: CEv
      In an equation for ‘t’: t CEv = False
    • Relevant bindings include
        t :: Comp (Vec m) (Vec n) r -> Bool (bound at src/Test.hs:17:1)
   |
18 | t CEv = False
   |   ^^^

我真的不知道这里发生了什么。为什么删除一个空约束会导致它中断？这两种类型有什么区别？

【问题讨论】：

在常规定义中foo :: c => d => T 等价于foo :: (c,d) => T，如果c 为空，则可以在两种形式中将其删除。但是，在模式同义词中，符号pattern Foo :: c => d => T 具有不同的含义，如下面的 Li-yao Xia 的回答中所解释的那样。也许以不同的含义重用相同的语法并不是那么明智（耸耸肩）。

标签： haskell pattern-matching

【解决方案1】：

Pattern synonyms 有两组约束：必需的和提供的约束。

pattern P :: Req => Prov => T

如果只有一个约束（即一个“=>”箭头），则将其解释为必需的约束：

pattern P :: Req => T  -- means  Req => () => T, with an empty Prov = ()

因此，如果您有一个空的 required 约束，则它没有缩写：

pattern P :: () => Prov => T

在此处删除 () 会将 Prov 约束变为必需的约束，其含义不同（参见 GHC user guide section on Pattern synonyms）。

【讨论】：