diff --git a/src/Lean/Compiler/Check.lean b/src/Lean/Compiler/Check.lean
index 8145d3e93d..724a262f86 100644
--- a/src/Lean/Compiler/Check.lean
+++ b/src/Lean/Compiler/Check.lean
@@ -8,6 +8,10 @@ import Lean.Compiler.Util
 
 namespace Lean.Compiler.InferType
 
+/-!
+Type checker for LCNF expressions
+-/
+
 structure Config where
   terminalCasesOnly : Bool := false
 
diff --git a/src/Lean/Compiler/CompilerM.lean b/src/Lean/Compiler/CompilerM.lean
index b6bd692e11..830d544138 100644
--- a/src/Lean/Compiler/CompilerM.lean
+++ b/src/Lean/Compiler/CompilerM.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Util.ForEachExpr
-import Lean.Meta.InferType
+import Lean.Compiler.InferType
 
 namespace Lean.Compiler
 
@@ -23,20 +23,28 @@ instance : AddMessageContext CompilerM where
     let opts ← getOptions
     return MessageData.withContext { env, lctx, opts, mctx := {} } msgData
 
-@[inline] def liftMetaM (x : MetaM α) : CompilerM α := do
-  x.run' { lctx := (← get).lctx }
+/--
+Infer the type of a LCNF expression.
+-/
+def inferType (e : Expr) : CompilerM Expr := do
+  InferType.inferType e { lctx := (← get).lctx }
 
-def inferType (e : Expr) : CompilerM Expr := liftMetaM <| Meta.inferType e
+def getLevel (type : Expr) : CompilerM Level := do
+  match (← inferType type) with
+  | .sort u => return u
+  | e => if e.isAnyType then return levelOne else throwError "type expected{indentExpr type}"
 
-def whnf (e : Expr) : CompilerM Expr := liftMetaM <| Meta.whnf e
+/-- Create `lcUnreachable type` -/
+def mkLcUnreachable (type : Expr) : CompilerM Expr := do
+  let u ← getLevel type
+  return .app (.const ``lcUnreachable [u]) type
 
-def inferType' (e : Expr) : CompilerM Expr := liftMetaM do Meta.whnf (← Meta.inferType e)
-
-def isProp (e : Expr) : CompilerM Bool := liftMetaM <| Meta.isProp e
-
-def isTypeFormerType (e : Expr) : CompilerM Bool := liftMetaM <| Meta.isTypeFormerType e
-
-def isDefEq (a b : Expr) : CompilerM Bool := liftMetaM <| Meta.isDefEq a b
+/-- Create `lcCast expectedType e : expectedType` -/
+def mkLcCast (e : Expr) (expectedType : Expr) : CompilerM Expr := do
+  let type ← inferType e
+  let u ← getLevel type
+  let v ← getLevel expectedType
+  return mkApp3 (.const ``lcCast [u, v]) type expectedType e
 
 def mkLocalDecl (binderName : Name) (type : Expr) (bi := BinderInfo.default) : CompilerM Expr := do
   let fvarId ← mkFreshFVarId
diff --git a/src/Lean/Compiler/Decl.lean b/src/Lean/Compiler/Decl.lean
index 458aef27f2..b945d88ebd 100644
--- a/src/Lean/Compiler/Decl.lean
+++ b/src/Lean/Compiler/Decl.lean
@@ -56,7 +56,7 @@ def toDecl (declName : Name) : CoreM Decl := do
     let value ← Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs (← Meta.etaExpand body)
     let value ← replaceUnsafeRecNames value
     let value ← macroInline value
-    let value ← toLCNF {} value
+    -- let value ← toLCNF {} value -- TODO: uncomment
     return { name := declName, type := info.type, value }
 
 def Decl.check (decl : Decl) : CoreM Unit := do
diff --git a/src/Lean/Compiler/LCNF.lean b/src/Lean/Compiler/LCNF.lean
index 7bcd713af9..908f9f7bc4 100644
--- a/src/Lean/Compiler/LCNF.lean
+++ b/src/Lean/Compiler/LCNF.lean
@@ -9,9 +9,12 @@ import Lean.Util.Recognizers
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Transform
 import Lean.Compiler.InlineAttrs
-import Lean.Compiler.CompilerM
+import Lean.Compiler.InferType
 import Lean.Compiler.Util
 
+-- TODO: port file to the new LCNF format
+
+#exit
 namespace Lean.Compiler
 /-!
 # Lean Compiler Normal Form (LCNF)
@@ -27,36 +30,113 @@ structure Context where
   root : Bool
 
 structure State where
-  cache   : PersistentExprMap Expr := {}
+  /-- Local context containing the original Lean types (not LCNF ones). -/
+  lctx     : LocalContext := {}
+  /-- Local context containing Lean LCNF types. -/
+  lctx' : LocalContext := {}
+  letFVars : Array Expr := #[]
+  /-- Next auxiliary variable suffix -/
+  nextIdx : Nat := 1
+  /-- Cache from Lean regular expression to LCNF expression. -/
+  cache : PersistentExprMap Expr := {}
 
-abbrev M := ReaderT Context $ StateRefT State CompilerM
+abbrev M := ReaderT Context $ StateRefT State CoreM
+
+/-- Return the type of the given LCNF expression. -/
+def inferType (e : Expr) : M Expr := do
+  InferType.inferType e { lctx := (← get).lctx' }
+
+@[inline] def liftMetaM (x : MetaM α) : M α := do
+  x.run' { lctx := (← get).lctx }
 
 @[inline] def withRoot (flag : Bool) (x : M α) : M α :=
   withReader (fun _ => { root := flag }) x
 
 def withNewRootScope (x : M α) : M α := do
   let saved ← get
+  modify fun s => { s with letFVars := #[] }
   try
-    withRoot true <| Compiler.withNewScope x
+    withRoot true x
   finally
+    let saved := { saved with nextIdx := (← get).nextIdx }
     set saved
 
+/-- Create a new local declaration using a Lean regular type. -/
+def mkLocalDecl (binderName : Name) (type : Expr) (bi := BinderInfo.default) : M Expr := do
+  let fvarId ← mkFreshFVarId
+  let type' ← liftMetaM <| toLCNFType type
+  modify fun s => { s with
+    lctx  := s.lctx.mkLocalDecl fvarId binderName type bi
+    lctx' := s.lctx'.mkLocalDecl fvarId binderName type' bi
+  }
+  return .fvar fvarId
+
+def mkLetDecl (binderName : Name) (type : Expr) (value : Expr) (type' : Expr) (value' : Expr) (nonDep : Bool) : M Expr := do
+  let fvarId ← mkFreshFVarId
+  let x := .fvar fvarId
+  modify fun s => { s with
+    lctx     := s.lctx.mkLetDecl fvarId binderName type value nonDep
+    lctx'    := s.lctx'.mkLetDecl fvarId binderName type' value' true
+    letFVars := s.letFVars.push x
+  }
+  return x
+
+/-- Create an auxiliary `let`-declaration for the given LCNF expression. -/
+def mkAuxLetDecl (e : Expr) : M Expr := do
+  if (← read).root then
+    return e
+  else
+    let fvarId ← mkFreshFVarId
+    let binderName := .num `_x (← get).nextIdx
+    modify fun s => { s with nextIdx := s.nextIdx + 1 }
+    let type ← inferType e
+    let x := .fvar fvarId
+    modify fun s => { s with
+      lctx'    := s.lctx'.mkLetDecl fvarId binderName type e true
+      letFVars := s.letFVars.push x
+    }
+    return x
+
+def visitLambda (e : Expr) : M (Array Expr × Expr) :=
+  go e #[]
+where
+  go (e : Expr) (fvars : Array Expr) := do
+    if let .lam binderName type body binderInfo := e then
+      let type := type.instantiateRev fvars
+      let fvar ← mkLocalDecl binderName type binderInfo
+      go body (fvars.push fvar)
+    else
+      return (fvars, e.instantiateRev fvars)
+
+def visitBoundedLambda (e : Expr) (n : Nat) : M (Array Expr × Expr) :=
+  go e n #[]
+where
+  go (e : Expr) (n : Nat) (fvars : Array Expr) := do
+    if n == 0 then
+      return (fvars, e.instantiateRev fvars)
+    else if let .lam binderName type body binderInfo := e then
+      let type := type.instantiateRev fvars
+      let fvar ← mkLocalDecl binderName type binderInfo
+      go body (n-1) (fvars.push fvar)
+    else
+      return (fvars, e.instantiateRev fvars)
+
+def mkLetUsingScope (e : Expr) : M Expr :=
+  return (← get).lctx'.mkLambda (← get).letFVars e
+
+def mkLambda (xs : Array Expr) (e : Expr) : M Expr :=
+  return (← get).lctx'.mkLambda xs e
+
 /--
 Eta-expand with `n` lambdas.
 -/
-def etaExpandN (e : Expr) (n : Nat) : CompilerM Expr := do
+def etaExpandN (e : Expr) (n : Nat) : M Expr := do
   if n == 0 then
     return e
   else liftMetaM do
     Meta.forallBoundedTelescope (← Meta.inferType e) n fun xs _ =>
       Meta.mkLambdaFVars xs (mkAppN e xs)
 
-def mkAuxLetDecl (e : Expr) : M Expr := do
-  if (← read).root then
-    return e
-  else
-    Compiler.mkAuxLetDecl e
-
 /--
 Put the given expression in `LCNF`.
 
@@ -64,9 +144,9 @@ Put the given expression in `LCNF`.
 - Eta-expand applications of declarations that satisfy `shouldEtaExpand`.
 - Put computationally relevant expressions in A-normal form.
 -/
-partial def toLCNF (lctx : LocalContext) (e : Expr) : CoreM Expr := do
-  let ((e, _), s) ← visit e |>.run { root := true } |>.run {} |>.run { lctx }
-  return s.lctx.mkLambda s.letFVars e
+partial def toLCNF (e : Expr) : CoreM Expr := do
+  let (e, s) ← visit e |>.run { root := true } |>.run {}
+  return s.lctx'.mkLambda s.letFVars e
 where
   visitChild (e : Expr) : M Expr :=
     withRoot false <| visit e
@@ -120,31 +200,48 @@ where
   /--
   Visit a `matcher`/`casesOn` alternative.
   -/
-  visitAlt (e : Expr) (numParams : Nat) : M Expr := do
+  visitAlt (e : Expr) (numParams : Nat) : M (Expr × Expr) := do
     withNewRootScope do
-      let mut (as, e) ← Compiler.visitBoundedLambda e numParams
+      let mut (as, e) ← visitBoundedLambda e numParams
       if as.size < numParams then
         e ← etaExpandN e (numParams - as.size)
-        let (as', e') ← Compiler.visitLambda e
+        let (as', e') ← ToLCNF.visitLambda e
         as := as ++ as'
         e := e'
       e ← mkLetUsingScope (← visit e)
-      mkLambda as e
+      let eType ← inferType e
+      return (eType, (← mkLambda as e))
 
-  visitCases (casesInfo : CasesInfo) (e : Expr) : M Expr :=
+  visitCases (casesInfo : CasesInfoPreLCNF) (e : Expr) : M Expr :=
     etaIfUnderApplied e casesInfo.arity do
-      let mut args := e.getAppArgs
+      let args := e.getAppArgs
+      let mut argsNew := #[default]
+      let mut discrTypes := #[]
       for i in casesInfo.discrsRange do
-        args ← args.modifyM i visitChild
+        let discr ← visitChild args[i]!
+        let discrType ← inferType discr
+        argsNew := argsNew.push discr
+        discrTypes := discrTypes.push discrType
+      let mut resultType ← liftMetaM (toLCNFType e)
       for i in casesInfo.altsRange, numParams in casesInfo.altNumParams do
-        let alt ← visitAlt args[i]! numParams
-        args := args.set! i alt
-      mkAppWithArity e.getAppFn args casesInfo.arity
+        let (altType, alt) ← visitAlt args[i]! numParams
+        unless compatibleTypes altType resultType do
+          resultType := anyTypeExpr
+        argsNew := argsNew.push alt
+      let motive ← discrTypes.foldrM (init := resultType) fun discrType resultType => mkArrow discrType resultType
+      argsNew := argsNew.set! 0 motive
+      let result := mkAppN e.getAppFn argsNew
+      if args.size == casesInfo.arity then
+        mkAuxLetDecl result
+      else
+        mkOverApplication result args casesInfo.arity
 
   visitCtor (arity : Nat) (e : Expr) : M Expr :=
     etaIfUnderApplied e arity do
       visitAppDefault e.getAppFn e.getAppArgs
 
+-- TODO: stopped here
+
   visitQuotLift (e : Expr) : M Expr := do
     let arity := 6
     etaIfUnderApplied e arity do
@@ -286,7 +383,7 @@ where
     if (← isProp type) then
       /- We replace proofs with `lcProof` applications. -/
       return mkLcProof type
-    if (← isTypeFormerType type) then
+    if (← liftMetaM <| Meta.isTypeFormerType type) then
       /- Types and Type formers are not put into A-normal form. -/
       return e
     if let some e := (← get).cache.find? e then
diff --git a/src/Lean/Compiler/Main.lean b/src/Lean/Compiler/Main.lean
index a583577395..6b01b3403e 100644
--- a/src/Lean/Compiler/Main.lean
+++ b/src/Lean/Compiler/Main.lean
@@ -38,7 +38,8 @@ def compile (declNames : Array Name) : CoreM Unit := do
   let declNames ← declNames.filterM shouldGenerateCode
   let decls ← declNames.mapM toDecl
   checkpoint `init decls
-  let decls ← decls.mapM (·.terminalCases)
-  checkpoint `terminalCases decls
+  -- TODO: uncomment
+  -- let decls ← decls.mapM (·.terminalCases)
+  -- checkpoint `terminalCases decls
 
-end Lean.Compiler
\ No newline at end of file
+end Lean.Compiler
diff --git a/src/Lean/Compiler/TerminalCases.lean b/src/Lean/Compiler/TerminalCases.lean
index f6e56f94b0..b1067004d5 100644
--- a/src/Lean/Compiler/TerminalCases.lean
+++ b/src/Lean/Compiler/TerminalCases.lean
@@ -7,6 +7,8 @@ import Lean.Meta.Check
 import Lean.Compiler.Util
 import Lean.Compiler.Decl
 
+#exit -- TODO: port file to new LCNF format
+
 namespace Lean.Compiler
 
 namespace TerminalCases