Pattern matching on types

typecase.idr

data Vect : Nat -> Type -> Type where
     Nil : Vect Z t
     (::) : a -> Vect k a -> Vect (S k) a

describe : Type -> String
describe Int = "Int"
describe (List t) = "List of " ++ describe t
describe (Vect n t) = "Vect of " ++ show n ++ " " ++ describe t
describe _ = "Something else"

{-
Main> describe Int
"Int"
Main> describe Nat
"Something else"
Main> describe (Vect 10 (List Int))
"Vect of 10 List of Int"
-}

-- Not allowed, because 'a' is a parameter
-- Just as well, because the type tells us this has to be the identity function
{-
failId : a -> a
failId {a = Nat} x = x + 1
failId x = x

"typecase.blod:12:1--13:1:Attempt to match on erased argument Nat"
-}

-- 'a' isn't a parameter here (having been explicitly bound) so we can
-- match on it...
-- So we know from the type that 'notId' might not be the identity function
notId : {a : Type} -> a -> a
notId {a = Nat} x = x + 1
notId x = x

{-
Main> notId (S (S Z))
S (S (S Z))
Main> notId 94
94
-}

Ah, nice, thanks!