unusable arguments

Stream: general

[Reid Barton]

From #2502:

instance forget₂ (F : Π {α}, d α → c α) [parent_projection @F] : has_forget₂ (bundled d) (bundled c) :=
{ forget₂ :=
  { obj := λ X, ⟨X, F X.2⟩,
    map := λ X Y f, f } }

Unless I am very confused, I'm pretty sure this is not usable as an instance because F could never be inferred (bundled doesn't mention it implicitly). Wasn't there some discussion about a linter for cases like this?

[Gabriel Ebner]

It can be inferred using an instance for parent_projection.

[Scott Morrison]

I think you're right, Reid, this should be a def, not an instance.

[Reid Barton]

It makes me wonder whether, in the context of #2502, parent_projection plays any role at all

[Reid Barton]

Gabriel, I don't understand. I see that we could infer F from the instance or the instance from F (by instance search), but how can either of them be determined by anything on the right side of the :?

[Gabriel Ebner]

I hope I understand how this is supposed to be used. Say you want to solve ?m_1 : has_forget₂ (bundled group) (bundled monoid), then Lean will apply the instance forget₂ and you get a new goal ?m_2 : @parent_projection monoid group ?m_3, which is then presumably solved using the instance Group.category_theory.bundled_hom.parent_projection : parent_projection group.to_monoid.

[Gabriel Ebner]

I think it would be a bit clearer if the type arguments in parent_projection were explicit and the functor was explicily marked as an out_param.

[Mario Carneiro]

Couldn't the functor be a field of parent_projection?

[Reid Barton]

I thought that the instance could only be used if F was an out_param.

[Gabriel Ebner]

If the functor is a field you'd need to reduce them afterwards to get acceptable terms.

[Gabriel Ebner]

out_param is only necessary at the interface between type-class search and the rest of Lean. Inside type-class search, everything is an out-param.

[Mario Carneiro]

no more than usual, I think

[Mario Carneiro]

With this setup it seems that parent_projection doesn't carry any information at all

[Reid Barton]

Gabriel Ebner said:

out_param is only necessary at the interface between type-class search and the rest of Lean. Inside type-class search, everything is an out-param.

Oh wow, that seems super crazy to me (but then I am used to the sensible world of Haskell)

[Reid Barton]

I feel like this is variable declaration all over again, where ALGOL 60 solved the problem properly and subsequently every dynamic language in the world decided it had a better idea how to do it.

[Gabriel Ebner]

I guess it explains some of our performance problems. Unfortunately the powers that be have decided to keep this Prolog-like search in Lean 4. AFAICT the only real application of this "feature" are the transitive instances for has_coe such as coe_trans. And Lean 4 isn't getting rid of coe_trans either, so we'll have to live with the coe_coe simp lemma hack. :disappointed:

[Reid Barton]

Well, I'd prefer an efficient, predictable, and dumb procedure over what we have in Lean 3. The dumb part is not a requirement :upside_down: We'll see how well the Lean 4 approach works when we start using it.

[Kevin Buzzard]

Gabriel Ebner said:

Unfortunately the powers that be have decided to keep this Prolog-like search in Lean 4.

Maybe it's time for a fork!

[Reid Barton]

Lean 4.0.0-beta-1-c-alpha?

[Reid Barton]

I wanted to believe that instance search doesn't really work the way Gabriel said, but it does. Here is a simplified example.

class is_good {α β : Type} (F : α → β)

instance : is_good nat.succ := ⟨⟩

class has_forget (α β : Type) :=
(forget : α → β)

instance I {α β : Type} (F : α → β) [is_good F] : has_forget α β :=
⟨F⟩

#reduce (show has_forget ℕ ℕ, by apply_instance)   -- {forget := nat.succ}

[Reid Barton]

Gabriel Ebner said:

out_param is only necessary at the interface between type-class search and the rest of Lean. Inside type-class search, everything is an out-param.

Is this something that could easily be "fixed" to behave more like a Haskell programmer (or at least a GHC developer :upside_down:) would expect, or do we think mathlib relies heavily on it? To be clear: the expected behavior is that when a instance search problem contains a metavariable, we never select an instance if it means assigning that metavariable. (But it's still fine to select an instance which has a variable where the search problem has a metavariable.)

[Reid Barton]

I think this is still compatible with "Prolog-like search" and backtracking; I'm not sure what Lean 4 does in this area but from my visit to MSR I have the impression that the plan was to do something like what I describe here.

[Gabriel Ebner]

I'm not exactly sure what you mean. Do you suggest that has_mem ?m (set ℕ) may not assign ?m? I think this would break lots of stuff. For example 42 ∈ A would no longer work if A : set ℝ.

[Reid Barton]

Sorry, what I say only applies in the absence of out_param.

[Reid Barton]

I'm not sure exactly what to say when there is out_param but I think it's roughly: allow assigning to a metavariable when that metavariable occurs in a position with out_param.

[Reid Barton]

∈ has

class has_mem (α : out_param $ Type u) (γ : Type v) := (mem : α → γ → Prop)

[Gabriel Ebner]

Can you maybe give an example?

[Reid Barton]

I think my previous message (from Apr 28) is an example: to apply the instance I we first have to solve is_good ?m_1 and we shouldn't be allowed to apply the instance for is_good nat.succ.

[Gabriel Ebner]

Ah, so does this question come from the "function expected" thread? Then I think the answer is "this will change in Lean 4".

[Reid Barton]

Yes.

[Reid Barton]

Can we change Lean 3 to what Lean 4 will do?

[Reid Barton]

And, the other question is will Lean 4 do more or less what I described above?

[Gabriel Ebner]

The Apr 28 example will not change. The only place where we make use of this feature is in transitive coercions. AFAICT Lean 4 will rely on transitive coercions implemented in this way even more heavily.

[Reid Barton]

I guess I can just test the Apr 28 example in current Lean 4.

[Reid Barton]

Indeed, it still seems to work :slight_frown:

[Reid Barton]

Well, with not so current Lean 4. I tried getting the latest version and building it, but the build instructions don't work for me:

rwbarton@operad:~/math/lean/lean4/build/release$ cmake ../..
-- The CXX compiler identification is GNU 7.5.0
-- The C compiler identification is GNU 7.5.0
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
CMake Error at CMakeLists.txt:76 (add_custom_target):
  The target name "test" is reserved or not valid for certain CMake features,
  such as generator expressions, and may result in undefined behavior.


-- Configuring incomplete, errors occurred!
See also "/home/rwbarton/math/lean/lean4/build/release/CMakeFiles/CMakeOutput.log".

[Reid Barton]

@Sebastian Ullrich :point_up: is this a cmake version issue perhaps?

[Sebastian Ullrich]

@Reid Barton Huh, that's interesting. Which cmake version are you using?

[Reid Barton]

cmake version 3.10.2

[Gabriel Ebner]

@Reid Barton Note that Lean 3 type class synthesis also works if the type contains metavariables, it's just that the elaborator refuses to add a coercion. This should be fixable.

class foo (α : Type) := (x : ℕ)
instance fourty_two (α) : foo α := ⟨42⟩
example : ℕ :=
begin
  have α : Type, tactic.swap,
  -- at this point α is still a metavariable
  exact foo.x α,
  --
  exact unit
end

[Reid Barton]

I also tried building a version from May 8 but I got a different error:

CMake Error at CMakeLists.txt:530 (if):
  if given arguments:

    "EQUAL" "0"

  Unknown arguments specified

[Sebastian Ullrich]

@Reid Barton It works on 3.16.5

[Reid Barton]

I'll see if Ubuntu has packaged some more recent version. But maybe it's easiest if you can just rename the target?

[Reid Barton]

Might hit that other error next though

[Reid Barton]

20.04 LTS has 3.16.3, maybe if I am feeling brave some day I can try upgrading to that.

[Reid Barton]

@Gabriel Ebner This example is unobjectionable because the instance claims to work for all types. If you change fourty_two to be about a specific type, then it fails (which is also correct). And this is good because it means there is always at most one value for x (assuming you don't write overlapping instances), but if you want to write an instance that fixes the same value of x for every type, then it works even when the type is unknown.

[Sebastian Ullrich]

@Reid Barton They changed this in 3.11.0 apparently. But you can try passing -Wno-dev to cmake ../..

[Gabriel Ebner]

@Reid Barton I am really dense today. Do you agree that fourty_two should work, or do you think it shouldn't?

[Reid Barton]

Your example should work.

[Reid Barton]

It should fail if you change fourty_two to be about a specific type (rather than an arbitrary α), and it does.

[Reid Barton]

Actually, in this setup with have α : Type, tactic.swap, it seems that instance search doesn't believe that α is a metavariable it could assign.

[Reid Barton]

@Sebastian Ullrich I got the same error, but I just renamed the test target locally and it seems to work fine for me for now.

[Reid Barton]

Of course you probably don't want to rename the target for other reasons, so I'm happy with this workaround for now.

[Reid Barton]

@Gabriel Ebner My main worry, which might be misplaced, is that if we have Lean look for a has_coe_to_fun instance too early, before we know anything about the actual type, it will commit to some nonsense instance.

[Reid Barton]

That is, the thing e we want to coerce is actually an equiv but we don't know this yet, and then instance selection chooses the instance for linear_fun or whatever, and then e gets type checked as a linear_fun.

[Reid Barton]

I'd rather fix this structurally by never letting instance selection refine a metavariable (unless directed to by out_param).

[Reid Barton]

The current implementation avoids this in the heavy-handed way of not even considering using a coercion until there are no metavariables, which has me worried that the problem I imagine is a real one.

[Reid Barton]

I guess a weaker sufficient property is "instance selection never refines a metavariable that existed beforehand", and I don't know whether this can fail.

[Gabriel Ebner]

Right now, type class synthesis just rejects all instances that contain metavariables, no matter whether they are introduced during TC search ("temporary metavariables") or are metavariables that existed before. I'll try weakening this check to "doesn't contain metavariables introduced during TC search", is that what you had in mind?

[Reid Barton]

I'm not sure what "instances that contain metavariables" means.
What I object to is the second (successful) step in the trace from the Apr 28 example:

[class_instances] (0) ?x_0 : has_forget ℕ ℕ := @I ?x_1 ?x_2 ?x_3 ?x_4
[class_instances] (1) ?x_4 : @is_good ℕ ℕ ?x_3 := nat.succ.is_good

Here nat.succ.is_good has type @is_good ℕ ℕ nat.succ. In order to apply this instance we need to assign ?x_3 := nat.succ; I claim we should never assign a metavariable in this way (except in the presence of out_param).
In general, a metavariable might be "owned" by something other than instance search and so it does not make sense for instance search to assign it. For example, it might be the type of an expression e in an application e x; we haven't elaborated e yet so we represent its type as a metavariable. In this case it is definitely not sensible for instance search to assign this metavariable (except in the presence of out_param, since this is its purpose).
Now, in the trace above, ?x_3 actually came from applying another instance, and so arguably it is "owned" by the instance search. This still seems dubious to me (and definitely breaks instance coherence), but it is better than assigning metavariables that existed prior to instance search. For example, if the type of ?x_0 contained a metavariable, it would definitely be wrong to assign it in the course of applying an instance.
It's possible that the behavior is already "instance selection never refines a metavariable that existed beforehand".

[Gabriel Ebner]

I don't like it either, but this required by how transitive coercions are encoded as type class resolution problems, which I don't like either. But for that reason it's very unlikely it will change in Lean 4.

[Mario Carneiro]

It sounds like Reid is not objecting to applying instances like coe_trans because these have a type like coe1 a b -> coe_t b c -> coe_t a c, and as long as both a and c are known then this can apply, because it's not assigning any existing metavariables, only creating a new one. (I would argue that this instance should have an out_param on b to flag that this new variable is okay, but that's another matter.) Reid's criterion means that the coe1 a ?b is now stuck, but coe_t ?b c can make progress because coe_t has an out_param on its first argument, and once it is done coe1 a b can fire.