The compiler applies transformations `t ==> s` where `t` and `s` are
only provably equal, but not definitionally equal. Moreover, in
dependent type theory `C[t]` may be type correct, but `C[s]` is not
when `t` is provably equal to `s`, but not definitionally equal.
Consider the following example:
```
fun n : nat,
let v : nat := 0+n in
let b : bv (0+n) := bv.mk v in
b
```
If we replace the first `0+n` with `n`, we produce the type incorrect
term
```
fun n : nat,
let v : nat := n in
let b : bv (0+n) := bv.mk v in
b
```
This is incorrect because `b : bv (0+n)` and `bv.mk v : bv n`, and
`0+n` is not definitionally equal to `n`.
We considered two approaches to address this problem:
1- A relaxed type checker (see deleted file `ctype_checker.cpp`).
This approach does not solve the problem, see example in the end
of the commit.
2- Introduce `lc_cast`-applications to "fix" type problems. However,
it seems it is too expensive to detect all places that require a
`lc_ast` application. We did that in a few places, but there is major
omission: when we simplify `x : t := v` to `x : t := w` (like in the
example above), we did not find an efficient way to repair all
affected places. We have implemented the function `replace_fvar_with`,
but we would have to execute after each `x : t := v` ==> `x : t := w`
where `v` is not definitionally equal to `w`. We considered grouping
many `replace_fvar_with` together, but it would still be very
expensive. Basically, for any occurrence of `x` we would have to check
whether the resulting type changed or not. Another issue is that the
restrictions considered at `replace_fvar_with` seem to restrictive:
for example `x` cannot occur in lambda/let-decl types. This happens
very frequently in code that uses types such as `decidable p`.
Remark: note that the Lean3 simplifier does not have support for
simplyfing let-decls for this reason. It offers only two options:
expand the `let`, or skip it.
So, this commit gives up the idea of ensuring that each compiler step
produces a type correct Lean term. That is, we preserve type
information, but we do not guarantee the terms are type correct after
we apply compiler transformations.
Here are examples that demonstrate the `ctype_checker` approach does
not work.
```
def C : bool → Type → Type
| tt α := nat × α
| ff α := string × α
def ex (α β : Type) (x : nat × α) (h₂ : α = β) : nat × β :=
let f : Π (b : bool) (h₁ : b = tt) (α β : Type) (x : C b α) (h₂ : α = β), nat × β
:= λ (b : bool) (h₁ : b = tt) (α β : Type) (x : C b α) (h₂ : α = β),
let x₁ : C b β := @eq.ndrec Type α (λ z : Type, C b z) x β h₂ in
@eq.ndrec bool b (λ z : bool, C z β) x₁ tt h₁
in f tt rfl α β x h₂
```
Now, suppose we want to put in LCNF. Then, we have to decide whether
each `eq.ndrec` will become a cast or not. Now, suppose we use the
compiler type checker `is_def_eq`.
Then, the first `eq.ndrec` application is `@eq.ndrec Type α (λ z :
Type, C b z) x β h₂`, and we have that `x : C b α` and the expected
type is `C b β`, both types are stuck since they reduce to
`bool.cases_on b (string × α) (nat × α)` and `bool.cases_on b (string
× β) (nat × β)` respectively. Thus, they are considered definitionally
equal, and we do not introduce a cast.
The second `eq.ndrec` application is
`@eq.ndrec bool b (λ z : bool, C z β) x₁ tt h₁`, and we have
`x₁ : C b β` and the expected type is `nat × β`, again they are definitionally equal since `C b β`.
Thus, in LCNF, the example above would be:
```
def ex (α β : Type) (x : nat × α) (h₂ : α = β) : nat × β :=
let f : Π (b : bool) (h₁ : b = tt) (α β : Type) (x : C b α) (h₂ : α = β), nat × β
:= λ (b : bool) (h₁ : b = tt) (α β : Type) (x : C b α) (h₂ : α = β), x
in f tt rfl α β x h₂
```
The compiler type checker (`ctype_checker`) would say this is a type correct term.
Now, suppose we reduce `f tt rfl α β x h₂` using `csimp`, this term
would reduce to `x`.
Then, `f` is eliminated since it is not used anymore and we have the new simplified term
```
def ex (α β : Type) (x : nat × α) (h₂ : α = β) : nat × β := x
```
`ctype_checker` will report it to be type incorrect. Since, `x : nat × α`
and the result type is `nat × β`, and both are not stuck.
This example shows that by applying simple reduction rules (zeta/beta
in the example above) we can transform a type correct term into a type
incorrect one.
The type `any` is also problematic. Consider the following example.
```
def ex (x : nat) : real :=
let f : any -> real := fun z, z in
f x
```
It is type correct. If we apply `csimp`, we will get.
```
def ex (x : nat) : real := x
```
which is type incorrect. Again, reduction may transform a type correct term into a type incorrect one.
Note that, I am not using anything fancy here. We are just treating
`any` as definitionally equal to any type.
We use the auxiliary procedure pull_nested_rec_fn to pull recursive
application in nested match expressions. This is needed because the
nested match expression is compiled before we process the recursive
procedure that contains it. This transformation may produce
performance problems if the recursive application does not depend on
the data being matched. Here is an example from the new test:
```
def tst : tree → nat
| (tree.leaf v) := v
| (tree.node v l r) :=
match f v with
| tt := tst l
| ff := tst r
end
```
pull_nested_rec_fn will convert it into
```
def tst : tree → nat
| (tree.leaf v) := v
| (tree.node v l r) := tst._match_1 (f v) (tst l) (tst r)
```
Since our interpreter uses eager evaluation, both `(tst l)` and `(tst r)`
are executed. This commit fixes this issue by expanding `tst._match_1`
during code generation.
This happened in Johannes' real number formalization. We tried to
unfold a noncomputable definition even though it would have been erased
afterwards, and failed.
The check_computable check was introduced in order to fix the error
message in #1401, the error message is still intelligible in that
example.
