I ran this program, and was very surprised that it type checked:
def A : Type := sorry
def B : Type := sorry
def f (a : A) : B := a
That seems wrong, why does it work?
The reason why this works is that sorry in both cases is short for sorryAx Type false, and it's the case that sorryAx Type false is definitionally equal to sorryAx Type false (they are identical). You should think of sorryAx as being sort of like a version of the axiom of choice — it picks out some unknown term of the type, but it's always the same unknown term.
However, in the next Lean release this behavior is changing due to #5757. Example:
def f (a : A) : B := a
/- ~~~
type mismatch
a
has type
A : Type
but is expected to have type
B : Type
-/
The difference is that sorry now creates a term that contains a unique token. It still pretty prints as sorry by default, but with a change to the pretty printer options the difference is evident:
set_option pp.explicit true
#print A
/-
def A : Type :=
sorryAx (Name → Type) false `lean.foo.12.16.12.21.16.21._sorry._@.lean.foo._hyg.123
-/
#print B
/-
def B : Type :=
sorryAx (Name → Type) false `lean.foo.13.16.13.21.16.21._sorry._@.lean.foo._hyg.128
-/
The trick is that the sorry is parameterized by a Lean.Name that encodes the token. Since the tokens are different, this allows sorryAx to choose "different" terms from Type. (More accurately, there could be a model where sorryAx chooses the same Type in both cases, but there's another model where it chooses different Types, so not only are A and B not defeq, but whether A is equal to B is unprovable one way or the other.)
The unique token encodes both a unique part as well as source position information. The source position lets you figure out where a sorry came from, either through doing a "go to definition" in the Infoview, or perhaps through some metaprogramming to find where all the unfinished results for a given theorem might be.
The motivation for this feature is that it is dangerous for a large formalization project to use the old version of sorry to stub out definitions. It lets you easily prove fake theorems that will become false once the sorry is replaced with the actual definition. With the new sorry, you can write
def g : Nat → Nat := sorry
and feel safe that no one will prove it is equal to anything else.
Word of warning, you must write it like that rather than
def g (n : Nat) : Nat := sorry
since this defines a constant function.
example : ∀ (m n : Nat), g m = g n := by intros; rfl