diff --git a/Makefile b/Makefile
index feb83b03..6e441b22 100644
--- a/Makefile
+++ b/Makefile
@@ -4,8 +4,8 @@
 
 NAME = 1ml
 MODULES = \
-  lib source prim syntax parser lexer \
-  fomega types iL env erase trace sub elab \
+  lib source prim fomega types env syntax \
+  parser lexer iL erase trace sub elab \
   lambda compile \
   main
 NOMLI = syntax iL main
diff --git a/elab.ml b/elab.ml
index 39cf2667..f1c2633b 100644
--- a/elab.ml
+++ b/elab.ml
@@ -557,6 +557,8 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
       ExT([], t), Pure, lift_warn exp.at t env (zs1 @ zs2 @ zs3),
       IL.LetE(e, "_", materialize_typ t)
     )
+  | EL.WithEnvE (toExp) ->
+    elab_exp env (toExp env) l
 
 (*
 rec (X : (b : type) => {type t; type u a}) fun (b : type) => {type t = (X int.u b, X bool.t); type u a = (a, X b.t)}
diff --git a/lexer.mll b/lexer.mll
index 376783db..bf9f7f29 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -70,6 +70,7 @@ rule token = parse
   | "_" { HOLE }
   | "and" { AND }
   | "as" { AS }
+  | "data" { DATA }
   | "do" { DO }
   | "else" { ELSE }
   | "end" { END }
diff --git a/parser.mly b/parser.mly
index 8f1a10c6..d7b61c26 100644
--- a/parser.mly
+++ b/parser.mly
@@ -35,6 +35,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %token DOT AT TICK
 %token COMMA SEMI
 %token TYPE_ERROR
+%token DATA
 
 %token EOF
 
@@ -322,6 +323,8 @@ annexp :
 exp :
   | annexp
     { $1 }
+  | DATA name name typparamlist SEAL typ
+    { dataE($2, $3, $4, $6, at())@@at() }
   | FUN param paramlist DARROW exp
     { funE($2::$3, $5)@@at() }
   | IF exp THEN exp ELSE infexp COLON typ
diff --git a/regression.1ml b/regression.1ml
index 1b07ed67..f97d8276 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -59,6 +59,112 @@ PolyRec = {
   t0 = @(t int) (right (@(t (type (int, int))) (left (0, 0))));
 };
 
+;;
+
+IT = data case t _ :> {
+  Int  :  Int.t -> case Int.t;
+  Text : Text.t -> case Text.t;
+};
+
+IT = let
+  type I (type t _) (type case _) = {
+    Int  :  Int.t -> case Int.t;
+    Text : Text.t -> case Text.t;
+  };
+  type J (type t _) = {type case _; ...I t case};
+  type T (type t _) x = (c: J t) -> c.case x;
+  ...{
+    t = rec (type t _) => fun (type x) => type wrap T t x;
+    case 'x (type case _) (cs: I t case) e =
+      (unwrap e.@(t _): wrap T t x) {case; ...cs};
+    mk 'x (c: T t x) = @(t x) (wrap c: wrap T t x);
+  } :> {
+    type t _;
+    case 'x: (type case _) => I t case => t x -> case x;
+    mk 'x: T t x => t x;
+  };
+  J = J t;
+in {
+  t; case;
+  Int  v = mk (fun (r: J) => r.Int  v);
+  Text v = mk (fun (r: J) => r.Text v);
+};
+
+IT = {
+  ...IT;
+
+  impossible: t int -> int = case (fun (type t) => t) {
+    Int  x = x;
+    Text x = x;
+  };
+
+  i: int = impossible (Int 9);
+  ;;t: text = impossible (Text "nine");
+};
+
+;;
+
+Ord = data case t :> {
+  Lt : case;
+  Eq : case;
+  Gt : case;
+};
+
+Opt = data case t x :> {
+  None :      case;
+  Some : x -> case;
+};
+
+Alt = {
+  ...data case t l r :> {
+    Left  : l -> case;
+    Right : r -> case;
+  };
+
+  ;;Left  'l 'r (v: l) = mk (fun (r: J t l r) => r.Left v);
+  ;;Right 'l 'r (v: r) = mk (fun (r: J t l r) => r.Right v);
+};
+
+List = let
+  ...let
+    type I (type case) (type t _) x = {
+      nil     :             case;
+      (::) 'n : x -> t x -> case;
+    };
+    type J (type t _) x = {type case; ...I case t x};
+    type T (type t _) x = (c: J t x) -> c.case;
+  in {
+    t = rec (type t _) => fun (type x) => type wrap T t x;
+    case '(type case) 'x 'n (cs: I case t x) (e: t x) =
+      (unwrap e.@(t x): wrap T t x) {case; ...cs};
+    mk 'x (c: T t x) = @(t x) (wrap c: wrap T t x);
+    D = J t;
+  } :> {
+    type t _;
+    case '(type case) 'x 'n: I case t x => t x -> case;
+    mk 'x: T t x => t x;
+    type D x = J t x;
+  };
+in {
+  t; case;
+  nil  'x                     = mk (fun (r: D x) => r.nil);
+  (::) 'x 'n (v: x) (vs: t x) = mk (fun (r: D x) => r.:: v vs);
+};
+
+List' = {
+  ...data case t x :> {
+    nil  :             case;
+    (::) : x -> t x => case;
+  };
+
+;;  nil  'x                  = mk (fun (r: J x) => r.nil);
+;;  (::) 'x (v: x) (vs: t x) = mk (fun (r: J x) => r.:: v vs);
+
+  isEmpty = case {nil = true; (::) _ _ = false};
+};
+
+;;
+
 N :> {
   type Z;
   type S _;
@@ -67,31 +173,50 @@ N :> {
   type S _ = {};
 };
 
+ListN'' = let
+    type I (type case _) (type t _ _) x = {
+      nil     :               case N.Z;
+      (::) 'n : x -> t x n -> case (N.S n);
+    };
+    type J (type t _ _) x = {type case _; ...I case t x};
+    type T (type t _ _) x n = (c: J t x) -> c.case n;
+  in {
+    t = rec (type t _ _) => fun (type x) (type n) => type wrap T t x n;
+    case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
+      (unwrap e.@(t x n): wrap T t x n) {case; ...cs};
+    mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n);
+    D = J t;
+  } :> {
+    type t _ _;
+    case (type case _) 'x 'n: I case t x => t x n -> case n;
+    mk 'x 'n: T t x n => t x n;
+    type D x = J t x;
+  };
+
 ListN = let
-  type I (type x) (type p _) (type t _ _) = {
-    nil     :               p N.Z;
-    (::) 'n : x -> t x n -> p (N.S n);
+  ...let
+    type I (type case _) (type t _ _) x = {
+      nil     :               case N.Z;
+      (::) 'n : x -> t x n -> case (N.S n);
+    };
+    type J (type t _ _) x = {type case _; ...I case t x};
+    type T (type t _ _) x n = (c: J t x) -> c.case n;
+  in {
+    t = rec (type t _ _) => fun (type x) (type n) => type wrap T t x n;
+    case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
+      (unwrap e.@(t x n): wrap T t x n) {case; ...cs};
+    mk 'x 'n (c: T t x n) = @(t x n) (wrap c: wrap T t x n);
+    D = J t;
+  } :> {
+    type t _ _;
+    case (type case _) 'x 'n: I case t x => t x n -> case n;
+    mk 'x 'n: T t x n => t x n;
+    type D x = J t x;
   };
-  type T x n (type t _ _) = (type p _) => I x p t -> p n;
 in {
-  t = rec (type t _ _) => fun (type x) (type n) => type wrap T x n t;
-
-  case 'x 'n (type p _) (cs: I x p t) e =
-    (unwrap e.@(t _ _): wrap T x n t) p cs;
-
-  local
-    mk 'x 'n (c: T x n t) = @(t x n) (wrap c: wrap T x n t);
-  in
-    nil  'x                       = mk (fun (type p _) (r: I x p t) => r.nil);
-    (::) 'x 'n (v: x) (vs: t x n) = mk (fun (type p _) (r: I x p t) => r.:: v vs);
-  end;
-} :> {
-  type t _ _;
-
-  case 'x 'n: (type p _) => I x p t => t x n -> p n;
-
-  nil  'x    :               t x N.Z;
-  (::) 'x 'n : x => t x n => t x (N.S n);
+  t; case;
+  nil  'x                       = mk (fun (r: D x) => r.nil);
+  (::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs);
 };
 
 ListN = {
@@ -101,4 +226,28 @@ ListN = {
       nil = nil;
       (::) x xs = xy x :: map xs;
     };
+  foldLeft 'x 's (sxs: s -> x -> s) = rec (foldLeft: 'n => s -> t x n -> s) => fun v =>
+    case (fun (type n) => s) {
+      nil = v;
+      (::) x xs = foldLeft (sxs v x) xs;
+    };
+  otw = 1 :: (2 :: (3 :: nil));
+  sum = foldLeft (+) 0 otw;
+  otw' = map (fun i => "Int.toText missing") otw;
+};
+
+ListN' = {
+  ...data case t x _ :> {
+    nil     :               case N.Z;
+    (::) 'n : x -> t x n -> case (N.S n);
+  };
+
+;;  nil  'x                       = mk (fun (r: D x) => r.nil);
+;;  (::) 'x 'n (v: x) (vs: t x n) = mk (fun (r: D x) => r.:: v vs);
+;;
+;;  map 'x 'y 'n (xy: x -> y) = rec (map: 'n => t x n -> t y n) =>
+;;    case (t y) {
+;;      nil = nil;
+;;      (::) x xs = xy x :: map xs;
+;;    };
 };
diff --git a/syntax.ml b/syntax.ml
index f317ad73..519f3aa1 100644
--- a/syntax.ml
+++ b/syntax.ml
@@ -51,6 +51,7 @@ and exp' =
   | UnwrapE of var * typ
   | UnrollE of var * typ
   | RecE of var * typ * exp
+  | WithEnvE of (Env.env -> exp)
 
 and bind = (bind', unit) phrase
 and bind' =
@@ -315,6 +316,143 @@ let rollP(p, t2) =
     Some (AsT(t2, PathT(RecE("_"@@t1.at, TypT@@t1.at,
       TypE(t1.it@@p.at)@@p.at)@@p.at)@@p.at)@@span[p.at; t2.at])
 
+(* data *)
+
+let toEP p =
+  let b, t = (defaultP p).it in
+  (b, t, Expl@@p.at)@@p.at
+
+let absTC = function
+  | [] -> TypT
+  | ({at} :: _) as tps ->
+     funT(List.map (function
+              | {it = ({it = VarB(_, _); at = atH}, t, i); at} ->
+                 (EmptyB@@atH, t, i)@@at
+              | unnamed -> unnamed) tps,
+          TypT@@at,
+          Pure@@at)
+
+let toCP v tps =
+  let at = v.at in
+  annotP(varP(v)@@at, absTC(tps)@@at)@@at
+
+let appPs f xs =
+  List.fold_left (fun f tp ->
+      match tp with
+      | {it = ({it = VarB(v, _)}, _, _); at} -> appE(f, VarE(v)@@at)@@at
+      | _ -> assert false) f xs
+
+let appTPs tc tps =
+  PathT (appPs tc tps)
+
+let toImpl = function
+  | {it = (b, ({it = TypT} as t), i); at} -> (b, t, Impl@@i.at)@@at
+  | other -> other
+
+let seqD = function
+  | [] -> EmptyD
+  | d::ds -> (List.fold_left (fun s d -> SeqD(s, d)@@d.at) d ds).it
+
+let seqB = function
+  | [] -> EmptyB
+  | b::bs -> (List.fold_left (fun s b -> SeqB(s, b)@@b.at) b bs).it
+
+let dataE(case_v, small_v, tps, cases, at) =
+  let ntps, utps, tps =
+    tps |> List.fold_left (fun (ntps, utps, tps) ->
+               function
+                 | {it = ({it = EmptyB; at = atH}, t, i); at} ->
+                   let unnamed = let b, _ = varP(var "_"@@atH) in (b, t, i)@@at in
+                   (ntps, utps @ [unnamed], tps @ [unnamed])
+                 | named ->
+                   (ntps @ [named], utps, tps @ [named]))
+             ([], [], []) in
+  let case_tp = toEP (toCP case_v utps) in
+  let small_p = toCP small_v tps in
+  let small_tp = toEP small_p in
+  let impure_v = "I$"@@at in
+  let impure_c = funE(case_tp::small_tp::ntps, TypE(cases)@@at)@@at in
+  let impure_t = appTPs (VarE(impure_v)@@at) (case_tp::small_tp::ntps)@@at in
+  let ex_v = "J$"@@at in
+  let ex_c =
+    funE(small_tp::ntps,
+         TypE(StrT(seqD [VarD(case_v, funT(utps, TypT@@at, Pure@@at)@@at)@@at;
+                         InclD(impure_t)@@at] @@at)@@at)@@at)@@at in
+  let ex_t = appTPs (VarE(ex_v)@@at) (small_tp::ntps)@@at in
+  let big_v = "T$"@@at in
+  let big_c =
+    let c_v = "c$"@@at in
+    funE(small_tp::tps,
+         TypE(funT([let b, _ = varP(c_v) in (b, ex_t, Expl@@at)@@at],
+                   appTPs (DotE(VarE(c_v)@@at, case_v)@@at) utps@@at,
+                   Impure@@at)@@at)@@at)@@at in
+  let big_t = appTPs (VarE(big_v)@@at) (small_tp::tps)@@at in
+  let small_c = recE(defaultTP small_p, funE(tps, TypE(WrapT(big_t)@@at)@@at)@@at)@@at in
+  let small_t = appTPs (VarE(small_v)@@at) tps@@at in
+  let cs_v = "cs$"@@at in
+  let cs_p = toEP (annotP(varP(cs_v)@@at, impure_t)@@at) in
+  let e_v = "e$"@@at in
+  let e_p = toEP (annotP(varP(e_v)@@at, small_t)@@at) in
+  let case_e =
+    funE(List.map toImpl (case_tp::tps) @ [cs_p; e_p],
+         appE(unwrapE(unrollE(VarE(e_v)@@at, small_t)@@at, WrapT(big_t)@@at)@@at,
+              StrE(SeqB(VarB(case_v, VarE(case_v)@@at)@@at,
+                        InclB(VarE(cs_v)@@at)@@at)@@at)@@at)@@at)@@at in
+  let mk_v = "mk$"@@at in
+  let c_v = "c$"@@at in
+  let c_p = toEP (annotP(varP(c_v)@@at, big_t)@@at) in
+  let mk_e =
+    funE(List.map toImpl tps @ [c_p],
+         rollE(wrapE(VarE(c_v)@@at, WrapT(big_t)@@at)@@at, small_t)@@at)@@at in
+  let d_v = "D$"@@at in
+  let d_e = funE(ntps, appPs (VarE(ex_v)@@at) (small_tp::ntps))@@at in
+  let seal_e =
+    StrT(seqD [VarD(small_v, absTC(tps)@@at)@@at;
+               VarD(case_v,
+                    funT(List.map toImpl (case_tp::tps) @ [cs_p],
+                         funT([e_p],
+                              appTPs (VarE(case_v)@@at) utps @@at,
+                              Impure@@at)@@at,
+                         Pure@@at)@@at)@@at;
+               VarD(mk_v, funT(List.map toImpl tps @ [c_p], small_t, Pure@@at)@@at)@@at;
+               VarD(d_v, funT(ntps, EqT(TypE(ex_t)@@at)@@at, Pure@@at)@@at)@@at] @@at)@@at in
+  letE(
+      InclB(
+          letE(seqB [VarB(impure_v, impure_c)@@at;
+                     VarB(ex_v, ex_c)@@at;
+                     VarB(big_v, big_c)@@at] @@at,
+               sealE(StrE(seqB [VarB(small_v, small_c)@@at;
+                                VarB(case_v, case_e)@@at;
+                                VarB(mk_v, mk_e)@@at;
+                                VarB(d_v, d_e)@@at]@@at)@@at,
+                     seal_e)@@at)@@at)@@at,
+      WithEnvE(fun env ->
+          let rec find_cases = function
+            | Types.TypT(Types.ExT(_, t)) -> find_cases t
+            | Types.FunT(_, _, Types.ExT(_, t), _) -> find_cases t
+            | Types.StrT(_::cases) -> cases
+            | _ -> failwith "bug" in
+          let cases = find_cases (Env.lookup_val d_v.it env) in
+          let cons =
+            cases
+            |> List.map (fun (label, ts) ->
+                   let rec initPs = function
+                     | Types.FunT (_, _, Types.ExT (_, ts), e) ->
+                        (match e with
+                         | Types.Implicit -> initPs ts
+                         | Types.Explicit _ ->
+                           toEP (varP(var "v$"@@at)@@at) :: initPs ts)
+                     | _ -> [] in
+                   let ps = initPs ts in
+                   let r_v = "r$"@@at in
+                   VarB(label@@at,
+                        funE(List.map toImpl ntps @ ps,
+                             appE(VarE(mk_v)@@at,
+                                  funE([toEP (annotP(varP(r_v)@@at, appTPs (VarE(d_v)@@at) ntps@@at)@@at)],
+                                       appPs (DotE(VarE(r_v)@@at, label@@at)@@at) ps)@@at)@@at)@@at)@@at) in
+          StrE(seqB ((VarB(small_v, VarE(small_v)@@at)@@at) ::
+                     (VarB(case_v, VarE(case_v)@@at)@@at) :: cons)@@at)@@at)@@at)
+
 
 (* String conversion *)
 
@@ -367,6 +505,7 @@ let label_of_exp e =
   | UnwrapE _ -> "UnwrapE"
   | UnrollE _ -> "UnrollE"
   | RecE _ -> "RecE"
+  | WithEnvE _ -> "WithEnvE"
 
 let label_of_bind b =
   match b.it with
@@ -425,6 +564,7 @@ and string_of_exp e =
   | UnwrapE(x, t) -> node' [string_of_var x; string_of_typ t]
   | UnrollE(x, t) -> node' [string_of_var x; string_of_typ t]
   | RecE(x, t, e) -> node' [string_of_var x; string_of_typ t; string_of_exp e]
+  | WithEnvE(_) -> node' ["<fun>"]
 
 and string_of_bind b =
   let node' = node (label_of_bind b) in