Non-covering case when pattern matching on dependent pair.

CantPatternMatchOnDPair.idr

module CantPatternMatchOnDPair

%default total

data Expr : Type -> Type where
  Lam : {a, b : Type} -> (a -> Expr b) -> Expr (a -> b)


-- this should be covering
f : (a : Type ** Expr a) -> (b : Type ** Expr b)
f (ty ** focus) = 
  case focus of
    (Lam f) => ?look_0