should TcCanonical.rewriteEvidence preserve ctev_nosh?

[Nicolas Frisby]

Thank you for confirming, Simon.

I opened https://gitlab.haskell.org/ghc/ghc/issues/16735

On Sun, Jun 2, 2019 at 8:33 AM Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> Nick
>
>
>
> That looks outright wrong to me.  Would you like to make a ticket for it?
> It should be easy to fix.
>
>
>
> I’m surprised it has not caused more trouble before now.
>
>
>
> Well spotted and well diagnosed!
>
>
>
> Simon
>
>
>
> *From:* ghc-devs <ghc-devs-bounces at haskell.org> *On Behalf Of *Nicolas
> Frisby
> *Sent:* 01 June 2019 04:24
> *To:* ghc-devs at haskell.org
> *Subject:* should TcCanonical.rewriteEvidence preserve ctev_nosh?
>
>
>
> A bit of context and then my question.
>
>
>
>
> https://gitlab.haskell.org/ghc/ghc/blob/master/compiler/typecheck/TcCanonical.hs#L2226
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fblob%2Fmaster%2Fcompiler%2Ftypecheck%2FTcCanonical.hs%23L2226&data=02%7C01%7Csimonpj%40microsoft.com%7Cd90efcd1da6f4058c00c08d6e640c7c2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636949563239275987&sdata=F7dgkceI2512TafrGNP38xvWAv2%2F6HKQscRnU%2Bypbf8%3D&reserved=0>
> 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".
>
>
>
> However, the `CtWanted` case just immediately calls `newWanted`, which
> ignores the incoming `ctev_nosh` flag and always uses `WDeriv`.
>
>
> ```
> rewriteEvidence ev@(CtWanted { ctev_dest = dest
>
>                              , ctev_loc = loc }) new_pred co
>
> = do { mb_new_ev <- newWanted loc new_pred
> ```
>
>
>
> (This is true in 8.6.5 and also right now at
> 6febc444c0abea6c033174aa0e813c950b9b2877.)
>
>
>
> Thus I'm seeing a [W] is become a [WD], which seems to contradict the
> comment's "same flag" claim.
>
>
>
> MY QUESTION ======> Is this "WD unsplitting" the intended behavior? See
> canonicalization tc-trace below.
>
>
>
> 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.
>
>
>
> 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.
>
>
>
> Thanks! -Nick
>
>
>
> Here's a -ddump-tc-trace of a canonicalization that goes from [W] to [WD]
> happen (with GHC 8.6.5):
>
> runStage canonicalization {
>   workitem   =  [W] $dMonadFree_a35V {0}:: MonadFree
>                                              ((fs_a2UF[sk:1] :- Const
> e_a2UE[sk:1])
>                                               :+ Const e_a2UE[sk:1])
>                                              (Free fs_a2UF[sk:1])
> (CDictCan)
> flatten_args {
>   (fs_a2UF[sk:1] :- Const e_a2UE[sk:1]) :+ Const e_a2UE[sk:1]
>   Free fs_a2UF[sk:1]
> matchFamTcM
>   Matching: (fs_a2UF[sk:1] :- Const e_a2UE[sk:1])
>             :+ Const e_a2UE[sk:1]
>   Match failed
> matchFamTcM
>   Matching: fs_a2UF[sk:1] :- Const e_a2UE[sk:1]
>   Match failed
> Unfilled tyvar fs_a2UF[sk:1]
> Unfilled tyvar e_a2UE[sk:1]
> flatten/flat-cache hit
>   :- [* -> *, fs_a2UF[sk:1], Const e_a2UE[sk:1]]
>   s_a35Z[fmv:1]
> Unfilled tyvar s_a35Z[fmv:1]
> Unfilled tyvar e_a2UE[sk:1]
> matchFamTcM
>   Matching: s_a35Z[fmv:1] :+ Const e_a2UE[sk:1]
>   Match failed
> New coercion hole: co_a365
> Emitting new coercion hole
>   {co_a365} :: (s_a35Z[fmv:1] :+ Const e_a2UE[sk:1])
>                GHC.Prim.~# s_a364[fmv:1]
> extendFlatCache
>   :+ [* -> *, s_a35Z[fmv:1], Const e_a2UE[sk:1]]
>   [WD]
>   s_a364[fmv:1]
> flatten/flat-cache miss
>   :+ [* -> *, s_a35Z[fmv:1], Const e_a2UE[sk:1]]
>   s_a364[fmv:1]
>   [WD] hole{co_a365} {0}:: (s_a35Z[fmv:1] :+ Const e_a2UE[sk:1])
>                            GHC.Prim.~# s_a364[fmv:1]
> Unfilled tyvar fs_a2UF[sk:1]
> flatten }
>   s_a364[fmv:1]
>   Free fs_a2UF[sk:1]
> Emitting new wanted
>   $dMonadFree_a366 :: MonadFree s_a364[fmv:1] (Free fs_a2UF[sk:1])
>   arising from a use of ‘wrap’ at tests/ill-typed/T7.hs:77:14-17
> addTcEvBind
>   a2V1
>   [W] $dMonadFree_a35V
>     = $dMonadFree_a366
>       `cast` ((MonadFree
>                  (Sym {co_a365} ; ((:+)
>                                      <* -> *>_N (Sym {co_a360}) <Const
> e_a2UE[sk:1]>_N)_N)
>                  <Free fs_a2UF[sk:1]>_N)_R
>               :: MonadFree s_a364[fmv:1] (Free fs_a2UF[sk:1])
>                  ~R# MonadFree
>                        ((fs_a2UF[sk:1] :- Const e_a2UE[sk:1]) :+ Const
> e_a2UE[sk:1])
>                        (Free fs_a2UF[sk:1]))
> canClass
>   [W] $dMonadFree_a35V {0}:: MonadFree
>                                ((fs_a2UF[sk:1] :- Const e_a2UE[sk:1]) :+
> Const e_a2UE[sk:1])
>                                (Free fs_a2UF[sk:1])
>   MonadFree s_a364[fmv:1] (Free fs_a2UF[sk:1])
>   ContinueWith [WD] $dMonadFree_a366 {0}:: MonadFree
>                                              s_a364[fmv:1] (Free
> fs_a2UF[sk:1])
> end stage canonicalization }
>
>
>
>
>
>
>
> and later
>
>
>
>
>
>
>
>
>
> try_fundeps
>   [WD] $dMonadFree_a36h {0}:: MonadFree
>                                 s_a36f[fmv:1] (Free fs_a2UF[sk:1])
> (CDictCan)
> emitFunDepDeriveds 1
>   0
>   [fs_a2UF[sk:1] ~ s_a36f[fmv:1]]
>   False
> Emitting new derived equality
>   [D] _ {0}:: fs_a2UF[sk:1] GHC.Prim.~# s_a36f[fmv:1]
>
>
>
>
>
>
>
>
>
> and then my plugin discards that [D] as a tautological, and then the [W]
> gets unsplit and the [D] comes back around etc
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190602/0c55a850/attachment.html>