Non-Exhaustive Pattern Matching

[ThePerfectComputer]

The haskell language server warns about the following pattern - that it is non-exhaustive, however, we know that it is:

blinky :: HiddenClockResetEnable dom => Signal dom (BitVector 1)
blinky = register 0 (fmap toggle curr_state)
  where curr_state   = blinky
        toggle state = case state of
                         0 -> 1
                         1 -> 0

I'm not familiar with the extent of dependent typing in Clash, but shouldn't it be possible to somehow inform the compiler about the possible domain of (BitVector 1)?

I genuinely appreciate when the compiler warns me about non-exhaustive cases, but false positive can decrease signal-to-noise ratio. What HDL would the compiler emit in a non-exhaustive case statement? For example, what would the compiler emit if we only had the 0 -> 1 case arm?

Yehowshua

[martijnbastiaan]

Let's prepend this reply by saying: no, it's currently not possible to inform GHC that your program covers all bases. What follows is an explanation on why this is the way it is, and what we could do in the mid-term to improve this.

---

Let's first have a look at a (seemingly equivalent) program that doesn't generate these warnings:

module D2426A where

import Clash.Prelude

data AB = A | B

isA :: AB -> Bool
isA ab =
  case ab of
    A -> True
    B -> False

By passing -ddump-simpl to Clash (or really, GHC) we can see what GHC makes of it:

isA :: AB -> Bool
[GblId, Arity=1, Unf=OtherCon []]
isA
  = \ (ab_a3yx :: AB) ->
      case ab_a3yx of {
        A -> GHC.Types.True;
        B -> GHC.Types.False
      }

So, plain and simple! GHC can do exhaustiveness checking on this as it can checker whether the constructors A and B are indeed all constructors of AB. Now let's have a look at your program:

module D2426 where

import Clash.Prelude

top :: BitVector 1 -> BitVector 1
top bv =
  case bv of
    0 -> 1
    1 -> 0

This generates:

top :: BitVector 1 -> BitVector 1
[GblId, Arity=1, Unf=OtherCon []]
top
  = \ (bv_a3JG :: BitVector 1) ->
      case ==
             @(BitVector 1)
             $dEq_r4A2
             bv_a3JG
             (fromInteger @(BitVector 1) $dNum_r4A1 0)
      of {
        False ->
          case ==
                 @(BitVector 1)
                 $dEq_r4A2
                 bv_a3JG
                 (fromInteger @(BitVector 1) $dNum_r4A1 1)
          of {
            False ->
              Control.Exception.Base.patError
                @'GHC.Types.LiftedRep
                @(BitVector 1)
                "D2426.hs:(9,3)-(11,10)|case"#;
            True -> fromInteger @(BitVector 1) $dNum_r4A1 0
          };
        True -> fromInteger @(BitVector 1) $dNum_r4A1 1
      }

If we squint our eyes a bit we can see that it generates:

top bv =
  case bv == 0 of
    False ->
      case bv == 1 of
        False -> error "hey something is wrong"
        True -> 0
    True -> 1

In the end, this is because Int, Signed, Index, etc. don't enumerate all their constructors. Instead they are (at some point) GHC primitives. GHC's exhaustiveness checker works solely on constructors, so we're out of luck.

---

In theory we should be able to come up with a GHC plugin to rewrite (exhaustive) patterns in such a way that GHC ignores it. E.g., we could inject our own error "Unreachable".

Hope this helps.

[DigitalBrains1]

I'm restating one thing from my own reply, and then I will hide that original thread because it accidentally derailed the discussion.

What HDL would the compiler emit in a non-exhaustive case statement? For example, what would the compiler emit if we only had the 0 -> 1 case arm?

The HDL's variant of unkown/X/undefined/.... So '-' for VHDL and 1'bx for Verilog. For the patterns not matched, that is; a 0 would still map to a 1 of course.