Avoid `runTcInteractive` in BuildDictionary by zliu41 · Pull Request #82 · compiling-to-categories/concat

zliu41 · 2021-10-17T02:34:44Z

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 · 2021-10-19T15:03:21Z

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 · 2021-10-20T12:11:33Z

@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 · 2021-10-20T16:09:13Z

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 · 2021-10-25T12:35:26Z

@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 · 2021-10-25T12:39:14Z

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 · 2021-10-28T04:39:38Z

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 · 2021-10-28T07:13:16Z

@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 · 2021-10-28T18:01:27Z

@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 · 2021-11-05T02:32:01Z

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 · 2021-11-05T05:01:28Z

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

mikesperber · 2021-11-15T15:05:04Z

@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 · 2021-11-17T16:48:20Z

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 · 2022-01-05T05:29:41Z

@mikesperber Here's our reason for the unsafeCoerce workaround: #34 (comment). 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 · 2022-01-05T06:56:54Z

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

The problem when our CoerceCat required Coercible is that the relevant data constructors are not in scope, but it is not the problem here
If I attempt to build Coercible a b where a and b don't have the same representation, it would still be a slightly different error

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

mikesperber · 2022-01-07T10:36:25Z

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

This commit turns a few datas into newtypes:

9fc2531

... 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 · 2022-01-07T15:34:03Z

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

So with that in place, our code runs.

mikesperber · 2022-02-08T12:37:41Z

* 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 · 2022-02-08T15:47:17Z

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 · 2022-02-08T16:49:44Z

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 :.:.

Avoid runTcInteractive in BuildDictionary

13a13b3

Run typechecker and hole fit plugins

68c4901

zliu41 marked this pull request as draft November 17, 2021 16:48

Conversation

zliu41 commented Oct 17, 2021

Uh oh!

conal commented Oct 19, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mikesperber commented Oct 20, 2021

Uh oh!

zliu41 commented Oct 20, 2021

Uh oh!

mikesperber commented Oct 25, 2021

Uh oh!

mikesperber commented Oct 25, 2021

Uh oh!

zliu41 commented Oct 28, 2021

Uh oh!

mikesperber commented Oct 28, 2021

Uh oh!

zliu41 commented Oct 28, 2021

Uh oh!

zliu41 commented Nov 5, 2021

Uh oh!

zliu41 commented Nov 5, 2021

Uh oh!

mikesperber commented Nov 15, 2021

Uh oh!

zliu41 commented Nov 17, 2021

Uh oh!

sellout commented Jan 5, 2022

Uh oh!

zliu41 commented Jan 5, 2022

Uh oh!

mikesperber commented Jan 7, 2022

Uh oh!

mikesperber commented Jan 7, 2022

Uh oh!

mikesperber commented Feb 8, 2022

Uh oh!

zliu41 commented Feb 8, 2022

Uh oh!

mikesperber commented Feb 8, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

conal commented Oct 19, 2021 •

edited

Loading