Haskell依赖类型模拟中，为何需显式写MkDoor而非_？

这种必须显式写MkDoor而非_的要求，不是技术上的绝对必要，而是GHC当前类型推导能力的局限所致：

• 尽管Door s只有MkDoor这一个构造函数，但GHC的模式匹配推导逻辑不会自动利用“类型唯一构造函数”这个信息，来为_模式关联对应的SDoorStateI s实例。
• 当你显式匹配MkDoor时，GHC会通过构造函数的类型定义，把s对应的单例实例（SDoorStateI s）带入当前作用域；但使用_的话，GHC仅能识别这是一个Door s类型的值，不会主动提取构造函数携带的实例约束。
• 从理论层面看，编译器完全可以实现这种推导——比如在确认类型只有唯一构造函数时，自动将_模式等价于匹配该构造函数，从而获取所需的实例。但目前GHC还没支持这个特性。

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