Compiler accepts DivBy with impossible

[Riateche]

div_by_crash.idr.zip

Steps to Reproduce

import Data.Primitives.Views

total
bad: Int -> Int
bad x with (divides x 2)
  bad (_ + _) | (DivBy _) impossible

Expected Behavior

This should be a valid case. The function should not be considered total.

Observed Behavior

The compiler accepts this as a total function. It crashes at run time.

[Riateche]

Can I get any confirmation or update on this?