@@ -254,9 +254,8 @@ execEff : Env m xs -> (p : EffElem e res xs) ->
254254 ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
255255execEff (val :: env) Here eff' k
256256 = handle val eff' (\v, res => k v (res :: env))
257−-- FIXME: Teach the elaborator to propagate parameters here
258−execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
259− = execEff {e} {a} {res} {resk} env p eff (\v, env' => k v (val :: env'))
257+execEff (val :: env) (There p) eff k
258+ = execEff env p eff (\v, env' => k v (val :: env'))
260259
261260-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
262261-- updates can be propagated even through failing computations?
@@ -271,11 +270,7 @@ eff env (liftP prf effP) k
271270 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
272271eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k
273272 = eff (res :: env) effP (\p', (val :: envk) => k p' envk)
274−-- FIXME:
275−-- xs is needed explicitly because otherwise the pattern binding for
276−-- 'l' appears too late. Solution seems to be to reorder patterns at the
277−-- end so that everything is in scope when it needs to be.
278−eff {xs = [l ::: x]} env (l :- prog) k
273+eff env (l :- prog) k
279274 = let env' = unlabel env in
280275 eff env' prog (\p', envk => k p' (relabel l envk))
281276