Flip the Left/Right branches of Data.So.choose

[msmorgan]

Since Idris 2 will be a "major version" release, I'm wondering if it would be acceptable to change the type of Data.So.choose. The current signature is surprising, since usually the Left variant of an Either is used for the error type, and Right is used for success. It's odd to see the negation of the boolean input be the Right variant.

Before: choose : (b : Bool) -> Either (So b) (So (not b)) After: choose : (b : Bool) -> Either (So (not b)) (So b)

Because this is a type-level change, existing programs using Data.So would fail to compile in Idris 2. Usually the fix will be to swap the Left and Right identifiers in a case expression.

[edwinb]

I'm not fussy about this one, to be honest - it feels like there ought to be a neater way to do it in any case (I'm not keen on So for anything except primitive types, and we probably ought to think more carefully about even that).

So if nobody else shouts, and you want to change it, please just go ahead.