haskell - 无法推断 (m ~ m1)

Question

在 GHC 中编译此程序时:

import Control.Monad

f x = let
  g y = let
    h z = liftM not x
    in h 0
  in g 0

我收到一个错误:

test.hs:5:21:
    Could not deduce (m ~ m1)
    from the context (Monad m)
      bound by the inferred type of f :: Monad m => m Bool -> m Bool
      at test.hs:(3,1)-(7,8)
    or from (m Bool ~ m1 Bool, Monad m1)
      bound by the inferred type of
               h :: (m Bool ~ m1 Bool, Monad m1) => t1 -> m1 Bool
      at test.hs:5:5-21
      `m' is a rigid type variable bound by
          the inferred type of f :: Monad m => m Bool -> m Bool
          at test.hs:3:1
      `m1' is a rigid type variable bound by
           the inferred type of
           h :: (m Bool ~ m1 Bool, Monad m1) => t1 -> m1 Bool
           at test.hs:5:5
    Expected type: m1 Bool
      Actual type: m Bool
    In the second argument of `liftM', namely `x'
    In the expression: liftM not x
    In an equation for `h': h z = liftM not x

为什么？此外，为 f 提供显式类型签名( f :: Monad m => m Bool -> m Bool ) 使错误消失。但这与 Haskell 为 f 推断的类型完全相同。自动，根据错误信息!

Answer 1

实际上，这很简单。 let 的推断类型-bound 变量被隐式推广到类型方案，所以你的方式有一个量词。 h 的广义类型是:

h :: forall a m. (Monad m) => a -> m Bool

和 f 的广义类型是:

f :: forall m. (Monad m) => m Bool -> m Bool

他们不一样 m .如果你写这个，你会得到基本上相同的错误:

f :: (Monad m) => m Bool -> m Bool
f x = let
  g y = let
    h :: (Monad m) => a -> m Bool
    h z = liftM not x
    in h 0
  in g 0

您可以通过启用“作用域类型变量”扩展来修复它:

{-# LANGUAGE ScopedTypeVariables #-}

f :: forall m. (Monad m) => m Bool -> m Bool
f x = let
  g y = let
    h :: a -> m Bool
    h z = liftM not x
    in h 0
  in g 0

或者通过禁用 let - 使用“单态本地绑定(bind)”扩展的泛化， MonoLocalBinds .