@@ -168,6 +168,11 @@ data EffM : (m : Type -> Type) -> (x : Type)
168 liftP : (prf : SubList ys xs) ->
168 liftP : (prf : SubList ys xs) ->
169 EffM m t ys ys' -> EffM m t xs (\v => updateWith (ys' v) xs prf)
169 EffM m t ys ys' -> EffM m t xs (\v => updateWith (ys' v) xs prf)
171+ new : Handler e' m => (e : EFFECT) -> resTy ->
172+ {auto prf : e = MkEff resTy e'} ->
173+ EffM m t (e :: es) (\v => e :: es) ->
174+ EffM m t es (\v => es)
171 (:-) : (l : ty) ->
176 (:-) : (l : ty) ->
172 EffM m t [x] xs' -> -- [x] (\v => xs) ->
177 EffM m t [x] xs' -> -- [x] (\v => xs) ->
173 EffM m t [l ::: x] (\v => map (l :::) (xs' v))
178 EffM m t [l ::: x] (\v => map (l :::) (xs' v))
@@ -263,6 +268,8 @@ eff env (callP prf effP) k = execEff env prf effP k
263eff env (liftP prf effP) k
268eff env (liftP prf effP) k
264 = let env' = dropEnv env prf in
269 = let env' = dropEnv env prf in
265 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
270 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
271+eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k
272+ = eff (res :: env) effP (\p', (val :: envk) => k p' envk)
267-- xs is needed explicitly because otherwise the pattern binding for
274-- xs is needed explicitly because otherwise the pattern binding for
268-- 'l' appears too late. Solution seems to be to reorder patterns at the
275-- 'l' appears too late. Solution seems to be to reorder patterns at the