Make Monad_stateT a local instance

examples/StateTMonad.v

@@ -0,0 +1,15 @@
+From ExtLib Require Import
+     Monad
+     OptionMonad
+     StateMonad.
+
+(** [Monad_stateT] is not in context, so this definition fails *)
+Fail Definition foo : stateT unit option unit :=
+  ret tt.
+
+(** Use [Existing Instance] to bring the Local [Monad_stateT] instance into context *)
+Existing Instance Monad_stateT.
+
+(** Now the definition succeeds *)
+Definition foo : stateT unit option unit :=
+  ret tt.

examples/_CoqProject

@@ -7,4 +7,5 @@ MonadReasoning.v
 Printing.v
 UsingSets.v
 WithDemo.v
-Notations.v
+Notations.v
+StateTMonad.v

theories/Data/Monads/StateMonad.v

@@ -43,8 +43,10 @@ Section StateType.
   Definition execStateT {t} (c : stateT t) (s : S) : m S :=
     bind (runStateT c s) (fun x => ret (snd x)).
 
-
-  Global Instance Monad_stateT : Monad stateT :=
+  (** [Monad_stateT] is not a Global Instance because it can cause an infinite loop
+     in typeclass inference under certain circumstances. Use [Existing Instance
+     Monad_stateT.] to bring the instance into context. *)
+  Instance Monad_stateT : Monad stateT :=
   { ret := fun _ x => mkStateT (fun s => @ret _ M _ (x,s))
   ; bind := fun _ _ c1 c2 =>
     mkStateT (fun s =>