Stream: Coq users

Topic: Opaque does not imply Typeclasses Opaque

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...

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.

Paolo Giarrusso (Oct 15 2020 at 04:28):

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

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...

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

Karl Palmskog (Oct 15 2020 at 07:02):

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

Maxime Dénès (Oct 15 2020 at 07:03):

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

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.

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.

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.

Pierre-Marie Pédrot (Oct 15 2020 at 07:50):

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

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:

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.

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.

Paolo Giarrusso (Oct 15 2020 at 17:39):

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

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 _.

Paolo Giarrusso (Oct 15 2020 at 19:02):

And BTW, apparently my theory wasn't accurate

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.

Pierre-Marie Pédrot (Oct 15 2020 at 20:22):

Surprising indeed.

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

Janno (Oct 16 2020 at 09:11):

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

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.

Maxime Dénès (Oct 16 2020 at 09:35):

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

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)

Maxime Dénès (Oct 16 2020 at 09:36):

you get something fast and predictible

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.

Maxime Dénès (Oct 16 2020 at 09:36):

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

Janno (Oct 16 2020 at 09:37):

@Christian Doczkal Okay, got it!

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..

Janno (Oct 16 2020 at 09:39):

(In our code base, I should add!)

Maxime Dénès (Oct 16 2020 at 09:40):

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

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

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

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

Janno (Oct 16 2020 at 09:42):

Yup :(

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

Janno (Oct 16 2020 at 11:37):

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

Last updated: Sep 25 2023 at 12:01 UTC