"Tried to evaluate non-dimension term ... as dimension"

[jonsterling]

I am getting this error when I try to eliminate out of the torus into a certain extension type. Sounds like a bug in the eliminators...

[jonsterling]

If you write:

let t2c2t (t : torus) : [i] torus [i=0 ⇒ c2t (t2c t) | i=1 ⇒ t] = ?

you can see that the resulting goal is incorrect:

  ?Hole:
   t : torus
  ⊢ (# <i>
        torus
        [i=0
         ((s1.elim
           [c] (→ [_ : s1] torus)
           (car
            (torus.elim
             [t] (× [_ : s1] s1)
             t
             (pt (pair base base))
             (p/one (pair (loop i) base))
             (p/two (pair base (loop i)))
             (square (pair (loop i) (loop {1})))))
           (base (λ [_] (s1.elim [c'] torus _ (base pt) (loop (p/two _)))))
           (loop
            (λ [_]
             (s1.elim [c'] torus _ (base (p/one i)) (loop (square _ {2}))))))
          (cdr
           (torus.elim
            [t] (× [_ : s1] s1)
            t
            (pt (pair base base))
            (p/one (pair (loop i) base))
            (p/two (pair base (loop i)))
            (square (pair (loop i) (loop {1}))))))]
        [i=1 t])

In particular, look for that {2} part; this is the way that a variable prints out when its index is actually out of range / not in scope. It means that binding of the eliminator is somehow getting fucked up. I think that {2} should be i. The same thing happens in the second torus.elim under cdr.