is type checking in D undecidable?

[Ola Fosheim Grøstad]

On Thursday, 22 October 2020 at 18:24:47 UTC, Bruce Carneal wrote:
> Per the wiki on termination analysis some languages with 
> dependent types (Agda, Coq) have built-in termination checkers.
>  I assume that DMD employs something short of such a checker, 
> some combination of cycle detection backed up by resource 
> bounds?

"Decidable" is a term that means that there are some cases which 
cannot be decided even if you had near infinite computational 
resources at your disposal. So it is a very theoretical term, and 
not very practical. I don't know what kind of solvers those 
languages use, so I am not exactly sure what they mean by 
"termination checker". In general, it is hard to tell if a 
computation is long-running or unsolvable.