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) 

与核心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的源代码中获得灵感，再次阅读这个Tweag教程，带着大量的启发和大量的试验和错误，我找到了解决方案。我的方法的想法是正确的，只有使用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
]