Case split

Test.idr

module Test                                                                                                                                                                                                         
                                                                                                                                                                                                                    
record Ann where                                                                                                                                                                                                    
  constructor MkAnn                                                                                                                                                                                                 
  ann1 : Type                                                                                                                                                                                                       
                                                                                                                                                                                                                    
data Test : Type where                                                                                                                                                                                              
  MkTest : Test                                                                                                                                                                                                     
                                                                                                                                                                                                                    
AnnTest : Ann -> Type                                                                                                                                                                                               
AnnTest a = (Test , ann1 a)                                                                                                                                                                                         
                                                                                                                                                                                                                    
TAnn : Ann                                                                                                                                                                                                          
TAnn = MkAnn ()                                                                                                                                                                                                     
             
-- this doesn't case split more

test : AnnTest TAnn -> ()                                                                                                                                                                                           
test (a, b) = ?test_rhs_1