diff --git a/examples/type-level.1ml b/examples/type-level.1ml
index 28fdba0b..6abe3fa8 100644
--- a/examples/type-level.1ml
+++ b/examples/type-level.1ml
@@ -2,74 +2,143 @@ local import "prelude"
 
 ;; 1ML basically gives you simply typed lambda calculus (STLC) at the type
 ;; level, which is unsurprising as 1ML is just as powerful as Fω.  You can even
-;; use lambda and let -expressions at the type level (note the `fst` and `snd`
-;; definitions below).  So, you can encode various kinds of stuff at the type
-;; level.  Of course, STLC is quite restrictive.
+;; use lambda and let -expressions at the type level.  STLC is quite
+;; restrictive, but you can still encode various kinds of stuff at the type
+;; level.
 
-TypeLevel = {
+TypeLevel: {
+  Pair: {
+    type t = (type _ _ _) -> type
+
+    fst: t -> type
+    snd: t -> type
+
+    of: type -> type -> t
+
+    cross: (type _ _) -> (type _ _) -> t -> t
+
+    map: (type _ _) -> t -> t
+  }
+
+  Bool: {
+    type t = type -> type -> type
+
+    true: t
+    false: t
+
+    not: t -> t
+
+    andAlso: t -> t -> t
+    orElse: t -> t -> t
+
+    equals: t -> t -> t
+  }
+
+  Alt: {
+    type t = (type _ _) -> (type _ _) -> type
+
+    inL: type -> t
+    inR: type -> t
+
+    isL: t -> Bool.t
+    isR: t -> Bool.t
+
+    case: t -> t
+  }
+
+  Nat: {
+    type t = (type _ _) -> type -> type
+
+    isZero: t -> Bool.t
+
+    zero: t
+    one: t
+
+    succ: t -> t
+    (+): t -> t -> t
+    (*): t -> t -> t
+  }
+
+  List: {
+    type t = type -> (type _ _ _) -> type
+
+    nil: t
+    (::): type -> t -> t
+
+    map: (type _ _) -> t -> t
+
+    isNil: t -> Bool.t
+
+    head: t -> type
+  }
+} = {
   Pair = {
     type t = (type _ _ _) -> type
 
-    type fst (p: t) = p fun fst _ => fst
-    type snd (p: t) = p fun _ snd => snd
+    type fst (p: t): type = p fun fst _ => fst
+    type snd (p: t): type = p fun _ snd => snd
 
-    type of fst snd (type d _ _) = d fst snd
+    type of fst snd: t = fun (type d _ _) => d fst snd
 
-    type cross (type f _) (type s _) (p: t) (type d _ _) =
+    type cross (type f _) (type s _) (p: t): t = fun (type d _ _) =>
       of (f (fst p)) (s (snd p)) d
 
-    type map (type f _) (p: t) (type d _ _) = cross f f p d
+    type map (type f _) (p: t): t = fun (type d _ _) => cross f f p d
   }
 
   Bool = {
     type t = type -> type -> type
 
-    type true  true     _ = true
-    type false    _ false = false
+    type  true: t = fun true     _ => true
+    type false: t = fun    _ false => false
 
-    type not (x: t) true false = x false true
+    type not (x: t): t = fun true false => x false true
 
-    type andAlso (l: t) (r: t) false true = l (r true false) false
-    type  orElse (l: t) (r: t) false true = l true (r true false)
+    type andAlso (l: t) (r: t): t = fun false true => l (r true false) false
+    type  orElse (l: t) (r: t): t = fun false true => l true (r true false)
 
-    type equals (l: t) (r: t) true false = l (r true false) (r false true)
+    type equals (l: t) (r: t): t =
+      fun true false => l (r true false) (r false true)
   }
 
   Alt = {
-    type t = (type -> type) -> (type -> type) -> type
+    type t = (type _ _) -> (type _ _) -> type
 
-    type inL v (type inL _) (type _   _) = inL v
-    type inR v (type _   _) (type inR _) = inR v
+    type inL v: t = fun (type inL _) (type _   _) => inL v
+    type inR v: t = fun (type _   _) (type inR _) => inR v
 
-    type isL (a: t) true false = a (fun _ => true) (fun _ => false)
-    type isR (a: t) true false = a (fun _ => false) (fun _ => true)
+    type isL (a: t): Bool.t =
+      fun true false => a (fun _ => true) (fun _ => false)
+    type isR (a: t): Bool.t =
+      fun true false => a (fun _ => false) (fun _ => true)
 
     type case (a: t) (type inL _) (type inR _) = a inL inR
   }
 
   Nat = {
-    type t = (type -> type) -> type -> type
+    type t = (type _ _) -> type -> type
 
-    type isZero (n: t) true false = n (fun _ => false) true
+    type isZero (n: t): Bool.t = fun true false => n (fun _ => false) true
 
-    type  zero (type _    _) zero = zero
-    type   one (type succ _) zero = succ zero
+    type zero: t = fun (type _    _) zero => zero
+    type  one: t = fun (type succ _) zero => succ zero
 
-    type  succ        (n: t) (type succ _) zero = succ (n succ zero)
-    type  plus (m: t) (n: t) (type succ _) zero = n succ (m succ zero)
-    type times (m: t) (n: t) (type succ _) zero = n (m succ) zero
+    type     succ (n: t): t = fun (type succ _) zero => succ (n succ zero)
+    type (m: t) + (n: t): t = fun (type succ _) zero => n succ (m succ zero)
+    type (m: t) * (n: t): t = fun (type succ _) zero => n (m succ) zero
   }
 
   List = {
-    type t = type -> (type -> type -> type) -> type
+    type t = type -> (type _ _ _) -> type
 
-    type nil            nil (type _ :: _) = nil
-    type (x :: (xs: t)) nil (type _ :: _) = x :: xs nil (::)
+    type nil           : t = fun nil (type _ :: _) => nil
+    type (x :: (xs: t)): t = fun nil (type _ :: _) => x :: xs nil (::)
 
-    type map (type fn _) (xs: t) nil (type _ :: _) = xs nil fun x => (::) (fn x)
+    type map (type fn _) (xs: t): t =
+      fun nil (type _ :: _) => xs nil fun x => (::) (fn x)
 
-    type isNil (xs: t) true false = xs true fun _ _ => false
+    type isNil (xs: t): Bool.t = fun true false => xs true fun _ _ => false
 
-    type head (xs: t) = xs zero fun h _ => h
+    type head (xs: t): type = xs zero fun h _ => h
   }
 }
diff --git a/parser.mly b/parser.mly
index a6c9bf5b..918cb198 100644
--- a/parser.mly
+++ b/parser.mly
@@ -116,10 +116,12 @@ implparam :
 annparam :
   | LPAR head COLON typ RPAR
     { (headB($2)@@ati 2, $4, Expl@@ati 3)@@at() }
-  | LPAR typpat RPAR
-    { let (head, typparams) = $2 in
-      (headB(head)@@head.at, funT(typparams, TypT@@at(), Pure@@ati 2)@@ati 2,
-        Expl@@ati 2)@@at() }
+  | LPAR typpat optannot RPAR
+    { let (h, tps) = $2 in
+      (headB(h)@@h.at,
+       funT(tps,
+         Lib.Option.value $3 ~default:(TypT@@at()), Pure@@ati 2)@@ati 2,
+       Expl@@ati 2)@@at() }
   | implparam
     { $1 }
 ;
@@ -220,9 +222,9 @@ optannot :
 
 opttypdef :
   |
-    { TypT@@at() }
+    { None }
   | EQUAL typ
-    { EqT(typE($2)@@ati 2)@@ati 2 }
+    { Some (typE($2)@@ati 2) }
 ;
 
 atdec :
@@ -233,8 +235,16 @@ atdec :
         @@at() }
   | name
     { VarD($1, funT([], EqT(VarE($1)@@ati 1)@@ati 1, Pure@@ati 1)@@ati 1)@@at() }
-  | typdec opttypdef
-    { VarD(fst $1, funT(snd $1, $2, Pure@@at())@@at())@@at() }
+  | typdec optannot opttypdef
+    { VarD(fst $1,
+        funT(snd $1,
+          (match $2, $3 with
+           | None, None -> TypT@@at()
+           | Some t2, None -> t2
+           | None, Some te3 -> EqT(te3)@@ati 3
+           | Some t2, Some te3 ->
+             EqT(annotE(te3, t2)@@span[ati 2; ati 3])@@span[ati 2; ati 3]),
+          Pure@@at())@@at())@@at() }
   | ELLIPSIS typ
     { InclD($2)@@at() }
   | LET bind IN typ
@@ -431,8 +441,8 @@ atbind :
     { patB($1, $2($4))@@at() }
   | name
     { VarB($1, VarE($1.it@@at())@@at())@@at() }
-  | typpat EQUAL typ
-    { VarB(fst $1, funE(snd $1, typE($3)@@ati 3)@@at())@@at() }
+  | typpat bindanns_opt EQUAL typ
+    { VarB(fst $1, funE(snd $1, $2(typE($4)@@span[ati 2; ati 4]))@@at())@@at() }
   | ELLIPSIS exp
     { InclB($2)@@at() }
   | DO exp
@@ -470,10 +480,12 @@ atpat :
     { annotP(headP($2)@@$2.at, funT($3::$4, $6, Pure@@at())@@at())@@at() }
   | LPAR patlist RPAR
     { match $2 with [p] -> p | ps -> tupP(ps, at())@@at() }
-  | LPAR typpat RPAR
-    { let (head, typparams) = $2 in
-      annotP(headP(head)@@head.at,
-        funT(typparams, TypT@@at(), Pure@@at())@@at())@@at() }
+  | LPAR typpat optannot RPAR
+    { let (h, tps) = $2 in
+      annotP(headP(h)@@h.at,
+        funT(tps,
+          Lib.Option.value $3 ~default:(TypT@@at()),
+          Pure@@at())@@at())@@at() }
 ;
 annpat_op :
   | COLON
@@ -510,10 +522,13 @@ atdecon :
   | name typparam typparamlist COLON typ
     { ($1, annotP(varP($1)@@$1.at,
        funT($2::$3, $5, Pure@@at())@@at())@@at())@@at() }
-  | typdec
-    { let (name, typparams) = $1 in
-      (name, annotP(varP(name)@@name.at,
-       funT(typparams, TypT@@at(), Pure@@at())@@at())@@at())@@at() }
+  | typdec optannot
+    { let (n, tps) = $1 in
+      (n,
+       annotP(varP(n)@@n.at,
+         funT(tps,
+           Lib.Option.value $2 ~default:(TypT@@at()),
+           Pure@@at())@@at())@@at())@@at() }
 /*
   | LPAR decon RPAR
     { $2 }
diff --git a/regression.1ml b/regression.1ml
index e871ebfb..66b1adeb 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -74,6 +74,22 @@ do ManifestTycon.t {} {type t = int, x = 1}
 
 ;;
 
+Nat: {
+  type t = (type _ _ : type) -> type -> type
+  type Zero       : t = fun (type S _ : type) Z : type => Z
+  type Inc (n: t) : t = fun (type S _ : type) Z : type => S (n S Z)
+} = {}
+
+let
+  {type P _: type -> type} = {P = Pair.t}
+  (type P' _: type -> type) = Pair.t
+  F (type P _: type -> type) = P int text
+  do (42, "101"): F P
+  do (42, "101"): F P'
+in {}
+
+;;
+
 AmateurOptics = {
   type FUNCTOR = {
     type t a