Creates a case where you don't use the results fails to type check sometimes

[redfish64]

This simple example is causing a problem for me, since if I use code resembling monad bind often the result gets ignored (ie. >>) , and so this issue crops up when I use a "case" within my code.

I tried this with v0.2.0 and with 59800e1f

Steps to Reproduce

https://gist.github.com/redfish64/6295c664e69f738bfc608754a325cdf1

foo : Int
foo = 
  let l = True
      lf = case l of 
             True => "1"
             False => "2"
  in
    1

Expected Behavior

OK!

Observed Behavior

• • Errors (1) `-- LearnBug2.idr line 5 col 21: While processing right hand side of foo at LearnBug2.idr:2:1--12:1: Can't solve constraint between: String and ?_ [no locals in scope]

[edwinb]

case is dependent, and it doesn't have enough information to infer the expected type if you don't use it, given that inference for dependent types is undecidable. I know it's clear to a human what you intended here, but the machine has to make an inference for ?caseType False = String and ?caseType True = Stringwhich it can't do in general, even if we did somehow allow this special case.

So this is expected, I'm afraid. I suppose it could be clearer if the message were to say it's trying to unify ?caseType False with String.

[gallais]

Nowadays the error message is slightly different:

Error: While processing right hand side of foo. Can't find an implementation for FromString ?_.

but is still not the clearest. It would be nice to be able to detect we are in a "infer the type of a case block" situation and give users a hint that they may want to add an annotation.

[gallais]

since if I use code resembling monad bind often the result gets ignored (ie. >>)

Note that nowadays (>>) has type Monad m => m () -> m a -> m a forcing the first argument to be of type m () which should help with inference.