Member constraints only allow nesting on the right

[robrix]

:+: can technically form the branches of a tree, but we always use it as a right-nested, Pure- or Lift m-terminated list.

This means that following #199, we can’t usefully reintroduce NonDet as a synonym for Choose :+: Empty, because that sum would be nested on the left; and while that wouldn’t impair anything using the Alternative interface, anything requiring Member Choose sig or Member Empty sig wouldn’t work, since neither Choose nor Empty separately unifies with Choose :+: Empty together.

The root of the problem is that even with overlapping instances, ghc’s non-backtracking constraint solver doesn’t allow us to select different instances for occurrences on the left or the right depending on the solution of the context’s constraints.

[robrix]

The root of the problem is that even with overlapping instances, ghc’s non-backtracking constraint solver doesn’t allow us to select different instances for occurrences on the left or the right depending on the solution of the context’s constraints.

We can, however, use advanced overlap techniques involving having a type family compute the path to a member and define instances against said path.

That would allow us to provide NonDet as a synonym for Choose :+: Empty while still satisfying both Member Choose sig and Member Empty sig constraints.

It remains to be seen what this would do to compile times.

[robrix]

This problem is also preventing us from splitting up Error into separate Throw and Catch effects (cf #154, 🎩 @mitchellwrosen), since requiring users to write Member (Catch e) sig, Member (Throw e) sig is a very poor substitute for Member (Error e) sig, on top of the already inconvenient requirement of providing both Member and Carrier constraints (cf #212).

[robrix]

This could potentially make it more convenient to write carriers handling multiple effects, since they could all nest on the left, with other effects on the right, making the shape of almost all Carrier instances much more uniform.

Further, @lexi-lambda had an idea for the carrier interface which IIRC would benefit from having this kind of uniformity.

[robrix]

I’m experimenting with this in diffused-effects; early results are promising, tho I haven’t thrown it at large effect lists yet: fused-effects/diffused-effects#5

[robrix]

Negligible effect on compile times unless combined with a type family solution to #212.