I tried to make a function in Idris like so:
strSplit : String -> Maybe (Char, String)
This would 'un-cons' the string into its first Char and the rest of the string, and return Nothing if it were empty.
So I wrote this, which failed:
strSplit x = case strM of
StrNil => Nothing
StrCons c cd => Just (c, cs)
So I then tried this, a bit like in Prelude.Strings:
strSplit x with (strM x)
strSplit "" | StrNil = Nothing
strSplit (strCons c cs) | (StrCons c cs) = Just (c, cs)
Which compiled and ran with no problems.
My question is, why do I have to use that with rule to split a string in this way, and why does my original method fail?
Note: Sorry, I can't access an interpreter at the moment, so I can't write the error message here yet.
There are two problems here. Firstly, in the 'case' block, the argument is strM rather than strM x as it is in the 'with' block, so you're inspecting different things.
There's a more interesting problem though, which is that if you try fixing the first one:
strSplit : String -> Maybe (Char, String)
strSplit x = case strM x of
StrNil => Nothing
StrCons c cd => Just (c, cs)
You'll get a different error (this is from current master which has reworded error messages):
Type mismatch between
StrM "" (Type of StrNil)
and
StrM x (Expected type)
So the distinction between 'case' and 'with' is that 'with' takes into account that the thing you're inspecting may influence the types and values on the left hand side. In the 'case', matching strM x means that x must be "", but a 'case' can appear anywhere and takes no account of the effect on the types of the other arguments (working out appropriate type checking rules for this would be quite a challenge...).
On the other hand, 'with' can only appear at the top level: effectively what it's doing is adding another top level thing to match on which, being top level, can affect the types and values of the other patterns.
So, the short answer is that 'with' supports dependent pattern matching, but 'case' does not.