diff --git a/spectec/src/backend-ast/print.ml b/spectec/src/backend-ast/print.ml
index 1372e94ea3..99ad5fe216 100644
--- a/spectec/src/backend-ast/print.ml
+++ b/spectec/src/backend-ast/print.ml
@@ -126,6 +126,7 @@ and exp e =
   | CatE (e1, e2) -> Node ("cat", [exp e1; exp e2])
   | CvtE (e1, nt1, nt2) -> Node ("cvt", [numtyp nt1; numtyp nt2; exp e1])
   | SubE (e1, t1, t2) -> Node ("sub", [typ t1; typ t2; exp e1])
+  | AnnE (e1, t1) -> Node ("ann", [typ t1; exp e1])
 
 and expfield (at, e) =
   Node ("field", [mixop (Mixop.Atom at); exp e])
diff --git a/spectec/src/frontend/det.ml b/spectec/src/frontend/det.ml
index 840479ea31..94ab7e2617 100644
--- a/spectec/src/frontend/det.ml
+++ b/spectec/src/frontend/det.ml
@@ -46,7 +46,7 @@ and det_exp e =
   (* We consider arithmetic expressions determinate,
    * since we sometimes need to use invertible formulas. *)
   | CvtE (e1, _, _) | UnE (#Xl.Num.unop, _, e1) | TheE e1 | LiftE e1
-  | SubE (e1, _, _) -> det_exp e1
+  | SubE (e1, _, _) | AnnE (e1, _) -> det_exp e1
   | BinE (#Xl.Num.binop, _, e1, e2) | CatE (e1, e2) -> det_exp e1 ++ det_exp e2
   | OptE eo -> free_opt det_exp eo
   | ListE es | TupE es -> det_list det_exp es
@@ -123,7 +123,7 @@ and det_quant_exp e =
   | VarE x -> bound_varid x
   | BoolE _ | NumE _ | TextE _ -> empty
   | UnE (_, _, e1) | ProjE (e1, _) | TheE e1 | LiftE e1 | LenE e1
-  | CvtE (e1, _, _) | SubE (e1, _, _) ->
+  | CvtE (e1, _, _) | SubE (e1, _, _) | AnnE (e1, _) ->
     det_quant_exp e1
   | BinE (_, _, e1, e2) | CmpE (_, _, e1, e2)
   | IdxE (e1, e2) | MemE (e1, e2) | CatE (e1, e2) | CompE (e1, e2) ->
diff --git a/spectec/src/frontend/dim.ml b/spectec/src/frontend/dim.ml
index 6e733fdb7e..1e974eaf83 100644
--- a/spectec/src/frontend/dim.ml
+++ b/spectec/src/frontend/dim.ml
@@ -215,6 +215,9 @@ and check_exp dims ctx e =
     check_exp dims ctx e1;
     check_typ dims ctx t1;
     check_typ dims ctx t2
+  | AnnE (e1, t1) ->
+    check_exp dims ctx e1;
+    check_typ dims ctx t1
 
 and check_expfield dims ctx (_, e) =
   check_exp dims ctx e
@@ -575,6 +578,10 @@ and annot_exp side dims e : exp * occur =
       let t1', occur2 = annot_typ dims t1 in
       let t2', occur3 = annot_typ dims t2 in
       SubE (e1', t1', t2'), union occur1 (union occur2 occur3)
+    | AnnE (e1, t1) ->
+      let e1', occur1 = annot_exp side dims e1 in
+      let t1', occur2 = annot_typ dims t1 in
+      AnnE (e1', t1'), union occur1 occur2
   in {e with it}, occur
 
 and annot_expfield side dims (atom, e) : expfield * occur =
diff --git a/spectec/src/il/ast.ml b/spectec/src/il/ast.ml
index 7cb5709e5c..5da22f2ce8 100644
--- a/spectec/src/il/ast.ml
+++ b/spectec/src/il/ast.ml
@@ -81,6 +81,7 @@ and exp' =
   | IterE of exp * iterexp                  (* exp iter *)
   | CvtE of exp * numtyp * numtyp           (* exp : typ1 <:> typ2 *)
   | SubE of exp * typ * typ                 (* exp : typ1 <: typ2 *)
+  | AnnE of exp * typ                       (* exp : typ *)
 
 and expfield = atom * exp                   (* atom exp *)
 
diff --git a/spectec/src/il/dune b/spectec/src/il/dune
index 7ed9035a82..582d6c4127 100644
--- a/spectec/src/il/dune
+++ b/spectec/src/il/dune
@@ -3,3 +3,5 @@
   (libraries util zarith xl el)
   (modules ast eq free fresh subst iter env eval print debug valid)
 )
+
+(env (dev (flags :standard -w -8-26-27-32-33-34)))
diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml
index 7bbaddb154..8336701de2 100644
--- a/spectec/src/il/eval.ml
+++ b/spectec/src/il/eval.ml
@@ -398,6 +398,14 @@ and reduce_exp env e : exp =
       {e1' with note = e.note}
     | _ -> SubE (e1', t1', t2') $> e
     )
+  | AnnE (e1, t1) ->
+    let e1' = reduce_exp env e1 in
+    let t1' = reduce_typ env t1 in
+    (match e1'.it with
+    | BoolE _ | NumE _ | TextE _ | UnE _ | BinE _ | CmpE _
+    | MemE _ | LenE _ | SubE _ | CvtE _ | AnnE _ -> e1'
+    | _ -> AnnE (e1', t1') $> e
+    )
 
 and reduce_iter env = function
   | ListN (e, ido) -> ListN (reduce_exp env e, ido)
diff --git a/spectec/src/il/free.ml b/spectec/src/il/free.ml
index 728810da51..8a679fce76 100644
--- a/spectec/src/il/free.ml
+++ b/spectec/src/il/free.ml
@@ -75,6 +75,7 @@ and free_exp e =
   | IterE (e1, ite) -> (free_exp e1 -- bound_iterexp ite) ++ free_iterexp ite
   | CvtE (e1, _nt1, _nt2) -> free_exp e1
   | SubE (e1, t1, t2) -> free_exp e1 ++ free_typ t1 ++ free_typ t2
+  | AnnE (e1, t1) -> free_exp e1 ++ free_typ t1
 
 and free_expfield (_, e) = free_exp e
 
diff --git a/spectec/src/il/iter.ml b/spectec/src/il/iter.ml
index 3688a48458..bc3a0e5eb1 100644
--- a/spectec/src/il/iter.ml
+++ b/spectec/src/il/iter.ml
@@ -174,6 +174,7 @@ and exp e =
   | IterE (e1, it) -> iterexp exp e1 it
   | CvtE (e1, nt1, nt2) -> exp e1; numtyp nt1; numtyp nt2
   | SubE (e1, t1, t2) -> exp e1; typ t1; typ t2
+  | AnnE (e1, t1) -> exp e1; typ t1
  
 and expfield (at, e) = atom at; exp e
 
diff --git a/spectec/src/il/print.ml b/spectec/src/il/print.ml
index 05aea3ef35..c17590f394 100644
--- a/spectec/src/il/print.ml
+++ b/spectec/src/il/print.ml
@@ -159,6 +159,7 @@ and string_of_exp e =
     "(" ^ string_of_exp e1 ^ " : " ^ string_of_numtyp nt1 ^ " <:> " ^ string_of_numtyp nt2 ^ ")"
   | SubE (e1, t1, t2) ->
     "(" ^ string_of_exp e1 ^ " : " ^ string_of_typ t1 ^ " <: " ^ string_of_typ t2 ^ ")"
+  | AnnE (e1, t1) -> "(" ^ string_of_exp e1 ^ " : " ^ string_of_typ t1 ^ ")"
   ) ^
   (if !print_notes then ")@[" ^ string_of_typ e.note ^ "]" else "")
 
diff --git a/spectec/src/il/subst.ml b/spectec/src/il/subst.ml
index 885ed05e40..fc70296354 100644
--- a/spectec/src/il/subst.ml
+++ b/spectec/src/il/subst.ml
@@ -191,6 +191,7 @@ and subst_exp s e =
     CaseE (op, subst_exp s e1)
   | CvtE (e1, nt1, nt2) -> CvtE (subst_exp s e1, nt1, nt2)
   | SubE (e1, t1, t2) -> SubE (subst_exp s e1, subst_typ s t1, subst_typ s t2)
+  | AnnE (e1, t1) -> AnnE (subst_exp s e1, subst_typ s t1)
   ) $$ e.at % subst_typ s e.note
 
 and subst_expfield s (atom, e) = (atom, subst_exp s e)
diff --git a/spectec/src/il/valid.ml b/spectec/src/il/valid.ml
index 7a0fe7eb65..d90ce3f1f4 100644
--- a/spectec/src/il/valid.ml
+++ b/spectec/src/il/valid.ml
@@ -187,7 +187,7 @@ let rec valid_iter ?(side = `Rhs) env iter : Env.t =
       Env.bind_var env id (NumT `NatT $ e.at)
     )
 
-and valid_iterexp ?(side = `Rhs) env (it, xes) at : iter * Env.t =
+and valid_iterexp ?(elab = false) ?(side = `Rhs) env (it, xes) at : iter * Env.t =
   Debug.(log_at "il.valid_iterexp" at
     (fun _ -> il_iter it)
     (fun (it', _) -> il_iter it')
@@ -196,9 +196,9 @@ and valid_iterexp ?(side = `Rhs) env (it, xes) at : iter * Env.t =
   if xes = [] && it <= List1 && side = `Rhs then error at "empty iteration";
   let it' = match it with Opt -> Opt | _ -> List in
   it',
-  List.fold_left (fun env' (x, e) ->
-    let t = infer_exp env e in
-    valid_exp ~side env e t;
+  valid_binders (fun env' (x, e) ->
+    let t = infer_exp ~elab env e in
+    valid_exp ~elab ~side env e t;
     let t1 = as_iter_typ it' "iterator" env Check t e.at in
     Env.bind_var env' x t1
   ) env' xes
@@ -229,6 +229,7 @@ and valid_typ_bind env t : Env.t =
   | IterT (t1, iter) ->
     match iter with
     | ListN (e, _) -> error e.at "definite iterator not allowed in type"
+    | List1 -> error t.at "non-empty iterator not allowed in type"
     | _ ->
       let env' = valid_iter env iter in
       valid_typ env' t1;
@@ -272,7 +273,7 @@ and valid_typcase env (mixop, (t, qs, prems), _hints) =
 
 (* Expressions *)
 
-and infer_exp (env : Env.t) e : typ =
+and infer_exp ?(elab = false) (env : Env.t) e : typ =
   Debug.(log_at "il.infer_exp" e.at
     (fun _ -> fmt "%s : %s" (il_exp e) (il_typ e.note))
     (fun r -> fmt "%s" (il_typ r))
@@ -285,39 +286,39 @@ and infer_exp (env : Env.t) e : typ =
   | UnE (op, ot, _) -> let _t1, t' = infer_unop e.at op ot in t' $ e.at
   | BinE (op, ot, _, _) -> let _t1, _t2, t' = infer_binop e.at op ot in t' $ e.at
   | CmpE _ | MemE _ -> BoolT $ e.at
-  | IdxE (e1, _) -> as_list_typ "expression" env Infer (infer_exp env e1) e1.at
+  | IdxE (e1, _) -> as_list_typ "expression" env Infer (infer_exp ~elab env e1) e1.at
   | SliceE (e1, _, _)
   | UpdE (e1, _, _)
-  | ExtE (e1, _, _)
-  | CompE (e1, _) -> infer_exp env e1
+  | ExtE (e1, _, _) -> infer_exp ~elab env e1
+  | CompE (e1, e2) -> (try infer_exp ~elab env e1 with _ -> infer_exp ~elab env e2)
   | StrE _ -> error e.at "cannot infer type of record"
   | DotE (e1, atom) ->
-    let tfs = as_struct_typ "expression" env Infer (infer_exp env e1) e1.at in
+    let tfs = as_struct_typ "expression" env Infer (infer_exp ~elab env e1) e1.at in
     let t, _qs, _prems = find_field tfs atom e1.at in
     t
   | TupE es ->
-    TupT (List.map (fun eI -> "_" $ eI.at, infer_exp env eI) es) $ e.at
+    TupT (List.map (fun eI -> "_" $ eI.at, infer_exp ~elab env eI) es) $ e.at
   | CallE (x, as_) ->
     let ps, t, _ = Env.find_def env x in
-    let s = valid_args env as_ ps Subst.empty e.at in
+    let s = valid_args ~elab env as_ ps Subst.empty e.at in
     Subst.subst_typ s t
   | IterE (e1, ite) ->
-    let it, env' = valid_iterexp env ite e.at in
-    IterT (infer_exp env' e1, it) $ e.at
+    let it, env' = valid_iterexp ~elab env ite e.at in
+    IterT (infer_exp ~elab env' e1, it) $ e.at
   | ProjE (e1, i) ->
-    let t1 = infer_exp env e1 in
+    let t1 = infer_exp ~elab env e1 in
     let xts = as_tup_typ "expression" env Infer t1 e1.at in
     proj_tup_typ i xts e1 e.at
   | UncaseE (e1, op) ->
-    let t1 = infer_exp env e1 in
+    let t1 = infer_exp ~elab env e1 in
     (match as_variant_typ "expression" env Infer t1 e1.at with
     | [(op', (t, _, _), _)] when Eq.eq_mixop op op' -> t
     | _ -> error e.at "invalid case projection";
     )
   | OptE _ -> error e.at "cannot infer type of option"
-  | TheE e1 -> as_iter_typ Opt "option" env Check (infer_exp env e1) e1.at
+  | TheE e1 -> as_iter_typ Opt "option" env Check (infer_exp ~elab env e1) e1.at
   | ListE es ->
-    (match List.map (infer_exp env) es with
+    (match List.map (infer_exp ~elab env) es with
     | [] -> error e.at "cannot infer type of list"
     | t :: ts ->
       if List.for_all (Eq.eq_typ t) ts then
@@ -326,104 +327,107 @@ and infer_exp (env : Env.t) e : typ =
         error e.at "cannot infer type of list"
     )
   | LiftE e1 ->
-    let t1 = as_iter_typ Opt "lifting" env Check (infer_exp env e1) e1.at in
+    let t1 = as_iter_typ Opt "lifting" env Check (infer_exp ~elab env e1) e1.at in
     IterT (t1, List) $ e.at
   | LenE _ -> NumT `NatT $ e.at
-  | CatE (e1, e2) ->
-    let t1 = infer_exp env e1 in
-    let t2 = infer_exp env e2 in
-    if Eq.eq_typ t1 t2 then
-      t1
+  | CatE (e1, e2) -> (try infer_exp ~elab env e1 with _ -> infer_exp ~elab env e2)
+  | CaseE _ ->
+    if elab then
+      error e.at "cannot infer type of case constructor" 
     else
-      error e.at "cannot infer type of concatenation"
-  | CaseE _ -> e.note (* error e.at "cannot infer type of case constructor" *)
+      e.note
   | CvtE (_, _, t2) -> NumT t2 $ e.at
   | SubE (_, _, t2) -> t2
+  | AnnE (_, t1) -> t1
 
-
-and valid_exp ?(side = `Rhs) env e t =
+and valid_exp ?(elab = false) ?(side = `Rhs) env e t =
   Debug.(log_at "il.valid_exp" e.at
     (fun _ -> fmt "%s :%s %s == %s" (il_exp e) (il_side side) (il_typ e.note) (il_typ t))
     (Fun.const "ok")
   ) @@ fun _ ->
   valid_typ env t;
-  match e.it with
+  (match e.it with
   | VarE x when x.it = "_" && side = `Lhs -> ()
   | VarE x ->
     let t' = Env.find_var env x in
     equiv_typ env t' t e.at
   | BoolE _ | NumE _ | TextE _ ->
-    let t' = infer_exp env e in
+    let t' = infer_exp ~elab env e in
     equiv_typ env t' t e.at
   | UnE (op, nt, e1) ->
     let t1, t' = infer_unop e.at op nt in
-    valid_exp ~side env e1 (t1 $ e.at);
+    valid_exp ~elab ~side env e1 (t1 $ e.at);
     equiv_typ env (t' $ e.at) t e.at
   | BinE ((`AddOp | `SubOp) as op, nt, e1, ({it = NumE (`Nat _); _} as e2))
   | BinE ((`AddOp | `SubOp) as op, nt, ({it = NumE (`Nat _); _} as e1), e2) when side = `Lhs ->
     let t1, t2, t' = infer_binop e.at op nt in
-    valid_exp ~side env e1 (t1 $ e.at);
-    valid_exp ~side env e2 (t2 $ e.at);
+    valid_exp ~elab ~side env e1 (t1 $ e.at);
+    valid_exp ~elab ~side env e2 (t2 $ e.at);
     equiv_typ env (t' $ e.at) t e.at
   | BinE (op, nt, e1, e2) ->
     let t1, t2, t' = infer_binop e.at op nt in
-    valid_exp env e1 (t1 $ e.at);
-    valid_exp env e2 (t2 $ e.at);
+    valid_exp ~elab env e1 (t1 $ e.at);
+    valid_exp ~elab env e2 (t2 $ e.at);
     equiv_typ env (t' $ e.at) t e.at
   | CmpE (op, nt, e1, e2) ->
     let t' =
       match infer_cmpop e.at op nt with
       | Some t' -> t' $ e.at
-      | None -> try infer_exp env e1 with _ -> infer_exp env e2
+      | None -> try infer_exp ~elab env e1 with _ -> infer_exp ~elab env e2
     in
     let side' = if op = `EqOp then `Lhs else `Rhs in (* HACK *)
-    valid_exp ~side:side' env e1 t';
-    valid_exp ~side:side' env e2 t';
+    valid_exp ~elab ~side:side' env e1 t';
+    valid_exp ~elab ~side:side' env e2 t';
     equiv_typ env (BoolT $ e.at) t e.at
   | IdxE (e1, e2) ->
-    let t1 = infer_exp env e1 in
-    let t' = as_list_typ "expression" env Infer t1 e1.at in
-    valid_exp env e1 t1;
-    valid_exp env e2 (NumT `NatT $ e2.at);
-    equiv_typ env t' t e.at
+    valid_exp ~elab env e1 (IterT (t, List) $ e1.at);
+    valid_exp ~elab env e2 (NumT `NatT $ e2.at);
   | SliceE (e1, e2, e3) ->
     let _typ' = as_list_typ "expression" env Check t e1.at in
-    valid_exp env e1 t;
-    valid_exp env e2 (NumT `NatT $ e2.at);
-    valid_exp env e3 (NumT `NatT $ e3.at)
+    valid_exp ~elab env e1 t;
+    valid_exp ~elab env e2 (NumT `NatT $ e2.at);
+    valid_exp ~elab env e3 (NumT `NatT $ e3.at)
   | UpdE (e1, p, e2) ->
-    valid_exp env e1 t;
-    let t2 = valid_path env p t in
-    valid_exp env e2 t2
+    valid_exp ~elab env e1 t;
+    let t2 = valid_path ~elab env p t in
+    valid_exp ~elab env e2 t2
   | ExtE (e1, p, e2) ->
-    valid_exp env e1 t;
-    let t2 = valid_path env p t in
+    valid_exp ~elab env e1 t;
+    let t2 = valid_path ~elab env p t in
     let _typ21 = as_list_typ "path" env Check t2 p.at in
-    valid_exp env e2 t2
+    valid_exp ~elab env e2 t2
   | StrE efs ->
     let tfs = as_struct_typ "record" env Check t e.at in
-    valid_list (valid_expfield ~side) env efs tfs e.at
+    valid_list (valid_expfield ~elab ~side) env efs tfs e.at
   | DotE (e1, atom) ->
-    let t1 = infer_exp env e1 in
-    valid_exp env e1 t1;
+    let t1 = infer_exp ~elab env e1 in
+    valid_exp ~elab env e1 t1;
     valid_atom env atom;
     let tfs = as_struct_typ "expression" env Check t1 e1.at in
     let t', _qs, _prems = find_field tfs atom e1.at in
     equiv_typ env t' t e.at
   | CompE (e1, e2) ->
     let _ = as_comp_typ "expression" env Check t e.at in
-    valid_exp env e1 t;
-    valid_exp env e2 t
+    valid_exp ~elab env e1 t;
+    valid_exp ~elab env e2 t
   | MemE (e1, e2) ->
-    let t2 = infer_exp env e2 in
-    let t1 = as_list_typ "expression" env Check t2 e2.at in
-    valid_exp env e1 t1;
-    valid_exp env e2 t2;
+    let t1, t2 =
+      (try
+        let t2 = infer_exp ~elab env e2 in
+        let t1 = as_list_typ "expression" env Check t2 e2.at in
+        (t1, t2)
+      with _ ->
+        let t1 = infer_exp ~elab env e1 in
+        let t2 = IterT (t1, List) $ e2.at in
+        (t1, t2)
+    ) in
+    valid_exp ~elab env e1 t1;
+    valid_exp ~elab env e2 t2;
     equiv_typ env (BoolT $ e.at) t e.at
   | LenE e1 ->
-    let t1 = infer_exp env e1 in
+    let t1 = infer_exp ~elab env e1 in
     let _typ11 = as_list_typ "expression" env Infer t1 e1.at in
-    valid_exp env e1 t1;
+    valid_exp ~elab env e1 t1;
     equiv_typ env (NumT `NatT $ e.at) t e.at
   | TupE es ->
     let xts = as_tup_typ "tuple" env Check t e.at in
@@ -441,21 +445,21 @@ and valid_exp ?(side = `Rhs) env e t =
     in loop 0 es xts Subst.empty
   | CallE (x, as_) ->
     let ps, t', _ = Env.find_def env x in
-    let s = valid_args env as_ ps Subst.empty e.at in
+    let s = valid_args ~elab env as_ ps Subst.empty e.at in
     equiv_typ env (Subst.subst_typ s t') t e.at
   | IterE (e1, ite) ->
-    let it, env' = valid_iterexp ~side env ite e.at in
+    let it, env' = valid_iterexp ~elab ~side env ite e.at in
     let t1 = as_iter_typ it "iteration" env Check t e.at in
     valid_exp ~side env' e1 t1
   | ProjE (e1, i) ->
-    let t1 = infer_exp env e1 in
+    let t1 = infer_exp ~elab env e1 in
     let xts = as_tup_typ "expression" env Infer t1 e1.at in
     let side' = if List.length xts > 1 then `Rhs else side in
-    valid_exp ~side:side' env e1 (TupT xts $ t1.at);
+    valid_exp ~elab ~side:side' env e1 (TupT xts $ t1.at);
     equiv_typ env (proj_tup_typ i xts e1 e.at) t e.at
   | UncaseE (e1, op) ->
-    let t1 = infer_exp env e1 in
-    valid_exp ~side env e1 t1;
+    let t1 = infer_exp ~elab env e1 in
+    valid_exp ~elab ~side env e1 t1;
     valid_mixop env op;
     (match as_variant_typ "expression" env Infer t1 e1.at with
     | [(op', (t', _, _), _)] when Eq.eq_mixop op op' ->
@@ -464,50 +468,54 @@ and valid_exp ?(side = `Rhs) env e t =
     )
   | OptE eo ->
     let t1 = as_iter_typ Opt "option" env Check t e.at in
-    Option.iter (fun e1 -> valid_exp ~side env e1 t1) eo
+    Option.iter (fun e1 -> valid_exp ~elab ~side env e1 t1) eo
   | TheE e1 ->
-    valid_exp ~side env e1 (IterT (t, Opt) $ e1.at)
+    valid_exp ~elab ~side env e1 (IterT (t, Opt) $ e1.at)
   | ListE es ->
     let t1 = as_iter_typ List "list" env Check t e.at in
-    List.iter (fun eI -> valid_exp ~side env eI t1) es
+    List.iter (fun eI -> valid_exp ~elab ~side env eI t1) es
   | LiftE e1 ->
     let t1 = as_iter_typ List "lifting" env Check t e.at in
-    valid_exp ~side env e1 (IterT (t1, Opt) $ e1.at)
+    valid_exp ~elab ~side env e1 (IterT (t1, Opt) $ e1.at)
   | CatE (e1, ({it = ListE _ | CatE ({it = ListE _; _}, _); _} as e2))
   | CatE (({it = ListE _ | CatE ({it = ListE _; _}, _); _} as e1), e2) when side = `Lhs ->
     let _typ1 = as_iter_typ List "list" env Check t e.at in
-    valid_exp ~side env e1 t;
-    valid_exp ~side env e2 t
+    valid_exp ~elab ~side env e1 t;
+    valid_exp ~elab ~side env e2 t
   | CatE (e1, e2) ->
     let _typ1 = as_iter_typ List "list" env Check t e.at in
-    valid_exp env e1 t;
-    valid_exp env e2 t
+    valid_exp ~elab env e1 t;
+    valid_exp ~elab env e2 t
   | CaseE (op, e1) ->
     let cases = as_variant_typ "case" env Check t e.at in
     let t1, _qs, _prems = find_case cases op e1.at in
     valid_mixop env op;
-    valid_exp ~side env e1 t1
+    valid_exp ~elab ~side env e1 t1
   | CvtE (e1, nt1, nt2) ->
-    valid_exp ~side env e1 (NumT nt1 $ e1.at);
+    valid_exp ~elab ~side env e1 (NumT nt1 $ e1.at);
     equiv_typ env (NumT nt2 $e.at) t e.at;
   | SubE (e1, t1, t2) ->
     valid_typ env t1;
     valid_typ env t2;
-    valid_exp ~side env e1 t1;
+    valid_exp ~elab ~side env e1 t1;
     equiv_typ env t2 t e.at;
     sub_typ env t1 t2 e.at
+  | AnnE (e1, t1) ->
+    valid_typ env t1;
+    valid_exp ~elab ~side env e1 t1
+  );
+  if elab then e.note <- t
 
-
-and valid_expmix ?(side = `Rhs) env mixop e (mixop', t) at =
+and valid_expmix ?(elab = false) ?(side = `Rhs) env mixop e (mixop', t) at =
   if not (Eq.eq_mixop mixop mixop') then
     error at (
       "mixin notation `" ^ string_of_mixop mixop ^
       "` does not match expected notation `" ^ string_of_mixop mixop' ^ "`"
     );
   valid_mixop env mixop;
-  valid_exp ~side env e t
+  valid_exp ~elab ~side env e t
 
-and valid_expfield ~side env (atom1, e) (atom2, (t, _qs, _prems), _) =
+and valid_expfield ?(elab = false) ~side env (atom1, e) (atom2, (t, _qs, _prems), _) =
   Debug.(log_in_at "il.valid_expfield" e.at
     (fun _ -> fmt "%s %s :%s %s %s"
       (il_atom atom1) (il_exp e) (il_side side)
@@ -516,31 +524,34 @@ and valid_expfield ~side env (atom1, e) (atom2, (t, _qs, _prems), _) =
   );
   if not (Eq.eq_atom atom1 atom2) then error e.at "unexpected record field";
   valid_atom env atom1;
-  valid_exp ~side env e t
+  valid_exp ~elab ~side env e t
 
-and valid_path env p t : typ =
+and valid_path ?(elab = false) env p t : typ =
   valid_typ env t;
   let t' =
     match p.it with
     | RootP -> t
     | IdxP (p1, e1) ->
-      let t1 = valid_path env p1 t in
-      valid_exp env e1 (NumT `NatT $ e1.at);
+      let t1 = valid_path ~elab env p1 t in
+      valid_exp ~elab env e1 (NumT `NatT $ e1.at);
       as_list_typ "path" env Check t1 p1.at
     | SliceP (p1, e1, e2) ->
-      let t1 = valid_path env p1 t in
-      valid_exp env e1 (NumT `NatT $ e1.at);
-      valid_exp env e2 (NumT `NatT $ e2.at);
+      let t1 = valid_path ~elab env p1 t in
+      valid_exp ~elab env e1 (NumT `NatT $ e1.at);
+      valid_exp ~elab env e2 (NumT `NatT $ e2.at);
       let _ = as_list_typ "path" env Check t1 p1.at in
       t1
     | DotP (p1, atom) ->
-      let t1 = valid_path env p1 t in
+      let t1 = valid_path ~elab env p1 t in
       valid_atom env atom;
       let tfs = as_struct_typ "path" env Check t1 p1.at in
       let t, _qs, _prems = find_field tfs atom p1.at in
       t
   in
-  equiv_typ env p.note t' p.at;
+  if elab then
+    p.note <- t'
+  else
+    equiv_typ env p.note t' p.at;
   t'
 
 
@@ -585,20 +596,20 @@ and valid_sym env g : typ =
 
 (* Premises *)
 
-and valid_prem env prem =
+and valid_prem ?(elab = false) env prem =
   Debug.(log_in_at "il.valid_prem" prem.at (fun _ -> il_prem prem));
   match prem.it with
   | RulePr (x, as_, mixop, e) ->
     let ps, mixop', t, _rules = Env.find_rel env x in
     assert (Mixop.eq mixop mixop');
-    let s = valid_args env as_ ps Subst.empty prem.at in
-    valid_expmix env mixop e (mixop, Subst.subst_typ s t) e.at
+    let s = valid_args ~elab env as_ ps Subst.empty prem.at in
+    valid_expmix ~elab env mixop e (mixop, Subst.subst_typ s t) e.at
   | IfPr e ->
-    valid_exp env e (BoolT $ e.at)
+    valid_exp ~elab env e (BoolT $ e.at)
   | LetPr (e1, e2, xs) ->
-    let t = infer_exp env e2 in
-    valid_exp ~side:`Lhs env e1 t;
-    valid_exp env e2 t;
+    let t = try infer_exp ~elab env e2 with _ -> infer_exp ~elab env e1 in
+    valid_exp ~elab ~side:`Lhs env e1 t;
+    valid_exp ~elab ~side:`Rhs env e2 t;
     let target_ids = Free.{empty with varid = Set.of_list xs} in
     let free_ids = Free.(free_exp e1) in
     if not (Free.subset target_ids free_ids) then
@@ -610,20 +621,22 @@ and valid_prem env prem =
   | ElsePr ->
     ()
   | IterPr (prem', ite) ->
-    let _it, env' = valid_iterexp env ite prem.at in
+    let _it, env' = valid_iterexp ~elab env ite prem.at in
     valid_prem env' prem'
 
 
 (* Definitions *)
 
-and valid_arg env a p s =
+and valid_arg ?(elab = false) env a p s =
   Debug.(log_at "il.valid_arg" a.at
     (fun _ -> fmt "%s : %s" (il_arg a) (il_param p)) (Fun.const "ok")
   ) @@ fun _ ->
   match a.it, (Subst.subst_param s p).it with
   | ExpA e, ExpP (x, t) ->
-    valid_exp ~side:`Lhs env e t; Subst.add_varid s x e
-  | TypA t, TypP x -> valid_typ env t; Subst.add_typid s x t
+    valid_exp ~elab ~side:`Lhs env e t;
+    Subst.add_varid s x e
+  | TypA t, TypP x ->
+    valid_typ env t; Subst.add_typid s x t
   | DefA x', DefP (x, ps, t) ->
     let ps', t', _ = Env.find_def env x' in
     if not (Eval.equiv_functyp env (ps', t') (ps, t)) then
@@ -642,7 +655,7 @@ and valid_arg env a p s =
     error a.at ("sort mismatch for argument, expected `" ^
       Print.string_of_param p ^ "`, got `" ^ Print.string_of_arg a ^ "`")
 
-and valid_args env as_ ps s at : Subst.t =
+and valid_args ?(elab = false) env as_ ps s at : Subst.t =
   Debug.(log_if "il.valid_args" (as_ <> [] || ps <> [])
     (fun _ -> fmt "{%s} : {%s}" (il_args as_) (il_params ps)) (Fun.const "ok")
   ) @@ fun _ ->
@@ -651,8 +664,8 @@ and valid_args env as_ ps s at : Subst.t =
   | a::_, [] -> error a.at "too many arguments"
   | [], _::_ -> error at "too few arguments"
   | a::as', p::ps' ->
-    let s' = valid_arg env a p s in
-    valid_args env as' ps' s' at
+    let s' = valid_arg ~elab env a p s in
+    valid_args ~elab env as' ps' s' at
 
 and valid_param env p : Env.t =
   match p.it with
@@ -686,7 +699,7 @@ let valid_inst env ps inst =
     let _s = valid_args env' as_ ps Subst.empty inst.at in
     valid_deftyp env' dt
 
-let valid_rule env mixop t rule =
+let valid_rule ?(elab = false) env mixop t rule =
   Debug.(log_in "il.valid_rule" line);
   Debug.(log_in_at "il.valid_rule" rule.at
     (fun _ -> fmt "%s : %s = ..." (il_mixop mixop) (il_typ t))
@@ -694,10 +707,10 @@ let valid_rule env mixop t rule =
   match rule.it with
   | RuleD (_x, qs, mixop', e, prems) ->
     let env' = valid_quants env qs in
-    valid_expmix ~side:`Lhs env' mixop' e (mixop, t) e.at;
-    List.iter (valid_prem env') prems
+    valid_expmix ~elab ~side:`Lhs env' mixop' e (mixop, t) e.at;
+    List.iter (valid_prem ~elab env') prems
 
-let valid_clause env x ps t clause =
+let valid_clause ?(elab = false) env x ps t clause =
   Debug.(log_in "il.valid_clause" line);
   Debug.(log_in_at "il.valid_clause" clause.at
     (fun _ -> fmt "%s : (%s) -> %s" (il_id x) (il_params ps) (il_typ t))
@@ -705,9 +718,9 @@ let valid_clause env x ps t clause =
   match clause.it with
   | DefD (qs, as_, e, prems) ->
     let env' = valid_quants env qs in
-    let s = valid_args env' as_ ps Subst.empty clause.at in
-    valid_exp env' e (Subst.subst_typ s t);
-    List.iter (valid_prem env') prems
+    let s = valid_args ~elab env' as_ ps Subst.empty clause.at in
+    valid_exp ~elab env' e (Subst.subst_typ s t);
+    List.iter (valid_prem ~elab env') prems
 
 let valid_prod env ps t prod =
   Debug.(log_in "il.valid_prod" line);
@@ -741,32 +754,32 @@ let infer_def env d : Env.t =
   | _ -> env
 
 
-let rec valid_def env d : Env.t =
+let rec valid_def ?(elab = false) env d : Env.t =
   Debug.(log_in "il.valid_def" line);
   Debug.(log_in_at "il.valid_def" d.at (fun _ -> il_def d));
   match d.it with
   | TypD (x, ps, insts) ->
     let env' = valid_params env ps in
-    List.iter (valid_inst env' ps) insts;
-    Env.bind_typ env x (ps, insts);
+    List.iter (valid_inst env' ps) insts;  (* TODO(zilinc): elab *)
+    Env.bind_typ env x (ps, insts)
   | RelD (x, ps, mixop, t, rules) ->
     let env' = valid_params env ps in
     valid_typcase env' (mixop, (t, [], []), []);
-    List.iter (valid_rule env' mixop t) rules;
+    List.iter (valid_rule ~elab env' mixop t) rules;
     Env.bind_rel env x (ps, mixop, t, rules)
   | DecD (x, ps, t, clauses) ->
     let env' = valid_params env ps in
     valid_typ env' t;
-    List.iter (valid_clause env' x ps t) clauses;
+    List.iter (valid_clause ~elab env' x ps t) clauses;
     Env.bind_def env x (ps, t, clauses)
   | GramD (x, ps, t, prods) ->
     let env' = valid_params env ps in
     valid_typ env' t;
-    List.iter (valid_prod env' ps t) prods;
+    List.iter (valid_prod env' ps t) prods;  (* TODO(zilinc): elab *)
     Env.bind_gram env x (ps, t, prods)
   | RecD ds ->
     let env' = valid_binders infer_def env ds in
-    let env' = valid_binders valid_def env' ds in
+    let env' = valid_binders (valid_def ~elab) env' ds in
     List.iter (fun d ->
       match (List.hd ds).it, d.it with
       | HintD _, _ | _, HintD _
@@ -785,5 +798,5 @@ let rec valid_def env d : Env.t =
 
 (* Scripts *)
 
-let valid ds =
-  ignore (valid_binders valid_def Env.empty ds)
+let valid ?(elab = false) ds =
+  ignore (valid_binders (valid_def ~elab) Env.empty ds)
diff --git a/spectec/src/il/valid.mli b/spectec/src/il/valid.mli
index 7c9b74c3f6..c226955414 100644
--- a/spectec/src/il/valid.mli
+++ b/spectec/src/il/valid.mli
@@ -1 +1,4 @@
-val valid : Ast.script -> unit (* raises Error.Error *)
+(* Raises Error.Error.
+   `~elab` defaults to false. If true, it updates the type annotations in the input Ast.
+*)
+val valid : ?elab:bool -> Ast.script -> unit
diff --git a/spectec/src/il2al/free.ml b/spectec/src/il2al/free.ml
index af0f4029f7..f7930a21c0 100644
--- a/spectec/src/il2al/free.ml
+++ b/spectec/src/il2al/free.ml
@@ -21,7 +21,7 @@ let rec free_exp ignore_listN e =
   match e.it with
   | VarE id -> free_varid id
   | BoolE _ | NumE _ | TextE _ -> empty
-  | CvtE (e1, _, _) | UnE (_, _, e1) | LiftE e1 | LenE e1 | TheE e1 | SubE (e1, _, _)
+  | CvtE (e1, _, _) | UnE (_, _, e1) | LiftE e1 | LenE e1 | TheE e1 | SubE (e1, _, _) | AnnE (e1, _)
   | ProjE (e1, _) ->
     f e1
   | DotE (e1, _) | CaseE (_, e1) | UncaseE (e1, _) ->
diff --git a/spectec/src/il2al/il_walk.ml b/spectec/src/il2al/il_walk.ml
index 90d5c842ef..69929bb7df 100644
--- a/spectec/src/il2al/il_walk.ml
+++ b/spectec/src/il2al/il_walk.ml
@@ -51,7 +51,8 @@ let rec transform_exp t e =
     | CatE (e1, e2) -> CatE (t_exp e1, t_exp e2)
     | MemE (e1, e2) -> MemE (t_exp e1, t_exp e2)
     | CaseE (mixop, e1) -> CaseE (mixop, t_exp e1)
-    | SubE (e1, _t1, t2) -> SubE (t_exp e1, _t1, t2)
+    | SubE (e1, t1, t2) -> SubE (t_exp e1, t1, t2)
+    | AnnE (e1, t1) -> AnnE (t_exp e1, t1)
   in
   f { e with it }
 
diff --git a/spectec/src/middlend/sideconditions.ml b/spectec/src/middlend/sideconditions.ml
index 5000d56768..66f4476721 100644
--- a/spectec/src/middlend/sideconditions.ml
+++ b/spectec/src/middlend/sideconditions.ml
@@ -79,6 +79,7 @@ let rec t_exp env e : prem list =
   | LiftE exp
   | CvtE (exp, _, _)
   | SubE (exp, _, _)
+  | AnnE (exp, _)
   -> t_exp env exp
   | BinE (_, _, exp1, exp2)
   | CmpE (_, _, exp1, exp2)
diff --git a/spectec/src/middlend/sub.ml b/spectec/src/middlend/sub.ml
index 1aa0fe5d91..fab239281a 100644
--- a/spectec/src/middlend/sub.ml
+++ b/spectec/src/middlend/sub.ml
@@ -167,6 +167,7 @@ and t_exp' env = function
   | CaseE (mixop, e) -> CaseE (mixop, t_exp env e)
   | CvtE (exp, t1, t2) -> CvtE (t_exp env exp, t1, t2)
   | SubE (e, t1, t2) -> SubE (e, t1, t2)
+  | AnnE (e1, t1) -> AnnE (t_exp env e1, t1)
 
 and t_iter env = function
   | ListN (e, id_opt) -> ListN (t_exp env e, id_opt)
diff --git a/spectec/src/middlend/totalize.ml b/spectec/src/middlend/totalize.ml
index ade0ec336c..263bc8c7c9 100644
--- a/spectec/src/middlend/totalize.ml
+++ b/spectec/src/middlend/totalize.ml
@@ -105,6 +105,7 @@ and t_exp' env = function
   | CaseE (mixop, e) -> CaseE (mixop, t_exp env e)
   | CvtE (exp, t1, t2) -> CvtE (t_exp env exp, t1, t2)
   | SubE (exp, t1, t2) -> SubE (t_exp env exp, t_typ env t1, t_typ env t2)
+  | AnnE (exp, t1) -> AnnE (t_exp env exp, t_typ env t1)
 
 and t_iter env = function
   | ListN (e, id_opt) -> ListN (t_exp env e, id_opt)
diff --git a/spectec/src/middlend/unthe.ml b/spectec/src/middlend/unthe.ml
index fb2155f825..9a20e1e0c8 100644
--- a/spectec/src/middlend/unthe.ml
+++ b/spectec/src/middlend/unthe.ml
@@ -136,6 +136,7 @@ and t_exp' n e : eqns * exp' =
   | CaseE (mixop, exp) -> t_e n exp (fun exp' -> CaseE (mixop, exp'))
   | CvtE (exp, a, b) -> t_e n exp (fun exp' -> CvtE (exp', a, b))
   | SubE (exp, a, b) -> t_e n exp (fun exp' -> SubE (exp', a, b))
+  | AnnE (exp, a) -> t_e n exp (fun exp' -> AnnE (exp', a))
 
   | BinE (bo, nto, exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> BinE (bo, nto, e1', e2'))
   | CmpE (co, nto, exp1, exp2) -> t_ee n (exp1, exp2) (fun (e1', e2') -> CmpE (co, nto, e1', e2'))
diff --git a/spectec/src/util/source.ml b/spectec/src/util/source.ml
index 58e72eec3f..943cb9f1db 100644
--- a/spectec/src/util/source.ml
+++ b/spectec/src/util/source.ml
@@ -38,18 +38,18 @@ let string_of_region r =
 
 (* Phrases *)
 
-type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b}
+type ('a, 'b) note_phrase = {at : region; it : 'a; mutable note : 'b}
 type 'a phrase = ('a, unit) note_phrase
 
 let ($) it at = {it; at; note = ()}
 let ($$) it (at, note) = {it; at; note}
 let (%) at note = (at, note)
+let ($>) it e = {e with it}
 
 let it {it; _} = it
 let at {at; _} = at
 let note {note; _} = note
 
-
 (* Utilities *)
 
 let map f {it; at; note} = {it = f it; at; note}
diff --git a/spectec/src/util/source.mli b/spectec/src/util/source.mli
index dd3fb44334..533b0b02c1 100644
--- a/spectec/src/util/source.mli
+++ b/spectec/src/util/source.mli
@@ -18,12 +18,13 @@ val string_of_region : region -> string
 
 (* Phrases *)
 
-type ('a, 'b) note_phrase = {at : region; it : 'a; note : 'b}
+type ('a, 'b) note_phrase = {at : region; it : 'a; mutable note : 'b}
 type 'a phrase = ('a, unit) note_phrase
 
 val ($) : 'a -> region -> 'a phrase
 val ($$) : 'a -> region * 'b -> ('a, 'b) note_phrase
 val (%) : region -> 'b -> region * 'b
+val ($>) : 'a -> ('a, 'b) note_phrase -> ('a, 'b) note_phrase 
 
 val it : ('a, 'b) note_phrase -> 'a
 val at : ('a, 'b) note_phrase -> region