Case splitting stops working when using Effects

[Termina1]

Hi, if I use Eff in type of function declaration case splitting stops working. I debugged and go the error message. I'm not sure it is a bug of package, but it least this error should appear somewhere:

"builtin:Elaborating {__infer0} arg {ival0}: 
CantUnify False (Effects.EffM {m508} Unit 
(Prelude.List.:: Effects.EFFECT Effect.StdIO.STDIO (Prelude.List.Nil Effects.EFFECT)) 
(\ v : Unit => Prelude.List.:: Effects.EFFECT Effect.StdIO.STDIO (Prelude.List.Nil Effects.EFFECT)),
Just (SourceTerm Main.test {__pi_arg507} {m508})) and ({__argTy103} -> {__retTy104},Just (TooManyArgs Main.test {__pi_arg507} {m508})) 
CantUnify False (Effects.EffM {m508} Unit (Prelude.List.:: Effects.EFFECT 
(Effects.MkEff Unit Effect.StdIO.StdIO) (Prelude.List.Nil Effects.EFFECT)),Nothing) and (\ {uv0} : Type .a => {__argTy103} -> {uv0},Nothing)  
in [({m508},Type 0 -> Type 0),({__pi_arg507},Main.Custom),
({__retTy104},Type 0),({__argTy103},Type 0),({iType101},Type 0)] 1 in [({m508},Type 0 -> Type 0),
({__pi_arg507},Main.Custom),({__retTy104},Type 0),({__argTy103},Type 0),({iType101},Type 0)] 1"

And this is the code that triggers the bug, if you try case-split on x:

import Effects
import Effect.StdIO

data Custom = First | Second

test : Custom -> Eff () [STDIO]
test x = ?test_rhs

[justjoheinz]

I am currently not sure if we can get access to this error message. emacs does, so we should be able to do so as well.

Have you already filed a bug with Idiris-dev, as this seems to be an underlying problem?

[Termina1]

@justjoheinz no, I didn't just checked this bug using code from idris master, it still can be reproduced. I will create the issue soon.