[Merged by Bors] - chore: remove many `Type _` before the colon by sgouezel · Pull Request #7718 · leanprover-community/mathlib4

sgouezel · 2023-10-16T18:23:25Z

We have turned to Type* instead of Type _, but many of them remained in mathlib because the straight replacement did not work. In general, having Type _ before the colon is a code smell, though, as it hides which types should be in the same universe and which shouldn't, and is not very robust.

This PR replaces most of the remaining Type _ before the colon (except those in category theory) by Type* or Type u. This has uncovered a few bugs (where declarations were not as polymorphic as they should be).

I had to increase heartbeats at two places when replacing Type _ by Type*, but I think it's worth it as it's really more robust.

sgouezel · 2023-10-16T18:24:03Z

Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean

 #align simply_connected_space.paths_homotopic SimplyConnectedSpace.paths_homotopic

-instance (priority := 100) ofContractible (Y : Type _) [TopologicalSpace Y] [ContractibleSpace Y] :
+instance (priority := 100) ofContractible (Y : Type u) [TopologicalSpace Y] [ContractibleSpace Y] :


With the old proof, Type _ expanded to just Type !!

sgouezel · 2023-10-16T18:26:31Z

Mathlib/Analysis/NormedSpace/Ray.lean

 theorem norm_sub (h : SameRay ℝ x y) : ‖x - y‖ = |‖x‖ - ‖y‖| := by
  rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
-  wlog hab : b ≤ a with H
+  wlog hab : b ≤ a generalizing a b with H


The old proof used the universe in {F : Type _} (where F is a variable not appearing in the theorem statement) in the wlog generalization, to match it with that of ℝ! (so replacing {F : Type _} with {F : Type*} broke the proof for dark magic reasons)

sgouezel · 2023-10-16T18:27:40Z

Mathlib/Algebra/Module/LocalizedModule.lean

-set_option maxHeartbeats 400000 in
-instance {A : Type _} [Semiring A] [Algebra R A] {S : Submonoid R} :
+set_option maxHeartbeats 500000 in
+instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} :


The type of the instance is the same with Type _ or Type* (so no added generality here), but it is just slightly slower with Type*...

I think @semorrison advocated that we should stick to powers of two bump factors rather than small bumps like this

In the end I think it was powers of 1.2 or 1.3, I think, so coherent with what I've done here.

sgouezel · 2023-10-16T18:30:37Z

Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean


 variable [CompactSpace X]

+set_option synthInstance.maxHeartbeats 30000 in


The proof is slightly slower with Type* than with Type _, although the statements are the same in the end...

eric-wieser · 2023-10-17T05:55:31Z

Mathlib/Data/Option/Basic.lean

 #align option.join_eq_join Option.joinM_eq_join

-theorem bind_eq_bind {α β : Type _} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=
+theorem bind_eq_bind {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=


Another reasonable option for these rare declarations is

Suggested change

theorem bind_eq_bind {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=

theorem bind_eq_bind.{u} {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=

or

Suggested change

theorem bind_eq_bind {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=

universe u in

theorem bind_eq_bind {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=

to keep the universe local

Thanks for the suggestions!

eric-wieser

bors d+

Thanks! I thought about doing this the other day, but struggled to justify the effort to do so!

eric-wieser · 2023-10-17T05:57:39Z

Mathlib/RingTheory/RingHomProperties.lean

-theorem RespectsIso.is_localization_away_iff (hP : RingHom.RespectsIso @P) {R S : Type _}
-    (R' S' : Type _) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R']
+theorem RespectsIso.is_localization_away_iff (hP : RingHom.RespectsIso @P) {R S : Type u}
+    (R' S' : Type u) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R']


This looks slightly suspicious to me; is there really no polymorphism here?

Yes. P only makes sense for rings in the given universe u, and the conclusion mentions P applied both to R, S and to R', S'.

bors · 2023-10-17T05:58:59Z

✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

sgouezel · 2023-10-17T08:28:40Z

bors r+

We have turned to `Type*` instead of `Type _`, but many of them remained in mathlib because the straight replacement did not work. In general, having `Type _` before the colon is a code smell, though, as it hides which types should be in the same universe and which shouldn't, and is not very robust. This PR replaces most of the remaining `Type _` before the colon (except those in category theory) by `Type*` or `Type u`. This has uncovered a few bugs (where declarations were not as polymorphic as they should be). I had to increase heartbeats at two places when replacing `Type _` by `Type*`, but I think it's worth it as it's really more robust.

bors · 2023-10-17T10:35:44Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

sgouezel added 11 commits October 14, 2023 08:26

start

1d5cf99

further cleanup

c0943e8

fix?

49d0d54

progress

685f685

more fixes

671d49d

fix

064fa61

Merge remote-tracking branch 'origin/master' into SG_clean_Type_

122225c

progress

30c3087

fix

8ab9fd6

more examples

7978eb2

cleanup

6187af7

sgouezel added the awaiting-review label Oct 16, 2023

sgouezel commented Oct 16, 2023

View reviewed changes

eric-wieser reviewed Oct 17, 2023

View reviewed changes

eric-wieser approved these changes Oct 17, 2023

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Oct 17, 2023

github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 17, 2023

bors bot changed the title ~~chore: remove many Type _ before the colon~~ [Merged by Bors] - chore: remove many Type _ before the colon Oct 17, 2023

bors bot closed this Oct 17, 2023

bors bot deleted the SG_clean_Type_ branch October 17, 2023 10:35


		variable [CompactSpace X]

		set_option synthInstance.maxHeartbeats 30000 in

	theorem bind_eq_bind {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=
	theorem bind_eq_bind.{u} {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=

	theorem bind_eq_bind {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=
	universe u in
	theorem bind_eq_bind {α β : Type u} {f : α → Option β} {x : Option α} : x >>= f = x.bind f :=

Conversation

sgouezel commented Oct 16, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

sgouezel Oct 16, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

bors bot commented Oct 17, 2023

Uh oh!

sgouezel commented Oct 17, 2023

Uh oh!

bors bot commented Oct 17, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

sgouezel Oct 16, 2023 •

edited

Loading