[kvb]

Not that it's a popular language, but a type-provider-like feature was recently added to the dependently-typed language Idris (see https://github.com/edwinb/Idris-dev/commit/46964d7d57c18826d...).