diff --git a/examples/StateTMonad.v b/examples/StateTMonad.v
new file mode 100644
index 00000000..fb8081a2
--- /dev/null
+++ b/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.
diff --git a/examples/_CoqProject b/examples/_CoqProject
index 4998808e..f6ed9c07 100644
--- a/examples/_CoqProject
+++ b/examples/_CoqProject
@@ -7,4 +7,5 @@ MonadReasoning.v
 Printing.v
 UsingSets.v
 WithDemo.v
-Notations.v
\ No newline at end of file
+Notations.v
+StateTMonad.v
diff --git a/theories/Data/Monads/StateMonad.v b/theories/Data/Monads/StateMonad.v
index af50696a..24485848 100644
--- a/theories/Data/Monads/StateMonad.v
+++ b/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 =>