Nuts to this sanity check

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,15 @@
 ;;; 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-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)))
 
@@ -595,6 +612,33 @@
   (check-true (v? (term (refl Nat))))
   (check-true (v? (term ((refl Nat) z)))))
 
+(define-metafunction tt-redL
+  elim-Θv-really : Σ Θv -> #t or #f
+  [(elim-Θv-really Σ hole) #t]
+  [(elim-Θv-really Σ (Θv (in-hole Θv_1 (elim x_D U))))
+   ,(and
+      (not (equal? (term (Θ-length Θv_1))
+                   (term (Σ-elim-arity Σ x_D))))
+      (term (elim-Θv-really Σ Θv_1))
+      (term (elim-Θv-really Σ Θv)))]
+  [(elim-Θv-really Σ (Θv v))
+   (elim-Θv-really Σ Θv)])
+
+(module+ test
+  (check-true
+    (term (elim-Θv-really ,Σ (hole (elim nat Type)))))
+  (check-true
+    (term (elim-Θv-really ,Σ (hole ((elim nat Type) (λ (x : nat) nat))))))
+  (check-true
+    (term (elim-Θv-really ,Σ (hole (((elim nat Type) (λ (x : nat) nat)) zero)))))
+  (check-true
+    (term (elim-Θv-really ,Σ (hole ((((elim nat Type) (λ (x : nat) nat)) zero)
+                                              (λ (x : nat) (λ (ih : nat) zero)))))))
+  (check-false
+    (term (elim-Θv-really ,Σ (hole (((((elim nat Type) (λ (x : nat) nat)) zero)
+                                               (λ (x : nat) (λ (ih : nat) zero)))
+                                                                  zero))))))
+
 (define tt-->
   (reduction-relation tt-redL
     (--> (Σ (in-hole E ((any (x : t_0) t_1) t_2)))
@@ -617,8 +661,10 @@
           | Unfortunately, Θ contexts turn all this inside out:
           | TODO: Write better abstractions for this notation
           |#
-          ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
-          ;; the discriminant: the constructor x_ci applied to its argument Θv_i
+         ;; Check that Θv only contains partially applied elims.
+         (side-condition (term (elim-Θv-really Σ Θv)))
+         ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
+         ;; the discriminant: the constructor x_ci applied to its argument Θv_i
          (where (in-hole (Θv_p (in-hole Θv_i x_ci)) Θv_m) Θv)
          ;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other
          ;; arguments.
@@ -648,8 +694,8 @@
    (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))
+        #;(unless (null? (cdr r))
+          (error "Church-Rosser broken" r (term e)))
         (car r)))])
 
 ;; TODO: Move equivalence up here, and use in these tests.

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,25 @@
   (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 '~a' does not have expected type; expected '~a' but inferred '~a'"
+                        (cur->datum #'e2)
+                        (cur->datum #'t1)
+                        (cur->datum (type-infer/syn #'e2)))
+                (quasisyntax/loc syn (e1 e2))))
+            #'(real-app e1 e2))]
+         [_ (raise-syntax-error
+              '#%app
+              (format "Operator '~a' does not have function type; inferred type was: '~a'"
+                      (cur->datum #'e1)
+                      (cur->datum f-type))
+              (quasisyntax/loc syn (e1 e2)))]))]
     [(_ e1 e2 e3 ...)
      #'(#%app (#%app e1 e2) e3 ...)]))