strange elaboration error

Stream: general

[Yury G. Kudryashov]

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]

I think I need to install new fonts...

[Eric Wieser]

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

[Yury G. Kudryashov]

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

[Eric Wieser]

{H_1 : Type u_4} looks suspicious there?

[Eric Wieser]

Try renaming H to H_not_the_a_bug_again?

[Eric Wieser]

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

[Gabriel Ebner]

Indeed, it's about the H:

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]

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

[Mario Carneiro]

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