Stream: Coq users

Topic: Existential variable hint

Lef Ioannidis (Nov 11 2021 at 17:31):

Hello,

I am defining some terms with existential variables in them. Let's say their type is
Term ?t

Coq is (rightfully) giving an "unresolved implicit parameters" error. I have a default type for ?t I can provide, is it possible to add a Hint Extern to
help the existential unification algorithm with the default type? What should I match on, is it possible to get an example? This looks related
https://coq.inria.fr/refman/language/extensions/evars.html#solving-existential-variables-using-tactics
but does not mention Hints.

EDIT: is this a use case for ltac:(refine)? Thank you

Paolo Giarrusso (Nov 11 2021 at 19:15):

typeclasses could solve your problem. If the type of t is foo, Existing Class foo would enable typeclass search to fill in values.

Paolo Giarrusso (Nov 11 2021 at 19:16):

and typeclass search is also controlled via hints — in the typeclass_instances database.

Paolo Giarrusso (Nov 11 2021 at 19:17):

_however_, using this directly in your case might be a bad idea, depending on what foo is. For instance, Existing Class nat + hints for that would be akin to Russian roulette.

Lef Ioannidis (Nov 11 2021 at 19:42):

I made a concrete example, Existing Class nat does not seem to work, perhaps I am missing the hint step if you could elaborate on that.

  (* Do type inference first, if no error would be thrown it's all good! *)
  Definition x := cons true nil.

  (* If type inference would fail, Instead of an error, I want to get `nil nat` *)
  Fail Definition t := nil.

  (* this works but I still have to be explicit about the type annotation *)
  Definition t' := ltac:(refine nil; exact nat).

  (* This confusingly does not work??? *)
  Ltac mk x := refine x; exact nat;
  Fail Definition t := ltac:(mk nil).

  (* This was mentioned as an alternative but seems like a noop? *)
  Existing Class nat.
  Fail Definition t := nil.

  (* This does work (credits to @**Li-yao** but perhaps there is a way to do without the ltac? *)
  Tactic Notation "mk" uconstr(x) := refine x; exact nat.
  Definition t := ltac:(mk nil).

Paolo Giarrusso (Nov 11 2021 at 19:50):

I thought you wanted to infer the argument to Term, not a Type.

Paolo Giarrusso (Nov 11 2021 at 19:51):

making _this example_ work seems a terrible idea.

Paolo Giarrusso (Nov 11 2021 at 19:51):

if you really want…

Paolo Giarrusso (Nov 11 2021 at 19:52):

the proposal wouldn’t be Existing Class nat. It would be Existing Class Type. Existing Instance nat., but it amounts to playing Russian roulette with a nuclear bomb, and it’d probably trigger exciting new bugs.

Lef Ioannidis (Nov 11 2021 at 19:53):

Oh boy, now I understand why you said it would be Russian roulette... What is the priority on instance resolution, after typechecking I suppose so x above still works?

Paolo Giarrusso (Nov 11 2021 at 19:55):

I haven’t memoized enough of the Coq semantics to predict what happens when fuzzing it.

Paolo Giarrusso (Nov 11 2021 at 19:55):

is this the actual example or did you have in mind some other application?

Paolo Giarrusso (Nov 11 2021 at 19:56):

in your original example, if you had Term : nat -> Type, I’d have considered creating a _new_ type Class myNat := { unwrap : nat }. and changing Term to Term : myNat -> Type.

Paolo Giarrusso (Nov 11 2021 at 19:56):

but if Term : my_new_type -> Type maybe you’d be fine.

Paolo Giarrusso (Nov 11 2021 at 19:58):

another option is to just change settings so that Definition t := nil. works but produces a polymorphic term — like with @nil. That’s easier (by changing which arguments are implicit) but it also breaks clients of the existing definition (especially if you really want to tune nil !)

Paolo Giarrusso (Nov 11 2021 at 19:59):

anyway, the TLDR is that inference of implicit arguments of type T (above, T := Type) happens only via unification not via hints, except if T is a typeclass.

Lef Ioannidis (Nov 11 2021 at 19:59):

Paolo Giarrusso said:

in your original example, if you had Term : nat -> Type, I’d have considered creating a _new_ type Class myNat := { unwrap : nat }. and changing Term to Term : myNat -> Type.

That is a very good idea, that would restrict the impact area to only occurences of myNat. I will try this!

Paolo Giarrusso (Nov 11 2021 at 20:00):

for typeclasses, I think instance search is always tried and I don’t think unification _can_ be used.

Paolo Giarrusso (Nov 11 2021 at 20:00):

if TC search fails you get an error, full stop.

Paolo Giarrusso (Nov 11 2021 at 20:00):

but you _can_ override it by hand

Paolo Giarrusso (Nov 11 2021 at 20:01):

you’ll want to take a look at the manual section on typeclasses tho (or a better reference, not sure which?), TCs can be tricky.

Gaëtan Gilbert (Nov 11 2021 at 20:02):

Paolo Giarrusso said:

for typeclasses, I think instance search is always tried and I don’t think unification _can_ be used.

that's wrong

Paolo Giarrusso (Nov 11 2021 at 20:03):

What are the rules? I wasn’t sure but I thought you get an error if TC search fails?

Paolo Giarrusso (Nov 11 2021 at 20:04):

Or is that only if TC search and unification both fail?

Paolo Giarrusso (Nov 11 2021 at 20:05):

I guess I made that up, but I’m not sure I’ve ever seen a case where trying both was useful; and in Agda implicit arguments and typeclass arguments are completely separate language constructs.

Gaëtan Gilbert (Nov 11 2021 at 20:05):

in coq typeclasses are a way to solve evars
unification is another way
implicit arguments automatically insert holes which get turned into evars

Paolo Giarrusso (Nov 11 2021 at 20:08):

Okay, but which is tried first?

Paolo Giarrusso (Nov 11 2021 at 20:08):

At least in Gallina, I mean.

Gaëtan Gilbert (Nov 11 2021 at 20:11):

they are interleaved
consider Definition foo : typ := body.
while elaborating typ unification problems appear
when one fails we try solving TC then retry the unification (hoping that solving TC gave us more info)
once we're done with typ we solve typeclasses in non-failing mode
then we do body similarly but at the end we solve in failing mode, meaning if there are any unsolvable evars we error

Gaëtan Gilbert (Nov 11 2021 at 20:13):

see also https://github.com/coq/coq/issues/13170

Paolo Giarrusso (Nov 11 2021 at 20:28):

Interesting examples...

Paolo Giarrusso (Nov 11 2021 at 20:29):

And to correct what I said above, unification can infer TC instances in reasonable scenarios; you just need to use typeclasses in "proof relevant" ways.

Paolo Giarrusso (Nov 11 2021 at 20:32):

for instance this will likely happen already in Class foo := { fooT : Type; union: fooT -> fooT -> fooT …}. … forall {foo0 : foo} (a : fooT foo0) b, union b a = union a b

Lef Ioannidis (Nov 11 2021 at 21:46):

So just to make sure I understand, unification of evars will call TC, only for types for which a class is relevant (ie: Existing Class). Then TC can do eauto so hints affect it. But not in the general setting of unifying evars for which there are no relevant classes, correct?

Gaëtan Gilbert (Nov 11 2021 at 21:53):

unification doesn't call tc except when it would otherwise error

Last updated: Oct 13 2024 at 01:02 UTC