[Agda] Strange normalization

[Sam Staton]

Hello.

Agda seems to normalize parameters to data types, to an excessive  
degree. See, for instance, the code below. I didn't expect this code  
to loop off forever, but it does.

Is this a feature? I have found it annoying. (I'm just getting the  
hang of Agda, and I'm not a Haskell expert, so I apologize if the  
question is naive.) Best regards, Sam

--

module strange where

   data Unit : Set where
     unit : Unit

   data Nat : Set where
     zero : Nat
     succ : Nat -> Nat

   ack : Nat -> Nat -> Nat
   ack zero n = succ n
   ack (succ m) zero = ack m (succ zero)
   ack (succ m) (succ n) = ack m (ack (succ m) n)

   bomb : Nat
   bomb = ack (succ (succ (succ (succ zero)))) (succ (succ zero))

   data D (f : Unit -> Nat) : Set where
     d : D f

   f : Unit -> Nat
   f r = bomb
--  f r = zero

   T : Set
   T = D f

-- everything is fine if you comment out the following lines.
   explode : T
   explode = d