ffiidristotality

How to crash on internal bug and force totality

I'm ffi-ing to C and the function I call returns an int to mean gt, eq or lt. I want to crash on anything other than 1, 0 or -1 cos that should never happen. And I'd like Idris to consider 0, 1 and -1 to be exhaustive matches. I tried

prim__compare : Scalar -> Scalar -> Int

Ord Scalar where
  compare x y = case prim__compare x y of
                  -1 => LT
                  0 => EQ
                  1 => GT
                  _ => idris_crash ""

but I get

Error: compare is not covering.

Calls non covering function Builtin.idris_crash
Solution

  • Since the crash can only be due to internal errors, it's reasonable to use assert_total

    Ord Scalar where
  compare x y = case prim__compare x y of
                  -1 => LT
                  0 => EQ
                  1 => GT
                  _ => (assert_total idris_crash) ""