Plus and times aren't robust for beta reduction

[HuwCampbell]

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

This works fine:

>>> (\x -> 3.4 + x) 1
4.4

But this one doesn't

>>> 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:

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

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

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

Could it instead be something like:

>>> :t (\x -> 1 + x)
forall (a : Type) such that (Natural <: a). a -> a

[Gabriella439]

Currently the type checker does not yet support subtyping constraints in types, but it might soon (as part of implementing support for record concatenation, which seems to require this)