The dependent types example seems underwhelming; rejecting arrays of unlike length at compile time is something I'd expect from a Pascal compiler from 1975.

How about C90: pointer to array of 10 is not compatible with a pointer to array 20:

  int process_array(int (*pa)[20]);

  int main(void)
  {
    int array[10];
    process_array(&array);
    return 0;
  }

GCC:

  array.c: In function ‘main’:
  array.c:6:17: warning: passing argument 1 of ‘process_array’ from incompatible pointer type [-Wincompatible-pointer-types]
    process_array(&array);
                 ^
  array.c:1:5: note: expected ‘int (*)[20]’ but argument is of type ‘int (*)[10]’
   int process_array(int (*pa)[20]);
       ^~~~~~~~~~~~~