Zulip Chat Archive

Stream: general

Topic: strange elaboration error


view this post on Zulip 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 ≃ₘ^nI, I' M', h.to_equiv)
| e, _, _ e', _, _ rfl := rfl

lemma ext {h h' : M ≃ₘ^nI, 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 ≃ₘ^ nI,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 ≃ₘ^ nI,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?

view this post on Zulip Gabriel Ebner (Mar 03 2021 at 16:53):

I think I need to install new fonts...

view this post on Zulip Eric Wieser (Mar 03 2021 at 16:55):

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

view this post on Zulip Yury G. Kudryashov (Mar 03 2021 at 16:56):

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

view this post on Zulip Eric Wieser (Mar 03 2021 at 16:56):

{H_1 : Type u_4} looks suspicious there?

view this post on Zulip Eric Wieser (Mar 03 2021 at 16:56):

Try renaming H to H_not_the_a_bug_again?

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Mar 03 2021 at 16:58):

Indeed, it's about the H:

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

view this post on Zulip Yury G. Kudryashov (Mar 03 2021 at 16:58):

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

view this post on Zulip 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