Nick writes
Here's a small indicative example. In the "simplify Givens" step, the plugin
receives
[G] (p `Union` Singleton A) ~ (q `Union` Singleton B)
and I would ideally simplify that to
[G] p ~ (x `Union` Singleton B)
[G] q ~ (x `Union` Singleton A)
If we think of Union as a type-level function (which it is?), then the step you
outline above is similar to what happens during “flattening” of the Givens. We
get this:
[G] fsk1 ~ p `Union` Singleton B (CFunEqCan)
[G] fsk2 ~ q `Union` Singleton A (CFunEqCan)
[G] fsk1 ~ fsk2 (CTyEqCan)
* The newly generated skolems are called “flatten-skolems” or fsks for
short.
* The new skolems are kept in the `inert_fsks` field of the `InertSet`.
* A new one is created by `TcSMonad.newFlattenSkolem`
* All fsks are eliminated by TsSMonad.unflattenGivens
Returning to your point, you are exploiting a property of sets that allows you
to say that if
p U X = q U Y
Then suppose r = p • q
then p = r U Y, q = r U X
And now we can eliminate all uses of p, q in favour of r. But if you do this
in a type system, we have a problem: where is ‘r’ bound? E.g. if you have
f :: forall p q. (p `Union` A) ~ (q `Union` B) => blah
Then p, q are bound by the forall, but r is not. To put it another way, what
well-typed Core program would you like to generate?
You could do this:
[G] fsk1 ~ p `Union` Singleton B (CFunEqCan)
[G] fsk2 ~ q `Union` Singleton A (CFunEqCan)
[G] fsk3 ~ p `Intersect` q (CFunEqCan)
[G] fsk4 ~ fsk3 `Union` Singleton B (CFunEqCan)
[G] fsk5 ~ fsk3 `Union` Singleton A (CFunEqCan)
[G] fsk1 ~ fsk2 (CTyEqCan)
[G] p ~ fks4 (CTyEqCan)
[G] q ~ fsk5 (CTyEqCan)
The ‘r’ is just fsk3. It’ll be eliminated by unflattenGivens, so there is no
problem with scoping.
I have no idea whether that’ll help you prove the things you want to prove!
Simon
From: ghc-devs
<[email protected]<mailto:[email protected]>> On Behalf
Of Nicolas Frisby
Sent: 24 June 2018 19:01
To: [email protected]<mailto:[email protected]>
Subject: Can a TC plugin create new skolem vars when simplifying Givens?
I'm still spending the occasional weekend working on a type checker plugin for
row types (actually "set" types at first, but I haven't thought of a less
ambiguous term for that).
One point of complexity in the plugin has to do with creating fresh variables
when simplifying Givens. Some constraints are traditionally simplified by
introducing a fresh variable. For Wanted constraints, that's easy
(newFlexiTyVar). For Givens, though, I haven't figured out how to do it.
This email is just to ask these two questions:
1) Is there a function to add a new skolem variable when simplifying Givens?
2) Assuming not, is there a strong reason for there to never be such a
function?
Here's a small indicative example. In the "simplify Givens" step, the plugin
receives
[G] (p `Union` Singleton A) ~ (q `Union` Singleton B)
and I would ideally simplify that to
[G] p ~ (x `Union` Singleton B)
[G] q ~ (x `Union` Singleton A)
for some fresh skolem variable x. But I don't see how to properly create a
fresh skolem variable in the Givens. If these were Wanteds, I would just use
newFlexiTyVar.
I think this is analogous to a hypothetical type checker plugin that eta
expands tuples. If we were to simplify
[G] ... (x :: (k1,k2)) ...
to
[G] ... '(x1 :: k1,x2 :: k2) ...
we'd have to generate x1 and x2 somehow. The only method I'm aware of for that
is to use Fst x and Snd x instead (ie type families). That might be acceptable
for the tuple expansion example, but I'm very reticent to use something like
that for the set types plugin.
I have a plan to get by without creating these variables when simplifying
Givens, but it's not simple. I'd be delighted if it were possible to create
them. Hence my two questions listed above.
Thank you for your time. -Nick
_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
