Evaluation of effectual functions giving unexpected results

Question

Title is fairly self explanatory. Using this paper as a reference, I have been working out how to properly use effects in Idris. Creating effectual functions seems straightforward, but the actual evaluation of the effectual functions is giving me results I do not expect. For context, if I have the following program:

h1 : Eff Nat [SYSTEM, RND]
h1 = do srand !time
        pure (fromInteger !(rndInt 0 6))

h2 : Eff Nat [SYSTEM]
h2 = pure (fromInteger !time)

h3 : Eff Nat [RND]
h3 = do srand 123456789
        pure (fromInteger !(rndInt 0 6))

runH : IO ()
runH = do
    x <- run h1            -- <---- This one works fine
    --let x = runPure h1   -- <---- This one does not work  << !!!
    y <- run h2            -- <---- This one works fine
    --let y = runPure h2   -- <---- This one does not work  << !!!
    --z <- run h3          -- <---- This one works fine
    let z = runPure h3     -- <---- This one works fine     << ???

    putStrLn $
      "test 1 : " ++ show x ++ "\n" ++
      "test 2 : " ++ show y ++ "\n" ++
      "test 3 : " ++ show z

I would expect to be able to get actual values out of h1, h2, and h3 with runPure, but the compiler will only let me do this for h3. Both h1 and h2 will only compile if they are evaluated with run. The only real differences I see are a) functions with multiple effects cannot use runPure or b) the SYSTEM effect cannot use runPure. Could anyone explain to me why the code above behaves the way it does?

The full error if I choose the line let y = runPure h2 over y <- run h2:

When checking right hand side of runH with 
expected type 
    IO ()
When checking argument env to function Effects.runPure:
Type mismatch between
    Env m [] (Type of [])
and
    Env id [SYSTEM] (Expected type)

Specifically:
Type mismatch between
    []
and
    [SYSTEM]