Minimal Example of odd not covering error from matching on Sigma types.

CantMatchOnSigmaFunc.idr

module CantMatchOnSigmaFunc

%default total      
      
data Expr : Type -> Type where      
  Lam : {a, b : Type} -> (a -> Expr b) -> Expr (a -> b)         
                                                                
{-
f : (a : Type ** Expr a) -> (b : Type ** Expr b)  
f (ty ** focus) =       
  case focus of         
    (Lam f) => ?stuck    
-}