app builder exception, caused by `subst`

Stream: general

[Scott Morrison]

Has anyone seen the error

app_builder_exception, more information can be obtained using command `set_option trace.app_builder true`

and then with trace_app_builder

[app_builder] failed to build eq.rec, invalid motive:
λ (r : ↥R), ↥S

This being caused by a call to subst z, where

R S : Ring,
r : ↥R,
r_1 : (forget Ring).obj S,
z : r = ⇑(equiv.symm (iso.to_equiv (map_iso (forget Ring).obj i))) r_1

[Scott Morrison]

I'm not really sure what problem I should be looking for.

[Mario Carneiro]

what is the goal?

[Mario Carneiro]

pp.all please

[Scott Morrison]

one sec, there's a duplicated variable name, let me get rid of that

[Scott Morrison]

https://gist.github.com/semorrison/a3c3c46a1b260fc04387c5492bca96d2

[Scott Morrison]

without pp.all the state is

app_builder_exception, more information can be obtained using command `set_option trace.app_builder true`
state:
R S : Ring,
i : R ≅ S,
r : ↥R,
x : (forget Ring).obj S,
z : r = ⇑(equiv.symm (iso.to_equiv (map_iso (forget Ring).obj i))) x
⊢ ↥S

and we're calling subst z.

[Mario Carneiro]

I also want to see that invalid motive with pp.all

[Scott Morrison]

[app_builder] failed to build eq.rec, invalid motive:
λ (r : @coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} R),
  @coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} S

[Scott Morrison]

seems harmless to me?

[Mario Carneiro]

Oh, I just checked the code and that term is supposed to be a pi type

[Mario Carneiro]

it gives that error because it's a lambda instead

[Mario Carneiro]

wait, scratch that, it infers the type and makes sure that is a pi type which is a sort

[Mario Carneiro]

I think I see how this is going wrong

[Mario Carneiro]

what is the type of that term?

[Mario Carneiro]

import algebra.category.CommRing.basic
universes u
variables (R S : Ring.{u})
#check
  λ (r : @coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} R),
  @coe_sort.{u+2 u+2} Ring.{u} Ring.has_coe_to_sort.{u} S
-- λ (r : ↥R), ↥S : ↥R → has_coe_to_sort.S Ring

[Mario Carneiro]

has_coe_to_sort.S Ring is defeq to Sort u but subst isn't trying hard enough to find that out

[Scott Morrison]

@Mario Carneiro, is there some simplification that I could do beforehand that might help subst? Or I'm I going to have to look into the implementation of subst_core?

[Mario Carneiro]

a quick fix might be to use cases or rw instead of subst

[Mario Carneiro]

Oh, actually the way it's written it doesn't even try to reduce the expression before matching it against Sort u. That's definitely a bug, it should whnf the thing first

[Mario Carneiro]

https://github.com/leanprover-community/lean/pull/165

[Scott Morrison]

Awesome :-)

[Scott Morrison]

Now I need to remember how to run against a branch of lean. I will try this out asap.

[Scott Morrison]

hmm, less easy than I hoped :-)