Idris 0.9.18 bug?

bug_test.idr

module Test

a : (String -> Either String String) -> String
a b =
	case b of
		Left err => err
		Right v => v

compiler_output.txt

error-test.idr:6:22:
When elaborating left hand side of Test.case block in a:
Can't unify
        Either a b (Type of Left _)
with
        String -> Either String String (Expected type)

Specifically:
        Can't unify
                Either a
        with
                \uv => String -> uv

the error is on line 5 though

The error is really that what you have on 5 doesn't match what you have on 6 - you're asking for an analysis of a variable with type A, but using patterns that assume it must have type B. IMO, it should feel free to report the error in either or both locations.

OTOH, it should also complain that String -> Either String String isn't a valid type to analyze with case. That would have been more helpful here.

I suppose it's worth a "this error message confused me" report.