Add more program structure to abstract terms.

Add more program structure to type inference and checking.

1 files changed, 5 insertions, 2 deletions

diff --git a/src/Obs/Logging.idr b/src/Obs/Logging.idr
index ef0bae6..5666001 100644
--- a/src/Obs/Logging.idr
+++ b/src/Obs/Logging.idr
@@ -126,8 +126,11 @@ inScope : (tag : String) -> Logging ann a -> Logging ann a
 inScope tag = mapMsg {tags $= (tag ::)}
 
 export
-inBounds : Bounds -> Logging ann a -> Logging ann a
-inBounds bounds = mapMsg {bounds $= maybe (Just bounds) Just}
+inBounds : WithBounds (Logging ann a) -> Logging ann a
+inBounds msg =
+  let map : Logging ann a -> Logging ann a
+      map = if msg.isIrrelevant then id else mapMsg {bounds $= maybe (Just msg.bounds) Just}
+  in map msg.val
 
 public export
 interface Loggable (0 ann, ty : Type) where