能否用类型同义词在声明实例时隐藏类型变量？

我定义了如下类型类：

class Monad m => Convertible m a b where
  convert :: a -> m b

对于许多类型对，转换可以纯函数式完成，无需monadic效应。我尝试用约束同义词简化这类实例的定义：

import Data.Kind
type PureConvertible :: Type -> Type -> Constraint
type PureConvertible a b = forall m . Monad m => Convertible m a b 

原本想通过这个同义词隐藏m，直接定义纯转换的实例：

instance PureConvertible Int String where
  convert _ = pure undefined

但编译报错：

‘convert’ is not a (visible) method of class ‘PureConvertible’

奇怪的是，如果Convertible类没有方法，下面的代码可以正常编译：

class Monad m => Convertible m a b where

type PureConvertible :: Type -> Type -> Constraint
type PureConvertible a b = forall m . Monad m => Convertible m a b 

instance PureConvertible Int String where

请问当类型类包含方法时，能否让这个隐藏m的类型同义词生效？我使用GHC 9.2.4，已启用的扩展包括：

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}

首先要明确：约束同义词不是类型类，它只是现有约束逻辑的别名，不能直接为它写实例并提供方法定义。你真正需要的是一次性为所有Monad m定义Convertible m a b实例，而非为约束同义词本身实现方法。

方法一：借助辅助类+量化约束 #

先定义一个专门处理纯转换的辅助类，再利用量化约束为所有Monad自动生成Convertible实例：

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}

class Monad m => Convertible m a b where
  convert :: a -> m b

-- 专门处理纯转换的辅助类
class PureConvertible a b where
  convertPurely :: a -> b

-- 对所有Monad m，只要PureConvertible a b成立，就自动实现Convertible m a b
instance (Monad m, PureConvertible a b) => Convertible m a b where
  convert = pure . convertPurely

-- 现在可以直接定义纯转换实例，无需关心Monad类型
instance PureConvertible Int String where
  convertPurely = show

方法二：直接定义覆盖所有Monad的实例 #

如果不想额外定义辅助类，也可以直接用forall m限定，一次性为所有Monad类型实现Convertible实例：

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}

class Monad m => Convertible m a b where
  convert :: a -> m b

-- 直接为所有Monad m定义Int到String的转换实例
instance forall m. Monad m => Convertible m Int String where
  convert = pure . show

关于约束同义词的正确用法 #

如果你还是想用PureConvertible约束同义词来表达“该转换对所有Monad都有效”，可以在函数类型签名中使用它强化约束，但实例定义仍需用上面的方式：

-- 保留约束同义词
type PureConvertible a b = forall m. Monad m => Convertible m a b

-- 函数要求输入输出必须是纯可转换的（对任意Monad都生效）
process :: PureConvertible a b => a -> IO b
process = convert

为什么原写法报错 #

PureConvertible是约束同义词，没有自己的方法集。当你写instance PureConvertible ... where convert = ...时，GHC找不到PureConvertible类对应的convert方法，因此报错。而当Convertible没有方法时，instance PureConvertible ...只是断言“对所有Monad m，Convertible m Int String成立”，不需要实现任何方法，所以能编译通过。

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