We should not rely on this feature. It can be quite expensive.
We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as
is_convertible(num, Nat)
If is_convertible starts unfolding opaque definitions, we would keep expanding num.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
The main motivation is that we will be able to move equalities between universes.
For example, suppose we have
A : (Type i)
B : (Type i)
H : @eq (Type j) A B
where j > i
We didn't find any trick for deducing (@eq (Type i) A B) from H.
Before this commit, heterogeneous equality as a constant with type
heq : {A B : (Type U)} : A -> B -> Bool
So, from H, we would only be able to deduce
(@heq (Type j) (Type j) A B)
Not being able to move the equality back to a smaller universe is
problematic in several cases. I list some instances in the end of the commit message.
With this commit, Heterogeneous equality is a special kind of expression.
It is not a constant anymore. From H, we can deduce
H1 : A == B
That is, we are essentially "erasing" the universes when we move to heterogeneous equality.
Now, since A and B have (Type i), we can deduce (@eq (Type i) A B) from H1. The proof term is
(to_eq (Type i) A B (to_heq (Type j) A B H)) : (@eq (Type i) A B)
So, it remains to explain why we need this feature.
For example, suppose we want to state the Pi extensionality axiom.
axiom hpiext {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} :
A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x)
This axiom produces an "inflated" equality at (Type U) when we treat heterogeneous
equality as a constant. The conclusion
(∀ x, B x) == (∀ x, B' x)
is syntax sugar for
(@heq (Type U) (Type U) (∀ x : A, B x) (∀ x : A', B' x))
Even if A, A', B, B' live in a much smaller universe.
As I described above, it doesn't seem to be a way to move this equality back to a smaller universe.
So, if we wanted to keep the heterogeneous equality as a constant, it seems we would
have to support axiom schemas. That is, hpiext would be parametrized by the universes where
A, A', B and B'. Another possibility would be to have universe polymorphism like Agda.
None of the solutions seem attractive.
So, we decided to have heterogeneous equality as a special kind of expression.
And use the trick above to move equalities back to the right universe.
BTW, the parser is not creating the new heterogeneous equalities yet.
Moreover, kernel.lean still contains a constant name heq2 that is the heterogeneous
equality as a constant.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Unification constraints of the form
ctx |- ?m[inst:i v] == T
and
ctx |- (?m a1 ... an) == T
are delayed by elaborator because the produce case-splits.
On the other hand, the step that puts terms is head-normal form is eagerly applied.
This is a bad idea for constraints like the two above. The elaborator will put T in head normal form
before executing process_meta_app and process_meta_inst. This is just wasted work, and creates
fully unfolded terms for solvers and provers.
The new test demonstrates the problem. In this test, we mark several terms as non-opaque.
Without this commit, the produced goal is a huge term.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Projections build more general solutions. This commit also adds a test that demonstrates the issue. Before this commit, the elaborator would produce the "constant" predicate (fun x, a + b = b + a).
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
