Allow adding new effects in Eff programs

This is only allowed if there is a handler for all computation contexts
the program could run in. In particular, if the program is in 'Eff'
rather than 'EffT', then it is only valid for 'pure' handlers, like
State.

Note that, as a result, the effects a program can run isn't now limited
to the top level set of effects. In the case of 'pure' effects, such as
State or Rnd, I argue that this is okay. In the case of external effects
such as IO related effects, you can only add effects if the top level
context is impure. Again, I argue that this is okay - if you don't want
to add impure effects, keep the top level context generic.

Also added a test (by way of example) in effects004

idris.cabal

@@ -373,6 +373,10 @@ Extra-source-files:
                        test/effects003/*.idr
                        test/effects003/expected
                        test/effects003/input
+                       test/effects004/run
+                       test/effects004/*.idr
+                       test/effects004/expected
+                       test/effects004/input
 
                        test/error001/run
                        test/error001/*.idr

libs/effects/Effects.idr

@@ -168,6 +168,11 @@ data EffM : (m : Type -> Type) -> (x : Type)
      liftP    : (prf : SubList ys xs) ->
                 EffM m t ys ys' -> EffM m t xs (\v => updateWith (ys' v) xs prf)
 
+     new      : Handler e' m => (e : EFFECT) -> resTy ->
+                {auto prf : e = MkEff resTy e'} ->
+                EffM m t (e :: es) (\v => e :: es) ->
+                EffM m t es (\v => es)
+
      (:-)     : (l : ty) ->
                 EffM m t [x] xs' -> -- [x] (\v => xs) ->
                 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
 eff env (liftP prf effP) k
    = let env' = dropEnv env prf in
          eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
+eff env (new (MkEff resTy newEff) res {prf=Refl} effP) k 
+   = eff (res :: env) effP (\p', (val :: envk) => k p' envk)
 -- FIXME:
 -- xs is needed explicitly because otherwise the pattern binding for
 -- 'l' appears too late. Solution seems to be to reorder patterns at the