Lean 3.36

Stream: general

[Yury G. Kudryashov]

Hi,
The branch#YK-pointwise builds with lean<3.36 and fails to build with lean 3.36 (git bisect points to 60e279ba2b as the "bad" commit). What were the backwards-incompatible changes in lean-3.36?

[Yury G. Kudryashov]

With 3.36 it fails at this line

[Anne Baanen]

It wouldn't surprise me if it was my commit allowing the elaborator to proceed a bit further in the presence of out_param.

[Anne Baanen]

Do you have a version of your branch updated to the new 3.36 syntax?

[Anne Baanen]

Alright, doing it myself wasn't too bad: branch#YK-pointwise-3.36-bump

[Anne Baanen]

The error with trace.type_context.is_def_eq_detail and trace.class_instances:

failed to synthesize type class instance for
F : Type u_1,
ι : out_param (Type u_2),
α : out_param (ι → Type u_3),
_inst_1 : Π (i : ι), comm_monoid (α i),
_inst_2 : fun_like F ι α,
_inst_3 :
  @has_pointwise_one F ι α
    (λ (i : ι),
       @mul_one_class.to_has_one (α i) (@monoid.to_mul_one_class (α i) (@comm_monoid.to_monoid (α i) (_inst_1 i))))
    _inst_2,
_inst_4 :
  @has_pointwise_mul F ι α
    (λ (i : ι),
       @mul_one_class.to_has_mul (α i) (@monoid.to_mul_one_class (α i) (@comm_monoid.to_monoid (α i) (_inst_1 i))))
    _inst_2,
_inst_5 :
  @has_pointwise_pow F ι α ℕ (λ (i : ι), @monoid.has_pow (α i) (@comm_monoid.to_monoid (α i) (_inst_1 i)))
    _inst_2
⊢ @has_pointwise_mul F ι α
    (λ (i : ι), @semigroup.to_has_mul (α i) (@comm_semigroup.to_semigroup (α i) (?m_1 i)))
    _inst_2
▶ 173:6-173:7: information:
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_4 : @has_pointwise_mul F ?x_0 ?x_1 ?x_2 ?x_3 := _inst_4
[type_context.is_def_eq_detail] [1]: @has_pointwise_mul F ?x_0 ?x_1 ?x_2 ?x_3 =?= @has_pointwise_mul F ?m__fresh.290.38668 ?m__fresh.290.38669 ?m__fresh.290.38670 _inst_2
[...]
[class_instances] caching instance for @has_pointwise_mul F ι α
  (λ (i : ι),
     @mul_one_class.to_has_mul (α i) (@monoid.to_mul_one_class (α i) (@comm_monoid.to_monoid (α i) (_inst_1 i))))
  _inst_2
_inst_4
[type_context.is_def_eq_detail] [1]: @semigroup.to_has_mul (α i) (@comm_semigroup.to_semigroup (α i) (?m_1 i)) =?= @mul_one_class.to_has_mul (α i) (@monoid.to_mul_one_class (α i) (@comm_monoid.to_monoid (α i) (_inst_1 i)))
[type_context.is_def_eq_detail] [2]: @has_mul.mk (α i) (@semigroup.mul (α i) (@comm_semigroup.to_semigroup (α i) (?m_1 i))) =?= @has_mul.mk (α i)
  (@mul_one_class.mul (α i) (@monoid.to_mul_one_class (α i) (@comm_monoid.to_monoid (α i) (_inst_1 i))))
[type_context.is_def_eq_detail] [3]: @semigroup.mul (α i) (@comm_semigroup.to_semigroup (α i) (?m_1 i)) =?= @mul_one_class.mul (α i) (@monoid.to_mul_one_class (α i) (@comm_monoid.to_monoid (α i) (_inst_1 i)))
[type_context.is_def_eq_detail] [4]: @comm_semigroup.mul (α i) (?m_1 i) =?= @monoid.mul (α i) (@comm_monoid.to_monoid (α i) (_inst_1 i))
[type_context.is_def_eq_detail] [5]: @comm_semigroup.mul (α i) (?m_1 i) =?= @comm_monoid.mul (α i) (_inst_1 i)
[type_context.is_def_eq_detail] [6]: comm_semigroup.mul =?= comm_monoid.mul
[type_context.is_def_eq_detail] on failure: comm_semigroup.mul =?= comm_monoid.mul
[type_context.is_def_eq_detail] on failure: @comm_semigroup.mul (α i) (?m_1 i) =?= @comm_monoid.mul (α i) (_inst_1 i)
[type_context.is_def_eq_detail] on failure: @has_mul.mk (α i) (@semigroup.mul (α i) (@comm_semigroup.to_semigroup (α i) (?m_1 i))) =?= @has_mul.mk (α i)
  (@mul_one_class.mul (α i) (@monoid.to_mul_one_class (α i) (@comm_monoid.to_monoid (α i) (_inst_1 i))))

[Anne Baanen]

So what's going on is that the comm_semigroup instance found on the right hand side isn't being used to solve the metavariable ?m_1 on the left, when checking that the has_pointwise_mul F instance is compatible with the context of its application.

[Anne Baanen]

Self-contained example of the unification failure:

example [Π i, comm_monoid (α i)] [fun_like F ι α] [has_pointwise_one F] [h : has_pointwise_mul F]
  [has_pointwise_pow F ℕ] : true :=
begin
  -- Create a new metavariable for the instance instead of inferring it
  let X : Π i, comm_semigroup (α i) := _, /- works with: λ i, (@@comm_monoid.to_comm_semigroup _ (id _)), -/
  have : @has_pointwise_mul F ι _ (λ i, @semigroup.to_has_mul (α i) (@comm_semigroup.to_semigroup (α i) (X i))) _,
  exact h, -- type error
  trivial
end

[Anne Baanen]

If I understand the unification process correctly, what should happen is that the ?m_1 metavariable is inferred, and then we can project out all the structures and show equality. Instead it remains a metavariable, the projection can't be unfolded past comm_semigroup.mul _ _ which is not defeq to comm_monoid.mul _ _ and we give up.

[Yury G. Kudryashov]

Is it easy to fix?

[Anne Baanen]

I have no big-picture overview of the unifier, so fixing Lean is pretty hard. Working around the missing instance error is not too hard, if we manipulate the elaboration order a bit:

@[to_additive]
instance [Π i, comm_monoid (α i)] [fun_like F ι α] [has_pointwise_one F] [has_pointwise_mul F]
  [has_pointwise_pow F ℕ] :
  comm_monoid F :=
{ .. fun_like.monoid F, .. @@fun_like.comm_semigroup F _ _ (by apply_instance) }

or here we can also use assumption instead of apply_instance:

@[to_additive]
instance [Π i, comm_monoid (α i)] [fun_like F ι α] [has_pointwise_one F] [has_pointwise_mul F]
  [has_pointwise_pow F ℕ] :
  comm_monoid F :=
{ .. fun_like.monoid F, .. @@fun_like.comm_semigroup F _ _ ‹_› }

[Anne Baanen]

For example, commit 0a86527548