Functions with forward-declared data as an argument incorrectly accepted as covering

[dunhamsteve]

Coverage checking appears to be broken when a forward declared data type is involved.

Steps to Reproduce

data Three = A | B | C
data Bar : Type
data Foo : Type where
  MkFoo : Three -> Bar -> Foo

fun : Foo -> String
fun (MkFoo A y) = ""
fun (MkFoo B y) = ""

data Bar : Type where
  MkBar : Bar

Expected Behavior

I expect Idris to call out the missing case of C in fun or complain that Bar hasn't been defined yet when checking fun.

What would be the ideal behavior in this case? Ignore the y slot and call out the missing C or make it an error to have undefined types when building case trees?

Observed Behavior

The function fun is accepted as covering, despite missing the C case. I believe it's deciding that case is impossible because one of the pattern variables doesn't have a valid constructor. Failing to distinguish between empty and no constructors defined yet.