Stream: Coq users

Topic: Opaque does not imply Typeclasses Opaque


view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 04:27):

I've got the following script to work, on a goal involving foo, which is declared as Global Opaque but not typeclass opaque. I used to expect that Opaque implies Typeclasses Opaque, and I thought I had confirmed that with somebody more competent than me. But that was foolish:

    apply _. (* succeeds on `SomeTC (... foo ... *)  *)
    Undo.
    Transparent foo. (* needed to mark foo as Typeclasses Opaque. *)
    Typeclasses Opaque foo.
    Opaque foo.
    Fail apply _.

I understand that Opaque and TC Opaque affect different unification algorithms, but this is still surprising...

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 04:27):

worse, if you try Typeclasses Opaque foo. when foo is Opaque, you get Cannot coerce only_provable to an evaluable reference.

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 04:28):

which is weird, since Opaque doesn't imply TC opaqueness...

view this post on Zulip Maxime Dénès (Oct 15 2020 at 06:52):

We could base the scenario of a horror movie on the current status of opacity in Coq...

view this post on Zulip Maxime Dénès (Oct 15 2020 at 06:53):

It would be worth opening an issue so that we clarify this Opaque vs TC Opaque status

view this post on Zulip Karl Palmskog (Oct 15 2020 at 07:02):

sounds like a commercial: "you may be opaque, but are you type class opaque?"

view this post on Zulip Maxime Dénès (Oct 15 2020 at 07:03):

I'm not convinced by the business plan behind it :D

view this post on Zulip Théo Zimmermann (Oct 15 2020 at 07:48):

There's a third Opaque command which is Hint Opaque. Typeclass Opaque is equivalent to Hint Opaque ... : typeclass_instances.

view this post on Zulip Théo Zimmermann (Oct 15 2020 at 07:49):

But Opaque itself is not respected by all the apply variants, so if it's not respected by autoapply, then it's not respected by typeclasses eauto.

view this post on Zulip Pierre-Marie Pédrot (Oct 15 2020 at 07:50):

I had a look recently at the implementation of hint opacity and the least I can say is that it's a tad peculiar.

view this post on Zulip Pierre-Marie Pédrot (Oct 15 2020 at 07:50):

Thus I am not surprised we can have this kind of behaviours.

view this post on Zulip Christian Doczkal (Oct 15 2020 at 08:28):

My two cents: I think that calling it "opaque" in the first place is a bit of a misnomer given that conversion must always be allowed to ignore (a posteriori) "opacity" changes in order to preserve well-typedness of existing definitions. Maybe calling it "translucent" (in the sense of: you can look through it, but it's not quite transparent) would be more honest. :shrug:

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 17:37):

For extra fun: making foo TC opaque seems to make a difference even if foo is an axiom.

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 17:38):

if foo is TC opaque, it seems that instances for SomeTC (foo ...) are tested using syntactic matching.

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 17:39):

if foo is TC transparent, instances for SomeTC (foo ...) are tested using some form of unification.

view this post on Zulip Janno (Oct 15 2020 at 18:54):

Here's the outcome of debugging this issue and you all get to enjoy the results in the form of a little quiz! Which apply _ call works? A, B, both, or neither?

Class A (n : nat) := {}.
Definition three := 3.
Instance A_three : A three := {}.
Definition three' := if true then three else 1.
Hint Opaque three : typeclass_instances.
(* A *) Goal A (three'). apply _.
(* B *) Goal A (if true then three else 1). apply _.

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 19:02):

And BTW, apparently my theory wasn't accurate

view this post on Zulip Pierre-Marie Pédrot (Oct 15 2020 at 20:20):

I'd wager that B works but not A, but I am too lazy to test this.

view this post on Zulip Pierre-Marie Pédrot (Oct 15 2020 at 20:22):

Surprising indeed.

view this post on Zulip Christian Doczkal (Oct 16 2020 at 09:10):

Well, "syntactic" matching against ifs/matches that can reduce can lead to all kinds of strange behaviors, depending on the unification algorithm used. See this wonderful issue for instance: https://github.com/math-comp/math-comp/issues/549

view this post on Zulip Janno (Oct 16 2020 at 09:11):

@Pierre-Marie Pédrot your guess is correct!

view this post on Zulip Janno (Oct 16 2020 at 09:16):

@Christian Doczkal I wouldn't say that TC search really counts as a syntactic matching procedure. In general it will attempt to unify all sorts of things unless the user opts out. The only thing I can think of that is unconditionally syntactic about it is the way that it uses the Class itself as an index. Everything after that (by default) is much closer to full (tactic) unification than it is to syntactic matching AFAICT.

view this post on Zulip Maxime Dénès (Oct 16 2020 at 09:35):

yeah but I'm starting to believe it should be the contrary

view this post on Zulip Maxime Dénès (Oct 16 2020 at 09:36):

by default, you probably want only first order unification in proof search (no conversion, no non-unique HO solutions)

view this post on Zulip Maxime Dénès (Oct 16 2020 at 09:36):

you get something fast and predictible

view this post on Zulip Christian Doczkal (Oct 16 2020 at 09:36):

@Janno , I wasn't implying that TC search is syntactic. I was merely saying that even for the "syntactic" matching (a la rewrite) your (if true ...) actually looks like a three if the algorithm used the one from evarconv.ml.

view this post on Zulip Maxime Dénès (Oct 16 2020 at 09:36):

then if you want search to sometimes do conversion, you can opt in

view this post on Zulip Janno (Oct 16 2020 at 09:37):

@Christian Doczkal Okay, got it!

view this post on Zulip Janno (Oct 16 2020 at 09:39):

@Maxime Dénès I agree wholeheartedly and I proactively extend my deepest condolences to whoever ends up implementing that change. I have tried to carefully make certain things Hint Opaque in typeclass_instances and the breakage seemed quite catastrophic..

view this post on Zulip Janno (Oct 16 2020 at 09:39):

(In our code base, I should add!)

view this post on Zulip Maxime Dénès (Oct 16 2020 at 09:40):

yeah, I'm not surprised given what we already see when working on unifall

view this post on Zulip Maxime Dénès (Oct 16 2020 at 09:41):

people happily rely on proof search finding a specific non-unique solution (so they rely critically on the order), don't properly define abstractions, etc

view this post on Zulip Maxime Dénès (Oct 16 2020 at 09:41):

it's a chicken-and-egg pb, because the language pushes users to do things that don't scale

view this post on Zulip Maxime Dénès (Oct 16 2020 at 09:41):

but once it is done, it is hard to make improvements without catastrophic breakage as you write

view this post on Zulip Janno (Oct 16 2020 at 09:42):

Yup :(

view this post on Zulip Maxime Dénès (Oct 16 2020 at 09:42):

but ok, maybe the way out is to pay the price to migrate the existing, and be more careful when designing new features

view this post on Zulip Janno (Oct 16 2020 at 11:37):

I opened an issue about this: https://github.com/coq/coq/issues/13209


Last updated: Jan 29 2023 at 01:02 UTC