Prove two values are equal from case statement

Question

The following example uses Data.Bin from the Bi package:

import Data.Bin

foo : (x, y : Bin) -> Dec (binCompare x y = LT)
foo x y = case binCompare x y of
    LT => Yes (C1 ?hole1)
    EQ => ...
    GT => ...

:t ?hole1
binCompare x y = LT

How can I get a proof that binCompare x y = LT when handling the LT case?

Answer 1

You need to use a view instead of a case:

Since types can depend on values, the form of some arguments can be determined by the value of others.

So the below version works as expected:

foo : (x, y : Bin) -> Dec (binCompare x y = LT)
foo x y with (binCompare x y)
  foo x y | LT = Yes Refl
  foo x y | EQ = ?q_2
  foo x y | GT = ?q_3