From 8209d2d839b4b3b26e70f8680ac1ef7fc1d8ef63 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 4 Oct 2025 14:41:48 -0700
Subject: [PATCH] Use numbers for constructor tags.

---
 TODO.md                  | 21 +++++++++++++-----
 src/Lib/Compile.newt     | 14 ++++++------
 src/Lib/CompileExp.newt  | 47 ++++++++++++++++++++--------------------
 src/Lib/Elab.newt        |  8 +++----
 src/Lib/Eval.newt        |  2 +-
 src/Lib/ProcessDecl.newt | 18 +++++++--------
 src/Lib/TCO.newt         | 32 +++++++++++++++------------
 src/Lib/Types.newt       |  4 ++--
 src/Main.newt            |  2 +-
 src/Prelude.newt         |  8 +++----
 10 files changed, 86 insertions(+), 70 deletions(-)

diff --git a/TODO.md b/TODO.md
index 701cee3..912e40d 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,11 +1,20 @@
 
 ## TODO
 
+- [ ] Add info to Ref/VRef (is dcon, arity, etc)
+  - To save lookups during compilation and it might make eval faster
+- [x] number tags for data constructors
+  - Numeric tags are about 9% faster
+  - Issues:
+    - They make debugging more difficult. I was able to sort out debruijn issues because the names were wrong.
+    - There are a couple of spots I have to fudge in the native code, because there is no constant for `Nil` and `_::_` tags
+    - the debugString pretty printer was leveraging the names
 - [x] Increment row/col in printing, so vscode can click on compiler output
 - [ ] Raw is duplicated between Lib.Syntax and Lib.Compile, but not detected
-  - Maybe add qualified names
+  - [ ] Maybe add qualified names to surface syntax and allow / detect conflicts on reference
+  - [ ] Add `export` keywords
 - [ ] vscode - run newt when switching editors
-- [ ] who calls X?  We can only do this scoped to the current context for now. Someday whole source dir
+- [ ] who calls X?  We can only do this scoped to the current context for now. Someday whole source dir.
 - [ ] case split
   - We could fake this up:
     - given a name and a point in the editor
@@ -14,10 +23,12 @@
     - enumerate valid constructors (and their arity)
     - Repeat the line with each, applied to args
     - For `<-` or `let` we'd want to fudge some `|` lines
-- [ ] inline struct getters during code generation (We'd like  `x.h1.h2`)
-- [ ] Better FC for parse errors (both EOF and the ones that show up just after the error)
 - [ ] Support "Add missing cases"
-- [ ] Code gen for PiType (rather than static JS)
+    - We could possibly fake up missing cases, too. Since they're listed and have an FC pointing at the first one
+    - [ ] Might need proper, enumerated errors for that
+- [x] inline struct getters during code generation (We'd like  `x.h1.h2`)
+- [ ] Better FC for parse errors (both EOF and the ones that show up just after the error)
+- [x] Code gen for PiType (rather than static JS)
 - [x] fix string highlighting
 - [x] implement tail call optimization
 - [x] implement magic nat
diff --git a/src/Lib/Compile.newt b/src/Lib/Compile.newt
index dfaefaf..bd900c9 100644
--- a/src/Lib/Compile.newt
+++ b/src/Lib/Compile.newt
@@ -25,7 +25,7 @@ JSStmt : StKind -> U
 JSExp : U
 
 data JAlt : U where
-  JConAlt : ∀ e. String -> JSStmt e -> JAlt
+  JConAlt : ∀ e. Nat -> JSStmt e -> JAlt
   JDefAlt : ∀ e. JSStmt e -> JAlt
   JLitAlt : ∀ e. JSExp -> JSStmt e -> JAlt
 
@@ -172,7 +172,7 @@ termToJS env (CLetRec nm t u) f =
   in case termToJS env' t (JAssign nm') of
     (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f)
     t' => JSnoc (JLet nm' t') (termToJS env' u f)
-termToJS env (CConstr nm args) f = go args 0 (\ args => f $ LitObject (("tag", LitString nm) :: args))
+termToJS env (CConstr ix _ args) f = go args 0 (\ args => f $ LitObject (("tag", LitInt (cast ix)) :: args))
   where
     go : ∀ e. List CExp -> Int -> (List (String × JSExp) -> JSStmt e) -> JSStmt e
     go Nil ix k = k Nil
@@ -207,14 +207,14 @@ termToJS {e} env (CCase t alts) f =
         else JSnoc (JConst nm t') (maybeCaseStmt env' (Var nm) alts)
   where
     termToJSAlt : JSEnv -> JSExp -> CAlt -> JAlt
-    termToJSAlt env nm (CConAlt name info args u) = JConAlt name (termToJS (mkEnv nm 0 env args) u f)
+    termToJSAlt env nm (CConAlt ix name info args u) = JConAlt ix (termToJS (mkEnv nm 0 env args) u f)
     -- intentionally reusing scrutinee name here
     termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS  (env) u f)
     termToJSAlt env nm (CLitAlt lit u) = JLitAlt (litToJS lit) (termToJS env u f)
 
     maybeCaseStmt : JSEnv -> JSExp -> List CAlt -> JSStmt e
     -- If there is a single alt, assume it matched
-    maybeCaseStmt env nm ((CConAlt _ info args u) :: Nil) = (termToJS (mkEnv nm 0 env args) u f)
+    maybeCaseStmt env nm ((CConAlt _ _ info args u) :: Nil) = (termToJS (mkEnv nm 0 env args) u f)
     maybeCaseStmt env nm alts@(CLitAlt _ _  :: _) =
         (JCase nm (map (termToJSAlt env nm) alts))
     maybeCaseStmt env nm alts =
@@ -278,7 +278,7 @@ caseBody {e} stmt@(JCase _ _) = nest 2 (line ++ stmtToDoc stmt </> text "break;"
 caseBody stmt = line ++ text "{" ++ nest 2 (line ++ stmtToDoc stmt </> text "break;") </> text "}"
 
 altToDoc : JAlt -> Doc
-altToDoc (JConAlt nm stmt) = text "case" <+> text (quoteString nm) ++ text ":" ++ caseBody stmt
+altToDoc (JConAlt nm stmt) = text "case" <+> text (show nm) ++ text ":" ++ caseBody stmt
 altToDoc (JDefAlt stmt) = text "default" ++ text ":" ++ caseBody stmt
 altToDoc (JLitAlt a stmt) = text "case" <+> expToDoc a ++ text ":" ++ caseBody stmt
 
@@ -374,7 +374,7 @@ sortedNames : SortedMap QName CExp → QName → List QName
 sortedNames defs qn = map snd $ filter (not ∘ fst) $ go Nil Nil (True, qn)
   where
     getBody : CAlt → CExp
-    getBody (CConAlt _ _ _ t) = t
+    getBody (CConAlt _ _ _ _ t) = t
     getBody (CLitAlt _ t) = t
     getBody (CDefAlt t) = t
 
@@ -398,7 +398,7 @@ sortedNames defs qn = map snd $ filter (not ∘ fst) $ go Nil Nil (True, qn)
     getNames deep acc (CRef qn) = (deep, qn) :: acc
     getNames deep acc (CLet _ t u) = getNames deep (getNames deep acc t) u
     getNames deep acc (CLetRec _ t u) = getNames deep (getNames deep acc t) u
-    getNames deep acc (CConstr _ ts) = foldl (getNames deep) acc ts
+    getNames deep acc (CConstr _ _ ts) = foldl (getNames deep) acc ts
     -- if the CRaw is called, then the deps are called
     getNames deep acc (CRaw _ deps) = map (_,_ deep) deps ++ acc
     -- wrote these out so I get an error when I add a new constructor
diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt
index 54e72fb..314ce53 100644
--- a/src/Lib/CompileExp.newt
+++ b/src/Lib/CompileExp.newt
@@ -17,7 +17,7 @@ import Data.SortedMap
 CExp : U
 
 data CAlt : U where
-  CConAlt : String → ConInfo → List String → CExp → CAlt
+  CConAlt : Nat → String → ConInfo → List String → CExp → CAlt
   -- REVIEW keep var name?
   CDefAlt : CExp -> CAlt
   -- literal
@@ -38,7 +38,7 @@ data CExp : U where
   CLetRec : Name -> CExp -> CExp -> CExp
   CErased : CExp
   -- Data / type constructor
-  CConstr : Name -> List CExp -> CExp
+  CConstr : Nat → Name -> List CExp -> CExp
   -- Raw javascript for `pfunc`
   CRaw : String -> List QName -> CExp
   -- Need this for magic Nat
@@ -70,7 +70,7 @@ arityForName fc nm = do
     Nothing => error fc "Name \{show nm} not in scope"
     (Just Axiom) => pure Z
     (Just (TCon arity strs)) => pure $ cast arity
-    (Just (DCon _ k str)) => pure $ cast k
+    (Just (DCon _ _ k str)) => pure $ cast k
     (Just (Fn t)) => pure $ lamArity t
     (Just (PrimTCon arity)) => pure $ cast arity
     (Just (PrimFn t arity used)) => pure arity
@@ -115,9 +115,9 @@ compileTerm t@(Ref fc nm@(QN _ tag)) = do
     (S Z) => pure $ CRef nm
     Z =>
       case the (Maybe Def) $ lookupMap' nm defs of
-        Just (DCon EnumCon _ _) => pure $ CLit $ LString tag
-        Just (DCon ZeroCon _ _) => pure $ CLit $ LInt 0
-        Just (DCon SuccCon _ _) =>
+        Just (DCon ix EnumCon _ _) => pure $ CLit $ LInt $ cast ix
+        Just (DCon _ ZeroCon _ _) => pure $ CLit $ LInt 0
+        Just (DCon _ SuccCon _ _) =>
           pure $ CLam "x" $ CPrimOp "+" (CLit $ LInt 1) (CBnd 0)
         _ => pure $ CRef nm
     _ => apply nm Nil Lin arity
@@ -136,7 +136,7 @@ compileTerm tm@(App _ _ _) = case funArgs tm of
         let (Nothing) = compilePrimOp (show nm) args'
           | Just cexp => pure cexp
         case the (Maybe Def) $ lookupMap' nm defs of
-          Just (DCon SuccCon _ _) => applySucc args'
+          Just (DCon _ SuccCon _ _) => applySucc args'
           _ => apply nm args' Lin arity
   -- REVIEW maybe we want a different constructor for non-Ref applications?
   (t, args) => do
@@ -163,23 +163,23 @@ compileTerm (Case fc t alts) = do
       defs <- getRef Defs
       def <- lookupDef emptyFC qn
       case def of
-        DCon info _ _ => CConAlt nm info args <$> compileTerm tm
+        DCon ix info _ _ => CConAlt ix nm info args <$> compileTerm tm
         _ => error fc "\{show nm} is not constructor"
 
     CaseLit lit tm => CLitAlt lit <$> compileTerm tm
   pure $ CCase t' $ fancyCons t' alts'
   where
     numAltP : CAlt → Bool
-    numAltP (CConAlt _ SuccCon _ _) = True
-    numAltP (CConAlt _ ZeroCon _ _) = True
+    numAltP (CConAlt _ _ SuccCon _ _) = True
+    numAltP (CConAlt _ _ ZeroCon _ _) = True
     numAltP _ = False
 
     enumAlt : CAlt → CAlt
-    enumAlt (CConAlt nm EnumCon args tm) = CLitAlt (LString nm) tm
+    enumAlt (CConAlt ix nm EnumCon args tm) = CLitAlt (LInt $ cast ix) tm
     enumAlt alt = alt
 
     isInfo : ConInfo → CAlt → Bool
-    isInfo needle (CConAlt _ info _ _)  = needle == info
+    isInfo needle (CConAlt _ _  info _ _)  = needle == info
     isInfo _ _ = False
 
     isDef : CAlt → Bool
@@ -187,14 +187,14 @@ compileTerm (Case fc t alts) = do
     isDef _ = False
 
     getBody : CAlt → CExp
-    getBody (CConAlt _ _ _ t) = t
+    getBody (CConAlt _ _ _ _ t) = t
     getBody (CLitAlt _ t) = t
     getBody (CDefAlt t) = t
 
     doNumCon : CExp → List CAlt → List CAlt
     doNumCon sc alts =
       let zeroAlt = case find (isInfo ZeroCon) alts of
-            Just (CConAlt _ _ _ tm) => CLitAlt (LInt 0) tm :: Nil
+            Just (CConAlt _ _ _ _ tm) => CLitAlt (LInt 0) tm :: Nil
             Just tm => fatalError "ERROR zeroAlt mismatch \{debugStr tm}"
             _ => case find isDef alts of
                   Just (CDefAlt tm) => CLitAlt (LInt 0) tm :: Nil
@@ -202,7 +202,7 @@ compileTerm (Case fc t alts) = do
                   _ => Nil
       in
       let succAlt = case find (isInfo SuccCon) alts of
-            Just (CConAlt _ _ _ tm) => CDefAlt (CLet "x" (CPrimOp "-" sc (CLit $ LInt 1)) tm) :: Nil
+            Just (CConAlt _ _ _ _ tm) => CDefAlt (CLet "x" (CPrimOp "-" sc (CLit $ LInt 1)) tm) :: Nil
             Just tm => fatalError "ERROR succAlt mismatch \{debugStr tm}"
             _ => case find isDef alts of
               Just alt => alt :: Nil
@@ -235,18 +235,19 @@ compileFun tm = go tm Lin
     go tm args = CFun (args <>> Nil) <$> compileTerm tm
 
 -- What are the Defs used for above? (Arity for name)
-compileDCon : QName → ConInfo → Int → CExp
-compileDCon (QN _ nm) EnumCon 0 = CLit $ LString nm
-compileDCon (QN _ nm) info 0 = CConstr nm Nil
-compileDCon (QN _ nm) info arity =
+compileDCon : Nat → QName → ConInfo → Int → CExp
+compileDCon ix (QN _ nm) EnumCon 0 = CLit $ LInt $ cast ix
+compileDCon ix (QN _ nm) info 0 = CConstr ix nm Nil
+compileDCon ix (QN _ nm) info arity =
   let args = map (\k => "h\{show k}") (range 0 arity) in
-  CFun args $ CConstr nm $ map (\k => CBnd $ arity - k - 1) (range 0 arity)
+  CFun args $ CConstr ix nm $ map (\k => CBnd $ arity - k - 1) (range 0 arity)
 
 -- probably want to drop the Ref2 when we can
 defToCExp : {{Ref2 Defs St}} → (QName × Def) -> M (QName × CExp)
 defToCExp (qn, Axiom)          = pure $ (qn, CErased)
-defToCExp (qn, DCon info arity _)   = pure $ (qn, compileDCon qn info arity)
-defToCExp (qn, TCon arity _)   = pure $ (qn, compileDCon qn NormalCon arity)
-defToCExp (qn, PrimTCon arity) = pure $ (qn, compileDCon qn NormalCon arity)
+defToCExp (qn, DCon ix info arity _)   = pure $ (qn, compileDCon ix qn info arity)
+-- FIXME need a number if we ever add typecase.
+defToCExp (qn, TCon arity _)   = pure $ (qn, compileDCon Z qn NormalCon arity)
+defToCExp (qn, PrimTCon arity) = pure $ (qn, compileDCon Z qn NormalCon arity)
 defToCExp (qn, PrimFn src _ deps) = pure $ (qn, CRaw src deps)
 defToCExp (qn, Fn tm)          = (_,_ qn) <$> compileFun tm
diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt
index ac8e67f..9217cdd 100644
--- a/src/Lib/Elab.newt
+++ b/src/Lib/Elab.newt
@@ -727,7 +727,7 @@ getConstructors ctx scfc (VRef fc nm _) = do
     lookupDCon nm = do
       top <- getTop
       case lookup nm top of
-        (Just (MkEntry _ name type (DCon _ k str) _)) => pure (name, k, type)
+        (Just (MkEntry _ name type (DCon _ _ k str) _)) => pure (name, k, type)
         Just _ => error fc "Internal Error: \{show nm} is not a DCon"
         Nothing => error fc "Internal Error: DCon \{show nm} not found"
 getConstructors ctx scfc tm = do
@@ -964,7 +964,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
               -- TODO can we check this when we make the PatCon?
               top <- getTop
               case lookup nm top of
-                  (Just (MkEntry _ name type (DCon _ k tcname) _)) =>
+                  (Just (MkEntry _ name type (DCon _ _ k tcname) _)) =>
                     if (tcname /= sctynm)
                       then error fc "Constructor is \{show tcname} expected \{show sctynm}"
                       else pure Nothing
@@ -992,7 +992,7 @@ mkPat (tm, icit) = do
   top <- getTop
   case splitArgs tm Nil of
     ((RVar fc nm), b) => case lookupRaw nm top of
-                (Just (MkEntry _ name type (DCon _ k str) _)) => do
+                (Just (MkEntry _ name type (DCon _ _ k str) _)) => do
                   -- TODO check arity, also figure out why we need reverse
                   bpat <- traverse (mkPat) b
                   pure $ PatCon fc icit name bpat Nothing
@@ -1365,7 +1365,7 @@ updateRec ctx fc clauses arg ty = do
       let (Just (MkEntry _ _ _ (TCon _ (conname :: Nil)) _)) = lookup nm top
         | Just _ => error fc "\{show nm} is not a record"
         | _ => error fc "\{show nm} not in scope"
-      let (Just (MkEntry _ _ ty (DCon _ _ _) _)) = lookup conname top
+      let (Just (MkEntry _ _ ty (DCon _ _ _ _) _)) = lookup conname top
         | _ => error fc "\{show conname} not a dcon"
       pure $ (conname, collect arg ty)
     --
diff --git a/src/Lib/Eval.newt b/src/Lib/Eval.newt
index bd4162b..9e9b009 100644
--- a/src/Lib/Eval.newt
+++ b/src/Lib/Eval.newt
@@ -108,7 +108,7 @@ evalCase env sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do
       debug $ \ _ =>  "ECase \{show nm} \{show sp} \{show nms} \{showTm t}"
       pushArgs env (sp <>> Nil) nms
     else case lookup nm top of
-      (Just (MkEntry _ str type (DCon _ k str1) _)) => evalCase env sc xs
+      (Just (MkEntry _ str type (DCon _ _ k str1) _)) => evalCase env sc xs
       -- bail for a stuck function
       _ => pure Nothing
   where
diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt
index 8a6675b..81bee6c 100644
--- a/src/Lib/ProcessDecl.newt
+++ b/src/Lib/ProcessDecl.newt
@@ -296,7 +296,7 @@ processInstance ns instfc ty decls = do
     | _ => error tyFC "\{show tconName} is not a type constructor"
   let (con :: Nil) = cons
     | _ => error tyFC "\{show tconName} has multiple constructors \{show cons}"
-  let (Just (MkEntry _ _ dcty (DCon _ _ _) _)) = lookup con top
+  let (Just (MkEntry _ _ dcty (DCon _ _ _ _) _)) = lookup con top
     | _ => error tyFC "can't find constructor \{show con}"
   vdcty@(VPi _ nm icit rig a b) <- eval Nil dcty
     | x => error (getFC x) "dcty not Pi"
@@ -411,20 +411,20 @@ populateConInfo entries =
   setInfo zero ZeroCon :: setInfo succ SuccCon :: Nil
   where
     setInfo : TopEntry → ConInfo → TopEntry
-    setInfo (MkEntry fc nm dty (DCon _ arity hn) flags) info = MkEntry fc nm dty (DCon info arity hn) flags
+    setInfo (MkEntry fc nm dty (DCon ix _ arity hn) flags) info = MkEntry fc nm dty (DCon ix info arity hn) flags
     setInfo x _ = x
 
     checkEnum : TopEntry → Maybe TopEntry
-    checkEnum (MkEntry fc nm dty (DCon _ 0 hn) flags) = Just $ MkEntry fc nm dty (DCon EnumCon 0 hn) flags
+    checkEnum (MkEntry fc nm dty (DCon ix _ 0 hn) flags) = Just $ MkEntry fc nm dty (DCon ix EnumCon 0 hn) flags
     checkEnum _ = Nothing
 
     isZero : TopEntry → Bool
-    isZero (MkEntry fc nm dty (DCon _ 0 hn) flags) = True
+    isZero (MkEntry fc nm dty (DCon _ _ 0 hn) flags) = True
     isZero _ = False
 
     -- TODO - handle indexes, etc
     isSucc : TopEntry → Bool
-    isSucc (MkEntry fc nm dty@(Pi _ _ _ _ (Ref _ a) (Ref _ b)) (DCon _ 1 hn) _) = a == b
+    isSucc (MkEntry fc nm dty@(Pi _ _ _ _ (Ref _ a) (Ref _ b)) (DCon _ _ 1 hn) _) = a == b
     isSucc _ = False
 
 processData : List String → FC → String → Raw → List Decl → M Unit
@@ -441,8 +441,8 @@ processData ns fc nm ty cons = do
       unifyCatch fc (mkCtx fc) tyty' type'
     Just _ => error fc "\{show nm} already declared"
     Nothing => setDef (QN ns nm) fc tyty Axiom Nil
-  entries <- join <$> (for cons $ \x => case x of
-      (TypeSig fc names tm) => do
+  entries <- join <$> (for (enumerate cons) $ \x => case x of
+      (ix, TypeSig fc names tm) => do
           traverse (checkAlreadyDef fc) names
           debug $ \ _ => "check dcon \{show names} \{show tm}"
           dty <- check (mkCtx fc) tm (VU fc)
@@ -457,8 +457,8 @@ processData ns fc nm ty cons = do
             | (tm, _) => error (getFC tm) "expected \{nm} got \{render 90 $ pprint tnames tm}"
           when (hn /= QN ns nm) $ \ _ =>
             error (getFC codomain) "Constructor codomain is \{render 90 $ pprint tnames codomain} rather than \{nm}"
-          pure $ map (\ nm' => (MkEntry fc (QN ns nm') dty (DCon NormalCon (getArity dty) hn) Nil)) names
-      decl => throwError $ E (getFC decl) "expected constructor declaration")
+          pure $ map (\ nm' => (MkEntry fc (QN ns nm') dty (DCon ix NormalCon (getArity dty) hn) Nil)) names
+      (_,decl) => throwError $ E (getFC decl) "expected constructor declaration")
   -- type level autos like _++_
   solveAutos
   let entries = populateConInfo entries
diff --git a/src/Lib/TCO.newt b/src/Lib/TCO.newt
index fa85315..cb38e7d 100644
--- a/src/Lib/TCO.newt
+++ b/src/Lib/TCO.newt
@@ -23,12 +23,12 @@ tailNames (CAppRef nm args n) = nm :: Nil
 tailNames (CCase _ alts) = join $ map altTailNames alts
   where
     altTailNames : CAlt → List QName
-    altTailNames (CConAlt _ _ _ exp) = tailNames exp
+    altTailNames (CConAlt _ _ _ _ exp) = tailNames exp
     altTailNames (CDefAlt exp) = tailNames exp
     altTailNames (CLitAlt _ exp) = tailNames exp
 tailNames (CLet _ _ t) = tailNames t
 tailNames (CLetRec _ _ t) = tailNames t
-tailNames (CConstr _ args) = Nil
+tailNames (CConstr _ _ args) = Nil
 tailNames (CBnd _) = Nil
 tailNames (CFun _ tm) = tailNames tm
 tailNames (CLam _ _) = Nil
@@ -46,16 +46,20 @@ tailNames (CPrimOp _ _ _) = Nil
 rewriteTailCalls : List QName → CExp → CExp
 rewriteTailCalls nms tm = case tm of
   CAppRef nm args 0 =>
-      if elem nm nms
-        then CConstr (show nm) args
-        else CConstr "return" (tm :: Nil)
+      case getTag (S Z) nm nms of
+        Just ix => CConstr ix (show nm) args
+        Nothing => CConstr Z "return" (tm :: Nil)
   CLetRec nm t u => CLetRec nm t $ rewriteTailCalls nms u
   CLet nm t u => CLet nm t $ rewriteTailCalls nms u
   CCase sc alts => CCase sc $ map rewriteAlt alts
-  tm => CConstr "return" (tm :: Nil)
+  tm => CConstr Z "return" (tm :: Nil)
   where
+      getTag : Nat → QName → List QName → Maybe Nat
+      getTag t nm Nil = Nothing
+      getTag t nm (n :: ns) = if n == nm then Just t else getTag (S t) nm ns
+
       rewriteAlt : CAlt -> CAlt
-      rewriteAlt (CConAlt nm info args t) = CConAlt nm info args $ rewriteTailCalls nms t
+      rewriteAlt (CConAlt ix nm info args t) = CConAlt ix nm info args $ rewriteTailCalls nms t
       rewriteAlt (CDefAlt t) = CDefAlt $ rewriteTailCalls nms t
       rewriteAlt (CLitAlt lit t) = CLitAlt lit $ rewriteTailCalls nms t
 
@@ -67,16 +71,16 @@ doOptimize : List (QName × CExp) → M (List (QName × CExp))
 doOptimize fns = do
   splitFuns <- traverse splitFun fns
   let nms = map fst fns
-  let alts = map (mkAlt nms) splitFuns
+  let alts = map (mkAlt nms) $ enumerate splitFuns
   recName <- mkRecName nms
   let recfun = CFun ("arg" :: Nil) $ CCase (CBnd 0) alts
-  wrapped <- traverse (mkWrap recName) fns
+  wrapped <- traverse (mkWrap recName) (enumerate fns)
   pure $ (recName, recfun) :: wrapped
   where
-    mkWrap : QName → QName × CExp → M (QName × CExp)
-    mkWrap recName (qn, CFun args _) = do
+    mkWrap : QName → Nat × QName × CExp → M (QName × CExp)
+    mkWrap recName (ix, qn, CFun args _) = do
       let arglen = length' args
-      let arg = CConstr (show qn) $ map (\k => CBnd (arglen - k - 1)) (range 0 arglen)
+      let arg = CConstr (S ix) (show qn) $ map (\k => CBnd (arglen - k - 1)) (range 0 arglen)
       let body = CAppRef bouncer (CRef recName :: arg :: Nil) 0
       pure $ (qn, CFun args body)
     mkWrap _ (qn, _) = error emptyFC "error in mkWrap: \{show qn} not a CFun"
@@ -85,8 +89,8 @@ doOptimize fns = do
     mkRecName Nil = error emptyFC "INTERNAL ERROR: Empty List in doOptimize"
     mkRecName (QN ns nm :: _) = pure $ QN ns "REC_\{nm}"
 
-    mkAlt : List QName → (QName × List Name × CExp) -> CAlt
-    mkAlt nms (qn, args, tm) = CConAlt (show qn) NormalCon args (rewriteTailCalls nms tm)
+    mkAlt : List QName → (Nat × QName × List Name × CExp) -> CAlt
+    mkAlt nms (ix, qn, args, tm) = CConAlt (S ix) (show qn) NormalCon args (rewriteTailCalls nms tm)
 
     splitFun : (QName × CExp) → M (QName × List Name × CExp)
     splitFun (qn, CFun args body) = pure (qn, args, body)
diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt
index 6741266..797b2f4 100644
--- a/src/Lib/Types.newt
+++ b/src/Lib/Types.newt
@@ -352,13 +352,13 @@ instance Show ConInfo where
   show ZeroCon = "[Z]"
   show EnumCon = "[E]"
 
-data Def = Axiom | TCon Int (List QName) | DCon ConInfo Int QName | Fn Tm | PrimTCon Int
+data Def = Axiom | TCon Int (List QName) | DCon Nat ConInfo Int QName | Fn Tm | PrimTCon Int
          | PrimFn String Nat (List QName)
 
 instance Show Def where
   show Axiom = "axiom"
   show (TCon _ strs) = "TCon \{show strs}"
-  show (DCon ci k tyname) = "DCon \{show k} \{show tyname} \{show ci}"
+  show (DCon ix ci k tyname) = "DCon \{show ix} \{show k} \{show tyname} \{show ci}"
   show (Fn t) = "Fn \{show t}"
   show (PrimTCon _) = "PrimTCon"
   show (PrimFn src arity used) = "PrimFn \{show src} \{show arity} \{show used}"
diff --git a/src/Main.newt b/src/Main.newt
index d8bbf8f..83d691d 100644
--- a/src/Main.newt
+++ b/src/Main.newt
@@ -51,7 +51,7 @@ writeSource fn = do
   docs <- compile
   let src = unlines $
         ( "\"use strict\";"
-        :: "const bouncer = (f,ini) => { let obj = ini; while (obj.tag !== 'return') obj = f(obj); return obj.h0 };"
+        :: "const bouncer = (f,ini) => { let obj = ini; while (obj.tag) obj = f(obj); return obj.h0 };"
         :: Nil)
         ++ map (render 90 ∘ noAlt) docs
   (Right _) <- liftIO {M} $ writeFile fn src
diff --git a/src/Prelude.newt b/src/Prelude.newt
index b6a70b6..f8040af 100644
--- a/src/Prelude.newt
+++ b/src/Prelude.newt
@@ -283,7 +283,7 @@ ptype Array : U → U
 pfunc listToArray : ∀ a. List a → Array a := `
 (a, l) => {
   let rval = []
-  while (l.tag !== 'Nil') {
+  while (l.tag !== 'Nil' && l.tag) {
     rval.push(l.h1)
     l = l.h2
   }
@@ -409,7 +409,7 @@ pfunc unpack uses (Nil _::_) : String → List Char
 
 pfunc pack : List Char → String := `(cs) => {
   let rval = ''
-  while (cs.tag === '_::_') {
+  while (cs.tag === '_::_' || cs.tag === 1) {
     rval += cs.h1
     cs = cs.h2
   }
@@ -642,7 +642,7 @@ pfunc ioArrayToList uses (Nil _::_ MkIORes) : ∀ a. IOArray a → IO (List a) :
 
 pfunc listToIOArray uses (MkIORes) : ∀ a. List a → IO (Array a) := `(a,list) => w => {
   let rval = []
-  while (list.tag === '_::_') {
+  while (list.tag === '_::_' || list.tag === 1) {
     rval.push(list.h1)
     list = list.h2
   }
@@ -704,7 +704,7 @@ instance Eq Ordering where
   GT == GT = True
   _ == _ = False
 
-pfunc jsCompare : ∀ a. a → a → Ordering := `(_, a, b) => a == b ? "EQ" : a < b ? "LT" : "GT"`
+pfunc jsCompare uses (EQ LT GT) : ∀ a. a → a → Ordering := `(_, a, b) => a == b ? Prelude_EQ : a < b ? Prelude_LT : Prelude_GT`
 
 infixl 6 _<_ _<=_ _>_
 class Ord a where