Stream: Coq devs & plugin devs

Topic: Why is unification right-to-left?


view this post on Zulip Jason Gross (Jul 20 2023 at 19:48):

Am I correct that Coq if Coq tries to unify f x y with f x' y', and y cannot be unified with y', then it gives up, rather than seeing if unifying x with x' resolves some evars in y or y' which would allow unification to succeed? (Why is it this way?)

view this post on Zulip Gaëtan Gilbert (Jul 20 2023 at 19:56):

old unification or evarconv?

view this post on Zulip Gaëtan Gilbert (Jul 20 2023 at 20:00):

I think evarconv is left to right, for instance

Universes u1 u2 v1 v2.
Constraint u1 < v1.
Constraint u2 < v2.

Axiom P : Type -> Type -> Prop -> Prop.

Axiom p : forall T (* needed to avoiding calling unification on evar free application *), P Type@{u1} Type@{u2} T.

Goal P Type@{v1} Type@{v2} True.
  refine (p _).

reports universe inconsistency about u1 = v1 ie the first argument

view this post on Zulip Gaëtan Gilbert (Jul 20 2023 at 20:12):

old unification also seems left to right, but it doesn't substitute the metas while unifying
and may treat defined evars in strange way, see use of EConstr.Unsafe in unification.ml

view this post on Zulip Gaëtan Gilbert (Jul 20 2023 at 20:13):

I think I saw an old comment or commit message which claimed that this was deliberate for performance but I don't remember details

view this post on Zulip Jason Gross (Jul 20 2023 at 20:47):

Which one is used by typeclasses eauto and reported with Set Debug "tactic-unification".?

view this post on Zulip Gaëtan Gilbert (Jul 20 2023 at 21:26):

old


Last updated: Dec 05 2023 at 12:01 UTC