Error in IDE mode when case splitting on functions that have Effect in signature

[Termina1]

Tried with version 1.0-git:e371823.
The minimal example to reproduce this bug:

import Effects
import Effect.StdIO

test : List Int -> Eff () [STDIO]
test xs = printLn "test"

If you try to case-split on xs you will get the following error:

builtin:Elaborating {__infer_0} arg {ival_0}: CantUnify False (Effects.EffM {m_508} Unit (Prelude.List.:: Effects.EFFECT (Effects.MkEff Unit Effect.StdIO.StdIO) (Prelude.List.Nil Effects.EFFECT)) (\ v : Unit => Prelude.List.:: Effects.EFFECT (Effects.MkEff Unit Effect.StdIO.StdIO) (Prelude.List.Nil Effects.EFFECT)),Just (SourceTerm Main.test {__pi_arg_507} {m_508})) and ({__argTy_103} -> {__retTy_104},Just (TooManyArgs Main.test {__pi_arg_507} {m_508})) CantUnify False (Effects.EffM {m_508} Unit (Prelude.List.:: Effects.EFFECT (Effects.MkEff Unit Effect.StdIO.StdIO) (Prelude.List.Nil Effects.EFFECT)),Nothing) and (\ {uv_0} : Type .a => {__argTy_103} -> {uv_0},Nothing)  in [({m_508},Type 0 -> Type 0),({__pi_arg_507},Prelude.List.List Int),({__retTy_104},Type 0),({__argTy_103},Type 0),({iType_101},Type 0)] 1 in [({m_508},Type 0 -> Type 0),({__pi_arg_507},Prelude.List.List Int),({__retTy_104},Type 0),({__argTy_103},Type 0),({iType_101},Type 0)] 1

It can be reproduced in Atom and VS Code IDE modes, so I believe it is an issue of the compiler itself. I opened a similar issue for the atom plugin, since it doesn't show error text (idris-hackers/atom-language-idris#154).

[ahmadsalim]

Thanks for reporting the issue.