Type typo

Stream: mathlib4

[Joris van Winden]

I ran into a universe issue when trying to apply gaussianReal_neg:

In Probability.Distributions.Gaussian.Real, line 350 states:

variable {Ω : Type} {mΩ : MeasurableSpace Ω} {P : Measure Ω} {X : Ω → ℝ}

Should Type be changed Type* here? More generally, how can I determine whether an instance of Type should actually be Type*?

[Rémy Degenne]

Yes it should be Type*. This is a clear typo. Everything should use Type*, unless there is a good reason for Type (and I never encounter any in probability files).

[Rémy Degenne]

Please make a PR!

[Johan Commelin]

I think assumptions should never use Type in Mathlib.
In proofs, and as return types, there can be good uses for Type.

[Joris van Winden]

Is this something which could be caught by a linter (possibly restricted to certain folders)?

To illustrate: when searching for : Type} in VSCode, I get 341 results in 140 files. Most are in CategoryTheory, but there are also some in e.g. Analysis/Specialfunctions/ExpDeriv, Analysis/Fourier/AddCircle, MeasureTheory/Measure/WithDensity where I suspect it should be Type* instead.

[Joris van Winden]

I guess as long as there are not too many it can be handled on a case by case basis.

[Kevin Buzzard]

Johan Commelin said:

I think assumptions should never use Type in Mathlib.
In proofs, and as return types, there can be good uses for Type.

In parts of representation theory you have to have k and G or G and M in the same universe, and then if one of them is the integers or complexes...

[Joris van Winden]

#35049

[Michael Rothgang]

Good catch! #35053 fixes MeasureTheory/Measure/WithDensity,

[Michael Rothgang]

#35054 fixes Analysis