Lost notations

Stream: general

[Patrick Massot]

For expository purposes, I'm trying to rewrite part of filter theory. But Lean loses its notations. In the following code (ran with Lean 3.5.1, not yet 3.6.0), do you see set membership and set inclusion notations disappearing from tactic state? Do you understand why?

import tactic
open set

structure base_de_filtre (X : Type*) :=
(ι        : Type*)
(s        : ι → set X)
(defaut   : ι)
(inter    : ∀ i j, ∃ k, s k ⊆ s i ∩ s j)

structure filtre (X : Type*) :=
(sets             : set (set X))
(univ_sets        : univ ∈ sets)
(sets_of_superset : ∀ {U V}, U ∈ sets → U ⊆ V → V ∈ sets)
(inter_sets       : ∀ {U V}, U ∈ sets → V ∈ sets → U ∩ V ∈ sets)

def filtre_de_base {X : Type*} (B : base_de_filtre X) : filtre X :=
{ sets := {U | ∃ i : B.ι, B.s i ⊆ U},
  univ_sets := begin
    use B.defaut,
    intros x hx,
    trivial,
  end,
  sets_of_superset := begin
    rintros U V ⟨i, hi⟩ hUV,
    use i,
    change B.s i ⊆ V,
    transitivity U ; assumption,
  end,
  inter_sets := begin
    rintros U V ⟨i, hi⟩ ⟨j, hj⟩,
    cases B.inter i j with k hk,
    use k,
    intros x hx,
    exact ⟨hi (hk hx).1, hj (hk hx).2⟩,
  end }

This is driving me crazy.

[Patrick Massot]

I see tactic states like:

1 goal
X : Type ?,
B : base_de_filtre X
⊢ set.mem univ {U : set X | ∃ (i : B.ι), set.subset (B.s i) U}

[Patrick Massot]

I just noticed the strange Type ? in the pasted state. Removing all Type* makes Lean use notations again!

[Patrick Massot]

Thanks to everybody (from every universe) who helped me fixing this.

[Patrick Massot]

I'm still interested in reading more explanation about why Lean is losing notations here.

[Floris van Doorn]

I could reproduce it, and it looks really weird. No idea why this happens.

[Mario Carneiro]

I recall @Chris Hughes filed a bug about this a while back

[Mario Carneiro]

The use of universe metavariables causes structure literals to unfold notations like has_mem.mem for some reason

[Mario Carneiro]

(This isn't actually a notation issue in the sense of printing; set.mem has no notation, only has_mem.mem. The question is why has_mem.mem was unfolded)

[Kevin Buzzard]

Is it the issue which is fixed by writing Type u instead of Type *?

[Kevin Buzzard]

weird coincidence -- this just happened to me when bundling subgroups. For me the universe u trick fixes it.