I've been wishing this from the time I ran into "errors" involving numpy broadcasting along incorrect dimensions. Errors of the kind: you wanted to add a 10-length vector to a (10,10)-matrix by treating the vector as a (10,1) matrix. But instead, no one told you about such errors and you spent hours debugging only to learn that a 10-length vector is treated as a (1,10)-matrix in this particular case.

But yup, computing on dimension information to provide static autocompletion as well as dimension checks themselves seems like a huge plus.

Besides compile time checks, another feature I have wished for is to index the array dimensions by the name of the dimension rather than its axis-number.

For me, Common Lisp coupled with CLTL2 and defacto-libraries is the closest language that comes to make this a possibility. The built-in Common Lisp array types are already fairly extensive in that they actually allow specifying the per-axis dimensions, which the compiler can then use to type check. Common Lisp's SBCL compiler does this in a fair number of cases. For example -

(declaim (inline add-vectors))
(defun add-vectors (a b out)
  (declare (type (simple-array single-float (10)) a b out))
  (loop for i below 10
        do (setf (aref out i)
                 (+ (aref a i)
                    (aref b i))))
  out)

Consider the add-vectors function defined above that takes three arrays each with element type single float and a single axis of length 10, adds the first two arguments x and y element-wise and stores the result into out.

Then, if you try to compile the following function:

(defun add-to-first (x y)
  (declare (type (simple-array single-float (10)) x)
           (type (simple-array single-float (05)) y))
  (add-vectors x y x))

The compiler SBCL actually signals an error during compilation itself:

; processing (DEFUN ADD-TO-FIRST ...)

; file: /tmp/slimeBh9nFb
; in: DEFUN ADD-TO-FIRST
;     (ADD-VECTORS X Y X)
;
; note: deleting unreachable code
;
; caught WARNING:
;   Derived type of COMMON-LISP-USER::Y is
;     (VALUES (SIMPLE-ARRAY SINGLE-FLOAT (5)) &OPTIONAL),
;   conflicting with its asserted type
;     (SIMPLE-ARRAY SINGLE-FLOAT (10)).
;   See also:
;     The SBCL Manual, Node "Handling of Types"
;
; compilation unit finished
;   caught 1 WARNING condition
;   printed 1 note

But that said, Common Lisp leaves a lot many things wanting. Not only are there no parametric types, its type system also has no formal structure like the Hindley-Milner type system. There's an attempt at Coalton to bridge this and bring HM-based type checking to Common Lisp.

However, even with HM, the notion of per-axis dimensions is hard, although doable. With a fair bit of macrology over the past two years, some of us* have been able to come up with something that allows for the following:

(in-package :polymorphic-functions)

(push (lambda (x)
        (member x '(<m> <len> <type>)))
      *parametric-type-symbol-predicates*)

(defpolymorph pf-add-vectors ((a   (simple-array <type> (<len>)))
                              (b   (simple-array <type> (<len>)))
                              (out (simple-array <type> (<len>))))
    (simple-array <type> (<len>))
  (loop :for i :below <len>
        :do (setf (aref out i)
                  (+ (aref a i)
                     (aref b i))))
  out)

And then if one tries to compile the add-to-first defined above:

(defun add-to-first (x y)
  (declare (type (simple-array single-float (10)) x)
           (type (simple-array single-float (05)) y)
           (optimize safety))
  (pf-add-vectors x y x))

One gets the following compiler note:

; processing (DEFUN ADD-TO-FIRST ...)
; While compiling
;     (PF-ADD-VECTORS X Y X)
;   Following notes were encountered:
;
;     No applicable POLYMORPH discovered for polymorphic-function
;       PF-ADD-VECTORS
;     and ARGS:
;
;       (X Y X)
;
;     derived to be of TYPES:
;
;       ((SIMPLE-ARRAY SINGLE-FLOAT (10)) (SIMPLE-ARRAY SINGLE-FLOAT (5))
;        (SIMPLE-ARRAY SINGLE-FLOAT (10)))
;
;     Available Effective-Type-Lists include:
;
;       ((SIMPLE-ARRAY <TYPE> (<LEN>)) (SIMPLE-ARRAY <TYPE> (<LEN>))
;        (SIMPLE-ARRAY <TYPE> (<LEN>)))

And the following compiles successfully:

(defun add-to-first (x y)
  (declare (type (simple-array single-float (10)) x)
           (type (simple-array single-float (10)) y)
           (optimize speed))
  (pf-add-vectors x y x))

And a fair bit optimally when declared so.:

; disassembly for ADD-TO-FIRST
; Size: 149 bytes. Origin: #x53BD456C                         ; ADD-TO-FIRST
.
.
.
; 5D0: L0:   F30F104C4E01     MOVSS XMM1, [RSI+RCX*2+1]
; 5D6:       F30F10544F01     MOVSS XMM2, [RDI+RCX*2+1]
; 5DC:       F30F58D1         ADDSS XMM2, XMM1
; 5E0:       F30F11544E01     MOVSS [RSI+RCX*2+1], XMM2
.
.
.

Note that there are no parametric types in the sense of HM types. This is rather a symbol substitution and declaration-propagation strategy that is being employed here. Regardless, this is very much rudimentary, has no formal semantics, and at the current rate, I will expect it to take several years for reaching maturity. But yeah, someone with the background in (dependent) type theory and the time to implement and debug it is certainly welcome to experiment with Common Lisp and SBCL to see what might be possible :D.