universe issue with `Type*`

Stream: general

[Kevin Buzzard]

There was a time when I was scared of Type*, preferring to roll my own universes. However there were changes, particularly the advent of {A B C : Type*}, and I switched back. But here's something which I think is odd:

import linear_algebra.basis

open submodule

open_locale big_operators classical

open finsupp

universe u

set_option pp.universes true

lemma submodule.span_as_sum {R : Type*} {M : Type*} [semiring R] [add_comm_group M] [semimodule R M]
  {m : M} {s : set M} (hm : m ∈ submodule.span R s) :
  ∃ c : M →₀ R, (c.support : set M) ⊆ s ∧ (c.sum (λ i, (smul_add_hom R M).flip i)) = m :=
begin
  refine span_induction hm (λ x hx, _) ⟨0, by simp⟩ _ _; clear hm m,
  { refine ⟨finsupp.single x 1, λ y hy, _, by simp⟩,
    rw [finset.mem_coe, mem_support_single] at hy,
    rwa hy.1 },
  { rintros x y ⟨c, hc, rfl⟩ ⟨d, hd, rfl⟩,
    refine ⟨c + d, _, by simp⟩,
    refine set.subset.trans _ (set.union_subset hc hd),
    rw [← finset.coe_union, finset.coe_subset],
    exact support_add },
  { rintros r m ⟨c, hc, rfl⟩,
    refine ⟨r • c, λ x hx, hc _, _⟩,
    { rw [finset.mem_coe, mem_support_iff] at hx ⊢,
      rw [finsupp.coe_smul] at hx,
      exact right_ne_zero_of_mul hx },
    { rw sum_smul_index' (λ (m : M), _),
      { convert (add_monoid_hom.map_finsupp_sum (smul_add_hom R M r) _ _).symm,
        ext m s,
        simp [mul_smul r s m] },
      { exact (((smul_add_hom R M).flip) m).map_zero } } }
end

#check @submodule.span_as_sum
/-
submodule.span_as_sum.{u_1 u_2 u_3} :
  ∀ {R : Type u_1} {M : Type (max u_2 u_3)} [_inst_1 : semiring.{u_1} R] [_inst_2 : add_comm_group.{(max u_2 u_3)} M]
  [_inst_3 : semimodule.{u_1 (max u_2 u_3)} R M] {m : M} {s : set.{(max u_2 u_3)} M},
    m ∈ span.{u_1 (max u_2 u_3)} R s →
    (∃ (c : M →₀ R),
       ↑(c.support) ⊆ s ∧ c.sum (λ (i : M), ⇑(⇑((smul_add_hom.{u_1 (max u_2 u_3)} R M).flip) i)) = m)
-/

I have R and M in two different universes, but somehow M's universe has become the max of two unspecified universes which I can't figure out the origin of. Paging through the proof I didn't spot any occurrence of u_2 or u_3 outside max u_2 u_3. Furthermore if I change {M : Type*} to {M : Type u} then the proof compiles just the same and the universes in the goal are what I would expect -- one for R and one for M and that's it.

What's going on?

[Kevin Buzzard]

Oh it's not even the proof -- if I sorry the proof I still observe the same phenomenon.

[Kevin Buzzard]

If I change (λ i, (smul_add_hom R M).flip i) to (λ m r, r • m) the issue disappears

[Kevin Buzzard]

Got it -- it's add_monoid_hom.flip.

[Damiano Testa]

I am still confused by this. Is there an explicit argument that smul_add_hom wants that is not there, then?

[Damiano Testa]

Should there be an extra R somewhere?

[Eric Wieser]

docs#add_monoid_hom.flip for reference

[Kevin Buzzard]

OK so here is some behaviour I find counterintuitive:

import algebra.module.basic

variables {R : Type*} {M : Type*} [semiring R] [add_comm_group M] [semimodule R M]

def a : R →+ M →+ M := smul_add_hom R M

#check @a -- Π {R : Type u_3} {M : Type u_4}

def b {R : Type*} {M : Type*} [semiring R] [add_comm_group M] [semimodule R M]
 : M →+ R →+ M := (smul_add_hom R M).flip

#check @b -- Π {R : Type u_3} {M : Type (max u_4 u_5)}  ...

def c : M →+ R →+ M := (smul_add_hom R M).flip

#check @c -- Π {R : Type u_3} {M : Type u_4} ...

def d : M →+ R →+ M := a.flip
/-
type mismatch at application
  a.flip
term
  a
has type
  ?m_1 →+ ?m_2 →+ ?m_2 : Type (max ? ?)
but is expected to have type
  ?m_1 →+ ?m_2 →+ ?m_3 : Type (max ? ? ?)
Additional information:
/home/buzzard/active-lean-projects/mathlib/scratch/scratch5.lean: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch at application
    a.flip
  term
    a
  has type
    ?m_1 →+ ?m_2 →+ ?m_2 : Type (max ? ?)
  but is expected to have type
    ?m_1 →+ ?m_2 →+ ?m_3 : Type (max ? ? ?)
-/

[Eric Wieser]

Type* in a lemma or definition is adjusted based on its use

[Eric Wieser]

Type* in variables always means "just make another universe"

[Eric Wieser]

I've seen this a lot where I write Sort* in a lemma, but lean has worked out that my typeclasses require Type* and changed it for me silently

[Kevin Buzzard]

variables {R : Type*} {M : Type*}

def a : R → M → M := λ r m, m

#check @a -- Π {R : Type u_3} {M : Type u_4}

def b {R : Type*} {M : Type*} : M → R → M := flip (λ r m, m)

#check @b -- Π {R : Type u_3} {M : Type u_4}  ...

So the phenomenon doesn't persist for bare functions.

[Kevin Buzzard]

import algebra.module.basic

universes u v w

variables {M : Type u} {N : Type v} {P : Type w}
  [add_monoid M] [add_monoid N] [add_comm_monoid P]

#check flip -- (M → N → P) → N → M → P
#check (M → N → P) → N → M → P -- Type (max (max u v w) v u w)

#check add_monoid_hom.flip -- (M →+ N →+ P) → N →+ M →+ P

#check (M →+ N →+ P) → N →+ M →+ P -- Type (max (max u v w) v u w)

This is the issue I think. add_monoid_hom.flip, and even flip, produce terms whose types have some pretty crazy universes.

[Kevin Buzzard]

I think we need to simp those universe parameters

[Kevin Buzzard]

I can't reproduce with normal functions :-/ I'm still wondering if this can be fixed in the sense that one could get a.flip working.

import algebra.module.basic

universes u v w

structure foo (M : Type u) (N : Type v) (P : Type w) :=
(hom : M → N → P)

variables {M : Type u} {N : Type v} {P : Type w} [has_scalar M N]

def foo.flip (c : foo M N P) : foo N M P := ⟨λ n m, c.hom m n⟩

def a : foo M N N := ⟨λ m n, m • n⟩

#check @a -- Π {M : Type u_1} {N : Type u_2} ...

def b {M N : Type*} [has_scalar M N]: foo N M N := (⟨λ m n, m • n⟩ : foo M N N).flip

#check @b -- Π {M : Type u_1} {N : Type u_2} ...

[Mario Carneiro]

This is usually the fault of a bad definition, which has two universe arguments and only uses max u v, like you found. But looking at add_monoid_hom.flip I don't see anything suspicious, it uses exactly as many universes as one would expect.

EDIT: Actually the issue is add_monoid_hom.flip, or more specifically the unification problem that arises when you match an argument of type R →+ M →+ M against the input to add_monoid_hom.flip, because this basically looks like

@add_monoid_hom.{?l_1 ?l_2} (@add_monoid_hom.{?l_2 ?l_2} M M)

vs

@add_monoid_hom.{?l_3 (max ?l_4 ?l_5)} ?m_6 (@add_monoid_hom.{?l_4 ?l_5} ?m_7 ?m_8))

which results in unifying ?l_2 against max ?l_4 ?l_5, resulting in two free universe metavariables that are later turned into real variables at the end.

The fix for this is simple: Use explicit universes in this particular theorem. This is an issue with the universe unification strategy, maybe it can be fixed, maybe not, but I still think it is best to let the algorithm handle universe variables where possible, in spite of these rare issues

[Kevin Buzzard]

So you're saying that I should just not worry about this and use Type u instead of Type* for the original theorem? That's fine by me! It's also kind of telling me to go back to using Type u in general.

[Mario Carneiro]

It is my impression that this doesn't happen very often

[Mario Carneiro]

I think if you use variables {R M : Type*} then it will use fresh universe variables, instead of metavariables, which are not susceptible to these spurious unification issues

[Mario Carneiro]

Arguably this is more natural default behavior

[Mario Carneiro]

I'm not sure which of these two is more expected:

variables {A B : Type*}
example : A = B := sorry -- fail
example {A B : Type*} : A = B := sorry -- ok

[Damiano Testa]

Thanks! At the moment, the theorem is stated with the M universe explicit.

[Kevin Buzzard]

If you use variables you can go back to Type*, if you care

[Damiano Testa]

Given that this lemma went in the middle of a file, where there were other conventions about variables, I think that I prefer to leave it as is. Had it been on a file that I started with this purpose in mind, I maybe would not have realized, since I might indeed had R and M declared as variables at the beginning.

[Nick Scheel]

I didn’t quite follow: was the problem determined to be that there were two universe variables that only appeared together as a max u v but never separately?

I think this situation is bound to come up, but if the type theory is parametric over universes it is okay to solve them to be the same variable. (The one I am studying has this property, so I will do that.) But I think in Lean, because you have LEM and things like ordinals and cardinals which change depending on their universe, it is no longer parametric? Correct me if I am wrong.

[Nick Scheel]

Or was the problem that the parts that should have determined the variables were also implicit?

[Kevin Buzzard]

The problem was that an equation which one has to solve using universes was solved in a suboptimal way if you ask the system to solve it in a certain way

[Kevin Buzzard]

Is this related?

Right now on master

import topology.algebra.group

set_option pp.universes true
/-
topological_group.of_nhds_one.{u_1 u_2} :
  ∀ {G : Type (max u_1 u_2)} [_inst_5 : group.{(max u_1 u_2)} G] [_inst_6 : topological_space.{(max u_1 u_2)} G],
    filter.tendsto.{(max u_1 u_2) (max u_1 u_2)}
      (function.uncurry.{(max u_1 u_2) (max u_1 u_2) (max u_1 u_2)} has_mul.mul.{(max u_1 u_2)})
      ((nhds.{(max u_1 u_2)} 1).prod (nhds.{(max u_1 u_2)} 1))
      (nhds.{(max u_1 u_2)} 1) →
    filter.tendsto.{(max u_1 u_2) (max u_1 u_2)} (λ (x : G), x⁻¹) (nhds.{(max u_1 u_2)} 1)
      (nhds.{(max u_1 u_2)} 1) →
    (∀ (x₀ : G),
       nhds.{(max u_1 u_2)} x₀ =
         filter.map.{(max u_1 u_2) (max u_1 u_2)} (λ (x : G), x₀ * x) (nhds.{(max u_1 u_2)} 1)) →
    (∀ (x₀ : G),
       filter.tendsto.{(max u_1 u_2) (max u_1 u_2)} (λ (x : G), x₀ * x * x₀⁻¹) (nhds.{(max u_1 u_2)} 1)
         (nhds.{(max u_1 u_2)} 1)) →
    topological_group.{(max u_1 u_2)} G
All Messages (1)

-/

Changing Type* to Type u in #6647 fixes this issue.

[Mario Carneiro]

yep

[Mario Carneiro]

I think it's tendsto (uncurry ((*) : G → G → G)) that causes the bad unify here

[Bryan Gin-ge Chen]

I've put #6647 on the queue. We should add a library note for this if we find some more examples.

[Kevin Buzzard]

It was flip before IIRC, which is of a similar nature to uncurry.

[Mario Carneiro]

I want to point my finger at expressions like G → G → G, where the type of the implication is something like imax u (imax u u) where u is the sort of G. That simplifies to u when it's a variable, but when that expression appears in stages, where ?u is a metavariable, it's not obvious that it's going to normalize at first. When it is G → H → G when the universes are actually different there is no issue because lean guesses correctly.