GHC无法根据输入类型推导InferDoorState类型类实例问题

先明确核心问题：手动实现单例类型和InferDoorState类型类后，编写doorStatus_函数时，不指定getSDoorState的类型参数会编译失败（报错“无法推导InferDoorState s0”），但显式指定@s或给参数加类型注解就能正常编译。疑问点在于：函数签名已经声明了InferDoorState s约束，为什么编译器不能自动推导getSDoorState的类型参数？

问题代码回顾 #

基础数据类型

data DoorState = Locked | Closed | Open deriving (Eq, Show) 
newtype Door (s :: DoorState) = UnsafeMkDoor {doorMaterial :: String} deriving (Eq, Show)

单例类型

data SDoorState :: DoorState -> * where
    SLocked :: SDoorState Locked
    SClosed :: SDoorState Closed
    SOpen :: SDoorState Open

类型类与实例

class InferDoorState s where
    getSDoorState :: SDoorState s
instance InferDoorState 'Closed where
    getSDoorState = SClosed
instance InferDoorState 'Locked where
    getSDoorState = SLocked
instance InferDoorState 'Open where
    getSDoorState = SOpen

编译失败的实现

doorStatus_ :: (InferDoorState s) => Door s -> DoorState
doorStatus_ _ = toDoorState getSDoorState -- 错误：无法推导InferDoorState s0

编译成功的实现

doorStatus_ :: (InferDoorState s) => Door s -> DoorState
doorStatus_ (_ :: Door s) = toDoorState (getSDoorState @s)

原因分析 #

Haskell的类型推断遵循Hindley-Milner算法，默认会将未约束的多态值的类型变量泛化。这里getSDoorState的类型是InferDoorState s' => SDoorState s'——它本身是多态的，编译器会把s'当成一个全新的、独立的类型变量，和函数签名里的s没有关联。

虽然函数签名声明了InferDoorState s约束，但这个约束只作用于函数的类型参数s，编译器没有理由自动把getSDoorState的s'和函数的s绑定在一起。没有显式提示的话，编译器无法确定这两个类型变量应该是同一个，因此会报错说无法推导InferDoorState s0（s0就是那个未绑定的s'）。

而显式指定getSDoorState @s，或者给参数加上(_ :: Door s)的注解，本质都是在给编译器传递明确信号：getSDoorState的类型参数就是函数签名里的s，这样InferDoorState s的约束就能被正确应用，编译器也能找到对应的实例。

其他解决方案 #

除了显式指定类型参数，还可以开启ScopedTypeVariables扩展，让函数体内的类型变量和签名里的绑定：

{-# LANGUAGE ScopedTypeVariables #-}

doorStatus_ :: forall s. InferDoorState s => Door s -> DoorState
doorStatus_ _ = toDoorState (getSDoorState :: SDoorState s)

这里forall s显式量化了类型参数，ScopedTypeVariables让函数体内的s和签名里的s指向同一个类型，编译器就能正确推导。

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