Can a TC plugin create new skolem vars when simplifying Givens?

[Nicolas Frisby]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20180624/561d5902/attachment.html>