@@ -286,7 +286,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
286286 -- block reduction immediately under codata (and not forced)
287287 ev ntimes stk top env
288288 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
289− | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl
289+ | dly == txt "Delay" && lco == txt "LazyCodata" && not (simpl || atRepl)
290290 = do let (f, _) = unApply arg
291291 let ntimes' = case f of
292292 P _ fn _ -> (fn, 0) : ntimes