# Zulip Chat Archive

## Stream: new members

### Topic: Unexpected type error in equality proposition

#### Kevin Sullivan (Feb 24 2019 at 02:28):

set_option pp.all true

#reduce eq.refl 0

#reduce eq.refl (1-1)

#check (eq.refl 0) = (eq.refl 0) -- this works

#check (eq.refl 0) = (eq.refl (1-1)) -- type error!>?<!

Why>

#### Andrew Ashworth (Feb 24 2019 at 04:15):

this also works: `#check (eq.refl (0)) = (eq.refl ((1 - 1):ℕ))`

#### Andrew Ashworth (Feb 24 2019 at 04:16):

Unfortunately I don't know why it needs a type ascription

#### Kevin Buzzard (Feb 24 2019 at 08:43):

Is it because Lean doesn't know what that zero is? It's just `has_zero.zero`

until you tell it that it's nat's zero

#### Kevin Sullivan (Feb 24 2019 at 16:13):

Or that it doesn't know what that (1-1) is? The preceding lines seem to indicate that all the terms really are equal, so this result is a bit mystifying.

#### Mario Carneiro (Feb 24 2019 at 16:50):

It's an elaborator order problem, as usual. For `eq.refl a = eq.refl b`

to typecheck, `a`

and `b`

must be defeq. These both work:

#check (eq.refl 0) = (eq.refl 0) #check (eq.refl (1-1)) = (eq.refl (1-1))

because lean knows that (0:A) == 0 definitionally and similarly for (1-1:A) == (1-1:A). In particular, it doesn't need to know that `A = nat`

for this to work. Now having successfully elaborated the term, it knows that the statement is `(eq.refl (0:?m)) = (eq.refl 0)`

, and so since there is a numeral with unknown type, lean does its late `nat`

defaulting, setting `?m = nat`

, inferring the typeclass args, and you get what you see in the pp.all.

In the case ` (eq.refl 0) = (eq.refl (1-1))`

, it doesn't work out so well. Lean tries to check `(0:A) =?= 1-1`

, and this fails, because in an arbitrary type with subtraction and 0 and 1 this doesn't necessarily hold by definition. So it fails right here, and never gets to the nat fallback.

#### Mario Carneiro (Feb 24 2019 at 16:52):

The moral of the story: don't trust nat defaulting. It's a convenience so that `#eval 1 + 1`

does what you expect. You should really think of these terms as having unknown type.

#### Kenny Lau (Feb 24 2019 at 16:54):

I think the correct answer is, what on earth are you doing with `(eq.refl 0) = (eq.refl (1-1))`

#### Kevin Sullivan (Feb 26 2019 at 18:19):

Mario, Thank you very much. That's was a very helpful answer. I had to read it a few times, but now I understand.

Kenny, Ha ha. I'm teaching early undergraduates students (400 of them) discrete math using Lean. One of them was dutifully exploring applications of the various principles I've taught them, tried out the example here, and was mystified by the answer.

Last updated: May 13 2021 at 19:20 UTC