<div dir="ltr"><div>A bit of context and then my question.</div><div><br></div><a href="https://gitlab.haskell.org/ghc/ghc/blob/master/compiler/typecheck/TcCanonical.hs#L2226">https://gitlab.haskell.org/ghc/ghc/blob/master/compiler/typecheck/TcCanonical.hs#L2226</a> declares `rewriteEvidence` with the comment that "rewriteEvidence old_ev new_pred co  ... Returns a new_ev : new_pred, with same wanted/given/derived flag as old_ev".<div><br></div><div>However, the `CtWanted` case just immediately calls `newWanted`, which ignores the incoming `ctev_nosh` flag and always uses `WDeriv`.<div><br>```<br>rewriteEvidence ev@(CtWanted { ctev_dest = dest<br><br>                             , ctev_loc = loc }) new_pred co <br><br>= do { mb_new_ev <- newWanted loc new_pred<br>```<br><div><br></div><div>(This is true in 8.6.5 and also right now at 6febc444c0abea6c033174aa0e813c950b9b2877.)<br></div><br class="gmail-Apple-interchange-newline"></div><div>Thus I'm seeing a [W] is become a [WD], which seems to contradict the comment's "same flag" claim.</div><div> <br></div><div>MY QUESTION ======> Is this "WD unsplitting" the intended behavior? See canonicalization tc-trace below.</div><div><br></div><div>If it is intended, I'll probably write a follow-up question asking for more advice. The constraint solver is looping unproductively because my plugin keeps discarding the (re-)emitted [D] shadow as a tautology, then the [W] "unsplits" during canonicalization (even though my plugin didn't touch the [W]), this re-emits the same [D] (via a fundep), and so on.</div><div><br></div><div>My continual disclaimer recently is that I'm seeing this behavior with my in-development plugin activated, so it's entirely I'm pushing GHC into unfamiliar waters or even just plain violating some invariants without realizing it. But this trace looks rather isolated from plugins.</div><div><br></div><div>Thanks! -Nick</div><div><br></div><div>Here's a -ddump-tc-trace of a canonicalization that goes from [W] to [WD] happen (with GHC 8.6.5):<br><br>runStage canonicalization {<br>  workitem   =  [W] $dMonadFree_a35V {0}:: MonadFree<br>                                             ((fs_a2UF[sk:1] :- Const e_a2UE[sk:1])<br>                                              :+ Const e_a2UE[sk:1])<br>                                             (Free fs_a2UF[sk:1]) (CDictCan)<br>flatten_args {<br>  (fs_a2UF[sk:1] :- Const e_a2UE[sk:1]) :+ Const e_a2UE[sk:1]<br>  Free fs_a2UF[sk:1]<br>matchFamTcM<br>  Matching: (fs_a2UF[sk:1] :- Const e_a2UE[sk:1])<br>            :+ Const e_a2UE[sk:1]<br>  Match failed<br>matchFamTcM<br>  Matching: fs_a2UF[sk:1] :- Const e_a2UE[sk:1]<br>  Match failed<br>Unfilled tyvar fs_a2UF[sk:1]<br>Unfilled tyvar e_a2UE[sk:1]<br>flatten/flat-cache hit<br>  :- [* -> *, fs_a2UF[sk:1], Const e_a2UE[sk:1]]<br>  s_a35Z[fmv:1]<br>Unfilled tyvar s_a35Z[fmv:1]<br>Unfilled tyvar e_a2UE[sk:1]<br>matchFamTcM<br>  Matching: s_a35Z[fmv:1] :+ Const e_a2UE[sk:1]<br>  Match failed<br>New coercion hole: co_a365<br>Emitting new coercion hole<br>  {co_a365} :: (s_a35Z[fmv:1] :+ Const e_a2UE[sk:1])<br>               GHC.Prim.~# s_a364[fmv:1]<br>extendFlatCache<br>  :+ [* -> *, s_a35Z[fmv:1], Const e_a2UE[sk:1]]<br>  [WD]<br>  s_a364[fmv:1]<br>flatten/flat-cache miss<br>  :+ [* -> *, s_a35Z[fmv:1], Const e_a2UE[sk:1]]<br>  s_a364[fmv:1]<br>  [WD] hole{co_a365} {0}:: (s_a35Z[fmv:1] :+ Const e_a2UE[sk:1])<br>                           GHC.Prim.~# s_a364[fmv:1]<br>Unfilled tyvar fs_a2UF[sk:1]<br>flatten }<br>  s_a364[fmv:1]<br>  Free fs_a2UF[sk:1]<br>Emitting new wanted<br>  $dMonadFree_a366 :: MonadFree s_a364[fmv:1] (Free fs_a2UF[sk:1])<br>  arising from a use of ‘wrap’ at tests/ill-typed/T7.hs:77:14-17<br>addTcEvBind<br>  a2V1<br>  [W] $dMonadFree_a35V<br>    = $dMonadFree_a366<br>      `cast` ((MonadFree<br>                 (Sym {co_a365} ; ((:+)<br>                                     <* -> *>_N (Sym {co_a360}) <Const e_a2UE[sk:1]>_N)_N)<br>                 <Free fs_a2UF[sk:1]>_N)_R<br>              :: MonadFree s_a364[fmv:1] (Free fs_a2UF[sk:1])<br>                 ~R# MonadFree<br>                       ((fs_a2UF[sk:1] :- Const e_a2UE[sk:1]) :+ Const e_a2UE[sk:1])<br>                       (Free fs_a2UF[sk:1]))<br>canClass<br>  [W] $dMonadFree_a35V {0}:: MonadFree<br>                               ((fs_a2UF[sk:1] :- Const e_a2UE[sk:1]) :+ Const e_a2UE[sk:1])<br>                               (Free fs_a2UF[sk:1])<br>  MonadFree s_a364[fmv:1] (Free fs_a2UF[sk:1])<br>  ContinueWith [WD] $dMonadFree_a366 {0}:: MonadFree<br>                                             s_a364[fmv:1] (Free fs_a2UF[sk:1])<br>end stage canonicalization }<br></div></div><div><br></div><div><br></div><div><br></div><div>and later</div><div><br></div><div><br></div><div><br></div><div><br></div><div>try_fundeps<br>  [WD] $dMonadFree_a36h {0}:: MonadFree<br>                                s_a36f[fmv:1] (Free fs_a2UF[sk:1]) (CDictCan)<br>emitFunDepDeriveds 1<br>  0<br>  [fs_a2UF[sk:1] ~ s_a36f[fmv:1]]<br>  False<br>Emitting new derived equality<br>  [D] _ {0}:: fs_a2UF[sk:1] GHC.Prim.~# s_a36f[fmv:1]<br></div><div><br></div><div><br></div><div><br></div><div><br></div><div>and then my plugin discards that [D] as a tautological, and then the [W] gets unsplit and the [D] comes back around etc</div></div>