ConCat plugin vs. unbound variable in inScope
Summary
I'm working on Conal Elliott's ConCat plugin here:
https://github.com/conal/concat
There's a thorny problem that arises from the construction of dictionaries,
which the plugin needs to do. Namely, dictionaries bound in one place
show up in the inScope parameter of the plugin rule outside the scope
of the dictionary binding.
Steps to reproduce
I've created a branch of ConCat here:
https://github.com/mikesperber/concat/tree/polymorphic-ghc-problem
stack build :ad-examples
produces output from a (messy, boiled-down) autoencoder example that shows
the problem as early as I can make it by -dcore-lint failing:
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
In the expression: $fFunctor:*:
@ (Vector Vector a_aJ5k) @ Par1 $dFunctor_aShp $fFunctorPar1
Out of scope: $dFunctor_aShp :: Functor (Vector Vector a_aJ5k)
[LclId]I've also attached full output:
Expected behavior
Some background: The plugin transforms core code by temporarily adding a rule defined by code,
and then calling the simplifier. The rule fires on calls to a function called toCcc', and may also generate more calls to toCcc' as subterms, where the plugin is supposed to be called again.
As part of its operation, the plugin generates code to make dictionaries. It uses the dictionaries already in scope by looking in the inScope argument to the rule.
I'm expecting the identifiers in inScope to also be bound in the generated code.
Actual behavior
The plugin generates this output (with some elisions). Note it constructs $dFunctor_aShp with goal type Functor (Vector Vector a_aJ5k).
fmapC
@ (GD (Dual (-+>)))
@ (Vector Vector a_aJ5k)
@ (Bump (Vector Vector a_aJ5k) R)
@ R
(let {
$dFunctor_aShp :: Functor (Vector Vector a_aJ5k)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=False, Value=False, ConLike=True,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dFunctor_aShp
= $fFunctorVector @ Vector @ a_aJ5k $fFunctorVector } in
let {
$dAdditive1_aShs :: Additive1 (Vector Vector a_aJ5k)
[LclId,
Arity=1,
Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 60}]
$dAdditive1_aShs = $fAdditive1Vector @ a_aJ5k $dKnownNat_aJ5v } in
$fFunctorCatGDh
@ (Dual (-+>))
@ (Vector Vector a_aJ5k)
($fIxProductCatDualh
@ (-+>)
@ (Vector Vector a_aJ5k)
($fIxCoproductPCat-+>h
@ (Vector Vector a_aJ5k)
($fSummableh
@ (Vector Vector a_aJ5k)
(($fRepresentableVector @ a_aJ5k $dKnownNat_aJ5v,
$fEqFinite @ a_aJ5k, $fZipVector @ a_aJ5k,
$fPointedVector @ a_aJ5k $dKnownNat_aJ5v,
$fFoldableVector @ Vector @ a_aJ5k $fFoldableVector)
`cast` (((%,,,,%)
<Representable (Vector Vector a_aJ5k)>_N
(Eq (Sym (D:R:RepVector[0] <a_aJ5k>_N)))_N
<Zip (Vector Vector a_aJ5k)>_N
<Pointed (Vector Vector a_aJ5k)>_N
<Foldable (Vector Vector a_aJ5k)>_N)_R
:: (Representable (Vector Vector a_aJ5k), Eq (Finite a_aJ5k),
Zip (Vector Vector a_aJ5k), Pointed (Vector Vector a_aJ5k),
Foldable (Vector Vector a_aJ5k))
~R# (Representable (Vector Vector a_aJ5k),
Eq (Rep (Vector Vector a_aJ5k)), Zip (Vector Vector a_aJ5k),
Pointed (Vector Vector a_aJ5k), Foldable (Vector Vector a_aJ5k)))))
$dAdditive1_aShs)
$dFunctor_aShp
$dAdditive1_aShs)
($fFunctorCatDualh
@ (Vector Vector a_aJ5k)
@ (-+>)
$dFunctor_aShp
($fZipCat-+>h
@ (Vector Vector a_aJ5k) ($fZipVector @ a_aJ5k) $dAdditive1_aShs)
$dAdditive1_aShs
($fFunctorCat-+>h
@ (Vector Vector a_aJ5k) $dFunctor_aShp $dAdditive1_aShs)))
(...
(toCcc'
@ (GD (Dual (-+>)))
@ (Bump (Vector Vector a_aJ5k) R)
@ R
(\ (ds1_aJmd :: Bump (Vector Vector a_aJ5k) R) ->
sumAC
@ (->)
@ (Bump (Vector Vector a_aJ5k))
@ R
(lvl_sNWG @ a_aJ5k)
(. @ (->)
@ (Bump (Vector Vector a_aJ5k) (R, R))
@ (Bump (Vector Vector a_aJ5k) R)
@ (Bump (Vector Vector a_aJ5k) R, Bump (Vector Vector a_aJ5k) R)
$fCategory->
((lvl_sNWH @ a_aJ5k)
`cast` (((%,,%)
(Sym (R:Ok->[0]) <(Bump (Vector Vector a_aJ5k) R,
Bump (Vector Vector a_aJ5k) R)>_N)
(Sym (R:Ok->[0]) <Bump (Vector Vector a_aJ5k) (R, R)>_N)
(Sym (R:Ok->[0]) <Bump (Vector Vector a_aJ5k) R>_N))_R
:: (Yes1
(Bump (Vector Vector a_aJ5k) R, Bump (Vector Vector a_aJ5k) R),
Yes1 (Bump (Vector Vector a_aJ5k) (R, R)),
Yes1 (Bump (Vector Vector a_aJ5k) R))
~R# (Ok
(->)
(Bump (Vector Vector a_aJ5k) R, Bump (Vector Vector a_aJ5k) R),
Ok (->) (Bump (Vector Vector a_aJ5k) (R, R)),
Ok (->) (Bump (Vector Vector a_aJ5k) R))))
(lvl_sNWP @ a_aJ5k)
(lvl_sNWV @ a_aJ5k)
(ds1_aJmd, a2_sNgO))))As part of processing the generated toCcc' call, the plugin will again need a dictionary with the same goal type. It checks inScope and finds $dFunctor_aShp there, so just generates a reference to it.
But note that the generated toCcc' call isn't in the scope of the binding for
$dFunctor_aShp, so we end up a free reference.
So, in summary, it appears that ghc is passing us stuff in inScope which it shouldn't.
PS: Many thanks to Richard Eisenberg for helping me get this far!
Environment
- GHC version used: 8.8.3