search

nfrisby / frags

Plugin gonna getcha, row types
0 stars 1 forks source link

better error message in `ill-typed/T7` #33

Open nfrisby opened 5 years ago

nfrisby commented 5 years ago

ill-typed/T7 arose from a simple mistake, but causes the solver to diverge. Fundeps seems involved. This ticket is just to improve the error message.

nfrisby commented 5 years ago

Here's a relevant snippet of the trace.

} simplifyW pluginResult
OUTPUT SOLVED
    ("fakeEvExpr Data.Frag.Plugin.Evidence.discardGivenPR"#,
     [D] _ {0}:: ((fs_a3jM[sk:1] :- Const e_a3jL[sk:1])
                  :+ Const e_a3jL[sk:1])
                 ~# fs_a3jM[sk:1] (CNonCanonical))
OUTPUT NEW [D] _ {0}:: 'Nil ~# 'Nil (CNonCanonical)
} simplifyW
FRAGPLUGIN
-----------
simplifyW {
simplifyW Unflat [a3ml :-> FragEQ
                             (Const e_a3jL[sk:1]) fs_a3jM[sk:1],
                  a3mq :-> FragLT (Const e_a3jL[sk:1]) fs_a3jM[sk:1]]
simplifyW gs [[G] $d~_a3mo {0}:: 'Nil ~ 'Nil (CDictCan),
              [G] $d~~_a3mp {0}:: 'Nil ~~ 'Nil (CDictCan),
              [G] $dKnownFragCard_a3jP {0}:: KnownFragCard
                                               fsk_a3mq[fsk:1] (CDictCan),
              [G] co_a3mn {1}:: fsk_a3ml[fsk:1] ~# 'Nil (CTyEqCan)]
simplifyW ds [[D] _ {0}:: ((fs_a3jM[sk:1] :- Const e_a3jL[sk:1])
                           :+ Const e_a3jL[sk:1])
                          ~# fs_a3jM[sk:1] (CNonCanonical)]
simplifyW ws [[W] $dMonadFree_a3vk {0}:: MonadFree
                                           ((fs_a3jM[sk:1] :- Const e_a3jL[sk:1])
                                            :+ Const e_a3jL[sk:1])
                                           (Free fs_a3jM[sk:1]) (CDictCan),
              [WD] $dKnownFragCard_a3vn {0}:: KnownFragCard
                                                (FragLT
                                                   (Const e_a3jL[sk:1])
                                                   (fs_a3jM[sk:1]
                                                    :- Const e_a3jL[sk:1])) (CDictCan),
              [WD] hole{co_a3vh} {51}:: FragEQ
                                          (Const e_a3jL[sk:1]) (fs_a3jM[sk:1] :- Const e_a3jL[sk:1])
                                        ~# 'Nil (CNonCanonical)]

Adding -ddump-tc-trace, I also see this repeated:

try_fundeps
  [WD] $dMonadFree_a35V {0}:: MonadFree
                                s_a35T[fmv:1] (Free fs_a2UF[sk:1]) (CDictCan)
emitFunDepDeriveds 1
  0
  [fs_a2UF[sk:1] ~ s_a35T[fmv:1]]
  False
Emitting new derived equality
  [D] _ {0}:: fs_a2UF[sk:1] GHC.Prim.~# s_a35T[fmv:1]

So I think we're looping because we're solving the fundep without updating the corresponding [W].

On the other hand, since we don't touch the [W] at all, it seems inappropriate for GHC to be emitting the [D] over and over. In fact, I see that TcCanonical.rewriteEvidence is turning that [W] backed into a [WD], which seems wrong. I emailed ghc-devs, I'll put the link here once it's on the archives.

Edit: SPJ confirmed this is unexpected: https://mail.haskell.org/pipermail/ghc-devs/2019-June/017743.html

nfrisby commented 5 years ago

This is the canonicalization step that seems somewhat dubious to me.

runStage canonicalization {
  workitem   =  [W] $dMonadFree_a366 {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_a36a[fmv:1]
Unfilled tyvar s_a36a[fmv:1]
Unfilled tyvar e_a2UE[sk:1]
matchFamTcM
  Matching: s_a36a[fmv:1] :+ Const e_a2UE[sk:1]
  Match failed
New coercion hole: co_a36g
Emitting new coercion hole
  {co_a36g} :: (s_a36a[fmv:1] :+ Const e_a2UE[sk:1])
               GHC.Prim.~# s_a36f[fmv:1]
extendFlatCache
  :+ [* -> *, s_a36a[fmv:1], Const e_a2UE[sk:1]]
  [WD]
  s_a36f[fmv:1]
flatten/flat-cache miss
  :+ [* -> *, s_a36a[fmv:1], Const e_a2UE[sk:1]]
  s_a36f[fmv:1]
  [WD] hole{co_a36g} {0}:: (s_a36a[fmv:1] :+ Const e_a2UE[sk:1])
                           GHC.Prim.~# s_a36f[fmv:1]
Unfilled tyvar fs_a2UF[sk:1]
flatten }
  s_a36f[fmv:1]
  Free fs_a2UF[sk:1]
Emitting new wanted
  $dMonadFree_a36h :: MonadFree s_a36f[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_a366
    = $dMonadFree_a36h
      `cast` ((MonadFree
                 (Sym {co_a36g} ; ((:+)
                                     <* -> *>_N (Sym {co_a36b}) <Const e_a2UE[sk:1]>_N)_N)
                 <Free fs_a2UF[sk:1]>_N)_R
              :: MonadFree s_a36f[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_a366 {0}:: MonadFree
                               ((fs_a2UF[sk:1] :- Const e_a2UE[sk:1]) :+ Const e_a2UE[sk:1])
                               (Free fs_a2UF[sk:1])
  MonadFree s_a36f[fmv:1] (Free fs_a2UF[sk:1])
  ContinueWith [WD] $dMonadFree_a36h {0}:: MonadFree
                                             s_a36f[fmv:1] (Free fs_a2UF[sk:1])
end stage canonicalization }
nfrisby commented 5 years ago

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

nfrisby commented 5 years ago

This ticket is in a sense blocked on https://gitlab.haskell.org/ghc/ghc/issues/16735, but it seems likely that #31 might address this specific repro.