@Kha we are getting better error message, but we need to figure out a
way to suppress error messages that come from the "plumbing".
For example, in the following example.
```
def f4 (b : Bool) (n : Nat) (v : Vector Nat n) : Vector Nat (n+1) := do
if b then
v := Vector.cons 1 v
Vector.cons 1 v
```
We get the nice "invalid reassignment" error at `v := ...`, but
we also get the nasty
```
error: application type mismatch
jp✝ v
argument
v
has type
Vector Nat (n + 1)
but is expected to have type
Vector Nat n
failed to synthesize instance
CoeT (Vector Nat (n + 1)) v (Vector Nat n)
```
Where `jp✝` is a joinpoint created by the do-notation macro expander.
I thought about using `withoutErrToSorry` when elaborating the expanded
`do` term.
We may also try to add more helper hints such as `ensureTypeOf!` and
use them around "plumbing" code (e.g., "joinpoint goto"s)
@Kha The new `do` notation works for pure code too.
It automatically inserts `Id` if the expected type is not a monad.
This works great when we are not conflating data and control.
After deleting `Monad List`, we will be able to write functions such as
```lean
def mapWhen (p : Nat → Bool) (f : Nat → Nat) (xs : List Nat) : List Nat := do
for x in xs do
if p x then
x := f x
```
without adding `Id.run` before the `do`.
In the following example, the output produced by `dbgTrace!` was not
being captured. It could break the lean server. At least, it broke the lean4-mode.
```lean
def f (x : Nat) : Nat :=
dbgTrace! ">>> " ++ toString x;
x + 1
eval f 10
```
cc @Kha
- Add support for `if h:c then t else e`, `h` may shadow reassignable
variables
- Pattern variables in `match` alternatives may shadow reassignable
variables
- A single declaration/reassignment in a `do` block may
declare/reassign multiple variables. Example: `let (x, y) := t`
