Found issues with elim reduction

Trying to write macros that provide better error messages, I found
issues with eliminator reduction. Can't define when a partially applied
eliminator is a value via grammar alone, but need to in order to give
deterministic reduction relation...

curnel/redex-core.rkt

@@ -500,6 +500,18 @@
     (term (Σ-methods-telescope ,sigma false (λ (y : false) (Π (x : Type) x))))
     (term hole)))
 
+;; Returns the number of arguments expected by the eliminator for type
+;; x_D, counting the motive, the methods, the parameters, and the discriminant
+(define-metafunction tt-ctxtL
+  Σ-elim-arity : Σ x_D -> natural
+  [(Σ-elim-arity Σ x_D)
+   ,(let ([cs (term (Σ-ref-constructors Σ x_D))])
+      (unless cs
+        (error 'Σ-elim-arity "~a is not defined in ~a" (term x_D) (term Σ)))
+      (+ 1 (length cs)
+       (term (Ξ-length (Σ-ref-parameter-Ξ Σ x_D)))
+       1))])
+
 ;; Computes the type of the eliminator for the inductively defined type x_D with a motive whose result
 ;; is in universe U.
 ;;
@@ -539,6 +551,7 @@
    ;; The types of the methods for this inductive.
    (where Ξ_m (Σ-methods-telescope Σ x_D x_P))])
 
+
 ;; TODO: This might belong in the next section, since it's related to evaluation
 ;; Generate recursive applications of the eliminator for each inductive argument of type x_D.
 ;; In more detaill, given motive t_P, parameters Θ_p, methods Θ_m, and arguments Θ_i to constructor
@@ -578,11 +591,19 @@
 ;;; The majority of this section is dedicated to evaluation of (elim x U), the eliminator for the
 ;;; inductively defined type x with a motive whose result is in universe U
 
+;; Necessary to get the side-condition patterns to work.
+(define current-Σ (make-parameter (term ∅)))
+(define (elim-arity x)
+  (term (Σ-elim-arity ,(current-Σ) ,x)))
+
 (define-extended-language tt-redL tt-ctxtL
-  ;; NB: (in-hole Θv (elim x U)) is only a value when it's a partially applied elim. However,
-  ;; determining whether or not it is partially applied cannot be done with the grammar alone.
-  (v   ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U)))
   (Θv  ::= hole (Θv v))
+  (v   ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x)
+           ;; NB: (in-hole Θv (elim x U)) is only a value when it's a partially applied elim.
+           (in-hole Θv (elim x U))
+           #;(side-condition
+             (not (equal? (term (Θ-length Θv_0))
+                          (elim-arity (term x_0))))))
   ;; call-by-value, plus reduce under Π (helps with typing checking)
   (E   ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) e)))
 
@@ -639,18 +660,19 @@
   step : Σ e -> e
   [(step Σ e)
    e_r
-   (where (_ e_r) ,(car (apply-reduction-relation tt--> (term (Σ e)))))])
+   (where (_ e_r) ,(parameterize ([current-Σ (term Σ)]) (car (apply-reduction-relation tt--> (term (Σ e))))))])
 
 (define-metafunction tt-redL
   reduce : Σ e -> e
   [(reduce Σ e)
    e_r
    (where (_ e_r)
-     ,(let ([r (apply-reduction-relation* tt--> (term (Σ e)) #:cache-all? #t)])
-        ;; Efficient check for (= (length r) 1)
-        (unless (null? (cdr r))
-          (error "Church-Rosser broken" r))
-        (car r)))])
+     ,(parameterize ([current-Σ (term Σ)])
+        (let ([r (apply-reduction-relation* tt--> (term (Σ e)) #:cache-all? #t)])
+         ;; Efficient check for (= (length r) 1)
+         (unless (null? (cdr r))
+           (error "Church-Rosser broken" r (term e)))
+         (car r))))])
 
 ;; TODO: Move equivalence up here, and use in these tests.
 (module+ test

stdlib/sugar.rkt

@@ -48,7 +48,7 @@
   (syntax-rules (:)
     [(_ (a : t) (ar : tr) ... b)
      (forall (a : t)
-        (forall* (ar : tr) ... b))]
+       (forall* (ar : tr) ... b))]
     [(_ b) b]))
 
 (define-syntax lambda*
@@ -62,7 +62,22 @@
   (syntax-case syn ()
     [(_ e) #'e]
     [(_ e1 e2)
-     #'(real-app e1 e2)]
+     (let  ([f-type (type-infer/syn #'e1)])
+       (syntax-case f-type ()
+         [(Π (x : t1) t2)
+          (begin
+            (unless (type-check/syn? #'e2 #'t1)
+              (raise-syntax-error
+                '#%app
+                (format "Operand does not have expected type; expected ~a but inferred ~a"
+                        (cur->datum #'t1)
+                        (cur->datum (type-infer/syn #'e2)))
+                f-type (quasisyntax/loc syn (e1 e2))))
+            #'(real-app e1 e2))]
+         [_ (raise-syntax-error
+              '#%app
+              (format "Operator does not have function type; inferred type was: ~a" (cur->datum f-type))
+              f-type (quasisyntax/loc syn (e1 e2)))]))]
     [(_ e1 e2 e3 ...)
      #'(#%app (#%app e1 e2) e3 ...)]))