来自《Haskell in Depth》一书的 §13.2节，讲的是通过单例在Haskell中“伪造”依赖类型。

下面是一段来自该节的代码片段：

doorState :: forall s. Door s -> DoorState
doorState MkDoor =
  case sDoorState :: SDoorState s of
    SOpened -> Opened
    SClosed -> Closed

紧接着是以下评注：

如果我们把左边的 MkDoor 模式替换为 _，将不会有对应的 SDoorStateI 实例可用。届时GHC会报错。理解类型层的信息随值而来这一点非常重要。我们通过模式匹配来访问它。

我的问题是：为什么？

至少在上面的例子中，MkDoor 是唯一的 Door s 构造器，

data Door (s :: DoorState) where
  MkDoor :: SDoorStateI s => Door s

因此它是在为 doorState 的定义编写模式匹配时唯一可能写的内容，即便我写成

doorState :: forall s. Door s -> DoorState
doorState _ =
  -- same as above

我也会预计GHC能推断出 MkDoor 是我在那儿可以写的唯一内容。

所以我的问题是：写成 MkDoor 而不是 _ 来引入 SDoorStateI s 的事实，是否是一个技术上的必然？也就是说，如果GHC把我的 _ 换成 MkDoor，并继续进行类型检查和编译，某些错误的程序可能会产生，还是仅仅是“没有人给GHC提供了这样一个能力”？

解决方案

你其实并没有把对这个新GHC能力的设想说清楚。你是在设想GHC在一个极其特殊的情形下——一个ADT或 GADT只有一个没有字段的构造子——会将模式 _ 替换为那个构造子吗？

如果是这样，这将改变某些程序的含义。给定：

data Foo = MkFoo

bar :: Foo -> Bool
bar _ = True

表达式 bar (last (repeat MkFoo)) 的求值结果是 True。如果GHC将 _ 重写为 MkFoo，它将得到 ⊥。