diff --git a/cur-lib/cur/curnel/redex-lang.rkt b/cur-lib/cur/curnel/redex-lang.rkt
index 12825ab..ce7147f 100644
--- a/cur-lib/cur/curnel/redex-lang.rkt
+++ b/cur-lib/cur/curnel/redex-lang.rkt
@@ -58,13 +58,41 @@
    (all-from-out syntax/parse)
    (all-from-out racket)
    (all-from-out racket/syntax)
-    cur->datum
-    cur-expand
-    type-infer/syn
-    type-check/syn?
-    normalize/syn
-    step/syn
-    cur-equal?))
+   raise-curnel-type-error
+   raise-curnel-syntax-error
+   cur->datum
+   cur-expand
+   type-infer/syn
+   type-check/syn?
+   normalize/syn
+   step/syn
+   cur-equal?))
+
+;; Exceptions
+(begin-for-syntax
+  (provide
+   (struct-out exn:cur)
+   (struct-out exn:cur:curnel)
+   (struct-out exn:cur:curnel:type)
+   (struct-out exn:cur:curnel:syntax))
+  (define-struct (exn:cur exn) () #:transparent)
+  (define-struct (exn:cur:curnel exn:cur) () #:transparent)
+  (define-struct (exn:cur:curnel:type exn:cur) () #:transparent)
+  (define-struct (exn:cur:curnel:syntax exn:cur) () #:transparent)
+
+  (define (raise-curnel-type-error name v . other)
+    (raise
+     (make-exn:cur:curnel:type
+      (for/fold ([msg (format "~a: Cur type error;~n  Typing judgment did not hold in Curnel~n    term: ~a" name v)])
+                ([t other])
+        (format "~a~n   additional context: ~a" msg t))
+      (current-continuation-marks))))
+
+  (define (raise-curnel-syntax-error name v [more ""])
+    (raise
+     (make-exn:cur:curnel:syntax
+      (format "~a: Cur syntax error;~n  Term is invalid Curnel syntax;~a~n    term: ~a" name more v)
+      (current-continuation-marks)))))
 
 (begin-for-syntax
   ;; TODO: Gamma and Delta seem to get reset inside a module+
@@ -73,7 +101,7 @@
       (term ∅)
       (lambda (x)
         (unless (Γ? x)
-          (error 'core-error "We built a bad term environment ~s" x))
+          (raise-curnel-syntax-error 'term-environment "term is not a well-formed Γ"))
         x)))
 
   (define delta
@@ -81,7 +109,7 @@
       (term ∅)
       (lambda (x)
         (unless (Δ? x)
-          (error 'core-error "We built a bad inductive declaration ~s" x))
+          (raise-curnel-syntax-error 'inductive-delcaration x "term is not a well-formed Δ"))
         x)))
 
   ;; These should be provided by core, so details of envs can be hidden.
@@ -118,7 +146,7 @@
      (list null null)
      (lambda (x)
        (unless (subst? x)
-           (error 'core-error "We build a bad subst ~s" x))
+         (raise-curnel-syntax-error 'top-level-bindings x))
        x)))
 
   (define (add-binding/term! x t)
@@ -156,8 +184,6 @@
   (define (cur->datum syn)
     ;; Main loop; avoid type
     (define reified-term
-      ;; TODO: This results in less good error messages. Add an
-      ;; algorithm to find the smallest ill-typed term.
       (parameterize ([inner-expand? #t])
         (let cur->datum ([syn syn])
           (syntax-parse (core-expand syn)
@@ -185,7 +211,7 @@
              (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
     (unless (or (inner-expand?) (type-infer/term reified-term))
       #;(printf "Delta: ~s~nGamma: ~s~n" (delta) (gamma))
-      (raise-syntax-error 'cur "term is ill-typed:" reified-term syn))
+      (raise-curnel-type-error 'cur->datum reified-term syn))
     reified-term)
 
   (define (datum->cur syn t)
@@ -223,8 +249,8 @@
       (term (reduce #,(delta) (subst-all #,(cur->datum syn) #,(first (bind-subst)) #,(second (bind-subst)))))))
 
   ;; Reflection tools
-  ;; TODO: Reflection tools should catch errors from eval-cur et al. to
-  ;; ensure users can provide better error messages.
+  ;; TODO: Reflection tools should catch internal errors, e.g., from eval-cur et al. to
+  ;; ensure users can provide better error messages. But should not catch errors caused by user macros.
 
   (define (local-env->gamma env)
     (for/fold ([gamma (gamma)])
@@ -247,14 +273,14 @@
     (and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t))
 
   ;; TODO: Document local-env
-  (define (type-infer/syn syn #:local-env [env '()])
+  (define (type-infer/syn #:local-env [env '()] syn)
     (parameterize ([gamma (local-env->gamma env)])
-      (with-handlers ([values (lambda _ #f)])
+      (with-handlers ([exn:cur:curnel:type? (lambda _ #f)])
         (let ([t (type-infer/term (eval-cur syn))])
         (and t (datum->cur syn t))))))
 
   (define (type-check/syn? syn type)
-    (with-handlers ([values (lambda _ #f)])
+    (with-handlers ([exn:cur:curnel:type? (lambda _ #f)])
       (type-check/term? (eval-cur syn) (eval-cur type))))
 
   ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is
diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt
index 8582306..b52733f 100644
--- a/cur-lib/cur/olly.rkt
+++ b/cur-lib/cur/olly.rkt
@@ -96,13 +96,12 @@
                          (thunk
                           (for/fold ([strs ""]
                                      [local-env (dict-set local-env #'n #'t)])
-                                    ([clause (syntax->list #'((x* : t*) ...))])
-                            (syntax-parse clause
-                               [(x (~datum :) t)
-                                (values
-                                 (format "~a~n| ~a : ~a" strs (syntax-e #'x)
-                                         (cur->coq #'t local-env))
-                                 (dict-set local-env #'x #'t))])))
+                                    ([x (attribute x*)]
+                                     [t (attribute t*)])
+                            (values
+                             (format "~a~n| ~a : ~a" strs (syntax-e x)
+                                     (cur->coq t local-env))
+                             (dict-set local-env x t))))
                          (lambda (x y) x))))
                "")]
             [(Type i) "Type"]
@@ -207,6 +206,7 @@
               lab:rule-name
               (~var t (conclusion name indices (attribute lab))))
              #:with constr-decl
+             ;; TODO: quasisyntax/loc
              #'(lab : (-> h ... (t.name t.arg ...)))
              ;; TODO: convert meta-vars such as e1 to e_1
              #:attr latex
diff --git a/cur-lib/cur/stdlib/sugar.rkt b/cur-lib/cur/stdlib/sugar.rkt
index 337e8d1..2ba03ef 100644
--- a/cur-lib/cur/stdlib/sugar.rkt
+++ b/cur-lib/cur/stdlib/sugar.rkt
@@ -31,7 +31,39 @@
     [lambda real-lambda]
     [define real-define]))
 
+;; Exceptions and such
 (begin-for-syntax
+  (define-struct (exn:cur:type exn:cur) () #:transparent)
+
+  (define (raise-cur-type-infer-error name v . other)
+    (format
+     "~aCur type error;~n  Could not infer any type~n    term: ~a~a"
+     (if name (format "~a:" name) "")
+     v
+     (for/fold ([str ""])
+               ([other other])
+       (format "~a~n    context: ~a" str other)))))
+
+(begin-for-syntax
+  #| TODO
+   | Design of "typed" macros for Cur.
+   |
+   | We can use syntax classes to emulate typed macros. The syntax
+   | class calls the type-checker to ensure the term parsed term is
+   | well-typed. This *must* not expand the the matched type as a side-effect.
+   | Unfortunately, to handle binding, patterns that have variables
+   | must thread binding information through while parsing in syntax
+   | parse. This would be simple if we had implicit monad syntax for
+   | it, but otherwise we must explicitly thread the environment
+   | information through the syntax classes. How annoying.
+   |
+   | Ideas:
+   |   Could create a "env" compile-time parameter...
+   |   Could expose Gamma, in some way...
+   |   Could use Racket namespaces? Might requrie abandoning Redex
+   |
+   |
+   |#
   (define (deduce-type-error term expected)
     (format
      "Expected ~a ~a, but ~a."
@@ -42,38 +74,68 @@
         "seems to be an unbound variable"]
        [_ "could not infer a type."])))
 
-  (define-syntax-class cur-term
+  (define-syntax-class cur-syntax
+    (pattern e:expr))
+
+  (define-syntax-class well-typed-cur-term
     (pattern
-     e:expr
+     e:cur-syntax
      #:attr type (type-infer/syn #'e)
-     ;; TODO: Reduce to smallest failing example.
-     #:fail-unless
-     (attribute type)
-     (deduce-type-error
-      #'e
-      "to be a well-typed Cur term")))
+     #:fail-unless (attribute type)
+     (raise-cur-type-infer-error #f #'e))))
 
+;; For delaying a type-check until the term is under a binder
+;; NB: This is an impressively awesome solution..... need to write something about it.
+(define-syntax (delayed-check syn)
+  (syntax-parse syn
+    [(_ e:well-typed-cur-term) #'e]))
+
+(begin-for-syntax
   (define-syntax-class parameter-declaration
-    (pattern (name:id (~datum :) type:cur-term))
+    #:commit
+    (pattern
+     (name:id (~datum :) ~! type:cur-syntax))
 
     (pattern
-     type:cur-term
-     #:attr name (format-id #'type "~a" (gensym 'anon-parameter)))))
+     type:cur-syntax
+     ;; NB: Anonymous parameters are not bound in the local env
+     #:attr name (format-id #'type "~a" (gensym 'anon-parameter))))
+
+  (define-syntax-class well-typed-parameter-declaration
+    #:commit
+    (pattern
+     (name:id (~datum :) ~! _type:cur-syntax)
+     #:attr type #'(delayed-check _type))
+
+    (pattern
+     _type:cur-syntax
+     ;; TODO: Duplicate code in parameter-declaration
+     #:attr type #'(delayed-check _type)
+     #:attr name (format-id #'type "~a" (gensym 'anon-parameter))))
+
+  (define-syntax-class well-typed-parameter-list
+    (pattern
+     (d:well-typed-parameter-declaration ...+)
+     #:attr names (attribute d.name)
+     #:attr types (attribute d.type))))
 
 ;; A multi-arity function type; takes parameter declaration of either
 ;; a binding (name : type), or type whose name is generated.
 ;; E.g.
 ;; (-> (A : Type) A A)
+
 (define-syntax (-> syn)
   (syntax-parse syn
-    [(_ d:parameter-declaration ...+ result:cur-term)
+    [(_ d:parameter-declaration ...+ e:cur-syntax)
+     #:with ds #'(d ...)
+     #:declare ds well-typed-parameter-list
      (foldr (lambda (src name type r)
               (quasisyntax/loc src
                 (forall (#,name : #,type) #,r)))
-            #'result
-            (attribute d)
-            (attribute d.name)
-            (attribute d.type))]))
+            #'(delayed-check e)
+            (syntax->list (attribute ds))
+            (attribute ds.names)
+            (attribute ds.types))]))
 
 ;; TODO: Add forall macro that allows specifying *names*, with types
 ;; inferred. unlike -> which require types but not names
@@ -82,23 +144,18 @@
 
 ;; TODO: Allows argument-declarations to have types inferred, similar
 ;; to above TODO forall
-(begin-for-syntax
-  ;; eta-expand syntax-class for error messages
-  (define-syntax-class argument-declaration
-    (pattern
-     e:parameter-declaration
-     #:attr name #'e.name
-     #:attr type #'e.type)))
 (define-syntax (lambda syn)
   (syntax-parse syn
-    [(_ d:argument-declaration ...+ body:expr)
+    [(_ d:parameter-declaration ... e:cur-syntax)
+     #:with ds #'(d ...)
+     #:declare ds well-typed-parameter-list
      (foldr (lambda (src name type r)
               (quasisyntax/loc src
                 (real-lambda (#,name : #,type) #,r)))
-            #'body
-            (attribute d)
-            (attribute d.name)
-            (attribute d.type))]))
+            #'(delayed-check e)
+            (syntax->list (attribute ds))
+            (attribute ds.names)
+            (attribute ds.types))]))
 
 (begin-for-syntax
   (define-syntax-class forall-type
@@ -123,7 +180,7 @@
 
 (define-syntax (#%app syn)
   (syntax-parse syn
-    [(_ f:cur-function ~! e:cur-term ...+)
+    [(_ f:well-typed-cur-term ~! e:well-typed-cur-term ...+)
      ;; Have to thread each argument through, to handle dependency.
      (for/fold ([type (attribute f.type)])
                ([arg (attribute e)]
@@ -143,8 +200,8 @@
        (normalize/syn
         #`(real-app
            (real-lambda (expected.parameter-name : expected.parameter-type)
-            expected.body)
-          #,arg)))
+                        expected.body)
+           #,arg)))
      (for/fold ([app (quasisyntax/loc syn
                        (real-app f #,(first (attribute e))))])
                ([arg (rest (attribute e))])
diff --git a/cur-test/cur/tests/olly.rkt b/cur-test/cur/tests/olly.rkt
index a2cda7b..35e4512 100644
--- a/cur-test/cur/tests/olly.rkt
+++ b/cur-test/cur/tests/olly.rkt
@@ -6,6 +6,9 @@
 (require
  rackunit
  cur/stdlib/sugar
+ cur/stdlib/nat
+ cur/stdlib/bool
+ cur/stdlib/prop
  cur/olly)
 
 (begin-for-syntax
@@ -30,28 +33,28 @@
    "(forall .+ : Type, Type)"
    (cur->coq #'(-> Type Type)))
   (let ([t (cur->coq
-            #'(define-relation (meow gamma term type)
-                [(g : gamma) (e : term) (t : type)
+            #'(define-relation (meow Nat Bool Nat)
+                [(n : Nat) (b : Bool) (m : Nat)
                  --------------- T-Bla
-                 (meow g e t)]))])
+                 (meow n b m)]))])
     (check-regexp-match
-     "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
+     "Inductive meow : \\(forall .+ : Nat, \\(forall .+ : Bool, \\(forall .+ : Nat, Type\\)\\)\\) :="
      (first (string-split t "\n")))
     (check-regexp-match
-     "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
+     "\\| T-Bla : \\(forall n : Nat, \\(forall b : Bool, \\(forall m : Nat, \\(\\(\\(meow n\\) b\\) m\\)\\)\\)\\)\\."
      (second (string-split t "\n"))))
   (let ([t (cur->coq
-            #'(elim nat Type (lambda (x : nat) nat) z
-                    (lambda (x : nat) (ih-x : nat) ih-x)
-                    e))])
+            #'(elim Nat Type (lambda (x : Nat) Nat) z
+                    (lambda (x : Nat) (ih-x : Nat) ih-x)
+                    z))])
     (check-regexp-match
-     "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
+     "\\(\\(\\(\\(Nat_rect \\(fun x : Nat => Nat\\)\\) z\\) \\(fun x : Nat => \\(fun ih_x : Nat => ih_x\\)\\)\\) z\\)"
      t))
   (check-regexp-match
-   "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
+   "Definition thm_plus_commutes := \\(forall n : Nat, \\(forall m : Nat, \\(\\(\\(== Nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
    (cur->coq
-    #'(define thm:plus-commutes (forall (n : nat) (m : nat)
-                                        (== nat (plus n m) (plus m n))))))
+    #'(define thm:plus-commutes (forall (n : Nat) (m : Nat)
+                                        (== Nat (plus n m) (plus m n))))))
   (check-regexp-match
-   "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
-   (cur->coq #'(define (add1 (n : nat)) (s n)))))
+   "Function add1 \\(n : Nat\\)  := \\(s n\\).\n"
+   (cur->coq #'(define (add1 (n : Nat)) (s n)))))