search

compiling-to-categories / concat

Compiling to Categories
http://conal.net/papers/compiling-to-categories
BSD 3-Clause "New" or "Revised" License
436 stars 50 forks source link

Avoid `runTcInteractive` in BuildDictionary #82

Open zliu41 opened 2 years ago

zliu41 commented 2 years ago

Instead of runTcInteractive, it now runs the TcM via initTcDsForSolver, followed by initDsWithModGuts.

This makes BuildDictionary work better with orphan instances. When using runTcInteractive we need to obtain the ModuleNames of the orphan Modules, add them to ic_imports, and they are then loaded back into Modules. This not only wastes work, but we must filter out the hidden modules since hidden modules can't be loaded. This means BuildDictionary can't find orphans in hidden modules.

In the new approach we can simply add the orphan Modules to the TcGblEnv. No need to re-load them.

I tested it in my work repository and it works as expected.

The use of initTcDsForSolver was suggested by Matthew Pickering in https://gitlab.haskell.org/ghc/ghc/-/issues/20499.

Fixes #81.

conal commented 2 years ago

Sounds great! Thanks for the contribution, @zliu41!

@mikesperber Since you folks are the primary users of concat other than KittyHawk I'm aware of (and since I'm currently not using it), would you please check out this PR to see how affects your use?

mikesperber commented 2 years ago

@mikesperber Since you folks are the primary users of concat other than KittyHawk I'm aware of (and since I'm currently not using it), would you please check out this PR to see how affects your use?

Unfortunately, it fails to solve some constraints it was able to solve pre-patch. We're investigatung. (Relevant, as we were also having problems pre-patch where the plugin was not seeing certain class instances.)

zliu41 commented 2 years ago

Thanks @mikesperber. I'd be curious what the error message is, and if it points to a missing instance, whether the module that defines it is included in dep_orphs (mg_deps guts).

mikesperber commented 2 years ago

@zliu41 It looks like it can't infer KnownNat constraints usually handled by GHC.TypeLits.KnownNat.Solver or GHC.TypeLits.Normalise anymore. Does that ring any bells?

mikesperber commented 2 years ago

Here's trace output that shows the problem:

    MatrixMapCat
    (GD (Dual (-+>))) (Vector m_abqT :.: Vector (n_abqS + 1))
    buildDictionary in-scope evidence
      ($dKnownNat_abqV, $dKnownNat_abqW, $dZip_sczL, $dMatrixMap_sczJ,
       lvl_scEI)
    buildDictionary': givens
      [[G] evidence_sdxl {0}:: KnownNat n_abqS (CNonCanonical),
       [G] evidence_sdxm {0}:: KnownNat m_abqT (CNonCanonical),
       [G] evidence_sdxn {0}:: Zip
                 (Vector Vector (n_abqS + 1)) (CNonCanonical),
       [G] evidence_sdxo {0}:: MatrixMap
                 (Vector m_abqT :.: Vector (n_abqS + 1)) (CNonCanonical),
       [G] evidence_sdxp {0}:: MatrixMapCat
                 (->) (Vector m_abqT :.: Vector (n_abqS + 1)) (CNonCanonical)]
    buildDictionary' back from solveWanteds
      WC {wc_simple =
        [WD] $dKnownNat_adBk {5}:: KnownNat fsk_adxV[fsk:0] (CDictCan)}
    buildDictionary' back from runTcS
      {[G] $dFunctor_adxU
     = $p1Zip @ (Vector Vector (n_abqS + 1)) evidence_sdxn,
       [G] co_adxW = CO: <n_abqS + 1>_N,
       [G] $dFunctor_adxX
     = $dFunctor_adxU
       `cast` (Sub (Sym (Functor (Vector <Vector>_N (Sym co_adxW))_N)_N)
           :: Functor (Vector Vector (n_abqS + 1))
              ~R# Functor (Vector Vector fsk_adxV[fsk:0])),
zliu41 commented 2 years ago

Nope, doesn't ring any bells. I'm happy to do some more investigation but it's not clear to me how to reproduce this. It sounds like you are using both the concat plugin, and the knownnat plugin, and with this change, somehow the knownnat plugin stopped working, and then concat tried to solve that constraint, but couldn't, either?

mikesperber commented 2 years ago

@zliu41 No: ConCat is trying to solve a KnownNat constraint, which it previously could solve using the GHC.TypeLits.KnownNat.Solver or GHC.TypeLits.Normalise plugin. With the patch, it can't anymore.

zliu41 commented 2 years ago

@mikesperber Ok thanks. I think we are basically saying the same thing. Seems like for some reason the knownnat plugin isn't properly triggered with this patch. I'll see if I can reproduce this.

zliu41 commented 2 years ago

I think the problem is that runTcInteractive invokes typechecker and hole-fit plugins, while the new approach doesn't:

runTcInteractive hsc_env thing_inside
  = initTcInteractive hsc_env $ withTcPlugins hsc_env $
    withDefaultingPlugins hsc_env $ withHoleFitPlugins hsc_env $

It would be a one-line fix if withTcPlugins and withHoleFitPlugins were exported, but they are not. But they are fairly small functions and it should be easy enough to make a copy.

zliu41 commented 2 years ago

@mikesperber Would you give 68c4901 a try, and see if it solves the problem? I think it should.

mikesperber commented 2 years ago

@mikesperber Would you give 68c4901 a try, and see if it solves the problem? I think it should.

Unfortunately, now I'm getting problems resolving CoerceCat constraints:

buildDictionary
  CoerceCat
(GD (Dual (-+>)))
((:.:) (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
(Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
buildDictionary in-scope evidence
  ($dKnownNat_acO8, $dKnownNat_acO9, $dOkType_acOa, $dAdditive_acOb,
   $dFloating_acOc, $dOrd_acOd, lvl_sdjg, $dNum_sdhk, $dNum_sdhj,
   $dZip_sdhm, lvl_sdBu, lvl_sdBv)
buildDictionary': givens
  [[G] evidence_sdGk {0}:: KnownNat n_acO4 (CNonCanonical),
   [G] evidence_sdGl {0}:: KnownNat m_acO5 (CNonCanonical),
   [G] evidence_sdGm {0}:: OkType numType_acO6 (CNonCanonical),
   [G] evidence_sdGn {0}:: Additive numType_acO6 (CNonCanonical),
   [G] evidence_sdGo {0}:: Floating numType_acO6 (CNonCanonical),
   [G] evidence_sdGp {0}:: Ord numType_acO6 (CNonCanonical),
   [G] evidence_sdGq {0}:: AddCat
             (->) (Vector Vector n_acO4) numType_acO6 (CNonCanonical),
   [G] evidence_sdGr {0}:: Fractional numType_acO6 (CNonCanonical),
   [G] evidence_sdGs {0}:: Num numType_acO6 (CNonCanonical),
   [G] evidence_sdGt {0}:: Zip (Vector Vector n_acO4) (CNonCanonical),
   [G] evidence_sdGu {0}:: ZipCat
             (->) (Vector Vector n_acO4) (CNonCanonical),
   [G] evidence_sdGv {0}:: ZipCat
             (->) (Vector Vector n_acO4) (CNonCanonical)]
buildDictionary' back from solveWanteds
  WC {wc_simple =
    [WD] hole{co_ahjy} {3}:: (:.:)
                   (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6
                 ~R# Vector
                   Vector
                   n_acO4
                   (Bump (Vector Vector n_acO4) numType_acO6) (CIrredCan(sol))}
buildDictionary' back from runTcS
  {[G] $dFractional_ahjc = $p1Floating @ numType_acO6 evidence_sdGo,
   [G] $dNum_ahjd = $p1Fractional @ numType_acO6 $dFractional_ahjc,
   [G] $dEq_ahje = $p1Ord @ numType_acO6 evidence_sdGp,
   [G] irred_ahjf
 = $p1AddCat
     @ (->) @ (Vector Vector n_acO4) @ numType_acO6 evidence_sdGq,
   [G] $dAdditive_ahjg
 = $p2AddCat
     @ (->) @ (Vector Vector n_acO4) @ numType_acO6 evidence_sdGq,
   [G] $dYes1_ahjh
 = irred_ahjf
   `cast` (Sub (Sym (Sym (R:Ok->[0]) <numType_acO6>_N))
       :: Ok (->) numType_acO6 ~R# Yes1 numType_acO6),
   [G] $dNum_ahji = $p1Fractional @ numType_acO6 evidence_sdGr,
   [G] $dFunctor_ahjj = $p1Zip @ (Vector Vector n_acO4) evidence_sdGt,
   [G] $dZip_ahjk
 = $p1ZipCat @ (->) @ (Vector Vector n_acO4) evidence_sdGu,
   [G] $dFunctor_ahjl = $p1Zip @ (Vector Vector n_acO4) $dZip_ahjk,
   [G] $dOkFunctor_ahjm
 = $p2ZipCat @ (->) @ (Vector Vector n_acO4) evidence_sdGu,
   [G] $dZip_ahjn
 = $p1ZipCat @ (->) @ (Vector Vector n_acO4) evidence_sdGv,
   [G] $dFunctor_ahjo = $p1Zip @ (Vector Vector n_acO4) $dZip_ahjn,
   [G] $dOkFunctor_ahjp
 = $p2ZipCat @ (->) @ (Vector Vector n_acO4) evidence_sdGv,
   [W] $dCoerceCat_ahja
 = $fCoerceCatTYPETYPEGDab
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @ (Dual (-+>))
     $dCoerceCat_ahjt
     $dCoerceCat_ahju,
   [W] $dCoerceCat_ahjt
 = $fCoerceCatTYPETYPE->ab
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     $dCoercible_ahjx,
   [W] $dCoercible_ahjx
 = MkCoercible
     @ *
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @~ ({co_ahjy}
     :: (:.:) (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6
        ~R# Vector
          Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6)),
   [W] $dCoerceCat_ahju
 = $fCoerceCatTYPETYPEDualab
     @ (-+>)
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     $dCoerceCat_ahjC,
   [W] $dCoerceCat_ahjC
 = $fCoerceCatTYPETYPE-+>ab
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     $dCoerceCat_ahjF,
   [W] $dCoerceCat_ahjF
 = $fCoerceCatTYPETYPE->ab
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     $dCoercible_ahjG,
   [W] $dCoercible_ahjG
 = MkCoercible
     @ *
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     @~ ({co_ahjH}
     :: Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6)
        ~R# (:.:)
          (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)}
buildDictionary' zonked
  {[G] $dFractional_ahjc = $p1Floating @ numType_acO6 evidence_sdGo,
   [G] $dNum_ahjd = $p1Fractional @ numType_acO6 $dFractional_ahjc,
   [G] $dEq_ahje = $p1Ord @ numType_acO6 evidence_sdGp,
   [G] irred_ahjf
 = $p1AddCat
     @ (->) @ (Vector Vector n_acO4) @ numType_acO6 evidence_sdGq,
   [G] $dAdditive_ahjg
 = $p2AddCat
     @ (->) @ (Vector Vector n_acO4) @ numType_acO6 evidence_sdGq,
   [G] $dYes1_ahjh
 = irred_ahjf
   `cast` (Sub (Sym (Sym (R:Ok->[0]) <numType_acO6>_N))
       :: Ok (->) numType_acO6 ~R# Yes1 numType_acO6),
   [G] $dNum_ahji = $p1Fractional @ numType_acO6 evidence_sdGr,
   [G] $dFunctor_ahjj = $p1Zip @ (Vector Vector n_acO4) evidence_sdGt,
   [G] $dZip_ahjk
 = $p1ZipCat @ (->) @ (Vector Vector n_acO4) evidence_sdGu,
   [G] $dFunctor_ahjl = $p1Zip @ (Vector Vector n_acO4) $dZip_ahjk,
   [G] $dOkFunctor_ahjm
 = $p2ZipCat @ (->) @ (Vector Vector n_acO4) evidence_sdGu,
   [G] $dZip_ahjn
 = $p1ZipCat @ (->) @ (Vector Vector n_acO4) evidence_sdGv,
   [G] $dFunctor_ahjo = $p1Zip @ (Vector Vector n_acO4) $dZip_ahjn,
   [G] $dOkFunctor_ahjp
 = $p2ZipCat @ (->) @ (Vector Vector n_acO4) evidence_sdGv,
   [W] $dCoerceCat_ahja
 = $fCoerceCatTYPETYPEGDab
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @ (Dual (-+>))
     $dCoerceCat_ahjt
     $dCoerceCat_ahju,
   [W] $dCoerceCat_ahjt
 = $fCoerceCatTYPETYPE->ab
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     $dCoercible_ahjx,
   [W] $dCoercible_ahjx
 = MkCoercible
     @ *
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @~ (co_ahjy
     :: (:.:) (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6
        ~R# Vector
          Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6)),
   [W] $dCoerceCat_ahju
 = $fCoerceCatTYPETYPEDualab
     @ (-+>)
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     $dCoerceCat_ahjC,
   [W] $dCoerceCat_ahjC
 = $fCoerceCatTYPETYPE-+>ab
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     $dCoerceCat_ahjF,
   [W] $dCoerceCat_ahjF
 = $fCoerceCatTYPETYPE->ab
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     $dCoercible_ahjG,
   [W] $dCoercible_ahjG
 = MkCoercible
     @ *
     @ (Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6))
     @ ((:.:)
      (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
     @~ (Sym co_ahjy
     :: Vector Vector n_acO4 (Bump (Vector Vector n_acO4) numType_acO6)
        ~R# (:.:)
          (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)}
Couldn't build dictionary for
  coerceC
@ (GD (Dual (-+>)))
@ ((:.:)
     (Vector n_acO4) (Bump (Vector Vector n_acO4)) numType_acO6)
@ (Vector
     n_acO4 (Bump (Vector Vector n_acO4) numType_acO6)) :: CoerceCat
                                 (GD (Dual (-+>)))
                                 ((:.:)
                                (Vector n_acO4)
                                (Bump (Vector Vector n_acO4))
                                numType_acO6)
                                 (Vector
                                n_acO4
                                (Bump
                                   (Vector Vector n_acO4)
                                   numType_acO6)) =>
                               GD
                                 (Dual (-+>))
                                 ((:.:)
                                (Vector n_acO4)
                                (Bump (Vector Vector n_acO4))
                                numType_acO6)
                                 (Vector
                                n_acO4
                                (Bump
                                   (Vector Vector n_acO4)
                                   numType_acO6)):
  unsolved constraints

(What a rabbit hole ...)

zliu41 commented 2 years ago

Thanks @mikesperber . We also use CoerceCat, but use unsafeCoerce to avoid needing Coercible (which requires importing an unbounded number of data constructors). That's probably why we don't run into this error. Anyway, converting the PR to draft

sellout commented 2 years ago

@mikesperber Here's our reason for the unsafeCoerce workaround: https://github.com/conal/concat/issues/34#issuecomment-682319522. I think @conal is right that the ultimate fix is in GHC, but converting coerce to unsafeCoerce in the plugin has been a massive usability help for our code base.

zliu41 commented 2 years ago

So I haven't been able to reproduce this exact error:

So I'm not sure what can lead to the "unsolved constraints"

mikesperber commented 2 years ago

Funny that I've just encountered RepCat along a different path.

This commit turns a few datas into newtypes:

https://github.com/conal/concat/commit/9fc25319c9fcd44f48d1942bea58dfd990083706

... but now the plugin takes a different path when applying the plugin again to the output of AD.

I'm sure I have only a very superficial understanding of the issues, but I did this:

     Trying("top newtype selector cast")
     e@(Cast e' _) 
       | Just repr <- mkReprC'_maybe funCat (exprType e')
       -> Doing("newtype selector cast")
          return (mkCcc (repr `App` e'))
     Trying("top newtype constructor cast")
     e@(Cast e' _) 
       | Just abst <- mkAbstC'_maybe funCat (exprType e)
       -> Doing("newtype constructor cast")
          return (mkCcc (abst `App` e'))

... turning core Cast into a RepCat call.

It's simplistic - I got a headache actually trying to examine the coercion expression. But I also can't immediately see why it's wrong.

mikesperber commented 2 years ago

@mikesperber Here's our reason for the unsafeCoerce workaround: [...]

So with that in place, our code runs.

mikesperber commented 2 years ago 
* The problem when our `CoerceCat` required `Coercible` is that the relevant data constructors are not in scope, but it is not the problem here

@sellout helped me understand the issues a bit better, so maybe we can make progress. @zliu41: How do you know this is not the problem here?

zliu41 commented 2 years ago

How do you know this is not the problem here?

If the problem is data constructor not being in scope for coerce, I believe it should fail at line 108, with "data constructor not in scope" as the error message, rather than at line 186.

mikesperber commented 2 years ago

If the problem is data constructor not being in scope for coerce, I believe it should fail at line 108, with "data constructor not in scope" as the error message, rather than at line 186.

Huh. Strange that the trace doesn't mention Coercible directly, but instead :.:.