Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make Monad_stateT a local instance #106

Merged
merged 3 commits into from
Jan 28, 2021

Conversation

jadephilipoom
Copy link
Contributor

Because Monad_stateT requires a monad argument, it can in some situations create infinite loops in typeclass resolution. My minimized example of the problem:

Require Import Structures.Monad.
Require Import Data.Monads.StateMonad.

Class A (proj : nat -> Type):=
  { m : Type -> Type;
    x : m (proj 1);
  }.

Definition hangs {proj} {a : A proj} {monad : Monad.Monad m} : m (proj 1) := ret x. (* infinite loop *)

The hangs definition is not properly typed (it has type m (m (proj 1)), but I'd still prefer to get a typeclass-resolution error here than to get an infinite loop. The trace from Typeclasses Debug is:

Debug: 1: looking for (A ?proj) with backtracking
Debug: 1.1: exact a on (A ?proj), 0 subgoal(s)
Debug: Finished run 1 of resolution.
Debug: 1: looking for (A ?proj) with backtracking
Debug: 1.1: exact a on (A ?proj), 0 subgoal(s)
Debug: Finished run 1 of resolution.
Debug: 1: looking for (Monad ?m) with backtracking
Debug: 1.1: simple apply Monad_state on (Monad ?m), 0 subgoal(s)
Debug: 2: looking for (A ?proj) with backtracking
Debug: 2: no match for (A ?proj), 1 possibilities
Debug: 1.2: simple apply Monad_stateT on (Monad ?m), 1 subgoal(s)
Debug: 1.2-1 : (Monad ?Goal0)
Debug: 1.2-1: looking for (Monad ?Goal0) with backtracking
Debug: 1.2-1.1: simple apply Monad_state on (Monad ?Goal0), 0 subgoal(s)
Debug: 2: looking for (A ?proj) with backtracking
Debug: 2: no match for (A ?proj), 1 possibilities
Debug: 1.2-1.2: simple apply Monad_stateT on (Monad ?Goal0), 1 subgoal(s)
Debug: 1.2-1.2-1 : (Monad ?Goal1)
Debug: 1.2-1.2-1: looking for (Monad ?Goal1) with backtracking
Debug: 1.2-1.2-1.1: simple apply Monad_state on (Monad ?Goal1), 0 subgoal(s)
Debug: 2: looking for (A ?proj) with backtracking
Debug: 2: no match for (A ?proj), 1 possibilities
Debug: 1.2-1.2-1.2: simple apply Monad_stateT on (Monad ?Goal1), 1 subgoal(s)
Debug: 1.2-1.2-1.2-1 : (Monad ?Goal2)
... <many more lines with the same pattern> ...

Removing the Global modifier from Monad_stateT locally fixes this issue for me, giving me the expected typeclass resolution error instead of the infinite loop. Although the rest of the Monad instances are Global, I think that it might make sense to make an exception for this one.

@liyishuai
Copy link
Member

This change breaks compilation in coq -freespec-core and coq-parsec:

#=== ERROR while compiling coq-parsec.dev =====================================#
# context     2.0.7 | linux/x86_64 | ocaml-base-compiler.4.05.0 | https://coq.inria.fr/opam/extra-dev#2021-01-14 10:00
# path        ~/.opam/4.05.0/.opam-switch/build/coq-parsec.dev
# command     /usr/bin/make -j2
# exit-code   2
# env-file    ~/.opam/log/coq-parsec-2355-ac853a.env
# output-file ~/.opam/log/coq-parsec-2355-ac853a.out
### output ###
# - ?Monad1: Cannot infer the implicit parameter Monad of ret whose type is
# [...]
#   H : Serialize P
#   H0 : forall p q : P, Decidable (p = q)
#   xs : list P
#   x : P
#   xs' : list P
#   u : unit
# 
# make[2]: *** [Makefile.coq:716: theories/Parser.vo] Error 1
# make[1]: *** [Makefile.coq:339: all] Error 2
# make[1]: Leaving directory '/home/coq/.opam/4.05.0/.opam-switch/build/coq-parsec.dev'
# make: *** [Makefile:4: all] Error 2


#=== ERROR while compiling coq-freespec-core.dev ==============================#
# context     2.0.7 | linux/x86_64 | ocaml-base-compiler.4.05.0 | https://coq.inria.fr/opam/extra-dev#2021-01-14 10:00
# path        ~/.opam/4.05.0/.opam-switch/build/coq-freespec-core.dev
# command     ~/.opam/4.05.0/bin/dune build -p coq-freespec-core -j 2
# exit-code   1
# env-file    ~/.opam/log/coq-freespec-core-2355-2e72e2.env
# output-file ~/.opam/log/coq-freespec-core-2355-2e72e2.out
### output ###
# [...]
# - ?Monad1: Cannot infer the implicit parameter Monad of ret whose type is
#   "Monad (instrument Ω ix)" (no type class instance found) in
#   environment:
#   ix, i : interface
#   H : MayProvide ix i
#   Ω : Type
#   c : contract i Ω
#   a : Type
#   e : ix a
#   x : a
#   y : Ω
# 



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-freespec-core dev
| - build coq-parsec        dev

@liyishuai
Copy link
Member

Minimal failing example:

From ExtLib Require Import
     Monad
     OptionMonad
     StateMonad.

Fail Definition foo : stateT unit option unit :=
  ret tt.

The command has indeed failed with message:
Unable to satisfy the following constraints:

?Monad : "Monad (stateT unit option)"

@jadephilipoom
Copy link
Contributor Author

jadephilipoom commented Jan 14, 2021

These failures can be fixed with Existing Instance Monad_stateT; it's up to the regular maintainers whether it's worse to require users of stateT to write Existing Instance or to cause the infinite-looping problem in certain setups for anyone who imports StateMonad (even transitively). If you feel it is not worth the change, I'll just close the PR.

@liyishuai
Copy link
Member

liyishuai commented Jan 14, 2021

I can add that line to Parsec immediately. Will merge if FreeSpec accepts that line as well.

@liyishuai
Copy link
Member

Also, could you document this requirement of Existing Instance by (1) commenting above the line you changed, and (2) adding a code snippet under examples directory?

@jadephilipoom
Copy link
Contributor Author

Comment and example are now added!

examples/StateTMonad.v Outdated Show resolved Hide resolved
theories/Data/Monads/StateMonad.v Outdated Show resolved Hide resolved
examples/StateTMonad.v Outdated Show resolved Hide resolved
examples/StateTMonad.v Outdated Show resolved Hide resolved
@liyishuai liyishuai enabled auto-merge (squash) January 14, 2021 13:48
@Lysxia
Copy link
Contributor

Lysxia commented Jan 14, 2021

That's a pretty far-reaching change. I don't have a concrete objection but it does raise some questions:

  1. Does this practice exist in other projects?
  2. How does it compare to bounding the type class search depth with Set Typeclasses eauto := <depth>
  3. For consistency, shouldn't this change be done to all instances (at least the instances for monad transformers) that take another instance as an argument?

@liyishuai liyishuai disabled auto-merge January 14, 2021 14:45
@jadephilipoom
Copy link
Contributor Author

  1. Does this practice exist in other projects?

I've been on a couple of Coq projects with the rule to avoid Global Instance wherever possible, because it makes it hard for importers to control typeclass resolution.

  1. How does it compare to bounding the type class search depth with Set Typeclasses eauto :=

I'd rather not do this for my use case, since typeclass resolution can for legitimate reasons go fairly deep and this could make resolution unpredictable, where some cases requiring a deep search fail to unify.

@lthms
Copy link
Member

lthms commented Jan 15, 2021

First, thank you for monitoring your dependencies to check whether or not they breaks with PR. This is really neat!

I was a bit surprised to see the content of your PR, and wonder if a different approach would be to put this instance in its own, dedicated module (similarly to what has been done in coq-simple-io for MonadFix). It would be paired with the appropriate warning about its danger.

@jadephilipoom
Copy link
Contributor Author

and wonder if a different approach would be to put this instance in its own, dedicated module (similarly to what has been done in coq-simple-io for MonadFix)

That solution would also work just fine for me! Is it preferred?

@lthms
Copy link
Member

lthms commented Jan 15, 2021

I personnally would find this less cumbersome. I feel like Existing Instance is way more “arcane” compared to importing a module.

@jadephilipoom
Copy link
Contributor Author

What needs to be done for this PR (or some alternative solution) to be merged?

@Lysxia
Copy link
Contributor

Lysxia commented Jan 20, 2021

That's up to @liyishuai, but as another user I think this can just be merged. Even though some of us are apprehensive about this different way of doing things, the motivation is sound and I the trade-off seems worth it.

@liyishuai liyishuai requested a review from gmalecha January 20, 2021 16:26
@lthms
Copy link
Member

lthms commented Jan 25, 2021

I just merged your PR in FreeSpec, so you can move forward with this :). Thanks again for the heads up!

@liyishuai
Copy link
Member

Propose merging on Wednesday if no more concerns arise.

@liyishuai liyishuai merged commit 737425e into coq-community:master Jan 28, 2021
lthms added a commit to lthms/coq-comparse that referenced this pull request Jun 24, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants