Impossible pattern in Idris

RegExp.idr

module RegExp

%default total

data RegExp : Type where
  Zero : RegExp
  Eps  : RegExp  
  Chr  : Char -> RegExp
  Cat  : RegExp -> RegExp -> RegExp
  Alt  : RegExp -> RegExp -> RegExp
  Star : RegExp -> RegExp

data hasEmpty : RegExp -> Type where
  hasEps  : hasEmpty Eps
  hasAltL : {l : RegExp} -> 
            (r : RegExp) -> 
            hasEmpty l   -> 
            hasEmpty (Alt l r)
  hasAltR : (l : RegExp) -> 
            {r : RegExp} -> 
            hasEmpty r   -> 
            hasEmpty (Alt l r)
  hasCat : {l : RegExp} ->
           {r : RegExp} ->
           hasEmpty l   ->
           hasEmpty r   ->
           hasEmpty (Cat l r)
  hasStar : (e : RegExp) ->
            hasEmpty (Star e)                    

hasEmptyZero : hasEmpty l -> Void
hasEmptyZero prf impossible  -- also tried this, with no success: hasEmptyZero impossible 

hasEmptyChr : {c : Char} -> hasEmpty (Chr c) -> Void
hasEmptyChr prf impossible

hasEmptyCatInv : {l : RegExp} ->
                 {r : RegExp} ->
                 hasEmpty (Cat l r) -> 
                 (hasEmpty l, hasEmpty r)
hasEmptyCatInv (hasCat l r) = (l , r)                
                                  
hasEmptyAltInv : {l : RegExp} ->
                 {r : RegExp} -> 
                 hasEmpty (Alt l r) -> 
                 Either (hasEmpty l) (hasEmpty r)
hasEmptyAltInv (hasAltL r pl) = Left pl
hasEmptyAltInv (hasAltR l pr) = Right pr               
                                    
hasEmptyDec : (e : RegExp) -> Dec (hasEmpty e)
hasEmptyDec Zero = No hasEmptyZero
hasEmptyDec Eps = Yes hasEps
hasEmptyDec (Chr c) = No hasEmptyChr
hasEmptyDec (Alt l r) with (hasEmptyDec l)
 | Yes prf = Yes (hasAltL r prf)
 | No nprf with (hasEmptyDec r)
      | Yes prf' = Yes (hasAltR l prf')
      | No nprf' = No (either nprf nprf' . hasEmptyAltInv)
hasEmptyDec (Cat l r) with (hasEmptyDec l)
                      | Yes prf with (hasEmptyDec r)
                                     | Yes prf' = Yes (hasCat prf prf')
                                     | No nprf' = No (nprf' . snd . hasEmptyCatInv)
                      | No nprf = No (nprf . fst . hasEmptyCatInv)               
hasEmptyDec (Star e) = Yes (hasStar e)