§ LCNF

• let x := v in e ~= (\x -> e) v

let x : Nat := 2
let xarr : Vec Int x := Nil
let 2arr : Vec Int 2 := Nil
in rfl : xarr = 2arr

(\x ->
   let xarr : Vec Int x := Nil
   let 2arr : Vec Int 2 := Nil
   in rfl : xarr = 2arr) 2
      ^^^^^^^^^^^^^^^^^ <---- (ill-typed under CIC)

Erased a ~ Erased b
(\x ->
   let xarr : Vec Int (Erased x) := Nil
   let 2arr : Vec Int (Erased 2) := Nil
   in rfl : xarr = 2arr) 2
      ^^^^^^^^^^^^^^^^^ <---- (ill-typed under CIC)

§ Erased

match x with
  | F1 f1 => h f1
  | F2 f2 => h f2

• Design an ill-typed type system to allow only the types of errors that occur when floating let/join points?

def tupleN (n: Nat) (t: Type) :=
  match n with
  | 0 => Unit
  | n+1 => t * (tupleN n t)

def foo n := Vec Int n

Any ~ t
def f (n: Nat): (tupleN n t) := ...
def f (n: Nat): Any := ...