Make Monad_stateT a local instance

[jadephilipoom]

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]

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]

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]

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]

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

[liyishuai]

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]

Comment and example are now added!

[Lysxia]

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?

[jadephilipoom]

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.

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

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]

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]

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

[jadephilipoom]

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

[Lysxia]

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.

[lthms]

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

[liyishuai]

Propose merging on Wednesday if no more concerns arise.