module Ids where

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

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

-- The example above is based on one in "Implementing Typed
-- Intermediate Languages" by Shao, League and Monnier.