We are considering removing `.` as an alternative for `·` in the
lambda dot notation (e.g., `(·+·)`).
Reasons:
- `.` is not a perfect replacement for `·` (e.g., `(·.insert ·)`)
- `.` is too overloaded: `(f.x)` and `(f .x)` and `(f . x)`. We want to keep the first two.
This modification is relevant for fixing regressions on recent changes
to the auto implicit behavior for inductive families.
The following declarations are now accepted:
```lean
inductive HasType : Fin n → Vector Ty n → Ty → Type where
| stop : HasType 0 (ty :: ctx) ty
| pop : HasType k ctx ty → HasType k.succ (u :: ctx) ty
inductive Sublist : List α → List α → Prop
| slnil : Sublist [] []
| cons l₁ l₂ a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
| cons2 l₁ l₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)
inductive Lst : Type u → Type u
| nil : Lst α
| cons : α → Lst α → Lst α
```
TODO: universe inference for `inductive` should be improved. The
current approach is not good enough when we have auto implicits.
TODO: allow implicit fixed indices that do not depend on indices that
cannot be moved to become parameters.
TODO: convert fixed indices to parameters. Motivation: types such as
```lean
inductive Foo : List α → Type
| mk : Foo []
```
Users should not need to write
```lean
inductive Foo {α} : List α → Type
| mk : Foo []
```
The new test exposes the problem fixed by this commit.
In the termination proof we have two `sizeOf xs` terms that are not
syntactically identical (only definitional equal) because the
instances are different.
The issue is only going to be properly fixed when we rewrite `csimp`
in Lean. The `csimp` performs transformations that do not preserve
typability, but it also uses the kernel `infer_type` which assumes the
input is type correct. In the new `csimp`, we must have a different
`infer_type` which returns an `Any` type in this kind of situation.
The workaround in this commit simply disables optimizations when
`infer_type` fails. It does not fix all occurrences of this problem,
but the two places that issue #1030 triggered.
closes#1030
