From 889ac541c305388bbbbbed632c2e4cd292d63c11 Mon Sep 17 00:00:00 2001
From: Li-yao Xia <lysxia@gmail.com>
Date: Mon, 21 Mar 2022 19:53:23 -0400
Subject: [PATCH] Add Hint Mode to Functor, Applicative, Monad

---
 theories/Data/Monads/EitherMonad.v |  2 +-
 theories/Data/Monads/OptionMonad.v |  2 +-
 theories/Structures/Applicative.v  |  2 ++
 theories/Structures/Functor.v      |  2 ++
 theories/Structures/Monad.v        |  2 ++
 theories/Structures/MonadLaws.v    |  4 ++--
 theories/Structures/Traversable.v  | 10 +++++-----
 7 files changed, 15 insertions(+), 9 deletions(-)

diff --git a/theories/Data/Monads/EitherMonad.v b/theories/Data/Monads/EitherMonad.v
index de969c2a..8c9a53b3 100644
--- a/theories/Data/Monads/EitherMonad.v
+++ b/theories/Data/Monads/EitherMonad.v
@@ -70,7 +70,7 @@ Section except.
   }.
 
   Global Instance MonadT_eitherT : MonadT eitherT m :=
-  { lift := fun _ c => mkEitherT (liftM ret c) }.
+  { lift := fun _ c => mkEitherT (liftM inr c) }.
 
   Global Instance MonadState_eitherT {T} (MS : MonadState T m) : MonadState T eitherT :=
   { get := lift get
diff --git a/theories/Data/Monads/OptionMonad.v b/theories/Data/Monads/OptionMonad.v
index 752b4f43..8627eac4 100644
--- a/theories/Data/Monads/OptionMonad.v
+++ b/theories/Data/Monads/OptionMonad.v
@@ -54,7 +54,7 @@ Section Trans.
   { mzero _A := mkOptionT (ret None) }.
 
   Global Instance MonadT_optionT : MonadT optionT m :=
-  { lift _A aM := mkOptionT (liftM ret aM) }.
+  { lift _A aM := mkOptionT (liftM Some aM) }.
 
   Global Instance State_optionT {T} (SM : MonadState T m) : MonadState T optionT :=
   { get := lift get
diff --git a/theories/Structures/Applicative.v b/theories/Structures/Applicative.v
index a395b2b4..7a9ba3f1 100644
--- a/theories/Structures/Applicative.v
+++ b/theories/Structures/Applicative.v
@@ -10,6 +10,8 @@ Class Applicative@{d c} (T : Type@{d} -> Type@{c}) :=
 ; ap : forall {A B : Type@{d}}, T (A -> B) -> T A -> T B
 }.
 
+Global Hint Mode Applicative ! : typeclass_instances.
+
 Module ApplicativeNotation.
   Notation "f <*> x" := (ap f x) (at level 52, left associativity).
 End ApplicativeNotation.
diff --git a/theories/Structures/Functor.v b/theories/Structures/Functor.v
index 2c1096ad..4ac3a761 100644
--- a/theories/Structures/Functor.v
+++ b/theories/Structures/Functor.v
@@ -6,6 +6,8 @@ Set Strict Implicit.
 Polymorphic Class Functor@{d c} (F : Type@{d} -> Type@{c}) : Type :=
 { fmap : forall {A B : Type@{d}}, (A -> B) -> F A -> F B }.
 
+Global Hint Mode Functor ! : typeclass_instances.
+
 Polymorphic Definition ID@{d} {T : Type@{d}} (f : T -> T) : Prop :=
   forall x : T, f x = x.
 
diff --git a/theories/Structures/Monad.v b/theories/Structures/Monad.v
index 2b500330..695d432d 100644
--- a/theories/Structures/Monad.v
+++ b/theories/Structures/Monad.v
@@ -10,6 +10,8 @@ Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
 ; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
 }.
 
+Global Hint Mode Monad ! : typeclass_instances.
+
 Section monadic.
 
   Definition liftM@{d c}
diff --git a/theories/Structures/MonadLaws.v b/theories/Structures/MonadLaws.v
index a95e10fd..3be836d0 100644
--- a/theories/Structures/MonadLaws.v
+++ b/theories/Structures/MonadLaws.v
@@ -40,9 +40,9 @@ Section MonadLaws.
     Context {S : Type}.
 
     Class MonadStateLaws  (MS : MonadState S m) : Type :=
-    { get_put : bind get put = ret tt
+    { get_put : bind get put = ret tt :> m unit
     ; put_get : forall x : S,
-        bind (put x) (fun _ => get) = bind (put x) (fun _ => ret x)
+        bind (put x) (fun _ => get) = bind (put x) (fun _ => ret x) :> m S
     ; put_put : forall {A} (x y : S) (f : unit -> m A),
         bind (put x) (fun _ => bind (put y) f) = bind (put y) f
     ; get_get : forall {A} (f : S -> S -> m A),
diff --git a/theories/Structures/Traversable.v b/theories/Structures/Traversable.v
index faae54ce..eb59141f 100644
--- a/theories/Structures/Traversable.v
+++ b/theories/Structures/Traversable.v
@@ -10,13 +10,13 @@ Polymorphic Class Traversable@{d r} (T : Type@{d} -> Type@{r}) : Type :=
 }.
 
 Polymorphic Definition sequence@{d r}
-            {T : Type@{d} -> Type@{d}}
+            {T : Type@{d} -> Type@{r}}
             {Tr:Traversable T}
-            {F : Type@{d} -> Type@{d}} {Ap:Applicative F} {A : Type@{d}}
-  : T (F A) -> F (T A) := mapT (@id _).
+            {F : Type@{d} -> Type@{r}} {Ap:Applicative F} {A : Type@{d}}
+  : T (F A) -> F (T A) := mapT (@id (F A)).
 
 Polymorphic Definition forT@{d r}
-            {T : Type@{d} -> Type@{d}}
-            {Tr:Traversable T} {F : Type@{d} -> Type@{d}} {Ap:Applicative F}
+            {T : Type@{d} -> Type@{r}}
+            {Tr:Traversable T} {F : Type@{d} -> Type@{r}} {Ap:Applicative F}
             {A B : Type@{d}} (aT:T A) (f:A -> F B) : F (T B)
 := mapT f aT.