Update 'Union' with use of more precise proof

[TheMatten]

Use of more precise:

data Elem :: Eff -> [Eff] -> Type where
  Here ::              Elem e (e ': es)
  In   :: Elem e es -> Elem e (d ': es)

instead of Nat+SNat allows us to prove important properties and makes implementation a little bit simpler, e.g.:

absurdU :: Union '[] m a -> a
absurdU = absurdU

can now be proved with EmptyCase:

absurdU (Union p  _) = case p of {}

TODO:

• Decide on custom type errors
• Make fundep plugin work again

[isovector]

Before going too far on this, I'd want to look at the perf. I have a sneaking suspicion that this thing will allocate much harder than Union. I spent a looooong time making the perf good on the current impl, and suspect that it's quite brittle to changes like these. Maybe we should hold off until 8.10 when it becomes easy to test something like this?

[TheMatten]

Okay, no problem - should I close it for now?

[isovector]

Your call! I'm curious what tangible benefits this buys us --- does it allow us to do anything we couldn't otherwise, or is it merely aesthetic?

[TheMatten]

Actually, #107 comes to my mind - Member' constraint would avoid need for equality (but there may be some other way too)

[isovector]

I'm going to close this for now --- feel free to reopen if you feel we should reconsider.

[KingoftheHomeless]

Stuff like #281 has made more more and more attracted to a solution like this. It'd make the machinery behind those kinds of stuff prettier. membership :: Member e r => Elem r e is also really powerful, and would enable stuff like a Compose :: EffectRow -> Effect effect, which I have trouble implementing using the current machinery.

You've commented about performance, but shouldn't Elem have just the same internal representation as SNat?

[isovector]

That's a reasonable argument. Anyone want to tackle this?

[KingoftheHomeless]

I already have a solution in the works, so I'm up for it, but @TheMatten is probably also interested.

Edit: Actually, it's very similar to what this pull request does, except it also addresses custom error messages.

[TheMatten]

@KingoftheHomeless I currently don't have time to finish this - go for it if you want 🙂