Stream: Coq users

Topic: Existential variable hint


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 19:16):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 19:50):

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

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 19:51):

making _this example_ work seems a terrible idea.

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 19:51):

if you really want…

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 19:55):

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

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 19:55):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 19:56):

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

view this post on Zulip 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 !)

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 20:00):

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

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 20:00):

but you _can_ override it by hand

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 20:04):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 20:08):

Okay, but which is tried first?

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 20:08):

At least in Gallina, I mean.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Nov 11 2021 at 20:13):

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

view this post on Zulip Paolo Giarrusso (Nov 11 2021 at 20:28):

Interesting examples...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Nov 11 2021 at 21:53):

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


Last updated: Feb 08 2023 at 23:03 UTC