Case split causes my function to no longer be covering

[FFFluoride]

Gist with minimal example

Steps to Reproduce

Case split on prf here

Expected Behavior

Case splits and decideWord is still covering after reloading.

Observed Behavior

decideWord is no longer covering

Error for reference:

- + Errors (1)
 `-- src/Test.idr line 9 col 0:
     decideWord is not covering.

     Test:9:1--9:80
      5 | 
      6 | data WordValidInput : Type -> Type where
      7 |   MkWordValidInput : (word : List Char) -> WordValidInput (Elem ' ' word -> Void)
      8 | 
      9 | decideWord : (word : List Char) -> Dec (WordValidInput (Elem ' ' word -> Void))
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

     Calls non covering function Test.case block in decideWord

[andrevidela]

what's the result of case-splitting?

[FFFluoride]

Refl I don't know if you want this but here's a gist it's almost exactly the same though

[CodingCellist]

Shrunk further:

decFn : (x : Char) -> Dec (x === ' ') -> ()
decFn ' ' (Yes Refl) = ?decFn_rhs_0
decFn x (No contra) = ?decFn_rhs_1

-----
-- Issue3364> :r
-- 1/1: Building Issue3364 (Issue3364.idr)
-- Error: isChEq is not covering.
--
-- Issue3364:8:1--8:45
--  4 | import Decidable.Equality
--  5 |
--  6 | %default covering
--  7 |
--  8 | isChEq : (x : Char) -> Dec (x === ' ') -> ()
--      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
--
-- Missing cases:
--     isChEq _ (Yes _)

Wat. :raised_eyebrow:

[gallais]

I get a different error @CodingCellist

- + Errors (1)
 `-- Issue3364.idr line 6 col 0:
     While processing left hand side of decFn. When unifying:
         fromChar ' '
     and:
         '='
     Mismatch between: ' ' and '='.

after fixing that typo, you can inspect :di decFn and see that the case splitter starts by casing on the Char hence the need for a catchall.

λΠ> :di decFn
Main.decFn
Arguments [{arg:0}, {arg:1}]
Compile time tree: case {arg:0} : Char of
  ' ' => case {arg:1} : Dec ({arg:0} = fromChar ' ') of
    Yes {e:2} {e:3} => case {e:3} : ' ' = fromChar ' ' of
      Refl {e:4} {e:5} => ?decFn_rhs_0 [no locals in scope]
      _ => case {arg:1} : Dec ({arg:0} = fromChar ' ') of
        No {e:0} {e:1} => ?decFn_rhs_1 [locals in scope: {arg:0}, {e:1}]
    _ => case {arg:1} : Dec ({arg:0} = fromChar ' ') of
      No {e:0} {e:1} => ?decFn_rhs_1 [locals in scope: {arg:0}, {e:1}]
  _ => case {arg:1} : Dec ({arg:0} = fromChar ' ') of
    No {e:0} {e:1} => ?decFn_rhs_1 [locals in scope: {arg:0}, {e:1}]
Refers to: Main.decFn_rhs_0, Main.decFn_rhs_1
Refers to (runtime): Main.decFn_rhs_0, Main.decFn_rhs_1, prim__crash
Flags: covering

As always, you can fix the issue in various ways:

1. guide the splitter by making the char erased

   decFn : (0 x : Char) -> Dec (x === ' ') -> ()

2. mark the pattern as forced

   decFn .(' ') (Yes Refl) = ?decFn_rhs_0

Of course that's harder to do in a case where you don't get to repeat the LHS...