diff --git a/Makefile b/Makefile
index fea2dc6f..2d333780 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 import elab \
+  lib source prim fomega types env syntax \
+  parser lexer iL erase trace sub import elab \
   lambda compile \
   main
 NOMLI = syntax iL main import
diff --git a/elab.ml b/elab.ml
index 474d39e9..af629af8 100644
--- a/elab.ml
+++ b/elab.ml
@@ -601,6 +601,7 @@ 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.ImportE(path) ->
     (match Import.resolve (Source.at_file path) path.it with
     | None -> Source.error path.at ("\""^path.it^"\" does not resolve to a file")
@@ -614,6 +615,9 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
       appE(FunE(x'@@t.at, t, VarE(x'@@t.at)@@t.at, Expl@@t.at)@@span[e.at; t.at], e)@@exp.at in
     elab_exp env exp l
 
+  | 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)}
 s1 = ?Xt:*->*, Xu:*->*->*. !b:*. [= b] -> {t : [= Xt b], u : !a:*. [= a] => [= Xu b a]}
diff --git a/examples/fc.1ml b/examples/fc.1ml
index a1bb894e..39e49267 100644
--- a/examples/fc.1ml
+++ b/examples/fc.1ml
@@ -9,26 +9,14 @@ local import "prelude"
 ;; clarity.
 
 GADTs = {
-  Exp = {
-    local
-      type I (type t _) = {
-        type case _
-        Zero       :               case int
-        Succ       :      t int ~> case int
-        Pair 'a 'b : t a ~> t b ~> case (a, b)
-      }
-      ...rec {type t _} => {type t a = wrap (m: I t) ~> m.case a}
-      I = I t
-    t
-    case (m: I) (e: t _) = e m
-    Zero     : t _ = fun (m: I) => m.Zero
-    Succ x   : t _ = fun (m: I) => m.Succ x
-    Pair l r : t _ = fun (m: I) => m.Pair l r
+  Exp = data case t _ :> {
+    Zero       :               case int
+    Succ       :      t int ~> case int
+    Pair 'a 'b : t a ~> t b ~> case (a, b)
   }
 
   eval = rec (eval 'a: Exp.t a ~> a) =>
-    Exp.case {
-      type case x = x
+    Exp.case (type fun x => x) {
       Zero = 0
       Succ x = eval x + 1
       Pair l r = (eval l, eval r)
diff --git a/examples/hoas.1ml b/examples/hoas.1ml
index a958a343..f398e77b 100644
--- a/examples/hoas.1ml
+++ b/examples/hoas.1ml
@@ -5,35 +5,13 @@ local import "prelude"
 ;;
 ;;   https://github.com/palladin/idris-snippets/blob/master/src/HOAS.idr
 
-let
-  type I (type case _) (type t _) = {
-    Val 'x       :                           x ~> case x
-    Bin 'x 'y 'z : (x ~> y ~> z) ~> t x ~> t y ~> case z
-    If  'x       :      t Bool.t ~> t x ~> t x ~> case x
-    App 'x 'y    :           t (x ~> y) ~> t x ~> case y
-    Lam 'x 'y    :                (t x ~> t y) ~> case (x ~> y)
-    Fix 'x 'y    :      t ((x ~> y) ~> x ~> y) ~> case (x ~> y)
-  }
-  type J (type t _) = {type case _, ...I case t}
-  type T (type t _) x = (c: J t) ~> c.case x
-  ...{
-    ...rec {type t _} => {type t x = wrap T t x}
-    case 'x (type case _) (cs: I case t) (e: t _) = e {case, ...cs}
-    mk (fn: T t _) = fn
-  } :> {
-    type t _
-    case 'x: (type case _) -> I case t -> t x ~> case x
-    mk 'x: T t x -> t x
-  }
-  J = J t
-in {
-  t, case
-  Val 'x                                   (v: x) = mk fun (e: J) => e.Val v
-  Bin 'x 'y 'z (f: x ~> y ~> z) (l: t x) (r: t y) = mk fun (e: J) => e.Bin f l r
-  If  'x          (b: t Bool.t) (c: t x) (a: t x) = mk fun (e: J) => e.If b c a
-  App 'x 'y              (f: t (x ~> y)) (a: t x) = mk fun (e: J) => e.App f a
-  Lam 'x 'y                       (f: t x ~> t y) = mk fun (e: J) => e.Lam f
-  Fix 'x 'y           (f: t ((x ~> y) ~> x ~> y)) = mk fun (e: J) => e.Fix f
+data case t _ :> {
+  Val 'x       :                           x ~> case x
+  Bin 'x 'y 'z : (x ~> y ~> z) ~> t x ~> t y ~> case z
+  If  'x       :      t Bool.t ~> t x ~> t x ~> case x
+  App 'x 'y    :           t (x ~> y) ~> t x ~> case y
+  Lam 'x 'y    :                (t x ~> t y) ~> case (x ~> y)
+  Fix 'x 'y    :      t ((x ~> y) ~> x ~> y) ~> case (x ~> y)
 }
 
 Fact = Fix <| Lam fun f => Lam fun x =>
diff --git a/examples/tiv.1ml b/examples/tiv.1ml
new file mode 100644
index 00000000..d22382fa
--- /dev/null
+++ b/examples/tiv.1ml
@@ -0,0 +1,116 @@
+local import "prelude"
+
+;; As 1ML is powerful enough to encode GADTs we can define a value independent
+;; type representation or a deep embedding of type constructors.
+
+type iso a b = {to: a ~> b, from: b ~> a}
+
+Rep = {
+  data case t _ :> {
+    bool: case bool
+    char: case char
+    int : case int
+    text: case text
+    unit: case unit
+
+    alt   'x 'y: t x ~> t y ~> case (alt x y)
+    (~~>) 'x 'y: t x ~> t y ~> case (x ~> y)
+    pair  'x 'y: t x ~> t y ~> case (x, y)
+
+    iso 'x 'y: iso x y ~> t y ~> case x
+
+    lazy 'x: ({} ~> t x) ~> case x
+  }
+
+  defaults (type t _) (default 'a: t a) = {
+    bool = default
+    char = default
+    int  = default
+    unit = default
+    text = default
+
+    alt   _ _ = default
+    _ ~~> _   = default
+    pair  _ _ = default
+
+    iso _ _ = default
+
+    lazy _ = default
+  }
+
+  local i = {to = Opt.case {none = inl {}, some = inr}
+             from = Alt.case {inl {} = none, inr = some}}
+  opt a = iso i (alt unit a)
+
+  local i = {to = List.case {nil = inl {}, x :: xs = inr (x, xs)}
+             from = Alt.case {inl {} = nil, inr (x, xs) = x::xs}}
+  list v = rec vs => lazy fun {} => iso i (alt unit (pair v vs))
+}
+
+;; Generic toText
+
+ToText = {type t x = x ~> text}
+
+toText = rec (toText 'x: Rep.t x ~> ToText.t x) => Rep.case ToText.t {
+  bool = Bool.toText
+  char c =  "'" ++ Text.fromChar c ++ "'"
+  int = Int.toText
+  text t = "\"" ++ t ++ "\""
+  unit {} = "{}"
+
+  alt aT bT = Alt.case {
+    inl a = "(inl " ++ toText aT a ++ ")"
+    inr b = "(inr " ++ toText bT b ++ ")"
+  }
+
+  (_ ~~> _) _ = "<fun>"
+
+  pair aT bT (a, b) = "(" ++ toText aT a ++ ", " ++ toText bT b ++ ")"
+
+  iso ab bT = ab.to >> toText bT
+
+  lazy th = toText (th {})
+}
+
+println rep x = print (toText rep x ++ "\n")
+
+do let ...Rep
+   println int 101
+   println (pair bool text) (true, "that")
+   println (opt bool) (some false)
+   println (iso {to i = i <> 0, from b = if b then 1 else 0} bool) 1
+   println (list int) (3 :: (1 :: (4 :: nil)))
+
+;; Generic eq
+
+Eq = {type t x = x ~> x ~> bool}
+
+eq = rec (eq 'x: Rep.t x ~> Eq.t x) => Rep.case Eq.t {
+  bool = Bool.==
+  char = Char.==
+  int = Int.==
+  text = Text.==
+  unit _ _ = true
+
+  alt aT bT l r = l |> Alt.case {
+    inl l = r |> Alt.case {inl = eq aT l, inr _ = false}
+    inr l = r |> Alt.case {inl _ = false, inr = eq bT l}
+  }
+
+  (_ ~~> _) _ _ = false
+
+  pair aT bT (l1, l2) (r1, r2) = eq aT l1 r1 && eq bT l2 r2
+
+  iso ab bT l r = eq bT (ab.to l) (ab.to r)
+
+  lazy th l r = eq (th {}) l r
+}
+
+do let ...Rep
+       test t l r = print ("eq " ++ toText t l ++
+                             " " ++ toText t r ++
+                           " = " ++ toText bool (eq t l r) ++ "\n")
+   test int 101 42
+   test (pair int bool) (1, true) (1, true)
+   test (list int) (3 :: (1 :: nil)) (4 :: (1 :: nil))
+   test (list int) (4 :: (2 :: nil)) (4 :: (2 :: nil))
diff --git a/examples/trie.1ml b/examples/trie.1ml
index c1173329..ff64b907 100644
--- a/examples/trie.1ml
+++ b/examples/trie.1ml
@@ -1,25 +1,14 @@
 local import "prelude"
 
 FunctionalTrie = {
-  local
-    type I (type t _ _) = {
-      type case _ _
-      unit 'v         : opt v            ~> case {} v
-      alt  'v 'k1 'k2 : t k1 v ~> t k2 v ~> case (alt k1 k2) v
-      pair 'v 'k1 'k2 : t k1 (t k2 v)    ~> case (k1, k2) v
-    }
-    ...rec {type t _ _} => {type t k v = wrap (m: I t) ~> m.case k v}
-    I = I t
-
-  t
-  case (m: I) (e: t _ _) = e m
-  unit vO : t _ _ = fun (m: I) => m.unit vO
-  alt l r : t _ _ = fun (m: I) => m.alt l r
-  pair lr : t _ _ = fun (m: I) => m.pair lr
+  data case t _ _ :> {
+    unit 'v         : opt v            ~> case {} v
+    alt  'v 'k1 'k2 : t k1 v ~> t k2 v ~> case (alt k1 k2) v
+    pair 'v 'k1 'k2 : t k1 (t k2 v)    ~> case (k1, k2) v
+  }
 
   lookup = rec (lookup 'k 'v: t k v ~> k ~> opt v) =>
-    case {
-      type case k v = k ~> opt v
+    case (type fun k v => k ~> opt v) {
       unit m {} = m
       alt ta tb = Alt.case {inl = lookup ta, inr = lookup tb}
       pair ta (a, b) = lookup ta a |> Opt.case {none, some tb = lookup tb b}
diff --git a/lexer.mll b/lexer.mll
index db5024de..8d21eae7 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -263,6 +263,7 @@ rule token = parse
   | "_" { HOLE }
   | "&&" { LOGICAL_AND }
   | "as" { AS }
+  | "data" { DATA }
   | "do" { DO }
   | "else" { ELSE }
   | "type_error" { TYPE_ERROR }
diff --git a/parser.mly b/parser.mly
index 6489e214..635f8cb8 100644
--- a/parser.mly
+++ b/parser.mly
@@ -39,6 +39,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %token IMPORT
 %token WRAP_OP UNWRAP_OP
 %token ROLL_OP UNROLL_OP
+%token DATA
 
 %token EOF
 
@@ -373,6 +374,8 @@ annexp :
     { $2($1, $3)@@at() }
 ;
 exp :
+  | DATA name name typparamlist annexp_op typ
+    { dataE($2, $3, $4, $5, $6, at())@@at() }
   | LET bind IN exp
     { letE($2, $4)@@at() }
   | IF exp THEN exp ELSE exp
@@ -453,6 +456,8 @@ atbind :
     { InclB(letE($2, $4)@@at())@@at() }
   | IMPORT TEXT
     { InclB(ImportE($2@@ati 2)@@at())@@at() }
+  | DATA name name typparamlist annexp_op typ
+    { InclB(dataE($2, $3, $4, $5, $6, at())@@at())@@at() }
 /*
   | LPAR bind RPAR
     { $2 }
diff --git a/prelude/index.1mls b/prelude/index.1mls
index 2ebae144..4597e697 100644
--- a/prelude/index.1mls
+++ b/prelude/index.1mls
@@ -100,6 +100,10 @@ Text: {
   print: t ~> {}
 }
 
+Unit: {
+  type t = {}
+}
+
 Zero: {
   type t
 }
@@ -111,6 +115,7 @@ type int = Int.t
 type list a = List.t a
 type opt a = Opt.t a
 type text = Text.t
+type unit = Unit.t
 type zero = Zero.t
 
 (%): int -> int -> int
diff --git a/regression.1ml b/regression.1ml
index 795653f2..9dcb8fc7 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -309,6 +309,112 @@ PolyRec = {
   t0 = inr (inl (0, 0) : t (int, int)) : t int
 }
 
+;;
+
+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
+  ...{
+    ...rec {type t _} => {type t x = wrap T t x}
+    case 'x (type case _) (cs: I t case) (e: t _) =
+      e {case, ...cs}
+    mk 'x (c: T t x) = c
+  } :> {
+    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 {
+    ...rec {type t _} => {type t x = wrap T t x}
+    case '(type case) 'x 'n (cs: I case t x) (e: t x) =
+      e {case, ...cs}
+    mk 'x (c: T t x) = c
+    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 _
@@ -346,3 +452,36 @@ ListN = {
       x :: xs = xy x :: map xs
     }
 }
+
+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 {
+  ...rec {type t _ _} => {type t x n = wrap T t x n}
+  case (type case _) 'x 'n (cs: I case t x) (e: t x n) =
+    e {case, ...cs}
+  mk 'x 'n (c: T t x n) = c
+  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' = {
+  data case t x _ :> {
+    nil     :               case N.Z
+    (::) 'n : x ~> t x n ~> case (N.S n)
+  }
+
+  map 'x 'y 'n (xy: x -> y) = rec (map 'n: t x n ~> t y n) =>
+    case (t y) {
+      nil
+      x :: xs = xy x :: map xs
+    }
+}
diff --git a/syntax.ml b/syntax.ml
index 80b64e27..2968b555 100644
--- a/syntax.ml
+++ b/syntax.ml
@@ -54,6 +54,7 @@ and exp' =
   | RecE of var * typ * exp
   | ImportE of path
   | AnnotE of exp * typ
+  | WithEnvE of (Env.env -> exp)
 
 and bind = (bind', unit) phrase
 and bind' =
@@ -334,6 +335,143 @@ let rollP(p, t2) =
    infer = None;
    annot = Some t2}
 
+(* 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 seqDs = function
+  | [] -> EmptyD
+  | d::ds -> (List.fold_left (fun s d -> seqD(s, d)@@d.at) d ds).it
+
+let seqBs = 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, ascribeE, 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 p = varP(var "_"@@atH) in (p.bind, 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(seqDs[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 p = varP(c_v) in (p.bind, 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(seqDs[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(seqBs[VarB(impure_v, impure_c)@@at;
+                     VarB(ex_v, ex_c)@@at;
+                     VarB(big_v, big_c)@@at] @@at,
+               ascribeE(StrE(seqBs[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(seqBs((VarB(small_v, VarE(small_v)@@at)@@at) ::
+                     (VarB(case_v, VarE(case_v)@@at)@@at) :: cons)@@at)@@at)@@at)
+
 
 (* String conversion *)
 
@@ -388,6 +526,7 @@ let label_of_exp e =
   | RecE _ -> "RecE"
   | ImportE _ -> "ImportE"
   | AnnotE _ -> "AnnotE"
+  | WithEnvE _ -> "WithEnvE"
 
 let label_of_bind b =
   match b.it with
@@ -448,6 +587,7 @@ and string_of_exp e =
   | RecE(x, t, e) -> node' [string_of_var x; string_of_typ t; string_of_exp e]
   | ImportE(p) -> node' ["\"" ^ String.escaped p.it ^ "\""]
   | AnnotE(e, t) -> node' [string_of_exp e; string_of_typ t]
+  | WithEnvE(_) -> node' ["<fun>"]
 
 and string_of_bind b =
   let node' = node (label_of_bind b) in
@@ -497,6 +637,7 @@ and imports_exp exp =
   | RecE(_, typ, exp) -> imports_typ typ @ imports_exp exp
   | ImportE path -> [path]
   | AnnotE(exp, typ) -> imports_exp exp @ imports_typ typ
+  | WithEnvE(fn) -> []
 
 and imports_bind bind =
   match bind.it with