启用GADTs扩展后Haskell类型推断异常的原因探究

一、启用GADTs后类型推断失败的原因 #

启用GADTs扩展后，即便你没有直接编写GADT语法的代码，GHC的类型推断规则也会发生全局调整：

• 局部定义泛化策略收紧：GADTs启用时，GHC会对let/where中的局部定义采用更保守的泛化逻辑，默认不会为其推断多态类型——哪怕开启NoMonomorphismRestriction也无法改变这一行为。
• 类型绑定优先级改变：你的代码中第一个调用isJust' "a" a会让GHC将isJust'的第二个参数类型固定为Maybe Int，后续传入Maybe [Int]和Maybe (a->a)自然触发类型不匹配错误。

这是因为GADTs扩展需要支持存在类型、依赖类型的检查，GHC必须调整整体类型推断的泛化规则以保证类型安全性，这种影响是全局的，并非只针对显式的GADT定义。

二、类型推断问题的解决方法 #

1. 显式标注局部函数类型 #

这是最直接的方案，即取消注释isJust'的类型注解，强制GHC为其推断多态类型：

isJust' :: String -> Maybe a -> m ()
isJust' tag v = unless (isJust v) do
  warn $ tag <> " is Nothing"

2. 将局部函数提升为顶层函数 #

把isJust'移到模块顶层，GHC会默认对顶层函数进行完全泛化，不受GADTs扩展的局部泛化限制影响：

isJust' :: MonadWriter [String] m => String -> Maybe a -> m ()
isJust' tag v = unless (isJust v) $ tell [tag <> " is Nothing"]

verify :: MonadWriter [String] m => some -> args -> m ()
verify _ _ = do
  let a = Just 1 :: Maybe Int
      b = Just [1, 23] :: Maybe [Int]
      c = Just (id :: forall a. a -> a)
  isJust' "a" a
  isJust' "b" b
  isJust' "c" c

三、fix的替代方案：无需fix获取m类型 #

你使用fix是为了在ScopedTypeVariables下捕获m的类型，更简洁的方式是通过显式forall绑定类型变量，将m的作用域扩展到整个函数体：

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}

module Lib where

import Control.Monad.Writer.CPS
import Data.Maybe
import Control.Monad

-- 用forall显式绑定m的作用域，函数体内可直接引用m
verify :: forall m some args. MonadWriter [String] m => some -> args -> m ()
verify _ _ = do
  let warn = tell . (: [])
      isJust' :: String -> Maybe a -> m ()
      isJust' tag v = unless (isJust v) do
        warn $ tag <> " is Nothing"
      a = Just 1 :: Maybe Int
      b = Just [1, 23] :: Maybe [Int]
      c = Just (id :: forall a. a -> a)
  isJust' "a" a
  isJust' "b" b
  isJust' "c" c

这种方式完全不需要依赖fix，同时保留了类型的多态性。如果不需要some和args的多态性，还可以直接用_代替参数进一步简化代码。

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