diff --git a/TODO.md b/TODO.md
index 0be092b..d18d1f5 100644
--- a/TODO.md
+++ b/TODO.md
@@ -3,6 +3,10 @@
 
 More comments in code! This is getting big enough that I need to re-find my bearings when fixing stuff.
 
+- [ ] tokenizer
+- [ ] string interpolation
+- [ ] pattern matching lambda
+  - I kept wanting this in AoC and use it a lot in the newt code
 - [ ] editor - indent newline on let with no in
   - I've seen this done in vi for Idris, but it seems non-trivial in vscode.
 - [x] Move on to next decl in case of error
@@ -47,8 +51,9 @@ More comments in code! This is getting big enough that I need to re-find my bear
 - [ ] **Translate newt to newt**
   - [x] Support @ on the LHS
   - [x] if / then / else sugar
-  - [ ] `data Foo = A | B` sugar
+  - [x] `data Foo = A | B` sugar
   - [x] records
+  - [ ] record sugar? (detailed above)
   - [x] where
   - [ ] add namespaces
   - [ ] magic nat?
@@ -58,7 +63,7 @@ More comments in code! This is getting big enough that I need to re-find my bear
 - [x] Strategy to avoid three copies of `Prelude.newt` in this source tree
 - [ ] `mapM` needs inference help when scrutinee (see Day2.newt)
   - Meta hasn't been solved yet. It's Normal, but maybe our delayed solving of Auto plays into it. Idris will peek at LHS of CaseAlts to guess the type if it doesn't have one.
-- [ ] Can't skip an auto. We need `{{_}}` to be auto or `%search` syntax.
+- [ ] Can't skip an auto. We need `{{_}}` to be auto or have a `%search` syntax.
 - [x] add filenames to FC
 - [ ] Add full ranges to FC
 - [x] maybe use backtick for javascript so we don't highlight strings as JS
@@ -74,9 +79,6 @@ More comments in code! This is getting big enough that I need to re-find my bear
   - maybe a file listing jobs, whether they are known broken, optional expected output, optional expected JS execution output.
 - [x] forall / ∀ sugar (Maybe drop this, issues with `.` and `{A}` works fine)
 - [x] Bad module name error has FC 0,0 instead of the module or name
-- [ ] ~~Remove context lambdas when printing solutions (show names from context)~~
-  - maybe build list of names and strip λ, then call pprint with names
-  - I've removed solution printing, so this is moot
 - [ ] Revisit substitution in case building
 - [x] Check for shadowing when declaring dcon
   - Handles the forward decl in `Zoo1.newt`, but we'll need different syntax if
@@ -131,7 +133,7 @@ More comments in code! This is getting big enough that I need to re-find my bear
 - [x] implicit patterns
 - [x] operators
 - [x] pair syntax (via comma operator)
-- [ ] `data` sugar: `data Maybe a = Nothing | Just a`
+- [x] `data` sugar: `data Maybe a = Nothing | Just a`
 - [x] matching on operators
   - [x] top level
   - [x] case statements
diff --git a/aoc2024/Day23.newt b/aoc2024/Day23.newt
index 4c8dbdb..a65fe9f 100644
--- a/aoc2024/Day23.newt
+++ b/aoc2024/Day23.newt
@@ -65,11 +65,6 @@ bronKerbosch g rs (p :: ps) xs =
     best a Nothing = a
     best (Just a) (Just b) = if length a < length b then Just b else Just a
 
-joinBy : String → List String → String
-joinBy _ Nil = ""
-joinBy _ (x :: Nil) = x
-joinBy s (x :: y :: xs) = joinBy s ((x ++ s ++ y) :: xs)
-
 run : String -> IO Unit
 run fn = do
   putStrLn fn
diff --git a/aoc2024/Day24.newt b/aoc2024/Day24.newt
index 35d5d26..1be9d0d 100644
--- a/aoc2024/Day24.newt
+++ b/aoc2024/Day24.newt
@@ -126,7 +126,6 @@ check : List Gate → List Int → String → Either (String × String) Unit
 check gates Nil carry = Right MkUnit
 check gates (bit :: bits) carry = do
   let xl = label 'x' bit
-  let yl = label 'x' bit
   let (Just a1) = matchIn xl And | _ => fail $ "no a1 " ++ show bit
   let (Just x1) = matchIn xl Xor | _ => fail $ "no x1 " ++ show bit
   -- just peel of the carry for bit0
@@ -174,11 +173,6 @@ trampoline gates acc = do
       putStrLn $ "SWAP " ++ a ++ " and " ++ b
       trampoline (map (swapPins a b) gates) (a :: b :: acc)
 
-joinBy : String → List String → String
-joinBy _ Nil = ""
-joinBy _ (x :: Nil) = x
-joinBy s (x :: y :: xs) = joinBy s ((x ++ s ++ y) :: xs)
-
 run : String -> IO Unit
 run fn = do
   putStrLn fn
diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json
index d662f61..b431f60 100644
--- a/newt-vscode/syntaxes/newt.tmLanguage.json
+++ b/newt-vscode/syntaxes/newt.tmLanguage.json
@@ -26,11 +26,14 @@
         { "include": "source.js" }
       ]
     },
+    {
+      "name": "string.newt",
+      "match": "'(.|\\\\.)'"
+    },
     {
       "name": "string.newt",
       "begin": "\"",
       "end": "\""
     }
-
   ]
 }
diff --git a/newt/Prelude.newt b/newt/Prelude.newt
index 79c11a8..bc9b66f 100644
--- a/newt/Prelude.newt
+++ b/newt/Prelude.newt
@@ -6,8 +6,7 @@ id x = x
 the : (a : U) → a → a
 the _ a = a
 
-data Bool : U where
-  True False : Bool
+data Bool = True | False
 
 not : Bool → Bool
 not True = False
@@ -33,9 +32,7 @@ infixl 6 _/=_
 _/=_ : ∀ a. {{Eq a}} → a → a → Bool
 a /= b = not (a == b)
 
-data Nat : U where
-  Z : Nat
-  S : Nat -> Nat
+data Nat = Z | S Nat
 
 pred : Nat → Nat
 pred Z = Z
@@ -46,22 +43,17 @@ instance Eq Nat where
   S n == S m = n == m
   x == y = False
 
-data Maybe : U -> U where
-  Just : ∀ a. a -> Maybe a
-  Nothing : ∀ a. Maybe a
+
+data Maybe a = Just a | Nothing
 
 fromMaybe : ∀ a. a → Maybe a → a
 fromMaybe a Nothing = a
 fromMaybe _ (Just a) = a
 
-data Either : U -> U -> U where
-  Left : {0 a b : U} -> a -> Either a b
-  Right : {0 a b : U} -> b -> Either a b
+data Either a b = Left a | Right b
 
 infixr 7 _::_
-data List : U -> U where
-  Nil : ∀ A. List A
-  _::_ : ∀ A. A → List A → List A
+data List a = Nil | a :: List a
 
 length : ∀ a. List a → Nat
 length Nil = Z
@@ -69,9 +61,7 @@ length (x :: xs) = S (length xs)
 
 
 infixl 7 _:<_
-data SnocList : U → U where
-  Lin : ∀ A. SnocList A
-  _:<_ : ∀ A. SnocList A → A → SnocList A
+data SnocList a = Lin | SnocList a :< a
 
 -- 'chips'
 infixr 6 _<>>_ _<><_
@@ -90,8 +80,7 @@ xs <>< (y :: ys) = (xs :< y) <>< ys
 
 infixr 8 _×_
 infixr 2 _,_
-data _×_ : U → U → U where
-  _,_ : ∀ A B. A → B → A × B
+data a × b = (a,b)
 
 fst : ∀ a b. a × b → a
 fst (a,b) = a
@@ -222,6 +211,8 @@ instance Mul Nat where
   Z * _ = Z
   S n * m = m + n * m
 
+pfunc mod : Int → Int → Int := `(a,b) => a % b`
+
 infixl 7 _-_
 class Sub a where
   _-_ : a → a → a
@@ -252,9 +243,7 @@ instance Eq String where
 instance Eq Char where
   a == b = jsEq a b
 
-
-data Unit : U where
-  MkUnit : Unit
+data Unit = MkUnit
 
 ptype Array : U → U
 pfunc listToArray : {a : U} -> List a -> Array a := `
@@ -324,8 +313,7 @@ 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
-  MkIORes : ∀ a. a -> World -> IORes a
+data IORes a = MkIORes a World
 
 IO : U -> U
 IO a = World -> IORes a
@@ -761,3 +749,16 @@ instance ∀ a. {{Eq a}} → Eq (List a) where
 find : ∀ a. (a → Bool) → List a → Maybe a
 find f Nil = Nothing
 find f (x :: xs) = if f x then Just x else find f xs
+
+-- TODO this would be faster, but less pure as a primitive
+-- fastConcat might be a good compromise
+joinBy : String → List String → String
+joinBy _ Nil = ""
+joinBy _ (x :: Nil) = x
+joinBy s (x :: y :: xs) = joinBy s ((x ++ s ++ y) :: xs)
+
+snoc : ∀ a. List a → a → List a
+snoc xs x = xs ++ (x :: Nil)
+
+instance ∀ a b. {{Show a}} {{Show b}} → Show (a × b) where
+  show (a,b) = "(" ++ show a ++ "," ++ show b ++ ")"
diff --git a/playground/src/monarch.ts b/playground/src/monarch.ts
index c1e8c4c..8b7f48b 100644
--- a/playground/src/monarch.ts
+++ b/playground/src/monarch.ts
@@ -110,7 +110,8 @@ export let newtTokens: monaco.languages.IMonarchLanguage = {
           },
         },
       ],
-
+      // char literal, but I don't think there is a class for that.
+      [/'\\?.'/, "string"],
       [/\d+/, "number"],
 
       // strings
@@ -125,7 +126,7 @@ export let newtTokens: monaco.languages.IMonarchLanguage = {
     string: [
       [/[^\\"]+/, "string"],
       // [/@escapes/, "string.escape"],
-      [/\\./, "string.escape.invalid"],
+      // [/\\./, "string.escape.invalid"],
       [/"/, { token: "string.quote", bracket: "@close", next: "@pop" }],
     ],
     whitespace: [
diff --git a/port/Prettier.newt b/port/Prettier.newt
index 59df4e6..7eb0057 100644
--- a/port/Prettier.newt
+++ b/port/Prettier.newt
@@ -14,7 +14,7 @@ import Prelude
 data Doc : U where
   Empty Line : Doc
   Text : String -> Doc
-  Nest : Nat -> Doc -> Doc
+  Nest : Int -> Doc -> Doc
   Seq : Doc -> Doc -> Doc
   Alt : Doc -> Doc -> Doc
 
@@ -24,7 +24,7 @@ data Doc : U where
 -- data Item = TEXT String | LINE Nat
 data Item : U where
   TEXT :  String -> Item
-  LINE : Nat -> Item
+  LINE : Int -> Item
 
 empty : Doc
 empty = Empty
@@ -43,13 +43,13 @@ group x = Alt (flatten x) x
 -- TODO - we can accumulate snoc and cat all at once
 layout : List Item -> SnocList String -> String
 layout Nil acc = fastConcat $ acc <>> Nil
-layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate k ' ')
+layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate (cast k) ' ')
 layout (TEXT str :: x) acc = layout x (acc :< str)
 
 -- Whether a documents first line fits.
-fits : Nat -> List Item -> Bool
+fits : Int -> List Item -> Bool
 fits 0 x = False
-fits w ((TEXT s) :: xs) = fits (w - length s) xs
+fits w ((TEXT s) :: xs) = fits (w - slen s) xs
 fits w _ = True
 
 -- vs Wadler, we're collecting the left side as a SnocList to prevent
@@ -58,21 +58,21 @@ fits w _ = True
 
 -- I've now added a `fit` boolean to indicate if we should cut when we hit the line length
 -- Wadler was relying on laziness to stop the first branch before LINE if necessary
-be : Bool -> SnocList Item -> Nat -> Nat -> List (Nat × Doc) -> Maybe (List Item)
+be : Bool -> SnocList Item -> Int -> Int -> List (Int × Doc) -> Maybe (List Item)
 be fit acc w k Nil = Just (acc <>> Nil)
 be fit acc w k ((i, Empty) :: xs) = be fit acc w k xs
 be fit acc w k ((i, Line) :: xs) = (be False (acc :< LINE i) w i xs)
 be fit acc w k ((i, (Text s)) :: xs) =
-  case not fit || (k + length s < w) of
-    True => (be fit (acc :< TEXT s) w (k + length s) xs)
+  case not fit || (k + slen s < w) of
+    True => (be fit (acc :< TEXT s) w (k + slen s) xs)
     False => Nothing
 be fit acc w k ((i, (Nest j x)) :: xs) = be fit acc w k ((i + j, x):: xs)
 be fit acc w k ((i, (Seq x y)) :: xs) = be fit acc w k ((i,x) :: (i,y) :: xs)
 be fit acc w k ((i, (Alt x y)) :: xs) =
   (_<>>_ acc) <$> (be True Lin w k ((i,x) :: xs) <|> be fit Lin w k ((i, y) :: xs))
 
-best : Nat -> Nat -> Doc -> List Item
-best w k x = fromMaybe Nil $ be False Lin w k ((Z,x) :: Nil)
+best : Int -> Int -> Doc -> List Item
+best w k x = fromMaybe Nil $ be False Lin w k ((0,x) :: Nil)
 
 -- interface Pretty a where
 --   pretty : a -> Doc
@@ -83,8 +83,8 @@ data Pretty : U -> U where
 pretty : {a} {{Pretty a}} → a → Doc
 pretty {{MkPretty p}} x = p x
 
-render : Nat -> Doc -> String
-render w x = layout (best w Z x) Lin
+render : Int -> Doc -> String
+render w x = layout (best w 0 x) Lin
 
 instance Semigroup Doc where
   x <+> y = Seq x (Seq (Text " ") y)
@@ -97,7 +97,7 @@ line = Line
 text : String -> Doc
 text = Text
 
-nest : Nat -> Doc -> Doc
+nest : Int -> Doc -> Doc
 nest = Nest
 
 instance Concat Doc where
@@ -123,7 +123,7 @@ stack = folddoc _</>_
 
 -- bracket x with l and r, indenting contents on new line
 bracket : String -> Doc -> String -> Doc
-bracket l x r = group (text l ++ nest (S (S Z)) (line ++ x) ++ line ++ text r)
+bracket l x r = group (text l ++ nest 2 (line ++ x) ++ line ++ text r)
 
 infixl 5 _<+/>_
 
@@ -138,7 +138,7 @@ fill Nil = Empty
 fill (x :: Nil) = x
 fill (x :: y :: xs) = Alt (flatten x <+> fill (flatten y :: xs)) (x </> fill (y :: xs))
 
--- separate with space
+-- separate with comma
 commaSep : List Doc -> Doc
 commaSep = folddoc (\a b => a ++ text "," <+/> b)
 
diff --git a/src/Lib/Common.idr b/src/Lib/Common.idr
index 13185c1..c0b72c4 100644
--- a/src/Lib/Common.idr
+++ b/src/Lib/Common.idr
@@ -30,12 +30,6 @@ quoteString str = pack $ encode (unpack str) [< '"']
       let v : Nat = cast c in
       if v < 32 then encode cs (acc :< '\\' :< 'u' :< hexDigit (div v 4096) :< hexDigit (div v 256) :< hexDigit (div v 16) :< hexDigit v )
       else encode cs (acc :< c)
-      -- else if v < 128 then encode cs (acc :< c)
-      -- if v < 32 then encode cs (acc :< '\\' :< 'x' :< hexDigit (div v 16) :< hexDigit v )
-      -- else if v < 128 then encode cs (acc :< c)
-      -- -- TODO unicode
-      -- else if v < 256 then encode cs (acc :< '\\' :< 'x' :< hexDigit (div v 16) :< hexDigit v )
-      -- else encode cs (acc :< '\\' :< 'u' :< hexDigit (div v 4096) :< hexDigit (div v 256) :< hexDigit (div v 16) :< hexDigit v )
 
 public export
 data Json : Type where
diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index e96da68..90ecc4f 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -24,7 +24,6 @@ collectDecl ((Def fc nm cl) :: rest@(Def _ nm' cl' :: xs)) =
   else (Def fc nm cl :: collectDecl rest)
 collectDecl (x :: xs) = x :: collectDecl xs
 
-
 -- renaming
 -- dom gamma ren
 data Pden = PR Nat Nat (List Nat)
@@ -724,7 +723,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
       Just cons <- rewriteConstraint sctynm vars cons [] | _ => pure Nothing
       pure $ Just $ MkClause fc cons pats expr
 
-
+export
 splitArgs : Raw -> List (Raw, Icit) -> (Raw, List (Raw, Icit))
 splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args)
 splitArgs tm args = (tm, args)
diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr
index 7c747be..900f3cd 100644
--- a/src/Lib/Parser.idr
+++ b/src/Lib/Parser.idr
@@ -174,16 +174,17 @@ letExpr = do
   alts <- startBlock $ someSame $ letAssign
   keyword' "in"
   scope <- typeExpr
-  pure $ foldl (\ acc, (n,fc,v) => RLet fc n (RImplicit fc) v acc) scope (reverse alts)
+  pure $ foldl (\ acc, (n,fc,ty,v) => RLet fc n (fromMaybe (RImplicit fc) ty) v acc) scope (reverse alts)
   where
-    letAssign : Parser (Name,FC,Raw)
+    letAssign : Parser (Name,FC,Maybe Raw,Raw)
     letAssign = do
       fc <- getPos
       name <- ident
       -- TODO type assertion
+      ty <- optional (keyword ":" *> typeExpr)
       keyword "="
       t <- typeExpr
-      pure (name,fc,t)
+      pure (name,fc,ty,t)
 
 pLamArg : Parser (Icit, String, Maybe Raw)
 pLamArg = (Implicit,,) <$> braces (ident <|> uident) <*> optional (sym ":" >> typeExpr)
@@ -441,13 +442,21 @@ parsePFunc = do
   pure $ PFunc fc nm (fromMaybe [] uses) ty src
 
 
+parseShortData : Parser Decl
+parseShortData = do
+  fc <- getPos
+  keyword "data"
+  lhs <- typeExpr
+  keyword "="
+  sigs <- sepBy (keyword "|") typeExpr
+  pure $ ShortData fc lhs sigs
+
 export
 parseData : Parser Decl
 parseData = do
   fc <- getPos
-  keyword "data"
-  name <- uident <|> ident <|> token MixFix
-  keyword ":"
+  -- commit when we hit ":"
+  name <- try $ (keyword "data" *> (uident <|> ident <|> token MixFix) <* keyword ":")
   ty <- typeExpr
   keyword "where"
   decls <- startBlock $ manySame $ parseSig
@@ -500,7 +509,7 @@ parseNorm = DCheck <$> getPos <* keyword "#check" <*> typeExpr <* keyword ":" <*
 export
 parseDecl : Parser Decl
 parseDecl = parseMixfix <|> parsePType <|> parsePFunc
-  <|> parseNorm <|> parseData <|> parseSig <|> parseDef
+  <|> parseNorm <|> parseData <|> parseShortData <|> parseSig <|> parseDef
   <|> parseClass <|> parseInstance <|> parseRecord
 
 
diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr
index 67eb9dc..99a0beb 100644
--- a/src/Lib/Parser/Impl.idr
+++ b/src/Lib/Parser/Impl.idr
@@ -140,6 +140,11 @@ mutual
   export many : Parser a -> Parser (List a)
   many p = some p <|> pure []
 
+-- one or more `a` seperated by `s`
+export
+sepBy : Parser s -> Parser a -> Parser (List a)
+sepBy s a = (::) <$> a <*> many (s *> a)
+
 export
 getPos : Parser FC
 getPos = P $ \toks, com, ops, indent => case toks of
@@ -196,7 +201,7 @@ token' k = pred (\t => t.val.kind == k) "Expected a \{show k} token"
 export
 keyword' : String -> Parser ()
 -- FIXME make this an appropriate whitelist
-keyword' kw = ignore $ pred (\t => t.val.text == kw && t.val.kind /= Character) "Expected \{kw}"
+keyword' kw = ignore $ pred (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number)) "Expected \{kw}"
 
 ||| expect indented token of given kind
 export
diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr
index fefbb17..c709fd8 100644
--- a/src/Lib/Prettier.idr
+++ b/src/Lib/Prettier.idr
@@ -138,7 +138,7 @@ fill [] = Empty
 fill [x] = x
 fill (x :: y :: xs) = (flatten x <+> fill (flatten y :: xs)) `Alt` (x </> fill (y :: xs))
 
-||| separate with space
+||| separate with comma
 export
 commaSep : List Doc -> Doc
 commaSep = folddoc (\a, b => a ++ text "," <+/> b)
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index f613724..99badbd 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -416,6 +416,28 @@ processDecl ns (Instance instfc ty decls) = do
     apply (VPi fc nm icit rig a b) (x :: xs) = apply !(b $$ x) xs
     apply x (y :: xs) = error instfc "expected pi type \{show x}"
 
+processDecl ns (ShortData fc lhs sigs) = do
+  (nm,args) <- getArgs lhs []
+  let ty = foldr (\ (fc,n), a => (RPi fc (BI fc n Explicit Many) (RU fc) a)) (RU fc) args
+  cons <- traverse (mkDecl args []) sigs
+  let dataDecl = Data fc nm ty cons
+  putStrLn "SHORTDATA"
+  putStrLn "\{pretty dataDecl}"
+  processDecl ns dataDecl
+  where
+    getArgs : Raw -> List (FC, String) -> M (String, List (FC, String))
+    getArgs (RVar fc1 nm) acc = pure (nm, acc)
+    getArgs (RApp _ t (RVar fc' nm) _) acc = getArgs t ((fc', nm) :: acc)
+    getArgs tm _ = error (getFC tm) "Expected contructor application, got: \{show tm}"
+
+    mkDecl : List (FC, Name) -> List Raw -> Raw -> M Decl
+    mkDecl args acc (RVar fc' name) = do
+      let base = foldr (\ ty, acc => RPi (getFC ty) (BI (getFC ty) "_" Explicit Many) ty acc) lhs acc
+      let ty = foldr (\ (fc,nm), acc => RPi fc (BI fc nm Implicit Zero) (RU fc) acc) base args
+      pure $ TypeSig fc' [name] ty
+    mkDecl args acc (RApp fc' t u icit) = mkDecl args (u :: acc) t
+    mkDecl args acc tm = error (getFC tm) "Expected contructor application, got: \{show tm}"
+
 processDecl ns (Data fc nm ty cons) = do
   putStrLn "-----"
   putStrLn "Data \{nm}"
diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr
index 358cf37..220f41c 100644
--- a/src/Lib/Syntax.idr
+++ b/src/Lib/Syntax.idr
@@ -120,6 +120,7 @@ data Decl
   | Def FC Name (List (Raw, Raw)) -- (List Clause)
   | DCheck FC Raw Raw
   | Data FC Name Raw (List Decl)
+  | ShortData FC Raw (List Raw)
   | PType FC Name (Maybe Raw)
   | PFunc FC Name (List String) Raw String
   | PMixFix FC (List Name) Nat Fixity
@@ -133,6 +134,7 @@ HasFC Decl where
   getFC (Def x str xs) = x
   getFC (DCheck x tm tm1) = x
   getFC (Data x str tm xs) = x
+  getFC (ShortData x _ _) = x
   getFC (PType x str mtm) = x
   getFC (PFunc x str _ tm str1) = x
   getFC (PMixFix x strs k y) = x
@@ -182,6 +184,7 @@ Show Decl where
   show (Data _ str xs ys) = foo ["Data", show str, show xs, show ys]
   show (DCheck _ x y) = foo ["DCheck", show x, show y]
   show (PType _ name ty) = foo ["PType", name, show ty]
+  show (ShortData _ lhs sigs) = foo ["ShortData", show lhs, show sigs]
   show (PFunc _ nm uses ty src) = foo ["PFunc", nm, show uses, show ty, show src]
   show (PMixFix _ nms prec fix) = foo ["PMixFix", show nms, show prec, show fix]
   show (Class _ nm tele decls) = foo ["Class",  nm, "...", show $ map show decls]
@@ -280,6 +283,9 @@ Pretty Raw where
 prettyBind : (BindInfo, Raw) -> Doc
 prettyBind (BI _ nm icit quant, ty) = wrap icit (text (show quant ++ nm) <+> text ":" <+> pretty ty)
 
+pipeSep : List Doc -> Doc
+pipeSep = folddoc (\a, b => a <+/> text "|" <+> b)
+
 export
 Pretty Decl where
   pretty (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty)
@@ -295,6 +301,7 @@ Pretty Decl where
   pretty (Class _ nm tele decls) = text "class" <+> text nm <+> ":" <+> spread (map prettyBind tele)
     <+> (nest 2 $ text "where" </> stack (map pretty decls))
   pretty (Instance _ _ _) = text "TODO pretty Instance"
+  pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> "=" <+> pipeSep (map pretty sigs)
 
 export
 Pretty Module where
diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr
index eb4c5e5..11c3a50 100644
--- a/src/Lib/Tokenizer.idr
+++ b/src/Lib/Tokenizer.idr
@@ -8,8 +8,8 @@ import Lib.Common
 keywords : List String
 keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
             "ptype", "pfunc", "module", "infixl", "infixr", "infix",
-            "∀", "forall",
-            "class", "instance",
+            "∀", "forall", "import", "uses",
+            "class", "instance", "record", "constructor",
             "if", "then", "else",
             "$", "λ", "?", "@",
              "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_", "|"]
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index a91e57d..13e2f0a 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -92,17 +92,6 @@ public export
 HasFC BindInfo where
   getFC (BI fc _ _ _) = fc
 
--- do we just admit string names for these and let the prim functions
--- sort it out?
--- I'd like Int / String to have syntax
-
-data PrimType = StringType | IntType
-
-data PrimVal : Type where
-  PrimString : String -> PrimVal
-  PrimInt : Int -> PrimVal
-  PrimChar : Char -> PrimVal
-
 public export
 data Tm : Type
 
diff --git a/src/Main.idr b/src/Main.idr
index 0712eab..a392e0e 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -93,14 +93,14 @@ fastReadFile fn = do
 
 
 ||| New style loader, one def at a time
-processModule : String -> List String -> String -> M String
-processModule base stk name = do
+processModule : FC -> String -> List String -> String -> M String
+processModule importFC base stk name = do
   top <- get
   let False := elem name top.loaded | _ => pure ""
   modify { loaded $= (name::) }
   let fn = if base == "" then name ++ ".newt" else base ++ "/" ++ name ++ ".newt"
   Right src <- fastReadFile $ fn
-    | Left err => fail "error reading \{fn}: \{show err}"
+    | Left err => fail "ERROR at \{show importFC}: error reading \{fn}: \{show err}"
   let Right toks = tokenise fn src
     | Left err => fail (showError src err)
 
@@ -119,7 +119,7 @@ processModule base stk name = do
     -- we could use `fc` if it had a filename in it
 
     when (name' `elem` stk) $ error emptyFC "import loop \{show name} -> \{show name'}"
-    processModule base (name :: stk) name'
+    processModule fc base (name :: stk) name'
 
   top <- get
   mc <- readIORef top.metas
@@ -163,7 +163,7 @@ processFile fn = do
   processDecl ["Prim"] (PType emptyFC "String" Nothing)
   processDecl ["Prim"] (PType emptyFC "Char" Nothing)
 
-  src <- processModule dir [] name
+  src <- processModule emptyFC dir [] name
   top <- get
   -- dumpContext top