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
-}

In the current world, by parametricity I know the second argument here:

foo : a -> ({x : Type} -> x -> b) -> b
foo x f = f x

is const b for some b. Does that go away with this feature? (not sure whether that's a problem or not)

The type there says that x is available at run time. However, in the new world, you can write it as follows:

foo : a -> ({0 x : Type} -> x -> b) -> b
foo x f = f x

Or even as:

foo : a -> (forall x . x -> b) -> b
foo x f = f x

Then you'll get the same guarantees as before.

Ah, nice, thanks!