is type checking in D undecidable?

[Bruce Carneal]

On Thursday, 22 October 2020 at 18:04:32 UTC, Ola Fosheim Grøstad 
wrote:
> On Thursday, 22 October 2020 at 17:25:44 UTC, Bruce Carneal 
> wrote:
>> Is type checking in D undecidable?  Per the wiki on dependent 
>> types it sure looks like it is.
>
> Even if it is, you can still write something that is decidable 
> in D, but impractical in terms of compile time.

Yep.  Within some non-exponential CTFE speed factor that's 
equivalent to saying your program might run too long.

>
> You probably mean more advanced type systems where these things 
> are expressed more implicitly. Basically type systems where you 
> can express and resolve properties related to infinite sizes. D 
> does not have such capabilities, so you have to go out of your 
> way to end up in that territory in D.

Where "out of your way" means what?  Use of templates with 
potentially unbounded recursive expression?  Other?

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?