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/Idr

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/46964d7d57c18826dec285dcfedfc4200f953fab https://github.com/edwinb/Idris-dev/commit/46964d7d57c18826d...).