For systems without dependent types, like Hindley-Milner type system, the types correspond to formulas of intuitionistic logic. There we know that its models are Heyting algebras, and in particular, to disprove a formula, we can restrict to one Heyting algebra where each formula is represented by an open subset of $\mathbb{R}$.
For example, if we want to show that $\forall\alpha.\alpha\lor(\alpha\rightarrow\bot)$ is not inhabited, we construct a mapping $\phi$ from formulas to open subsets of $\mathbb{R}$ by defining: \begin{align} \phi(\alpha) &= (-\infty, 0) \end{align} Then \begin{align} \phi(\alpha\rightarrow\bot) &= \mbox{int}( [0, \infty) ) \\ & = (0,\infty) \\ \phi(\alpha\lor(\alpha\rightarrow\bot)) &= (-\infty, 0) \cup (0,\infty) \\ &= \mathbb{R} \setminus {0}. \end{align} This shows that the original formula cannot be provable, since we have a model where it's not true, or equivalently (by Curry-Howard isomorphism) the type cannot be inhabited.
Another possibility would be to use Kriepke frames.
Are there any similar methods for systems with dependent types? Like some generalization of Heyting algebras or Kripke frames?
Note: I'm not asking for a decision procedure, I know there cannot be any. I'm asking just for a mechanism that allows to witness unprovability of a formula - to convince someone that it's unprovable.