Zulip Chat Archive

Stream: general

Topic: error: expected type equals given type


view this post on Zulip Johan Commelin (Jan 15 2019 at 10:47):

A mystery:

type mismatch at application
  functor.on_iso (yoneda.obj F)
term
  yoneda.obj F
has type
  presheaf Xᵒᵖ  Type (max u v)
but is expected to have type
  presheaf Xᵒᵖ  Type (max u v)

Last week @Reid Barton and I encountered a similar error when working on over categories. Back then we could fix it by specifying a universe variable. But that still felt like a hack around a bug. This time universe annotations don't seem to help.

Anyway, I'm more interested in fact that Lean thinks two types are the same, but isn't happy to move on.
Here is the pp.all version:

has type
  @category_theory.functor.{(max u v) (max u v) (max u (v+1)) (max u v)+1}
    (category_theory.op.{(max u (v+1))} (@category_theory.presheaf.{v u} X 𝒳))
    (@category_theory.opposite.{(max u v) (max u (v+1))} (@category_theory.presheaf.{v u} X 𝒳)
       (@category_theory.presheaf.category_theory.category.{v u} X 𝒳))
    (Type (max u v))
    category_theory.types.{(max u v)}
but is expected to have type
  @category_theory.functor.{(max u v) (max u v) (max u (v+1)) (max u v)+1}
    (category_theory.op.{(max u (v+1))} (@category_theory.presheaf.{v u} X 𝒳))
    (@category_theory.opposite.{(max u v) (max u (v+1))} (@category_theory.presheaf.{v u} X 𝒳)
       (@category_theory.presheaf.category_theory.category.{v u} X 𝒳))
    (Type (max u v))
    category_theory.types.{(max u v)}

view this post on Zulip Sebastian Ullrich (Jan 15 2019 at 11:32):

If you have too much time and want to take a closer look, you could try turning on the various defeq traces. Not sure if the output will be of any help.

view this post on Zulip Johan Commelin (Jan 15 2019 at 12:03):

@Sebastian Ullrich I have a bit of time. Do you have a guess about what's going on? Are you interested in those traces? How do I turn them on?

view this post on Zulip Sebastian Ullrich (Jan 15 2019 at 12:07):

It should be trace.type_context.is_def_eq and trace.type_context.is_def_eq_detail. I can take a look, though I won't promise anything :) .

view this post on Zulip Johan Commelin (Jan 15 2019 at 12:09):

Output of trace.type_context.is_def_eq:

[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] category ?m_1 =?= category ?m_1 ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] category ?m_1 =?= category ?m_1 ... success  (approximate mode)
[type_context.is_def_eq] ?m_1  ?m_1ᵒᵖ  Type ? =?= ?m_3  ?m_5 ... success  (approximate mode)
[type_context.is_def_eq] ?m_1  ?m_3 =?= ?m_5 ... success  (approximate mode)
[type_context.is_def_eq] presheaf X =?= ?m_1 ... success  (approximate mode)
[type_context.is_def_eq] presheaf X =?= ?m_1 ... success  (approximate mode)
[type_context.is_def_eq] ?m_1 =?= F ... success  (approximate mode)
[type_context.is_def_eq] ?m_1 =?= ?m_2  ?m_4 ... failed  (approximate mode)
[type_context.is_def_eq] ?m_1 =?= presheaf.category_theory.category ... success  (approximate mode)
[type_context.is_def_eq] ?m_1 =?= presheaf.category_theory.category ... success  (approximate mode)
[type_context.is_def_eq] category_theory.types =?= category_theory.types ... success  (approximate mode)
[type_context.is_def_eq] category_theory.opposite =?= category_theory.opposite ... success  (approximate mode)
[type_context.is_def_eq] functor.category presheaf Xᵒᵖ (Type (max u v)) =?= functor.category presheaf Xᵒᵖ (Type (max u v)) ... success  (approximate mode)
[type_context.is_def_eq] ?x_1 =?= presheaf Xᵒᵖ  Type (max u v) ... success  (approximate mode)
[type_context.is_def_eq] ?x_0 =?= presheaf Xᵒᵖ  Type (max u v) ... success  (approximate mode)

view this post on Zulip Johan Commelin (Jan 15 2019 at 12:10):

Output of trace.type_context.is_def_eq_detail:

[type_context.is_def_eq_detail] [1]: ?m_1  ?m_1ᵒᵖ  Type ? =?= ?m_3  ?m_5
[type_context.is_def_eq_detail] [2]: functor =?= functor
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] [2]: category ?m_1 =?= category ?m_2
[type_context.is_def_eq_detail] [3]: category =?= category
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2ᵒᵖ  Type ?
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2ᵒᵖ  Type ?
[type_context.is_def_eq_detail] process_assignment ?m_1 := functor.category ?m_2ᵒᵖ (Type ?)
[type_context.is_def_eq_detail] [2]: category ?m_1 =?= category (?m_2ᵒᵖ  Type ?)
[type_context.is_def_eq_detail] [3]: category =?= category
[type_context.is_def_eq_detail] assign: ?m_1 := functor.category ?m_2ᵒᵖ (Type ?)
[type_context.is_def_eq_detail] [1]: ?m_1  ?m_3 =?= ?m_5ᵒᵖ  Type ?
[type_context.is_def_eq_detail] [2]: functor =?= functor
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2ᵒᵖ
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2ᵒᵖ
[type_context.is_def_eq_detail] process_assignment ?m_1 := category_theory.opposite
[type_context.is_def_eq_detail] [2]: category ?m_1 =?= category ?m_2ᵒᵖ
[type_context.is_def_eq_detail] [3]: category =?= category
[type_context.is_def_eq_detail] assign: ?m_1 := category_theory.opposite
[type_context.is_def_eq_detail] process_assignment ?m_1 := Type ?
[type_context.is_def_eq_detail] assign: ?m_1 := Type ?
[type_context.is_def_eq_detail] process_assignment ?m_1 := category_theory.types
[type_context.is_def_eq_detail] [2]: category ?m_1 =?= large_category (Type ?)
[type_context.is_def_eq_detail] unfold right: category_theory.large_category
[type_context.is_def_eq_detail] [3]: category ?m_1 =?= category (Type ?)
[type_context.is_def_eq_detail] [4]: category =?= category
[type_context.is_def_eq_detail] assign: ?m_1 := category_theory.types
[type_context.is_def_eq_detail] process_assignment ?m_1 := presheaf X
[type_context.is_def_eq_detail] assign: ?m_1 := presheaf X
[type_context.is_def_eq_detail] process_assignment ?m_1 := F
[type_context.is_def_eq_detail] assign: ?m_1 := F
[type_context.is_def_eq_detail] [1]: presheaf Xᵒᵖ  Type ? =?= ?m_2  ?m_4
[type_context.is_def_eq_detail] [2]: functor =?= functor
[type_context.is_def_eq_detail] [2]: category_theory.opposite =?= category_theory.opposite
[type_context.is_def_eq_detail] [2]: category_theory.types =?= category_theory.types
[type_context.is_def_eq_detail] on failure: presheaf Xᵒᵖ  Type ? =?= ?m_2  ?m_4
[type_context.is_def_eq_detail] process_assignment ?m_1 := presheaf.category_theory.category
[type_context.is_def_eq_detail] [1]: category ?m_1 =?= category (presheaf X)
[type_context.is_def_eq_detail] [2]: category =?= category
[type_context.is_def_eq_detail] assign: ?m_1 := presheaf.category_theory.category
[type_context.is_def_eq_detail] [1]: category_theory.types =?= category_theory.types
[type_context.is_def_eq_detail] [1]: category_theory.opposite =?= category_theory.opposite
[type_context.is_def_eq_detail] process_assignment ?x_1 := presheaf Xᵒᵖ  Type (max u v)
[type_context.is_def_eq_detail] assign: ?x_1 := presheaf Xᵒᵖ  Type (max u v)
[type_context.is_def_eq_detail] process_assignment ?x_0 := presheaf Xᵒᵖ  Type (max u v)
[type_context.is_def_eq_detail] assign: ?x_0 := presheaf Xᵒᵖ  Type (max u v)

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:14):

what does convert yoneda F give?

view this post on Zulip Johan Commelin (Jan 15 2019 at 12:14):

The error is in a have statement...

have := @functor.on_iso _ _ _ _ (yoneda.obj F),

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:15):

can you fill in the underscores?

view this post on Zulip Johan Commelin (Jan 15 2019 at 12:15):

I'll try. Give me a second.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:16):

also your op has a really confusing precedence

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:16):

there is no way lean can parse presheaf Xᵒᵖ means (presheaf X)ᵒᵖ but the printer seems to think so

view this post on Zulip Johan Commelin (Jan 15 2019 at 12:17):

have := @functor.on_iso ((presheaf X)ᵒᵖ) _ _ _ (yoneda.obj F),

Wow... this works...

view this post on Zulip Reid Barton (Jan 15 2019 at 12:24):

there is no way lean can parse presheaf Xᵒᵖ means (presheaf X)ᵒᵖ but the printer seems to think so

I thought this was actually possible by using a precedence above 1000?

view this post on Zulip Reid Barton (Jan 15 2019 at 12:25):

I was wondering whether we should do that

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:26):

I think you want high precedence (above max = 1024) to get presheaf Xᵒᵖ = presheaf (Xᵒᵖ)

view this post on Zulip Reid Barton (Jan 15 2019 at 12:27):

Oh, I misread

view this post on Zulip Reid Barton (Jan 15 2019 at 12:27):

What you just wrote is what I want

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:28):

most postfix notations are at precedence :max+1 for this reason

view this post on Zulip Kevin Buzzard (Jan 15 2019 at 12:28):

Has this fixed the error Johan?

view this post on Zulip Reid Barton (Jan 15 2019 at 12:28):

I'm not really sure how it works now actually. But I know there are a lot of parentheses in category_theory that look like they ought to be unnecessary

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:28):

I doubt it addresses the error though, I'm still perplexed

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:29):

it seems like it's an elaboration order issue

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:31):

what's up with this name? category_theory.presheaf.category_theory.category

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:31):

just in case you forgot it's about categories

view this post on Zulip Reid Barton (Jan 15 2019 at 12:35):

Just wait until we have the category of categories

view this post on Zulip Reid Barton (Jan 15 2019 at 12:36):

or the category of theories

view this post on Zulip Chris Hughes (Jan 15 2019 at 12:37):

or the category of theories

Is that a thing?

view this post on Zulip Johan Commelin (Jan 15 2019 at 12:39):

I still don't understand the error.
But I no longer need a solution, because I proved it differently.

view this post on Zulip Johan Commelin (Jan 15 2019 at 12:39):

It's just weird that this shows up. And like I said: Reid and I had a similar thing last week when we worked with over categories.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 12:41):

is that a thing?

Sure, you can use interpretations as morphisms between theories even with different languages

view this post on Zulip Reid Barton (Jan 16 2019 at 11:48):

I think you want high precedence (above max = 1024) to get presheaf Xᵒᵖ = presheaf (Xᵒᵖ)

Implemented at https://github.com/leanprover/mathlib/pull/600 (@Johan Commelin FYI)

view this post on Zulip Johan Commelin (Jan 16 2019 at 12:04):

@Reid Barton Thanks!


Last updated: May 15 2021 at 23:13 UTC