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 mailto:ghc-devs-bounces@haskell.org> On Behalf Of Nicolas Frisby Sent: 24 June 2018 19:01 To: ghc-devs@haskell.orgmailto:ghc-devs@haskell.org 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