Sorry of wrong type!

Stream: general

[Moses Schönfinkel]

Heh...

type mismatch at field 'le_refl'
  sorry
has type
  ∀ (a : α), ?m_1 a a
but is expected to have type
  ∀ (a : α), a ≤ a

[Mario Carneiro]

did you put sorry for the definition of le as well?

[Mario Carneiro]

le := _, le_refl := sorry will error

[Moses Schönfinkel]

Yes :). I just sorried everything to build it incrementally, I know I don' goof'd, it's just amusing that sorry can actually fail to typecheck.

[Moses Schönfinkel]

Indeed! :)

[Moses Schönfinkel]

It's the first time I've seen sorry being red-squiggled in Lean

[Mario Carneiro]

I think it is having difficulty unifying the types, this would happen also if you tried to use something of type \forall {x : Type*}. x

[Moses Schönfinkel]

So I guess sorry first needs to know the type and then gives you a bogus term thereof, rather than just "closing the goal" as if by magic? Would the latter behaviour lead to weirdness in scenarios where something depends on a (presumably temporary) sorry?

[Mario Carneiro]

I think the problem has to do with unresolved metavariables in the type

[Mario Carneiro]

You should always be able to sorry everything, but you have to work from the beginning, from the nondependent sorrys to the dependent ones

[Moses Schönfinkel]

Right. It's just interesting that sorry cares about anything at all :)! So for example, { le := sorry, le_refl := sorry ... } would work but { le := _, le_refl := sorry ... } would not.

[Kevin Buzzard]

I got sorry red-squiggled about 2 weeks ago, for probably the first time. I awarded myself an achievement.

[Mario Carneiro]

It's like the dual problem of proving an inconsistency :)

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/too.20many.20axioms.20in.20comm_ring.20class/near/123391025