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

let x : Nat := 2let xarr : Vec Int x := Nillet 2arr : Vec Int 2 := Nilin 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 nAny ~ tdef f (n: Nat): (tupleN n t) := ...def f (n: Nat): Any := ...