Turn pureM into a function

Logic:
```idris
pureM val = with_val val (pure ())
```
Let `val : a`, then
```idris
with_val val : Eff () xs  (\v => xs' val) -> Eff a xs xs'
pure ()      : Eff () xs1 (\v => xs1    )
```
(after α-renaming in the type of `pure ()`). Now unify `xs` = `xs1` = `xs' val` to apply:
```idris
with_val val (pure ()) : Eff a (xs' val) xs'
```
Pulling `val` back out as an argument gives
```idris
pureM : (val : a) -> Eff a (xs' val) xs'
```

The following testcase from eff-tutorial §4.2 continues to work:
```idris
readInt : { [STATE (Vect n Int), STDIO] ==>
            {ok} if ok then [STATE (Vect (S n) Int), STDIO]
                       else [STATE (Vect n Int), STDIO] }
          Eff Bool
readInt = do let x = trim !getStr
             case all isDigit (unpack x) of
                  False => pureM False
                  True => do putM (cast x :: !get)
                             pureM True
```