doc(elabissues): typeclass loop issue and suggestions

[dselsam]

No description provided.

[leodemoura]

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]

@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]

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]

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]

@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]

@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]

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.

[leodemoura]

I have merged this PR yesterday. Let's continue the discussion on Zulip.
@dselsam Please use the new commit message conventions from now on.
There is no (...) before :.
The message should be doc: typeclass loop issue and suggestions.

[leodemoura]

@Kha @dselsam
I accidentally merged the PR yesterday without fixing the commit message.
I performed a destructive update to fix this mistake.