method handle is not total as there are missing cases due to Prelude.Interfaces.case block in divBigInt

[Ptival]

The following code:

module Choose

import Data.Fin
import Data.Vect
import Effects
import Effect.Random

randomElement : (l : List a) -> {ok : NonEmpty l} -> Eff a [RND]
randomElement []     {ok} = absurd ok
randomElement (h::t) {ok} = do
  let vl = fromList (h::t)
  fin <- rndFin $ length t
  pure $ index fin vl

data ChooseEffect : Effect where
  Choose : (l : List a) -> {ok : NonEmpty l} -> sig ChooseEffect a ()

CHOOSE : EFFECT
CHOOSE = MkEff () ChooseEffect

choose : (l : List a) -> {ok : NonEmpty l} -> Eff a [CHOOSE]
choose l {ok} = call $ Choose l {ok}

[chooseRandom] Handler ChooseEffect IO where
  handle () (Choose l {ok}) k = do
    a <- run $ randomElement l {ok}
    k a ()

produces this error:

   |
25 |   handle () (Choose l {ok}) k = do
   |   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
Effects.Choose.chooseRandom, method handle is not total as there are missing cases due to Prelude.Interfaces.case block in divBigInt at ./Prelude/Interfaces.idr:341:22-27

I'm a beginner to Idris, but this error seems spurious to me.