Why is this there? Is it to facilitate things like Typeable? I believe that there's no language-level way to do things like runtime type reflection. And even if there were, how would one express a complex type like (Vector (forall a. MyTypeClass a => a -> Int, String))?
I'm also curious if dependently typed languages like Idris, which presumably must be able to have runtime access to type information, handle this stuff.
For values, laziness means there is a tag bit for whether a value is a thunk or evaluated. Sum types use tags to determine which variant is active.
For functions, because a function that takes two arguments and returns a value (a -> a -> a) has the same type as a function that takes one argument and returns a function that takes another argument that returns a value (a -> a -> a), the arity of functions is stored in the tag.
Some of these tags are eliminated by inlining but if you sit down and read some typical Haskell output you'll see a _whole lot_ of tag checks.
Source: spent a lot of time reading GHC output and writing high-performance Haskell code.
I'm also curious if dependently typed languages like Idris, which presumably must be able to have runtime access to type information, handle this stuff.