Inconsistency: Unfinished function definition hides negative occurences

[jasoncarr0]

Steps to Reproduce

Define an inductive type mutually with a total function that computes a type with negative usages: bad.idr.txt

%default total

neg : Type -> Type
data Bad : Type -> Type where
  CBad : neg a -> Bad a
neg a = Bad a -> a

extract : Bad Void -> Void
extract c@(CBad f) = f c

inconsistent : Void
inconsistent =
  let b = CBad extract
  in extract b

Expected Behavior

Main.inconsistent is not total

Observed Behavior

*bad> :m
No global holes to solve
*bad> :total inconsistent
Main.inconsistent is Total

Using idris version 1.3.1 from nixpkgs