Add bidi type inference to monad class constructors

This improves error messages when the fields are messed up.
MetaCoq · May 3, 2023 · a200254 · a200254
1 parent 6c63eac
commit a200254
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/utils/theories/monad_utils.v b/utils/theories/monad_utils.v
@@ -12,11 +12,13 @@ Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
 { ret : forall {t : Type@{d}}, t -> m t
 ; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
 }.
+Global Arguments Build_Monad _ & _ _. (* for better type inference and error messages *)
 
 Class MonadExc E (m : Type -> Type) : Type :=
 { raise : forall {T}, E -> m T
 ; catch : forall {T}, m T -> (E -> m T) -> m T
 }.
+Global Arguments Build_MonadExc _ _ & _ _. (* for better type inference and error messages *)
 
 
 Module MCMonadNotation.