A small correction: GHC uses plenty of type tagging information. In fact, its metadata overhead is relatively high.
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 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.