should TcCanonical.rewriteEvidence preserve ctev_nosh?

Nicolas Frisby nicolas.frisby at gmail.com
Wed Jun 5 03:02:21 UTC 2019


I commented in the affirmative on your MR, Simon. Should I also re-assign
it back to you?

https://gitlab.haskell.org/ghc/ghc/merge_requests/1094

On Sun, Jun 2, 2019 at 12:15 PM Nicolas Frisby <nicolas.frisby at gmail.com>
wrote:

> 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/20190604/d6b7c5d2/attachment.html>


More information about the ghc-devs mailing list