Zulip Chat Archive

Stream: general

Topic: let fails with coe_sort


view this post on Zulip Eric Wieser (Mar 16 2021 at 10:23):

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

view this post on Zulip Anne Baanen (Mar 16 2021 at 10:27):

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

view this post on Zulip Anne Baanen (Mar 16 2021 at 10:27):

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

view this post on Zulip Anne Baanen (Mar 16 2021 at 10:28):

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

view this post on Zulip Anne Baanen (Mar 16 2021 at 10:30):

As a workaround, you can do:

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

view this post on Zulip Anne Baanen (Mar 16 2021 at 10:35):

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.

view this post on Zulip Eric Wieser (Mar 16 2021 at 10:38):

let x : ↥s seems to work too

view this post on Zulip Anne Baanen (Mar 16 2021 at 10:39):

Eric Wieser said:

let x : ↥s seems to work too

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

view this post on Zulip Eric Wieser (Mar 16 2021 at 10:39):

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

view this post on Zulip Eric Wieser (Mar 16 2021 at 10:40):

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

view this post on Zulip Anne Baanen (Mar 16 2021 at 10:43):

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

view this post on Zulip Anne Baanen (Mar 16 2021 at 11:13):

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?

view this post on Zulip Anne Baanen (Mar 16 2021 at 11:14):

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

view this post on Zulip Gabriel Ebner (Mar 16 2021 at 11:14):

Do you have a mathlib-free mwe?

view this post on Zulip Anne Baanen (Mar 16 2021 at 11:17):

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

view this post on Zulip Anne Baanen (Mar 16 2021 at 11:19):

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

view this post on Zulip Gabriel Ebner (Mar 16 2021 at 11:20):

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

view this post on Zulip Anne Baanen (Mar 16 2021 at 11:21):

The let should work.

view this post on Zulip Gabriel Ebner (Mar 16 2021 at 11:21):

Ok, I'll fix the have as well.

view this post on Zulip Gabriel Ebner (Mar 16 2021 at 11:23):

lean#555

view this post on Zulip Anne Baanen (Mar 16 2021 at 11:24):

Great, thank you!

view this post on Zulip Eric Wieser (Mar 16 2021 at 11:27):

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

view this post on Zulip Gabriel Ebner (Mar 16 2021 at 11:28):

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

view this post on Zulip Gabriel Ebner (Mar 16 2021 at 11:31):

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

view this post on Zulip Eric Wieser (Mar 16 2021 at 11:34):

assume (x : foo.bar) is broken too

view this post on Zulip Eric Wieser (Mar 16 2021 at 11:35):

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

view this post on Zulip Eric Wieser (Mar 16 2021 at 11:36):

With

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

view this post on Zulip Mario Carneiro (Mar 16 2021 at 20:22):

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

view this post on Zulip Gabriel Ebner (Mar 16 2021 at 21:38):

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.


Last updated: May 12 2021 at 03:23 UTC