Demonstrates how trying to match against a runtime-determined value in a case seems to always pick that as the match

MysteriouslyUnreachableCase.idr

{-
> idris --execute MysteriouslyUnreachableCase.idr
MysteriouslyUnreachableCase.idr:17:10:warning - Unreachable case: case block in thingFromInt n rawA n
ok? False
-}
data Thing = A | AAAA


thingToInt : Thing -> Int
thingToInt thing =
    case thing of
        A =>
            1

        AAAA =>
            2


thingFromInt : Int -> Thing
thingFromInt n =
    let rawA = (thingToInt A) in
    case n of
        rawA =>
            A

        -- ???: Why is this case block unreachable?
        _ =>
            AAAA


isAAAA : Thing -> Bool
isAAAA thing =
        case thing of
            AAAA =>
                True

            _ =>
                False


main : IO ()
main = do
    let int = 2
    let thing = thingFromInt int
    let ok = isAAAA thing
    putStrLn $ "ok? " ++ (show ok)

Discussed this on IRC at freenode/#idris with lightandlight. If you convert thingFromInt's definition to repeat the function name rather than using a case, like so:

thingFromInt : Int -> Thing
thingFromInt (thingToInt A) = A
thingFromInt _ = AAAA

Then you get an error, rather than a warning:

Type checking ./foo.idr
foo.idr:10:14:When checking left hand side of thingFromInt:
Can't match on thingFromInt (thingToInt A)

It looks like this just isn't doable as such. If I implemented Eq, then I could probably do an if/then/if/then thing.

The simplest solution for bridging C enums back and forth between a case and an Int seems to be to use an association list plus lookup and just swap the pairs around to look up the other way. This has the benefit of making it easier to do the right thing with Maybe vs just substituting in a default, as I did for laziness.