GHC TcPlugin: replace constraints with simplified ones-CodePudding

I'm trying to write a type checking plugin for GHC, which simplifies type family applications in constraints. From my tcPluginTrace, everything looks good, but then, Core Lint and compilation fails. Probably something with coercions but it's hard for me to understand the error messages as a newbie and there are very few tutorials on the topic. Could someone please help me and tell me what's wrong with my approach? using ghc-tcplugin-extra 0.4.2 and 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)

With Core Lint off, I get the following error:

  (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

The Core Lint reports (For what it's worth - there are many internal details of my plugin)

    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: []]

CodePudding user response：

Taking inspiration from ghc-tcplugin-api's source code, reading this Tweag tutorial again, with a blaze of enlightment and a lot of trial and error, I've found the solution. The idea of my approach was correct, only the coercion generated using evByFiat was not the right one. I had to use evCast coercion (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
        ]