Add Hint Mode to Functor, Applicative, Monad

coq-community · Jan 26, 2024 · d47e472 · andres-erbsen · Jan 27, 2024 · liyishuai
1 parent 961c802
commit d47e472
Show file tree

Hide file tree

Showing 7 changed files with 15 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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.