From a2002540de4821769bce66a9044e157444104e38 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 3 May 2023 12:34:25 -0700 Subject: [PATCH] Add bidi type inference to monad class constructors This improves error messages when the fields are messed up. --- utils/theories/monad_utils.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/utils/theories/monad_utils.v b/utils/theories/monad_utils.v index e417e82ba..fde6782b3 100644 --- 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.