Haskell中是否可无需额外参数引入存在类型量化带约束类型变量？

现有代码报错的本质 #

你定义的Exists是基于GADT的存在量化类型，构造器内部绑定的类型变量m，作用域完全封闭在构造器内部，对外是不可见的。之前的convBad实现里，手动写@m指称的变量既没有在函数顶层签名中声明，也不属于当前作用域的合法绑定，自然会触发“Not in scope: type variable ‘m’”的类型错误。

你之前借助Proxy中转的实现方案，本质是把本该封装在存在类型内部的m，强行暴露成了函数的顶层参数，让调用者可以直接选择m的具体类型，这恰恰破坏了存在类型“隐藏内部实现细节”的设计初衷。

无需额外参数的正确实现 #

完全不需要Proxy做类型中转，只要借助类型推导的自动绑定，就能实现符合设计要求的逻辑：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- 保持原有存在类型定义不变
data Exists x = forall m. Monad m => Exists (m x)

-- 无任何额外参数的合法实现
conv :: Monad m => x -> Exists x
conv x = Exists (return x)

这个实现的核心逻辑：

• 函数顶层签名里声明的m，是带Monad约束的合法类型变量，作用域覆盖整个函数体
• 调用Exists构造器时，类型检查器会自动把传入的return x对应的类型，匹配绑定到构造器要求的存在变量m上，既不需要手动用@m显式指称，也不需要额外的参数中转
• 整个流程中m是函数实现层的内部选择，对外完全隐藏，完全符合Exists类型的封装设计目标

拓展说明 #

如果构造Exists时使用的m不是来自函数顶层签名的类型变量，也完全可以根据传入的表达式自动推导，不需要任何外部参数：

-- 直接固定用IO作为内部monad构造值
convToIO :: x -> Exists x
convToIO x = Exists (pure x :: IO x)

类型检查器会自动识别传入表达式的具体类型m，验证它满足Monad约束后正常构造Exists值，全程不需要任何显式的类型参数传递。

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