## 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.