Zulip Chat Archive

Stream: general

Topic: bug with typeclasses


view this post on Zulip Kenny Lau (Mar 07 2018 at 19:30):

Forgive me for not minimizing:

instance structure_presheaf_value_has_zero {R : Type*} [comm_ring R] (U : set (X R)) (HU : is_open U) :
  has_zero (structure_presheaf_value U HU) :=
⟨⟨λ P HP, 0, sorry⟩⟩
#check λ {R : Type*} [comm_ring R] (U : set (X R)) (HU : is_open U), (by apply_instance : has_zero (structure_presheaf_value U HU))

Here the #check succeeds with this trace:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_zero (@structure_presheaf_value R _inst_1 U HU) := @structure_presheaf_value_has_zero ?x_1 ?x_2 ?x_3 ?x_4
[class_instances] (1) ?x_2 : comm_ring R := _inst_1

instance structure_presheaf_value_has_zero {R : Type*} [comm_ring R] (U : set (X R)) (HU : is_open U) :
  has_zero (structure_presheaf_value U HU) :=
⟨⟨λ P HP, 0, λ u hu,
let ⟨V, ⟨f, hf⟩, huV, hVU⟩ := (D_f_form_basis R).2 U HU u hu in
⟨f, hf ▸ huV, hf ▸ hVU, 0, λ Q hQ h2, eq.symm $ is_ring_hom.map_zero _⟩⟩⟩
#check λ {R : Type*} [comm_ring R] (U : set (X R)) (HU : is_open U), (by apply_instance : has_zero (structure_presheaf_value U HU))

Here the #check fails with the following trace:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_zero (@structure_presheaf_value R _inst_1 U HU) := @structure_presheaf_value_has_zero ?x_1 ?x_2 ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : has_zero (@structure_presheaf_value R _inst_1 U HU) := rat.has_zero
failed is_def_eq
[... more shenanigans ...]

But if I change the last line to:

#check λ {R : Type*} [comm_ring R] (U : set (X R)) (HU : is_open U), (structure_presheaf_value_has_zero U HU : has_zero (structure_presheaf_value U HU))

Then it succeeds with the following trace:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : comm_ring R := _inst_1

any idea why?

view this post on Zulip Simon Hudon (Mar 07 2018 at 19:56):

Can you show the definition of structure_resheaf_value along with any attributes it may have?

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:01):

definition structure_presheaf_value {R : Type*} [comm_ring R] (U : set (X R)) (HU : is_open U) :=
(structure_presheaf_of_types_on_affine_scheme R).F U HU

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:02):

and then instance structure_presheaf_value_has_add {R : Type*} [comm_ring R] (U : set (X R)) (HU : is_open U) : has_add (structure_presheaf_value U HU) :=...

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:02):

and instance structure_presheaf_value_has_neg, mul , zero and one.

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:25):

Structures drive me nuts.

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:26):

I see different behaviour if I set mul := [long definition]

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:26):

to if I make the long definition outside and let mul be that.

view this post on Zulip Kenny Lau (Mar 07 2018 at 20:28):

https://github.com/kbuzzard/lean-stacks-project/blob/708d11f6afbcffb0fd552cd7087100a1400fe40d/src/scheme.lean
most of the things are here

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:37):

OK so we have a workaround

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:38):

  mul_assoc := λ _ _ _,subtype.eq (funext (λ _,funext (λ _,mul_assoc _ _ _))),
  add_assoc := λ _ _ _,subtype.eq (funext (λ _,funext (λ _,add_assoc _ _ _))),
  zero_add := λ _,subtype.eq (funext (λ _,funext (λ _,zero_add _))),

view this post on Zulip Kevin Buzzard (Mar 07 2018 at 20:38):

and so on and so on

view this post on Zulip Kenny Lau (Mar 08 2018 at 19:17):

@Mario Carneiro could you have a look?


Last updated: May 07 2021 at 00:30 UTC