From 4d4e467392207d05dbedae4daf1563e7cd95560e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 21 Mar 2024 10:01:13 +0100 Subject: [PATCH] feat: `MonadAlwaysExcept` for `MonadCacheT` (#3726) --- src/Lean/Util/Trace.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index b5bbd6a8be..9cf33d0981 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -189,18 +189,22 @@ really need to handle (and then re-throw) every exception lest we end up with a class MonadAlwaysExcept (ε : outParam (Type u)) (m : Type u → Type v) where except : MonadExceptOf ε m --- instance sufficient for inferring `MonadAlwaysExcept` for the elaboration monads +-- instances sufficient for inferring `MonadAlwaysExcept` for the elaboration monads -instance (ε) : MonadAlwaysExcept ε (EIO ε) where +instance : MonadAlwaysExcept ε (EIO ε) where except := inferInstance -instance (ε) [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateT σ m) where +instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateT σ m) where except := let _ := always.except; inferInstance -instance (ε) [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateRefT' ω σ m) where +instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (StateRefT' ω σ m) where except := let _ := always.except; inferInstance -instance (ε) [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (ReaderT ρ m) where +instance [always : MonadAlwaysExcept ε m] : MonadAlwaysExcept ε (ReaderT ρ m) where + except := let _ := always.except; inferInstance + +instance [always : MonadAlwaysExcept ε m] [STWorld ω m] [BEq α] [Hashable α] : + MonadAlwaysExcept ε (MonadCacheT α β m) where except := let _ := always.except; inferInstance def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls : Name)