Alexis
Thanks for writing this up so carefully. I hope that others will join in.
And please then put the distilled thought onto the wiki page(s) so they are not
lost.
Some quick thoughts from me:
* Flattening. I’m pretty sure we pass constraints unflattened because
that’s what someone wanted at the time. It could easily be changed, but it
might complicate the API. E.g. you might reasonably want to know the mapping
from type variable to function application. There is no fundameental obstacle.
* Letting the plugin add given constraints. This looks a bit like: let the
plugin prove lemmas and hand them back to GHC (along with their proof) to
exploit. Yes, that seems reasonable too. Again, something new in the API.
I don’t understand enough of your type-class instance question to comment
meaningfully, but perhaps others will.
Nothing about the plugin interface is cast in stone. There are quite a few
“customers” but few enough that they’ll probably be happy to adapt to changes.
Go for it, in consultation with them!
Simon
From: ghc-devs <ghc-devs-boun...@haskell.org> On Behalf Of Alexis King
Sent: 01 August 2019 07:55
To: ghc-devs@haskell.org
Subject: Properly writing typechecker plugins
Hi all,
I have recently decided to try writing a GHC typechecker plugin so I can get my
hands on some extra operations on type-level strings. My plugin works, but only
sort of—I know some things about it are plain wrong, and I have a sneaking
suspicion that plenty of other things are not handled properly.
First, some context about what I do and don’t already know: I have a high-level
understanding of the basic concepts behind GHC’s solver. I understand what
evidence is and what purpose it serves, I mostly understand the different
flavors of constraints, and I think I have a decent grasp on some of the
operational details of how individual passes work. I’ve spent a little time
reading through comments in the GHC source code, along with pieces of the
source code itself, but I’m sure my understanding is pretty patchy.
With that out of the way, here are my questions:
1. First, I’m trying to understand: why are wanted constraints passed to
typechecker plugins unflattened? This is my single biggest point of confusion.
It certainly seems like the opposite of what I want. Consider that I have a
type family
type family ToUpper (s :: Symbol) :: Symbol where {}
that I wish to solve in my plugin. At first, I just naïvely looked through the
bag of wanted constraints and looked for constraints of the shape
t ~ ToUpper s
but this isn’t good enough, since my plugin regularly receives constraints that
look more like
t ~ SomeOtherTypeFamily (ToUpper s)
so I have to recursively grovel through every type equality constraint looking
for an application of a family I care about. Furthermore, once I’ve found one,
I’m not sure how to actually let GHC know that I’ve solved it—do I really have
to just generate a new given constraint and let GHC’s solver connect the dots?
I have seen the note on the typechecker plugins wiki
page<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fwikis%2Fplugins%2Ftype-checker%23under-discussion-defining-type-families&data=02%7C01%7Csimonpj%40microsoft.com%7C66b089f679154ccfd8a108d7164d2ce1%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637002393033597031&sdata=dr9ERzE28ev%2B3R0EbajMqM166YVI5dFm2J2Jd2D2mYo%3D&reserved=0>
about possibly baking support for type families into the plugin interface,
which would indeed be nicer than the status quo, but it seems odd to me that
they aren’t just passed to plugins flattened, which seems like it would spare a
lot of effort. Isn’t the flattened representation really what typechecker
plugins would like to see, anyway?
2. But let’s put families aside for a moment. I’m not just solving type
families in my plugin, I’m also solving classes. These classes have no methods,
but they do have functional dependencies. For example, I have a class
class Append (a :: Symbol) (b :: Symbol) (c :: Symbol) | a b -> c, a c ->
b, b c -> a
which is like GHC.TypeLits.AppendSymbol, but the fundeps make GHC a bit happier
when running it “backwards” (since GHC doesn’t really know about AppendSymbol’s
magical injectivity, so it sometimes complains).
In any case, I was hoping that GHC’s solver would handle the improvement
afforded by the fundeps for me once I provided evidence for Append constraints,
but that doesn’t seem to be the case. Currently, I am therefore manually
generating derived constraints based on the functional dependency information,
plumbing FunDepOrigin2 through and all. Is there some way to cooperate better
with GHC’s solver so I don’t have to duplicate all that logic in my plugin?
I guess one thing I didn’t try is returning given constraints from my solver
instead of just solving them and providing evidence. That is, if my plugin
received a
[W] d1 :: Append "foo" "bar" c
constraint, then instead of solving the constraint directly, I could leave it
alone and instead return a new constraint
[G] d2 :: Append "foo" "bar" "baz"
and presumably GHC’s solver would use that constraint to improve and solve d1.
But similar to my confusion about type families above, I’m uncertain if that’s
the intended method or not, since it seems like it’s sort of circumventing the
plugin API.
3. Finally, on a related note, building evidence for these solver-generated
typeclass instances is a bit of a pain. They have no methods, but they do
sometimes have superclasses. Currently, I’ve been generating CoreExprs as
carefully as I’m able to after reading through the desugaring code: I call
dataConWrapId on the result of classDataCon, then use mkTyConApp and mkCoreApps
on that directly. It seems to work okay now, but it didn’t always: -dcore-lint
thankfully caught my mistakes, but I’ve been wondering if there’s a safer way
to build the dictionary that I’ve been missing.
That’s it for now—I’ve just been muddling through until things work. Once I get
something that feels closer to right, maybe I’ll put the code somewhere and ask
for more low-level comments if anyone would like to take the time to offer
them, but for now, I’m still working on the high-level ideas. The wiki pages
I’ve found have been very helpful; my appreciation to all who have contributed
to them!
Many thanks,
Alexis
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
