Changes between Initial Version and Version 5 of Ticket #5441


Ignore:
Timestamp:
Sep 9, 2011 9:20:43 AM (3 years ago)
Author:
simonpj
Comment:

Ulf, thank you for identifying a nice small test case. Very helpful. Agda stresses unsafeCoerce like nothing else.

Try now.

Simon

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #5441

    • Property Status changed from new to closed
    • Property Test Case changed from to simplCore/should_run/T5441
    • Property Type of failure changed from None/Unknown to Runtime crash
    • Property Owner set to simonmar
    • Property Resolution changed from to fixed
  • Ticket #5441 – Description

    initial v5  
    11The following module is the smallest one I've been able to find exhibiting the bug. Any simplification (that I've tried) results in the problem going away. 
    2  
     2{{{ 
    33module Any where 
    44 
     
    4040showNat :: Nat -> String 
    4141showNat = coe2 (showInBase Z) 
    42  
     42}}} 
    4343Now given this main module (it needs to be a different module) 
    44  
     44{{{ 
    4545import Any 
    4646main = putStrLn (showNat Z) 
    47  
     47}}} 
    4848Compiling with optimisations: 
    49  
     49{{{ 
    5050$ ghc -O --make Main.hs 
    5151... 
    5252$ ./Main 
    5353Bus error: 10 
    54  
     54}}} 
    5555Without optimizations it prints 0 as expected. 
    5656