why Haskell doesn't have a type-level identity function

Main.agda

-- in reply to http://www.reddit.com/r/haskell/comments/26dshj/why_doesnt_haskell_allow_type_aliases_in_the/
module Main where

open import Data.Nat
open import Data.List renaming (monad to List-Monad)
open import Category.Monad
open import Relation.Binary.PropositionalEquality


-- Unlike Haskell, Agda supports arbitrary functions from type to type.
Id : Set → Set
Id a = a

-- And you can write monad instances for those functions.
Id-Monad : RawMonad Id
Id-Monad = record
  { return = \x → x
  ; _>>=_  = \x f → f x
  }

-- An Agda version of replicateM [1].
-- 
-- [1] http://hackage.haskell.org/package/base-4.7.0.0/docs/Control-Monad.html#v:replicateM
replicateM : {M : Set → Set} → {a : Set}
           → RawMonad M
           → ℕ → M a → M (List a)
replicateM {M} {a} M-Monad n mx = go n
  where
    open RawMonad M-Monad
    go : ℕ → M (List a)
    go zero    = return []
    go (suc n) = mx   >>= \x →
                 go n >>= \xs →
                 return (x ∷ xs)

-- `replicateM Id-Monad` is precisely `replicate` [2].
-- 
-- [2] http://hackage.haskell.org/package/base-4.7.0.0/docs/Prelude.html#v:replicate
square₁ : List (List ℕ)
square₁ = replicateM Id-Monad 3 (0 ∷ 1 ∷ [])

result₁ : square₁ ≡ ( (0 ∷ 1 ∷ [])
                    ∷ (0 ∷ 1 ∷ [])
                    ∷ (0 ∷ 1 ∷ [])
                    ∷ []
                    )
result₁ = refl

-- Using the list monad, the result is completely different.
square₂ : List (List ℕ)
square₂ = replicateM List-Monad 3 (0 ∷ 1 ∷ [])

result₂ : square₂ ≡ ( (0 ∷ 0 ∷ 0 ∷ [])
                    ∷ (0 ∷ 0 ∷ 1 ∷ [])
                    ∷ (0 ∷ 1 ∷ 0 ∷ [])
                    ∷ (0 ∷ 1 ∷ 1 ∷ [])
                    ∷ (1 ∷ 0 ∷ 0 ∷ [])
                    ∷ (1 ∷ 0 ∷ 1 ∷ [])
                    ∷ (1 ∷ 1 ∷ 0 ∷ [])
                    ∷ (1 ∷ 1 ∷ 1 ∷ [])
                    ∷ []
                    )
result₂ = refl

-- Note that we have to explicitly pass the monad instance to `replicateM`,
-- because the compiler cannot infer which of the two instances we want.

-- In Haskell, we can write `replicateM [0,1]` without specifying which monad
-- instance we want, because there is only one possibility: we must want the
-- list monad. We cannot want the identity monad, because there is no such
-- thing in Haskell.

-- Haskell has, however, something very close: the Identity monad,
-- with a capital 'I'.
record Identity (A : Set) : Set where
  field
    runIdentity : A
open Identity

mkIdentity : ∀ {A} → A → Identity A
mkIdentity x = record { runIdentity = x }

Identity-Monad : RawMonad Identity
Identity-Monad = record
  { return = mkIdentity
  ; _>>=_  = \ix f → f (runIdentity ix)
  }

-- This time, Haskell would have been able to infer that we meant to use the
-- Identity monad, because the type of the input is `Identity (List ℕ)`.
square₃ : Identity (List (List ℕ))
square₃ = replicateM Identity-Monad 3 (mkIdentity (0 ∷ 1 ∷ []))

result₃ : square₃ ≡ mkIdentity ( (0 ∷ 1 ∷ [])
                               ∷ (0 ∷ 1 ∷ [])
                               ∷ (0 ∷ 1 ∷ [])
                               ∷ []
                               )
result₃ = refl