Plus and times aren't robust for beta reduction

The subtyping and ad-hoc type of `+` make it a bit flaky.

This works fine:
```haskell
>>> (\x -> 3.4 + x) 1
4.4
```

But this one doesn't
```haskell
>>> 3.4 + 1
Not a subtype
The following type:
Real
… cannot be a subtype of:
Natural
```

All I've done here is beta reduction, which one would usually expect to preserve type inference.

Ideally, I think this should also work:

```haskell
>>> (\x -> 1 + x) 3.14
Not a subtype
…
```

I can see why is doesn't, but Ignoring that `+` also does lists and text.

```haskell
>>> :t (\x -> 1 + x)
Natural -> Natural
```

Could it instead be something like:
```haskell
>>> :t (\x -> 1 + x)
forall (a : Type) such that (Natural <: a). a -> a
```

Start by reproducing the two REPL examples and the `:t (\x -> 1 + x)` query described in the issue. Trace how beta reduction, subtyping, and the ad-hoc type of `+` interact; done means the numeric examples preserve type inference without losing the existing list and text behavior.

Written by the indexing model from the issue text.