Stream: general

Topic: strange elaboration error

Yury G. Kudryashov (Mar 03 2021 at 16:51):

Hi, the following code fails with a strange error:

import geometry.manifold.diffeomorph

open_locale manifold

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [normed_space 𝕜 E]
{E' : Type*} [normed_group E'] [normed_space 𝕜 E']
{H : Type*} [topological_space H]
{H' : Type*} [topological_space H']
(I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H')

variables (M : Type*) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
(M' : Type*) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']
(n : with_top ℕ)

namespace times_diffeomorph

lemma to_equiv_inj : function.injective (λ h : M ≃ₘ^n⟮I, I'⟯ M', h.to_equiv)
| ⟨e, _, _⟩ ⟨e', _, _⟩ rfl := rfl

lemma ext {h h' : M ≃ₘ^n⟮I, I'⟯ M'} (H : ∀ x, h x = h' x) : h = h' :=
by { apply to_equiv_inj, ext, apply H }

end times_diffeomorph


Error message:

21:7: kernel failed to type check declaration 'ext' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
∀ {𝕜 : Type u_1} [_inst_1 : nondiscrete_normed_field 𝕜] {E : Type u_2} [_inst_2 : normed_group E]
[_inst_3 : normed_space 𝕜 E] {E' : Type u_3} [_inst_4 : normed_group E'] [_inst_5 : normed_space 𝕜 E']
[_inst_6 : topological_space H] {H' : Type u_5} [_inst_7 : topological_space H'] (I : model_with_corners 𝕜 E H)
(I' : model_with_corners 𝕜 E' H') (M : Type u_6) [_inst_8 : topological_space M] [_inst_9 : charted_space H M]
[_inst_10 : smooth_manifold_with_corners I M] (M' : Type u_7) [_inst_11 : topological_space M']
[_inst_12 : charted_space H' M'] [_inst_13 : smooth_manifold_with_corners I' M'] (n : with_top ℕ) {H_1 : Type u_4}
{h h' : M ≃ₘ^ n⟮I,I'⟯M'}, (∀ (x : M), ⇑h x = ⇑h' x) → h = h'
elaborated value:
λ {𝕜 : Type u_1} [_inst_1 : nondiscrete_normed_field 𝕜] {E : Type u_2} [_inst_2 : normed_group E]
[_inst_3 : normed_space 𝕜 E] {E' : Type u_3} [_inst_4 : normed_group E'] [_inst_5 : normed_space 𝕜 E']
[_inst_6 : topological_space H] {H' : Type u_5} [_inst_7 : topological_space H'] (I : model_with_corners 𝕜 E H)
(I' : model_with_corners 𝕜 E' H') (M : Type u_6) [_inst_8 : topological_space M] [_inst_9 : charted_space H M]
[_inst_10 : smooth_manifold_with_corners I M] (M' : Type u_7) [_inst_11 : topological_space M']
[_inst_12 : charted_space H' M'] [_inst_13 : smooth_manifold_with_corners I' M'] (n : with_top ℕ) {H_1 : Type u_4}
{h h' : M ≃ₘ^ n⟮I,I'⟯M'} (H_1 : ∀ (x : M), ⇑h x = ⇑h' x),
to_equiv_inj I I' M M' n (equiv.ext (λ (x : M), H_1 x))
nested exception message:
failed to add declaration to environment, it contains local constants


@Gabriel Ebner Do you know what does this error message mean? How can I avoid it?

Gabriel Ebner (Mar 03 2021 at 16:53):

I think I need to install new fonts...

Eric Wieser (Mar 03 2021 at 16:55):

I think last time I saw this message it was a stupid mistake I made...

Yury G. Kudryashov (Mar 03 2021 at 16:56):

I wonder what is {H_1 : Type u_4} in the error message

Eric Wieser (Mar 03 2021 at 16:56):

{H_1 : Type u_4} looks suspicious there?

Eric Wieser (Mar 03 2021 at 16:56):

Try renaming H to H_not_the_a_bug_again?

Eric Wieser (Mar 03 2021 at 16:57):

Oh, you have both a type H and a hypothesis H, and it's getting them confused

Gabriel Ebner (Mar 03 2021 at 16:58):

lemma ext {h h' : M ≃ₘ^n⟮I, I'⟯ M'} (H : ∀ x, h x = h' x) : h = h' :=
by do
unfreezing revert_all,
tgt ← target,
trace tgt.list_local_consts
-- [H]


Yury G. Kudryashov (Mar 03 2021 at 16:58):

If I rename the assumption H to something else, it works.

Mario Carneiro (Mar 04 2021 at 02:57):

this isn't really the a bug, since both variables were named by the user, introducing some explicit name shadowing that some tactics automatically dedup

Last updated: May 16 2021 at 20:13 UTC