[Agda] Agda performance improvements

[Nils Anders Danielsson]

On 2011-08-25 15:56, Martin Escardo wrote:
> I see that the example I reported a while ago producing a heap
> exhaustion now type-checks, as tested by you, and fast.

This seems to be due to a different optimisation: the unifier is now
less keen to unfold things. This has the undesirable consequence that
some programs that were previously accepted are now rejected by the
termination checker. Ulf provided the following example:

   data Nat : Set where
     zero : Nat
     suc  : Nat → Nat

   id : {A : Set} → A → A
   id x = x

   data T : Nat → Set where
     c : ∀ n → T (id n)

   foo : ∀ n → T n → Nat
   foo zero    _ = zero
   foo (suc n) t = foo _ (c n)

The underscore is now instantiated with id n, which is not seen to be
structurally smaller than suc n.

-- 
/NAD