Idris convinced that all cases are impossible, but also admits there are possible cases

[Kazark]

Steps to Reproduce

Using Idris 1.3.1, I am able to compile

module Again

%default total
%access public export

||| A "full" or non-empty list
FList : Type -> Type
FList a = (xs : List a ** NonEmpty xs)

infixr 5 :::

(:::) : a -> List a -> FList a
(:::) x xs = ((x :: xs) ** IsNonEmpty)

||| Proof that the first list is an improper prefix of the second list, with the
||| third list as the remainder.
data IsPrefixOf : FList a -> FList a -> List a -> Type where
  SingletonPrefix : IsPrefixOf (x ::: []) (x ::: rem) rem
  SuccPrefix : IsPrefixOf (xs ** _) (ys ** _) rem
            -> IsPrefixOf (x ::: xs) (x ::: ys) rem


prefixAntisym : (xs : FList a) -> (ys : FList a) -> (zs : List a)
              -> IsPrefixOf xs ys zs -> IsPrefixOf ys xs zs
              -> (xs = ys, zs = [])
prefixAntisym (xs ** xpf) (ys ** ypf) [] SingletonPrefix _ impossible
prefixAntisym (xs ** xpf) (ys ** ypf) [] (SuccPrefix _) _ impossible
prefixAntisym (xs ** xpf) (ys ** ypf) (_ :: _) SingletonPrefix _ impossible
prefixAntisym (xs ** xpf) (ys ** ypf) (_ :: _) (SuccPrefix _) _ impossible

I got these impossible cases by using case splitting. However, convinced that there are possible cases, I then began to write this definition out more by hand, without so much reliance on Idris' auto-editing capabilities:

prefixAntisym' : (xs : FList a) -> (ys : FList a) -> (zs : List a)
              -> IsPrefixOf xs ys zs -> IsPrefixOf ys xs zs
              -> (xs = ys, zs = [])
prefixAntisym' ((x :: []) ** IsNonEmpty) ((x :: []) ** IsNonEmpty) [] SingletonPrefix SingletonPrefix = (Refl, Refl)
prefixAntisym' ((x :: []) ** IsNonEmpty) ((y :: (y' :: ys)) ** IsNonEmpty) [] ipo1 ipo2 = ?prefixAntisym'_rhs_5
prefixAntisym' ((x :: (x' :: xs)) ** IsNonEmpty) ((y :: []) ** IsNonEmpty) [] ipo1 ipo2 = ?prefixAntisym'_rhs_1
prefixAntisym' ((x :: (x' :: xs)) ** IsNonEmpty) ((y :: (y' :: ys)) ** IsNonEmpty) [] ipo1 ipo2 = ?prefixAntisym'_rhs_6
prefixAntisym' ((x :: xs) ** IsNonEmpty) ((y :: ys) ** IsNonEmpty) (z :: zs) ipo1 ipo2 = ?prefixAntisym'_rhs_3

which though it is incomplete, type checks, thus demonstrating that Idris disagrees with itself about the impossibility of the first several cases. I wonder if this is a duplicate of #4582 , but being that I experienced it in a different way, I thought I might open a separate issue. I am at least hoping that this is not a separate root problem though!

Expected Behavior

1. On case splitting: that Idris would give me case splits which still contained equations with holes.
2. On type checking: that Idris would not type-check the proof that falsely claims all cases are impossible. I have seen before where it goofed up on the auto-editing but caught the problem it had introduced on a subsequent type check.

Observed Behavior

1. On case splitting: Idris falsely jumps to the conclusion that all cases are impossible.
2. On type checking: Idris doesn't catch the bug it introduced during case splitting.