Idris accepts code that matches on erased value

[dunhamsteve]

Idris appears to be accepting a program that matches on an erased value.

Steps to Reproduce

Type check this code:

data Foo : Type where
    NoFoo : Foo
    MkFoo : (0 _ : Maybe String) -> Foo

data Bar : Foo -> Type where
    Baz : Bar (MkFoo v)

foo : Bar f -> Bool
foo {f = MkFoo (Just _)} Baz = True
foo {f = MkFoo Nothing} Baz = False

Expected Behavior

Error: While processing left hand side of foo. Can't match on Just ?_ (Erased argument).

Observed Behavior

The program is accepted.

Idris will reject the program if the NoFoo constructor is commented out. I think both the specific MkFoo v in the type of Baz and having more than one constructor on Foo are necessary to trigger this issue.

I found this while looking into mattpolzin/ncurses-idris#34

[dunhamsteve]

Interestingly, if we use a Bool instead of Maybe String:

data Foo : Type where
    NoFoo : Foo
    MkFoo : (0 _ : Bool) -> Foo

data Bar : Foo -> Type where
    Baz : Bar (MkFoo v)

foo : Bar f -> Bool
foo {f = MkFoo True} Baz = True
foo {f = MkFoo False} Baz = False

Slightly older versions of Idris incorrectly accept it, but current "main" branch reports that the second clause (the False one) is unreachable.