看似无可辩驳的 GADT 模式上的失败匹配

Question

继续我的十字军打击MonadFail是在我的单子约束，我现在面临如下：

data Thing :: Bool -> Type where
  TrueThing :: Thing 'True
  FalseThing :: Thing 'False

myFunc :: Monad m => m ()
myFunc = do
  TrueThing <- return TrueThing
  return ()

这不会编译，因为你猜对了：

• Could not deduce (MonadFail m)
    arising from a do statement
    with the failable pattern ‘TrueThing’

事实上，如果我阅读了我能找到的关于该主题的任何¹文档，我不太清楚匹配应该如何在 GADT 上工作。我显然会认为这个案例属于“无条件匹配”的保护伞。但我承认它不符合“单一构造函数data类型” ^{2 的条件}。尽管避免这种歧义是首先使用 GADT 的重点。

当然~lazyPattern有效，但这只是创可贴。我已经对比赛进行了脱糖：

myFunc' :: Monad m => m ()
myFunc' = let f :: _
              f TrueThing = return ()
          in return TrueThing >>= f

现在，虽然错误消息不是那么明确 ( Couldn't match expected type ‘p’ with actual type ‘m0 ())，但类型通配符更能说明问题：

• Found type wildcard ‘_’ standing for ‘Thing a -> p’

……并引导我走向“解决方案”：

myFunc' :: forall m. Monad m => m ()
myFunc' = let f :: Thing 'True -> m ()
              f TrueThing = return ()
          in return TrueThing >>= f

Well, that works. Can I sugar it back? f doesn't occur in the initial expression, but there are two spots I can annotate with a type: the monadic expression and the pattern. I've tried both separately as well as together, and it's all “could not deduce MonadFail”.

I suppose my expectations were too high, but I'd like to understand why. Is it some type inference limitation? A GADT one? Am I not using the right machinery in the first place? How could this pattern fail at all?

---

(1) It's hard to find an authority on the subject. The GHC manual mentions MonadFail, but links to the HaskellPrime wiki, which seems to be an older revision of the same page on the Haskell wiki

(2)也Bool用()作品代替。但就我的实际问题而言，这过于简单化了。

Answer 1

这可能不是一个完全令人满意的答案，但无论如何我想分享我的发现。

我从确实可能发生模式匹配失败的情况开始，修改您的 GADT 为'True. 然后我添加了一个MonadFail上下文只是为了让 ti 编译，稍后看看它在哪里使用。

{-# LANGUAGE GADTs , DataKinds, KindSignatures #-}
{-# OPTIONS -Wall #-}

import Data.Kind
import Control.Monad.Fail

data Thing :: Bool -> Type where
  TrueThing :: Thing 'True
  FalseThing :: Thing 'False
  TrueThing2 :: Thing 'True

myFunc :: (Monad m, MonadFail m) => m ()
myFunc = do
  TrueThing <- return TrueThing
  return ()

上面的代码产生以下核心：

myFunc
  = \ (@ (m_a1mR :: * -> *))
      _ [Occ=Dead]
      ($dMonadFail_a1mU :: MonadFail m_a1mR) ->
      let {
        $dMonad1_a1nj :: Monad m_a1mR
        [LclId]
        $dMonad1_a1nj
          = Control.Monad.Fail.$p1MonadFail @ m_a1mR $dMonadFail_a1mU } in
      >>=
        @ m_a1mR
        $dMonad1_a1nj
        @ (Thing 'True)
        @ ()
        (return
           @ m_a1mR $dMonad1_a1nj @ (Thing 'True) GADTmonad.$WTrueThing)
        (\ (ds_d1ol :: Thing 'True) ->
           case ds_d1ol of {
             TrueThing co_a1n5 ->
               return @ m_a1mR $dMonad1_a1nj @ () GHC.Tuple.();
             TrueThing2 ipv_s1ph ->
               Control.Monad.Fail.fail
                 @ m_a1mR
                 $dMonadFail_a1mU
                 @ ()
                 (GHC.CString.unpackCString#
                    "Pattern match failure in do expression at GADTmonad.hs:15:3-11"#)
           })

以上，我们可以看到：

• Monad正在传递的字典myFunc被丢弃！相反，字典是从字典中恢复的MonadFail（包括字典Monad）。我不知道为什么 GHC 更喜欢那个。
• 该MonadFail词典是用来处理TrueThing2在最后的比赛情况。这是预料之中的。

现在，如果我们删除TrueThing2构造函数，我们会得到以下核心：

myFunc
  = \ (@ (m_a1mJ :: * -> *))
      _ [Occ=Dead]
      ($dMonadFail_a1mM :: MonadFail m_a1mJ) ->
      let {
        $dMonad1_a1nb :: Monad m_a1mJ
        [LclId]
        $dMonad1_a1nb
          = Control.Monad.Fail.$p1MonadFail @ m_a1mJ $dMonadFail_a1mM } in
      >>=
        @ m_a1mJ
        $dMonad1_a1nb
        @ (Thing 'True)
        @ ()
        (return
           @ m_a1mJ $dMonad1_a1nb @ (Thing 'True) GADTmonad.$WTrueThing)
        (\ (ds_d1od :: Thing 'True) ->
           case ds_d1od of { TrueThing co_a1mX ->
           return @ m_a1mJ $dMonad1_a1nb @ () GHC.Tuple.()
           })

现在TrueThing2案例消失了，并且fail从MonadFail.

然而，出于某种原因，Monad字典仍然是通过MonadFail字典获得的，即使现在可以避免。

我的猜测是这是 GHC 的当前限制。原则上它可以脱糖，生成Core，然后观察MonadFail不需要的。但是，我认为类型检查是在这些步骤发生之前执行的，那时 GHC 会为最坏的情况做准备，MonadFail以后可能仍然需要这种情况。我不知道应该添加多少工作以使其在类型检查期间更智能并避免要求，MonadFail除非确实需要。