diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs
index 2c7508e1..c2e93447 100644
--- a/brat/Brat/Checker.hs
+++ b/brat/Brat/Checker.hs
@@ -13,13 +13,14 @@ module Brat.Checker (checkBody
 import Control.Monad (foldM, forM, zipWithM_)
 import Control.Monad.Freer
 import Data.Bifunctor
-import Data.Foldable (for_)
+import Data.Foldable (for_, traverse_)
 import Data.Functor (($>), (<&>))
 import Data.List ((\\), intercalate)
 import Data.List.NonEmpty (NonEmpty(..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Map as M
 import Data.Maybe (fromJust)
+import qualified Data.Set as S
 import Data.Traversable (for)
 import Data.Type.Equality ((:~:)(..), testEquality)
 import Prelude hiding (filter)
@@ -27,6 +28,7 @@ import Prelude hiding (filter)
 import Brat.Checker.Helpers
 import Brat.Checker.Monad
 import Brat.Checker.Quantity
+import Brat.Checker.SolveConstraints (fulbournConstraint, simplify)
 import Brat.Checker.SolveHoles (typeEq)
 import Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve, typeOfEnd)
 import Brat.Checker.Types
@@ -48,7 +50,9 @@ import Brat.Syntax.Simple
 import Brat.Syntax.Value
 import Bwd
 import Hasochism
-import Util (zipSameLength)
+import Util (log2, zipSameLength)
+
+import Debug.Trace
 
 -- Put things into a standard form in a kind-directed manner, such that it is
 -- meaningful to do case analysis on them
@@ -231,6 +235,11 @@ check' (Lambda c@(WC abstFC abst,  body) cs) (overs, unders) = do
           let srcMap = fromJust $ zipSameLength (fst <$> usedOvers) (fst <$> fakeOvers)
           let fakeProblem = [ (fromJust (lookup src srcMap), pat) | (src, pat) <- problem ]
           fakeEnv <- localFC abstFC $ solve ?my fakeProblem >>= (solToEnv . snd)
+          case ?my of
+            Braty -> do
+              constraints <- constraintsFromEnv (concat . M.elems $ fakeEnv)
+              traverse_ fulbournConstraint constraints
+            _ -> pure ()
           pure (fakeEnv, fakeAcc)
         localEnv fakeEnv $ do
           (_, fakeUnders, [], _) <- anext "lambda_fake_target" Hypo fakeAcc outs R0
@@ -387,16 +396,19 @@ check' (Var x) ((), ()) = (, ((), ())) . ((),) <$> case ?my of
   Kerny -> req (KLup x) >>= \case
     Just (p, ty) -> pure [(p, ty)]
     Nothing -> err $ KVarNotFound (show x)
-check' (Arith op l r) ((), u@(hungry, ty):unders) = case (?my, ty) of
-  (Braty, ty) -> do
-    ty <- evalBinder Braty ty
-    case ty of
-      Right TNat -> check_arith TNat
-      Right TInt -> check_arith TInt
-      Right TFloat -> check_arith TFloat
-      _ -> err . ArithNotExpected $ show u
+check' (Arith op l r) ((), (hungry, ty):unders) = case (?my, ty) of
+  (Braty, ty) -> checkNumTy ty
   (Kerny, _) -> err ArithInKernel
  where
+  checkNumTy :: BinderType Brat -> Checking (SynConnectors m d k, ChkConnectors m d k)
+  checkNumTy (Right ty) | ty `elem` [TNat, TInt, TFloat] = check_arith ty
+  -- Why don't we allow Left Nat??
+  checkNumTy (Right ty@(VApp (VPar e) B0)) = do
+    mkYield (NeedToKnow e) "WaitingForArithHope" (S.singleton e)
+    ty <- eval S0 ty
+    checkNumTy (Right ty)
+  checkNumTy _ = err $ ArithNotExpected (show ty)
+
   check_arith ty = let ?my = Braty in do
     let inRo = RPr ("left", ty) $ RPr ("right", ty) R0
     let outRo = RPr ("out", ty) R0
@@ -707,10 +719,39 @@ check' (Hope ident) ((), (tgt@(NamedPort bang _), ty):unders) = case (?my, ty) o
     defineSrc' "check hope (src)" dangling (endVal k (toEnd hungry))
     req (ANewDynamic (end hungry) fc)
     pure (((), ()), ((), unders))
-  (Braty, Right _ty) -> typeErr "Can only infer kinded things with !"
+  (Braty, Right (VEqn lhs rhs)) -> do
+    mkFork "SolveHopedConstraint" $ solveConstraint ident tgt (lhs, rhs)
+    pure (((), ()), ((), unders))
+  (Braty, Right _ty) -> typeErr "Can only infer kinded things or equations with !"
   (Kerny, _) -> typeErr "Won't infer kernel typed !"
 check' tm _ = error $ "check' " ++ show tm
 
+solveConstraint :: String -> Tgt -> (NumSum (VVar Z), NumSum (VVar Z))
+                -> Checking ()
+solveConstraint ident tgt (lhs,rhs) = do
+  CtxEnv _ locals <- req AskVEnv
+  constraints <- constraintsFromEnv (concat (M.elems locals))
+  traceM ("Got:\n> " ++ show constraints)
+  lhs <- numSumUpdate lhs
+  rhs <- numSumUpdate rhs
+  let eqSimp@(lhsSimp, rhsSimp) = simplify (lhs, rhs)
+  traceM ("Want:\n> " ++ show eqSimp)
+  if eqSimp `elem` ((NumSum 0 [], NumSum 0 []):constraints)
+  then defineTgt' ident tgt (VEqn lhsSimp rhsSimp)
+  else do
+   mkFork "" $ fulbournConstraint eqSimp
+   mkYield (WaitingForConstraint (show eqSimp)) ident (S.fromList $ depEnds eqSimp)
+   solveConstraint ident tgt eqSimp
+
+
+constraintsFromEnv :: [(a, BinderType Brat)] -> Checking [(NumSum (VVar Z), NumSum (VVar Z))]
+constraintsFromEnv [] = pure []
+constraintsFromEnv ((_, Right (VEqn lhs rhs)):overs) = do
+  lhs <- numSumUpdate lhs
+  rhs <- numSumUpdate rhs
+  let eqn = simplify (lhs, rhs)
+  (eqn:) <$> constraintsFromEnv overs
+constraintsFromEnv (_:xs) = constraintsFromEnv xs
 
 -- Clauses from either function definitions or case statements, as we get
 -- them from the elaborator
@@ -744,7 +785,13 @@ checkClause my fnName cty clause = modily my $ do
     problem <- argProblems (fst <$> overs) (unWC $ lhs clause) []
     (tests, sol) <- localFC (fcOf (lhs clause)) $ solve my problem
     (sol, defs) :: ([(String, (Src, BinderType m))], [((String, TypeKind), Val Z)]) <- case my of
-      Braty -> postProcessSolAndOuts sol unders
+      Braty -> do
+        (sol, defs) <- postProcessSolAndOuts sol unders
+        constraints <- constraintsFromEnv (second snd <$> sol)
+        traverse fulbournConstraint constraints
+        --traceM ("We've got (checkClause):\n  " ++ show constraints)
+        pure (sol, defs)
+
       Kerny -> pure (sol, [])
     -- The solution gives us the variables bound by the patterns.
     -- We turn them into a row
@@ -789,7 +836,8 @@ checkClause my fnName cty clause = modily my $ do
   (Some stk) <><< (x:xs) = Some (stk :<< x) <><< xs
 
   -- Process a solution, finding Ends that support the solved types, and return a list of definitions for substituting later on
-  postProcessSolAndOuts :: [(String, (Src, BinderType Brat))] -> [(Tgt, BinderType Brat)] -> Checking ([(String, (Src, BinderType Brat))], [((String, TypeKind), Val Z)])
+  postProcessSolAndOuts :: [(String, (Src, BinderType Brat))] -> [(Tgt, BinderType Brat)]
+                        -> Checking ([(String, (Src, BinderType Brat))], [((String, TypeKind), Val Z)])
   postProcessSolAndOuts sol outputs = worker B0 sol
    where
     worker :: Bwd (String, (Src, BinderType Brat)) -> [(String, (Src, BinderType Brat))] -> Checking ([(String, (Src, BinderType Brat))], [((String, TypeKind), Val Z)])
@@ -805,9 +853,6 @@ checkClause my fnName cty clause = modily my $ do
          zx <- pure $ foldl (\sol srcAndTy -> insert ("$" ++ show (end (fst srcAndTy)), srcAndTy) sol) zx srcAndTys
          (sol, defs) <- worker (zx {-:< entry-}) sol
          pure ({-(patVar, (src, Left k)):-}sol, ((patVar, k), def):defs)
-    -- Pat vars beginning with '_' aren't in scope, we can ignore them
-    -- (but if they're kinded they might come up later as the dependency of something else)
-    worker zx (('_':_, _):sol) = worker zx sol
     worker zx (entry@(_patVar, (_src, Right ty)):sol) = do
       trackM ("processSol (typed): " ++ show entry)
       ty <- eval S0 ty
@@ -1043,13 +1088,92 @@ kindCheck ((hungry, Nat):unders) (Con c arg)
      defineTgt' "kind8" hungry v
      pure ([v], unders)
 
+kindCheck ((hungry, Star []):unders) (Eqn (WC lwc lhs) (WC rwc rhs)) = do
+  -- Should we make a new `NodeType` for this?
+  (_, [(lunder,_),(runder,_)], [(dangling,_)], _) <- next "Eq" Hypo (S0, Some (Zy :* S0))
+                                                        (REx ("lhs", Nat) (REx ("rhs", Nat) R0))
+                                                        (REx ("out", Star []) R0)
+  lns <- localFC lwc $ kindCheckNumSum lunder lhs
+  rns <- localFC rwc $ kindCheckNumSum runder rhs
+  wire (dangling, TUnit, hungry)
+  pure ([VEqn lns rns], unders)
 kindCheck ((_, k):_) tm = typeErr $ "Expected " ++ show tm ++ " to have kind " ++ show k
 
 
+-- N.B. We're not really doing any defining that would be useful for the
+-- typechecker yet. The obvious defining isn't possible because NumSum is not a
+-- `Val`.
+kindCheckNumSum :: Tgt -- Nat kinded tgt to wire numsum to
+                -> Term Chk Noun -- The term to turn into a numsum
+                -> Checking (NumSum (VVar Z))
+kindCheckNumSum hungry (Arith op (WC lwc lhs) (WC rwc rhs)) = do
+  (_, [(lunder,_),(runder,_)], [(dangling, _)], _) <- next (show op ++ "NS") (ArithNode op)
+                                                      (S0, Some (Zy :* S0))
+                                                      (REx ("lhs", Nat) (REx ("rhs", Nat) R0))
+                                                      (REx ("out", Nat) R0)
+
+  ns <- case op of
+    Add -> do
+      lns <- kindCheckNumSum lunder lhs
+      rns <- kindCheckNumSum runder rhs
+      pure (lns <> rns)
+    Mul -> do
+      lns <- kindCheckNumSum lunder lhs
+      rns <- kindCheckNumSum runder rhs
+      case (lns, rns) of
+        (NumSum c [], _) -> let ns = multNumSum rns c in ns <$ wire (dangling, TNat, hungry)
+        (_, NumSum c []) -> let ns = multNumSum lns c in ns <$ wire (dangling, TNat, hungry)
+        _ -> localFC eqFC $ typeErr "Constraint too complicated: must be between sums"
+    Sub -> do
+      lns <- kindCheckNumSum lunder lhs
+      rns <- kindCheckNumSum runder rhs
+      case numSumSub lns rns of
+        Just ns -> ns <$ wire (dangling, TNat, hungry)
+        Nothing -> localFC rwc $ typeErr "Subtraction too complicated"
+    Pow -> do
+      lns <- kindCheckNumSum lunder lhs
+      rns <- kindCheckNumSum runder rhs
+      case (lns, rns) of
+        (NumSum n [], rns)
+         | Just k <- log2 n, Just nv <- sumToVal rns -> pure (nv_to_sum (powN k nv))
+        _ -> localFC eqFC $ typeErr "Power too confusing"
+
+    Div -> localFC eqFC $ typeErr "Won't handle division in equations"
+  wire (dangling, TNat, hungry)
+  pure ns
+ where
+  eqFC = spanFC lwc rwc
+
+  -- Take 2^n
+  powN :: Integer -> NumVal v -> NumVal v
+  powN 0 nv = nv
+  powN k nv = powN (k - 1) (nPlus 1 (nFull nv))
+
+  numSumSub :: NumSum (VVar Z) -> NumSum (VVar Z) -> Maybe (NumSum (VVar Z))
+  numSumSub (NumSum c vs) (NumSum d ws) | c >= d = NumSum (c-d) <$> aux vs ws
+   where
+    -- blah blah O(n^2)
+    aux :: [(Monotone (VVar Z), Integer)] -> [(Monotone (VVar Z), Integer)]
+        -> Maybe [(Monotone (VVar Z), Integer)]
+    aux monos [] = Just monos
+    aux monos ((v, n):vs) = case [ m | (w, m) <- monos, w == v ] of
+      [m] | m >= n -> ((v, m - n):) <$> aux monos vs
+      [] -> Nothing
+
+  sumToVal :: NumSum v -> Maybe (NumVal v)
+  sumToVal (NumSum up [(n, k)]) | Just l <- log2 k = Just $ nPlus up (n2PowTimes l (numValue n))
+  sumToVal _ = Nothing
+
+kindCheckNumSum under tm = do
+  ([val], []) <- kindCheck [(under, Nat)] tm
+  case val of
+    VNum nv -> let ns = nv_to_sum nv in pure ns -- TODO: Wiring
+    x -> error $ "Didn't expect: " ++ show x
+
 -- Checks the kinds of the types in a dependent row
 kindCheckRow :: Modey m
              -> String -- for node name
-             -> [(PortName, ThunkRowType m)] -- The row to process
+             -> [TypeRowElem TermConstraint (ThunkRowType m)] -- The row to process
              -> Checking (Some (Ro m Z))
 kindCheckRow my name r = do
   name <- req $ Fresh $ "__kcr_" ++ name
@@ -1060,7 +1184,7 @@ kindCheckRow my name r = do
 -- evaluation of the type of an Id node passing through such values
 kindCheckAnnotation :: Modey m
                     -> String -- for node name
-                    -> [(PortName, ThunkRowType m)]
+                    -> [TypeRowElem TermConstraint (ThunkRowType m)]
                     -> Checking (CTy m Z)
 kindCheckAnnotation my name outs = do
   trackM "kca"
@@ -1080,17 +1204,19 @@ kindCheckRow' :: forall m n
               -> Endz n -- kind outports so far
               -> VEnv -- from string variable names to VPar's
               -> (Name, Int) -- node name and next free input (under to 'kindCheck' a type)
-              -> [(PortName, ThunkRowType m)]
+              -> [TypeRowElem TermConstraint (ThunkRowType m)]
               -> Checking (Int, VEnv, Some (Endz :* Ro m n))
 kindCheckRow' _ ez env (_,i) [] = pure (i, env, Some (ez :* R0))
-kindCheckRow' Braty (ny :* s) env (name,i) ((p, Left k):rest) = do -- s is Stack Z n
+
+kindCheckRow' my nys env (name, i) ((Anon ty):rest) = kindCheckRow' my nys env (name, i) ((Named ('_':show i) ty):rest)
+kindCheckRow' Braty (ny :* s) env (name,i) ((Named p (Left k)):rest) = do -- s is Stack Z n
   let dangling = Ex name (ny2int ny)
   req (Declare (ExEnd dangling) Braty (Left k) Definable) -- assume none are SkolemConst??
   env <- pure $ M.insert (plain p) [(NamedPort dangling p, Left k)] env
   (i, env, ser) <- kindCheckRow' Braty (Sy ny :* (s :<< ExEnd dangling)) env (name, i) rest
   case ser of
     Some (s_m :* ro) -> pure (i, env, Some (s_m :* REx (p,k) ro))
-kindCheckRow' my ez@(ny :* s) env (name, i) ((p, bty):rest) = case (my, bty) of
+kindCheckRow' my ez@(ny :* s) env (name, i) ((Named p bty):rest) = case (my, bty) of
   (Braty, Right ty) -> helper ty (Star [])
   (Kerny, ty) -> helper ty (Dollar [])
 
@@ -1229,6 +1355,9 @@ abstractPattern my (dangling, bty) pat@(PCon pcon abst) = case (my, bty) of
                                                      ,"with type"
                                                      ,show ty])
 
+  -- N.B. We desperately want to delete these functions and have Let binding use
+  -- the normal SolvePatterns logic, so we haven't bothered to solve equations
+  -- from the CArgs here.
   abstractCon :: Modey m
               -> (QualName -> QualName -> Checking (CtorArgs m))
               -> (QualName, [Val Z])
diff --git a/brat/Brat/Checker/Arithmetic.hs b/brat/Brat/Checker/Arithmetic.hs
new file mode 100644
index 00000000..abdc15e6
--- /dev/null
+++ b/brat/Brat/Checker/Arithmetic.hs
@@ -0,0 +1,137 @@
+module Brat.Checker.Arithmetic where
+
+import Data.Maybe (fromMaybe)
+import qualified Data.Set as S
+
+import Brat.Syntax.Value
+
+nsConst :: Integer -> NumSum var
+nsConst n = NumSum n []
+
+nsVar :: var -> NumSum var
+nsVar v = NumSum 0 [(Linear v, 1)]
+
+nsMul :: NumSum var -> Integer -> NumSum var
+nsMul _ 0 = NumSum 0 []
+nsMul (NumSum n xs) m = NumSum (n*m) [(x, k*m) | (x, k) <- xs]
+
+(-/) :: Integer -> Integer -> Integer
+a -/ b = case a-b of
+    x | x >0 -> x
+    _ -> 0
+
+type Eqn var = (NumSum var, NumSum var)
+
+simplify :: Ord var => Eqn var -> Eqn var
+simplify (NumSum n xs, NumSum m ys) = minOnLeft $ defactor (NumSum (n -/ m) xs', NumSum (m -/ n) ys')
+ where
+  Pullbacks xs' _ ys' = pullbacks xs ys
+
+  defactor (NumSum n xs, NumSum m ys) = (NumSum (n `div` g) [(x, k `div` g) | (x, k) <- xs]
+                                  ,NumSum (m `div` g) [(y, k `div` g) | (y, k) <- ys]
+                                  )
+   where
+    g = foldr gcd 0 (n : m : map snd (xs ++ ys))
+
+  minOnLeft (s1@(NumSum _ []), s2@(NumSum _ (_:_))) = (s2, s1)
+  minOnLeft (s1@(NumSum _ (x:_)), s2@(NumSum _ (y:_))) | y<x = (s2, s1)
+  minOnLeft eqn = eqn
+
+data Pullbacks m = Pullbacks {
+    leftDiff :: m,
+    common :: m,
+    rightDiff :: m
+  }
+
+class (Eq m, Monoid m) => PullbackMonoid m where
+  pullbacks :: m -> m -> Pullbacks m
+
+min_with_diffs :: Integer -> Integer -> Pullbacks Integer
+min_with_diffs x y = let m = min x y in Pullbacks (x - m) m (y - m) -- if x < y then (0, x, y-x) else (x-y, y, 0)
+
+instance Ord thing => PullbackMonoid [(thing, Integer)] where
+  pullbacks [] ys = Pullbacks [] [] ys
+  pullbacks xs [] = Pullbacks xs [] []
+  pullbacks xxs@((x, n):xs) yys@((y, m):ys) = case compare x y of
+        LT -> let Pullbacks {..} = pullbacks xs yys in Pullbacks {leftDiff=(x,n):leftDiff, ..}
+        EQ -> let Pullbacks px pc py = pullbacks xs ys
+                  Pullbacks qx qc qy = min_with_diffs n m
+                  cons_non0 (t,q) ts = if q==0 then ts else (t,q):ts
+               in Pullbacks {
+                    leftDiff = cons_non0 (x, qx) px,
+                    common = cons_non0 (x, qc) pc,
+                    rightDiff = cons_non0 (y, qy) py
+               }
+        GT -> let Pullbacks {..} = pullbacks xxs ys in Pullbacks {rightDiff = (y,m):rightDiff, ..}
+
+instance Ord var => PullbackMonoid (NumSum var) where
+    pullbacks (NumSum n xs) (NumSum m ys) =
+        let Pullbacks x c y = min_with_diffs n m
+            Pullbacks {..} = pullbacks xs ys
+        in Pullbacks (NumSum x leftDiff) (NumSum c common) (NumSum y rightDiff)
+
+-- Might not be necessary to sort vars but it's easy enough
+vars :: Ord var => Eqn var -> [Monotone var]
+vars (NumSum _ xs, NumSum _ ys) = merge (map fst xs) (map fst ys)
+ where
+  merge [] ys = ys
+  merge xs [] = xs
+  merge xxs@(x:xs) yys@(y:ys) = if x<y then x:(merge xs yys) else y:(merge xxs ys)
+
+eFlip :: Eqn var -> Eqn var
+eFlip (s1, s2) = (s2, s1)
+
+eAdd :: Ord var => Eqn var -> Eqn var -> Eqn var
+eAdd (s1, s2) (s1', s2') = simplify (s1 <> s1', s2 <> s2')
+
+eSub :: Ord var => Eqn var -> Eqn var -> Eqn var
+eSub e1 e2 = e1 `eAdd` (eFlip e2)
+
+eMul :: Eqn var -> Integer -> Eqn var
+eMul (s1, s2) m | m >= 0 = (s1 `multNumSum` m, s2 `multNumSum` m)
+eMul e m = eMul (eFlip e) (-m)
+
+lweight :: Eq var => Eqn var -> Monotone var -> Maybe Integer
+lweight (NumSum _ ts, _) v = lookup ts
+ where
+  lookup ((x,n):_) | x == v = Just n
+  lookup (_:xs) = lookup xs
+  lookup [] = Nothing
+
+sweight :: Eq var => Eqn var -> Monotone var -> Integer
+sweight e v = fromMaybe (fromMaybe 0 $ lweight (eFlip e) v) $ lweight e v
+
+gauss_elim :: forall var. Ord var => [Eqn var] -> [Eqn var]
+gauss_elim eqns = fst $ foldl elim ([], eqns) (S.toList $ S.fromList $ mconcat $ map vars eqns)
+ where
+  -- first element of pair are reduced: each Eqn is the only one mentioning its first variable
+  -- in second element of pair, no Eqn mentions any variable that is first var of any reduced
+  -- variable identifies what to reduce, i.e. 'elim' constructs an equation where that var is first
+  elim :: ([Eqn var], [Eqn var]) -> Monotone var -> ([Eqn var], [Eqn var])
+  elim (redns, eqns) v = (e1:(map rm_v redns), (map rm_v eqns))
+   where
+    (e1, w1) = foldl1 eqn_one ((redns ++ eqns) >>= v_on_left)
+    v_on_left :: Eqn var -> [(Eqn var, Integer)]
+    v_on_left e = case sweight e v of
+        0 -> []
+        w | w<0 -> [(eFlip e, -w)]
+          | otherwise -> [(e, w)]
+
+    -- make an equation containing exactly one 'v'
+    -- both arguments, and result, are (equation, number of 'v's)
+    --     where equation has 'v' on LHS, and number is strictly positive
+    eqn_one :: (Eqn var, Integer) -> (Eqn var, Integer) -> (Eqn var, Integer)
+    eqn_one (e, 1) _ = (e, 1)
+    eqn_one e@(_, w) e2@(_, w2) | w2 > w = eqn_one e (e2 `vlsub` e)
+                                | w2 == w = e -- gcd is >1, best we can do
+                                | otherwise = eqn_one (e `vlsub` e2) e2
+    vlsub :: (Eqn var, Integer) -> (Eqn var, Integer) -> (Eqn var, Integer)
+    vlsub (e1, w1) (e2, w2) = let e = e1 `eSub` e2 -- puts min var on left...perhaps we shouldn't?
+                              in (,w1-w2) $ case sweight e v of
+                                              w | w<0 -> eFlip e
+                                                | w>0 -> e
+
+    -- remove 'v' from equation 'e', where 'e' might be any equation
+    rm_v e = let w = sweight e v
+                 gw = gcd w w1
+              in if w==0 then e else (e `eMul` (w1 `div` gw)) `eSub` (e1 `eMul` (w `div` gw))
diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs
index 618fc4f6..deab00c5 100644
--- a/brat/Brat/Checker/Helpers.hs
+++ b/brat/Brat/Checker/Helpers.hs
@@ -23,6 +23,7 @@ import Control.Monad.Freer
 import Control.Monad.State.Lazy (StateT(..), runStateT)
 import Data.Bifunctor
 import Data.Foldable (foldrM)
+import Data.Kind (Type)
 import Data.List (partition)
 import Data.Maybe (isJust)
 import Data.Type.Equality (TestEquality(..), (:~:)(..))
@@ -46,7 +47,7 @@ simpleCheck my ty tm = case (my, ty) of
     else isSkolem e >>= \case
       SkolemConst -> throwLeft $ helper Braty ty tm
       Definable -> do
-        mkYield "simpleCheck" (S.singleton e)
+        mkYield (NeedToKnow e) "simpleCheck" (S.singleton e)
         ty <- eval S0 ty
         simpleCheck Braty ty tm
   _ -> throwLeft $ helper my ty tm
@@ -109,13 +110,7 @@ pullPortsRow :: Show ty
              -> Checking [(NamedPort e, ty)]
 pullPortsRow = pullPorts (portName . fst) showRow
 
-pullPortsSig :: Show ty
-             => [PortName]
-             -> [(PortName, ty)]
-             -> Checking [(PortName, ty)]
-pullPortsSig = pullPorts fst showSig
-
-pullPorts :: forall a
+pullPorts :: forall a ty
            . (a -> PortName) -- A way to get a port name for each element
           -> ([a] -> String) -- A way to print the list
           -> [PortName] -- Things to pull to the front
@@ -133,10 +128,7 @@ pullPorts toPort showFn to_pull types =
 
 ensureEmpty :: Show ty => String -> [(NamedPort e, ty)] -> Checking ()
 ensureEmpty _ [] = pure ()
-ensureEmpty str xs = err $ InternalError $ "Expected empty " ++ str ++ ", got:\n  " ++ showSig (rowToSig xs)
-
-rowToSig :: Traversable t => t (NamedPort e, ty) -> t (PortName, ty)
-rowToSig = fmap $ first portName
+ensureEmpty str xs = err $ InternalError $ "Expected empty " ++ str ++ ", got:\n  " ++ showRow xs
 
 showMode :: Modey m -> String
 showMode Braty = ""
@@ -150,14 +142,21 @@ type family ThunkRowType (m :: Mode) where
   ThunkRowType Brat = KindOr (Term Chk Noun)
   ThunkRowType Kernel = Term Chk Noun
 
+simpleTypeRow :: [(PortName, ty)] -> [TypeRowElem a ty]
+simpleTypeRow = fmap aux where aux (p, ty) = Named p ty
+
 mkThunkTy :: Modey m
           -> ThunkFCType m
           -> [(PortName, ThunkRowType m)]
           -> [(PortName, ThunkRowType m)]
           -> Term Chk Noun
 -- mkThunkTy Braty fc ss ts = C (WC fc (ss :-> ts))
-mkThunkTy Braty _ ss ts = C (ss :-> ts)
-mkThunkTy Kerny () ss ts = K (ss :-> ts)
+mkThunkTy Braty _ ss ts = C (simpleTypeRow ss :-> simpleTypeRow ts)
+mkThunkTy Kerny () ss ts = K (simpleTypeRow ss :-> simpleTypeRow ts)
+
+data RowPolarity :: Type -> Type where
+   InputRow :: RowPolarity InPort
+   OutputRow :: RowPolarity OutPort
 
 anext :: forall m i j k
        . EvMode m
@@ -183,8 +182,8 @@ anext' :: forall m i j k
 anext' str th vals0 ins outs skol = do
   node <- req (Fresh str) -- Pick a name for the thunk
   -- Use the new name to generate Ends with which to instantiate types
-  (unders, vals1) <- endPorts node InEnd In 0 vals0 ins
-  (overs, vals2)  <- endPorts node ExEnd Ex 0 vals1 outs
+  (unders, vals1) <- endPorts node InputRow 0 vals0 ins
+  (overs, vals2)  <- endPorts node OutputRow 0 vals1 outs
   () <- sequence_ $
         [ declareTgt tgt (modey @m) ty | (tgt, ty) <- unders ] ++
         [ req (Declare (ExEnd (end src)) (modey @m) ty skol) | (src, ty) <- overs ]
@@ -204,25 +203,35 @@ mkNode Kerny = KernelNode
 
 type Endz = Ny :* Stack Z End
 
+port2End :: RowPolarity port -> port -> End
+port2End InputRow = InEnd
+port2End OutputRow = ExEnd
+
+mkPort :: RowPolarity port -> Name -> Int -> port
+mkPort InputRow = In
+mkPort OutputRow = Ex
+
 -- endPorts instantiates the de Bruijn variables in a row with Ends
 endPorts :: forall m i j port
           . EvMode m
-         => Name -> (port -> End) -> (Name -> Int -> port)
+         => Name
+         -> RowPolarity port
          -> Int -- Next free port on the node
          -> (Semz i, Some Endz)
          -> Ro m i j
          -> Checking ([(NamedPort port, BinderType m)], (Semz j, Some Endz))
-endPorts _ _ _ _ stuff R0 = pure ([], stuff)
-endPorts node port2End mkPort n (ga, ez) (RPr (p,ty) ro) = do
+endPorts _ _ _ stuff R0 = pure ([], stuff)
+endPorts node rowPol n (ga, ez) (RPr (p,ty) ro) = do
   ty <- eval ga ty
-  (row, stuff) <- endPorts node port2End mkPort (n + 1) (ga, ez) ro
-  pure ((NamedPort (mkPort node n) p, tyBinder @m ty):row, stuff)
-endPorts node port2End mkPort n (ga, Some (ny :* endz)) (REx (p, k) ro) = do
-  let port = mkPort node n
-  let end = port2End port
-  (row, stuff) <- endPorts node port2End mkPort (n + 1)
+  (row, stuff) <- endPorts node rowPol (n + 1) (ga, ez) ro
+  pure ((NamedPort (mkPort rowPol node n) p, tyBinder @m ty):row, stuff)
+endPorts node rowPol n (ga, Some (ny :* endz)) (REx (p, k) ro) = do
+  let port = mkPort rowPol node n
+  let end = port2End rowPol port
+  (row, stuff) <- endPorts node rowPol (n + 1)
                   (ga :<< SApp (SPar end) B0, Some (Sy ny :* (endz :<< end))) ro
   pure ((NamedPort port p, Left k):row, stuff)
+
 next :: String -> NodeType Brat -> (Semz i, Some Endz)
      -> Ro Brat i j
      -> Ro Brat j k
@@ -525,13 +534,16 @@ makeHalf (ExEnd e) = do
   pure (toEnd halveOut)
 
 makePred :: End -> Checking End
-makePred (InEnd e) = do
-  (succIn, succOut) <- buildAdd 1
+makePred = makeSub 1
+
+makeSub :: Integer -> End -> Checking End
+makeSub n (InEnd e) = do
+  (succIn, succOut) <- buildAdd n
   req (Wire (end succOut, TNat, e))
   defineTgt' "Helpers"(NamedPort e "") (VNum (nVar (VPar (toEnd succOut))))
   pure (toEnd succIn)
-makePred (ExEnd e) = do
-  (predIn, predOut) <- buildSub 1
+makeSub n (ExEnd e) = do
+  (predIn, predOut) <- buildSub n
   req (Wire (e, TNat, end predIn))
   defineSrc (NamedPort e "") (VNum (nVar (VPar (toEnd predIn))))
   pure (toEnd predOut)
@@ -731,7 +743,7 @@ mineToSolve = allowedToSolve <$> whoAmI
 -- defined is passed in.
 awaitTypeDefinition :: Val Z -> Checking (Val Z)
 awaitTypeDefinition ty = eval S0 ty >>= \case
-  VApp (VPar e) _ -> mkYield "awaitTypeDefinition" (S.singleton e) >> awaitTypeDefinition ty
+  VApp (VPar e) _ -> mkYield (NeedToKnow e) "awaitTypeDefinition" (S.singleton e) >> awaitTypeDefinition ty
   ty -> pure ty
 
 mkGraph :: TypeKind -> Val Z -> Checking Src
diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs
index 12f15aca..6ae05a86 100644
--- a/brat/Brat/Checker/Monad.hs
+++ b/brat/Brat/Checker/Monad.hs
@@ -22,18 +22,18 @@ import Data.List (intercalate)
 import qualified Data.Map as M
 import qualified Data.Set as S
 
--- import Debug.Trace
+import Debug.Trace
 
 -- Used for messages about thread forking / spawning
 thTrace = const id
 --thTrace = trace
 
 trackM :: Monad m => String -> m ()
-trackM = const (pure ())
---trackM = traceM
+--trackM = const (pure ())
+trackM = traceM
 
-track = const id
---track = trace
+--track = const id
+track = trace
 trackShowId x = track (show x) x
 
 -- Data for using a type alias. E.g.
@@ -82,8 +82,8 @@ data Context = Ctx { globalVEnv :: VEnv
 mkFork :: String -> Free sig () -> Free sig ()
 mkFork d par = thTrace ("Forking " ++ d) $ Fork d par $ pure ()
 
-mkYield :: String -> S.Set End -> Free sig ()
-mkYield desc es = thTrace ("Yielding in " ++ desc ++ "\n  " ++ show es) $ Yield (AwaitingAny es) (\_ -> trackM ("woke up " ++ desc) >> Ret ())
+mkYield :: ErrorMsg -> String -> S.Set End -> Free sig ()
+mkYield err desc es = thTrace ("Yielding in " ++ desc ++ "\n  " ++ show es) $ Yield err (AwaitingAny es) (\n -> trackM ("woke up " ++ desc ++ "\n" ++ show n) >> Ret ())
 
 -- Commands for synchronous operations
 data CheckingSig ty where
@@ -121,13 +121,14 @@ data CheckingSig ty where
   AskDynamics :: CheckingSig (M.Map InPort FC)
   AddCapture :: Name -> (QualName, [(Src, BinderType Brat)]) -> CheckingSig ()
 
+
 wrapper :: (forall a. CheckingSig a -> Checking (Maybe a)) -> Checking v -> Checking v
 wrapper _ (Ret v) = Ret v
 wrapper f (Req s k) = f s >>= \case
   Just v -> wrapper f (k v)
   Nothing -> Req s (wrapper f . k)
 wrapper f (Define lbl v e k) = Define lbl v e (wrapper f . k)
-wrapper f (Yield st k) = Yield st (wrapper f . k)
+wrapper f (Yield err st k) = Yield err st (wrapper f . k)
 wrapper f (Fork d par c) = Fork d (wrapper f par) (wrapper f c)
 
 wrapper2 :: (forall a. CheckingSig a -> Maybe a) -> Checking v -> Checking v
@@ -238,7 +239,7 @@ localKVar env (Req KDone k) = case [ x | (x,(One,_)) <- M.assocs env ] of
                                               ]
 localKVar env (Req r k) = Req r (localKVar env . k)
 localKVar env (Define lbl e v k) = Define lbl e v (localKVar env . k)
-localKVar env (Yield st k) = Yield st (localKVar env . k)
+localKVar env (Yield err st k) = Yield err st (localKVar env . k)
 localKVar env (Fork desc par c) =
   -- can't send end both ways, so until we can join (TODO), restrict Forks to local scope
   thTrace ("Spawning(LKV) " ++ desc) $ localKVar env $ par *> c
@@ -253,7 +254,7 @@ catchErr (Ret t) = Ret (Right t)
 catchErr (Req (Throw e) _) = pure $ Left e
 catchErr (Req r k) = Req r (catchErr . k)
 catchErr (Define lbl e v k) = Define lbl e v (catchErr . k)
-catchErr (Yield st k) = Yield st (catchErr . k)
+catchErr (Yield err st k) = Yield err st (catchErr . k)
 catchErr (Fork desc par c) = thTrace ("Spawning(catch) " ++ desc) $ catchErr $ par *> c
 
 handler :: Free CheckingSig v
@@ -347,10 +348,13 @@ handler (Define lbl end v k) ctx g = let st@Store{typeMap=tm, valueMap=vm} = sto
                                                  (M.delete inport (dynamicSet ctx))
                                         Nothing -> dynamicSet ctx
                           }) g
-handler (Yield Unstuck k) ctx g = handler (k mempty) ctx g
-handler (Yield (AwaitingAny ends) _k) ctx _ = Left $ dumbErr $ TypeErr $ unlines $
+handler (Yield _err Unstuck k) ctx g = handler (k mempty) ctx g
+handler (Yield err (AwaitingAny ends) _k) ctx _ = Left $ dumbErr $ Both
+                                                                   (TypeErr $ unlines $
   ("Typechecking blocked on:":(show <$> S.toList ends))
-  ++ "":"Dynamic set is":(show <$> M.keys (dynamicSet ctx)) ++ ["Try writing more types! :-)"]
+  ++ "":"Dynamic set is":(show <$> M.keys (dynamicSet ctx))
+  ++ "":["Try writing more types! :-)"])
+ err
 handler (Fork desc par c) ctx g = handler (thTrace ("Spawning " ++ desc) $ par *> c) ctx g
 
 type Checking = Free CheckingSig
@@ -404,7 +408,7 @@ localNS ns (Req (SplitNS str) k) = let (subSpace, newRoot) = split str ns in
 localNS ns (Req AskNS k) = localNS ns (k (fst ns))
 localNS ns (Req c k) = Req c (localNS ns . k)
 localNS ns (Define lbl e v k) = Define lbl e v (localNS ns . k)
-localNS ns (Yield st k) = Yield st (localNS ns . k)
+localNS ns (Yield err st k) = Yield err st (localNS ns . k)
 localNS ns (Fork desc par c) = let (subSpace, newRoot) = split desc ns in
                                  Fork desc (localNS subSpace par) (localNS newRoot c)
 
diff --git a/brat/Brat/Checker/SolveConstraints.hs b/brat/Brat/Checker/SolveConstraints.hs
new file mode 100644
index 00000000..571c325d
--- /dev/null
+++ b/brat/Brat/Checker/SolveConstraints.hs
@@ -0,0 +1,66 @@
+module Brat.Checker.SolveConstraints where
+
+import Brat.Checker.Helpers (mineToSolve)
+import Brat.Checker.Monad (Checking)
+import Brat.Checker.SolveNumbers (unifyNum, demandAtLeast)
+import Brat.Syntax.Value
+import Hasochism (N(..))
+
+type Eqn v = (NumSum v, NumSum v)
+
+(-/) :: Integer -> Integer -> Integer
+a -/ b = case a-b of
+    x | x >0 -> x
+    _ -> 0
+
+div0 :: Integer -> Integer -> Integer
+div0 0 _ = 0
+div0 a b = a `div` b
+
+
+simplify :: Ord v => Eqn v -> Eqn v
+simplify (NumSum n xs, NumSum m ys) = cas
+  (NumSum (n' `div0` g) (xs' `divs` g)
+  ,NumSum (m' `div0` g) (ys' `divs` g)
+  )
+ where
+  n' = n -/ m
+  m' = m -/ n
+
+  g = g' `gcd` n' `gcd` m'
+
+  (g', xs', ys') = aux xs ys
+
+  consNon0 (t,q) ts = if q==0 then ts else (t,q):ts
+
+  aux :: Ord v => [(v, Integer)] -> [(v, Integer)] -> (Integer, [(v, Integer)], [(v, Integer)])
+  aux [] ys = (foldr gcd 0 (snd <$> ys), [], ys)
+  aux xs [] = (foldr gcd 0 (snd <$> xs), xs, [])
+  aux xxs@((x, n):xs) yys@((y, m):ys) = case compare x y of
+    LT -> let (g, xs', ys') = aux xs yys in (gcd g n, (x, n):xs', ys')
+    EQ -> let (g, xs', ys') = aux xs ys
+              n' = n -/ m
+              m' = m -/ n
+          in  (g `gcd` n' `gcd` m', consNon0 (x, n') xs', consNon0 (y, m') ys')
+    GT -> let (g, xs', ys') = aux xxs ys in (gcd g m, xs', (y, m):ys')
+
+  divs :: [(v, Integer)] -> Integer -> [(v, Integer)]
+  divs xs g = fmap (fmap (`div0` g)) xs
+
+  cas :: Ord v => Eqn v -> Eqn v
+  cas (lhs,rhs)
+   | lhs <= rhs = (lhs,rhs)
+   | otherwise = (rhs, lhs)
+
+fulbournConstraint :: Eqn (VVar Z) -> Checking ()
+fulbournConstraint (lhs,rhs)
+ | Just lhs <- numSumToNum lhs
+ , Just rhs <- numSumToNum rhs = do
+   mine <- mineToSolve
+   unifyNum mine lhs rhs
+fulbournConstraint (lhs, NumSum n _)
+ | Just lnv <- numSumToNum lhs = demandAtLeast n lnv
+fulbournConstraint (NumSum n _, rhs)
+ | Just rnv <- numSumToNum rhs = demandAtLeast n rnv
+
+fulbournConstraint _ = pure ()
diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs
index 2631a4f6..f3bd2554 100644
--- a/brat/Brat/Checker/SolveHoles.hs
+++ b/brat/Brat/Checker/SolveHoles.hs
@@ -93,7 +93,7 @@ typeEqEta tm stuff@(ny :* _ks :* _sems) _ k exp act = do
   unless (exp == act) $ case flexes act ++ flexes exp of
     [] -> typeEqRigid tm stuff k exp act -- easyish, both rigid i.e. already defined
     -- tricky: must wait for one or other to become more defined
-    es -> mkYield "typeEqEta" (S.fromList es) >> typeEq' tm stuff k exp act
+    es@(e:_) -> mkYield (NeedToKnow e) "typeEqEta" (S.fromList es) >> typeEq' tm stuff k exp act
 
 typeEqs :: String -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n -> [TypeKind] -> [Val n] -> [Val n] -> Checking ()
 typeEqs _ _ [] [] [] = pure ()
diff --git a/brat/Brat/Checker/SolveNumbers.hs b/brat/Brat/Checker/SolveNumbers.hs
index 8089c506..2c1550ce 100644
--- a/brat/Brat/Checker/SolveNumbers.hs
+++ b/brat/Brat/Checker/SolveNumbers.hs
@@ -1,4 +1,4 @@
-module Brat.Checker.SolveNumbers (unifyNum) where
+module Brat.Checker.SolveNumbers (unifyNum, demandAtLeast) where
 
 import Brat.Checker.Monad
 import Brat.Checker.Helpers
@@ -105,11 +105,11 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
        | Just _ <- mine e' -> do
           req (Wire (dangling, TNat, p))
           defineSrc' ("flex-flex In Ex") (NamedPort dangling "") (VNum (nVar v))
-       | otherwise -> mkYield "flexFlex" (S.singleton e) >> unifyNum mine (nVar v) (nVar v')
+       | otherwise -> mkYield (NeedToKnow e) "flexFlex" (S.singleton e) >> unifyNum mine (nVar v) (nVar v')
       (VPar e@(InEnd p), VPar e'@(InEnd p'))
        | Just _ <- mine e -> defineTgt' "flex-flex In In1" (NamedPort p "") (VNum (nVar v'))
        | Just _ <- mine e' -> defineTgt' "flex-flex In In0"(NamedPort p' "") (VNum (nVar v))
-       | otherwise -> mkYield "flexFlex" (S.fromList [e, e']) >> unifyNum mine (nVar v) (nVar v')
+       | otherwise -> mkYield (Both (NeedToKnow e) (NeedToKnow e')) "flexFlex" (S.fromList [e, e']) >> unifyNum mine (nVar v) (nVar v')
 
   lhsStrictMono :: StrictMono (VVar Z) -> NumVal (VVar Z) -> Checking ()
   lhsStrictMono (StrictMono 0 mono) num = lhsMono mono num
@@ -123,19 +123,19 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
   lhsMono lhs@(Linear (VPar e)) num | [e'] <- numVars num, e == e' = case num of
     (NumValue 0 (StrictMonoFun sm)) -> case anyDoubsAnyFulls sm of
       (True, _) -> lhsMono lhs (nConstant 0)
-      (False, True) -> mkYield "lhsMono2Sols" (S.singleton e) >>
+      (False, True) -> mkYield (NeedToKnow e) "lhsMono2Sols" (S.singleton e) >>
                        unifyNum mine (nVar (VPar e)) num
       (False, False) -> pure ()
     _ -> err . UnificationError $ "Can't make " ++ show e ++ " = " ++ show num
   lhsMono (Linear (VPar e)) num = case mine e of
     Just loc -> loc -! solveNumMeta mine e num
-    _ -> mkYield "lhsMono" (S.singleton e) >>
+    _ -> mkYield (NeedToKnow e) "lhsMono" (S.singleton e) >>
          unifyNum mine (nVar (VPar e)) num
   lhsMono (Full sm) (NumValue 0 (StrictMonoFun (StrictMono 0 (Full sm'))))
     = lhsFun00 (StrictMonoFun sm) (NumValue 0 (StrictMonoFun sm'))
   lhsMono m@(Full _) (NumValue 0 gro) = trail "lhsMono swaps" $ lhsFun00 gro (NumValue 0 (StrictMonoFun (StrictMono 0 m)))
   lhsMono (Full sm) (NumValue up gro) = do
-    smPred <- traceChecking "lhsMono demandSucc" demandSucc (NumValue 0 (StrictMonoFun sm))
+    smPred <- traceChecking "lhsMono demandSucc" (demandSucc mine) (NumValue 0 (StrictMonoFun sm))
     _ <- numEval S0 sm
     -- trailM $ "succ now " ++ show (quoteNum Zy sm)
     unifyNum mine (n2PowTimes 1 (nFull smPred)) (NumValue (up - 1) gro)
@@ -152,34 +152,6 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
     _ -> err . UnificationError $ "Couldn't force " ++ show n ++ " to be 0"
   demand0 n = err . UnificationError $ "Couldn't force " ++ show n ++ " to be 0"
 
-  -- Complain if a number isn't a successor, else return its predecessor
-  demandSucc :: NumVal (VVar Z) -> Checking (NumVal (VVar Z))
-      --   2^k * x
-      -- = 2^k * (y + 1)
-      -- = 2^k + 2^k * y
-      -- Hence, the predecessor is (2^k - 1) + (2^k * y)
-  demandSucc (NumValue k x) | k > 0 = pure (NumValue (k - 1) x)
-  demandSucc (NumValue 0 (StrictMonoFun (mono@(StrictMono k (Linear (VPar e))))))
-    | Just loc <- mine e = do
-      pred <- loc -! traceChecking "makePred" makePred e
-      pure (nPlus ((2^k) - 1) (nVar (VPar pred)))
-
-  --   2^k * full(n + 1)
-  -- = 2^k * (1 + 2 * full(n))
-  -- = 2^k + 2^(k + 1) * full(n)
-
-    | otherwise = do
-      mkYield "demandSucc" (S.singleton e)
-      nv <- quoteNum Zy <$> numEval S0 mono
-      demandSucc nv
-
-  -- if it's not "mine" should we wait?
-  demandSucc (NumValue 0 (StrictMonoFun (StrictMono k (Full nPlus1)))) = do
-    n <- traceChecking "demandSucc" demandSucc (NumValue 0 (StrictMonoFun nPlus1))
-    -- foo <- numEval S0 x
-    -- trailM $ "ds: " ++ show x ++ " -> " ++ show (quoteNum Zy foo)
-    pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes (k + 1) $ nFull n
-  demandSucc n = err . UnificationError $ "Couldn't force " ++ show n ++ " to be a successor"
 
   -- Complain if a number isn't even, otherwise return half
   demandEven :: NumVal (VVar Z) -> Checking (NumVal (VVar Z))
@@ -196,7 +168,7 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
           half <- traceChecking "makeHalf" makeHalf e
           pure (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear (VPar half)))))
         | otherwise -> do
-          mkYield "evenGro" (S.singleton e)
+          mkYield (NeedToKnow e) "evenGro" (S.singleton e)
           nv <- quoteNum Zy <$> numEval S0 mono
           demandEven nv
       Full sm -> nConstant 0 <$ demand0 (NumValue 0 (StrictMonoFun sm))
@@ -205,5 +177,41 @@ unifyNum' mine (NumValue lup lgro) (NumValue rup rgro)
     -- Check a numval is odd, and return its rounded down half
     oddGro :: NumVal (VVar Z) -> Checking (NumVal (VVar Z))
     oddGro x = do
-     pred <- demandSucc x
+     pred <- demandSucc mine x
      demandEven pred
+
+-- Complain if a number isn't a successor, else return its predecessor
+demandSucc :: (End -> Maybe String) -> NumVal (VVar Z) -> Checking (NumVal (VVar Z))
+    --   2^k * x
+    -- = 2^k * (y + 1)
+    -- = 2^k + 2^k * y
+    -- Hence, the predecessor is (2^k - 1) + (2^k * y)
+demandSucc _ (NumValue k x) | k > 0 = pure (NumValue (k - 1) x)
+demandSucc mine (NumValue 0 (StrictMonoFun (mono@(StrictMono k (Linear (VPar e))))))
+  | Just loc <- mine e = do
+    pred <- loc -! traceChecking "makePred" makePred e
+    pure (nPlus ((2^k) - 1) (nVar (VPar pred)))
+
+--   2^k * full(n + 1)
+-- = 2^k * (1 + 2 * full(n))
+-- = 2^k + 2^(k + 1) * full(n)
+
+  | otherwise = do
+    mkYield (NeedToKnow e) "demandSucc" (S.singleton e)
+    nv <- quoteNum Zy <$> numEval S0 mono
+    demandSucc mine nv
+
+-- if it's not "mine" should we wait?
+demandSucc mine (NumValue 0 (StrictMonoFun (StrictMono k (Full nPlus1)))) = do
+  n <- traceChecking "demandSucc" (demandSucc mine) (NumValue 0 (StrictMonoFun nPlus1))
+  -- foo <- numEval S0 x
+  -- trailM $ "ds: " ++ show x ++ " -> " ++ show (quoteNum Zy foo)
+  pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes (k + 1) $ nFull n
+demandSucc _ n = err . UnificationError $ "Couldn't force " ++ show n ++ " to be a successor"
+
+demandAtLeast :: Integer -> NumVal (VVar Z) -> Checking ()
+demandAtLeast 0 _ = pure ()
+demandAtLeast n nv = do
+  mine <- mineToSolve
+  nv <- demandSucc mine nv
+  demandAtLeast (n - 1) nv
diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs
index cd49a366..672ae729 100644
--- a/brat/Brat/Checker/SolvePatterns.hs
+++ b/brat/Brat/Checker/SolvePatterns.hs
@@ -23,10 +23,13 @@ import Brat.Syntax.Port (toEnd)
 import Control.Monad (unless)
 import Data.Bifunctor (first)
 import Data.Functor ((<&>))
+import Data.List (isPrefixOf)
 import qualified Data.Map as M
 import Data.Maybe (fromJust)
 import Data.Type.Equality ((:~:)(..), testEquality)
 
+--import Debug.Trace
+
 -- Refine clauses from function definitions (and potentially future case statements)
 -- by processing each one in sequence. This will involve repeating tests for various
 -- branches, the removal of which is a future optimisation.
@@ -71,15 +74,18 @@ solve my ((src, DontCare):p) = do
     Braty -> do
       ty <- typeOfSrc Braty src
       (tests, sol) <- solve my p
-      case ty of
-        Right _ -> pure (tests, sol)
-        -- Kinded things might be used to solve hopes. We pass them through so
-        -- that we can do the proper wiring in this case
-        Left _ -> pure (tests, ('_':portName src, (src, ty)):sol)
+      -- Kinded things might be used to solve hopes. We pass them through so
+      -- that we can do the proper wiring in this case.
+      -- N.B. When we automatically create a variable name, we add `'`
+      -- characters to the later instances in the row to avoid name collisions.
+      let newName = '_':portName src
+      let bump x = if newName `isPrefixOf` x then x ++ "'" else x
+      --traceM ("Adding " ++ newName ++ " :: " ++ show ty)
+      pure (tests, (newName, (src, ty)):(first bump <$> sol))
 solve my ((src, Bind x):p) = do
-  ty <- typeOfSrc my src
+  ty <- typeOfSrc my src -- TODO: Check if VEqn
   (tests, sol) <- solve my p
-  pure (tests, (x, (src, ty)):sol)
+  pure (tests, (x, (src, ty)):sol) --
 solve my ((src, Lit tm):p) = do
   ty <- typeOfSrc my src
   -- let's just check the literal is ok at this type, and maybe learn a number
diff --git a/brat/Brat/Constructors.hs b/brat/Brat/Constructors.hs
index 16b196bc..5f3f33d6 100644
--- a/brat/Brat/Constructors.hs
+++ b/brat/Brat/Constructors.hs
@@ -30,6 +30,7 @@ defaultConstructors = M.fromList
   [(CSucc, M.fromList
      [(CNat, CArgs [] Zy R0 (RPr ("value", TNat) R0))
      ,(CInt, CArgs [] Zy R0 (RPr ("value", TInt) R0))
+     ,(CThin, CArgs [VPNum (NP1Plus NPVar), VPNum (NP1Plus NPVar)] (Sy (Sy Zy)) (REx ("wee", Nat) (REx ("big", Nat) R0)) (RPr ("thinning", TThin (VNum (nVar (VInx (VS VZ)))) (VNum (nVar (VInx VZ)))) R0))
      ])
   ,(CDoub, M.fromList
      [(CNat, CArgs [] Zy R0 (RPr ("value", TNat) R0))
@@ -38,6 +39,7 @@ defaultConstructors = M.fromList
   ,(CZero, M.fromList
      [(CNat, CArgs [] Zy R0 R0)
      ,(CInt, CArgs [] Zy R0 R0)
+     ,(CThin, CArgs [VPNum NP0, VPNum NP0] Zy R0 R0)
      ])
   ,(CNil, M.fromList
      [(CList, CArgs [VPVar] (Sy Zy) (REx ("elementType", Star []) R0) R0)
@@ -102,6 +104,19 @@ defaultConstructors = M.fromList
         (RPr ("value", VApp (VInx VZ) B0) R0))])
   ,(CTrue, M.fromList [(CBool, CArgs [] Zy R0 R0)])
   ,(CFalse, M.fromList [(CBool, CArgs [] Zy R0 R0)])
+  ,(COmit, M.fromList
+    [(CThin, CArgs [VPNum NPVar, VPNum (NP1Plus NPVar)] (Sy (Sy Zy))
+      -- args to type constructor
+      (REx ("wee", Nat) (REx ("big", Nat) R0)) -- n <= m'
+      -- Args to val constructor
+      (RPr ("thinning", TThin (VNum (nVar (VInx (VS VZ)))) (VNum (nVar (VInx VZ))))
+       (REx ("k", Nat) (RPr ("eq",VEqn
+                                  (NumSum 0 [(Linear (VInx (VS VZ)), 1)]) -- m'
+                                  (NumSum 0 [(Linear (VInx VZ), 1) -- k
+                                            ,(Linear (VInx (VS (VS VZ))), 1) -- n
+                                            ])
+                            ) R0)))
+     )])
   ]
 
 kernelConstructors :: ConstructorMap Kernel
@@ -138,6 +153,7 @@ defaultTypeConstructors = M.fromList
   ,((Brat, CNat),    [])
   ,((Brat, CNil),    [])
   ,((Brat, CCons),   [("head", Star []), ("tail", Star [])])
+  ,((Brat, CThin),   [("wee", Nat), ("big", Nat)])
   ,((Kernel, CQubit), [])
   ,((Kernel, CMoney), [])
   ,((Kernel, CVec), [("X", Dollar []), ("n", Nat)])
diff --git a/brat/Brat/Constructors/Patterns.hs b/brat/Brat/Constructors/Patterns.hs
index 4fd6fac1..86db9abc 100644
--- a/brat/Brat/Constructors/Patterns.hs
+++ b/brat/Brat/Constructors/Patterns.hs
@@ -3,7 +3,7 @@ module Brat.Constructors.Patterns where
 import Brat.QualName
 
 pattern CSucc, CDoub, CFull, CNil, CCons, CSome, CNone, CTrue, CFalse, CZero, CSnoc,
-        CConcatEqEven, CConcatEqOdd, CRiffle :: QualName
+        CConcatEqEven, CConcatEqOdd, CRiffle, CRefl, COmit :: QualName
 pattern CSucc = PrefixName [] "succ"
 pattern CDoub = PrefixName [] "doub"
 pattern CFull = PrefixName [] "full"
@@ -18,8 +18,10 @@ pattern CSnoc = PrefixName [] "snoc"
 pattern CConcatEqEven = PrefixName [] "concatEqEven"
 pattern CConcatEqOdd = PrefixName [] "concatEqOdd"
 pattern CRiffle = PrefixName [] "riffle"
+pattern CRefl = PrefixName [] "refl"
+pattern COmit = PrefixName [] "omit"
 
-pattern CList, CVec, CNat, CInt, COption, CBool, CBit, CFloat, CString :: QualName
+pattern CList, CVec, CNat, CInt, COption, CBool, CBit, CFloat, CString, CEq, CThin :: QualName
 pattern CList = PrefixName [] "List"
 pattern CVec = PrefixName [] "Vec"
 pattern CNat = PrefixName [] "Nat"
@@ -29,6 +31,8 @@ pattern CBool = PrefixName [] "Bool"
 pattern CBit = PrefixName [] "Bit"
 pattern CFloat = PrefixName [] "Float"
 pattern CString = PrefixName [] "String"
+pattern CEq = PrefixName [] "Eq"
+pattern CThin = PrefixName [] "Thin"
 
 pattern CQubit, CMoney :: QualName
 pattern CQubit = PrefixName [] "Qubit"
diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs
index 2546dca3..28d2a698 100644
--- a/brat/Brat/Elaborator.hs
+++ b/brat/Brat/Elaborator.hs
@@ -1,6 +1,6 @@
 module Brat.Elaborator where
 
-import Control.Monad (forM, (>=>))
+import Control.Monad ((>=>))
 import Data.Bifunctor (second)
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Map (empty)
@@ -179,6 +179,7 @@ elaborate' (FAnnotation a ts) = do
   (SomeRaw a) <- elaborate a
   a <- assertChk a
   a <- assertNoun a
+  ts <- fmap (fmap unWC) <$> traverse elabSigElem ts
   pure $ SomeRaw' (a ::::: ts)
 elaborate' (FInto a b) = elaborate' (FApp b a)
 elaborate' (FOf n e) = do
@@ -187,14 +188,42 @@ elaborate' (FOf n e) = do
   SomeRaw e <- elaborate e
   e <- assertNoun e
   pure $ SomeRaw' (ROf n e)
-elaborate' (FFn cty) = pure $ SomeRaw' (RFn cty)
-elaborate' (FKernel sty) = pure $ SomeRaw' (RKernel sty)
+elaborate' (FFn cty) = SomeRaw' . RFn . fmap (fmap unWC) <$> traverse elabSigElem cty
+elaborate' (FKernel cty) = SomeRaw' . RKernel . fmap (fmap unWC) <$> traverse elabSigElem cty
 elaborate' FIdentity = pure $ SomeRaw' RIdentity
 -- We catch underscores in the top-level elaborate so this case
 -- should never be triggered
 elaborate' FUnderscore = Left (dumbErr (InternalError "Unexpected '_'"))
 elaborate' FFanOut = pure $ SomeRaw' RFanOut
 elaborate' FFanIn = pure $ SomeRaw' RFanIn
+elaborate' (FEqn lhs rhs) = do
+  lhs <- elaborateChkNoun lhs
+  rhs <- elaborateChkNoun rhs
+  pure $ SomeRaw' (REqn lhs rhs)
+
+elabRowConstraint :: TypeRowElem (WC Flat) ty -> Either Error (TypeRowElem (WC RawVType) ty)
+elabRowConstraint (Anon ty) = pure $ Anon ty
+elabRowConstraint (Named p ty) = pure $ Named p ty
+
+class Elaborable t where
+  type Elaborated t
+  elab :: WC t -> Either Error (WC (Elaborated t))
+
+-- This is a hack to make elabSigElem nice
+instance Elaborable Flat where
+  type Elaborated Flat = Raw Chk Noun
+  elab = elaborateChkNoun
+
+instance Elaborable t => Elaborable (KindOr t) where
+  type Elaborated (KindOr t) = KindOr (Elaborated t)
+  elab (WC fc (Left k)) = pure (WC fc (Left k))
+  elab (WC fc (Right ty)) = fmap Right <$> elab (WC fc ty)
+
+elabSigElem :: Elaborable t
+            => TypeRowElem (WC Flat) (WC t)
+            -> Either Error (TypeRowElem (WC RawVType) (WC (Elaborated t)))
+elabSigElem (Anon ty) = Anon <$> elab ty
+elabSigElem (Named p ty) = Named p <$> elab ty
 
 elabBody :: FBody -> FC -> Either Error (FunBody Raw Noun)
 elabBody (FClauses cs) fc = ThunkOf . WC fc . Clauses <$> traverse elab1Clause cs
@@ -217,14 +246,17 @@ elabBody FUndefined _ = pure Undefined
 elabFunDecl :: FDecl -> Either Error RawFuncDecl
 elabFunDecl d = do
   rc <- elabBody (fnBody d) (fnLoc d)
+  sig <- traverse elabSigElem (fnSig d)
   pure $ FuncDecl
     { fnName = fnName d
     , fnLoc = fnLoc d
-    , fnSig = fnSig d
+    , fnSig = fmap unWC <$> sig -- sus
     , fnBody = rc
     , fnLocality = fnLocality d
     }
 
+elabAlias :: FAlias -> Either Error RawAlias
+elabAlias (TypeAlias fc name tys tm) = TypeAlias fc name tys . unWC <$> elaborateChkNoun (WC fc tm)
 
 elabEnv :: FEnv -> Either Error RawEnv
-elabEnv (ds, x) = (,x,empty) <$> forM ds elabFunDecl
+elabEnv (ds, as) = (,,empty) <$> traverse elabFunDecl ds <*> traverse elabAlias as
diff --git a/brat/Brat/Error.hs b/brat/Brat/Error.hs
index dbccdbb1..b93b6ec3 100644
--- a/brat/Brat/Error.hs
+++ b/brat/Brat/Error.hs
@@ -11,7 +11,7 @@ module Brat.Error (ParseError(..)
 
 import Brat.FC
 import Data.Bracket
-import Brat.Syntax.Port (PortName)
+import Brat.Syntax.Port (End, PortName)
 
 import Data.List (intercalate)
 import System.Exit
@@ -109,6 +109,9 @@ data ErrorMsg
  | ThunkLeftUnders String
  | BracketErr BracketErrMsg
  | RemainingNatHopes [String]
+ | NeedToKnow End
+ | Both ErrorMsg ErrorMsg
+ | WaitingForConstraint String
 
 instance Show ErrorMsg where
   show (TypeErr x) = "Type error: " ++ x
@@ -194,6 +197,10 @@ instance Show ErrorMsg where
   show (ThunkLeftUnders unders) = "Expected function to return additional values of type: " ++ unders
   show (BracketErr msg) = show msg
   show (RemainingNatHopes hs) = unlines ("Expected to work out values for these holes:":(("    " ++) <$> hs))
+  show (NeedToKnow end) = unlines ["I wanna know what:", ' ':show end,"is."]
+  show (Both err1 err2) = unlines [show err1,""," AND WORSE","",show err2]
+  show (WaitingForConstraint msg) = "Waiting for constraint:\n " ++ msg
+
 
 data Error = Err { fc  :: Maybe FC
                  , msg :: ErrorMsg
diff --git a/brat/Brat/Eval.hs b/brat/Brat/Eval.hs
index d7ee14c6..534879ee 100644
--- a/brat/Brat/Eval.hs
+++ b/brat/Brat/Eval.hs
@@ -18,9 +18,12 @@ module Brat.Eval (EvMode(..)
                  ,kindType
                  ,numVal
                  ,quote
-                 ,quoteNum
+		 ,quoteNum
+                 ,quoteVar
                  ,getNumVar
-                 ,instantiateMeta
+		 ,instantiateMeta
+                 ,numSumEval
+                 ,numSumUpdate
                  ) where
 
 import Brat.Checker.Monad
@@ -91,6 +94,16 @@ sem ga (VApp f vz) = do
     f <- semVar ga f
     vz <- traverse (sem ga) vz
     applySem f vz
+sem ga (VEqn lhs rhs) = SEqn <$> semNS ga lhs <*> semNS ga rhs
+
+
+semNS :: forall n. Stack Z Sem n -> NumSum (VVar n) -> Checking (NumSum SVar)
+semNS ga (NumSum c vs) = do
+  nss <- traverse semV vs
+  pure $ foldr (<>) (NumSum c []) nss
+ where
+  semV :: (Monotone (VVar n), Integer) -> Checking (NumSum SVar)
+  semV (mono, n) = flip multNumSum n . nv_to_sum <$> (numEval ga mono)
 
 semVar :: Stack Z Sem n -> VVar n -> Checking Sem
 semVar vz (VInx inx) = pure $ proj vz inx
@@ -127,6 +140,7 @@ quote lvy (SLam stk body) = do
   VLam <$> quote (Sy lvy) body
 quote lvy (SFun my ga cty) = VFun my <$> quoteCTy lvy my ga cty
 quote lvy (SApp f vz) = VApp (quoteVar lvy f) <$> traverse (quote lvy) vz
+quote lvy (SEqn lhs rhs) = pure $ VEqn (quoteVar lvy <$> lhs) (quoteVar lvy <$> rhs)
 
 quoteCTy :: Ny lv -> Modey m -> Stack Z Sem n -> CTy m n -> Checking (CTy m lv)
 quoteCTy lvy my ga (ins :->> outs) = quoteRo my ga ins lvy >>= \case
@@ -160,6 +174,16 @@ quoteRo m ga (REx pk r) lvy = do
   (ga, Some (r :* lvy)) <- quoteRo m (ga :<< semLvl lvy) r (Sy lvy)
   pure (ga, Some (REx pk r :* lvy))
 
+-- Maintains NumSum invariants through use of (<>)
+numSumEval :: forall n. Stack Z Sem n -> NumSum (VVar n) -> Checking (NumSum SVar)
+numSumEval ga (NumSum c vs) = (NumSum c [] <>) . mconcat <$> traverse aux vs
+ where
+  aux :: (Monotone (VVar n), Integer) -> Checking (NumSum SVar)
+  aux (mono, n) = (flip multNumSum n) . nv_to_sum <$> numEval ga mono
+
+numSumUpdate :: NumSum (VVar Z) -> Checking (NumSum (VVar Z))
+numSumUpdate ns = numSumEval S0 ns >>= pure . fmap (quoteVar Zy)
+
 class NumEval (f :: Type -> Type) where
   numEval :: Stack Z Sem n -> f (VVar n) -> Checking (NumVal SVar)
 
@@ -300,13 +324,22 @@ eqTests tm lvkz = go
   go _ us vs = pure . Left . TypeErr $ "Arity mismatch in type constructor arguments:\n  "
                    ++ show us ++ "\n  " ++ show vs
 
-getNumVar :: NumVal (VVar n) -> Maybe End
-getNumVar (NumValue _ (StrictMonoFun (StrictMono _ mono))) = case mono of
-  Linear v -> case v of
-    VPar e -> Just e
-    _ -> Nothing
-  Full sm -> getNumVar (numValue sm)
-getNumVar _ = Nothing
+class GetNumVar nv where
+  getNumVar :: nv -> Maybe End
+
+instance GetNumVar (NumVal (VVar n)) where
+  getNumVar (NumValue _ sm) = getNumVar sm
+
+instance GetNumVar (Fun00 (VVar n)) where
+  getNumVar Constant0 = Nothing
+  getNumVar (StrictMonoFun sm) = getNumVar sm
+
+instance GetNumVar (StrictMono (VVar n)) where
+  getNumVar (StrictMono _ mono) = getNumVar mono
+
+instance GetNumVar (Monotone (VVar n)) where
+  getNumVar (Linear (VPar e)) = Just e
+  getNumVar (Full sm) = getNumVar sm
 
 -- Be conservative, fail if in doubt. Not dangerous like being wrong while succeeding
 -- We can have bogus failures here because we're not normalising under lambdas
@@ -322,6 +355,10 @@ doesntOccur e (VLam body) = doesntOccur e body
 doesntOccur e (VFun my (ins :->> outs)) = case my of
   Braty -> doesntOccurRo my e ins *> doesntOccurRo my e outs
   Kerny -> doesntOccurRo my e ins *> doesntOccurRo my e outs
+doesntOccur e (VEqn lhs rhs) = doesntOccurNS e lhs *> doesntOccurNS e rhs
+
+doesntOccurNS :: End -> NumSum (VVar n) -> Either ErrorMsg ()
+doesntOccurNS e (NumSum _ vs) = traverse_ (\(mono,_) -> traverse_ (collision e) (getNumVar mono)) vs
 
 -- This should only be called after checking we have the right to solve the end
 instantiateMeta :: String -> End -> Val Z -> Checking ()
diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs
index bb495407..5dc332c9 100644
--- a/brat/Brat/Load.hs
+++ b/brat/Brat/Load.hs
@@ -2,6 +2,7 @@ module Brat.Load (loadFilename
                  ,loadFiles
                  ,parseFile
                  ,desugarEnv
+                 ,VDecl(..)
                  ,VMod
                  ) where
 
@@ -41,6 +42,15 @@ import System.FilePath
 
 import Prelude hiding (last)
 
+newtype VDecl = VDecl (FuncDecl (Some (Ro Brat Z)) (FunBody Term Noun))
+
+instance Show VDecl where
+  show (VDecl decl) = show $ aux decl
+   where
+    aux :: FuncDecl (Some (Ro Brat Z)) body -> FuncDecl String body
+    aux (FuncDecl { .. }) = case fnSig of
+      Some sig -> FuncDecl { fnName = fnName, fnSig = show sig, fnBody = fnBody, fnLoc = fnLoc, fnLocality = fnLocality }
+
 -- A Module is a node in the dependency graph
 type FlatMod = ((FEnv, String) -- data at the node: declarations, and file contents
                ,Import -- name of this node
diff --git a/brat/Brat/Machine.hs b/brat/Brat/Machine.hs
index 45037279..a6b0c8fc 100644
--- a/brat/Brat/Machine.hs
+++ b/brat/Brat/Machine.hs
@@ -320,6 +320,8 @@ evalConstructor CTrue [] = BoolV True
 evalConstructor CFalse [] = BoolV False
 evalConstructor CZero [] = IntV 0
 evalConstructor CSucc [IntV n] = IntV (n + 1)
+evalConstructor CSucc [th@(ThinConsV _ _)] = ThinConsV True th
+evalConstructor COmit [th] = ThinConsV False th
 evalConstructor CDoub [IntV n] = IntV (2 * n)
 evalConstructor CFull [IntV n] = IntV ((2 ^ n) - 1)
 evalConstructor CNil [] = VecV []
@@ -381,6 +383,10 @@ testCtor CBool CTrue (BoolV True) = Just []
 testCtor CBool CFalse (BoolV False) = Just []
 testCtor CNat CZero (IntV 0) = Just []
 testCtor CNat CSucc (IntV x) | x > 0 = Just [IntV (x - 1)]
+testCtor CThin CZero (IntV 0) = Just []
+testCtor CThin CSucc (IntV x) | x > 0 = Just [IntV (x - 1)]
+testCtor CThin CSucc (ThinConsV True th) = Just [th]
+testCtor CThin COmit (ThinConsV False th) = Just [th]
 testCtor CVec CNil (VecV []) = Just []
 testCtor CVec CCons (VecV (v:vs)) = Just [v, VecV vs]
 testCtor CVec CSnoc (VecV vs@(_:_)) = Just [VecV (init vs), last vs]
@@ -414,6 +420,7 @@ data Value =
   | VecV [Value]
   | ThunkV BratThunk
   | KernelV (HG.HugrGraph HG.NodeId)
+  | ThinConsV Bool Value
   | DummyV
   | StringV String
 
@@ -431,6 +438,7 @@ instance Show Value where
   show (ThunkV (VectorisedThunks ths)) = "<vectorized thunk of " ++ show (length ths) ++ ">"
   show (ThunkV _) = "<thunk>"
   show (KernelV k) = "Kernel (" ++ show k ++ ")"
+  show (ThinConsV b val) = (if b then "1" else "0") ++ "-" ++ show val
   show DummyV = "Dummy"
   show (StringV str) = show str
 
diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs
index 84b34aae..0aeb8d04 100644
--- a/brat/Brat/Parser.hs
+++ b/brat/Brat/Parser.hs
@@ -13,9 +13,7 @@ import Brat.Syntax.Common hiding (end)
 import qualified Brat.Syntax.Common as Syntax
 import Brat.Syntax.FuncDecl (FuncDecl(..), Locality(..))
 import Brat.Syntax.Concrete
-import Brat.Syntax.Raw
 import Brat.Syntax.Simple
-import Brat.Elaborator
 import Data.Bracket
 import Util ((**^))
 
@@ -214,7 +212,8 @@ abstractor = do ps <- many (try portPull)
       WC fc () <- matchString c
       pure $ WC fc (PCon (plain c) AEmpty)
 
-    nullaryConstructors = msum (try . nullaryConstructor <$> ["zero", "nil", "none", "true", "false"])
+    -- TODO: Consult the constructor table!
+    nullaryConstructors = msum (try . nullaryConstructor <$> ["zero", "nil", "none", "true", "false", "refl"])
 
     constructorWithArgs :: String -> Parser (WC Pattern)
     constructorWithArgs c = do
@@ -222,7 +221,8 @@ abstractor = do ps <- many (try portPull)
       abs <- inBracketsFC Paren (unWC <$> abstractor)
       pure $ WC (spanFCOf str abs) (PCon (plain c) (unWC abs))
 
-    constructorsWithArgs = msum (try . constructorWithArgs <$> ["succ", "doub", "cons", "some"])
+    -- TODO: Consult the constructor table!
+    constructorsWithArgs = msum (try . constructorWithArgs <$> ["succ", "doub", "cons", "some", "omit"])
 
 simpleTerm :: Parser (WC SimpleTerm)
 simpleTerm =
@@ -259,40 +259,44 @@ typekind = try (fmap (const Nat) <$> matchFC Hash) <|> kindHelper Lexer.Dollar S
     match TypeColon
     (p,) . unWC <$> typekind
 
-vtype :: Parser (WC (Raw Chk Noun))
-vtype = cnoun (expr' PApp)
+vtype :: Parser (WC Flat)
+vtype = try constraint <|> expr' PApp
+ where
+  constraint :: Parser (WC Flat)
+  constraint = do
+    lhs <- expr' PAddSub
+    match Equal
+    rhs <- expr' PAddSub
+    pure (WC (spanFCOf lhs rhs) (FEqn lhs rhs))
 
 -- Parse a row of type and kind parameters
 -- N.B. kinds must be named
 -- TODO: Update definitions so we can retain the FC info, instead of forgetting it
-rawIOFC :: Parser (TypeRow (WC (KindOr RawVType)))
-rawIOFC = rowElem `sepBy` void (try comma)
+flatIO :: Parser [FlatIO]
+flatIO = rowElem `sepBy` void (try comma)
  where
-  rowElem :: Parser (TypeRowElem (WC (KindOr RawVType)))
+  rowElem :: Parser FlatIO
   rowElem = try (inBrackets Paren rowElem') <|> rowElem'
 
-  rowElem' :: Parser (TypeRowElem (WC (KindOr RawVType)))
+  rowElem' :: Parser FlatIO
   rowElem' = try namedKind <|> try namedType <|> ((\(WC tyFC ty) -> Anon (WC tyFC (Right ty))) <$> vtype)
 
-  namedType :: Parser (TypeRowElem (WC (KindOr RawVType)))
+  namedType :: Parser FlatIO
   namedType = do
     WC pFC p <- port
     match TypeColon
     WC tyFC ty <- vtype
     pure (Named p (WC (spanFC pFC tyFC) (Right ty)))
 
-  namedKind :: Parser (TypeRowElem (WC (KindOr ty)))
+  namedKind :: Parser FlatIO
   namedKind = do
     WC pFC p <- port
     match TypeColon
     WC kFC k <- typekind
     pure (Named p (WC (spanFC pFC kFC) (Left k)))
 
-rawIO :: Parser [RawIO]
-rawIO = fmap (fmap unWC) <$> rawIOFC
-
-rawIO' :: Parser ty -> Parser (TypeRow ty)
-rawIO' tyP = rowElem `sepBy` void (try comma)
+flatIO' :: Parser ty -> Parser (TypeRow (WC Flat) ty)
+flatIO' tyP = rowElem `sepBy` void (try comma)
  where
   rowElem = try (inBrackets Paren rowElem') <|> rowElem'
 
@@ -305,13 +309,13 @@ rawIO' tyP = rowElem `sepBy` void (try comma)
        Just (WC _ p) -> Named p <$> tyP
        Nothing -> Anon <$> tyP
 
-spanningFC :: TypeRow (WC ty) -> Parser (WC (TypeRow ty))
-spanningFC [] = customFailure (Custom "Internal: RawIO shouldn't be empty")
-spanningFC [x] = pure (WC (fcOf $ forgetPortName x) [unWC <$> x])
-spanningFC (x:xs) = pure (WC (spanFC (fcOf $ forgetPortName x) (fcOf . forgetPortName $ last xs)) (fmap unWC <$> (x:xs)))
+spanningFC :: TypeRow (WC con) (WC ty) -> Parser (WC (TypeRow (WC con) (WC ty)))
+spanningFC [] = customFailure (Custom "Internal: FlatIO shouldn't be empty")
+spanningFC [x] = pure (WC (either (uncurry spanFCOf) fcOf $ forgetPortName x) [x])
+spanningFC (x:xs) = pure (WC (spanFC (either (uncurry spanFCOf) fcOf $ forgetPortName x) (either (uncurry spanFCOf) fcOf . forgetPortName $ last xs)) (x:xs))
 
-rawIOWithSpanFC :: Parser (WC [RawIO])
-rawIOWithSpanFC = spanningFC =<< rawIOFC
+flatIOWithSpanFC :: Parser (WC [FlatIO])
+flatIOWithSpanFC = spanningFC =<< flatIO
 
 vec :: Parser (WC Flat)
 vec = (\(WC fc x) -> WC fc (unWC (vec2Cons fc x))) <$> inBracketsFC Square elems
@@ -342,15 +346,15 @@ cthunk :: Parser (WC Flat)
 cthunk = try bratFn <|> try kernel <|> thunk
  where
   bratFn = inBracketsFC Brace $ do
-    ss <- rawIO
+    ss <- flatIO
     match Arrow
-    ts <- rawIO
+    ts <- flatIO
     pure $ FFn (ss :-> ts)
 
   kernel = inBracketsFC Brace $ do
-    ss <- rawIO' (unWC <$> vtype)
+    ss <- flatIO' vtype
     match Lolly
-    ts <- rawIO' (unWC <$> vtype)
+    ts <- flatIO' vtype
     pure $ FKernel (ss :-> ts)
 
 
@@ -515,7 +519,7 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr]
   annotation = do
     tm <- subExpr PAnn
     colon <- matchFC TypeColon
-    WC (spanFCOf tm colon) . FAnnotation tm <$> rawIO
+    WC (spanFCOf tm colon) . FAnnotation tm <$> flatIO
 
   letIn :: Parser (WC Flat)
   letIn = label "let ... in" $ do
@@ -594,27 +598,14 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr]
 fanout = inBracketsFC Square (FFanOut <$ match Slash <* match Backslash)
 fanin = inBracketsFC Square (FFanIn <$ match Backslash <* match Slash)
 
-cnoun :: Parser (WC Flat) -> Parser (WC (Raw 'Chk 'Noun))
-cnoun pe = do
-  e <- pe
-  case elaborate e of
-    Left err -> fail (showError err)
-    Right (SomeRaw r) -> case do
-      r <- assertChk r
-      assertNoun r
-     of
-      Left err -> fail (showError err)
-      Right r -> pure r
-
-
 decl :: Parser FDecl
 decl = do
       (fc, nm, ty, body) <- do
         WC startFC nm <- simpleName
         WC _ ty <- declSignature
         let allow_clauses = case ty of
-                                 [Named _ (Right t)] -> is_fun_ty t
-                                 [Anon (Right t)] -> is_fun_ty t
+                                 [Named _ (WC _ (Right t))] -> is_fun_ty t
+                                 [Anon (WC _ (Right t))] -> is_fun_ty t
                                  _ -> False
         WC endFC body <- if allow_clauses
                          then declClauses nm <|> declNounBody nm
@@ -628,9 +619,9 @@ decl = do
         , fnLocality = Local
         }
     where
-      is_fun_ty :: RawVType -> Bool
-      is_fun_ty (RFn _) = True
-      is_fun_ty (RKernel _) = True
+      is_fun_ty :: Flat -> Bool
+      is_fun_ty (FFn _) = True
+      is_fun_ty (FKernel _) = True
       is_fun_ty _ = False
 
       declClauses :: String -> Parser (WC FBody)
@@ -735,11 +726,11 @@ pstmt = ((comment <?> "comment")                 <&> \_ -> ([] , []))
         <|> try (extDecl                         <&> \x -> ([x], []))
         <|> ((decl <?> "declaration")            <&> \x -> ([x], []))
  where
-  alias :: Parser RawAlias
+  alias :: Parser FAlias
   alias = aliasContents <&>
           \(fc, name, args, ty) -> TypeAlias fc name args ty
 
-  aliasContents :: Parser (FC, QualName, [(String, TypeKind)], RawVType)
+  aliasContents :: Parser (FC, QualName, [(String, TypeKind)], Flat)
   aliasContents = do
     WC startFC () <- matchFC (K KType)
     WC _ alias <- qualName
@@ -780,31 +771,31 @@ pstmt = ((comment <?> "comment")                 <&> \_ -> ([] , []))
                  , fnLocality = Extern symbol
                  }
 
-declSignature :: Parser (WC [RawIO])
+declSignature :: Parser (WC [FlatIO])
 declSignature = try nDecl <|> vDecl where
- nDecl = match TypeColon >> rawIOWithSpanFC
- vDecl = functionSignature <&> fmap (\ty -> [Named "thunk" (Right ty)])
+ nDecl :: Parser (WC [FlatIO])
+ nDecl = match TypeColon >> flatIOWithSpanFC
 
- functionSignature :: Parser (WC RawVType)
- functionSignature = try (fmap RFn <$> ctype) <|> (fmap RKernel <$> kernel)
+ vDecl :: Parser (WC [FlatIO])
+ vDecl = functionSignature <&> (\(WC fc ty) -> WC fc [Named "thunk" (WC fc (Right ty))])
+
+ functionSignature :: Parser (WC Flat)
+ functionSignature = try (fmap FFn <$> ctype) <|> (fmap FKernel <$> kernel)
   where
-   ctype :: Parser (WC RawCType)
+   ctype :: Parser (WC (CType' FlatIO))
    ctype = do
-     WC startFC ins <- inBracketsFC Paren rawIO
+     WC startFC ins <- inBracketsFC Paren flatIO
      match Arrow
-     WC endFC outs <- rawIOWithSpanFC
+     WC endFC outs <- flatIOWithSpanFC
      pure (WC (spanFC startFC endFC) (ins :-> outs))
 
-   kernel :: Parser (WC RawKType)
+   kernel :: Parser (WC (CType' (TypeRowElem (WC Flat) (WC Flat))))
    kernel = do
-     WC startFC ins <- inBracketsFC Paren $ rawIO' (unWC <$> vtype)
+     WC startFC ins <- inBracketsFC Paren $ flatIO' vtype
      match Lolly
-     WC endFC outs <- spanningFC =<< rawIO' vtype
+     WC endFC outs <- spanningFC =<< flatIO' vtype
      pure (WC (spanFC startFC endFC) (ins :-> outs))
 
-
-
-
 pfile :: Parser ([Import], FEnv)
 pfile = do
   imports <- many pimport
diff --git a/brat/Brat/Syntax/Common.hs b/brat/Brat/Syntax/Common.hs
index f393755d..ac04a226 100644
--- a/brat/Brat/Syntax/Common.hs
+++ b/brat/Brat/Syntax/Common.hs
@@ -38,7 +38,8 @@ module Brat.Syntax.Common (PortName,
                            ArithOp(..),
                            pattern Dollar,
                            pattern Star,
-                           Precedence(..)
+                           Precedence(..),
+                           TypeAliasF(..)
                           ) where
 
 import Brat.FC
@@ -46,7 +47,7 @@ import Brat.QualName
 import Brat.Syntax.Abstractor
 import Brat.Syntax.Port
 
-import Data.Bifunctor (first)
+import Data.Bifunctor
 import Data.List (intercalate)
 import Data.Kind (Type)
 import Data.Type.Equality (TestEquality(..), (:~:)(..))
@@ -94,25 +95,39 @@ instance TestEquality Modey where
   testEquality Kerny Kerny = Just Refl
   testEquality _ _ = Nothing
 
-data TypeRowElem ty = Named PortName ty | Anon ty deriving (Foldable, Functor, Traversable)
-type TypeRow ty = [TypeRowElem ty]
+-- This is double parameterised because Constraints are parsed as if they're terms
+-- and require some extra elaboration
+data TypeRowElem expr ty = Named PortName ty | Anon ty
+ deriving (Functor, Foldable, Traversable)
 
-forgetPortName :: TypeRowElem ty -> ty
-forgetPortName (Anon ty) = ty
-forgetPortName (Named _ ty) = ty
+instance Bifunctor TypeRowElem where
+  first _ (Named p ty) = Named p ty
+  first _ (Anon ty) = Anon ty
 
-toTypeRow :: [(String, ty)] -> TypeRow ty
+  second f (Named p ty) = Named p (f ty)
+  second f (Anon ty) = Anon (f ty)
+
+type TypeRow expr ty = [TypeRowElem expr ty]
+
+forgetPortName :: TypeRowElem expr ty -> Either (expr,expr) ty
+forgetPortName (Anon ty) = Right ty
+forgetPortName (Named _ ty) = Right ty
+
+toTypeRow :: [(String, ty)] -> TypeRow expr ty
 toTypeRow = fmap (uncurry Named)
 
-instance Show ty => Show (TypeRowElem ty) where
+instance (Show ty, Show expr) => Show (TypeRowElem expr ty) where
   show (Named p ty) = p ++ " :: " ++ show ty
   show (Anon ty) = show ty
 
+{-
 instance Eq ty => Eq (TypeRowElem ty) where
   Named _ ty == Named _ ty' = ty == ty'
   Anon ty == Named _ ty' = ty == ty'
   Named _ ty == Anon ty' = ty == ty'
   Anon ty == Anon ty' = ty == ty'
+  _ == _ = False
+-}
 
 data TypeKind = TypeFor Mode [(PortName, TypeKind)] | Nat
   deriving (Eq, Ord)
@@ -200,14 +215,18 @@ instance Show Import where
     showSelection (ImportPartial fns) = "(":(unWC <$> fns) ++ [")"]
     showSelection (ImportHiding fns) = "hiding (":(unWC <$> fns) ++ [")"]
 
-showSig :: Show ty => [(String, ty)] -> String
+showSig :: (Show ty) => [TypeRowElem con ty] -> String
 showSig [] = "()"
-showSig (x:xs)
-  = intercalate ", " [ '(':p ++ " :: " ++ show ty ++ ")"
-                     | (p, ty) <- x:xs]
+showSig (hd:tl) = parens $ concat (tail (showElem hd) ++ [unwords (showElem x) | x <- tl])
+ where
+  parens x = '(':x ++ ")"
+
+  showElem (Anon ty) = [",", show ty]
+  showElem (Named p ty) = [",", '(':p ++ " :: " ++ show ty ++ ")"]
 
 showRow :: Show ty => [(NamedPort e, ty)] -> String
-showRow = showSig . fmap (first portName)
+showRow = parens . intercalate ", " . fmap (\(np, ty) -> unwords [portName np, "::", show ty])
+ where parens x = '(':x ++ ")"
 
 
 data ArithOp = Add | Sub | Mul | Div | Pow deriving (Eq, Show)
@@ -228,3 +247,5 @@ data Precedence
  | PAnn
  | PApp
  deriving (Bounded, Enum, Eq, Ord, Show)
+
+data TypeAliasF tm = TypeAlias FC QualName [(PortName,TypeKind)] tm deriving Show
diff --git a/brat/Brat/Syntax/Concrete.hs b/brat/Brat/Syntax/Concrete.hs
index 10bcb2e0..ac3660e6 100644
--- a/brat/Brat/Syntax/Concrete.hs
+++ b/brat/Brat/Syntax/Concrete.hs
@@ -6,19 +6,21 @@ import Brat.FC
 import Brat.QualName
 import Brat.Syntax.Common
 import Brat.Syntax.FuncDecl (FuncDecl(..))
-import Brat.Syntax.Raw
 import Brat.Syntax.Simple
 
+type FAlias = TypeAliasF Flat
+type FEnv = ([FDecl], [FAlias])
+
+type FlatIO = TypeRowElem (WC Flat) (WC (KindOr Flat))
+
 data FBody
   = FClauses (NonEmpty (WC Abstractor, WC Flat))
   | FNoLhs (WC Flat)
   | FUndefined
  deriving Show
 
-type FDecl = FuncDecl [RawIO] FBody
+type FDecl = FuncDecl [FlatIO] FBody
 deriving instance Show FDecl
-type FEnv = ([FDecl], [RawAlias])
-
 
 data Flat
  = FVar QualName
@@ -32,7 +34,7 @@ data Flat
  | FInto (WC Flat) (WC Flat)
  | FArith ArithOp (WC Flat) (WC Flat)
  | FLambda (NonEmpty (WC Abstractor, WC Flat))
- | FAnnotation (WC Flat) [RawIO]
+ | FAnnotation (WC Flat) [FlatIO]
  | FLetIn (WC Abstractor) (WC Flat) (WC Flat)
  | FSimple SimpleTerm
  | FHole String
@@ -40,12 +42,13 @@ data Flat
  | FEmpty
  | FPull [PortName] (WC Flat)
  -- We can get away with not elaborating type signatures in the short term
- | FFn RawCType
- | FKernel RawKType
+ | FFn (CType' FlatIO)
+ | FKernel (CType' (TypeRowElem (WC Flat) (WC Flat)))
  | FUnderscore
  | FPass
  | FFanOut
  | FFanIn
  | FIdentity
  | FOf ({- number :: -}WC Flat) {- of -} ({- expr -}WC Flat)
+ | FEqn (WC Flat) (WC Flat)
  deriving Show
diff --git a/brat/Brat/Syntax/Core.hs b/brat/Brat/Syntax/Core.hs
index 286b2f0f..16ab390d 100644
--- a/brat/Brat/Syntax/Core.hs
+++ b/brat/Brat/Syntax/Core.hs
@@ -3,7 +3,8 @@ module Brat.Syntax.Core (Term(..)
                         ,Output
                         ,InOut
                         ,CType
-                        ,CoreFuncDecl
+--                        ,CoreFuncDecl
+                        ,TermConstraint
                         ,Precedence(..)
                         ,precedence
                         ) where
@@ -17,20 +18,20 @@ import Brat.FC
 import Brat.Naming
 import Brat.QualName
 import Brat.Syntax.Common
-import Brat.Syntax.FuncDecl
 import Brat.Syntax.Simple
+import Brat.Syntax.Value (NumSum)
 
 import Data.Kind (Type)
 import Data.Maybe (fromJust)
 
+type TermConstraint = NumSum QualName
+
 type Input = InOut
 type Output = InOut
-type InOut = (PortName, KindOr (Term Chk Noun))
+type InOut = (KindOr (Term Chk Noun))
 
 type CType = CType' InOut
 
-type CoreFuncDecl = FuncDecl [InOut] (FunBody Term Noun)
-
 data Term :: Dir -> Kind -> Type where
   Simple   :: SimpleTerm -> Term Chk Noun
   Let      :: WC Abstractor -> WC (Term Syn Noun) -> WC (Term d k) -> Term d k
@@ -54,7 +55,7 @@ data Term :: Dir -> Kind -> Type where
   Of       :: WC (Term Chk Noun) -> WC (Term d Noun) -> Term d Noun
 
   -- Type annotations (annotating a term with its outputs)
-  (:::)    :: WC (Term Chk Noun) -> [Output] -> Term Syn Noun
+  (:::)    :: WC (Term Chk Noun) -> [TypeRowElem TermConstraint (KindOr (Term Chk Noun))] -> Term Syn Noun
   -- Composition: values fed from source (first) into dest (second),
   -- of number/type determined by the source
   (:-:)    :: WC (Term Syn k) -> WC (Term d UVerb) -> Term d k
@@ -67,13 +68,14 @@ data Term :: Dir -> Kind -> Type where
   -- Type constructors
   Con      :: QualName -> WC (Term Chk Noun) -> Term Chk Noun
   -- Brat function types
-  C        :: CType' (PortName, KindOr (Term Chk Noun)) -> Term Chk Noun
+  C        :: CType' (TypeRowElem TermConstraint (KindOr (Term Chk Noun))) -> Term Chk Noun
   -- Kernel types
-  K        :: CType' (PortName, Term Chk Noun) -> Term Chk Noun
+  K        :: CType' (TypeRowElem TermConstraint (Term Chk Noun)) -> Term Chk Noun
   FanOut   :: Term Syn UVerb
   FanIn    :: Term Chk UVerb
+  Eqn      :: WC (Term Chk Noun) -> WC (Term Chk Noun) -> Term Chk Noun
 
-deriving instance Eq (Term d k)
+-- deriving instance Eq (Term d k)
 
 -- N.B. The effort going into making a nice show instance for Term should also
 -- go into the Show instance for Flat, which should be the user facing format,
diff --git a/brat/Brat/Syntax/Raw.hs b/brat/Brat/Syntax/Raw.hs
index 956cc55f..34fcee95 100644
--- a/brat/Brat/Syntax/Raw.hs
+++ b/brat/Brat/Syntax/Raw.hs
@@ -6,9 +6,7 @@ import Control.Monad (unless, when)
 import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.State
-import Data.Bifunctor
 import Data.Kind (Type)
-import Data.List.NonEmpty (fromList, NonEmpty(..))
 import Data.Map (disjoint, member, union)
 import qualified Data.Map as M
 import Data.Tuple.HT (thd3)
@@ -23,7 +21,7 @@ import Brat.Syntax.Common
 import Brat.Syntax.Core
 import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..))
 import Brat.Syntax.Simple
-import Util (names, (**^))
+import Util ((**^))
 
 type family TypeOf (k :: Kind) :: Type where
   TypeOf Noun = [InOut]
@@ -31,29 +29,22 @@ type family TypeOf (k :: Kind) :: Type where
 
 type RawVType = Raw Chk Noun
 
-type RawIO = TypeRowElem (KindOr RawVType)
+-- Raw stuff that's also used in Brat.Syntax.Concrete
+type RawIO = TypeRowElem (WC RawVType) (KindOr RawVType)
 
 type RawCType = CType' RawIO
-type RawKType = CType' (TypeRowElem RawVType)
+type RawKType = CType' (TypeRowElem (WC RawVType) RawVType)
 
-data TypeAliasF tm = TypeAlias FC QualName [(PortName,TypeKind)] tm deriving Show
-type RawAlias = TypeAliasF (Raw Chk Noun)
 type TypeAlias = TypeAliasF (Term Chk Noun)
 
 type TypeAliasTable = M.Map QualName TypeAlias
 
+type RawAlias = TypeAliasF (Raw Chk Noun)
+
+
 type RawEnv = ([RawFuncDecl], [RawAlias], TypeAliasTable)
 type RawFuncDecl = FuncDecl [RawIO] (FunBody Raw Noun)
-
-addNames :: TypeRow ty -> [(PortName, ty)]
-addNames tms = aux (fromList names) tms
- where
-  -- aux is passed the infinite list `names`, so we can use the partial function
-  -- `fromList` to repeatedly convert it to NonEmpty so GHC doesn't complain
-  -- about the missing case `aux [] _`
-  aux (n :| ns) ((Anon tm):tms) = (n, tm) : aux (fromList ns) tms
-  aux ns ((Named n tm):tms)  = (n, tm) : aux ns tms
-  aux _ [] = []
+type CoreFuncDecl = FuncDecl (TypeRow TermConstraint (KindOr (Term Chk Noun))) (FunBody Term Noun)
 
 data Raw :: Dir -> Kind -> Type where
   RSimple   :: SimpleTerm -> Raw Chk Noun
@@ -85,6 +76,7 @@ data Raw :: Dir -> Kind -> Type where
   RKernel   :: RawKType -> Raw Chk Noun
   RFanOut   :: Raw Syn UVerb
   RFanIn    :: Raw Chk UVerb
+  REqn      :: WC (Raw Chk Noun) -> WC (Raw Chk Noun) -> Raw Chk Noun
 
 class Dirable d where
   dir :: Raw d k -> Diry d
@@ -134,7 +126,6 @@ instance Show (Raw d k) where
 
 type Desugar = StateT Namespace (ReaderT (RawEnv, Bwd QualName) (Except Error))
 
--- instance {-# OVERLAPPING #-} MonadFail Desugar where
 instance {-# OVERLAPPING #-} MonadFail Desugar where
   fail = throwError . desugarErr
 
@@ -164,23 +155,6 @@ isAlias name = do
   pure $ M.member name aliases
 
 
-{-
-findDuplicates :: Env -> Desugar ()
-findDuplicates (ndecls, vdecls, aliases)
-  = aux $ concat [(fst &&& show . fst . snd) <$> (unWC <$> ndecls)
-                 ,(fst &&& show . fst . snd) <$> (unWC <$> vdecls)
-                 ,(fst &&& show . snd) <$> aliases]
- where
-  aux :: [(String, String)] -> Desugar ()
-  aux xs = case filter ((1<).length) [ filter ((==x).fst) xs | (x,_) <- xs ] of
-             []  -> pure () -- all good
-             ([]:_) -> undefined -- this should be unreachable
-             -- TODO: Include FC
-             ((x:xs):_) -> desugarErr . unlines $ (("Multiple definitions of " ++ fst x)
-                                                   :(snd <$> (x:xs))
-                                                  )
--}
-
 desugarErr :: String -> Error
 desugarErr = dumbErr . DesugarErr
 
@@ -194,10 +168,16 @@ class Desugarable ty where
 
   desugar' :: ty -> Desugar (Desugared ty)
 
-instance Desugarable ty => Desugarable (TypeRow ty) where
-  type Desugared (TypeRow ty) = TypeRow (Desugared ty)
-  desugar' = traverse (traverse desugar')
+instance Desugarable ty => Desugarable (TypeRowElem (WC RawVType) ty) where
+    type Desugared (TypeRowElem (WC RawVType) ty) = TypeRowElem TermConstraint (Desugared ty)
+    desugar' (Anon ty) = Anon <$> desugar' ty
+    desugar' (Named x ty) = Named x <$> desugar' ty
+
+instance Desugarable (TypeRowElem con ty) => Desugarable [TypeRowElem con ty] where
+  type Desugared [TypeRowElem con ty] = [Desugared (TypeRowElem con ty)]
+  desugar' = traverse desugar'
 
+-- Desugaring terms
 instance (Kindable k) => Desugarable (Raw d k) where
   type Desugared (Raw d k) = Term d k
   -- TODO: holes need to know their arity for type checking
@@ -239,7 +219,7 @@ instance (Kindable k) => Desugarable (Raw d k) where
   desugar' (fun ::$:: arg) = (:$:) <$> desugar fun <*> desugar arg
   desugar' (tm ::::: outputs) = do
     tm <- desugar tm
-    (tys, ()) <- desugarBind outputs $ pure ()
+    tys <- traverse desugar' outputs
     pure (tm ::: tys)
   desugar' (syn ::-:: verb) = (:-:) <$> desugar syn <*> desugar verb
   desugar' (RLambda c cs) = Lambda <$> (id **^ desugar) c <*> traverse (id **^ desugar) cs
@@ -250,16 +230,14 @@ instance (Kindable k) => Desugarable (Raw d k) where
   desugar' RFanOut = pure FanOut
   desugar' RFanIn = pure FanIn
   desugar' (ROf n e) = Of <$> desugar n <*> desugar e
+  desugar' (REqn lhs rhs) = Eqn <$> desugar lhs <*> desugar rhs
 
-instance Desugarable ty => Desugarable (PortName, ty) where
-  type Desugared (PortName, ty) = (PortName, Desugared ty)
-  desugar' (p, ty) = (p,) <$> desugar' ty
-
-instance Desugarable (CType' (TypeRowElem RawVType)) where
-  type Desugared (CType' (TypeRowElem RawVType)) = CType' (PortName, Term Chk Noun)
+instance Desugarable (CType' (TypeRowElem (WC RawVType) RawVType)) where
+  type Desugared (CType' (TypeRowElem (WC RawVType) RawVType)) = CType' (TypeRowElem TermConstraint (Term Chk Noun))
+  desugar' :: CType' (TypeRowElem (WC RawVType) RawVType) -> Desugar (CType' (TypeRowElem TermConstraint (Term Chk Noun)))
   desugar' (ss :-> ts) = do
-    ss <- traverse desugar' (addNames ss)
-    ts <- traverse desugar' (addNames ts)
+    ss <- traverse desugar' ss -- (addNames ss)
+    ts <- traverse desugar' ts -- (addNames ts)
     pure (ss :-> ts)
 
 isConOrAlias :: QualName -> Desugar Bool
@@ -283,27 +261,9 @@ instance Desugarable ty => Desugarable (KindOr ty) where
   desugar' (Left k) = pure (Left k)
   desugar' (Right ty) = Right <$> desugar' ty
 
-desugarBind :: forall t. [RawIO]
-            -> Desugar t
-            -> Desugar ([(PortName, KindOr (Term Chk Noun))], t)
-desugarBind tys m = worker (addNames tys)
- where
-  worker :: [(PortName, KindOr (Raw Chk Noun))]
-         -> Desugar ([(PortName, KindOr (Term Chk Noun))], t)
-  worker ((p, Left k):ns) = do
-    (ns, t) <- local (second (:< PrefixName [] p)) $ worker ns
-    pure ((p, Left k):ns, t)
-  worker ((p, Right ty):ns) = do
-    ty <- desugar' ty
-    (ns, t) <- worker ns
-    pure ((p, Right ty):ns, t)
-  worker [] = ([],) <$> m
-
-instance Desugarable (CType'  RawIO) where
-  type Desugared (CType' RawIO) = CType' (PortName, KindOr (Term Chk Noun))
-  desugar' (ss :-> ts) = do
-    (ss, (ts, ())) <- desugarBind ss $ desugarBind ts $ pure ()
-    pure $ ss :-> ts
+instance Desugarable (CType' RawIO) where
+  type Desugared (CType' RawIO) = CType' (TypeRowElem TermConstraint (KindOr (Term Chk Noun)))
+  desugar' (ss :-> ts) = (:->) <$> desugar' ss <*> desugar' ts
 
 instance Desugarable RawAlias where
   type Desugared RawAlias = TypeAlias
@@ -326,7 +286,7 @@ desugarVBody Undefined = pure Undefined
 instance Desugarable RawFuncDecl where
   type Desugared RawFuncDecl = CoreFuncDecl
   desugar' d@FuncDecl{..} = do
-    tys  <- addNames <$> desugar' fnSig
+    tys  <- desugar' fnSig
     noun <- desugarNBody fnBody
     pure $ d { fnBody = noun
              , fnSig  = tys
diff --git a/brat/Brat/Syntax/Value.hs b/brat/Brat/Syntax/Value.hs
index 1af8b94e..f462625c 100644
--- a/brat/Brat/Syntax/Value.hs
+++ b/brat/Brat/Syntax/Value.hs
@@ -25,10 +25,9 @@ module Brat.Syntax.Value {-(VDecl
 import Brat.Error
 import Brat.QualName
 import Brat.Syntax.Common
-import Brat.Syntax.Core (Term (..))
-import Brat.Syntax.FuncDecl (FunBody, FuncDecl(..))
 import Bwd
 import Hasochism
+import Util (log2)
 
 import Data.List (intercalate, minimumBy)
 import Data.Ord (comparing)
@@ -36,15 +35,6 @@ import Data.Kind (Type)
 import Data.Maybe (isJust)
 import Data.Type.Equality ((:~:)(..), testEquality)
 
-newtype VDecl = VDecl (FuncDecl (Some (Ro Brat Z)) (FunBody Term Noun))
-
-instance MODEY Brat => Show VDecl where
-  show (VDecl decl) = show $ aux decl
-   where
-    aux :: FuncDecl (Some (Ro Brat Z)) body -> FuncDecl String body
-    aux (FuncDecl { .. }) = case fnSig of
-      Some sig -> FuncDecl { fnName = fnName, fnSig = show sig, fnBody = fnBody, fnLoc = fnLoc, fnLocality = fnLocality }
-
 ------------------------------------ Variable Indices ------------------------------------
 -- Well scoped de Bruijn indices
 data Inx :: N -> Type where
@@ -161,6 +151,7 @@ data Val :: N -> Type where
   VLam :: Val (S n) -> Val n -- Just body (binds DeBruijn index n)
   VFun :: MODEY m => Modey m -> CTy m n -> Val n
   VApp :: VVar n -> Bwd (Val n) -> Val n
+  VEqn :: NumSum (VVar n) -> NumSum (VVar n) -> Val n
 
 -- Define a naive version of equality, which only says whether the data
 -- structures are on-the-nose equal
@@ -188,7 +179,7 @@ instance MODEY m => Eq (CTy m i) where
     roEq _ _ _ = Nothing
 
 data SVar = SPar End | SLvl Int
- deriving (Show, Eq)
+ deriving (Show, Eq, Ord)
 
 -- Semantic value, used internally by normalization; contains Lvl's but no Inx's
 data Sem where
@@ -201,6 +192,7 @@ data Sem where
   SApp :: SVar -> Bwd Sem -> Sem
   -- Sum types, stash like SLam (shared between all variants)
   SSum :: MODEY m => Modey m -> Stack Z Sem n -> [Some (Ro m n)] -> Sem
+  SEqn :: NumSum SVar -> NumSum SVar -> Sem
 deriving instance Show Sem
 
 data CTy :: Mode -> N -> Type where
@@ -237,7 +229,7 @@ instance forall m top bot. MODEY m => Show (Ro m bot top) where
                                       Braty -> show ty
                                       Kerny -> show ty
                                 in  ('(':p ++ " :: " ++ tyStr ++ ")"):roToList ro
-    roToList  (REx (p, k) ro) = ('(':p ++ " :: " ++ show k ++ ")"):roToList ro
+    roToList (REx (p, k) ro) = ('(':p ++ " :: " ++ show k ++ ")"):roToList ro
 
 instance Show (Val n) where
   show v@(VCon _ _) | Just vs <- asList v = show vs
@@ -251,6 +243,7 @@ instance Show (Val n) where
   show (VFun m cty) = "{ " ++ modily m (show cty) ++ " }"
   show (VApp v ctx) = "VApp " ++ show v ++ " " ++ show ctx
   show (VLam body) = "VLam " ++ show body
+  show (VEqn lhs rhs) = show lhs ++ " = " ++ show rhs
 
 ---------------------------------- Patterns -----------------------------------
 pattern TNat, TInt, TFloat, TBool, TText, TUnit, TNil :: Val n
@@ -266,9 +259,11 @@ pattern TList, TOption :: Val n -> Val n
 pattern TList ty = VCon (PrefixName [] "List") [ty]
 pattern TOption ty = VCon (PrefixName [] "Option") [ty]
 
-pattern TVec, TCons :: Val n -> Val n -> Val n
+pattern TVec, TCons, TEq, TThin :: Val n -> Val n -> Val n
 pattern TVec ty n = VCon (PrefixName [] "Vec") [ty, n]
 pattern TCons x ys = VCon (PrefixName [] "cons") [x, ys]
+pattern TEq a b = VCon (PrefixName [] "Eq") [a,b]
+pattern TThin a b = VCon (PrefixName [] "Thin") [a,b]
 
 pattern TQ, TMoney, TBit :: Val n
 pattern TQ = VCon (PrefixName [] "Qubit") []
@@ -288,7 +283,7 @@ type family BinderVal (m :: Mode) where
 data NumVal x = NumValue
   { upshift :: Integer
   , grower  :: Fun00 x
-  } deriving (Eq, Foldable, Functor, Traversable)
+  } deriving (Eq, Foldable, Functor, Ord, Traversable)
 
 instance Show x => Show (NumVal x) where
   show (NumValue 0 g) = show g
@@ -299,7 +294,7 @@ instance Show x => Show (NumVal x) where
 data Fun00 x
  = Constant0
  | StrictMonoFun (StrictMono x)
- deriving (Eq, Foldable, Functor, Traversable)
+ deriving (Eq, Foldable, Functor, Ord, Traversable)
 
 instance Show x => Show (Fun00 x) where
   show Constant0 = "0"
@@ -309,7 +304,7 @@ instance Show x => Show (Fun00 x) where
 data StrictMono x = StrictMono
  { multBy2ToThe :: Integer
  , monotone :: Monotone x
- } deriving (Eq, Foldable, Functor, Traversable)
+ } deriving (Eq, Foldable, Functor, Ord, Traversable)
 
 instance Show x => Show (StrictMono x) where
   show (StrictMono 0 m) = show m
@@ -320,7 +315,7 @@ instance Show x => Show (StrictMono x) where
 data Monotone x
  = Linear x
  | Full (StrictMono x)
- deriving (Eq, Foldable, Functor, Traversable)
+ deriving (Eq, Foldable, Functor, Ord, Traversable)
 
 instance Show x => Show (Monotone x) where
   show (Linear v) = show v
@@ -546,6 +541,8 @@ instance DeBruijn Val where
     = VFun Braty $ changeVar vc cty
   changeVar vc (VFun Kerny cty)
     = VFun Kerny $ changeVar vc cty
+  changeVar vc (VEqn lhs rhs)
+    = VEqn (changeVar vc <$> lhs) (changeVar vc <$> rhs)
 
 varChangerThroughRo :: VarChanger src tgt
                     -> Ro m src src'
@@ -636,6 +633,10 @@ numVars nv = [e | VPar e <- vvars nv]
 class DepEnds t where
   depEnds :: t -> [End]
 
+instance DepEnds (VVar n) where
+  depEnds (VPar e) = [e]
+  depEnds _ = []
+
 instance DepEnds (NumVal (VVar n)) where
   depEnds nv = [e | VPar e <- vvars nv]
    where
@@ -649,6 +650,7 @@ instance DepEnds (Val n) where
   depEnds (VFun _ cty) = depEnds cty
   depEnds (VApp (VPar e) args) = e : depEnds args
   depEnds (VApp _ args) = depEnds args
+  depEnds (VEqn lhs rhs) = (foldMap depEnds lhs) ++ (foldMap depEnds rhs)
 
 instance DepEnds t => DepEnds [t] where
   depEnds = concatMap depEnds
@@ -663,3 +665,69 @@ instance DepEnds (Ro m i j) where
 
 instance DepEnds (CTy m n) where
   depEnds (ss :->> ts) = depEnds ss ++ depEnds ts
+
+-- number plus sum over a sequence of (variable/Full * number), ordered and distinct
+-- All Integers positive, all multipliers strictly so
+data NumSum var = NumSum Integer [(Monotone var, Integer)]
+  deriving (Eq, Foldable, Functor, Ord, Traversable)
+
+instance Show var => Show (NumSum var) where
+  show (NumSum i vars) = let const = case (i == 0, null vars) of
+                               (True, True) -> "0"
+                               (True, False) -> ""
+                               (False, True) -> show i
+                               (False, False) -> show i ++ " + "
+                             showMult (v,1) = show v
+                             showMult (v,m) = show m ++ "*(" ++ show v ++ ")"
+                         in  const ++ intercalate " + " (showMult <$> vars)
+
+
+instance Ord var => Monoid (NumSum var) where
+    mempty = NumSum 0 []
+    mappend (NumSum n ts) (NumSum n' ts') = NumSum (n + n') (merge ts ts')
+     where
+      merge [] ys = ys
+      merge xs [] = xs
+      merge xxs@((x, n):xs) yys@((y, m):ys) = case compare x y of
+        LT -> (x, n):(merge xs yys)
+        EQ -> (x, n+m):(merge xs ys)
+        GT -> (y, m):(merge xxs ys)
+
+instance Ord var => Semigroup (NumSum var) where
+    (<>) = mappend
+
+numSumVar :: var -> NumSum var
+numSumVar v = NumSum 0 [(Linear v, 1)]
+
+multNumSum :: NumSum v -> Integer -> NumSum v
+multNumSum (NumSum c vs) m = NumSum (c*m) [ (v, n*m) | (v, n) <- vs ]
+
+changeNumSumVars :: VarChanger src tgt -> NumSum (VVar src) -> NumSum (VVar tgt)
+changeNumSumVars ch = fmap (changeVar ch)
+
+nv_to_sum :: NumVal var -> NumSum var
+nv_to_sum (NumValue up grow) = NumSum up $ case grow of
+    Constant0 -> []
+    (StrictMonoFun (StrictMono numDoub mono)) -> [(mono, 2 ^ numDoub)]
+
+nvs_to_sum :: Ord var => [NumVal var] -> NumSum var
+nvs_to_sum = foldMap nv_to_sum
+
+numSumToNum :: NumSum var -> Maybe (NumVal var)
+numSumToNum (NumSum c []) = Just (nConstant c)
+numSumToNum (NumSum c [(mono, n)])
+ | Just k <- log2 n = Just $ NumValue c (StrictMonoFun $ StrictMono k mono)
+numSumToNum _ = Nothing
+
+instance DepEnds v => DepEnds (StrictMono v) where
+  depEnds (StrictMono _ v) = depEnds v
+
+instance DepEnds v => DepEnds (Monotone v) where
+  depEnds (Linear v) = depEnds v
+  depEnds (Full sm) = depEnds sm
+
+instance DepEnds (NumSum (VVar Z)) where
+  depEnds (NumSum _ vs) = concat [depEnds v | (v,_) <- vs]
+
+instance (DepEnds a, DepEnds b) => DepEnds (a, b) where
+  depEnds (a, b) = depEnds a ++ depEnds b
diff --git a/brat/Brat/Unelaborator.hs b/brat/Brat/Unelaborator.hs
index b06509f0..d7a50177 100644
--- a/brat/Brat/Unelaborator.hs
+++ b/brat/Brat/Unelaborator.hs
@@ -1,16 +1,21 @@
 module Brat.Unelaborator (unelab) where
 
-import Brat.FC (unWC)
-import Brat.Syntax.Concrete (Flat(..))
-import Brat.Syntax.Common (Dir(..), Kind(..), Diry(..), Kindy(..)
-                          ,KindOr, PortName, TypeRowElem(Named), CType'(..)
+import Brat.FC (dummyFC, unWC, WC(..))
+import Brat.QualName (QualName(..))
+import Brat.Syntax.Common (ArithOp(..), Dir(..), Kind(..), Diry(..), Kindy(..)
+                          ,KindOr, TypeRowElem(..), CType'(..)
                           )
-import Brat.Syntax.Core (Term(..))
-import Brat.Syntax.Raw (Raw(..), RawVType)
+import Brat.Syntax.Concrete (Flat(..))
+import Brat.Syntax.Core (Term(..), TermConstraint)
+import Brat.Syntax.Raw (Raw(..))
+import Brat.Syntax.Simple (SimpleTerm(..))
+import Brat.Syntax.Value (Monotone(..), NumSum(..), StrictMono(..))
 
-import Data.Bifunctor (second)
+import Data.Bifunctor (bimap, second)
 import Data.List.NonEmpty (NonEmpty(..))
 
+type Type = Term Chk Noun
+
 unelab :: Diry d -> Kindy k -> Term d k -> Flat
 unelab _ _ (Simple tm) = FSimple tm
 unelab dy ky (Let abs expr body) = FLetIn abs (unelab Syny Nouny <$> expr) (unelab dy ky <$> body)
@@ -28,17 +33,23 @@ unelab _ ky (Pull ps tm) = FPull ps (unelab Chky ky <$> tm)
 unelab _ _ (Var v) = FVar v
 unelab dy ky (Arith op lhs rhs) = FArith op (unelab dy ky <$> lhs) (unelab dy ky <$> rhs)
 unelab dy _ (Of n e) = FOf (unelab Chky Nouny <$> n) (unelab dy Nouny <$> e)
-unelab _ _ (tm ::: outs) = FAnnotation (unelab Chky Nouny <$> tm) (toRawRo outs)
+unelab _ _ (tm ::: outs) = FAnnotation (unelab Chky Nouny <$> tm) (unelabRowElem (dummyFC . second (unelab Chky Nouny)) <$> outs)
 unelab dy ky (top :-: bot) = case ky of
   Nouny -> FInto (unelab Syny Nouny <$> top) (unelab dy UVerby <$> bot)
   _ -> FApp (unelab Syny ky <$> top) (unelab dy UVerby <$> bot)
 unelab dy ky (f :$: s) = FApp (unelab dy KVerby <$> f) (unelab Chky ky <$> s)
 unelab dy _ (Lambda (abs,rhs) cs) = FLambda ((abs, unelab dy Nouny <$> rhs) :| (second (fmap (unelab Chky Nouny)) <$> cs))
 unelab _ _ (Con c args) = FCon c (unelab Chky Nouny <$> args)
-unelab _ _ (C (ss :-> ts)) = FFn (toRawRo ss :-> toRawRo ts)
-unelab _ _ (K cty) = FKernel $ fmap (\(p, ty) -> Named p (toRaw ty)) cty
+unelab _ _ (C (ss :-> ts)) = FFn ((f <$> ss)
+                                  :->
+                                  (f <$> ts)
+                                 )
+ where
+  f :: TypeRowElem TermConstraint (KindOr (Term Chk Noun)) -> TypeRowElem (WC Flat) (WC (KindOr Flat))
+  f = unelabRowElem (dummyFC . second (unelab Chky Nouny))
+unelab _ _ (K cty) = FKernel $ fmap (unelabRowElem (dummyFC . unelab Chky Nouny)) cty
 unelab _ _ Identity = FIdentity
-unelab _ _ (Hope ident) = FHope ident
+unelab _ _ (Hope i) = (FHope i)
 unelab _ _ FanIn = FFanIn
 unelab _ _ FanOut = FFanOut
 
@@ -60,17 +71,74 @@ toRaw (Pull ps tm) = RPull ps $ toRaw <$> tm
 toRaw (Var v) = RVar v
 toRaw (Arith op lhs rhs) = RArith op (toRaw <$> lhs) (toRaw <$> rhs)
 toRaw (Of n e) = ROf (toRaw <$> n) (toRaw <$> e)
-toRaw (tm ::: outs) = (toRaw <$> tm) ::::: toRawRo outs
+toRaw (tm ::: outs) = (toRaw <$> tm) ::::: (fmap (unelabRowElem (second toRaw)) outs)
 toRaw (top :-: bot) = (toRaw <$> top) ::-:: (toRaw <$> bot)
 toRaw (f :$: s) = (toRaw <$> f) ::$:: (toRaw <$> s)
 toRaw (Lambda (abs,rhs) cs) = RLambda (abs, toRaw <$> rhs) (second (fmap toRaw) <$> cs)
 toRaw (Con c args) = RCon c (toRaw <$> args)
-toRaw (C (ss :-> ts)) = RFn (toRawRo ss :-> toRawRo ts)
-toRaw (K cty) = RKernel $ (\(p, ty) -> Named p (toRaw ty)) <$> cty
+toRaw (C (ss :-> ts)) = let f row = fmap (unelabRowElem (second toRaw)) row
+                         in RFn (f ss :-> f ts)
+toRaw (K (ss :-> ts)) = let f row = fmap (unelabRowElem toRaw) row
+                         in RKernel (f ss :-> f ts)
 toRaw Identity = RIdentity
-toRaw (Hope ident) = RHope ident
+toRaw (Hope i) = (RHope i)
 toRaw FanIn = RFanIn
 toRaw FanOut = RFanOut
 
-toRawRo :: [(PortName, KindOr (Term Chk Noun))] -> [TypeRowElem (KindOr RawVType)]
-toRawRo = fmap (\(p, bty) -> Named p (second toRaw bty))
+--rawConstraints :: NumSum QualName -> WC (Raw Chk Noun)
+--rawConstraints = transformConstraints RArith RSimple (REmb . dummyFC . RVar)
+
+class TypeRowTransform raw where
+  -- Constructor for an arith op in `raw`
+  fArith :: ArithOp -> WC raw -> WC raw -> raw
+  -- Constructor for simple terms in `raw`
+  fSimple :: SimpleTerm -> raw
+  -- Constructor for variables in `raw`
+  fVar :: QualName -> raw
+
+--  -- Transform types
+--  transformType :: Term d k -> raw
+
+--  transform :: [TypeRowElem (NumSum QualName) (Term d k)] -> [TypeRowElem (WC raw) raw]
+--  transform = fmap (bimap transformConstraint transformRow)
+--
+--  transformRow :: [TypeRowElem con (Term d k)] -> [TypeRowElem con raw]
+--  transformRow = fmap (second transformType)
+
+  transformConstraint :: NumSum QualName -> WC raw
+  transformConstraint ns = dummyFC (nsToRaw ns)
+   where
+    arith :: ArithOp -> raw -> raw -> raw
+    arith op lhs rhs = fArith op (dummyFC lhs) (dummyFC rhs)
+
+    num :: Integer -> raw
+    num n = fSimple (Num (fromIntegral n))
+
+    nsToRaw :: NumSum QualName -> raw
+    nsToRaw (NumSum 0 [nk]) = nkToRaw nk
+    nsToRaw (NumSum 0 (nk:rest)) = arith Add (nkToRaw nk) (nsToRaw (NumSum 0 rest))
+    nsToRaw (NumSum n nks) = arith Add (num n) (nsToRaw (NumSum 0 nks))
+
+    nkToRaw (n, k) = arith Mul (num k) (monoToRaw n)
+
+    monoToRaw :: Monotone QualName -> raw
+    monoToRaw (Linear name) = fVar name
+    monoToRaw (Full mono) = let pow = arith Pow (num 2) (smToRaw mono)
+                             in arith Sub pow (num 1)
+
+    smToRaw :: StrictMono QualName -> raw
+    smToRaw (StrictMono 0 mono) = monoToRaw mono
+    smToRaw (StrictMono k mono) = arith Mul (arith Pow (num 2) (num k)) (monoToRaw mono)
+
+instance TypeRowTransform (Raw Chk Noun) where
+  fArith = RArith
+  fSimple = RSimple
+  fVar = REmb . dummyFC . RVar
+
+instance TypeRowTransform Flat where
+  fArith = FArith
+  fSimple = FSimple
+  fVar = FVar
+
+unelabRowElem :: TypeRowTransform rawCon => (ty -> rawTy) -> TypeRowElem (NumSum QualName) ty -> TypeRowElem (WC rawCon) rawTy
+unelabRowElem f = bimap transformConstraint f
diff --git a/brat/Control/Monad/Freer.hs b/brat/Control/Monad/Freer.hs
index ed8b7455..24ff09e2 100644
--- a/brat/Control/Monad/Freer.hs
+++ b/brat/Control/Monad/Freer.hs
@@ -1,5 +1,6 @@
 module Control.Monad.Freer where
 
+import Brat.Error (ErrorMsg(..))
 import Brat.Syntax.Port (End)
 import Brat.Syntax.Value (Val)
 import Hasochism (N(..))
@@ -13,7 +14,7 @@ import qualified Data.Set as S
 --  * e -> Unstuck means e has been solved
 --  * e -> Awaiting es means the problem's been transferred
 --  * e not in news means no change to e
-newtype News = News (M.Map End Stuck)
+newtype News = News (M.Map End Stuck) deriving Show
 
 updateEnd :: News -> End -> Stuck
 updateEnd (News m) e = case M.lookup e m of
@@ -44,14 +45,14 @@ data Free (sig :: Type -> Type) (v :: Type) where
   Ret :: v -> Free sig v
   Req ::  sig t -> (t -> Free sig v) -> Free sig v
   Define :: String -> End -> Val Z -> (News -> Free sig v) -> Free sig v
-  Yield :: Stuck -> (News -> Free sig v) -> Free sig v
+  Yield :: ErrorMsg -> Stuck -> (News -> Free sig v) -> Free sig v
   Fork :: String -> Free sig () -> Free sig v -> Free sig v
 
 instance Functor (Free sig) where
   fmap f (Ret v) = Ret (f v)
   fmap f (Req sig k) = Req sig (fmap f . k)
   fmap f (Define lbl e v k) = Define lbl e v (fmap f . k)
-  fmap f (Yield st k) = Yield st (fmap f . k)
+  fmap f (Yield err st k) = Yield err st (fmap f . k)
   fmap f (Fork d par c) = Fork d par (fmap f c)
 
 class NewsWatcher t where
@@ -68,7 +69,7 @@ instance NewsWatcher (Free sig v) where
   Ret v /// _ = Ret v
   Req sig k /// n = Req sig $ \v -> k v /// n
   Define lbl e v k /// n = Define lbl e v (k /// n)
-  Yield st k /// n = Yield (st /// n) (k /// n)
+  Yield err st k /// n = Yield err (st /// n) (k /// n)
   Fork d par c /// n = Fork d (par /// n) (c /// n)
 
 instance Applicative (Free sig) where
@@ -76,8 +77,8 @@ instance Applicative (Free sig) where
 
   -- Left biased scheduling of commands:
   -- First, get rid of Yield Unstuck
-  Yield Unstuck k <*> a = k mempty <*> a
-  f <*> Yield Unstuck k = f <*> k mempty
+  Yield _ Unstuck k <*> a = k mempty <*> a
+  f <*> Yield _ Unstuck k = f <*> k mempty
 
   -- Aggressively forward Forks
   Fork d par c <*> ma = Fork d par (c <*> ma)
@@ -91,7 +92,7 @@ instance Applicative (Free sig) where
   -- What happens when Yield is on the left
   y <*> Ret v = fmap ($ v) y
   y <*> Req sig k = Req sig $ \v -> y <*> k v
-  y1@(Yield st1 _) <*> y2@(Yield st2 _) = Yield (st1 <> st2) $
+  y1@(Yield err1 st1 _) <*> y2@(Yield err2 st2 _) = Yield (Both err1 err2) (st1 <> st2) $
     \n -> (y1 /// n) <*> (y2 /// n)
   y <*> Define lbl e v k = Define lbl e v $ \n -> (y /// n) <*> k n
 
@@ -99,7 +100,7 @@ instance Monad (Free sig) where
   Ret v >>= k = k v
   Req r j >>= k = Req r (j >=> k)
   Define lbl e v k1 >>= k2 = Define lbl e v (k1 >=> k2)
-  Yield st k1 >>= k2 = Yield st (k1 >=> k2)
+  Yield err st k1 >>= k2 = Yield err st (k1 >=> k2)
   --- equivalent to
   -- Yield st k1 >>= k2 = Yield st (\n -> (k1 n) >>= k2)
   Fork d par k1 >>= k2 = Fork d par (k1 >>= k2)
diff --git a/brat/brat.cabal b/brat/brat.cabal
index f237c89e..3222be26 100644
--- a/brat/brat.cabal
+++ b/brat/brat.cabal
@@ -47,7 +47,7 @@ common warning-flags
     -Werror=unused-imports
     -Werror=unused-matches
     -Werror=missing-methods
-    -Werror=unused-top-binds
+--    -Werror=unused-top-binds
     -Werror=unused-local-binds
     -Werror=redundant-constraints
     -Werror=orphans
@@ -64,10 +64,12 @@ library
   exposed-modules:     Brat.Checker.Quantity,
                        Brat.Dot,
                        Brat.Eval,
-                       Brat.Lexer
+                       Brat.Lexer,
+                       Brat.Checker.Arithmetic,
                        Brat.Checker.Helpers,
                        Brat.Checker.Helpers.Nodes,
                        Brat.Checker.Monad,
+                       Brat.Checker.SolveConstraints,
                        Brat.Checker.SolveHoles,
                        Brat.Checker.SolveNumbers,
                        Brat.Checker.SolvePatterns,
@@ -162,6 +164,7 @@ test-suite tests
   hs-source-dirs:      test
   main-is:             Main.hs
   other-modules:       Test.Abstractor,
+                       Test.Arithmetic,
                        Test.Checking,
                        Test.Compile.Hugr,
                        Test.Elaboration,
diff --git a/brat/examples/mergesort.brat b/brat/examples/mergesort.brat
new file mode 100644
index 00000000..6de0fefb
--- /dev/null
+++ b/brat/examples/mergesort.brat
@@ -0,0 +1,16 @@
+leq(n :: Nat, m :: Nat) -> Bool
+leq(0, _) = true
+leq(_, 0) = false
+leq(succ(n), succ(m)) = leq(n, m)
+
+ifthenelse(X :: *, b :: Bool, { -> X }, { -> X }) -> X
+ifthenelse(_, true, then, _) = then()
+ifthenelse(_, false, _, else) = else()
+
+merge(l :: #, n :: #, m :: #, Vec(Nat, l), Vec(Nat, n), l + n = m) -> Vec(Nat, m)
+merge(_, _, _, [], ys, _) = ys
+merge(_, _, _, xs, [], _) = xs
+merge(_, _, _, x ,- xs, y ,- ys, _) =
+ ifthenelse(!, leq(x, y),
+            { => x ,- merge(!, !, !, xs, y ,- ys, !) },
+            { => y ,- merge(!, !, !, x ,- xs, ys, !) })
diff --git a/brat/examples/thin.brat b/brat/examples/thin.brat
index 92c99e46..3d93895c 100644
--- a/brat/examples/thin.brat
+++ b/brat/examples/thin.brat
@@ -1,23 +1,64 @@
---!xfail-parsing
--- Experiments with selecting out of vectors with first class selections
--- This feature has fallen by the wayside, so expect this to fail
+--partition(X :: *, l :: #, n :: #, m :: #, l + n = m, Thin(n, m), Vec(X, m)) -> Vec(X, l), Vec(X, n)
+--partition(_, _, _, _, _, zero, []) = [], []
+--partition(_, _, _, _, _, succ(th), z ,- zs) =
+-- let xs', ys' = partition(!, !, !, !, !, th, zs) in xs', z ,- ys'
+--partition(_, _, _, _, _, omit(th), z ,- zs) =
+-- let xs', ys' = partition(!, !, !, !, !, th, zs) in z ,- xs', ys'
+--partition(_, succ(l'), _, _, _, omit(th), z ,- zs) =
+-- let xs', ys' = partition(!, l', !, !, !, th, zs) in z ,- xs', ys'
 
--- This type is WRONG
-test :: Vec(X, 2) <<< Vec(X, 2)
-test = {0..} -- The identity thinning
+select(X :: *, n :: #, m :: #, Thin(n, m), Vec(X, m)) -> Vec(X, n)
+select(_, _, _, zero, []) = []
+select(_, _, _, succ(th), x ,- xs) = x ,- select(!, !, !, th, xs)
+select(_, _, _, omit(th), _ ,- xs) = select(!, !, !, th, xs)
 
-test' :: Vec(X, 1) <<< Vec(X, 9)
-test' = {5} -- just the fifth
+reject(X :: *, l :: #, n :: #, m :: #, l + n = m, Thin(n, m), Vec(X, m)) -> Vec(X, l)
+reject(_, _, _, _, _, zero, []) = []
+reject(_, _, _, _, _, succ(th), _ ,- xs) = reject(!, !, !, !, !, th, xs)
+reject(_, _, _, _, _, omit(th), x ,- xs) = x ,- reject(!, !, !, !, !, th, xs)
 
-vec :: Vec(Nat, 5)
-vec = [1, 2, 3, 4, 5]
- 
-test'' :: Vec(Nat, 1)
-test'' = vec{0} -- vec{2,4,5}
--- test''' :: Vec Nat 1
--- test''' = <0>
+identity(n :: #) -> Thin(n, n)
+identity(0) = zero
+identity(succ(_)) = succ(identity(!))
 
-mapOn :: (th :: x <<< y), (f :: X -> X), Vec(X, y) -> Vec(X, y)
-mapOn = ?mapOn
+empty(n :: #) -> Thin(0, n)
+empty(0) = zero
+empty(succ(_)) = omit(empty(!))
 
-map = mapOn {1,4} f vec
+comp(l :: #, n :: #, m :: #, Thin(l, n), Thin(n, m)) -> Thin(l, m)
+comp(_, _, _, th, omit(ph)) = omit(comp(!, !, !, th, ph))
+comp(_, _, _, omit(th), succ(ph)) = omit(comp(!, !, !, th, ph))
+comp(_, _, _, succ(th), succ(ph)) = succ(comp(!, !, !, th, ph))
+comp(_, _, _, zero, zero) = zero
+
+thinning1 :: Thin(3, 5)
+thinning1 = succ(omit(succ(succ(omit(zero)))))
+
+thinning2 :: Thin(1, 3)
+thinning2 = omit(succ(omit(zero)))
+
+thinning :: Thin(1, 5)
+thinning = comp(!, !, !, thinning2, thinning1)
+
+go2 :: Vec(Nat, 3)
+go2 = select(!, !, !, thinning1, [1,2,3,4,5])
+
+go :: Vec(Nat, 1)
+go = select(!, !, !, thinning, [1,2,3,4,5])
+
+merge(X :: *, l :: #, n :: #, m :: #, Thin(n, m), Vec(X, n), Vec(X, l), l + n = m) -> Vec(X, m)
+merge(_, _, _, _, zero, [], ys, _) = ys
+merge(_, _, _, _, succ(th), x ,- xs, ys, _) = x ,- merge(!, !, !, !, th, xs, ys, !)
+merge(_, _, _, _, omit(th), xs, y ,- ys, _) = y ,- merge(!, !, !, !, th, xs, ys, !)
+
+--partMerge(X :: *, l :: #, n :: #, m :: #, l + n = m, Thin(n, m), Vec(X, m)) -> Vec(X, m)
+--partMerge(_, _, _, _, _, th, xs) =
+-- let outs, ins = partition(!, !, !, !, !, th, xs) in
+--  merge(!, !, !, !, th, outs, ins, !)
+
+
+-- focus(X :: *, n :: #, m :: #, Thin(n, m), { Vec(X, n) -> Vec(X, n) }) -> { Vec(X, m) -> Vec(X, m) }
+-- focus(_, _, th, f) = { xs =>
+--  let outs, ins = partition(!, !, !, !, !, th, xs) in
+--    merge(!, !, !, !, th, f(ins), outs, !)
+-- }
diff --git a/brat/lsp/Brat/LSP/Find.hs b/brat/lsp/Brat/LSP/Find.hs
index 098ba526..2ed9987f 100644
--- a/brat/lsp/Brat/LSP/Find.hs
+++ b/brat/lsp/Brat/LSP/Find.hs
@@ -6,12 +6,12 @@ import Data.List.NonEmpty (NonEmpty(..), toList)
 import Data.Maybe (mapMaybe)
 
 import Brat.FC
+import Brat.Load (VDecl(..))
 import Brat.LSP.State
 import Brat.Syntax.Common
 import Brat.Syntax.Concrete (Flat(..))
 import Brat.Syntax.Core
 import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..))
-import Brat.Syntax.Value (VDecl(..))
 import Brat.Unelaborator (unelab)
 
 data Context
diff --git a/brat/lsp/Brat/LSP/State.hs b/brat/lsp/Brat/LSP/State.hs
index c6300ace..41e4f44c 100644
--- a/brat/lsp/Brat/LSP/State.hs
+++ b/brat/lsp/Brat/LSP/State.hs
@@ -1,8 +1,8 @@
 module Brat.LSP.State (ProgramState(..), emptyPS, updateState) where
 
 import Brat.Checker.Types (TypedHole)
+import Brat.Load (VDecl)
 import Brat.Syntax.Raw
-import Brat.Syntax.Value (VDecl)
 
 data ProgramState
   = PS { decls :: [VDecl]
diff --git a/brat/test/Main.hs b/brat/test/Main.hs
index 3e0fda2b..dd056fd5 100644
--- a/brat/test/Main.hs
+++ b/brat/test/Main.hs
@@ -2,6 +2,7 @@ import Test.Tasty  (testGroup)
 import Test.Tasty.Silver.Interactive (defaultMain)
 
 import Test.Abstractor
+import Test.Arithmetic
 import Test.Examples
 import Test.Graph
 import Test.Elaboration
@@ -35,7 +36,7 @@ coroT1 = do
           Just _ -> err $ InternalError "already defined"
           Nothing -> defineEnd "test" e (VCon (PrefixName [] "nil") [])
       )
-  mkYield "coroT1" (S.singleton e) >> pure ()
+  mkYield (TypeErr "coroT1") "coroT1" (S.singleton e) >> pure ()
   --traceM "Yield continued"
   v <- req $ ELup e
   case v of
@@ -48,7 +49,7 @@ coroT2 = do
   let e = InEnd $ In name 0
   req $ Declare e Braty (Left $ Star []) Definable
   v <- do
-    mkYield "coroT2" (S.singleton e)
+    mkYield (TypeErr "coroT2") "coroT2" (S.singleton e)
     req $ ELup e
   -- No way to execute this without a 'v'
   mkFork "t2" $ defineEnd "test" e (VCon (PrefixName [] "nil") [])
@@ -79,4 +80,5 @@ main = do
                                 ,typeArithTests
                                 ,coroTests
                                 ,spliceTests
+                                ,test_simplify
                                 ]
diff --git a/brat/test/Test/Arithmetic.hs b/brat/test/Test/Arithmetic.hs
new file mode 100644
index 00000000..834f8ebb
--- /dev/null
+++ b/brat/test/Test/Arithmetic.hs
@@ -0,0 +1,19 @@
+module Test.Arithmetic where
+
+import Brat.Checker.Arithmetic
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+test_simplify :: TestTree
+test_simplify = testGroup "simplify" $
+    [testCase "gcd_and_flip" $
+       (nsVar "x" `nsMul` 2, nsVar "y" <> nsConst 3) @=? simplify (nsConst 6 <> (nsVar "y" `nsMul` 2), nsVar "x" `nsMul` 4)
+    ,testCase "onevar" $
+        let expected = (nsVar "x", nsConst 3)
+            lhs = (nsConst 42) <> (nsVar "x" `nsMul` 10)
+            rhs = (nsConst 63) <> (nsVar "x" `nsMul` 3)
+        in expected @=? simplify (lhs, rhs)
+    ,testCase "multi" $
+      (nsVar "x", nsConst 1) @=? simplify (nsVar "x" `nsMul` 2 <> nsVar "y", nsVar "y" <> nsConst 2)
+    ]
diff --git a/brat/test/Test/Syntax/Let.hs b/brat/test/Test/Syntax/Let.hs
index bd748872..71dcd966 100644
--- a/brat/test/Test/Syntax/Let.hs
+++ b/brat/test/Test/Syntax/Let.hs
@@ -28,8 +28,8 @@ test = testCase "let" $
       tm = Let
         (dummyFC ("x" :||: "y"))
         (dummyFC (dummyFC (num 1 :|: num 2)
-               ::: [("a", Right (Con (plain "Int") (dummyFC Empty)))
-                   ,("b", Right (Con (plain "Int") (dummyFC Empty)))
+               ::: [Named "a" (Right (Con (plain "Int") (dummyFC Empty)))
+                   ,Named "b" (Right (Con (plain "Int") (dummyFC Empty)))
                    ])
         )
         (dummyFC (Var "x"))
diff --git a/brat/test/golden/binding/let.brat.golden b/brat/test/golden/binding/let.brat.golden
index 95c5c1c9..86ac42af 100644
--- a/brat/test/golden/binding/let.brat.golden
+++ b/brat/test/golden/binding/let.brat.golden
@@ -3,5 +3,5 @@ badBinding = let x = twoThings in x
              ^^^^^^^^^^^^^^^^^^^^^^
 
   Internal error: Expected empty unders after abstract, got:
-  (b1 :: Int)
+  (_1 :: Int)
 
diff --git a/brat/test/golden/error/apply_two_thunks.brat.golden b/brat/test/golden/error/apply_two_thunks.brat.golden
index a91ab7f1..ec1da67f 100644
--- a/brat/test/golden/error/apply_two_thunks.brat.golden
+++ b/brat/test/golden/error/apply_two_thunks.brat.golden
@@ -3,5 +3,5 @@ go(n) = thunks(n)
         ^^^^^^^^^
 
   Type error: Expected function thunks() to consume all of its arguments (「n」)
- but found leftovers: (a1 :: Int)
+ but found leftovers: (_0 :: Int)
 
diff --git a/brat/test/golden/error/empty_into.brat.golden b/brat/test/golden/error/empty_into.brat.golden
index 9f669992..fe635cc5 100644
--- a/brat/test/golden/error/empty_into.brat.golden
+++ b/brat/test/golden/error/empty_into.brat.golden
@@ -3,7 +3,7 @@ intoErr = |> makeInt
           ^^^^^^^^^^
 
   Type mismatch when checking makeInt()(())
-Expected: (a1 :: Bool)
-But got:  (a1 :: Int)
+Expected: (_0 :: Bool)
+But got:  (_0 :: Int)
 
 
diff --git a/brat/test/golden/error/fanout-diff-types.brat.golden b/brat/test/golden/error/fanout-diff-types.brat.golden
index abde4a2f..82430baa 100644
--- a/brat/test/golden/error/fanout-diff-types.brat.golden
+++ b/brat/test/golden/error/fanout-diff-types.brat.golden
@@ -3,7 +3,7 @@ f = { [/\] }
       ^^^^
 
   Type mismatch when checking [/\]
-Expected: (b1 :: Bit)
+Expected: (_1 :: Bit)
 But got:  (head :: Qubit)
 
 
diff --git a/brat/test/golden/error/fanout-not-enough-overs.brat.golden b/brat/test/golden/error/fanout-not-enough-overs.brat.golden
index a1ac9d3c..7cb723fb 100644
--- a/brat/test/golden/error/fanout-not-enough-overs.brat.golden
+++ b/brat/test/golden/error/fanout-not-enough-overs.brat.golden
@@ -2,5 +2,5 @@ Error in test/golden/error/fanout-not-enough-overs.brat on line 2:
 f = { [/\] }
     ^^^^^^^^
 
-  Expected function to return additional values of type: (c1 :: Nat)
+  Expected function to return additional values of type: (_3 :: Nat)
 
diff --git a/brat/test/golden/error/pair.brat.golden b/brat/test/golden/error/pair.brat.golden
index 51074f8a..33fd6b91 100644
--- a/brat/test/golden/error/pair.brat.golden
+++ b/brat/test/golden/error/pair.brat.golden
@@ -3,7 +3,7 @@ pair = row -- Distinct from a pair
        ^^^
 
   Type mismatch when checking row
-Expected: (a1 :: [Int,Bool])
-But got:  (a1 :: Int), (b1 :: Bool)
+Expected: (_0 :: [Int,Bool])
+But got:  (_0 :: Int, _1 :: Bool)
 
 
diff --git a/brat/test/golden/error/portpull-ambiguous.brat.golden b/brat/test/golden/error/portpull-ambiguous.brat.golden
index bc45791d..f9d0e292 100644
--- a/brat/test/golden/error/portpull-ambiguous.brat.golden
+++ b/brat/test/golden/error/portpull-ambiguous.brat.golden
@@ -2,5 +2,5 @@ Error in test/golden/error/portpull-ambiguous.brat on line 6:
 id2 = x, y => (id,id)(a1:x, y)
                      ^^^^^^^^^
 
-  Port a1 is ambiguous in (a1 :: Nat), (a1 :: Nat)
+  Port not found: a1 in (_0 :: Nat, _0 :: Nat)
 
diff --git a/brat/test/golden/error/portpull.brat.golden b/brat/test/golden/error/portpull.brat.golden
index f6a2fd2a..7d0e7bc0 100644
--- a/brat/test/golden/error/portpull.brat.golden
+++ b/brat/test/golden/error/portpull.brat.golden
@@ -2,5 +2,5 @@ Error in test/golden/error/portpull.brat on line 6:
 id2 = x,y => (id, id)(a1:x, y)
                      ^^^^^^^^^
 
-  Port a1 is ambiguous in (a1 :: Nat), (a1 :: Nat)
+  Port not found: a1 in (_0 :: Nat, _0 :: Nat)
 
diff --git a/brat/test/golden/error/remaining_holes.brat.golden b/brat/test/golden/error/remaining_holes.brat.golden
index 73ae06cc..829d801b 100644
--- a/brat/test/golden/error/remaining_holes.brat.golden
+++ b/brat/test/golden/error/remaining_holes.brat.golden
@@ -1,4 +1,4 @@
 Can't compile file with remaining holes
-  ?a_hole :: (a1 :: Bit)
-  ?b_hole :: (thunk :: { (a1 :: Int) -> (a1 :: List(Int)) })
+  ?a_hole :: (_0 :: Bit)
+  ?b_hole :: (thunk :: { (_0 :: Int) -> (_1 :: List(Int)) })
 
diff --git a/brat/test/golden/error/toplevel-leftovers.brat.golden b/brat/test/golden/error/toplevel-leftovers.brat.golden
index 797eac59..222e5cb4 100644
--- a/brat/test/golden/error/toplevel-leftovers.brat.golden
+++ b/brat/test/golden/error/toplevel-leftovers.brat.golden
@@ -3,7 +3,7 @@ f = 42
     ^^
 
   Type mismatch when checking f
-Expected: (a1 :: Nat), (b1 :: Bool)
-But got:  (a1 :: Nat)
+Expected: (_0 :: Nat, _1 :: Bool)
+But got:  (_0 :: Nat)
 
 
diff --git a/brat/test/golden/error/toplevel-leftovers2.brat.golden b/brat/test/golden/error/toplevel-leftovers2.brat.golden
index 7951cf7e..47ac772b 100644
--- a/brat/test/golden/error/toplevel-leftovers2.brat.golden
+++ b/brat/test/golden/error/toplevel-leftovers2.brat.golden
@@ -4,7 +4,7 @@ f(x) = x
 
   Type mismatch when checking x => 「x」
 
-Expected: (a1 :: Nat), (b1 :: Bool)
-But got:  (a1 :: Nat)
+Expected: (_1 :: Nat, _2 :: Bool)
+But got:  (_1 :: Nat)
 
 
diff --git a/brat/test/golden/error/toplevel-leftovers3.brat.golden b/brat/test/golden/error/toplevel-leftovers3.brat.golden
index 84290ebb..b661fdff 100644
--- a/brat/test/golden/error/toplevel-leftovers3.brat.golden
+++ b/brat/test/golden/error/toplevel-leftovers3.brat.golden
@@ -2,5 +2,5 @@ Error in test/golden/error/toplevel-leftovers3.brat on line 2:
 f(x) = x
   ^
 
-  Type error: Inputs (b1 :: Bool) weren't used
+  Type error: Inputs (_1 :: Bool) weren't used
 
diff --git a/brat/test/golden/error/vectorise-type-mismatch.brat.golden b/brat/test/golden/error/vectorise-type-mismatch.brat.golden
index 85d0a773..22634fd0 100644
--- a/brat/test/golden/error/vectorise-type-mismatch.brat.golden
+++ b/brat/test/golden/error/vectorise-type-mismatch.brat.golden
@@ -3,6 +3,6 @@ panic = 2 of 42
         ^^^^^^^
 
   Type error: Got: Vector of length 2
-Expected: (a1 :: Vec(Nat, 1))
+Expected: (_0 :: Vec(Nat, 1))
 
 
diff --git a/brat/test/golden/error/vectorise3.brat.golden b/brat/test/golden/error/vectorise3.brat.golden
index b21f57b1..1e44756c 100644
--- a/brat/test/golden/error/vectorise3.brat.golden
+++ b/brat/test/golden/error/vectorise3.brat.golden
@@ -3,5 +3,5 @@ f(_, _, n, f, xs) = (n of f)(xs)
                     ^^^^^^^^^^^^
 
   Type error: Expected function 「n」 of f() to consume all of its arguments (「xs」)
- but found leftovers: (b1 :: Vec(VApp VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 0 B0, VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 2))
+ but found leftovers: (_1 :: Vec(VApp VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 0 B0, VPar Ex checking_vectorise3_check_defs_1_f_$lhs_3_lambda_fake_source 2))
 
diff --git a/brat/test/golden/graph/addN2.brat.graph b/brat/test/golden/graph/addN2.brat.graph
index 7dfa6937..fb55e830 100644
--- a/brat/test/golden/graph/addN2.brat.graph
+++ b/brat/test/golden/graph/addN2.brat.graph
@@ -18,7 +18,7 @@ Nodes:
 (addN2.brat_globals_Int_12,BratNode (Constructor Int) [] [("value",[])])
 (addN2.brat_globals_decl_13_addN,BratNode Id [("thunk",{ (inp :: Int) -> (out :: Int) })] [("thunk",{ (inp :: Int) -> (out :: Int) })])
 (addN2.brat_globals_prim_2_N,BratNode (Prim ("","N")) [] [("value",Int)])
-(addN2.brat_globals_prim_8_add,BratNode (Prim ("","add")) [] [("a1",{ (a :: Int), (b :: Int) -> (c :: Int) })])
+(addN2.brat_globals_prim_8_add,BratNode (Prim ("","add")) [] [("_0",{ (a :: Int), (b :: Int) -> (c :: Int) })])
 
 Wires:
 (Ex addN2.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_$rhs_4_Eval 0,Int,In addN2.brat_check_defs_1_addN_LambdaChk_9_checkClauses_1_lambda.0_rhs/out_2 0)
diff --git a/brat/test/golden/graph/cons.brat.graph b/brat/test/golden/graph/cons.brat.graph
index 7dc26783..fe6f49bc 100644
--- a/brat/test/golden/graph/cons.brat.graph
+++ b/brat/test/golden/graph/cons.brat.graph
@@ -30,8 +30,8 @@ Nodes:
 (cons.brat_globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
 (cons.brat_globals_const_3,BratNode (Const 2) [] [("value",Nat)])
 (cons.brat_globals_const_8,BratNode (Const 3) [] [("value",Nat)])
-(cons.brat_globals_decl_4_two,BratNode Id [("a1",Vec(Int, 2))] [("a1",Vec(Int, 2))])
-(cons.brat_globals_decl_9_three,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
+(cons.brat_globals_decl_4_two,BratNode Id [("_0",Vec(Int, 2))] [("_0",Vec(Int, 2))])
+(cons.brat_globals_decl_9_three,BratNode Id [("_0",Vec(Int, 3))] [("_0",Vec(Int, 3))])
 
 Wires:
 (Ex cons.brat_check_defs_1_three_2_$rhs_check'Con__2 0,[],In cons.brat_check_defs_1_three_2_$rhs_check'Con_$!_pat2val 0)
diff --git a/brat/test/golden/graph/id.brat.graph b/brat/test/golden/graph/id.brat.graph
index 7d16ffe1..e6a6e03d 100644
--- a/brat/test/golden/graph/id.brat.graph
+++ b/brat/test/golden/graph/id.brat.graph
@@ -11,7 +11,7 @@ Nodes:
 (id.brat_check_defs_1_main_$rhs_check'Th_thunk_thunk_2,BratNode (Box id.brat_check_defs_1_main_$rhs_check'Th_thunk/in id.brat_check_defs_1_main_$rhs_check'Th_thunk/out_1) [] [("thunk",{ (a :: Qubit) -o (b :: Qubit) })])
 (id.brat_globals_Qubit_2,BratNode (Constructor Qubit) [] [("value",[])])
 (id.brat_globals_Qubit_4,BratNode (Constructor Qubit) [] [("value",[])])
-(id.brat_globals_decl_5_main,BratNode Id [("a1",{ (a :: Qubit) -o (b :: Qubit) })] [("a1",{ (a :: Qubit) -o (b :: Qubit) })])
+(id.brat_globals_decl_5_main,BratNode Id [("_0",{ (a :: Qubit) -o (b :: Qubit) })] [("_0",{ (a :: Qubit) -o (b :: Qubit) })])
 
 Wires:
 (Ex id.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 0,Qubit,In id.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 0)
diff --git a/brat/test/golden/graph/kernel.brat.graph b/brat/test/golden/graph/kernel.brat.graph
index 130eb5b5..f5bcae9a 100644
--- a/brat/test/golden/graph/kernel.brat.graph
+++ b/brat/test/golden/graph/kernel.brat.graph
@@ -1,7 +1,7 @@
 Nodes:
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1,KernelNode Target [("a1",Vec(Qubit, 3))] [])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1) [] [("thunk",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in,KernelNode Source [] [("_0",Qubit),("_1",Qubit),("_2",Qubit)])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1,KernelNode Target [("_0",Vec(Qubit, 3))] [])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/out_1) [] [("thunk",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })])
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con__2,BratNode (Dummy $) [] [("dummy",[])])
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_pat2val,BratNode Id [("",[])] [("",[])])
@@ -25,19 +25,19 @@ Nodes:
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst,BratNode (Const 2) [] [("value",Nat)])
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_typeEqsTail_1_$!_1_buildConst_2,BratNode (Const 0) [] [("value",Nat)])
 (kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1,KernelNode Source [] [("q0",Qubit),("q1",Qubit),("q2",Qubit)])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2,KernelNode Target [("a1",Vec(Qubit, 3))] [])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2) [] [("thunk",{ (q0 :: Qubit), (q1 :: Qubit), (q2 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda,KernelNode (PatternMatch ((TestMatchData Kerny (MatchSequence {matchInputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "a1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "b1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "c1"},Qubit)], matchTests = [], matchOutputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "a1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "b1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "c1"},Qubit)]}),kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3) :| [])) [("a1",Qubit),("b1",Qubit),("c1",Qubit)] [("a1",Vec(Qubit, 3))])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1,KernelNode Target [("a1",Vec(Qubit, 3))] [])
-(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1) [] [("thunk",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2,KernelNode Target [("_0",Vec(Qubit, 3))] [])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2) [] [("thunk",{ (q0 :: Qubit), (q1 :: Qubit), (q2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda,KernelNode (PatternMatch ((TestMatchData Kerny (MatchSequence {matchInputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "_0"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "_1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "_2"},Qubit)], matchTests = [], matchOutputs = [(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 0, portName = "_0"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 1, portName = "_1"},Qubit),(NamedPort {end = Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$lhs_lambda.0_setup/in 2, portName = "_2"},Qubit)]}),kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs_thunk_3) :| [])) [("_0",Qubit),("_1",Qubit),("_2",Qubit)] [("_0",Vec(Qubit, 3))])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in,KernelNode Source [] [("_0",Qubit),("_1",Qubit),("_2",Qubit)])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1,KernelNode Target [("_0",Vec(Qubit, 3))] [])
+(kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2,BratNode (Box kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/out_1) [] [("thunk",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })])
 (kernel.brat_globals_Qubit_2,BratNode (Constructor Qubit) [] [("value",[])])
 (kernel.brat_globals_Qubit_3,BratNode (Constructor Qubit) [] [("value",[])])
 (kernel.brat_globals_Qubit_4,BratNode (Constructor Qubit) [] [("value",[])])
 (kernel.brat_globals_Qubit_7,BratNode (Constructor Qubit) [] [("value",[])])
 (kernel.brat_globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
 (kernel.brat_globals_const_8,BratNode (Const 3) [] [("value",Nat)])
-(kernel.brat_globals_decl_9_id3,BratNode Id [("a1",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })] [("a1",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
+(kernel.brat_globals_decl_9_id3,BratNode Id [("_0",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })] [("_0",{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) })])
 
 Wires:
 (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con__2 0,[],In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_check'Con_$!_pat2val 0)
@@ -62,7 +62,7 @@ Wires:
 (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 0,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 0)
 (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 1,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 1)
 (Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk/in 2,Qubit,In kernel.brat_check_defs_1_id3_$rhs_check'Th_LambdaChk_6_lambda 2)
-(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2 0,{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) },In kernel.brat_globals_decl_9_id3 0)
+(Ex kernel.brat_check_defs_1_id3_$rhs_check'Th_thunk_thunk_2 0,{ (_0 :: Qubit), (_1 :: Qubit), (_2 :: Qubit) -o (_0 :: Vec(Qubit, 3)) },In kernel.brat_globals_decl_9_id3 0)
 (Ex kernel.brat_globals_Qubit_2 0,[],In kernel.brat_globals___kcr__1 0)
 (Ex kernel.brat_globals_Qubit_3 0,[],In kernel.brat_globals___kcr__1 1)
 (Ex kernel.brat_globals_Qubit_4 0,[],In kernel.brat_globals___kcr__1 2)
diff --git a/brat/test/golden/graph/list.brat.graph b/brat/test/golden/graph/list.brat.graph
index 5b7fb356..77e74475 100644
--- a/brat/test/golden/graph/list.brat.graph
+++ b/brat/test/golden/graph/list.brat.graph
@@ -16,7 +16,7 @@ Nodes:
 (list.brat_check_defs_1_xs_$rhs_check'Con_const_4,BratNode (Const 1) [] [("value",Int)])
 (list.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (list.brat_globals_List_1,BratNode (Constructor List) [("listValue",[])] [("value",[])])
-(list.brat_globals_decl_3_xs,BratNode Id [("a1",List(Int))] [("a1",List(Int))])
+(list.brat_globals_decl_3_xs,BratNode Id [("_0",List(Int))] [("_0",List(Int))])
 
 Wires:
 (Ex list.brat_check_defs_1_xs_$rhs_check'Con__2 0,[],In list.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val 0)
diff --git a/brat/test/golden/graph/num.brat.graph b/brat/test/golden/graph/num.brat.graph
index 099d7e13..5365a1e0 100644
--- a/brat/test/golden/graph/num.brat.graph
+++ b/brat/test/golden/graph/num.brat.graph
@@ -5,8 +5,8 @@ Nodes:
 (num.brat_check_defs_1_n_$rhs_check'Con_succ_1,BratNode (Constructor succ) [("value",Nat)] [("value",Nat)])
 (num.brat_globals_Int_4,BratNode (Constructor Int) [] [("value",[])])
 (num.brat_globals_Nat_1,BratNode (Constructor Nat) [] [("value",[])])
-(num.brat_globals_decl_2_n,BratNode Id [("a1",Nat)] [("a1",Nat)])
-(num.brat_globals_decl_5_m,BratNode Id [("a1",Int)] [("a1",Int)])
+(num.brat_globals_decl_2_n,BratNode Id [("_0",Nat)] [("_0",Nat)])
+(num.brat_globals_decl_5_m,BratNode Id [("_0",Int)] [("_0",Int)])
 
 Wires:
 (Ex num.brat_check_defs_1_m_2_$rhs_check'Con_const_2 0,Int,In num.brat_check_defs_1_m_2_$rhs_check'Con_doub_1 0)
diff --git a/brat/test/golden/graph/pair.brat.graph b/brat/test/golden/graph/pair.brat.graph
index 7ac1db68..065f7796 100644
--- a/brat/test/golden/graph/pair.brat.graph
+++ b/brat/test/golden/graph/pair.brat.graph
@@ -16,7 +16,7 @@ Nodes:
 (pair.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (pair.brat_globals_cons_1,BratNode (Constructor cons) [("head",[]),("tail",[])] [("value",[])])
 (pair.brat_globals_cons_3,BratNode (Constructor cons) [("head",[]),("tail",[])] [("value",[])])
-(pair.brat_globals_decl_6_xs,BratNode Id [("a1",[Int,Bool])] [("a1",[Int,Bool])])
+(pair.brat_globals_decl_6_xs,BratNode Id [("_0",[Int,Bool])] [("_0",[Int,Bool])])
 (pair.brat_globals_nil_5,BratNode (Constructor nil) [] [("value",[])])
 
 Wires:
diff --git a/brat/test/golden/graph/rx.brat.graph b/brat/test/golden/graph/rx.brat.graph
index f0767503..38869cc3 100644
--- a/brat/test/golden/graph/rx.brat.graph
+++ b/brat/test/golden/graph/rx.brat.graph
@@ -13,7 +13,7 @@ Nodes:
 (rx.brat_check_defs_1_nums_$rhs_const,BratNode (Const 1) [] [("value",Int)])
 (rx.brat_check_defs_1_nums_$rhs_const_1,BratNode (Const 2) [] [("value",Int)])
 (rx.brat_check_defs_1_nums_$rhs_const_2,BratNode (Const 3) [] [("value",Int)])
-(rx.brat_check_defs_1_xish_1_$rhs_Eval,BratNode (Eval (Ex rx.brat_globals_prim_7_Rx 0)) [("th",Float)] [("a1",{ (rxa :: Qubit) -o (rxb :: Qubit) })])
+(rx.brat_check_defs_1_xish_1_$rhs_Eval,BratNode (Eval (Ex rx.brat_globals_prim_7_Rx 0)) [("th",Float)] [("_1",{ (rxa :: Qubit) -o (rxb :: Qubit) })])
 (rx.brat_check_defs_1_xish_1_$rhs_const_1,BratNode (Const 30.0) [] [("value",Float)])
 (rx.brat_globals_Float_2,BratNode (Constructor Float) [] [("value",[])])
 (rx.brat_globals_Int_9,BratNode (Constructor Int) [] [("value",[])])
@@ -26,9 +26,9 @@ Nodes:
 (rx.brat_globals_Qubit_21,BratNode (Constructor Qubit) [] [("value",[])])
 (rx.brat_globals_Qubit_23,BratNode (Constructor Qubit) [] [("value",[])])
 (rx.brat_globals_decl_12_nums,BratNode Id [("x",Int),("y",Int),("z",Int)] [("x",Int),("y",Int),("z",Int)])
-(rx.brat_globals_decl_18_xish,BratNode Id [("a1",{ (rxa :: Qubit) -o (rxb :: Qubit) })] [("a1",{ (rxa :: Qubit) -o (rxb :: Qubit) })])
-(rx.brat_globals_decl_24_main,BratNode Id [("a1",{ (a :: Qubit) -o (b :: Qubit) })] [("a1",{ (a :: Qubit) -o (b :: Qubit) })])
-(rx.brat_globals_prim_7_Rx,BratNode (Prim ("","Rx")) [] [("thunk",{ (th :: Float) -> (a1 :: { (rxa :: Qubit) -o (rxb :: Qubit) }) })])
+(rx.brat_globals_decl_18_xish,BratNode Id [("_0",{ (rxa :: Qubit) -o (rxb :: Qubit) })] [("_0",{ (rxa :: Qubit) -o (rxb :: Qubit) })])
+(rx.brat_globals_decl_24_main,BratNode Id [("_0",{ (a :: Qubit) -o (b :: Qubit) })] [("_0",{ (a :: Qubit) -o (b :: Qubit) })])
+(rx.brat_globals_prim_7_Rx,BratNode (Prim ("","Rx")) [] [("thunk",{ (th :: Float) -> (_1 :: { (rxa :: Qubit) -o (rxb :: Qubit) }) })])
 
 Wires:
 (Ex rx.brat_check_defs_1_main_3_$rhs_check'Th_LambdaChk_6_checkClauses_1_$rhs_4_Splice 0,Qubit,In rx.brat_check_defs_1_main_3_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 0)
diff --git a/brat/test/golden/graph/swap.brat.graph b/brat/test/golden/graph/swap.brat.graph
index 931f8f27..876ad656 100644
--- a/brat/test/golden/graph/swap.brat.graph
+++ b/brat/test/golden/graph/swap.brat.graph
@@ -13,7 +13,7 @@ Nodes:
 (swap.brat_globals_Qubit_3,BratNode (Constructor Qubit) [] [("value",[])])
 (swap.brat_globals_Qubit_5,BratNode (Constructor Qubit) [] [("value",[])])
 (swap.brat_globals_Qubit_6,BratNode (Constructor Qubit) [] [("value",[])])
-(swap.brat_globals_decl_7_main,BratNode Id [("a1",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })] [("a1",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })])
+(swap.brat_globals_decl_7_main,BratNode Id [("_0",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })] [("_0",{ (a :: Qubit), (b :: Qubit) -o (b :: Qubit), (a :: Qubit) })])
 
 Wires:
 (Ex swap.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/in_1 0,Qubit,In swap.brat_check_defs_1_main_$rhs_check'Th_LambdaChk_6_checkClauses_1_lambda.0_rhs/out_2 1)
diff --git a/brat/test/golden/graph/two.brat.graph b/brat/test/golden/graph/two.brat.graph
index 3afc7eab..3722863d 100644
--- a/brat/test/golden/graph/two.brat.graph
+++ b/brat/test/golden/graph/two.brat.graph
@@ -8,7 +8,7 @@ Nodes:
 (two.brat_globals_Int_7,BratNode (Constructor Int) [] [("value",[])])
 (two.brat_globals_Int_10,BratNode (Constructor Int) [] [("value",[])])
 (two.brat_globals_decl_8_one,BratNode Id [("n",Int)] [("n",Int)])
-(two.brat_globals_decl_11_two,BratNode Id [("a1",Int)] [("a1",Int)])
+(two.brat_globals_decl_11_two,BratNode Id [("_0",Int)] [("_0",Int)])
 (two.brat_globals_prim_5_add,BratNode (Prim ("","add")) [] [("thunk",{ (a :: Int), (b :: Int) -> (c :: Int) })])
 
 Wires:
diff --git a/brat/test/golden/graph/vec.brat.graph b/brat/test/golden/graph/vec.brat.graph
index 301605ea..719e888a 100644
--- a/brat/test/golden/graph/vec.brat.graph
+++ b/brat/test/golden/graph/vec.brat.graph
@@ -27,7 +27,7 @@ Nodes:
 (vec.brat_globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (vec.brat_globals_Vec_1,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
 (vec.brat_globals_const_3,BratNode (Const 3) [] [("value",Nat)])
-(vec.brat_globals_decl_4_xs,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
+(vec.brat_globals_decl_4_xs,BratNode Id [("_0",Vec(Int, 3))] [("_0",Vec(Int, 3))])
 
 Wires:
 (Ex vec.brat_check_defs_1_xs_$rhs_check'Con__2 0,[],In vec.brat_check_defs_1_xs_$rhs_check'Con_$!_pat2val 0)
diff --git a/brat/test/golden/kernel/kernel_application.brat.golden b/brat/test/golden/kernel/kernel_application.brat.golden
index af09def9..0e8f7657 100644
--- a/brat/test/golden/kernel/kernel_application.brat.golden
+++ b/brat/test/golden/kernel/kernel_application.brat.golden
@@ -2,5 +2,5 @@ Error in test/golden/kernel/kernel_application.brat on line 16:
 rotate = { q => maybeRotate(true) }
                 ^^^^^^^^^^^
 
-  Type error: Expected a (kernel) function or vector of functions, got { (a1 :: Bool) -> (a1 :: { (a1 :: Qubit) -o (a1 :: Qubit) }) }
+  Type error: Expected a (kernel) function or vector of functions, got { (_0 :: Bool) -> (_1 :: { (_0 :: Qubit) -o (_0 :: Qubit) }) }