Skip to content

doc(elabissues): typeclass loop issue and suggestions #61

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
dselsam wants to merge 1 commit into from
Closed

doc(elabissues): typeclass loop issue and suggestions #61

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
65 changes: 65 additions & 0 deletions tests/elabissues/typeclass_nested_validate.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
/-
This example demonstrates a case where Lean4's tabled typeclass resolution may loop.
It also suggests a workaround, new instance binder semantics, new syntax support, and a new instance validation rule.
-/

class Field (K : Type) := (u : Unit)
class VectorSpace (K : Type) [Field K] (E : Type) := (u : Unit)
instance VectorSpaceSelf (K : Type) [Field K] : VectorSpace K K := {u:=()}
class CompleteSpace (α : Type) := (u : Unit)
def AlgebraicClosure (K : Type) [Field K] : Type := K

/-
Note that this instance is not a problem when `K` is known,
because it will only ever "unpack" AlgebraicClosures, not create new ones
However, if `K` is ever not known, it will create them ad infinitum!
-/
instance AlgebraicClosure.Field (K : Type) [Field K] : Field (AlgebraicClosure K) := {u:=()}

/-
Here is the "bad" instance one may be tempted to write:

<<
instance bad (K E : Type) [Field K] [VectorSpace K E] [CompleteSpace K] : CompleteSpace E := {u := ()}
>>

It is bad because typeclass resolution will try to find `Field ?K` before it knows what `?K` is,
which in conjunction with the instance `AlgebraicClosure.Field`, will cause resolution to diverge.

Here is the workaround, which is very ugly:

<<
instance veryUgly (K E : Type) {fK : Field K} [@VectorSpace K fK E] [CompleteSpace K] : CompleteSpace E := {u := ()}
>>

Here, `Field ?K` is not solved by typeclass resolution, and instead `VectorSpace ?K ?fK E` will be solved first instead.

With the Lean3 instance semantics, one could make this less ugly by writing
-/
instance ugly (K E : Type) {_ : Field K} [VectorSpace K E] [CompleteSpace K] : CompleteSpace E := {u := ()}

/-
This would work because the `Field K` instance would still be considered for typeclass resolution even though it was not in a `[]` binder.
However, the original plan for Lean4 was that one would only consider `[]` binders for typeclass resolution.
We suggest that we revert to the Lean3 protocol instead, and consider any local variable with class type as a candidate instance.

Finally, this instance could be made reasonable by allowing `{}` binders without names:
<<
instance reasonable (K E : Type) {Field K} [VectorSpace K E] [CompleteSpace K] : CompleteSpace E := {u := ()} -- should work in Lean4
>>

@leodemoura leodemoura Nov 8, 2019

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The syntax {Field K} is ambiguous :(
It can be interpreted also as {Field K : _}. Note that we use this version all the time (e.g., {α β}).

@Kha: please take a look at this thread, and chime in.

@leodemoura leodemoura Nov 8, 2019

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Kha: @dselsam and I considered silently converting

instance bad (K E : Type) [Field K] [VectorSpace K E] [CompleteSpace K] : CompleteSpace E := {u := ()}

into

instance bad (K E : Type) {_ : Field K} [VectorSpace K E] [CompleteSpace K] : CompleteSpace E := {u := ()}

since the local instance Field K occurs at [VectorSpace K E].
We discarded it because we believed it would confuse users. However, I am considering it again.
Another motivation is the following example:

variables  (K E : Type) [Field K]
instance reasonable [VectorSpace K E] [CompleteSpace K] : CompleteSpace E := ...

works as expected, and the argument [Field K] is automatically added to the signature as expected.
On the other hand, the following example will fail to be elaborated:

variables  (K E : Type) {_ : Field K}
instance reasonable [VectorSpace K E] [CompleteSpace K] : CompleteSpace E := ...

@leodemoura leodemoura Nov 8, 2019

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am on the fence. The "silent conversion" described above is changing the "logic program" written by the user. For this particular scenario, the modification is beneficial, but in other scenarios, it may have a negative impact.

@Kha Kha Nov 8, 2019

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The silent conversion would have been my first idea as well, but I can see how it could not always be wanted. We should search for examples where it is not.

@Kha Kha Nov 8, 2019 •
edited
Loading

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@dselsam AFAICT, Coq does something quite similar to this by delaying dependent goals, right? So there is at least precedent. How would you compare these two approaches (delaying and conversion)?

@dselsam dselsam Nov 8, 2019 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Kha Yes, it is a good point. During typeclass resolution, Coq will "shelve" dependent goals and only try them after all goals that depend on them have been solved.

It is also worth noting Coq's implicit generalization feature `{...}, which allows omitting the field argument from the instance declaration:

Instance Bad (K E : Type) `{_ : VectorSpace K E} { _ : CompleteSpace K} 
  : CompleteSpace E := {}.
Check Bad.
(* Bad : forall (K E : Type) (_inst_ : Field K),
       VectorSpace K E -> CompleteSpace K -> CompleteSpace E *)

Though if you recall, you found this surprising when you exported the algebraic hierarchy to Coq. Also, if Field K appears multiple times, it would be implicitly generalized multiple times as well.

Also note that every variant of this problem I try in Coq immediately enters an infinite loop for silly reasons, because Coq doesn't table.

@dselsam dselsam Nov 8, 2019 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How would you compare these two approaches (delaying and conversion)?

@Kha Here is an artificial example where they differ:

class Base (α : Type) := (u:Unit)
class Depends (α : Type) [Base α] := (u:Unit)
class Top := (u:Unit)

Suppose, for some reason, the user made this Base α argument implicit instead of inst-implicit:

instance DependsNotConstrainingImplicit {α : Type} 
  /- [Base α] -/ {_:Base α} : Depends α := {u:=()}

Then replacing BaseAsInstImplicit with BaseAsImplicit below will cause typeclass resolution to fail on the #synth Top query below:

--instance BaseAsInstImplicit {α : Type} [Base α] [Depends α] : Top := {u:=()}
instance BaseAsImplicit {α : Type} {_:Base α} [Depends α] : Top := {u:=()}

axiom K : Type
instance BaseK : Base K := {u:=()}

#synth Top

On the other hand, Coq's approach of shelving goals would still work,
because it would shelve the [Base α] of BaseAsInstImplicit,
but eventually return to it and find the BaseK instance.

-/

axiom K : Type
instance K_Field : Field K := {u:=()}

#synth CompleteSpace K -- should fail quickly (and in particular, not run forever)

/-
The bad instance above could trigger a validation warning:

<<
instance bad (K E : Type) [Field K] [VectorSpace K E] [CompleteSpace K] : CompleteSpace E := {u := ()}
>>
-- Warning: argument #3 is a class that occurs in downstream arguments and not the return type.
-- You may want to replace [Field K] with {Field K} so typeclass resolution infers this instance after solving downstream instances.
-/