GHC TcPlugin：用简化的约束替换约束

Question

我正在尝试为 GHC 编写一个类型检查插件，它可以简化约束中的类型族应用程序。从我的 tcPluginTrace 来看，一切看起来都不错，但是随后，Core Lint 和编译失败了。可能是带有强制的东西，但作为新手我很难理解错误消息，而且关于这个主题的教程很少。有人可以帮助我并告诉我我的方法有什么问题吗？使用 ghc-tcplugin-extra 0.4.2 和 ghc 9.2.1

  ...
  -- reduceCt tries to simplify a constraint and returns Nothing if no rewriting has been done
  wanteds' <- mapM (reduceCt :: Ct -> TcPluginM (Maybe PredType)) (wanteds :: [Ct])

  -- create rewritings
  newWanteds <- for (zip wanteds' wanteds) \case
    (Nothing, _) -> return Nothing
    (Just pred, ct) -> Just . mkNonCanonical <$> GHC.TcPluginM.Extra.newWanted (ctLoc ct) pred

  -- if a rewriting exists for a constraint ct, add it to the removed list
  -- with an evidence that says:
  -- "The constraint ct has been rewritten to ct' by myplugin."
  let removedWanteds =
        [ (evByFiat "myplugin" (ctPred ct) (ctPred ct'), ct)
        | (Just ct', ct) <- zip newWanteds wanteds
        ]
    
  -- the outputs look legit
  tcPluginTrace "---Plugin removedWanteds---" $ ppr removedWanteds
  tcPluginTrace "---Plugin newWanteds---" $ ppr $ catMaybes newWanteds
  return $ TcPluginOk removedWanteds (catMaybes newWanteds)

关闭 Core Lint 后，出现以下错误：

  (GHC version 9.2.1:
        refineFromInScope
  InScope {wild_00 main x_a3qj x_a3yf $cmonadfn_a4vo $dShow_a4C2
           $cmonadfn_a4Co $dShow_a4DN s_a55C hardFunction main $fMonadFnKIO
           $fMonadFnKIO0 $tcEven $trModule $tcOdd $cmonadfn_s53E
           $cmonadfn_s55b $trModule_s55c $trModule_s55d $trModule_s55e
           $trModule_s55f $tcEven_s55g $tcEven_s55h $tcOdd_s55i $tcOdd_s55j}
  $dMonadFn_a4uR
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
        pprPanic, called at compiler/GHC/Core/Opt/Simplify/Env.hs:706:30 in ghc:GHC.Core.Opt.Simplify.Env

Core Lint 报告（就其价值而言 - 我的插件有很多内部细节）

    Argument value doesn't match argument type:
    Fun type:
        (GetK
           "k02"
           ('Name "k03" (GetK "k01" ('Name "k01" ('K 'Zero Even) ':+: 'End))
            ':+: ('Name
                    "k02" (GetK "k01" ('Name "k01" ('K 'Zero Even) ':+: 'End))
                  ':+: 'End))
         ~# 'K 'Zero Even)
        -> GetK
             "k02"
             ('Name "k03" (GetK "k01" ('Name "k01" ('K 'Zero Even) ':+: 'End))
              ':+: ('Name
                      "k02" (GetK "k01" ('Name "k01" ('K 'Zero Even) ':+: 'End))
                    ':+: 'End))
           ~ 'K 'Zero Even
    Arg type:
        (GetK
           "k02"
           ('Name "k03" (GetK "k01" ('Name "k01" ('K 'Zero Even) ':+: 'End))
            ':+: ('Name
                    "k02" (GetK "k01" ('Name "k01" ('K 'Zero Even) ':+: 'End))
                  ':+: 'End))
         ~# 'K 'Zero Even)
        ~# ('K 'Zero Even ~# 'K 'Zero Even)
    Arg:
        CO: Univ(nominal plugin "typedict"
                 :: GetK
                      "k02"
                      ('Name "k03" (GetK "k01" ('Name "k01" ('K 'Zero Even) ':+: 'End))
                       ':+: ('Name
                               "k02" (GetK "k01" ('Name "k01" ('K 'Zero Even) ':+: 'End))
                             ':+: 'End))
                    ~# 'K 'Zero Even, 'K 'Zero Even ~# 'K 'Zero Even)
    In the RHS of $d~_a4w0 :: GetK
                                "k02"
                                ('Name "k03" (GetK "k01" ('Name "k01" ('K 'Zero Even) ':+: 'End))
                                 ':+: ('Name
                                         "k02" (GetK "k01" ('Name "k01" ('K 'Zero Even) ':+: 'End))
                                       ':+: 'End))
                              ~ 'K 'Zero Even
    Substitution: [TCvSubst
                     In scope: InScope {}
                     Type env: []
                     Co env: []]

Answer 1

从 ghc-tcplugin-api 的 source code, reading this Tweag tutorial again 中汲取灵感，经过大量的启发和大量的反复试验，我找到了解决方案。我的想法是正确的，只是使用 evByFiat 生成的强制转换不正确。我不得不使用 evCast 强制 (ct' |> Univ R "myplugin" ct' ct) :: ct:

  let removedWanteds =
        [ ( evCast (ctEvExpr $ ctEvidence ct') $
            mkUnivCo (PluginProv "myplugin") Representational (ctPred ct') (ctPred ct)
          , ct
          )
        | (Just ct', ct) <- zip newWanteds wanteds
        ]

GHC TcPlugin：用简化的约束替换约束

GHC TcPlugin: replace constraints with simplified ones

plugins

haskell

typechecking

ghc