agda/notes/papers/implicit/examples/Crash.epi

------------------------------------------------------------------------------
                                          (   n : Nat   !
data (---------!  where (------------! ;  !-------------!
     ! Nat : * )        ! zero : Nat )    ! suc n : Nat )
------------------------------------------------------------------------------
data (----------!  where (--------------! ;  (-------------!
     ! Bool : * )        ! false : Bool )    ! true : Bool )
------------------------------------------------------------------------------
     ( b : Bool !    
let  !----------!    
     ! F b : *  )    
                     
     F b <= case b   
     { F false => Nat
       F true => Bool
     }               
------------------------------------------------------------------------------
     (   b : Bool   !   
let  !--------------!   
     ! not b : Bool )   
                        
     not b <= case b    
     { not false => true
       not true => false
     }                  
------------------------------------------------------------------------------
     ( (    x : F ?    !                   !    
     ! !---------------! ;  h : F (g zero) !    
     ! ! g : F (not x) )                   !    
let  !-------------------------------------! ;  
     !             j g h : Nat             )    
------------------------------------------------------------------------------
[There is some magic going on here which prevents the type of!
![g zero] i.e. [F (not zero)] from being evaluated.          ]
------------------------------------------------------------------------------
     ( g : all x : F ? => F (not x) !    
let  !------------------------------! ;  
     !          h g : Nat           )    
------------------------------------------------------------------------------
[We are not allowed to give a definition to h, since the type isn't!
!guaranteed to be correct.                                         ]
------------------------------------------------------------------------------