In the new frontend,
```lean
@[macroInline] def or : Bool → Bool → Bool
| true, _ => true
| false, b => b
```
is compiled as
```lean
def or (x y : Bool) : Bool :=
or.match_1 _ x y (fun _ => true) (fun b => b)
```
Thus, the `[macroInline]` attribute does not guarantee that `y` is
evalutated only when `x` is `false`. The new definition does.
This issue was not exposed before because the compiler has an
optimization that float let-decls when they are used in a single
branch.
@Kha We have talked about removing `macroInline`, and defining
functions such as `or` as
```lean
@[inline] def or (x : Bool) (y : Unit -> Bool) : Bool :=
match x with
| true => true
| false => y ()
```
and define `x || y` as notation for `or x (fun _ => y)`.
I think this is the way to go for polymorphic operators such as `<|>`,
but I am not sure about `or`. New users will probably be puzzled by
it. In particular when they are writing proofs.
After this commit, we have to use an explicit `discard` in code such as
```
def g (x : Nat) : IO Nat := ...
def f (x : Nat) : IO Unit := do
discard <| g x -- type error without the `discard`
IO.println x
```
Motivation: prevent users from making mistakes such as
```
def f (xs : Array Nat) : IO Unit := do
xs.set! 0 1
IO.println xs
```
when they meant to write
```
def f (xs : Array Nat) : IO Unit := do
let xs := xs.set! 0 1
IO.println xs
```
@Kha The motivation is to allow users to define default instances such as
```lean
@[defaultInstance 1]
instance : OfScientific Real where
...
```
Then, numerals such as `1.2` and `3.4e10` will be `Real` by default instead of `Float`.
Before this commit, the threshold was the amount of "fuel".
Now, it is the maximum number of instances used to solve a TC problem.
We have two thresholds
- `maxInstSize`: default 128
- `maxCoeSize`: default 16. It is similar to `maxInstSize`, but used for automatic coercions.
cc @Kha
