`Sort _` の厄介な点、`Sort*` の利点

Sort _ のユニバースレベル自動推論について

Lean で Sort _ や Type _ と書くと、
Lean はその _ の部分、つまりユニバースレベルを自動で決めてくれるの。

でもね、これが思ったより狭く（具体的に）決まっちゃうことがあるの。

例：

import Mathlib.Data.Countable.Defs

example (α : Sort _) (x y : α) (_ : Countable α := inferInstance) : x = y := by
  rfl

このコードでは、
inferInstance が Prop.countable を見つけてしまうので、
Sort _ の α が Prop に限定されちゃうんだ。

つまり、α : Prop になって、x : α と y : α は証明の無差別性（proof irrelevance）により定義的に等しい（＝同じもの）と見なされるよ。

もっと古い Lean バージョンの例

Lean 4.8.0 などの昔のバージョンだと、こういう書き方でさらに起こりやすかった：

example {α : Sort _} (x y : α) : x = y := by
  have := α ∧ α -- α を Prop に強制
  rfl

α が Prop になるように強制しているね。

だからどうすればいいの？

こういう予期しないユニバースレベルの縮小を防ぐために、

• Sort _ や Type _ のかわりに、
• Sort* や Type* を使うのがオススメ！

Sort* と Type* は、使うたびに新しいユニバースパラメータを強制的に作るので、
ユニバースレベルが不意に狭まるのを防げるよ。

または、

• ユニバースレベルを明示的に指定してしまうのも手だよ。

The issue names no repository file, test, or entry point. First identify where Lean language examples and explanatory pages are maintained, then use the supplied Sort _ and Sort* examples as the proposed scope. The work is done when the explanation and recommendation are placed in the appropriate documentation location and rendered correctly.