Some serious bug-fix work to get HTML example to compile; this includes fixing a bug with 'val' patterns in Unnest and the need for more local reduction in Especialize

15 files changed, 295 insertions, 49 deletions

diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index 19983cd2..f2dffd38 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -79,7 +79,7 @@ val strsub : string -> int -> char
 val strsuffix : string -> int -> string
 val strchr : string -> char -> option string
 val strindex : string -> char -> option int
-val strcspn : string -> string -> option int
+val strcspn : string -> string -> int
 val substring : string -> int -> int -> string
 val str1 : char -> string
 
diff --git a/lib/ur/string.ur b/lib/ur/string.ur
index f19ce174..f7781e01 100644
--- a/lib/ur/string.ur
+++ b/lib/ur/string.ur
@@ -11,7 +11,15 @@ val suffix = Basis.strsuffix
 val index = Basis.strindex
 val atFirst = Basis.strchr
 
-fun mindex {Haystack = s, Needle = chs} = Basis.strcspn s chs
+fun mindex {Haystack = s, Needle = chs} =
+    let
+        val n = Basis.strcspn s chs
+    in
+        if n >= length s then
+            None
+        else
+            Some n
+    end
 
 fun substring s {Start = start, Len = len} = Basis.substring s start len
 
diff --git a/src/compiler.sig b/src/compiler.sig
index 16207e8b..7e3e8ffc 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -129,10 +129,14 @@ signature COMPILER = sig
     val toTag : (string, Core.file) transform
     val toReduce : (string, Core.file) transform
     val toShakey : (string, Core.file) transform
-    val toUnpoly : (string, Core.file) transform 
-    val toSpecialize : (string, Core.file) transform 
+    val toUnpoly : (string, Core.file) transform
+    val toSpecialize : (string, Core.file) transform
     val toShake4 : (string, Core.file) transform
-    val toEspecialize2 : (string, Core.file) transform 
+    val toEspecialize2 : (string, Core.file) transform
+    val toShake4' : (string, Core.file) transform
+    val toUnpoly2 : (string, Core.file) transform
+    val toShake4'' : (string, Core.file) transform
+    val toEspecialize3 : (string, Core.file) transform
     val toReduce2 : (string, Core.file) transform
     val toShake5 : (string, Core.file) transform
     val toMarshalcheck : (string, Core.file) transform
diff --git a/src/compiler.sml b/src/compiler.sml
index 1d15367f..dcc1e5b3 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -1013,8 +1013,12 @@ val toSpecialize = transform specialize "specialize" o toUnpoly
 val toShake4 = transform shake "shake4" o toSpecialize
 
 val toEspecialize2 = transform especialize "especialize2" o toShake4
+val toShake4' = transform shake "shake4'" o toEspecialize2
+val toUnpoly2 = transform unpoly "unpoly2" o toShake4'
+val toShake4'' = transform shake "shake4'" o toUnpoly2
+val toEspecialize3 = transform especialize "especialize3" o toShake4''
 
-val toReduce2 = transform reduce "reduce2" o toEspecialize2
+val toReduce2 = transform reduce "reduce2" o toEspecialize3
 
 val toShake5 = transform shake "shake5" o toReduce2
 
diff --git a/src/core_print.sml b/src/core_print.sml
index fd0556e6..f18ea4b9 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -233,12 +233,19 @@ fun p_pat' par env (p, _) =
                                                     p_pat' true env p])
       | PRecord xps =>
         box [string "{",
-             p_list_sep (box [string ",", space]) (fn (x, p, _) =>
+             p_list_sep (box [string ",", space]) (fn (x, p, t) =>
                                                       box [string x,
                                                            space,
                                                            string "=",
                                                            space,
-                                                           p_pat env p]) xps,
+                                                           p_pat env p,
+                                                           if !debug then
+                                                               box [space,
+                                                                    string ":",
+                                                                    space,
+                                                                    p_con env t]
+                                                           else
+                                                               box []]) xps,
              string "}"]
 
 and p_pat x = p_pat' false x
diff --git a/src/elab_env.sig b/src/elab_env.sig
index a5b8751a..769fea58 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -118,6 +118,7 @@ signature ELAB_ENV = sig
     val chaseMpath : env -> (int * string list) -> Elab.str * Elab.sgn
 
     val patBinds : env -> Elab.pat -> env
+    val patBindsN : Elab.pat -> int
 
     exception Bad of Elab.con * Elab.con
 
diff --git a/src/elab_env.sml b/src/elab_env.sml
index dd050c9e..bb34c345 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1512,6 +1512,15 @@ fun patBinds env (p, loc) =
       | PCon (_, _, _, SOME p) => patBinds env p
       | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps
 
+fun patBindsN (p, _) =
+    case p of
+        PWild => 0
+      | PVar _ => 1
+      | PPrim _ => 0
+      | PCon (_, _, _, NONE) => 0
+      | PCon (_, _, _, SOME p) => patBindsN p
+      | PRecord xps => foldl (fn ((_, p, _), n) => patBindsN p + n) 0 xps
+
 fun edeclBinds env (d, loc) =
     case d of
         EDVal (p, _, _) => patBinds env p
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 86448659..42a0a107 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -252,12 +252,19 @@ fun p_pat' par env (p, _) =
                                                   p_pat' true env p])
       | PRecord xps =>
         box [string "{",
-             p_list_sep (box [string ",", space]) (fn (x, p, _) =>
+             p_list_sep (box [string ",", space]) (fn (x, p, t) =>
                                                       box [string x,
                                                            space,
                                                            string "=",
                                                            space,
-                                                           p_pat env p]) xps,
+                                                           p_pat env p,
+                                                           if !debug then
+                                                               box [space,
+                                                                    string ":",
+                                                                    space,
+                                                                    p_con env t]
+                                                           else
+                                                               box []]) xps,
              string "}"]
 
 and p_pat x = p_pat' false x
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 8345e3f3..ec6c51ba 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -429,8 +429,10 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                                                                     | PRecord xps => foldl (fn ((_, p, _), ctx) =>
                                                                                                pb (p, ctx)) ctx xps
                                                           in
-                                                              S.map2 (mfe (pb (p, ctx)) e,
-                                                                   fn e' => (p, e'))
+                                                              S.bind2 (mfp ctx p,
+                                                                       fn p' =>
+                                                                          S.map2 (mfe (pb (p', ctx)) e,
+                                                                               fn e' => (p', e')))
                                                           end) pes,
                                     fn pes' =>
                                        S.bind2 (mfc ctx disc,
@@ -482,6 +484,32 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                                    fn k' =>
                                       (EKApp (e', k'), loc)))
 
+        and mfp ctx (pAll as (p, loc)) =
+            case p of
+                PWild => S.return2 pAll
+              | PVar (x, t) =>
+                S.map2 (mfc ctx t,
+                        fn t' =>
+                           (PVar (x, t'), loc))
+              | PPrim _ => S.return2 pAll
+              | PCon (dk, pc, args, po) =>
+                S.bind2 (ListUtil.mapfold (mfc ctx) args,
+                      fn args' =>
+                         S.map2 ((case po of
+                                      NONE => S.return2 NONE
+                                    | SOME p => S.map2 (mfp ctx p, SOME)),
+                              fn po' =>
+                                 (PCon (dk, pc, args', po'), loc)))
+              | PRecord xps =>
+                S.map2 (ListUtil.mapfold (fn (x, p, c) =>
+                                              S.bind2 (mfp ctx p,
+                                                       fn p' =>
+                                                          S.map2 (mfc ctx c,
+                                                                  fn c' =>
+                                                                     (x, p', c')))) xps,
+                         fn xps' =>
+                            (PRecord xps', loc))
+
         and mfed ctx (dAll as (d, loc)) =
             case d of
                 EDVal (p, t, e) =>
diff --git a/src/especialize.sml b/src/especialize.sml
index 7d129b8b..3fa3ea1d 100644
--- a/src/especialize.sml
+++ b/src/especialize.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2009, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -278,7 +278,7 @@ fun specialize' (funcs, specialized) file =
                     NONE => default ()
                   | SOME (f, xs) =>
                     case IM.find (#funcs st, f) of
-                        NONE => default ()
+                        NONE => ((*print ("No find: " ^ Int.toString f ^ "\n");*) default ())
                       | SOME {name, args, body, typ, tag} =>
                         let
                             val (xs, st) = ListUtil.foldlMap (fn (e, st) => exp (env, e, st)) st xs
@@ -415,6 +415,8 @@ fun specialize' (funcs, specialized) file =
                                                                              (body', typ') fvs
                                                 val mns = !mayNotSpec
                                                 (*val () = mayNotSpec := SS.add (mns, name)*)
+                                                (*val () = print ("NEW: " ^ name ^ "__" ^ Int.toString f' ^ "\n");*)
+                                                val body' = ReduceLocal.reduceExp body'
                                                 (*val () = Print.preface ("PRE", CorePrint.p_exp CoreEnv.empty body')*)
                                                 val (body', st) = exp (env, body', st)
                                                 val () = mayNotSpec := mns
@@ -424,7 +426,6 @@ fun specialize' (funcs, specialized) file =
                                                                   e' fvs
                                                 val e' = foldl (fn (arg, e) => (EApp (e, arg), loc))
                                                                e' xs
-                                                (*val () = print ("NEW: " ^ name ^ "__" ^ Int.toString f' ^ "\n");*)
                                                 (*val () = Print.prefaces "Brand new"
                                                                         [("e'", CorePrint.p_exp CoreEnv.empty e'),
                                                                          ("e", CorePrint.p_exp CoreEnv.empty e),
diff --git a/src/expl_print.sml b/src/expl_print.sml
index 15838729..c953350c 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -234,12 +234,19 @@ fun p_pat' par env (p, _) =
 
       | PRecord xps =>
         box [string "{",
-             p_list_sep (box [string ",", space]) (fn (x, p, _) =>
+             p_list_sep (box [string ",", space]) (fn (x, p, t) =>
                                                       box [string x,
                                                            space,
                                                            string "=",
                                                            space,
-                                                           p_pat env p]) xps,
+                                                           p_pat env p,
+                                                           if !debug then
+                                                               box [space,
+                                                                    string ":",
+                                                                    space,
+                                                                    p_con env t]
+                                                           else
+                                                               box []]) xps,
              string "}"]
 
 and p_pat x = p_pat' false x
diff --git a/src/monoize.sml b/src/monoize.sml
index e2377bae..d43002cb 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -2737,7 +2737,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                      (L.ECApp (
                       (L.ECApp (
                        (L.EFfi ("Basis", "tag"),
-                        _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _),
+                        _), (L.CRecord (_, attrsGiven), _)), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _),
                class), _),
               attrs), _),
              tag), _),
@@ -2768,7 +2768,10 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
                 val (attrs, fm) = monoExp (env, st, fm) attrs
                 val attrs = case #1 attrs of
                                 L'.ERecord xes => xes
-                              | _ => raise Fail "Non-record attributes!"
+                              | _ => map (fn ((L.CName x, _), t) => (x, (L'.EField (attrs, x), loc), monoType env t)
+                                           | (c, t) => (E.errorAt loc "Non-constant field name for HTML tag attribute";
+                                                        Print.eprefaces' [("Name", CorePrint.p_con env c)];
+                                                        ("", (L'.EField (attrs, ""), loc), monoType env t))) attrsGiven
 
                 val attrs =
                     if List.exists (fn ("Link", _, _) => true
diff --git a/src/reduce.sml b/src/reduce.sml
index b2911a5f..963863e8 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -65,6 +65,18 @@ val dangling =
                                         CoreUtil.Exp.RelE _ => n + 1
                                       | _ => n}
 
+val cdangling =
+    CoreUtil.Exp.existsB {kind = fn _ => false,
+                          con = fn (n, c) =>
+                                   case c of
+                                       CRel n' => n' >= n
+                                     | _ => false,
+                          exp = fn _ => false,
+                          bind = fn (n, b) =>
+                                    case b of
+                                        CoreUtil.Exp.RelC _ => n + 1
+                                      | _ => n}
+
 datatype env_item =
          UnknownK
        | KnownK of kind
@@ -86,6 +98,15 @@ val edepth' = foldl (fn (UnknownE, n) => n + 1
                       | (Lift (_, _, n'), n) => n + n'
                       | (_, n) => n) 0
 
+val cdepth = foldl (fn (UnknownC, n) => n + 1
+                     | (KnownC _, n) => n + 1
+                     | (_, n) => n) 0
+
+val cdepth' = foldl (fn (UnknownC, n) => n + 1
+                      | (KnownC _, n) => n + 1
+                      | (Lift (_, n', _), n) => n + n'
+                      | (_, n) => n) 0
+
 type env = env_item list
 
 fun ei2s ei =
@@ -344,6 +365,11 @@ fun kindConAndExp (namedC, namedE) =
                               raise Fail "!")
                          else
                              ()*)
+                (*val () = if cdangling (cdepth env) all then
+                             Print.prefaces "Bad exp" [("e", CorePrint.p_exp CoreEnv.empty all),
+                                                       ("env", Print.PD.string (e2s env))]
+                         else
+                             ()*)
 
                 val r = case e of
                             EPrim _ => all
@@ -636,6 +662,12 @@ fun kindConAndExp (namedC, namedE) =
                      raise Fail "!!")
                 else
                     ();*)
+                (*if cdangling (cdepth' (deKnown env)) r then
+                    (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
+                                           ("r", CorePrint.p_exp CoreEnv.empty r)];
+                     raise Fail "!!")
+                else
+                    ();*)
                 r
             end
     in
diff --git a/src/reduce_local.sml b/src/reduce_local.sml
index 4c5ab52e..43317b9e 100644
--- a/src/reduce_local.sml
+++ b/src/reduce_local.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -43,11 +43,15 @@ datatype env_item =
          Unknown
        | Known of exp
 
-       | Lift of int
+       | UnknownC
+       | KnownC of con
+
+       | Lift of int * int
 
 type env = env_item list
 
 val deKnown = List.filter (fn Known _ => false
+                            | KnownC _ => false
                             | _ => true)
 
 datatype result = Yes of env | No | Maybe
@@ -120,39 +124,140 @@ fun match (env, p : pat, e : exp) =
         match (env, p, e)
     end
 
+fun con env (all as (c, loc)) =
+    ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*)
+     case c of
+         TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
+       | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc)
+       | TKFun (x, c2) => (TKFun (x, con env c2), loc)
+       | TRecord c => (TRecord (con env c), loc)
+
+       | CRel n =>
+         let
+             fun find (n', env, nudge, liftC) =
+                 case env of
+                     [] => raise Fail "Reduce.con: CRel"
+                   | Unknown :: rest => find (n', rest, nudge, liftC)
+                   | Known _ :: rest => find (n', rest, nudge, liftC)
+                   | Lift (liftC', _) :: rest => find (n', rest, nudge + liftC',
+                                                               liftC + liftC')
+                   | UnknownC :: rest =>
+                     if n' = 0 then
+                         (CRel (n + nudge), loc)
+                     else
+                         find (n' - 1, rest, nudge, liftC + 1)
+                   | KnownC c :: rest =>
+                     if n' = 0 then
+                         con (Lift (liftC, 0) :: rest) c
+                     else
+                         find (n' - 1, rest, nudge - 1, liftC)
+         in
+             (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
+             find (n, env, 0, 0)
+         end
+       | CNamed _ => all
+       | CFfi _ => all
+       | CApp (c1, c2) =>
+         let
+             val c1 = con env c1
+             val c2 = con env c2
+         in
+             case #1 c1 of
+                 CAbs (_, _, b) =>
+                 con (KnownC c2 :: deKnown env) b
+
+               | CApp ((CMap (dom, ran), _), f) =>
+                 (case #1 c2 of
+                      CRecord (_, []) => (CRecord (ran, []), loc)
+                    | CRecord (_, (x, c) :: rest) =>
+                      con (deKnown env)
+                          (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
+                                    (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc)
+                    | _ => (CApp (c1, c2), loc))                           
+
+               | _ => (CApp (c1, c2), loc)
+         end
+       | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc)
+
+       | CKApp (c1, k) =>
+         let
+             val c1 = con env c1
+         in
+             case #1 c1 of
+                 CKAbs (_, b) =>
+                 con (deKnown env) b
+
+               | _ => (CKApp (c1, k), loc)
+         end
+       | CKAbs (x, b) => (CKAbs (x, con env b), loc)
+
+       | CName _ => all
+
+       | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
+       | CConcat (c1, c2) =>
+         let
+             val c1 = con env c1
+             val c2 = con env c2
+         in
+             case (#1 c1, #1 c2) of
+                 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
+                 (CRecord (k, xcs1 @ xcs2), loc)
+               | (CRecord (_, []), _) => c2
+               | (_, CRecord (_, [])) => c1
+               | _ => (CConcat (c1, c2), loc)
+         end
+       | CMap _ => all
+
+       | CUnit => all
+
+       | CTuple cs => (CTuple (map (con env) cs), loc)
+       | CProj (c, n) =>
+         let
+             val c = con env c
+         in
+             case #1 c of
+                 CTuple cs => List.nth (cs, n - 1)
+               | _ => (CProj (c, n), loc)
+         end)
+
+fun patCon pc =
+    case pc of
+        PConVar _ => pc
+      | PConFfi {mod = m, datatyp, params, con = c, arg, kind} =>
+        PConFfi {mod = m, datatyp = datatyp, params = params, con = c,
+                 arg = Option.map (con (map (fn _ => UnknownC) params)) arg,
+                 kind = kind}
+
 fun exp env (all as (e, loc)) =
     case e of
         EPrim _ => all
       | ERel n =>
         let
-            fun find (n', env, nudge, lift) =
+            fun find (n', env, nudge, liftC, liftE) =
                 case env of
                     [] => (ERel (n + nudge), loc)
-                  | Lift lift' :: rest => find (n', rest, nudge + lift', lift + lift')
+                  | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', liftC + liftC', liftE + liftE')
+                  | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE)
+                  | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE)
                   | Unknown :: rest =>
                     if n' = 0 then
                         (ERel (n + nudge), loc)
                     else
-                        find (n' - 1, rest, nudge, lift + 1)
+                        find (n' - 1, rest, nudge, liftC, liftE + 1)
                   | Known e :: rest =>
                     if n' = 0 then
                         ((*print "SUBSTITUTING\n";*)
-                         exp (Lift lift :: rest) e)
+                         exp (Lift (liftC, liftE) :: rest) e)
                     else
-                        find (n' - 1, rest, nudge - 1, lift)
+                        find (n' - 1, rest, nudge - 1, liftC, liftE)
         in
-            find (n, env, 0, 0)
+            find (n, env, 0, 0, 0)
         end
       | ENamed _ => all
-      | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc)
+      | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, map (con env) cs, Option.map (exp env) eo), loc)
       | EFfi _ => all
       | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
 
-      | EApp ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _,
-                                           (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _),
-                      t), _), e) =>
-        (ECon (dk, pc, [t], SOME (exp env e)), loc)
-
       | EApp (e1, e2) =>
         let
             val e1 = exp env e1
@@ -163,21 +268,28 @@ fun exp env (all as (e, loc)) =
               | _ => (EApp (e1, e2), loc)
         end
 
-      | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc)
+      | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (Unknown :: env) e), loc)
 
-      | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) =>
-        (ECon (dk, pc, [t], NONE), loc)
+      | ECApp (e, c) =>
+        let
+            val e = exp env e
+            val c = con env c
+        in
+            case #1 e of
+                ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b
+              | _ => (ECApp (e, c), loc)
+        end
 
-      | ECApp (e, c) => (ECApp (exp env e, c), loc)
-      | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc)
+      | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc)
 
       | EKApp (e, k) => (EKApp (exp env e, k), loc)
       | EKAbs (x, e) => (EKAbs (x, exp env e), loc)
 
-      | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc)
+      | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
       | EField (e, c, others) =>
         let
             val e = exp env e
+            val c = con env c
 
             fun default () = (EField (e, c, others), loc)
         in
@@ -189,12 +301,16 @@ fun exp env (all as (e, loc)) =
               | _ => default ()
         end
 
-      | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc)
-      | ECut (e, c, others) => (ECut (exp env e, c, others), loc)
-      | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc)
+      | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, con env c1, exp env e2, con env c2), loc)
+      | ECut (e, c, {field = f, rest = r}) => (ECut (exp env e,
+                                                     con env c,
+                                                     {field = con env f, rest = con env r}), loc)
+      | ECutMulti (e, c, {rest = r}) => (ECutMulti (exp env e, con env c, {rest = con env r}), loc)
 
-      | ECase (e, pes, others) =>
+      | ECase (e, pes, {disc = d, result = r}) =>
         let
+            val others = {disc = con env d, result = con env r}
+
             fun patBinds (p, _) =
                 case p of
                     PWild => 0
@@ -204,9 +320,18 @@ fun exp env (all as (e, loc)) =
                   | PCon (_, _, _, SOME p) => patBinds p
                   | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
 
+            fun pat (all as (p, loc)) =
+                case p of
+                    PWild => all
+                  | PVar (x, t) => (PVar (x, con env t), loc)
+                  | PPrim _ => all
+                  | PCon (dk, pc, cs, po) =>
+                    (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
+                  | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
+
             fun push () =
                 (ECase (exp env e,
-                        map (fn (p, e) => (p,
+                        map (fn (p, e) => (pat p,
                                            exp (List.tabulate (patBinds p,
                                                             fn _ => Unknown) @ env) e))
                             pes, others), loc)
@@ -226,9 +351,9 @@ fun exp env (all as (e, loc)) =
       | EWrite e => (EWrite (exp env e), loc)
       | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
 
-      | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc)
+      | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (Unknown :: env) e2), loc)
 
-      | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, t), loc)
+      | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, con env t), loc)
 
 fun reduce file =
     let
diff --git a/src/unnest.sml b/src/unnest.sml
index 77589bfb..a2ec32b0 100644
--- a/src/unnest.sml
+++ b/src/unnest.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -204,12 +204,19 @@ fun exp ((ks, ts), e as old, st : state) =
                                   | PRecord xpcs =>
                                     foldl (fn ((_, p, _), ts) => doVars (p, ts))
                                           ts xpcs
+
+                            fun bindOne subs = ((0, (ERel 0, #2 ed))
+                                                :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)
+
+                            fun bindMany (n, subs) =
+                                case n of
+                                    0 => subs
+                                  | _ => bindMany (n - 1, bindOne subs)
                         in
                             ([(EDVal (p, t, e), #2 ed)],
                              (doVars (p, ts),
                               maxName, ds,
-                              ((0, (ERel 0, #2 ed))
-                               :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs),
+                              bindMany (E.patBindsN p, subs),
                               by))
                         end
                       | EDValRec vis =>
@@ -310,6 +317,7 @@ fun exp ((ks, ts), e as old, st : state) =
                                                                          let
                                                                              (*val () = print (Int.toString ex ^ "\n")*)
                                                                              val (name, t') = List.nth (ts, ex)
+                                                                             val t' = squishCon cfv t'
                                                                          in
                                                                              ((EAbs (name,
                                                                                      t',
@@ -354,6 +362,8 @@ fun exp ((ks, ts), e as old, st : state) =
             (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e),
                                      ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))),
                                      ("e'", ElabPrint.p_exp ElabEnv.empty e')];*)
+            (*Print.prefaces "Let" [("Before", ElabPrint.p_exp ElabEnv.empty (old, ErrorMsg.dummySpan)),
+                                  ("After", ElabPrint.p_exp ElabEnv.empty (ELet (eds, e', t), ErrorMsg.dummySpan))];*)
             (ELet (eds, e', t),
              {maxName = maxName,
               decls = ds})