Improvements to erasure checking, fix to codegen issue

2024-11-29 10:02:45 -08:00
parent 052bab81cb
commit 18e44cb7d3
18 changed files with 581 additions and 233 deletions
--- a/TODO.md
+++ b/TODO.md
@@ -1,6 +1,14 @@

 ## TODO

+- [ ] make $ special
+  - Makes inference easier, cleaner output, and allows `foo $ \ x => ...`
+  - remove hack from Elab.infer
+- [ ] Support @ on the LHS
+- [ ] records
+- [ ] rework unify case tree
+  - Idris needs help with the case tree to keep code size down, do it in stages, one dcon at a time.
+- [ ] Strategy to avoid three copies of `Prelude.newt` in this source tree
 - [x] add filenames to FC
 - [x] maybe use backtick for javascript so we don't highlight strings as JS
 - [ ] add namespaces
@@ -8,6 +16,7 @@
 - [x] imported files leak info messages everywhere
  - For now, take the start ix for the file and report at end starting there
 - [ ] update node shim to include idris2-playground changes
+- [ ] refactor playground to better share code with idris2-playground
 - [ ] accepting DCon for another type (skipping case, but should be an error)
 - [ ] don't allow (or dot) duplicate names on LHS
 - [ ] remove metas from context, M has TopContext
@@ -40,9 +49,7 @@
  - [x] equational reasoning sample (maybe PLFA "Lists")
  - actual `if_then_else_` isn't practical because the language is strict
 - [x] Search should look at context
- [ ] records
 - [ ] copattern matching
- [ ] Support @ on the LHS
 - [ ] Get `Combinatory.newt` to work
 - [x] Remember operators from imports
 - [ ] Default cases for non-primitives (currently gets expanded to all constructors)
--- a/aoc2023/Day2.newt
+++ b/aoc2023/Day2.newt
@@ -29,7 +29,7 @@ pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o`
 pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, '  ')`
 pfunc toInt : String -> Int := `s => Number(s)`

-mapM : {a b c : U} -> (a -> Either b c) -> List a -> Either b (List c)
+mapM : ∀ a b c. (a -> Either b c) -> List a -> Either b (List c)
 mapM f Nil = Right Nil
 mapM f (x :: xs) = case f x of
  Left msg => Left msg
--- a/newt/Prelude.newt
+++ b/newt/Prelude.newt
@@ -15,36 +15,49 @@ _||_ : Bool → Bool → Bool
 True || _ = True
 False || b = b

+infixl 6 _==_
+class Eq a where
+  _==_ : a → a → Bool
+
 data Nat : U where
  Z : Nat
  S : Nat -> Nat

-data Maybe : U -> U where
-  Just : {a : U} -> a -> Maybe a
-  Nothing : {a : U} -> Maybe a
+instance Eq Nat where
+  Z == Z = True
+  S n == S m = n == m
+  x == y = False

-fromMaybe : {a} → a → Maybe a → a
+data Maybe : U -> U where
+  Just : ∀ a. a -> Maybe a
+  Nothing : ∀ a. Maybe a
+
+fromMaybe : ∀ a. a → Maybe a → a
 fromMaybe a Nothing = a
 fromMaybe _ (Just a) = a

 data Either : U -> U -> U where
-  Left : {a b : U} -> a -> Either a b
-  Right : {a b : U} -> b -> Either a b
+  Left : {0 a b : U} -> a -> Either a b
+  Right : {0 a b : U} -> b -> Either a b

 infixr 7 _::_
 data List : U -> U where
-  Nil : {A} → List A
-  _::_ : {A} → A → List A → List A
+  Nil : ∀ A. List A
+  _::_ : ∀ A. A → List A → List A
+
+length : ∀ a. List a → Nat
+length Nil = Z
+length (x :: xs) = S (length xs)


 infixl 7 _:<_
 data SnocList : U → U where
-  Lin : {A} → SnocList A
-  _:<_ : {A} → SnocList A → A → SnocList A
+  Lin : ∀ A. SnocList A
+  _:<_ : ∀ A. SnocList A → A → SnocList A

 -- 'chips'
 infixr 6 _<>>_
-_<>>_ : {a} → SnocList a → List a → List a
+_<>>_ : ∀ a. SnocList a → List a → List a
 Lin <>> ys = ys
 (xs :< x) <>> ys = xs <>> x :: ys

@@ -52,53 +65,36 @@ Lin <>> ys = ys
 -- inference? Figure out why.
 -- Currently very noisy in generated code (if nothing else, optimize it out?)
 infixr 0 _$_
-_$_ : {a b : U} -> (a -> b) -> a -> b
+_$_ : ∀ a b. (a -> b) -> a -> b
 f $ a = f a

 infixr 8 _×_
 infixr 2 _,_
 data _×_ : U → U → U where
-  _,_ : {A B} → A → B → A × B
-
+  _,_ : ∀ A B. A → B → A × B

 infixl 6 _<_
-data Ord : U → U where
-  MkOrd : {A} → (A → A → Bool) → Ord A
+class Ord a where
+  _<_ : a → a → Bool

-_<_ : {A} {{Ord A}} → A → A → Bool
-_<_ {{MkOrd cmp}} a b = cmp a b
-
-cmpNat : Nat → Nat → Bool
-cmpNat Z Z = True
-cmpNat Z m = False
-cmpNat n Z = True
-cmpNat (S n) (S m) = True
-
-OrdNat : Ord Nat
-OrdNat = MkOrd cmpNat
+instance Ord Nat where
+  _ < Z = False
+  Z < S _ = True
+  S n < S m = n < m

 -- Monad

-- TODO sugar for if then else (mixfix is too eager)
-
-- TODO stack with Applicative, etc?
-
-data Monad : (U -> U) -> U where
-  MkMonad : { M : U -> U } ->
-            (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
-            (pure : {A : U} -> A -> M A) ->
-            Monad M
+class Monad (m : U → U) where
+  bind : {0 a b} → m a → (a → m b) → m b
+  pure : {0 a} → a → m a

 infixl 1 _>>=_ _>>_
-_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
-_>>=_ {a} {b} {m} {{MkMonad bind' _}}  ma amb = bind' {a} {b} ma amb
+_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
+ma >>= amb = bind ma amb

-_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
+_>>_ :  {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b
 ma >> mb = mb

-pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
-pure {_} {_} {{MkMonad _ pure'}} a = pure' a
-
 -- Equality

 infixl 1 _≡_
@@ -114,114 +110,90 @@ sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a
 sym Refl = Refl

 -- Functor
-data Functor : (U → U) → U where
-  MkFunctor : {m : U → U} → ({a b : U} → (a → b) → m a → m b) → Functor m

-map : {m} {{Functor m}} → {a b} → (a → b) → m a → m b
-map {{MkFunctor f}} ma = f ma
+class Functor (m : U → U) where
+  map : {0 a b} → (a → b) → m a → m b

 infixr 4 _<$>_
-_<$>_ : {f : U → U} {{Functor f}} {a b} → (a → b) → f a → f b
+_<$>_ : {0 f} {{Functor f}} {0 a b} → (a → b) → f a → f b
 f <$> ma = map f ma

+instance Functor Maybe where
+  map f Nothing = Nothing
+  map f (Just a) = Just (f a)

-mapMaybe : {a b} → (a → b) → Maybe a → Maybe b
-mapMaybe f Nothing = Nothing
-mapMaybe f (Just a) = Just (f a)
+instance Functor List where
+  map f Nil = Nil
+  map f (x :: xs) = f x :: map f xs

-FunctorMaybe : Functor Maybe
-FunctorMaybe = MkFunctor mapMaybe
+instance Functor SnocList where
+  map f Lin = Lin
+  map f (xs :< x) = map f xs :< f x

-
-
-- Idris is lazy in second arg, we don't have that.
-data Alternative : (U → U) → U where
-  MkAlt : {m : U → U} →
-          ({a} → m a → m a → m a) →
-          Alternative m
+-- TODO this probably should depend on / entail Functor
+infixl 3 _<*>_
+class Applicative (f : U → U) where
+  -- appIsFunctor : Functor f
+  return : {0 a} → a → f a
+  _<*>_ : {0 a b} -> f (a → b) → f a → f b

 infixr 2 _<|>_
-_<|>_ : {m : U → U} {{Alternative m}} → {a} → m a → m a → m a
-_<|>_ {m} {{MkAlt f}} {a} x y = f x y
+class Alternative (m : U → U) where
+  _<|>_ : {0 a} → m a → m a → m a

-altMaybe : {a} → Maybe a → Maybe a → Maybe a
-altMaybe Nothing x = x
-altMaybe (Just x) _ = Just x
-
-AltMaybe : Alternative Maybe
-AltMaybe = MkAlt altMaybe
+instance Alternative Maybe where
+  Nothing <|> x = x
+  Just x <|> _ = Just x

 -- Semigroup

 infixl 8 _<+>_
-data Semigroup : U → U where
-  MkSemi : {a} → (a → a → a) → Semigroup a
-
-_<+>_ : {a} {{Semigroup a}} → a → a → a
-_<+>_ {{MkSemi op}} x y = op x y
-
+class Semigroup a where
+  _<+>_ : a → a → a

 infixl 7 _+_
-data Add : U → U where
-  MkAdd : {A} → (A → A → A) → Add A
-
-_+_ : {A} {{Add A}} → A → A → A
-_+_ {{MkAdd add}} x y  = add x y
+class Add a where
+  _+_ : a → a → a

 infixl 8 _*_
-data Mul : U → U where
-  MkMul : {A} →
-          (A → A → A) →
-          Mul A
+class Mul a where
+  _*_ : a → a → a

-_*_ : {A} {{Mul A}} → A → A → A
-_*_ {{MkMul mul}} x y  = mul x y
+instance Add Nat where
+  Z + m = m
+  S n + m = S (n + m)
+
+instance Mul Nat where
+  Z * _ = Z
+  S n * m = m + n * m


-- TODO codata/copatterns might be nice here?
-- AddNat : AddNat
-- AddNat .add Z m = m
-- AddNat .add (S n) m = S (self .add n m)
-
-addNat : Nat → Nat → Nat
-addNat Z m = m
-addNat (S n) m = S (addNat n m)
-
-AddNat : Add Nat
-AddNat = MkAdd addNat
-
-mulNat : Nat → Nat → Nat
-mulNat Z _ = Z
-mulNat (S n) m = m + mulNat n m
-
-MulNat : Mul Nat
-MulNat = MkMul mulNat
-
-
-- TODO Sub
 infixl 7 _-_
-_-_ : Nat -> Nat -> Nat
+class Sub a where
+  _-_ : a → a → a
+
+instance Sub Nat where
  Z - m = Z
  n - Z = n
  S n - S m = n - m

+infixr 7 _++_
+class Concat a where
+  _++_ : a → a → a

 ptype String
 ptype Int
 ptype Char

-- probably want to switch to Int or implement magic Nat
-pfunc length : String → Nat := "(s) => {
-  let rval = Z
-  for (let i = 0; i < s.length; s++) rval = S(rval)
-  return rval
-}"
+pfunc sconcat : String → String → String := `(x,y) => x + y`
+instance Concat String where
+  _++_ = sconcat

 data Unit : U where
  MkUnit : Unit

 ptype Array : U → U
-pfunc listToArray : {a : U} -> List a -> Array a := "
+pfunc listToArray : {a : U} -> List a -> Array a := `
 (a, l) => {
  let rval = []
  while (l.tag !== 'Nil') {
@@ -230,17 +202,54 @@ pfunc listToArray : {a : U} -> List a -> Array a := "
  }
  return rval
 }
-"
-pfunc alen : {a : U} -> Array a -> Int := `(a,arr) => arr.length`
-pfunc aget : {a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]`
-pfunc aempty : {a : U} -> Unit -> Array a := `() => []`
+`

+pfunc alen : {0 a : U} -> Array a -> Int := `(a,arr) => arr.length`
+pfunc aget : {0 a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]`
+pfunc aempty : {0 a : U} -> Unit -> Array a := `() => []`
+
+pfunc arrayToList uses (Nil _::_) : {0 a} → Array a → List a := `(a,arr) => {
+  let rval = Nil(a)
+  for (let i = arr.length - 1;i >= 0; i--) {
+    rval = _$3A$3A_(a, arr[i], rval)
+  }
+  return rval
+}`
+
+
+
+-- for now I'll run this in JS
+pfunc lines : String → List String := `(s) => arrayToList(s.split('\n'))`
+
+pfunc p_strHead : (s : String) -> Char := `(s) => s[0]`
+pfunc p_strTail : (s : String) -> String := `(s) => s[0]`
+
+pfunc trim : String -> String := `s => s.trim()`
+pfunc split uses (Nil _::_) : String -> String -> List String := `(s, by) => {
+  let parts = s.split(by)
+  let rval = Nil(String)
+  parts.reverse()
+  parts.forEach(p => { rval = _$3A$3A_(undefined, p, rval) })
+  return rval
+}`
+
+pfunc slen : String -> Int := `s => s.length`
+pfunc sindex : String -> Int -> Char := `(s,i) => s[i]`
+
+-- TODO represent Nat as number at runtime
+pfunc natToInt : Nat -> Int := `(n) => {
+  let rval = 0
+  while (n.tag === 'S') {
+    n = n.h0
+    rval++
+  }
+  return rval
+}`

 pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')`
-pfunc replicate : Nat -> Char → String := `() => abort('FIXME replicate')`
-
-
+pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))`

+-- I don't want to use an empty type because it would be a proof of void
 ptype World

 data IORes : U -> U where
@@ -249,16 +258,143 @@ data IORes : U -> U where
 IO : U -> U
 IO a = World -> IORes a

-- TODO - if I move w to the left, I get "extra pattern variable"
-- because I'm not looking instide the IO b type, probably should force it.
-iobind : {a b : U} -> IO a -> (a -> IO b) -> IO b
-iobind ma mab = \ w => case ma w of
-  (MkIORes a w) => mab a w
+instance Monad IO where
+  bind ma mab = \ w => case ma w of
+    MkIORes a w => mab a w
+  pure a = \ w => MkIORes a w

-iopure : {a : U} -> a -> IO a
-iopure a = \ w => MkIORes a w
+bindList : ∀ a b. List a → (a → List b) → List b

-IOMonad : Monad IO
-IOMonad = MkMonad iobind iopure
+instance ∀ a. Concat (List a) where
+  Nil ++ ys = ys
+  (x :: xs) ++ ys = x :: (xs ++ ys)

-pfunc putStrLn : String -> IO Unit := `(s) => (w) => console.log(s)`
+instance Monad List where
+  pure a = a :: Nil
+  bind Nil amb = Nil
+  bind (x :: xs) amb = amb x ++ bind xs amb
+
+class HasIO (m : U -> U) where
+  liftIO : ∀ a. IO a → m a
+
+instance HasIO IO where
+  liftIO a = a
+
+pfunc debugLog uses (MkIORes MkUnit) : ∀ a. a -> IO Unit := `(_,s) => (w) => {
+  console.log(s)
+  return MkIORes(undefined,MkUnit,w)
+}`
+
+pfunc primPutStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
+  console.log(s)
+  return MkIORes(undefined,MkUnit,w)
+}`
+
+putStrLn : ∀ io. {{HasIO io}} -> String -> io Unit
+putStrLn s = liftIO (primPutStrLn s)
+
+pfunc showInt : Int -> String := `(i) => String(i)`
+
+class Show a where
+  show : a → String
+
+instance Show String where
+  show a = a
+
+instance Show Int where
+  show = showInt
+
+pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)`
+
+infix 6 _<=_
+pfunc _<=_ uses (True False) : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False`
+
+pfunc unpack : String -> List Char
+  := `(s) => {
+    let acc = Nil(Char)
+    for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc)
+    return acc
+}`
+
+pfunc pack : List Char → String := `(cs) => {
+  let rval = ''
+  while (cs.tag === '_::_') {
+    rval += cs.h1
+    cs = cs.h2
+  }
+
+  return rval
+}
+`
+
+pfunc debugStr : ∀ a. a → String := `(_, obj) => {
+  const go = (obj) => {
+    if (obj?.tag) {
+      let rval = '('+obj.tag
+      for(let i=0;;i++) {
+        let key = 'h'+i
+        if (!(key in obj)) break
+        rval += ' ' + go(obj[key])
+      }
+      return rval+')'
+    } else {
+      return JSON.stringify(obj)
+    }
+  }
+  return go(obj)
+}`
+
+pfunc stringToInt : String → Int := `(s) => {
+  let rval = Number(s)
+  if (isNaN(rval)) throw new Error(s + " is NaN")
+  return rval
+}`
+
+foldl : ∀ A B. (B -> A -> B) -> B -> List A -> B
+foldl f acc Nil = acc
+foldl f acc (x :: xs) = foldl f (f acc x) xs
+
+infixl 9 _∘_
+_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
+(f ∘ g) x = f (g x)
+
+
+pfunc addInt : Int → Int → Int := `(x,y) => x + y`
+pfunc mulInt : Int → Int → Int := `(x,y) => x * y`
+pfunc subInt : Int → Int → Int := `(x,y) => x - y`
+pfunc ltInt uses (True False) : Int → Int → Bool := `(x,y) => x < y ? True : False`
+
+instance Mul Int where
+  x * y = mulInt x y
+
+instance Add Int where
+  x + y = addInt x y
+
+instance Sub Int where
+  x - y = subInt x y
+
+instance Ord Int where
+  x < y = ltInt x y
+
+printLn : {m} {{HasIO m}} {a} {{Show a}} → a → m Unit
+printLn a = putStrLn (show a)
+
+-- opaque JSObject
+ptype JSObject
+
+reverse : ∀ a. List a → List a
+reverse {a} = go Nil
+  where
+    go : List a → List a → List a
+    go acc Nil = acc
+    go acc (x :: xs) = go (x :: acc) xs
+
+-- Like Idris1, but not idris2, we need {a} to put a in scope.
+span : ∀ a. (a -> Bool) -> List a -> List a × List a
+span {a} f xs = go xs Nil
+  where
+    go : List a -> List a -> List a × List a
+    go Nil left = (reverse left, Nil)
+    go (x :: xs) left = if f x
+      then go xs (x :: left)
+      else (reverse left, x :: xs)
--- a/playground/samples/Day2.newt
+++ b/playground/samples/Day2.newt
@@ -34,7 +34,7 @@ pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o`
 pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, '  ')`
 pfunc toInt : String -> Int := `s => Number(s)`

-mapM : {a b c : U} -> (a -> Either b c) -> List a -> Either b (List c)
+mapM : ∀ a b c. (a -> Either b c) -> List a -> Either b (List c)
 mapM f Nil = Right Nil
 mapM f (x :: xs) = case f x of
  Left msg => Left msg
--- a/playground/samples/Lists.newt
+++ b/playground/samples/Lists.newt
@@ -44,11 +44,11 @@ data _≡_ : ∀ A . A -> A -> U where
    Refl : ∀ A . {a : A} -> a ≡ a

 -- If a ≡ b then b ≡ a
-sym : {A} {a b : A} -> a ≡ b -> b ≡ a
+sym : ∀ A. {0 a b : A} -> a ≡ b -> b ≡ a
 sym Refl = Refl

 -- if a ≡ b and b ≡ c then a ≡ c
-trans : {A : U} {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
+trans : ∀ A. {0 a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
 trans Refl x = x

 -- This lets us replace a with b inside an expression if a ≡ b
--- a/playground/samples/Prelude.newt
+++ b/playground/samples/Prelude.newt
@@ -29,10 +29,10 @@ instance Eq Nat where
  x == y = False

 data Maybe : U -> U where
-  Just : {a : U} -> a -> Maybe a
-  Nothing : {a : U} -> Maybe a
+  Just : ∀ a. a -> Maybe a
+  Nothing : ∀ a. Maybe a

-fromMaybe : {a} → a → Maybe a → a
+fromMaybe : ∀ a. a → Maybe a → a
 fromMaybe a Nothing = a
 fromMaybe _ (Just a) = a

@@ -45,6 +45,10 @@ data List : U -> U where
  Nil : ∀ A. List A
  _::_ : ∀ A. A → List A → List A

+length : ∀ a. List a → Nat
+length Nil = Z
+length (x :: xs) = S (length xs)
+

 infixl 7 _:<_
 data SnocList : U → U where
@@ -61,7 +65,7 @@ Lin <>> ys = ys
 -- inference? Figure out why.
 -- Currently very noisy in generated code (if nothing else, optimize it out?)
 infixr 0 _$_
-_$_ : {a b : U} -> (a -> b) -> a -> b
+_$_ : ∀ a b. (a -> b) -> a -> b
 f $ a = f a

 infixr 8 _×_
@@ -181,13 +185,6 @@ ptype String
 ptype Int
 ptype Char

-- probably want to switch to Int or implement magic Nat
-pfunc length : String → Nat := `(s) => {
-  let rval = Z
-  for (let i = 0; i < s.length; s++) rval = S(rval)
-  return rval
-}`
-
 pfunc sconcat : String → String → String := `(x,y) => x + y`
 instance Concat String where
  _++_ = sconcat
@@ -211,7 +208,7 @@ pfunc alen : {0 a : U} -> Array a -> Int := `(a,arr) => arr.length`
 pfunc aget : {0 a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]`
 pfunc aempty : {0 a : U} -> Unit -> Array a := `() => []`

-pfunc arrayToList : {0 a} → Array a → List a := `(a,arr) => {
+pfunc arrayToList uses (Nil _::_) : {0 a} → Array a → List a := `(a,arr) => {
  let rval = Nil(a)
  for (let i = arr.length - 1;i >= 0; i--) {
    rval = _$3A$3A_(a, arr[i], rval)
@@ -228,11 +225,11 @@ pfunc p_strHead : (s : String) -> Char := `(s) => s[0]`
 pfunc p_strTail : (s : String) -> String := `(s) => s[0]`

 pfunc trim : String -> String := `s => s.trim()`
-pfunc split : String -> String -> List String := `(s, by) => {
+pfunc split uses (Nil _::_) : String -> String -> List String := `(s, by) => {
  let parts = s.split(by)
  let rval = Nil(String)
  parts.reverse()
-  parts.forEach(p => { rval = _$3A$3A_(List(String), p, rval) })
+  parts.forEach(p => { rval = _$3A$3A_(undefined, p, rval) })
  return rval
 }`

@@ -266,12 +263,28 @@ instance Monad IO where
    MkIORes a w => mab a w
  pure a = \ w => MkIORes a w

+bindList : ∀ a b. List a → (a → List b) → List b
+
+instance ∀ a. Concat (List a) where
+  Nil ++ ys = ys
+  (x :: xs) ++ ys = x :: (xs ++ ys)
+
+instance Monad List where
+  pure a = a :: Nil
+  bind Nil amb = Nil
+  bind (x :: xs) amb = amb x ++ bind xs amb
+
 class HasIO (m : U -> U) where
  liftIO : ∀ a. IO a → m a

 instance HasIO IO where
  liftIO a = a

+pfunc debugLog uses (MkIORes MkUnit) : ∀ a. a -> IO Unit := `(_,s) => (w) => {
+  console.log(s)
+  return MkIORes(undefined,MkUnit,w)
+}`
+
 pfunc primPutStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
  console.log(s)
  return MkIORes(undefined,MkUnit,w)
@@ -303,9 +316,41 @@ pfunc unpack : String -> List Char
    return acc
 }`

+pfunc pack : List Char → String := `(cs) => {
+  let rval = ''
+  while (cs.tag === '_::_') {
+    rval += cs.h1
+    cs = cs.h2
+  }

+  return rval
+}
+`

-foldl : {A B : U} -> (B -> A -> B) -> B -> List A -> B
+pfunc debugStr : ∀ a. a → String := `(_, obj) => {
+  const go = (obj) => {
+    if (obj?.tag) {
+      let rval = '('+obj.tag
+      for(let i=0;;i++) {
+        let key = 'h'+i
+        if (!(key in obj)) break
+        rval += ' ' + go(obj[key])
+      }
+      return rval+')'
+    } else {
+      return JSON.stringify(obj)
+    }
+  }
+  return go(obj)
+}`
+
+pfunc stringToInt : String → Int := `(s) => {
+  let rval = Number(s)
+  if (isNaN(rval)) throw new Error(s + " is NaN")
+  return rval
+}`
+
+foldl : ∀ A B. (B -> A -> B) -> B -> List A -> B
 foldl f acc Nil = acc
 foldl f acc (x :: xs) = foldl f (f acc x) xs

@@ -337,3 +382,19 @@ printLn a = putStrLn (show a)
 -- opaque JSObject
 ptype JSObject

+reverse : ∀ a. List a → List a
+reverse {a} = go Nil
+  where
+    go : List a → List a → List a
+    go acc Nil = acc
+    go acc (x :: xs) = go (x :: acc) xs
+
+-- Like Idris1, but not idris2, we need {a} to put a in scope.
+span : ∀ a. (a -> Bool) -> List a -> List a × List a
+span {a} f xs = go xs Nil
+  where
+    go : List a -> List a -> List a × List a
+    go Nil left = (reverse left, Nil)
+    go (x :: xs) left = if f x
+      then go xs (x :: left)
+      else (reverse left, x :: xs)
--- a/playground/samples/Reasoning.newt
+++ b/playground/samples/Reasoning.newt
@@ -2,20 +2,20 @@ module Reasoning

 infix 4 _≡_
 data _≡_ : {A : U} → A → A → U where
-  Refl : {A} {x : A} → x ≡ x
+  Refl : ∀ A. {x : A} → x ≡ x

-sym : {A} {x y : A} → x ≡ y → y ≡ x
+sym : ∀ A. {x y : A} → x ≡ y → y ≡ x
 sym Refl = Refl

-trans : {A} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+trans : ∀ A. {x y z : A} → x ≡ y → y ≡ z → x ≡ z
 trans Refl eq = eq

-cong : {A B} (f : A → B) {x y : A}
+cong : ∀ A B. (f : A → B) {x y : A}
  → x ≡ y
  → f x ≡ f y
 cong f Refl = Refl

-cong-app : {A B} {f g : A → B}
+cong-app : ∀ A B. {f g : A → B}
  → f ≡ g
  → (x : A) →  f x ≡ g x
 cong-app Refl = λ y => Refl
@@ -24,16 +24,16 @@ infixl 1 begin_
 infixr 2 _≡⟨⟩_ _≡⟨_⟩_
 infixl 3 _∎

-begin_ : {A} {x y : A} → x ≡ y → x ≡ y
-begin_ x≡y = x≡y
+begin_ : ∀ A. {x y : A} → x ≡ y → x ≡ y
+begin x≡y = x≡y

-_≡⟨⟩_  : {A} (x : A) {y : A} → x ≡ y → x ≡ y
+_≡⟨⟩_  : ∀ A. (x : A) {y : A} → x ≡ y → x ≡ y
 x ≡⟨⟩ x≡y = x≡y

-_≡⟨_⟩_ : {A} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
+_≡⟨_⟩_ : ∀ A. (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
 x ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z

-_∎ : {A} → (x : A) → x ≡ x
+_∎ : ∀ A. (x : A) → x ≡ x
 x ∎ = Refl


--- a/playground/samples/Tour.newt
+++ b/playground/samples/Tour.newt
@@ -136,8 +136,8 @@ concat a b = a + b

 -- Now we define Monad
 class Monad (m : U -> U) where
-  pure : {a} -> a -> m a
-  bind : {a b} -> m a -> (a -> m b) -> m b
+  pure : ∀ a. a -> m a
+  bind : ∀ a b. m a -> (a -> m b) -> m b

 /-
 This desugars to:
--- a/playground/samples/TypeClass.newt
+++ b/playground/samples/TypeClass.newt
@@ -1,11 +1,11 @@
 module TypeClass

 class Monad (m : U → U) where
-  bind : {a b} → m a → (a → m b) → m b
-  pure : {a} → a → m a
+  bind : ∀ a b. m a → (a → m b) → m b
+  pure : ∀ a. a → m a

 infixl 1 _>>=_ _>>_
-_>>=_ : {m} {{Monad m}} {a b} -> (m a) -> (a -> m b) -> m b
+_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
 ma >>= amb = bind ma amb

 _>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
@@ -15,7 +15,7 @@ data Either : U -> U -> U where
  Left : ∀ A B. A -> Either A B
  Right : ∀ A B. B -> Either A B

-instance {a} → Monad (Either a) where
+instance {a} -> Monad (Either a) where
  bind (Left a) amb = Left a
  bind (Right b) amb = amb b

--- a/port/Prelude.newt
+++ b/port/Prelude.newt
@@ -32,28 +32,28 @@ data Maybe : U -> U where
  Just : {a : U} -> a -> Maybe a
  Nothing : {a : U} -> Maybe a

-fromMaybe : {a} → a → Maybe a → a
+fromMaybe : ∀ a. a → Maybe a → a
 fromMaybe a Nothing = a
 fromMaybe _ (Just a) = a

 data Either : U -> U -> U where
-  Left : {a b : U} -> a -> Either a b
-  Right : {a b : U} -> b -> Either a b
+  Left : {0 a b : U} -> a -> Either a b
+  Right : {0 a b : U} -> b -> Either a b

 infixr 7 _::_
 data List : U -> U where
-  Nil : {A} → List A
-  _::_ : {A} → A → List A → List A
+  Nil : ∀ A. List A
+  _::_ : ∀ A. A → List A → List A


 infixl 7 _:<_
 data SnocList : U → U where
-  Lin : {A} → SnocList A
-  _:<_ : {A} → SnocList A → A → SnocList A
+  Lin : ∀ A. SnocList A
+  _:<_ : ∀ A. SnocList A → A → SnocList A

 -- 'chips'
 infixr 6 _<>>_
-_<>>_ : {a} → SnocList a → List a → List a
+_<>>_ : ∀ a. SnocList a → List a → List a
 Lin <>> ys = ys
 (xs :< x) <>> ys = xs <>> x :: ys

@@ -61,13 +61,13 @@ Lin <>> ys = ys
 -- inference? Figure out why.
 -- Currently very noisy in generated code (if nothing else, optimize it out?)
 infixr 0 _$_
-_$_ : {a b : U} -> (a -> b) -> a -> b
+_$_ : ∀ a b. (a -> b) -> a -> b
 f $ a = f a

 infixr 8 _×_
 infixr 2 _,_
 data _×_ : U → U → U where
-  _,_ : {A B} → A → B → A × B
+  _,_ : ∀ A B. A → B → A × B

 infixl 6 _<_
 class Ord a where
@@ -81,14 +81,14 @@ instance Ord Nat where
 -- Monad

 class Monad (m : U → U) where
-  bind : {a b} → m a → (a → m b) → m b
-  pure : {a} → a → m a
+  bind : {0 a b} → m a → (a → m b) → m b
+  pure : {0 a} → a → m a

 infixl 1 _>>=_ _>>_
-_>>=_ : {m} {{Monad m}} {a b} -> (m a) -> (a -> m b) -> m b
+_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
 ma >>= amb = bind ma amb

-_>>_ :  {m} {{Monad m}} {a b} -> m a -> m b -> m b
+_>>_ :  {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b
 ma >> mb = mb

 -- Equality
@@ -108,10 +108,10 @@ sym Refl = Refl
 -- Functor

 class Functor (m : U → U) where
-  map : {a b} → (a → b) → m a → m b
+  map : {0 a b} → (a → b) → m a → m b

 infixr 4 _<$>_
-_<$>_ : {f} {{Functor f}} {a b} → (a → b) → f a → f b
+_<$>_ : {0 f} {{Functor f}} {0 a b} → (a → b) → f a → f b
 f <$> ma = map f ma

 instance Functor Maybe where
@@ -130,12 +130,12 @@ instance Functor SnocList where
 infixl 3 _<*>_
 class Applicative (f : U → U) where
  -- appIsFunctor : Functor f
-  return : {a} → a → f a
-  _<*>_ : {a b} -> f (a → b) → f a → f b
+  return : {0 a} → a → f a
+  _<*>_ : {0 a b} -> f (a → b) → f a → f b

 infixr 2 _<|>_
 class Alternative (m : U → U) where
-  _<|>_ : {a} → m a → m a → m a
+  _<|>_ : {0 a} → m a → m a → m a

 instance Alternative Maybe where
  Nothing <|> x = x
@@ -266,11 +266,20 @@ instance Monad IO where
    MkIORes a w => mab a w
  pure a = \ w => MkIORes a w

-pfunc putStrLn : String -> IO Unit := `(s) => (w) => {
+class HasIO (m : U -> U) where
+  liftIO : ∀ a. IO a → m a
+
+instance HasIO IO where
+  liftIO a = a
+
+pfunc primPutStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
  console.log(s)
-  return MkIORes(Unit,MkUnit,w)
+  return MkIORes(undefined,MkUnit,w)
 }`

+putStrLn : ∀ io. {{HasIO io}} -> String -> io Unit
+putStrLn s = liftIO (primPutStrLn s)
+
 pfunc showInt : Int -> String := `(i) => String(i)`

 class Show a where
@@ -285,8 +294,7 @@ instance Show Int where
 pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)`

 infix 6 _<=_
-pfunc _<=_ : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False`
-
+pfunc _<=_ uses (True False) : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False`

 pfunc unpack : String -> List Char
  := `(s) => {
@@ -296,8 +304,7 @@ pfunc unpack : String -> List Char
 }`


-
-foldl : {A B : U} -> (B -> A -> B) -> B -> List A -> B
+foldl : ∀ A B. (B -> A -> B) -> B -> List A -> B
 foldl f acc Nil = acc
 foldl f acc (x :: xs) = foldl f (f acc x) xs

@@ -309,7 +316,7 @@ _∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
 pfunc addInt : Int → Int → Int := `(x,y) => x + y`
 pfunc mulInt : Int → Int → Int := `(x,y) => x * y`
 pfunc subInt : Int → Int → Int := `(x,y) => x - y`
-pfunc ltInt : Int → Int → Bool := `(x,y) => x < y ? True : False`
+pfunc ltInt uses (True False) : Int → Int → Bool := `(x,y) => x < y ? True : False`

 instance Mul Int where
  x * y = mulInt x y
@@ -323,8 +330,8 @@ instance Sub Int where
 instance Ord Int where
  x < y = ltInt x y

-printLn : {a} {{Show a}} → a → IO Unit
-printLn a = putStrLn $ show a
+printLn : {m} {{HasIO m}} {a} {{Show a}} → a → m Unit
+printLn a = putStrLn (show a)

 -- opaque JSObject
 ptype JSObject
--- a/src/Lib/Compile.idr
+++ b/src/Lib/Compile.idr
@@ -126,11 +126,19 @@ termToJS env (CLetRec nm t u) f =
    (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f)
    t' => JSnoc (JLet nm' t') (termToJS env' u f)

-termToJS env (CApp t args) f = termToJS env t (\ t' => argsToJS args [<] (\ args' => f (Apply t' args')))
+termToJS env (CApp t args etas) f = termToJS env t (\ t' => (argsToJS t' args [<] f)) --  (f (Apply t' args'))))
  where
-    argsToJS : List CExp -> SnocList JSExp -> (List JSExp -> JSStmt e) -> JSStmt e
-    argsToJS [] acc k = k (acc <>> [])
-    argsToJS (x :: xs) acc k = termToJS env x (\ x' => argsToJS xs (acc :< x') k)
+    etaExpand : JSEnv -> Nat -> SnocList JSExp -> JSExp -> JSExp
+    etaExpand env Z args tm = Apply tm (args <>> [])
+    etaExpand env (S etas) args tm =
+      let nm' = fresh "eta" env
+          env' = push env (Var nm')
+       in JLam [nm'] $ JReturn $ etaExpand (push env (Var nm')) etas (args :< Var nm') tm
+
+    argsToJS : JSExp -> List CExp -> SnocList JSExp -> (JSExp -> JSStmt e) -> JSStmt e
+    argsToJS tm [] acc k = k (etaExpand env etas acc tm)
+    -- k (acc <>> [])
+    argsToJS tm (x :: xs) acc k = termToJS env x (\ x' => argsToJS tm xs (acc :< x') k)


 termToJS env (CCase t alts) f =
@@ -171,7 +179,8 @@ jsString str = text (show str)
 keywords : List String
 keywords = [
  "var", "true", "false", "let", "case", "switch", "if", "then", "else", "String",
-  "function", "void", "undefined", "null", "await", "async", "return", "const"
+  "function", "void", "undefined", "null", "await", "async", "return", "const",
+  "Number"
 ]

 ||| escape identifiers for js
@@ -293,7 +302,7 @@ process (done,docs) nm = do
  where
    walkTm : Tm -> (List String, List Doc) -> M (List String, List Doc)
    walkAlt : (List String, List Doc) -> CaseAlt -> M (List String, List Doc)
-    walkAlt acc (CaseDefault t) = pure acc
+    walkAlt acc (CaseDefault t) = walkTm t acc
    walkAlt acc (CaseCons name args t) = walkTm t acc
    walkAlt acc (CaseLit lit t) = walkTm t acc

--- a/src/Lib/CompileExp.idr
+++ b/src/Lib/CompileExp.idr
@@ -1,6 +1,9 @@
 ||| First pass of compilation
 ||| - work out arities and fully apply functions / constructors (currying)
-||| - expand metas
+|||     currying is problemmatic because we need to insert lambdas (η-expand) and
+|||     it breaks all of the de Bruijn indices
+||| - expand metas (this is happening earlier)
+||| - erase stuff (there is another copy that essentially does the same thing)
 ||| I could make names unique (e.q. on lambdas), but I might want that to vary per backend?
 module Lib.CompileExp

@@ -27,7 +30,9 @@ data CExp : Type where
  CBnd : Nat -> CExp
  CLam : Name -> CExp -> CExp
  CFun : List Name -> CExp -> CExp
-  CApp : CExp -> List CExp -> CExp
+  -- REVIEW This feels like a hack, but if we put CLam here, the
+  -- deBruijn gets messed up in code gen
+  CApp : CExp -> List CExp -> Nat -> CExp
  -- TODO make DCon/TCon app separate so we can specialize
  -- U / Pi are compiled to type constructors
  CCase : CExp -> List CAlt -> CExp
@@ -71,19 +76,21 @@ compileTerm : Tm -> M CExp
 -- need to eta out extra args, fill in the rest of the apps
 apply : CExp -> List CExp -> SnocList CExp -> Nat -> Tm -> M CExp
 -- out of args, make one up (fix that last arg)
-apply t [] acc (S k) ty = pure $
-  CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k ty)
+apply t [] acc (S k) ty = pure $ CApp t (acc <>> []) (S k)
+  -- inserting Clam, index wrong?
+  -- CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k ty)
 apply t (x :: xs) acc (S k) (Pi y str icit Zero a b) =  apply t xs (acc :< CErased) k b
 apply t (x :: xs) acc (S k) (Pi y str icit Many a b) =  apply t xs (acc :< x) k b
 -- see if there is anything we have to handle here
-apply t (x :: xs) acc (S k) ty = error (getFC ty) "Expected pi \{showTm ty}"
-apply t ts acc 0 ty = go (CApp t (acc <>> [])) ts
+apply t (x :: xs) acc (S k) ty = error (getFC ty) "Expected pi \{showTm ty}. Overapplied function that escaped type checking?"
+-- once we hit zero, we fold the rest
+apply t ts acc 0 ty = go (CApp t (acc <>> []) Z) ts
  where
    go : CExp -> List CExp -> M CExp
    -- drop zero arg call
-    go (CApp t []) args = go t args
+    go (CApp t [] Z) args = go t args
    go t [] = pure t
-    go t (arg :: args) = go (CApp t [arg]) args
+    go t (arg :: args) = go (CApp t [arg] 0) args

 -- apply : CExp -> List CExp -> SnocList CExp -> Nat -> M CExp
 -- -- out of args, make one up
@@ -111,7 +118,7 @@ compileTerm (Lam _ nm t) = pure $ CLam nm !(compileTerm t)
 compileTerm tm@(App _ _ _) with (funArgs tm)
  _ | (Meta _ k, args) = do
        -- this will be undefined, should only happen for use metas
-        pure $ CApp (CRef "Meta\{show k}") []
+        pure $ CApp (CRef "Meta\{show k}") [] Z
  _ | (t@(Ref fc nm _), args) = do
        args' <- traverse compileTerm args
        arity <- arityForName fc nm
@@ -126,7 +133,7 @@ compileTerm tm@(App _ _ _) with (funArgs tm)
        apply t' args' [<] 0 (U emptyFC)
        -- error (getFC t) "Don't know how to apply \{showTm t}"
 compileTerm (U _) = pure $ CRef "U"
-compileTerm (Pi _ nm icit rig t u) = pure $ CApp (CRef "PiType") [ !(compileTerm t), CLam nm !(compileTerm u)]
+compileTerm (Pi _ nm icit rig t u) = pure $ CApp (CRef "PiType") [ !(compileTerm t), CLam nm !(compileTerm u)] Z
 compileTerm (Case _ t alts) = do
  t' <- compileTerm t
  alts' <- traverse (\case
@@ -137,6 +144,7 @@ compileTerm (Case _ t alts) = do
 compileTerm (Lit _ lit) = pure $ CLit lit
 compileTerm (Let _ nm t u) = pure $ CLet nm !(compileTerm t) !(compileTerm u)
 compileTerm (LetRec _ nm t u) = pure $ CLetRec nm !(compileTerm t) !(compileTerm u)
+compileTerm (Erased _) = pure CErased

 export
 compileFun : Tm -> M CExp
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -175,6 +175,7 @@ rename meta ren lvl v = go ren lvl v
    go ren lvl (VLam fc n t) = pure (Lam fc n !(go (lvl :: ren) (S lvl) !(t $$ VVar fc lvl [<])))
    go ren lvl (VPi fc n icit rig ty tm) = pure (Pi fc n icit rig !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<])))
    go ren lvl (VU fc) = pure (U fc)
+    go ren lvl (VErased fc) = pure (Erased fc)
    -- for now, we don't do solutions with case in them.
    go ren lvl (VCase fc sc alts) = error fc "Case in solution"
    go ren lvl (VLit fc lit) = pure (Lit fc lit)
@@ -379,7 +380,6 @@ insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val)
 insert ctx tm ty = do
  case !(forceMeta ty) of
    VPi fc x Auto rig a b => do
-      -- FIXME mark meta as auto, maybe try to solve here?
      m <- freshMeta ctx (getFC tm) a AutoSolve
      debug "INSERT Auto \{pprint (names ctx) m} : \{show a}"
      debug "TM \{pprint (names ctx) tm}"
@@ -528,14 +528,6 @@ updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus`
    replaceV 0 x (y :: xs) = x :: xs
    replaceV (S k) x (y :: xs) = y :: replaceV k x xs

-forcedName : Context -> String -> Maybe Name
-forcedName ctx nm = case lookupName ctx nm of
-  Just (Bnd fc ix, ty) => case getAt ix ctx.env of
-    (Just (VRef x nm y sp)) => -- TODO verify is constructor?
-      Just nm
-    _ => Nothing
-  _ => Nothing
-
 -- ok, so this is a single constructor, CaseAlt
 -- return Nothing if dcon doesn't unify with scrut
 buildCase : Context -> Problem -> String -> Val -> (String, Nat, Tm) -> M (Maybe CaseAlt)
@@ -1000,7 +992,8 @@ infer ctx (RVar fc nm) = go 0 ctx.types
      Nothing => error fc "\{show nm} not in scope"
    go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd fc i, ty)
      else go (i + 1) xs
-  -- need environment of name -> type..
+-- FIXME tightens up output but hardcodes a name
+-- infer ctx (RApp fc (RVar _ "_$_") u icit) = infer ctx u
 infer ctx (RApp fc t u icit) = do
  -- If the app is explicit, add any necessary metas
  (icit, t, tty) <- case the Icit icit of
--- a/src/Lib/Erasure.idr
+++ b/src/Lib/Erasure.idr
@@ -0,0 +1,92 @@
+module Lib.Erasure
+
+import Lib.Types
+import Data.SnocList
+import Lib.TopContext
+
+EEnv = List (String, Quant)
+
+-- check App at type
+
+getType : Tm -> M (Maybe Tm)
+getType (Ref fc nm x) = do
+  top <- get
+  case lookup nm top of
+    Nothing => pure Nothing
+    (Just (MkEntry name type def)) => pure $ Just type
+getType tm = pure Nothing
+
+export
+erase : EEnv -> Tm -> List (FC, Tm) -> M Tm
+
+-- App a spine using type
+eraseSpine : EEnv -> Tm -> List (FC, Tm) -> Maybe Tm -> M Tm
+eraseSpine env tm [] _ = pure tm
+eraseSpine env t ((fc, arg) :: args) (Just (Pi fc1 str icit Zero a b)) = do
+  let u = Erased (getFC arg)
+  eraseSpine env (App fc t u) args (Just b)
+eraseSpine env t ((fc, arg) :: args) (Just (Pi fc1 str icit Many a b)) = do
+  u <- erase env arg []
+  eraseSpine env (App fc t u) args (Just b)
+eraseSpine env t ((fc, arg) :: args) _ = do
+  u <- erase env arg []
+  eraseSpine env (App fc t u) args Nothing
+
+doAlt : EEnv -> CaseAlt -> M CaseAlt
+-- REVIEW do we extend env?
+doAlt env (CaseDefault t) = CaseDefault <$> erase env t []
+doAlt env (CaseCons name args t) = do
+  top <- get
+  let Just (MkEntry str type def) = lookup name top
+    | _ => error emptyFC "\{name} dcon missing from context"
+  let env' = piEnv env type args
+  CaseCons name args <$> erase env' t []
+  where
+    piEnv : EEnv -> Tm -> List String -> EEnv
+    piEnv env (Pi fc nm icit rig t u) (arg :: args) = piEnv ((arg,rig) :: env) u args
+    piEnv env _ _ = env
+
+doAlt env (CaseLit lit t) = CaseLit lit <$> erase env t []
+
+-- Check erasure and insert "Erased" value
+-- We have a solution for Erased values, so important thing here is checking.
+-- build stack, see what to do when we hit a non-app
+erase env t sp = case t of
+  (App fc u v) => erase env u ((fc,v) :: sp)
+  (Ref fc nm x) => do
+    top <- get
+    case lookup nm top of
+      Nothing => eraseSpine env t sp Nothing
+      (Just (MkEntry name type def)) => eraseSpine env t sp (Just type)
+  (Lam fc nm u) => Lam fc nm <$> erase ((nm, Many) :: env) u []
+  -- If we get here, we're looking at a runtime pi type
+  (Pi fc nm icit rig u v) => do
+    u' <- erase env u []
+    v' <- erase ((nm, Many) :: env) v []
+    eraseSpine env (Pi fc nm icit rig u' v') sp Nothing
+  -- leaving as-is for now, we don't know the quantity of the apps
+  (Meta fc k) => pure t
+  (Case fc u alts) => do
+    -- REVIEW check if this pushes to env, and write that down or get an index on there
+    u' <- erase env u []
+    alts' <- traverse (doAlt env) alts
+    eraseSpine env (Case fc u' alts') sp Nothing
+  (Let fc nm u v) => do
+    u' <- erase env u []
+    v' <- erase ((nm, Many) :: env) v []
+    eraseSpine env (Let fc nm u' v') sp Nothing
+  (LetRec fc nm u v) => do
+    u' <- erase ((nm, Many) :: env) u []
+    v' <- erase ((nm, Many) :: env) v []
+    eraseSpine env (LetRec fc nm u' v') sp Nothing
+  (Bnd fc k) => do
+    case getAt k env of
+      Nothing => error fc "bad index \{show k}"
+      -- This is working, but empty FC
+      Just (nm, Zero) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)"
+      Just (nm, Many) => eraseSpine env t sp Nothing
+  (U fc) => eraseSpine env t sp Nothing
+  (Lit fc lit) => eraseSpine env t sp Nothing
+  Erased fc => eraseSpine env t sp Nothing
+
+
--- a/src/Lib/Eval.idr
+++ b/src/Lib/Eval.idr
@@ -145,6 +145,7 @@ bind v env = v :: env
 eval env mode (Ref fc x def) = pure $ VRef fc x def [<]
 eval env mode (App _ t u) = vapp !(eval env mode t) !(eval env mode u)
 eval env mode (U fc) = pure (VU fc)
+eval env mode (Erased fc) = pure (VErased fc)
 eval env mode (Meta fc i) =
  case !(lookupMeta i) of
        (Unsolved _ k xs _ _ _) => pure $ VMeta fc i [<]
@@ -179,7 +180,7 @@ quoteSp lvl t (xs :< x) =
  pure $ App emptyFC !(quoteSp lvl t xs) !(quote lvl x)

 quote l (VVar fc k sp) = if k < l
-  then quoteSp l (Bnd emptyFC ((l `minus` k) `minus` 1)) sp -- level to index
+  then quoteSp l (Bnd fc ((l `minus` k) `minus` 1)) sp -- level to index
  else ?borken
 quote l (VMeta fc i sp) =
  case !(lookupMeta i) of
@@ -193,6 +194,7 @@ quote l (VU fc) = pure (U fc)
 quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp
 quote l (VCase fc sc alts) = pure $ Case fc !(quote l sc) alts
 quote l (VLit fc lit) = pure $ Lit fc lit
+quote l (VErased fc) = pure $ Erased fc

 -- Can we assume closed terms?
 -- ezoo only seems to use it at [], but essentially does this:
@@ -234,6 +236,23 @@ appSpine : Tm -> List Tm -> Tm
 appSpine t [] = t
 appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs

+-- REVIEW When metas are subst in, the fc point elsewhere
+-- We might want to update when it is solved and update recursively?
+-- For errors, I think we want to pretend the code has been typed in place
+tweakFC : FC -> Tm -> Tm
+tweakFC fc (Bnd fc1 k) = Bnd fc k
+tweakFC fc (Ref fc1 nm x) = Ref fc nm x
+tweakFC fc (U fc1) = U fc
+tweakFC fc (Meta fc1 k) = Meta fc k
+tweakFC fc (Lam fc1 nm t) = Lam fc nm t
+tweakFC fc (App fc1 t u) = App fc t u
+tweakFC fc (Pi fc1 nm icit x t u) = Pi fc nm icit x t u
+tweakFC fc (Case fc1 t xs) = Case fc t xs
+tweakFC fc (Let fc1 nm t u) = Let fc nm t u
+tweakFC fc (LetRec fc1 nm t u) = LetRec fc nm t u
+tweakFC fc (Lit fc1 lit) = Lit fc lit
+tweakFC fc (Erased fc1) = Erased fc
+
 -- TODO replace this with a variant on nf
 zonkApp : TopContext -> Nat -> Env -> Tm -> List Tm -> M Tm
 zonkApp top l env (App fc t u) sp = zonkApp top l env t (!(zonk top l env u) :: sp)
@@ -243,7 +262,8 @@ zonkApp top l env t@(Meta fc k) sp = case !(lookupMeta k) of
    debug "zonk \{show k} -> \{show v} spine \{show sp'}"
    foo <- vappSpine v ([<] <>< sp')
    debug "-> result is \{show foo}"
-    quote l foo
+    tweakFC fc <$> quote l foo
+
  (Unsolved x j xs _ _ _) => pure $ appSpine t sp
 zonkApp top l env t sp = pure $ appSpine !(zonk top l env t) sp

@@ -268,3 +288,4 @@ zonk top l env t = case t of
  Lit fc lit => pure $ Lit fc lit
  Bnd fc ix => pure $ Bnd fc ix
  Ref fc ix def => pure $ Ref fc ix def
+  Erased fc => pure $ Erased fc
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -111,8 +111,8 @@ pratt ops prec stop left spine = do
            else
              runRule p fix stop rule (RApp fc (RVar fc name) left Explicit) rest
          Just _ => fail "expected operator"
-          Nothing => pratt ops prec stop (RApp fc left tm Explicit) rest
-    ((icit, fc, tm) :: rest) => pratt ops prec stop (RApp fc left tm icit) rest
+          Nothing => pratt ops prec stop (RApp (getFC left) left tm Explicit) rest
+    ((icit, fc, tm) :: rest) => pratt ops prec stop (RApp (getFC left) left tm icit) rest
  where
    runRule : Int -> Fixity -> String -> List String -> Raw -> AppSpine -> Parser (Raw,AppSpine)
    runRule p fix stop [] left spine = pure (left,spine)
@@ -121,7 +121,7 @@ pratt ops prec stop left spine = do
      case spine of
                ((_, fc, right) :: rest) => do
                  (right, rest) <- pratt ops pr stop right rest
-                  pratt ops prec stop (RApp fc left right Explicit) rest
+                  pratt ops prec stop (RApp (getFC left) left right Explicit) rest
                _ => fail "trailing operator"

    runRule p fix stop (nm :: rule) left spine = do
@@ -131,7 +131,7 @@ pratt ops prec stop left spine = do
        | _ => fail "expected \{nm}"

      if name == nm
-          then runRule p fix stop rule (RApp fc left right Explicit) rest
+          then runRule p fix stop rule (RApp (getFC left) left right Explicit) rest
          else fail "expected \{nm}"


@@ -257,8 +257,9 @@ term =  caseExpr
    <|> letExpr
    <|> lamExpr
    <|> doExpr
-    <|> parseOp
    <|> ifThenElse
+    -- Make this last for better error messages
+    <|> parseOp

 varname : Parser String
 varname = (ident <|> uident <|> keyword "_" *> pure "_")
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -13,6 +13,7 @@ import Lib.TopContext
 import Lib.Eval
 import Lib.Types
 import Lib.Util
+import Lib.Erasure

 -- Check that the arguments are not explicit and the type constructor in codomain matches
 -- Later we will build a table of codomain type, and maybe make the user tag the candidates
@@ -223,6 +224,12 @@ processDecl (Def fc nm clauses) = do
  -- tm' <- nf [] tm
  tm' <- zonk top 0 [] tm
  putStrLn "NF\n\{render 80 $ pprint[] tm'}"
+  -- TODO we want to keep both versions, but this is checking in addition to erasing
+  -- currently CompileExp is also doing erasure.
+  -- TODO we need erasure info on the lambdas or to fake up an appropriate environment
+  -- and erase inside. Currently the checking is imprecise
+  tm'' <- erase [] tm' []
+  putStrLn "ERASED\n\{render 80 $ pprint[] tm'}"
  debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}"
  updateDef nm fc ty (Fn tm')
  -- logMetas mstart
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -127,6 +127,7 @@ data Tm : Type where
  -- for desugaring where
  LetRec : FC -> Name -> Tm -> Tm -> Tm
  Lit : FC -> Literal -> Tm
+  Erased : FC -> Tm

 %name Tm t, u, v

@@ -143,6 +144,7 @@ HasFC Tm where
  getFC (Lit fc _) = fc
  getFC (Let fc _ _ _) = fc
  getFC (LetRec fc _ _ _) = fc
+  getFC (Erased fc) = fc

 covering
 Show Tm
@@ -168,6 +170,7 @@ Show Tm where
  show (Case _ sc alts) = "(Case \{show sc} \{show alts})"
  show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})"
  show (LetRec _ nm t u) = "(LetRec \{nm} \{show t} \{show u})"
+  show (Erased _) = "ERASED"

 public export
 showTm : Tm -> String
@@ -242,7 +245,7 @@ pprint names tm = go 0 names tm
    go p names (Lit _ lit) = text (show lit)
    go p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> ":=" <+> go 0 names t <+> "in" </> (nest 2 $ go 0 (nm :: names) u)
    go p names (LetRec _ nm t u) = parens 0 p $ text "letrec" <+> text nm <+> ":=" <+> go 0 names t <+> "in" </> (nest 2 $ go 0 (nm :: names) u)
-
+    go p names (Erased _) = "ERASED"
 data Val : Type


@@ -276,6 +279,7 @@ data Val : Type where
  VLet : FC -> Name -> Val -> Val -> Val
  VLetRec : FC -> Name -> Val -> Val -> Val
  VU : FC -> Val
+  VErased : FC -> Val
  VLit : FC -> Literal -> Val

 public export
@@ -287,6 +291,7 @@ getValFC (VMeta fc _ _) = fc
 getValFC (VLam fc _ _) = fc
 getValFC (VPi fc _ _ _ a b) = fc
 getValFC (VU fc) = fc
+getValFC (VErased fc) = fc
 getValFC (VLit fc _) = fc
 getValFC (VLet fc _ _ _) = fc
 getValFC (VLetRec fc _ _ _) = fc
@@ -312,6 +317,7 @@ Show Val where
  show (VLit _ lit) = show lit
  show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}"
  show (VLetRec _ nm a b) = "(%letrec \{show nm} = \{show a} in \{show b}"
+  show (VErased _) = "ERASED"

 public export
 Env : Type
@@ -521,7 +527,7 @@ freshMeta ctx fc ty kind = do
  mc <- readIORef top.metas
  debug "fresh meta \{show mc.next} : \{show ty}"
  writeIORef top.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind [] ::) } mc
-  pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds
+  pure $ applyBDs 0 (Meta fc mc.next) ctx.bds
  where
    -- hope I got the right order here :)
    applyBDs : Nat -> Tm -> Vect k BD -> Tm