How can I implement a typeOf function?

Question

Since types are first-class in Idris, it seems like I should be able to write a typeOf function that returns the type of its argument:

typeOf : a => a -> Type
typeOf x = a

However, when I attempt to call this function, I get what looks like an error:

*example> typeOf 42
Can't find implementation for Integer

How can I properly implement this typeOf function? Or is there something more subtle about the idea of "getting the type of a value" that I'm missing, which would prevent the existence of such a function?

Answer 1

Write it this way:

typeOf : {a : Type} -> a -> Type
typeOf {a} _ = a

a => b is a function which has an implicit argument filled in by interface resolution. {a : b} -> c is a function with an implicit argument filled in by unification.

There is no need to refer to interfaces here. Every term has a single type. If you write typeOf 42, the implicit a is inferred to Integer by unification.