Rebindable Syntax and LinearTypes (allow a version of RebindableSyntax without ifThenElse)

When working with both LinearTypes and unlifted data types, I find I often want to use RebindableSyntax to overload things.

However, right now RebindableSyntax is one monolithic switch which turns on things that are desirable to overload e.g. numeric literals, but also turns on things that I can't properly typecheck myself, such as ifThenElse.

Being able to split apart the scope of RebindableSyntax to allow the exclusion of ifThenElse would suffice.

Alternatives

Morally, one can view the issue that viewed as a function ifThenElse doesn't really look like ifThenElse :: Bool -> a -> a -> a. The one supplied by GHC has superpowers that such a function lacks.

First, it works for all runtime representations, and it only forces one of its arguments. You see this if you to to define

ifThenElse :: forall (a :: TYPE 'IntRep). Bool -> a -> a -> a
ifThenElse True t _ = t
ifThenElse False _ f = f

Evaluating ifThenElse False undefined 1# now throws an exception.

We can fix this part by defining

type Lev (a :: TYPE r) = ()~() => a
ifThenElse :: forall (a :: TYPE r). Bool -> Lev a -> Lev a -> a
ifThenElse True t _ = t
ifThenElse False _ f = f

Now, ifThenElse False undefined 1# returns 1# as expected. Lev also trickily let us side-step any levity polymorphism concerns with taking values of unknown RuntimeRep in negative position.

However, even if we can fix the levity issue we can't currently fix the linearity issue with the current type.

ifThenElse :: forall (a :: TYPE r). Bool -> a -> a -> a

isn't general enough to handle if _ then _ else _ at linear types.

We can't put

ifThenElse :: forall (a :: TYPE r). Bool -> a %1 -> a %1 -> a

as we don't use each branch linearly. Morally we don't take two functions, we take the "with" or & of two functions in the linear logic sense. With a b isn't two separate arguments it a single-shot user choice to get one of the two things. It is the third linear logic connective that usually shows up in intuitionistic linear logic. In the vending machine metaphor. (a,b) is the ability/requirement to consume a and b both. Either a b is the ability/requirement to consume a or b, but you don't get to pick which, it is the suppliers choice. With a b is the ability/requirement to consume a or b, but the consumer gets to pick. That is exactly what ifThenElse is doing above when linear types are turned on.

We can model With in haskell as a function.

data Choice a b x where
  L :: Choice a b a
  R :: Choice a b b

newtype With a b = With { runWith :: (forall x. Choice a b x %1 -> x) }

pickL :: With a b -> a
pickR :: With a b -> b

Then a user version of ifThenElse morally wants to consume the With of two code branches it is supplied.

However, here the rabbit hole ends, it's not really all that convenient to define such a beast, and even if we made up a With data type and used it to wrap both branches of the ifThenElse, this style of overloading ifThenElse isn't compatible with the version that arises in EDSLs and needs GADTs, RankNTypes...

As a result, I currently have to just advocate for users using MultiWayIf or pattern guards if they use my library, but would like to be able to leave them access to if then else notation.

tl;dr I'd like some way to split off ifThenElse from RebindableSyntax it is currently quite the blunt instrument and ifThenElse currently can't be overloaded correctly in light of new language features.