don't know how to synthesize placeholder

Stream: new members

[Michael Beeson]

Here is a short code sample that generates the error message in the post's title. Why does it
generate this message, and how do I get rid of it?

class  ExampleClass (M:Type) :=
(Rel: M →  Prop)
(p44:M)

variables (M:Type) [ExampleClass M] (a b x y z: M)
open ExampleClass

lemma test: (Rel  p44) :=
  begin
    sorry,
  end

[Patrick Massot]

It means Lean has no way to infer M.

[Patrick Massot]

One way to fix it is to write lemma test: Rel (p44 : M).

[Michael Beeson]

Yes, that worked, and also, if I add p44 to the list of variables of type M that works too.
"Lean has no way to infer that M is the type of p44" or
"Lean has no way to infer the type of p44"
There's really no other possibility in sight... but I see now what Lean needs, thank you.

[Michael Beeson]

What is the meaning of "placeholder" here? Why doesn't it say "don't know how to infer the type of a variable" ?

[Patrick Massot]

It's not about Lean. That lemma that you wrote never mention M anywhere!

[Patrick Massot]

And if you add p44 to your list of variable it simply shadows what you have from ExampleClass.

[Patrick Massot]

It doesn't say "don't know how to infer the type of a variable" because that's not the issue.

[Patrick Massot]

Maybe we could help you more if you could tell more about what you actually want to do. Maybe you minimized so much that it became meaningless.

[Kevin Buzzard]

Rel p44 is just a Prop. It can't see M any more

[Michael Beeson]

OK, then, I haven't understood what IS the issue. I still don't know what "placeholder means" . I thought that
"open ExampleClass" would mean that I could mention p44 and Lean would understand it as the p44 declared in ExampleClass to be of type M. So the lemma doesn't contain "M" literally but it does contain p44, which is declared in ExampleClass to be of type M. Something is wrong, that is fixed by explicitly saying (p44:M) instead of just p44, but I'm told inferring the type of a variable is not the issue. Well, I would like to understand exactly what is going on here....

[Alex J. Best]

If there is some information (a type or a term) that you don't want to provide explicitly, you can often write an "_" to signify that you want lean to try and work out what should go in place of "_" by its own. This is useful as sometimes what should go in the space is long or boring to work out, but clear from context, for example I can do this

example : 1 + 2 = 2 + 1 :=
begin
  exact add_comm _ _,
end

I could have written add_comm 1 2 but then I'd have to remember which way around the 1 and 2 should go in add_comm. This underscore is an explicit placeholder, by using a placeholder instead lean can work out what should go in the underscore for this to work.

Now in your example you haven't written any underscore explicitly, but there is information which is left implicit, and to lean there are terms which are left as placeholders, so lean has too try and work it out, but cannot, hence it complains that it can't fill in the blank (which is implicitly there).

[Alex J. Best]

You could think of it as if you wrote

lemma test: ((Rel : _ → Prop) (p44 : _)) :=
  begin
    sorry,
  end

those types are the placeholders lean can't fill. In most situations its okay not to write explicitly the type of everything all the time, just not in this situation!

[Marc Huisinga]

if i am understanding correctly:
variables are not passed to every function/lemma, only those that reference something of that name.
so in your definition of test, lean will look at Rel and p44, the type of which reference some type M'. because you're never referencing M anywhere in your lemma, M is not a parameter to test, and lean will not know that you want M for M', and hence it will yield an error.

[Marc Huisinga]

note that even adding M to the parameter list will still yield an error, because lean isn't sure whether M is the M' that you want

[Marc Huisinga]

when adding the type annotation, you tell lean that M' = M

[Marc Huisinga]

i think it says placeholder instead of missing type because placeholder is a more general concept that might also apply to other things like terms.

patrick's comment about it not being about lean refers to the first step with variables i mentioned: lean can't even take a stab at figuring out that the type is M because M does not appear in the parameter list when it is not mentioned. once you explicitly add it to the parameter list, lean still complains, but this time because it doesn't just nilly-willy want to assume that M' = M :)

[Michael Beeson]

So, the parameter M:Type that is mentioned in the class definition doesn't get passed automatically with the members of the class, in this case Rel and p44. I need to mention M in defining test. When I've successfully defined test, and I want to use it, I have to pass M as the first argument, e.g. test M. Then it's the passed M that will be used as the type of p44. That explains why you have to pass M as an argument to test. Are these statements correct?

[Alex J. Best]

Well the parameter M is exactly that a parameter, it could vary if you had

variables (M:Type) [ExampleClass M] (a b x y z: M)
variables (N:Type) [ExampleClass N]
open ExampleClass

lemma test: Rel p44 :=
  begin
    sorry,
  end

lean can't tell if you want the Rel and p44 from ExampleClass M or from ExampleClass N.

[Alex J. Best]

If test was enough to specify M it wouldn't be necessary to tell it: e.g. if you had

lemma test: p44 =x:=
  begin
    sorry,
  end

it works fine as x is of type M so lean knows what p44's type should be