Zulip Chat Archive

Stream: general

Topic: spot the metavariable


view this post on Zulip Kevin Buzzard (Apr 08 2018 at 23:45):

#print false.rec -- protected eliminator false.rec : Π (C : Sort l), false → C
constant oops : false
definition n := false.rec  oops -- the "expected type must not contain metavariables" error
definition m := @false.rec  oops -- typechecks just fine

view this post on Zulip Kevin Buzzard (Apr 08 2018 at 23:46):

I am not sure I have seen foo and @foo behave differently before, in a situation where there are no implicit arguments

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 06:02):

In case you didn't already see it, the metavariable is in the type of the definition:

def n : _ := ...
def m : _ := ...

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 06:04):

The elaborator does not only take a pre-expression, but also an expected type as argument. Expected types are important to elaborate many pre-expressions, for example recursor applications or anonymous structure instances. This is why foo works but bar doesn't:

def foo :  ×  := 1, 2
def bar := 1, 2

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 06:29):

Elaboration of recursor applications is particularly sensitive to the expected type since the motive is computed by generalizing all occurrences of the major premise in the expected type. So when we elaborate nat.rec_on k _ _, we elaborate the major premise k and then replace k by a fresh variable in the expected type to get the motive. If the expected type is C k (k+1) for example, then we'd compute the motive λ x, C x (x+1). In your example, the elaborator just has a metavariable as expected type and cannot replace occurrences of the major premise (in a sensible way) to compute a motive.

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 06:32):

Maybe this is already clear, but in elaboration the "expected type" is the type the elaborated expression is supposed to have. For example, when we elaborate ⟨1, 2⟩ : ℕ × ℕ, we elaborate the pre-expression ⟨1, 2⟩ with the expected type ℕ × ℕ.

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 06:33):

Fun trick: you can suppress expected type propagation with : _.

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 10:36):

I don't understand your answer. In contrast to most blah.rec recursors, which have type Π {C : blah -> Sort u},..., false.rec has type Π (C : Sort u_1), false → C , so whilst in general I can see the issue and why that generic error shows up, for false.rec the information is there. I guess what I am saying is that perhaps the definition false.rec seems to have been explicitly manipulated by the system so that the motive is not implicit, but the error seems to indicate that some generic rule for recursors has been applied without noticing that in this case it does not apply. I have given Lean all the information it needs to work out the expected type and it has chosen to ignore it because I didn't put the @. That's the point I'm trying to make -- the elaborator, in this case, has all the information it needs, despite no @.

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 10:37):

I am trying to figure out how the elaborator works without reading the source code. Am I crazy? Is this not even possible, really? Stuff like " The elaborator does not only take a pre-expression, but also an expected type as argument. " are gold dust to me because I don't see any way of working this stuff out without asking.

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 10:42):

Another way of saying what I don't understand -- false.rec ℕ oops and @false.rec ℕ oops carry exactly the same information, but one works in a situation where the other does not, so it looks to me like some code somewhere is incorrectly distinguishing between them based on a "oh, there's an eliminator without an @, we are going to have to do some guesswork" principle which does not apply in this case.

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 10:48):

I guess a rather more tasteful way of demonstrating this behaviour is definition n (oops : false) := false.rec ℕ oops

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 11:10):

the error seems to indicate that some generic rule for recursors has been applied without noticing that in this case it does not apply.

You're completely right. https://github.com/leanprover/lean/blob/8f55ec4c50379c612731ced2424fd3eda0cf69a6/src/frontends/lean/elaborator.cpp#L117-L121

    if (inductive::is_elim_rule(env, n) ||
        is_aux_recursor(env, n) ||
        is_user_defined_recursor(env, n)) {
        return elaborator_strategy::AsEliminator;
    }

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 11:18):

I have given Lean all the information it needs

The goal of the elaborator is not to fill in missing pieces, it is to create a type-correct expression using the pre-expression as a recipe. The meaning of false.rec _ oops is not app (app (const `false.rec [level.mvar `a]) [mvar `b]) (local_const `oops ...) , it is a command to the elaborator, instructing it to (essentially) do an induction on oops. And well, the induction tactic can fail even if the goal would be solvable by induction.

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 11:19):

Do you think that I will have to learn some C++ if I want to understand Lean well enough to use it in practice?

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 11:21):

I don't think it's necessary to know the Lean implementation or even just C++ in order to understand and use Lean. I think I have a good mental model of how C++ or Scala work, without ever having seen their compilers.

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 11:22):

That's a relief :-)

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 11:23):

I think it took me about half a year to have a mental model for the Lean elaborator. I looked into the C++ code, though.

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 11:23):

Before that, I just added type annotations everywhere until the red squiggles went away.

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 11:23):

My impression is that it's very difficult to get a clear idea of what the elaborator is doing without reading the source.

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 11:24):

Currently I just add type class annotations everywhere until the red squiggles go away.

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 11:25):

I mean, there are general principles, but to get beyond them I think you just have to look at what is actually going on.

view this post on Zulip Kevin Buzzard (Apr 09 2018 at 11:26):

Thanks for your help, by the way!

view this post on Zulip Gabriel Ebner (Apr 09 2018 at 11:26):

You're welcome.


Last updated: May 17 2021 at 22:15 UTC