A strange error (or lack thereof)

[mikeshulman]

Commit d238e03e3eb is on top of PR #470. It causes compilation to fail in Pushout.v with the error

File "./theories/hit/Pushout.v", line 77, characters 2-51:
Error:
Cannot infer an internal placeholder of type "TruncType.TruncType minus_two" in environment:

A : hSet
B : hSet
f : A -> B

I have two questions:

1. Why is this? Why do we get an error in Pushout by changing ReflectiveSubuniverse (which is not even imported directly into Pushout) to import (but not use anything from) Functorish?
2. Why did the offending line Definition setcone := Truncation 0 (pushout f !). ever work in the first place? As far as I can tell, ! is a notation for the unique map from any type to any contractible type, so how did Coq guess in this case that the contractible type should be Unit?

[JasonGross]

1. Coq is terrible at modularity; typeclass instance track Requires, not Imports. If ReflectiveSubuniverse shows up anywhere in the dependency graph of Pushout, things Required (they don't even need to be Imported) by ReflectiveSubuniverse can affect Pushout. The coqdevs now agree that side effects of Require are a terrible idea, and have stipped out most of them. The two that immediately come to mind are typeclass instances (should be easily fixable, but the devs'll need a backwards compatibility story; I'll poke them about it) and (Reserved) Notations (we'd need a better parser than camlp to fix this problem). I'll go open a separate issue saying that we should make a file, reserving all the notations that we use, and Export it from Overture to ameliorate this bit.
2. When I wrote the code, I was careful to make the instance for Unit the only priority 0 truncation hint to be imported, after I encountered that error message and was confused. So there is an easy fix of adding | 1 To all of the other Contr/IsTrunc hints which take no typeclass arguments. I seem to recall mentioning this somewhere (I'm not at a computer right now so I can't check), but it should definately be mentioned where ! is defined, if it's not there already. Still, perhaps this is too much magic; I will leave that to others to decide. I personally like the generality here, and plan on seeing if I can get ! to also work as "a functor to a terminal category" and have it play well with !x meaning "the constant functor from a terminal category, sending everything to x".

[mikeshulman]

1. I'm not sure what you're saying, but it sounds like you don't know exactly what happened?

2. Are you saying that given a typeclass foo (A:Type) which has only one instance of priority 0, a hypothesis of {A:Type} {f:foo A} will be automatically guessed to be that instance? I think that's a terrible idea! Shouldn't a typeclass with a parameter be regarded as a property of that parameter? Just because there's only one known type with a given property, why would I want to assume that all types with that property are the known one?

   I wonder if this might explain some other very annoying behavior I was seeing where refine (BuildEquiv _ _ _ _) automatically inserted a transport idmap?

[mikeshulman]

Also, it seems like a bad idea from a pure code-maintainability perspective to depend on behavior that can be messed up nonlocally by someone defining a new instance anywhere else in the code and failing to include some black magic that they wouldn't know about unless they read the definition of ! (and why would they expect to have to do that before defining an instance of Contr?)

I'm not really a fan of ! denoting the unique map to the terminal object anyway except in commutative diagrams; in general I don't think punctuation should be used as a variable name. Why not define const for a constant function and then ! can be replaced with const center, or const tt if we want to make clear its target?

[JasonGross]

1. I don't know exactly what happened, but I'm pretty sure I know enough to fully explain the behavior that's mysterious to you. If you look in all of the files that are Required by Pushout.v, and all the files Required by those, and so on, you'll get all of the files recursively required by Pushout.v. Any typeclass instance in any of those files will be picked up automatically by typeclass resolution in Pushout.v. I'm confident that adding Require Import Functorish to ReflectiveSubuniverse added some files to this list, and in one of those files is an instance of Contr that has priority 0. The only information I don't know is which particular file and instance were included; I know the rest of the mechanism.
2. Not quite. I'm saying that given a typeclass foo (A:Type) and an instance of that typeclass which takes no typeclass arguments, Coq will use it to resolve a goal of type foo ?1 (where ?1 stands in for any evar), and sometimes give you the internal placeholder error message if it fails, I think. So it's not that Coq assumes that all types with the given property are the known one, just that all completely free/unknown types might, in the absence of other errors, be the known one. So, yes, this is probably the same issue as refine (BuildEquiv _ _ _ _) causing Coq to go "ooh, I know an equivalence! transport idmap is an equivalence. And transport idmap typechecks as a function I can use here! You must be looking for transport idmap!"

[JasonGross]

I've made a feature request for a refine that doesn't trigger typeclass resolution.

[JasonGross]

What do you think of !x meaning "the constant function" and using ! tt or ! (center _)?

[mikeshulman]

1. You're right. Adding | 1 to all the instances in TruncType fixes it --- I mean, makes the questionable code in Pushout go back to compiling.
2. Ugh! Where is that documented? Is there any way to turn it off? I would consider it a bug.
3. I don't like !x either. What's wrong with const? Surely constant functions don't occur so frequently that a few extra characters make much of a difference.

[mikeshulman]

It's not even just "an instance that takes no typeclass arguments":

Class qux.
Instance q : qux.
Class foo (A:Type).
Instance f `{qux} : foo Type.
Definition bar : {B:Type & foo B}.
eexists.
exact _.
Defined.

This is almost enough to make me swear off typeclasses entirely. Why would you want this?

[JasonGross]

1. (markdown will eat my 2 if I don't have this)
2. I don't know if it's documented, except that it's implied by the fact that "typeclass resolution" means, essentially, eauto with typeclass_instances, and eauto is allowed to instantiate evars. There's no way to turn it off, except by manually declaring all of your instances to not resolve if there are evars laying around, via Hint Extern n class_name => <check for no evars in the goal>; apply instance : typeclass_instances. I don't think this being the default behavior is a bug; I think setoid rewriting will break if you can't use typeclass resolution to figure out what the right intermediate subrelations and respectfulness properties are, because you want to, effectively, do transitivity in the middle of resolution to find subrelations. Perhaps @mattam82 can say more. Are you looking for a mode of typeclass inference that refuses to instantiate any evars? (Or one that only instantiates some evars?) (Feel free to request such a mode on the Coq bug tracker.)
3. When I talk about the category (C / x), either I need to use tactics in notations to infer that x is an object (which I'm still in the process of doing), or I need to, as I currently do, say (C / !x). Writing (C / (const x)) is longer and visually

Note: you can define a refine that doesn't do typeclass resolution as

Tactic Notation "refine_noTC" open_constr(term) := let G := match goal with |- ?G => constr:(G) end in refine (term : G).

because open_consr doesn't do typeclass resolution.

[mikeshulman]

It seems to me that typeclass resolution should not be guessing anything that's not part of the typeclass itself. I don't know much about setoid rewriting, but if you want typeclass inference to be inferring something, then it seems to me that you should make the thing to be inferred one of the fields of the class-record.

I'm not going to tell you what to do in categories, since I've never touched or looked at that code, but in the core, I am against this notation. (We also fairly recently discussed going back to using ! as a prefix for path-inversion, and the consensus seemed to be that we should do it, but no one has done it yet.)

And maybe I misunderstand, but refine_noTC doesn't seem to work:

Tactic Notation "refine_noTC" open_constr(term) := refine term.
Class foo.
Instance f : foo.
Definition bar `{foo} : Type := Type.
Definition baz : Type.
refine_noTC (@bar _).
Defined.

finds the instance f. And if I leave out the instance f, then it turns the missing foo into an evar, which is not what I would want either.

[mikeshulman]

If the issue is just that typeclass resolution instantiates evars, then in refine (BuildEquiv _ _ _ _), why is the function (the third argument of BuildEquiv) an evar? I thought that refine just tried to unify its argument with the goal and gave back any missing holes as new goals; why is it creating evars? Sorry if this is a silly question, I don't understand very much about Coq's internals or, I guess, even what an evar really is.

[mikeshulman]

The reference manual says that evars

can be generated from “_” when the corresponding implicit argument is unsolvable.

That sounds to me as though the typechecker will try to solve the implicit arguments, and then if it fails, it will make them into evars. But it seems that in order for your explanation of what's happening to be correct, it must go on trying to solve the implicit arguments after making them into evars. Or is it that it tries to solve the implicit arguments one-by-one, making each failed one into an evar before going on to the next one?

[JasonGross]

When you have a function f : A -> B -> Type, and your goal is f a b, and you have a hypothesis H : R a a', and you rewrite H, you can look for an instance that f respects R in the first variable and eq in the second. But perhaps you didn't register that as an instance, and instead registered that f respects RA in the first argument and RB in the second argument, and you also have an instance saying that R is a subrelation of RA, and an instance saying that RB is Reflexive. It would be nice to have Coq automatically infer this without having to give every possible combination of instances.

More precisely, to setoid rewrite with H, Coq currently tries, I believe, to solve the problems "f respects (?1 ==> ?2 ==> ?3)", "R is a subrelation of ?1", "Reflexive ?2", and "?3 is a subrelation of impl" (impl A B := A -> B) . Now, maybe you're saying that instead it should try to solve "f respects (R ==> @eq B ==> impl)". Somehow, though, I think we want to be able to replace @eq B with any reflexive relation.

I think I'm fine with ! being only a prefix notation.

Oops. Yes, I think you're right. Thanks for testing. (I'm confused why typeclass resolution triggers, but your point about evars is a showstopper, I think.) I've mentioned these at a relevant bug report; you might want to follow that.

[mikeshulman]

Couldn't you solve the rewriting problem by writing a general instance saying that if RA1 is a subrelation of RA2 and RB1 is a subrelation of RB2, then any function which respects RA2 and RB2 also respects RA1 and RB1 (and similarly that any function which respects a reflexive relation also respects eq)?

[JasonGross]

I thought that refine just tried to unify its argument with the goal and gave back any missing holes as new goals; why is it creating evars?

There is no single type of "holes" in Coq's internals; the notions of "metas" and "evars" are both ways of talking about "holes". (Note: evars can be either "shelved" or "unshelved". An "unshelved evar" shows up as a dependent goal; a "shelved evar" is like an "unshelved evar", but the goal is hidden.) It's not entirely clear to me which holes get turned into metas and which holes get turned into evars, nor why there's really a distinction. (I think we're moving towards having only evars, but I'm not sure.) I'm not sure how to reconcile this with what the manual says; perhaps @mattam82 can say more. I'll probably ask on coq-club and see if someone can explain it.

Couldn't you solve the rewriting problem by writing a general instance saying that if RA1 is a subrelation of RA2 and RB1 is a subrelation of RB2, then any function which respects RA2 and RB2 also respects RA1 and RB1 (and similarly that any function which respects a reflexive relation also respects eq)?

Yes. So you try to solve "f respects (R ==> @eq B ==> impl) by applying subrelation RA1 RA2 -> subrelation RB1 RB2 -> respectful (RA2 ==> RB2 ==> impl) f -> respectful (RA1 ==> RB1 ==> impl) f, and you are left with the goals subrelation R ?1, subrelation (@eq B) ?2, and respectful (?1 ==> ?2 ==> impl) f. Since all of these have evars, none of these will be solvable by your proposed algorithm. Unless I'm misunderstanding your proposal? (Perhaps if you give me a list of goals or pseudogoals you expect to see, and how you expect each to be solved, I'll understand better?)

[mikeshulman]

Does that mean that all goals are evars? Or are some of them metas? What is the difference between a meta and an evar?

Ah, I see the point about setoid respecting. But couldn't you do that by "making the thing to be inferred one of the fields of the class-record" as I originally suggested? So that the typeclass respectful would have the relevant setoid relations as fields rather than parameters?

[JasonGross]

Updated view of how I think things work: When you have holes in your term, Coq will first run unification to try to solve them. If unification fails, or if it succeeds but does not fully resolve all holes, any remaining holes are turned into evars, and typeclass resolution is run in the "goal" corresponding to any evar whose type is a typeclass. Then, if unification previously failed (e.g., it tried to unify nat with arg1_type ?1 and failed), it will resume/try again. I'm not actually sure if the difference between metas and evars is relevant, nor exactly what the difference is; I haven't read the code.

You're suggesting something like

Class respectful {A B} (f : A -> B) :=
  { RA : relation A
  ; RB : relation B
  ; _ : "f respects RA and RB" }.

and then setoid rewriting will pose the goals ?1 : respectful f, subrelation R ?1.(RA), and subrelation (@eq B) ?1.(RB). And the typeclass resolution will be backtracking but not run when there are evars, so you'll just try to solve subrelation R RA0 and subrelation (@eq B) RB0 for any RA0 and RB0 that you have a respectful instance for. You still need to do the subrelation all in one step, though, but perhaps this isn't terrible. @mattam82, do you have any thoughts or comments to add?

[mikeshulman]

Ok, I think I see a little better where the motivation for this comes from. I can certainly see that it's nice to be able to automatically make chains of subrelations, and I can't think of any way to do that without evars. I can even imagine maybe wanting to use a feature like this for something someday.

But there ought to be a way to turn it off (which I guess means not instantiating evars while doing typeclass resolution). Either globally, or locally on a per-class or per-instance basis (I'm not sure which would be better), or both. Maybe I will submit a feature request.

[JasonGross]

I'd made a request for the per-instance version, which should basically just be syntactic sugar on top of

Hint Extern n <class> => match goal with |- ?G => try (has_evar G; fail 1) end; eapply lem : typeclass_instances.

Feel free to add to that feature request, or make a related one if that doesn't cover what you want.

[mikeshulman]

Your Hint Extern doesn't seem to work for me. I assumed you meant to write that instead of declaring something to be an instance, such as

Class foo (A:Type) :=
  foof : Unit.

Definition f : foo Unit := tt.

Hint Extern 0 foo => match goal with |- ?G => try (has_evar G; fail 1) end; eapply f : typeclass_instances.

Definition bar : {B:Type & foo B}.
exists Unit.
exact _.
Defined.

But that doesn't work for me; neither exact _ or eauto with typeclass_instances can solve the goal.

[JasonGross]

Oops. I should test these before suggesting them.

Hint Extern 0 (foo _) => match goal with |- ?G => try (has_evar G; fail 1) end; eapply f : typeclass_instances.

I guess, in this case, you can probably do Hint Extern 0 (foo Unit) => apply f : typeclass_instances.. But in general, you'll want to leave holes or pattern variables.

[mikeshulman]

Thanks, that seems to work.

Hint Extern 0 (foo ?G) => try (has_evar G; fail 1); eapply f : typeclass_instances.

seems to also work.

Did you have a specific reason for requesting the per-instance version, other than the fact that it can be almost-implemented with existing hint commands?

[JasonGross]

No, I think that was the only reason.

[mikeshulman]

I tried this out, and it seems to mostly work: see 34303e64c. A few things need to be modified because some people have been sloppily using Equiv objects in place of IsEquiv ones (I didn't try to fix the occurrence(s) in categories). The definition of isequiv_path_equiv takes a long time to find the right instance for some reason; of course we could give it explicitly if we wanted. But other than that, nothing else breaks.

With this change, refine (BuildEquiv _ _ _ _) no longer inserts transport idmap, nor does it insert equiv_isequiv (which it started doing after I stopped it from inserting transport idmap). Instead, it spins forever. (-: I prefer that (it's less confusing), but it would be nice if it could actually generate a couple of subgoals; however, I guess there's probably no way around that until we have a version of refine that doesn't do any typeclass resolution.

[mattam82]

Ok, I just added a (long called for) flag for restricting resolution to matching (i.e. no instanciation of the goal evars) on a class by class basis, governed by a flag "Set Typeclasses Strict Resolution". It should have more or less the same semantics as this check that no evars appear, except it would be a bit more applicable and doesn't prevent Hint Extern's from circumventing it.

2014-09-09 22:24 GMT+02:00 Mike Shulman notifications@github.com:

I tried this out, and it seems to mostly work: see 34303e6 https://github.com/HoTT/HoTT/commit/34303e64ca6089e3f6bcad5b14a15b87ab1f2357. A few things need to be modified because some people have been sloppily using Equiv objects in place of IsEquiv ones (I didn't try to fix the occurrence(s) in categories). The definition of isequiv_path_equiv takes a long time to find the right instance for some reason; of course we could give it explicitly if we wanted. But other than that, nothing else breaks.

With this change, refine (BuildEquiv ) no longer inserts transport idmap, nor does it insert equiv_isequiv (which it started doing after I stopped it from inserting transport idmap). Instead, it spins forever. (-: I prefer that (it's less confusing), but it would be nice if it could actually generate a couple of subgoals; however, I guess there's probably no way around that until we have a version of refine that doesn't do any typeclass resolution.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/479#issuecomment-55028750.

-- Matthieu

[mikeshulman]

Awesome!! Thank you so much @mattam82 . So the idea is that the restriction is implemented for classes that were defined while "Set Typeclasses Strict Resolution" is on?

We should bump our coq submodule version to get this.

[mikeshulman]

I pulled Coq trunk to get this and tried to compile the HoTT library (without changing anything), but I got

File "./theories/categories/Comma/ProjectionFunctors.v", line 95, characters 4-16:
In nested Ltac calls to "comma_laws_t", last call failed.
Anomaly: Uncaught exception Invalid_argument("Array.fold_left2", _).
Please report.

I'm not sure how to go about reporting this; what do I do to get it down to a MWE for a bug report?

[mattam82]

On 11 sept. 2014, at 18:54, Mike Shulman notifications@github.com wrote:

Awesome!! Thank you so much @mattam82 . So the idea is that the restriction is implemented for classes that were defined while "Set Typeclasses Strict Resolution" is on?

Yes, exactly. A Global Set … will make all of them require strict resolution, but I expect for some cases when using type classes for proof search you wouldn’t want these semantics.

— Matthieu=

[JasonGross]

@mikeshulman: https://github.com/JasonGross/coq-bug-finder

cd theories
make categories/Comma/ProjectionFunctors.vo # we really just need the .glob file
/path/to/coq-bug-finder/find-bug.py categories/Comma/ProjectionFunctors.v bug_anomaly_fold_left_01.v --topname HoTT --coqc ../hoqc --coqtop ../hoqtop

You can add -v or -vv to the last invocation to make it more verbose. It'll compile the file, inline the dependencies, make sure you get the same error message, and then go to work at minimizing it.

[mikeshulman]

Thanks! Did you write that script yourself?

[mikeshulman]

It's running, but it remarked Your version of coqtop doesn't support -time. Falling back to more error-prone method. What would I have to do to get a version of coqtop supporting -time?

[JasonGross]

Yes, I did. I'm planning on making it much faster in the hopefully near future, by teaching it about BackTo.

Run mkdir coq/toploop. Or rull the most recent version of the repo and run make. I updated the configure script a few days ago to create the coq/toploop directory. If it doesn't exist, hoqtop -help fails.

[mikeshulman]

I'm still getting Your version of coqtop doesn't support -time. Running ./hoqtop -help in the HoTT root says System error: "/home/shulman/hott/coq/coq/ide: No such file or directory".

[mikeshulman]

I guess also symlinking ./coq/ide to ./coq-HoTT/ide works?

[JasonGross]

Oh, yeah, if you don't configure with -coqide no, I guess you have to do that, too. #500

[JasonGross]

I should also note that Your version of coqtop doesn't support -time only matters for the splitting-to-definitions step; if it successfully completes that step, then it will subsequently run identically in both cases.

[JasonGross]

@mikeshulman, I encountered that bug in my eta-proj-functor branch, and tracked it down (apologies for any wasted work). I've reported it and have a workaround.

[mikeshulman]

No problem. Have you tested whether with that workaround everything compiles with current trunk?

[JasonGross]

Everything on my eta-proj-functor branch compiles. I haven't checked if everything compiles without my primitive projection changes, but since it all compiles with my changes, I'd be surprised if if doesn't compile without them.

[mikeshulman]

Ok, I have the library compiling with current trunk, with your workaround and one additional fix to HoTTBook.v. I then tried to turn on Set Typeclasses Strict Resolution, and a few things had to be changed here and there. Some of them are things that I would consider bad style anyway, like passing the name of the IsEquiv instance to BuildEquiv and asking it to guess the function rather than the other way round, or talking about quotient _ rather than quotient R when the relation R is in the context for a whole section. Others are weird and I don't understand what they have to do with typeclasses at all, like having to write apply f. apply g. instead of apply f, g.

And some, perhaps unsurprisingly, have made me better appreciate the value of having typeclass inference guessing evars. In particular, I realized that the typeclasses I used for reflective subuniverses and modalities should be guessing evars, e.g. a hypothesis of inO A for a particular subuniverse subU matching a hole in the goal should allow Coq to guess that I want to be talking about subU --- at least, in the context where there's only one subuniverse around. It seems possible that if I were talking about more than one subuniverse, I wouldn't want this inference to be happening, and yet the typeclasses would be the same. I wonder whether it would be possible for a flag that affects proofs that happen while it is on, rather than classes that are defined while it is on?

I also wonder whether it would be possible to specify that some of the parameters of a typeclass should be guessed if they occur as evars but not others. For instance, when filling a hypothesis of IsTrunc n A it seems sometimes useful for Coq to be able to guess the value of n, but I don't think I would ever want it to be guessing the value of A.

(These Warning: Invalid character '?' at beginning of identifier "?42". messages we get with current trunk are also really annoying.)

[mikeshulman]

Oh, right, see this branch.

[mikeshulman]

Oh, and categories would also need some fixes to work with the Local Set Typeclasses Strict Resolution that I put in Overture, but I'm not familiar enough with it to do them myself.

[JasonGross]

@mattam82 could tell us for sure, but I suspect it would be a 10-line change (9 lines to declare the global flag, and one line to change if cl.cl_strict then to if cl.cl_strict || !typeclasses_currently_strict then or whatever) to get a per-proof version of the flag. Here's my attempt at what it would look like (completely untested), based on https://github.com/coq/coq/commit/2378b5ccee0e62d0b93935aa69c0bfedd2ac720e, and with a terrible name that I haven't put much thought into:

--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
+let typeclasses_currently_strict = ref false
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "currently strict typeclass resolution";
+      optkey   = ["Typeclasses";"Currently";"Strict";"Resolution"];
+      optread  = (fun () -> !typeclasses_currently_strict);
+      optwrite = (fun b -> typeclasses_currently_strict := b); }
+
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
  let freeze =
    try
      let cl = Typeclasses.class_info hdc in
-       if cl.cl_strict then
+       if cl.cl_strict || !typeclasses_currently_strict then
         Evarutil.evars_of_term concl
       else Evar.Set.empty
    with _ -> Evar.Set.empty
  in

As to declaring this on a per-parameter basis... I'm sure it could be done, but it might take me five days instead of five minutes to take a stab at it. (Though @mattam82 could say how easy it actually is.)

Oh, right, there was the refine/exact in HoTTBook that I reported a bug for. Anyway, @mattam82 has fixed the anomaly (thanks!), and Hugo has fixed the Warning: Invalid character '?' at beginning of identifier "?42"., so if you update to the latest trunk, you should need only the fix for HoTTBook.

Is there something wrong with the style @BuildEquiv _ _ _ (BuildIsEquiv f g s r e), or do you mean something else by "passing the [name of the] IsEquiv instance to BuildEquiv"?

The apply f, g failing sounds like a bug. Does apply f; apply g (or apply f; [ apply g | .. ]) work? Do you want to throw coq-bug-finder at it (using something like (apply f; apply g) || fail "bad". Undo. apply f, g. to get it to see the right error, and track the situation where apply f; apply g succeeds but apply f, g fails?

If you turn on travis for your fork of the repo, then I can see error messages without having to compile things myself. :-) As for categories, I don't think I use typeclasses much; I use them a bit for equivalences, and in many places to automatically handle the IsTrunc obligations of making things precategories. I suspect you're hitting the latter one, though I suppose it's possible that you're hitting poor style with Isomorphic and IsIsomorphism or something. Do you want to take a stab at fixing it? (I have the selfish motivation here of wanting to get other people interested in and using the category theory stuff. Speaking of which, I'm considering trying to do framed bicategories at some point, which David Spivak tells me you're the ... uh ... founder of?)

[mattam82]

Having the restriction on a parameter by parameter basis is easy for classes, that's like the declaration of input/output modes in logic programming (e.g. http://twelf.org/wiki/%25mode). Then in "strict resolution", all parameters would be inputs and resolution would fail if any of them contains evars. I have a patch that adds this.

I feel the "currently_strict" is a bit too stateful. It seems what you want is rather that the solution is unique. I've pushed a patch that did this a few days ago: "Set Typeclasses Unique Solutions" will check that there is a single solution to typeclass constraints but I didn't find a way yet to allow mixing this with class constraints for which you'd rather allow multiple solutions. For example, IsTrunc n A might be provable in mulitple ways but this should be irrelevant whereas having a unique instance of Eq A might be necessary.

[mikeshulman]

Yes, it is like input/output modes! That patch sounds great, are you planning to push it?

In the other case, you could be right that uniqueness is what I want, but to be really sure I'll want to try it out. I need to do a bit of the theory of lex modalities first, but then I'll be able to attack the propositional fracture theorem which uses two modalities at once, and that'll be a good test case for this. I don't quite understand what you mean by "mixing"; do you mean that it's not yet possible to have some typeclasses require unique solutions but other ones allow multiples? What exactly is the effect of "Set Typeclasses Unique Solutions" -- does it also alter the behavior of those classes defined while it is in effect?

[mikeshulman]

@JasonGross, I would prefer @BuildEquiv _ _ f (BuildIsEquiv _ g s r e), but that's not a big deal (style-wise). However, often it happens that the isequiv was defined previously rather than inline, and I think

Instance isequiv_f : IsEquiv f.

Definition equiv_f := BuildEquiv _ _ f _.

is more readable than

Instance isequiv_f : IsEquiv f.

Definition equiv_f := BuildEquiv _ _ _ isequiv_f.

It also follows the general principle of avoiding referring to typeclass instances by name.

I'll look at the other stuff when I get a chance. I didn't turn strict resolution on globally, only for the classes defined in Overture, so it's probably IsEquiv or IsTrunc that's causing problems in categories.

[mikeshulman]

re apply f,g: https://coq.inria.fr/bugs/show_bug.cgi?id=3633

[mikeshulman]

Ok, @mattam82 it looks like "Set Typeclasses Unique Solutions" applies to all typeclass resolution that happens while it's on, rather than only to particular classes? I haven't been able to try it on an example yet, but I think what I'm worried about is not unique solutions to typeclass instances but unique solutions to evars that are getting instantiated by typeclass inference.

[mikeshulman]

When Coq appears to be diverging on a given tactic call, is there any way to tell exactly what it's trying to do?

[JasonGross]

Depending on what you're doing, you can try Set Typeclasses eauto := debug., Set Ltac Debug., or info tac.. If those don't work, you can just copy-paste the tactic call and insert periods until I find the primitive tactic that's diverging.