Can not detect "impossibility" / How to build a contradiction

[canonic-epicure]

In my code I have a predicate like "QueryHasExactlyOneColumn" which is a wrapper around the ListHasExactlyOneElement

The proofs were pretty straightforward, and typechecker was extremely helpful.

Now I'm just copy-pasting the code, putting it in different namespace and just changing the record accessor from fieldsAcc to baseTableAcc.

I was expecting the code to type-check immediately, but instead I'm stuck with this hole. The context is:

*LanguageReduced> :t nocols
  ast : QueryAbstractSyntaxTree
  p : [] = baseTable ast
  prf : ListHasExactlyOneElement QuerySource (baseTable ast)
--------------------------------------
nocols : Void

In scope there are both proof that base tables equal to empty list: [] = baseTable ast and that the same list has exactly one element. This is obviously a contradiction and when case matching on any of the proofs using the interactive code assistant, the only case branch is marked as impossible:

        noColsProof1 : (p : [] = baseTableAcc ast) -> QueryHasExactlyOneBaseTable ast -> Void
        noColsProof1 p (Because {ast} {prf}) = case p of
            Refl impossible

But, after typecheck, I have a compiler error:

at line 140, character 13, file /home/nickolay/workspace/Idris/horn/src/LanguageReduced.idr
case block in noColsProof1 at /home/nickolay/workspace/Idris/horn/src/LanguageReduced.idr:139:53 _ Refl _ p is a valid case

Nearly exactly the same code compiles fine, just few lines above - how it can be? (it matches on the one el proof)

Is there any other way to express the whole? (using "absurd" function?)

[canonic-epicure]

To extend, if you make a valid branch for the Refl case above, like this:

        noColsProof1 : (p : [] = baseTableAcc ast) -> QueryHasExactlyOneBaseTable ast -> Void
        noColsProof1 p (Because {ast} {prf}) = case p of
            Refl => ?zxc

You get an error message like (note at line 0, no file):

at line 0, file (no file)
When checking left hand side of LanguageReduced.QueryHasExactlyOneBaseTable.case block in noColsProof1 at /home/nickolay/workspace/Idris/horn/src/LanguageReduced.idr:139:53:
Type mismatch between
        baseTable ast = baseTable ast (Type of Refl)
and
        [] = baseTableAcc ast (Expected type)

Specifically:
        Type mismatch between
                baseTable ast
        and
                []

In the same time in scope, there's a proof p : [] = baseTableAcc ast. This is something strange.