let fails with coe_sort

Stream: general

[Eric Wieser]

What's going on here?

import algebra.algebra.subalgebra

variables (R A : Type*) [comm_semiring R] [semiring A] [algebra R A]

example (s : subalgebra R A) : true := begin
  -- invalid definev tactic, value has type
  --   {x // x ∈ has_coe_t_aux.coe s}
  -- but is expected to have type
  --   s
  let x : s := ⟨0, _⟩,
end

[Anne Baanen]

I tend to have these kinds of issues when reduction gets stuck on a metavariable. Do you have pp.all output?

[Anne Baanen]

Got it:

invalid definev tactic, value has type
  @subtype.{u_2+1} A
    (λ (x : A),
       @has_mem.mem.{u_2 u_2} A
         (@submodule.{u_1 u_2} R A (@comm_semiring.to_semiring.{u_1} R _inst_1)
            (@semiring.to_add_comm_monoid.{u_2} A _inst_2)
            (@algebra.to_semimodule.{u_1 u_2} R A _inst_1 _inst_2 _inst_3))
         (@submodule.has_mem.{u_1 u_2} R A (@comm_semiring.to_semiring.{u_1} R _inst_1)
            (@semiring.to_add_comm_monoid.{u_2} A _inst_2)
            (@algebra.to_semimodule.{u_1 u_2} R A _inst_1 _inst_2 _inst_3))
         x
         (@has_coe_t_aux.coe.{u_2+1 u_2+1} (@subalgebra.{u_1 u_2} R A _inst_1 _inst_2 _inst_3)
            (@submodule.{u_1 u_2} R A (@comm_semiring.to_semiring.{u_1} R _inst_1)
               (@semiring.to_add_comm_monoid.{u_2} A _inst_2)
               (@algebra.to_semimodule.{u_1 u_2} R A _inst_1 _inst_2 _inst_3))
            (@coe_base_aux.{u_2+1 u_2+1} (@subalgebra.{u_1 u_2} R A _inst_1 _inst_2 _inst_3)
               (@submodule.{u_1 u_2} R A (@comm_semiring.to_semiring.{u_1} R _inst_1)
                  (@semiring.to_add_comm_monoid.{u_2} A _inst_2)
                  (@algebra.to_semimodule.{u_1 u_2} R A _inst_1 _inst_2 _inst_3))
               (@subalgebra.coe_to_submodule.{u_1 u_2} R A _inst_1 _inst_2 _inst_3))
            s))
but is expected to have type
  s

[Anne Baanen]

Aha, so let just doesn't realize it has to turn s into coe_sort s.

[Anne Baanen]

As a workaround, you can do:

  let x : coe_sort s := ⟨0, _⟩,
-- or
  let x : (s : Sort*) := ⟨0, _⟩,

[Anne Baanen]

Looks like assertv_definev_core just infers the type of v (here ⟨0, _⟩), checks for defeq with t (here s), and errors if they are not equal. Let me see if I can convince it to coerce t to a sort.

[Eric Wieser]

let x : ↥s seems to work too

[Anne Baanen]

Eric Wieser said:

let x : ↥s seems to work too

Indeed, I was just too lazy to copypaste the arrow :)

[Eric Wieser]

Term mode let fails in the same way on the same input, interestingly

[Eric Wieser]

example (s : subalgebra R A) : true :=
  -- invalid constructor ⟨...⟩, expected type is not an inductive type
  --   s
  let x : s := ⟨0, s.zero_mem⟩ in trivial

[Anne Baanen]

Looks like it's the same thing, with pp.all it only says s, not has_coe_to_sort.coe_sort _.

[Anne Baanen]

I'm a bit stuck here. I think elaborator::visit_typed_expr will do the right thing here, inserting the correct coercions to make t a type and v a term of that type. But I'm not sure that we can get at the elaborator from the tactic state in assertv_definev_core. @Gabriel Ebner, could you help out?

[Anne Baanen]

(I'm not necessarily saying that visit_typed_expr is exactly the correct thing to call, just that we should emulate what it does.)

[Gabriel Ebner]

Do you have a mathlib-free mwe?

[Anne Baanen]

inductive foo | bar

instance : has_coe_to_sort foo :=
⟨Type, λ _, unit⟩

set_option pp.all true

example : true :=
begin
  let x : foo.bar := (),
  trivial
end

[Anne Baanen]

Note that the error on let does not mention any coe_sort.

[Gabriel Ebner]

Do you want the let to work, or do you want to get a better error from definev?

[Anne Baanen]

The let should work.

[Gabriel Ebner]

Ok, I'll fix the have as well.

[Gabriel Ebner]

lean#555

[Anne Baanen]

Great, thank you!

[Eric Wieser]

@Gabriel Ebner, I assume that fixes tactic- but not term- mode?

[Gabriel Ebner]

Yes, this was not in the mwe. Give me a second.

[Gabriel Ebner]

That was another one-line fix. I wonder why we didn't run into this issue before though.

[Eric Wieser]

assume (x : foo.bar) is broken too

[Eric Wieser]

example : foo.bar → true := begin
  assume (x : foo.bar),
  trivial
end

[Eric Wieser]

With

unify tactic failed, failed to unify
  foo.bar : foo
and
  ↥foo.bar : has_coe_to_sort.S foo

[Mario Carneiro]

Doesn't `(e:Sort*) use coe instead of coe_sort for the coercion? I've been aware of this issue but the problem is that there isn't an easy way to create "elaborate as a type" without putting it in places like the binder of a lambda and throwing away the lambda

[Gabriel Ebner]

Whew! For a moment, you got me really worried there. But luckily, the mk_coercion function contains this wonderful part:

    if (is_sort(whnf_type)) {
        if (auto r = mk_coercion_to_sort(e, e_type, ref)) {
            return r;
        }
    }

And I've just checked: both the term-mode and the tactic versions produce the serif uparrow.