diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs
index 3b317be0..4e5cbe18 100644
--- a/brat/Brat/Checker.hs
+++ b/brat/Brat/Checker.hs
@@ -48,6 +48,8 @@ import Bwd
 import Hasochism
 import Util (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
 standardise :: TypeKind -> Val Z -> Checking (Val Z)
@@ -456,11 +458,23 @@ check' tm@(Con vcon vargs) ((), (hungry, ty):unders) = case (?my, ty) of
  where
   aux :: Modey m -> (QualName -> QualName -> Checking (CtorArgs m)) -> Val Z -> Checking ()
   aux my lup ty = do
+    -- TODO: Use concurrency to avoid strictness - we don't have to work out that
+    -- this is a VCon immediately.
     VCon tycon tyargs <- eval S0 ty
+    -- traceM $ "checking constructor of type: " ++ show tycon ++ " " ++ show tyargs
     (CArgs pats nFree _ argTypeRo) <- lup vcon tycon
     -- Look for vectors to produce better error messages for mismatched lengths
-    wrap <- detectVecErrors vcon tycon tyargs pats ty (Left tm)
-    Some (ny :* env) <- throwLeft $ valMatches tyargs pats
+    -- wrap <- detectVecErrors vcon tycon tyargs pats ty (Left tm)
+    -- Get the kinds of type args
+    let m = deModey my -- TODO: remember what this is
+    (_, ks) <- unzip <$> tlup (m, tycon)
+    -- Turn `pats` into values for unification
+    (varz, patVals) <- valPats2Val ks pats
+    -- traceM $ "problem: " ++ show tyargs ++ " =?= " ++ show patVals
+    -- Create a unification problem between tyargs and the value versions of pats
+    typeEq (show tycon) (TypeFor m []) (VCon tycon tyargs) (VCon tycon patVals)
+    -- traceM "Made it past unification"
+    Some (ny :* env) <- pure $ bwdStack varz
     -- Make sure env is the correct length for args
     Refl <- throwLeft $ natEqOrBust ny nFree
     let topy = roTopM my ny argTypeRo
@@ -468,10 +482,11 @@ check' tm@(Con vcon vargs) ((), (hungry, ty):unders) = case (?my, ty) of
     -- in the kernel case the bottom and top of the row are the same
     let ty' = weaken topy ty
     env <- traverseStack (sem S0) env
+    -- traceM $ "Matchenv: " ++ show env
     (_, argUnders, [(dangling, _)], _) <- anext (show vcon) (Constructor vcon)
                                           (env, Some (Zy :* S0))
                                           argTypeRo (RPr ("value", ty') R0)
-    (((), ()), ((), leftUnders)) <- wrapError wrap $ check vargs ((), argUnders)
+    (((), ()), ((), leftUnders)) <- {- wrapError wrap $ -} check vargs ((), argUnders)
     ensureEmpty "con unders" leftUnders
     wire (dangling, ty, hungry)
 
@@ -663,7 +678,7 @@ check' (Of n e) ((), unders) = case ?my of
 check' Hope ((), (NamedPort hope _, ty):unders) = case (?my, ty) of
   (Braty, Left _k) -> do
     fc <- req AskFC
-    req (ANewHope hope fc)
+    req (ANewHope hope (HopeData (Just fc) True))
     pure (((), ()), ((), unders))
   (Braty, Right _ty) -> typeErr "Can only infer kinded things with !"
   (Kerny, _) -> typeErr "Won't infer kernel typed !"
@@ -1146,11 +1161,11 @@ run ve initStore ns m = do
   -- If the `hopes` set has any remaining holes with kind Nat, we need to abort.
   -- Even though we didn't need them for typechecking problems, our runtime
   -- behaviour depends on the values of the holes, which we can't account for.
-  case M.toList $ M.filterWithKey (\e _ -> isNatKinded tyMap (InEnd e)) (hopes ctx) of
+  case M.toList $ M.filterWithKey (\e hd -> isNatKinded tyMap (InEnd e) && hopeDynamic hd) (hopes ctx) of
     [] -> pure (a, (holes, store ctx, graph))
     -- Just use the FC of the first hole while we don't have the capacity to
     -- show multiple error locations
-    hs@((_,fc):_) -> Left $ Err (Just fc) (RemainingNatHopes (show . fst <$> hs))
+    hs@((_,hd):_) -> Left $ Err (hopeFC hd) (RemainingNatHopes (show . fst <$> hs))
  where
   isNatKinded tyMap e = case tyMap M.! e of
     EndType Braty (Left Nat) -> True
diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs
index 9b0871e5..63141788 100644
--- a/brat/Brat/Checker/Helpers.hs
+++ b/brat/Brat/Checker/Helpers.hs
@@ -18,12 +18,13 @@ module Brat.Checker.Helpers {-(pullPortsRow, pullPortsSig
                             ,uncons
                             ,evalBinder
                             ,evalSrcRow, evalTgtRow
+			    ,solveHopeVal, solveHopeSem
                             )-} where
 
-import Brat.Checker.Monad (Checking, CheckingSig(..), captureOuterLocals, err, typeErr, kindArgRows, defineEnd)
+import Brat.Checker.Monad (Checking, CheckingSig(..), HopeData(..), captureOuterLocals, err, typeErr, kindArgRows, defineEnd, tlup)
 import Brat.Checker.Types
 import Brat.Error (ErrorMsg(..))
-import Brat.Eval (eval, EvMode(..), kindType)
+import Brat.Eval (eval, EvMode(..), kindType, quote, doesntOccur)
 import Brat.FC (FC)
 import Brat.Graph (Node(..), NodeType(..))
 import Brat.Naming (Name, FreshMonad(..))
@@ -36,6 +37,7 @@ import Bwd
 import Hasochism
 import Util (log2)
 
+import Control.Monad ((>=>))
 import Control.Monad.State.Lazy (StateT(..), runStateT)
 import Control.Monad.Freer (req)
 import Data.Bifunctor
@@ -45,6 +47,8 @@ import Data.Type.Equality (TestEquality(..), (:~:)(..))
 import qualified Data.Map as M
 import Prelude hiding (last)
 
+-- import Debug.Trace
+
 simpleCheck :: Modey m -> Val Z -> SimpleTerm -> Either ErrorMsg ()
 simpleCheck Braty TNat (Num n) | n >= 0 = pure ()
 simpleCheck Braty TInt (Num _) = pure ()
@@ -272,58 +276,12 @@ vecLayers :: Modey m -> Val Z -> Checking ([(Src, NumVal (VVar Z))] -- The sizes
                                           ,CTy m Z -- The function type at the end
                                           )
 vecLayers my (TVec ty (VNum n)) = do
-  src <- mkStaticNum n
+  src <- buildNatVal n
   first ((src, n):) <$> vecLayers my ty
 vecLayers Braty (VFun Braty cty) = pure ([], cty)
 vecLayers Kerny (VFun Kerny cty) = pure ([], cty)
 vecLayers my ty = typeErr $ "Expected a " ++ showMode my ++ "function or vector of functions, got " ++ show ty
 
-mkStaticNum :: NumVal (VVar Z) -> Checking Src
-mkStaticNum n@(NumValue c gro) = do
-  (_, [], [(constSrc,_)], _) <- next "const" (Const (Num (fromIntegral c))) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
-  src <- case gro of
-    Constant0 -> pure constSrc
-    StrictMonoFun sm -> do
-      (_, [(lhs,_),(rhs,_)], [(src,_)], _) <- next "add_const" (ArithNode Add) (S0, Some (Zy :* S0))
-                                              (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0))
-                                              (RPr ("value", TNat) R0)
-      smSrc <- mkStrictMono sm
-      wire (constSrc, TNat, lhs)
-      wire (smSrc, TNat, rhs)
-      pure src
-  defineSrc src (VNum n)
-  pure src
- where
-  mkStrictMono :: StrictMono (VVar Z) -> Checking Src
-  mkStrictMono (StrictMono k mono) = do
-    (_, [], [(constSrc,_)], _) <- next "2^k" (Const (Num (2^k))) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
-    (_, [(lhs,_),(rhs,_)], [(src,_)], _) <- next "mult_const" (ArithNode Mul) (S0, Some (Zy :* S0))
-                                            (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0))
-                                            (RPr ("value", TNat) R0)
-    monoSrc <- mkMono mono
-    wire (constSrc, TNat, lhs)
-    wire (monoSrc, TNat, rhs)
-    pure src
-
-  mkMono :: Monotone (VVar Z) -> Checking Src
-  mkMono (Linear (VPar (ExEnd e))) = pure (NamedPort e "mono")
-  mkMono (Full sm) = do
-    (_, [], [(twoSrc,_)], _) <- next "2" (Const (Num 2)) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
-    (_, [(lhs,_),(rhs,_)], [(powSrc,_)], _) <- next "2^" (ArithNode Pow) (S0, Some (Zy :* S0))
-                                               (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0))
-                                               (RPr ("value", TNat) R0)
-    smSrc <- mkStrictMono sm
-    wire (twoSrc, TNat, lhs)
-    wire (smSrc, TNat, rhs)
-
-    (_, [], [(oneSrc,_)], _) <- next "1" (Const (Num 1)) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
-    (_, [(lhs,_),(rhs,_)], [(src,_)], _) <- next "n-1" (ArithNode Sub) (S0, Some (Zy :* S0))
-                                            (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0))
-                                            (RPr ("value", TNat) R0)
-    wire (powSrc, TNat, lhs)
-    wire (oneSrc, TNat, rhs)
-    pure src
-
 vectorise :: forall m. Modey m -> (Src, Val Z) -> Checking (Src, CTy m Z)
 vectorise my (src, ty) = do
   (layers, cty) <- vecLayers my ty
@@ -493,7 +451,242 @@ runArith (NumValue upl grol) Pow (NumValue upr gror)
  = pure $ NumValue (upl ^ upr) (StrictMonoFun (StrictMono (l * upr) (Full (StrictMono (k + k') mono))))
 runArith _ _ _ = Nothing
 
+buildArithOp :: ArithOp -> Checking ((Tgt, Tgt), Src)
+buildArithOp op = do
+  (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next (show op) (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0)
+  pure ((lhs, rhs), out)
+
 buildConst :: SimpleTerm -> Val Z -> Checking Src
 buildConst tm ty = do
   (_, _, [(out,_)], _) <- next "buildConst" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0)
   pure out
+
+buildNum :: Integer -> Checking Src
+buildNum n = buildConst (Num (fromIntegral n)) TNat
+
+buildAdd :: Integer -> Checking (Tgt, Src)
+buildAdd n = do
+  nDangling <- buildNum n
+  ((lhs,rhs),out) <- buildArithOp Add
+  req $ Wire (end nDangling, TNat, end lhs)
+  defineSrc out (VNum (nPlus n (nVar (VPar (toEnd rhs)))))
+  pure (rhs, out)
+
+buildSub :: Integer -> Checking (Tgt, Src)
+buildSub n = do
+  nDangling <- buildNum n
+  ((lhs,rhs),out) <- buildArithOp Sub
+  req $ Wire (end nDangling, TNat, end rhs)
+  defineTgt lhs (VNum (nPlus n (nVar (VPar (toEnd out)))))
+  pure (lhs, out)
+
+buildDoub :: Checking (Tgt, Src)
+buildDoub = do
+  nDangling <- buildNum 2
+  ((lhs,rhs),out) <- buildArithOp Mul
+  req $ Wire (end nDangling, TNat, end lhs)
+  defineSrc out (VNum (n2PowTimes 1 (nVar (VPar (toEnd rhs)))))
+  pure (rhs, out)
+
+buildHalve :: Checking (Tgt, Src)
+buildHalve = do
+  nDangling <- buildNum 2
+  ((lhs,rhs),out) <- buildArithOp Div
+  req $ Wire (end nDangling, TNat, end rhs)
+  defineTgt lhs (VNum (n2PowTimes 1 (nVar (VPar (toEnd out)))))
+  pure (lhs, out)
+
+replaceHope :: InPort -> InPort -> Checking ()
+replaceHope old new = do
+  hs <- req AskHopes
+  case M.lookup old hs of
+    Nothing -> pure ()
+    Just hd -> do
+      req (RemoveHope old)
+      req (ANewHope new (HopeData Nothing (hopeDynamic hd)))
+
+-- Return an End with the same polarity whose value is half that of the input End
+makeHalf :: End -> Checking End
+makeHalf (InEnd e) = do
+  (doubIn, doubOut) <- buildDoub
+  req (Wire (end doubOut, TNat, e))
+  defineTgt (NamedPort e "") (VNum (nVar (VPar (toEnd doubOut))))
+  replaceHope e (end doubIn)
+  pure (InEnd (end doubIn))
+makeHalf (ExEnd e) = do
+  (halveIn, halveOut) <- buildHalve
+  req (Wire (e, TNat, end halveIn))
+  defineSrc (NamedPort e "") (VNum (nVar (VPar (toEnd halveIn))))
+  pure (toEnd halveOut)
+
+makePred :: End -> Checking End
+makePred (InEnd e) = do
+  (succIn, succOut) <- buildAdd 1
+  req (Wire (end succOut, TNat, e))
+  defineTgt (NamedPort e "") (VNum (nVar (VPar (toEnd succOut))))
+  replaceHope e (end succIn)
+  pure (toEnd succIn)
+makePred (ExEnd e) = do
+  (predIn, predOut) <- buildSub 1
+  req (Wire (e, TNat, end predIn))
+  defineSrc (NamedPort e "") (VNum (nVar (VPar (toEnd predIn))))
+  pure (toEnd predOut)
+
+-- Generate wiring to produce a dynamic instance of the numval argument
+-- N.B. In these functions, we wire using Req, rather than the `wire` function
+-- because we don't want it to do any extra evaluation.
+buildNatVal :: NumVal (VVar Z) -> Checking Src
+buildNatVal nv@(NumValue n gro) = case n of
+  0 -> buildGro gro
+  n -> do
+    (inn, out) <- buildAdd n
+    src <- buildGro gro
+    req $ Wire (end src, TNat, end inn)
+    defineTgt inn (VNum (nVar (VPar (toEnd src))))
+    pure out
+ where
+  buildGro :: Fun00 (VVar Z) -> Checking Src
+  buildGro Constant0 = buildNum 0
+  buildGro (StrictMonoFun sm) = buildSM sm
+
+  buildSM :: StrictMono (VVar Z) -> Checking Src
+  buildSM (StrictMono k mono) = do
+    factor <- buildNum $ 2 ^ k
+    -- Multiply mono by 2^k; note we could avoid this if k==0
+    ((lhs,rhs),out) <- buildArithOp Mul
+    monoDangling <- buildMono mono
+    req $ Wire (end factor, TNat, end lhs)
+    req $ Wire (end monoDangling, TNat, end rhs)
+    defineSrc out (VNum (n2PowTimes k (nVar (VPar (toEnd monoDangling)))))
+    pure out
+
+  buildMono :: Monotone (VVar Z) -> Checking Src
+  buildMono (Linear (VPar (ExEnd e))) = pure $ NamedPort e "numval"
+  buildMono (Full sm) = do
+    -- Calculate 2^n as `outPlus1`
+    two <- buildNum 2
+    dangling <- buildSM sm
+    ((lhs,rhs),outPlus1) <- buildArithOp Pow
+    req $ Wire (end two, TNat, end lhs)
+    req $ Wire (end dangling, TNat, end rhs)
+    -- Then subtract 1
+    one <- buildNum 1
+    ((lhs,rhs),out) <- buildArithOp Sub
+    req $ Wire (end outPlus1, TNat, end lhs)
+    req $ Wire (end one, TNat, end rhs)
+    defineSrc out (VNum (nFull (nVar (VPar (toEnd dangling)))))
+    pure out
+  buildMono _ = err . InternalError $ "Trying to build a non-closed nat value: " ++ show nv
+
+invertNatVal :: NumVal (VVar Z) -> Checking Tgt
+invertNatVal (NumValue up gro) = case up of
+  0 -> invertGro gro
+  _ -> do
+    ((lhs,rhs),out) <- buildArithOp Sub
+    upSrc <- buildNum up
+    req $ Wire (end upSrc, TNat, end rhs)
+    tgt <- invertGro gro
+    req $ Wire (end out, TNat, end tgt)
+    defineTgt tgt (VNum (nVar (VPar (toEnd out))))
+    defineTgt lhs (VNum (nPlus up (nVar (VPar (toEnd tgt)))))
+    pure lhs
+ where
+  invertGro Constant0 = error "Invariant violated: the numval arg to invertNatVal should contain a variable"
+  invertGro (StrictMonoFun sm) = invertSM sm
+
+  invertSM (StrictMono k mono) = case k of
+    0 -> invertMono mono
+    _ -> do
+      divisor <- buildNum (2 ^ k)
+      ((lhs,rhs),out) <- buildArithOp Div
+      tgt <- invertMono mono
+      req $ Wire (end out, TNat, end tgt)
+      req $ Wire (end divisor, TNat, end rhs)
+      defineTgt tgt (VNum (nVar (VPar (toEnd out))))
+      defineTgt lhs (VNum (n2PowTimes k (nVar (VPar (toEnd tgt)))))
+      pure lhs
+
+  invertMono (Linear (VPar (InEnd e))) = pure (NamedPort e "numval")
+  invertMono (Full sm) = do
+    (_, [(llufTgt,_)], [(llufSrc,_)], _) <- next "luff" (Prim ("BRAT","lluf")) (S0, Some (Zy :* S0)) (REx ("n", Nat) R0) (REx ("n", Nat) R0)
+    tgt <- invertSM sm
+    req $ Wire (end llufSrc, TNat, end tgt)
+    defineTgt tgt (VNum (nVar (VPar (toEnd llufSrc))))
+    defineTgt llufTgt (VNum (nFull (nVar (VPar (toEnd tgt)))))
+    pure llufTgt
+
+-- This will update the `hopes`, potentially invalidating things that have
+-- been eval'd.
+-- The Sem is closed, for now.
+solveHopeVal :: TypeKind -> InPort -> Val Z -> Checking ()
+solveHopeVal k hope v = case doesntOccur (InEnd hope) v of
+  Right () -> do
+    defineEnd (InEnd hope) v
+    dangling <- case (k, v) of
+      (Nat, VNum v) -> buildNatVal v
+      (Nat, _) -> err $ InternalError "Head of Nat wasn't a VNum"
+      _ -> buildConst Unit TUnit
+    req (Wire (end dangling, kindType k, hope))
+    req (RemoveHope hope)
+  Left msg -> case v of
+    VApp (VPar (InEnd end)) B0 | hope == end -> pure ()
+    -- TODO: Not all occurrences are toxic. The end could be in an argument
+    -- to a hoping variable which isn't used.
+    -- E.g. h1 = h2 h1 - this is valid if h2 is the identity, or ignores h1.
+    _ -> err msg
+
+solveHopeSem :: TypeKind -> InPort -> Sem -> Checking ()
+solveHopeSem k hope = quote Zy >=> solveHopeVal k hope
+
+-- Convert a pattern into a value for the purposes of solving it with unification
+-- for pattern matching. This is used for checking type constructors - we're only
+-- dealing in static information.
+valPat2Val :: TypeKind
+           -> ValPat
+           -> Checking (Bwd (Val Z) -- Values of the pattern vars
+                       ,Val Z  -- The value of the whole pattern
+                       )
+valPat2Val k VPVar = do
+  (_, [(idTgt, _)], [_], _) <- anext "pat2val" Id (S0, Some (Zy :* S0)) (REx ("", k) R0) (REx ("", k) R0)
+  let val = VApp (VPar (toEnd idTgt)) B0
+  req (ANewHope (end idTgt) (HopeData Nothing False))
+  pure (B0 :< val, val)
+valPat2Val (TypeFor m _) (VPCon con args) = do
+  ks <- fmap snd <$> tlup (m, con)
+  (stk, args) <- valPats2Val ks args
+  let val = VCon con args
+  pure (stk, val)
+valPat2Val Nat (VPNum n) = numPat2Val n >>= \(stk, nv) -> pure (stk, VNum nv)
+ where
+  numPat2Val :: NumPat -> Checking (Bwd (Val Z), NumVal (VVar Z))
+  numPat2Val NP0 = pure (B0, nZero)
+  numPat2Val (NP1Plus np) = second (nPlus 1) <$> numPat2Val np
+  numPat2Val (NP2Times np) = second (n2PowTimes 1) <$> numPat2Val np
+  numPat2Val NPVar = do
+    (_, [(idTgt, _)], [_], _) <- anext "numpat2val" Id (S0, Some (Zy :* S0)) (REx ("", Nat) R0) (REx ("", Nat) R0)
+    req (ANewHope (end idTgt) (HopeData Nothing False))
+    let var = endVal Nat (toEnd idTgt)
+    pure (B0 :< var, nVar (VPar (toEnd idTgt)))
+
+valPats2Val :: [TypeKind]
+            -> [ValPat]
+            -> Checking (Bwd (Val Z) -- Values of the pattern vars
+                        ,[Val Z]  -- The value of the whole pattern
+                        )
+valPats2Val (k:ks) (v:vs) = do
+  (stk, v) <- valPat2Val k v
+  (stk', vs) <- valPats2Val ks vs
+  pure (stk <+ stk', v:vs)
+valPats2Val [] [] = pure (B0, [])
+valPats2Val _ _ = err $ InternalError "Type args didn't match expected - kindCheck should've sorted it"
+
+{-
+traceChecking :: (Show a, Show b) => String -> (a -> Checking b) -> (a -> Checking b)
+traceChecking lbl m a = do
+  traceM ("Enter " ++ lbl ++ ": " ++ show a)
+  b <- m a
+  traceM ("Exit  " ++ lbl ++ ": " ++ show b)
+  pure b
+-}
+
+traceChecking = const id
\ No newline at end of file
diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs
index baecc9e6..d049e078 100644
--- a/brat/Brat/Checker/Monad.hs
+++ b/brat/Brat/Checker/Monad.hs
@@ -50,7 +50,12 @@ data CtxEnv = CtxEnv
   , locals :: VEnv
   }
 
-type Hopes = M.Map InPort FC
+data HopeData = HopeData
+  { hopeFC :: Maybe FC
+  , hopeDynamic :: Bool
+  } deriving (Eq, Ord, Show)
+
+type Hopes = M.Map InPort HopeData
 
 data Context = Ctx { globalVEnv :: VEnv
                    , store :: Store
@@ -92,7 +97,7 @@ data CheckingSig ty where
   AskVEnv :: CheckingSig CtxEnv
   Declare :: End -> Modey m -> BinderType m -> CheckingSig ()
   Define  :: End -> Val Z -> CheckingSig ()
-  ANewHope :: InPort -> FC -> CheckingSig ()
+  ANewHope :: InPort -> HopeData -> CheckingSig ()
   AskHopes :: CheckingSig Hopes
   RemoveHope :: InPort -> CheckingSig ()
 
@@ -167,6 +172,9 @@ kclup :: QualName -- Value constructor
       -> Checking (CtorArgs Kernel)
 kclup vcon tycon = req AskFC >>= \fc -> req (KCLup fc vcon tycon)
 
+-- TODO: Future proof this by taking a TypeKind argument instead of a mode.
+-- Currently we have kinds `Nat` for `TypeFor m`, where we don't lookup `Nat`
+-- with tlup, but this will change!
 tlup :: (Mode, QualName) -> Checking [(PortName, TypeKind)]
 tlup (m, c) = req (TLup (m, c)) >>= \case
   Nothing -> req (TLup (otherMode, c)) >>= \case
@@ -273,7 +281,7 @@ handler (Req s k) ctx g
                 M.lookup tycon tbl
         handler (k args) ctx g
 
-      ANewHope e fc -> handler (k ()) (ctx { hopes = M.insert e fc (hopes ctx) }) g
+      ANewHope e hd -> handler (k ()) (ctx { hopes = M.insert e hd (hopes ctx) }) g
 
       AskHopes -> handler (k (hopes ctx)) ctx g
 
diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs
index d26361dd..5b70acca 100644
--- a/brat/Brat/Checker/SolveHoles.hs
+++ b/brat/Brat/Checker/SolveHoles.hs
@@ -1,16 +1,18 @@
 module Brat.Checker.SolveHoles (typeEq) where
 
-import Brat.Checker.Helpers (buildConst)
+import Brat.Checker.Helpers (solveHopeSem)
 import Brat.Checker.Monad
 import Brat.Checker.Types (kindForMode)
+import Brat.Checker.SolveNumbers
 import Brat.Error (ErrorMsg(..))
 import Brat.Eval
 import Brat.Syntax.Common
-import Brat.Syntax.Simple (SimpleTerm(..))
+-- import Brat.Syntax.Simple (SimpleTerm(..))
 import Brat.Syntax.Value
 import Control.Monad.Freer
 import Bwd
 import Hasochism
+-- import Brat.Syntax.Port (toEnd)
 
 import Control.Monad (when)
 import Data.Bifunctor (second)
@@ -44,10 +46,6 @@ typeEq' str stuff@(_ny :* _ks :* sems) k exp act = do
   act <- sem sems act
   typeEqEta str stuff hopes k exp act
 
-isNumVar :: Sem -> Maybe SVar
-isNumVar (SNum (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear v))))) = Just v
-isNumVar _ = Nothing
-
 -- Presumes that the hope set and the two `Sem`s are up to date.
 typeEqEta :: String -- String representation of the term for error reporting
           -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n
@@ -67,12 +65,15 @@ typeEqEta tm (lvy :* kz :* sems) hopes (TypeFor m ((_, k):ks)) exp act = do
 -- (We don't solve under binders for now, so we only consider Zy here)
 -- 1. "easy" flex cases
 typeEqEta _tm (Zy :* _ks :* _sems) hopes k (SApp (SPar (InEnd e)) B0) act
-  | M.member e hopes = solveHope k e act
+  | M.member e hopes = solveHopeSem k e act
 typeEqEta _tm (Zy :* _ks :* _sems) hopes k exp (SApp (SPar (InEnd e)) B0)
-  | M.member e hopes = solveHope k e exp
-typeEqEta _ (Zy :* _ :* _) hopes Nat exp act
+  | M.member e hopes = solveHopeSem k e exp
+typeEqEta _ (Zy :* _ :* _) _ {-hopes-} Nat (SNum exp) (SNum act) = do
+  unifyNum (quoteNum Zy exp) (quoteNum Zy act)
+  {-
   | Just (SPar (InEnd e)) <- isNumVar exp, M.member e hopes = solveHope Nat e act
   | Just (SPar (InEnd e)) <- isNumVar act, M.member e hopes = solveHope Nat e exp
+  -}
 -- 2. harder cases, neither is in the hope set, so we can't define it ourselves
 typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do
   exp <- quote ny exp
@@ -92,26 +93,6 @@ typeEqEta tm stuff@(ny :* _ks :* _sems) hopes k exp act = do
   getEnd (VNum n) = getNumVar n
   getEnd _ = Nothing
 
--- This will update the `hopes`, potentially invalidating things that have
--- been eval'd.
--- The Sem is closed, for now.
-solveHope :: TypeKind -> InPort -> Sem -> Checking ()
-solveHope k hope v = quote Zy v >>= \v -> case doesntOccur (InEnd hope) v of
-  Right () -> do
-    defineEnd (InEnd hope) v
-    dangling <- case (k, v) of
-      (Nat, VNum _v) -> err $ Unimplemented "Nat hope solving" []
-      (Nat, _) -> err $ InternalError "Head of Nat wasn't a VNum"
-      _ -> buildConst Unit TUnit
-    req (Wire (end dangling, kindType k, hope))
-    req (RemoveHope hope)
-  Left msg -> case v of
-    VApp (VPar (InEnd end)) B0 | hope == end -> pure ()
-    -- TODO: Not all occurrences are toxic. The end could be in an argument
-    -- to a hoping variable which isn't used.
-    -- E.g. h1 = h2 h1 - this is valid if h2 is the identity, or ignores h1.
-    _ -> err msg
-
 typeEqs :: String -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n -> [TypeKind] -> [Val n] -> [Val n] -> Checking ()
 typeEqs _ _ [] [] [] = pure ()
 typeEqs tm stuff (k:ks) (exp:exps) (act:acts) = typeEqs tm stuff ks exps acts <* typeEq' tm stuff k exp act
@@ -145,7 +126,7 @@ typeEqRigid tm (_ :* _ :* semz) Nat exp act = do
   act <- sem semz act
   if getNum exp == getNum act
   then pure ()
-  else err $ TypeMismatch tm (show exp) (show act)
+  else err $ TypeMismatch tm ("TYPEEQRIGID " ++ show exp) ("TODO " ++ show act)
 typeEqRigid tm stuff@(_ :* kz :* _) (TypeFor m []) (VApp f args) (VApp f' args') | f == f' =
   svKind f >>= \case
     TypeFor m' ks | m == m' -> typeEqs tm stuff (snd <$> ks) (args <>> []) (args' <>> [])
diff --git a/brat/Brat/Checker/SolveNumbers.hs b/brat/Brat/Checker/SolveNumbers.hs
new file mode 100644
index 00000000..b46f5e85
--- /dev/null
+++ b/brat/Brat/Checker/SolveNumbers.hs
@@ -0,0 +1,193 @@
+module Brat.Checker.SolveNumbers (unifyNum) where
+
+import Brat.Checker.Monad
+import Brat.Checker.Helpers
+import Brat.Syntax.Value
+import Brat.Syntax.Common
+import Brat.Syntax.Port
+import Brat.Error
+import Brat.Eval
+import Brat.Graph (NodeType(..))
+import Hasochism
+import Control.Monad.Freer
+
+-- import Debug.Trace
+import qualified Data.Map as M
+
+-- trail = trace
+
+-- This is currently lifted from SolvePatterns, which still imports it.
+-- It is also used in SolveHoles, where it does the right mathematics
+-- but the wrong wiring.
+
+-- Solve a Nat kinded metavariable. Unlike `instantiateMeta`, this function also
+-- makes the dynamic wiring for a metavariable. This only needs to happen for
+-- numbers because they have nontrivial runtime behaviour.
+--
+-- We assume that the caller has done the occurs check and rules out trivial equations.
+solveNumMeta :: End -> NumVal (VVar Z) -> Checking ()
+-- solveNumMeta e nv | trace ("solveNumMeta " ++ show e ++ " " ++ show nv) False = undefined
+solveNumMeta e nv = case (e, vars nv) of
+ -- Compute the thing that the rhs should be based on the src, and instantiate src to that
+ (ExEnd src,  [VPar (InEnd _tgt)]) -> do
+   -- Compute the value of the `tgt` variable from the known `src` value by inverting nv
+   tgtSrc <- invertNatVal nv
+   instantiateMeta (ExEnd src) (VNum (nVar (VPar (toEnd tgtSrc))))
+   wire (NamedPort src "", TNat, tgtSrc)
+
+ (ExEnd src, _) -> instantiateMeta (ExEnd src) (VNum nv)
+
+ -- Both targets, we need to create the thing that they both derive from
+ (InEnd bigTgt, [VPar (InEnd weeTgt)]) -> do
+   (_, [(idTgt, _)], [(idSrc, _)], _) <- anext "numval id" Id (S0, Some (Zy :* S0))
+                                         (REx ("n", Nat) R0) (REx ("n", Nat) R0)
+   defineSrc idSrc (VNum (nVar (VPar (toEnd idTgt))))
+   hopes <- req AskHopes
+   instantiateMeta (InEnd weeTgt) (VNum (nVar (VPar (toEnd idSrc))))
+   if M.member weeTgt hopes then req (RemoveHope weeTgt) else pure ()
+   wire (idSrc, TNat, NamedPort weeTgt "")
+   let nv' = fmap (const (VPar (toEnd idSrc))) nv -- weeTgt is the only thing to replace
+   bigSrc <- buildNatVal nv'
+   instantiateMeta (InEnd bigTgt) (VNum nv')
+   if M.member bigTgt hopes then req (RemoveHope bigTgt) else pure ()
+   wire (bigSrc, TNat, NamedPort bigTgt "")
+
+ -- RHS is constant or Src, wire it into tgt
+ (InEnd tgt,  _) -> do
+   src <- buildNatVal nv
+   instantiateMeta (InEnd tgt) (VNum nv)
+   hopes <- req AskHopes
+   if M.member tgt hopes then req (RemoveHope tgt) else pure ()
+   wire (src, TNat, NamedPort tgt "")
+ where
+  vars :: NumVal a -> [a]
+  vars = foldMap pure
+
+unifyNum :: NumVal (VVar Z) -> NumVal (VVar Z) -> Checking ()
+unifyNum nv0 nv1 = do
+  -- traceM $ ("unifyNum In\n  " ++ show nv0 ++ "\n  " ++ show nv1)
+  nv0 <- numEval S0 nv0
+  nv1 <- numEval S0 nv1
+  unifyNum' (quoteNum Zy nv0) (quoteNum Zy nv1)
+  -- nv0 <- numEval S0 (quoteNum Zy nv0)
+  -- nv1 <- numEval S0 (quoteNum Zy nv1)
+  -- traceM $ ("unifyNum Out\n  " ++ show (quoteNum Zy nv0) ++ "\n  " ++ show (quoteNum Zy nv1)) 
+
+-- Need to keep track of which way we're solving - which side is known/unknown
+-- Things which are dynamically unknown must be Tgts - information flows from Srcs
+-- ...But we don't need to do any wiring here, right?
+unifyNum' :: NumVal (VVar Z) -> NumVal (VVar Z) -> Checking ()
+-- unifyNum' a b | trace ("unifyNum'\n  " ++ show a ++ "\n  " ++ show b) False = undefined
+unifyNum' (NumValue lup lgro) (NumValue rup rgro)
+  | lup <= rup = lhsFun00 lgro (NumValue (rup - lup) rgro)
+  | otherwise  = lhsFun00 rgro (NumValue (lup - rup) lgro)
+ where
+  lhsFun00 :: Fun00 (VVar Z) -> NumVal (VVar Z) -> Checking ()
+  lhsFun00 Constant0 num = demand0 num
+  -- Both sides are variables
+  lhsFun00 (StrictMonoFun (StrictMono 0 (Linear v))) (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear v')))) = flexFlex v v'
+  -- There's just a variable on the right - move it to the left
+  lhsFun00 sm (NumValue 0 (StrictMonoFun smv@(StrictMono 0 (Linear _)))) = lhsStrictMono smv (NumValue 0 sm)
+  lhsFun00 (StrictMonoFun sm) num = lhsStrictMono sm num
+
+  flexFlex :: VVar Z -> VVar Z -> Checking ()
+  flexFlex v v' = case compare v v' of
+    GT -> flexFlex v' v
+    EQ -> pure ()
+    LT -> case (v, v') of
+      (VPar (ExEnd e), v@(VPar (ExEnd _))) -> defineSrc (NamedPort e "") (VNum (nVar v))
+      (VPar (InEnd e), v@(VPar (ExEnd dangling))) -> do
+        req (Wire (dangling, TNat, e))
+        defineTgt (NamedPort e "") (VNum (nVar v))
+        (M.member e <$> req AskHopes) >>= \case
+          True -> req (RemoveHope e)
+          False -> pure ()
+      (v@(VPar (InEnd e)), v'@(VPar (InEnd e'))) -> do
+        hs <- req AskHopes
+        case (M.lookup e hs, M.lookup e' hs) of
+          (Nothing, Just _) -> do
+            defineTgt (NamedPort e' "") (VNum (nVar v))
+            req (RemoveHope e')
+          (Just _, Nothing) -> do
+            defineTgt (NamedPort e "") (VNum (nVar v'))
+            req (RemoveHope e)
+          (Nothing, Nothing) -> error "Two non-hopes in unifyNum"
+          (Just hd, Just hd') -> if hopeDynamic hd
+                                 then do defineTgt (NamedPort e' "") (VNum (nVar v))
+                                         req (RemoveHope e')
+                                 else do defineTgt (NamedPort e "") (VNum (nVar v'))
+                                         req (RemoveHope e)
+
+  lhsStrictMono :: StrictMono (VVar Z) -> NumVal (VVar Z) -> Checking ()
+  lhsStrictMono (StrictMono 0 mono) num = lhsMono mono num
+  lhsStrictMono (StrictMono n mono) num = do
+    num <- traceChecking "lhsSM demandEven" demandEven num
+    lhsFun00 (StrictMonoFun (StrictMono (n - 1) mono)) num
+
+  lhsMono :: Monotone (VVar Z) -> NumVal (VVar Z) -> Checking ()
+  lhsMono (Linear (VPar e)) num = throwLeft (doesntOccur e (VNum num)) *>
+                                  solveNumMeta 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) = lhsFun00 gro (NumValue 0 (StrictMonoFun (StrictMono 0 m)))
+  lhsMono (Full sm) (NumValue up gro) = do
+    smPred <- traceChecking "lhsMono demandSucc" demandSucc sm
+    sm <- numEval S0 sm
+    -- traceM $ "succ now " ++ show (quoteNum Zy sm)
+    unifyNum (n2PowTimes 1 (nFull smPred)) (NumValue (up - 1) gro)
+
+  demand0 :: NumVal (VVar Z) -> Checking ()
+  demand0 (NumValue 0 Constant0) = pure ()
+  demand0 n@(NumValue 0 (StrictMonoFun (StrictMono _ mono))) = case mono of
+    Linear (VPar e) -> solveNumMeta e (nConstant 0)
+    Full sm -> demand0 (NumValue 0 (StrictMonoFun sm))
+    _ -> 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 :: StrictMono (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 (StrictMono k (Linear (VPar e))) = do
+    pred <- 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)
+  demandSucc x@(StrictMono k (Full nPlus1)) = do
+    n <- traceChecking "demandSucc" demandSucc nPlus1
+    -- foo <- numEval S0 x
+    -- traceM $ "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))
+  demandEven n@(NumValue up gro) = case up `divMod` 2 of
+    (up, 0) -> NumValue up <$> traceChecking "evenGro" evenGro gro
+    (up, 1) -> nPlus (up + 1) <$> traceChecking "oddGro" oddGro gro
+   where
+    evenGro :: Fun00 (VVar Z) -> Checking (Fun00 (VVar Z))
+    evenGro Constant0 = pure Constant0
+    evenGro (StrictMonoFun (StrictMono 0 mono)) = case mono of
+      Linear (VPar e) -> do
+        -- traceM $ "Calling makeHalf (" ++ show e ++ ")"
+        half <- traceChecking "makeHalf" makeHalf e
+        pure (StrictMonoFun (StrictMono 0 (Linear (VPar half))))
+      Full sm -> StrictMonoFun sm <$ demand0 (NumValue 0 (StrictMonoFun sm))
+    evenGro (StrictMonoFun (StrictMono n mono)) = pure (StrictMonoFun (StrictMono (n - 1) mono))
+
+    -- Check a numval is odd, and return its rounded down half
+    oddGro :: Fun00 (VVar Z) -> Checking (NumVal (VVar Z))
+    oddGro (StrictMonoFun (StrictMono 0 mono)) = case mono of
+      Linear (VPar e) -> do
+        pred <- traceChecking "makePred" makePred e
+        half <- traceChecking "makeHalf" makeHalf pred
+        pure (nVar (VPar half))
+      -- full(n + 1) = 1 + 2 * full(n)
+      -- hence, full(n) is the rounded down half
+      Full sm -> nFull <$> traceChecking "demandSucc" demandSucc sm
+    oddGro _ = err . UnificationError $ "Can't force " ++ show n ++ " to be even"
diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs
index 7339157d..af68231e 100644
--- a/brat/Brat/Checker/SolvePatterns.hs
+++ b/brat/Brat/Checker/SolvePatterns.hs
@@ -3,6 +3,7 @@ module Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve)
 import Brat.Checker.Monad
 import Brat.Checker.Helpers
 import Brat.Checker.Types (EndType(..))
+import Brat.Checker.SolveNumbers
 import Brat.Constructors
 import Brat.Constructors.Patterns
 import Brat.Error
@@ -16,13 +17,13 @@ import Brat.QualName
 import Bwd
 import Control.Monad.Freer
 import Hasochism
+import Brat.Syntax.Port (toEnd)
 
 import Control.Monad (unless)
 import Data.Bifunctor (first)
 import qualified Data.Map as M
 import Data.Maybe (fromJust)
 import Data.Type.Equality ((:~:)(..), testEquality)
-import Brat.Syntax.Port (toEnd)
 
 -- Refine clauses from function definitions (and potentially future case statements)
 -- by processing each one in sequence. This will involve repeating tests for various
@@ -193,123 +194,6 @@ unify l k r = do
 
 -- Solve a metavariable statically - don't do anything dynamic
 -- Once a metavariable is solved, we expect to not see it again in a normal form.
-instantiateMeta :: End -> Val Z -> Checking ()
-instantiateMeta e val = do
-  throwLeft (doesntOccur e val)
-  defineEnd e val
-
-
--- Need to keep track of which way we're solving - which side is known/unknown
--- Things which are dynamically unknown must be Tgts - information flows from Srcs
--- ...But we don't need to do any wiring here, right?
-unifyNum :: NumVal (VVar Z) -> NumVal (VVar Z) -> Checking ()
-unifyNum (NumValue lup lgro) (NumValue rup rgro)
-  | lup <= rup = lhsFun00 lgro (NumValue (rup - lup) rgro)
-  | otherwise  = lhsFun00 rgro (NumValue (lup - rup) lgro)
- where
-  lhsFun00 :: Fun00 (VVar Z) -> NumVal (VVar Z) -> Checking ()
-  lhsFun00 Constant0 num = demand0 num
-  lhsFun00 (StrictMonoFun sm) num = lhsStrictMono sm num
-
-  lhsStrictMono :: StrictMono (VVar Z) -> NumVal (VVar Z) -> Checking ()
-  lhsStrictMono (StrictMono 0 mono) num = lhsMono mono num
-  lhsStrictMono (StrictMono n mono) num = do
-    num <- demandEven num
-    lhsStrictMono (StrictMono (n - 1) mono) num
-
-  lhsMono :: Monotone (VVar Z) -> NumVal (VVar Z) -> Checking ()
-  lhsMono (Linear v) num = case v of
-    VPar e -> instantiateMeta e (VNum num)
-    _ -> case num of -- our only hope is to instantiate the RHS
-      NumValue 0 (StrictMonoFun (StrictMono 0 (Linear (VPar (ExEnd e))))) -> instantiateMeta (toEnd e) (VNum (nVar v))
-      _ -> err . UnificationError $ "Couldn't instantiate variable " ++ show v
-  lhsMono (Full sm) (NumValue 0 (StrictMonoFun (StrictMono 0 (Full sm'))))
-    = lhsStrictMono sm (NumValue 0 (StrictMonoFun sm'))
-  lhsMono m@(Full _) (NumValue 0 gro) = lhsFun00 gro (NumValue 0 (StrictMonoFun (StrictMono 0 m)))
-  lhsMono (Full sm) (NumValue up gro) = do
-    smPred <- demandSucc sm
-    unifyNum (n2PowTimes 1 (nFull smPred)) (NumValue (up - 1) gro)
-
-  demand0 :: NumVal (VVar Z) -> Checking ()
-  demand0 (NumValue 0 Constant0) = pure ()
-  demand0 n@(NumValue 0 (StrictMonoFun (StrictMono _ mono))) = case mono of
-    Linear (VPar e) -> instantiateMeta e (VNum (nConstant 0))
-    Full sm -> demand0 (NumValue 0 (StrictMonoFun sm))
-    _ -> 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 :: StrictMono (VVar Z) -> Checking (NumVal (VVar Z))
-  --   2^k * x
-  -- = 2^k * (y + 1)
-  -- = 2^k + 2^k * y
-  demandSucc (StrictMono k (Linear (VPar (ExEnd out)))) = do
-    y <- mkPred out
-    pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k y
-  --   2^k * full(n + 1)
-  -- = 2^k * (1 + 2 * full(n))
-  -- = 2^k + 2^(k + 1) * full(n)
-  demandSucc (StrictMono k (Full nPlus1)) = do
-    n <- demandSucc nPlus1
-    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))
-  demandEven n@(NumValue up gro) = case up `divMod` 2 of
-    (up, 0) -> NumValue up <$> evenGro gro
-    (up, 1) -> nPlus (up + 1) <$> oddGro gro
-   where
-    evenGro :: Fun00 (VVar Z) -> Checking (Fun00 (VVar Z))
-    evenGro Constant0 = pure Constant0
-    evenGro (StrictMonoFun (StrictMono 0 mono)) = case mono of
-      Linear (VPar (ExEnd out)) -> do
-        half <- mkHalf out
-        pure (StrictMonoFun (StrictMono 0 (Linear (VPar (toEnd half)))))
-      Linear _ -> err . UnificationError $ "Can't force " ++ show n ++ " to be even"
-      Full sm -> StrictMonoFun sm <$ demand0 (NumValue 0 (StrictMonoFun sm))
-    evenGro (StrictMonoFun (StrictMono n mono)) = pure (StrictMonoFun (StrictMono (n - 1) mono))
-
-    -- Check a numval is odd, and return its rounded down half
-    oddGro :: Fun00 (VVar Z) -> Checking (NumVal (VVar Z))
-    oddGro (StrictMonoFun (StrictMono 0 mono)) = case mono of
-      Linear (VPar (ExEnd out)) -> mkPred out >>= demandEven
-      Linear _ -> err . UnificationError $ "Can't force " ++ show n ++ " to be even"
-      -- full(n + 1) = 1 + 2 * full(n)
-      -- hence, full(n) is the rounded down half
-      Full sm -> nFull <$> demandSucc sm
-    oddGro _ = err . UnificationError $ "Can't force " ++ show n ++ " to be even"
-
-  -- Add dynamic logic to compute half of a variable.
-  mkHalf :: OutPort -> Checking Src
-  mkHalf out = do
-    (_, [], [(const2,_)], _) <- next "const2" (Const (Num 2)) (S0, Some (Zy :* S0))
-                                R0
-                                (RPr ("value", TNat) R0)
-    (_, [(lhs,_),(rhs,_)], [(half,_)], _) <- next "div2" (ArithNode Div) (S0, Some (Zy :* S0))
-                                             (RPr ("left", TNat) (RPr ("right", TNat) R0))
-                                             (RPr ("out", TNat) R0)
-    wire (NamedPort out "numerator", TNat, lhs)
-    wire (const2, TNat, rhs)
-    req $ Define (toEnd out) (VNum (n2PowTimes 1 (nVar (VPar (toEnd half)))))
-    pure half
-
-
-  -- Add dynamic logic to compute the predecessor of a variable, and return that
-  -- predecessor.
-  -- The variable must be a non-zero nat!!
-  mkPred :: OutPort -> Checking (NumVal (VVar Z))
-  mkPred out = do
-    (_, [], [(const1,_)], _) <- next "const1" (Const (Num 1)) (S0, Some (Zy :* S0))
-                                R0
-                                (RPr ("value", TNat) R0)
-    (_, [(lhs,_),(rhs,_)], [(pred,_)], _) <- next "minus1" (ArithNode Sub) (S0, Some (Zy :* S0))
-                                             (RPr ("left", TNat) (RPr ("right", TNat) R0))
-                                             (RPr ("out", TNat) R0)
-    wire (NamedPort out "", TNat, lhs)
-    wire (const1, TNat, rhs)
-    req $ Define (ExEnd out) (VNum (nPlus 1 (nVar (VPar (toEnd pred)))))
-    pure (nVar (VPar (toEnd pred)))
 
 -- The variable must be a non-zero nat!!
 patVal :: ValPat -> [End] -> (Val Z, [End])
diff --git a/brat/Brat/Eval.hs b/brat/Brat/Eval.hs
index 3625c80b..e64041bb 100644
--- a/brat/Brat/Eval.hs
+++ b/brat/Brat/Eval.hs
@@ -2,6 +2,7 @@
 
 module Brat.Eval (EvMode(..)
                  ,ValPat(..)
+                 ,NumEval(..)
                  ,NumPat(..)
                  ,apply
                  ,applySem
@@ -17,7 +18,9 @@ module Brat.Eval (EvMode(..)
                  ,kindType
                  ,numVal
                  ,quote
+		 ,quoteNum
                  ,getNumVar
+		 ,instantiateMeta
                  ) where
 
 import Brat.Checker.Monad
@@ -117,7 +120,7 @@ semLvl lvy = SApp (SLvl $ ny2int lvy) B0
 
 -- note that typeEq is a kind of quote but that also does eta-expansion
 quote :: Ny lv -> Sem -> Checking (Val lv)
-quote lvy (SNum num) = pure $ VNum (fmap (quoteVar lvy) num)
+quote lvy (SNum num) = pure $ VNum (quoteNum lvy num)
 quote lvy (SCon nm args) = VCon nm <$> traverse (quote lvy) args
 quote lvy (SLam stk body) = do
   body <- sem (stk :<< semLvl lvy) body
@@ -130,6 +133,9 @@ quoteCTy lvy my ga (ins :->> outs) = quoteRo my ga ins lvy >>= \case
   (ga', Some (ins' :* lvy')) -> quoteRo my ga' outs lvy' >>= \case
     (_, Some (outs' :* _)) -> pure (ins' :->> outs')
 
+quoteNum ::  Ny lv -> NumVal SVar -> NumVal (VVar lv)
+quoteNum lvy num = fmap (quoteVar lvy) num
+
 -- first number is next Lvl to use in Value
 --         require every Lvl in Sem is < n (converted by n - 1 - lvl), else must fail at runtime
 quoteVar :: Ny n -> SVar -> VVar n
@@ -316,6 +322,11 @@ 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
 
+instantiateMeta :: End -> Val Z -> Checking ()
+instantiateMeta e val = do
+  throwLeft (doesntOccur e val)
+  defineEnd e val
+
 collision :: End -> End -> Either ErrorMsg ()
 collision e v | e == v = Left . UnificationError $
                          show e ++ " is cyclic"
diff --git a/brat/Brat/Syntax/Common.hs b/brat/Brat/Syntax/Common.hs
index f90dbed6..c13195a9 100644
--- a/brat/Brat/Syntax/Common.hs
+++ b/brat/Brat/Syntax/Common.hs
@@ -34,6 +34,7 @@ module Brat.Syntax.Common (PortName,
                            KINDY(..),
                            DIRY(..),
                            modily,
+                           deModey,
                            ArithOp(..),
                            pattern Dollar,
                            pattern Star,
@@ -84,6 +85,10 @@ modily :: Modey m -> (MODEY m => t) -> t
 modily Braty t = t
 modily Kerny t = t
 
+deModey :: Modey m -> Mode
+deModey Braty = Brat
+deModey Kerny = Kernel
+
 instance TestEquality Modey where
   testEquality Braty Braty = Just Refl
   testEquality Kerny Kerny = Just Refl
diff --git a/brat/Brat/Syntax/Port.hs b/brat/Brat/Syntax/Port.hs
index 4b118576..5ce7c8d3 100644
--- a/brat/Brat/Syntax/Port.hs
+++ b/brat/Brat/Syntax/Port.hs
@@ -41,6 +41,7 @@ instance ToEnd InPort where
 instance ToEnd OutPort where
   toEnd = ExEnd
 
+-- N.B. Ord is derived with In < Ex
 data End = InEnd InPort | ExEnd OutPort
  deriving (Eq, Ord)
 
diff --git a/brat/Brat/Syntax/Value.hs b/brat/Brat/Syntax/Value.hs
index 4bc71fcd..c12aa149 100644
--- a/brat/Brat/Syntax/Value.hs
+++ b/brat/Brat/Syntax/Value.hs
@@ -53,6 +53,7 @@ data Inx :: N -> Type where
   VS :: Inx n -> Inx (S n)
 
 deriving instance Eq (Inx n)
+deriving instance Ord (Inx n)
 
 instance Show (Inx n) where
   show = show . toNat
@@ -143,6 +144,7 @@ data VVar :: N -> Type where
   VPar :: End -> VVar n  -- Has to be declared in the Store (for equality testing)
   VInx :: Inx n -> VVar n
 
+deriving instance Ord (VVar n)
 deriving instance Show (VVar n)
 
 instance Eq (VVar n) where
@@ -347,7 +349,7 @@ instance NumFun Monotone where
   calculate (Linear n) = n
   calculate (Full sm) = full (calculate sm)
    where
-    full n = 2 ^ n - 1
+    full n = (2 ^ n) - 1
 
   numValue = numValue . StrictMono 0
 
diff --git a/brat/brat.cabal b/brat/brat.cabal
index 3873bcf1..3999cf9b 100644
--- a/brat/brat.cabal
+++ b/brat/brat.cabal
@@ -44,11 +44,11 @@ common warning-flags
     -Wno-unused-do-bind
     -Wno-missing-signatures
     -Wno-noncanonical-monoid-instances
-    -Werror=unused-imports
-    -Werror=unused-matches
+--    -Werror=unused-imports
+--    -Werror=unused-matches
     -Werror=missing-methods
-    -Werror=unused-top-binds
-    -Werror=unused-local-binds
+--    -Werror=unused-top-binds
+--    -Werror=unused-local-binds
     -Werror=redundant-constraints
     -Werror=orphans
     -Werror=overlapping-patterns
@@ -69,6 +69,7 @@ library
                        Brat.Checker.Helpers.Nodes,
                        Brat.Checker.Monad,
                        Brat.Checker.SolveHoles,
+		       Brat.Checker.SolveNumbers,
                        Brat.Checker.SolvePatterns,
                        Brat.Checker.Types,
                        Brat.Compile.Hugr,
diff --git a/brat/examples/eatsfull.brat b/brat/examples/eatsfull.brat
new file mode 100644
index 00000000..bce0d05a
--- /dev/null
+++ b/brat/examples/eatsfull.brat
@@ -0,0 +1,4 @@
+eatsfull(n :: #, xs :: Vec(Bool, full(n))) -> Nat
+eatsfull(n, _) = n
+mkftwo :: Nat
+mkftwo = eatsfull(!, [false,false,false])
diff --git a/brat/examples/eatsfullbis.brat b/brat/examples/eatsfullbis.brat
new file mode 100644
index 00000000..2a94d1fc
--- /dev/null
+++ b/brat/examples/eatsfullbis.brat
@@ -0,0 +1,6 @@
+eatsfull(n :: #, xs :: Vec(Bool, full(n))) -> Nat
+eatsfull(n, _) = n
+falses :: Vec(Bool, 3)
+falses = [false, false, false]
+mkftwo :: Nat
+mkftwo = eatsfull(!, falses)
diff --git a/brat/examples/infer.brat b/brat/examples/infer.brat
index e10ee44e..62b0955b 100644
--- a/brat/examples/infer.brat
+++ b/brat/examples/infer.brat
@@ -2,7 +2,28 @@ map(X :: *, Y :: *, { X -> Y }, List(X)) -> List(Y)
 map(_, _, _, []) = []
 map(_, _, f, x ,- xs) = f(x) ,- map(!, !, f, xs)
 
--- TODO: Make BRAT solve for the # kinded args
 mapVec(X :: *, Y :: *, { X -> Y }, n :: #, Vec(X, n)) -> Vec(Y, n)
 mapVec(_, _, _, _, []) = []
-mapVec(_, _, f, succ(n), x ,- xs) = f(x) ,- mapVec(!, !, f, n, xs)
+mapVec(_, _, f, _, x ,- xs) = f(x) ,- mapVec(!, !, f, !, xs)
+
+isfull(n :: #) -> Bool
+isfull(succ(doub(n))) = isfull(n)
+isfull(0) = true
+isfull(_) = false
+
+hasfulllen(n :: #, Vec(Bool, n)) -> Bool
+hasfulllen(n, x ,- (xs =,= ys)) = hasfulllen(!, xs)
+hasfulllen(_, []) = true
+hasfulllen(_, _) = false
+
+eatsfull(n :: #, xs :: Vec(Bool, full(n))) -> Nat
+eatsfull(n, _) = n
+mkftwo :: Nat
+mkftwo = eatsfull(!, [false,false,false])
+
+eatsodd(n :: #, xs :: Vec(Bool, succ(doub(n)))) -> Nat
+eatsodd(n, _) = n
+mkotwo' :: Nat
+mkotwo' = eatsodd(2, [false,false,false,false,false])
+mkotwo :: Nat
+mkotwo = eatsodd(!, [false,false,false,false,false])
diff --git a/brat/examples/unified.brat b/brat/examples/unified.brat
index f04c167a..becc483e 100644
--- a/brat/examples/unified.brat
+++ b/brat/examples/unified.brat
@@ -28,3 +28,15 @@ swapFront(X :: *, n :: #, Vec(X, n)) -> Vec(X, n)
 swapFront(_, _, []) = []
 swapFront(_, _, [x]) = [x]
 swapFront(X, _, cons(x, cons(y, zs))) = cons(y, cons(x, zs))
+
+filled(X :: *, n :: #, Vec(X, full(n))) -> Vec(X, full(n))
+filled(_, _, xsl =, x ,= xsr) = xsl =, x ,= xsr
+
+fullId(X :: *, n :: #, Vec(X, full(n))) -> Vec(X, full(n))
+fullId(_, _, [] =,= []) = []
+fullId(_, _, [] =, x ,= []) = [x]
+fullId(_, succ(n), xl =, x ,= xr) = fullId(!, n, xl) =, x ,= fullId(!, n, xr)
+
+-- mapAndConquer(X :: *, Y :: *, n :: #, f :: { X -> Y }, Vec(X, succ(n))) -> Vec(Y, succ(n))
+-- mapAndConquer(_, _, doub(n), f, xsl =, x ,= xsr) = mapAndConquer(!, !, n, f, xsl) =, f(x) ,= mapAndConquer(!, !, n, f, xsr)
+-- mapAndConquer(_, _, succ(doub(n)), f, xsl =,= xsr) = mapAndConquer(!, !, n, f, xsl) =,= mapAndConquer(!, !, n, f, xsr)
diff --git a/brat/test/golden/error/badvec.brat.golden b/brat/test/golden/error/badvec.brat.golden
index 35e9fc33..f60758f4 100644
--- a/brat/test/golden/error/badvec.brat.golden
+++ b/brat/test/golden/error/badvec.brat.golden
@@ -2,9 +2,5 @@ Error in test/golden/error/badvec.brat on line 2:
 v3 = [1]
      ^^^
 
-  Expected vector of length 3
-from the type:  Vec(Int, 3)
-but got vector: [1]
-of length 1
-
+  Unification error: Couldn't force 2 to be 0
 
diff --git a/brat/test/golden/error/badvec2.brat.golden b/brat/test/golden/error/badvec2.brat.golden
index 2029db69..6d897a48 100644
--- a/brat/test/golden/error/badvec2.brat.golden
+++ b/brat/test/golden/error/badvec2.brat.golden
@@ -2,9 +2,5 @@ Error in test/golden/error/badvec2.brat on line 2:
 v3 = nil
      ^^^
 
-  Expected vector of length 3
-from the type:  Vec(Int, 3)
-but got vector: []
-of length 0
-
+  Unification error: Couldn't force 3 to be 0
 
diff --git a/brat/test/golden/error/badvec3.brat.golden b/brat/test/golden/error/badvec3.brat.golden
index 76e928b2..a17674df 100644
--- a/brat/test/golden/error/badvec3.brat.golden
+++ b/brat/test/golden/error/badvec3.brat.golden
@@ -2,9 +2,5 @@ Error in test/golden/error/badvec3.brat on line 2:
 v3 = cons(1, nil)
      ^^^^^^^^^^^^
 
-  Expected vector of length 0
-from the type:  Vec(Int, 0)
-but got vector: [1]
-of length (> 0)
-
+  Unification error: Couldn't force 1 + VPar In checking_check_defs_1_v3_numpat2val_1 0 to be 0
 
diff --git a/brat/test/golden/error/badvec4.brat.golden b/brat/test/golden/error/badvec4.brat.golden
index 7fe59dfd..13b202ae 100644
--- a/brat/test/golden/error/badvec4.brat.golden
+++ b/brat/test/golden/error/badvec4.brat.golden
@@ -2,9 +2,5 @@ Error in test/golden/error/badvec4.brat on line 2:
 v3 = [1,2]
      ^^^^^
 
-  Expected vector of length 3
-from the type:  Vec(Int, 3)
-but got vector: [1,2]
-of length 2
-
+  Unification error: Couldn't force 1 to be 0
 
diff --git a/brat/test/golden/error/kbadvec.brat.golden b/brat/test/golden/error/kbadvec.brat.golden
index 07a9e553..73424591 100644
--- a/brat/test/golden/error/kbadvec.brat.golden
+++ b/brat/test/golden/error/kbadvec.brat.golden
@@ -2,9 +2,5 @@ Error in test/golden/error/kbadvec.brat on line 2:
 triple = { b => [b] }
                 ^^^
 
-  Expected vector of length 3
-from the type:  Vec(Bit, 3)
-but got vector: [「b」]
-of length 1
-
+  Unification error: Couldn't force 2 to be 0
 
diff --git a/brat/test/golden/error/kbadvec2.brat.golden b/brat/test/golden/error/kbadvec2.brat.golden
index c70190e9..e245c2cb 100644
--- a/brat/test/golden/error/kbadvec2.brat.golden
+++ b/brat/test/golden/error/kbadvec2.brat.golden
@@ -2,9 +2,5 @@ Error in test/golden/error/kbadvec2.brat on line 2:
 triple = { b => nil }
                 ^^^
 
-  Expected vector of length 3
-from the type:  Vec(Bit, 3)
-but got vector: []
-of length 0
-
+  Unification error: Couldn't force 3 to be 0
 
diff --git a/brat/test/golden/error/kbadvec3.brat.golden b/brat/test/golden/error/kbadvec3.brat.golden
index 97be8bec..d8718593 100644
--- a/brat/test/golden/error/kbadvec3.brat.golden
+++ b/brat/test/golden/error/kbadvec3.brat.golden
@@ -2,9 +2,5 @@ Error in test/golden/error/kbadvec3.brat on line 2:
 constNil = { b => cons(1, nil) }
                   ^^^^^^^^^^^^
 
-  Expected vector of length 0
-from the type:  Vec(Bit, 0)
-but got vector: [1]
-of length (> 0)
-
+  Unification error: Couldn't force 1 + VPar In checking_check_defs_1_constNil_thunk_2_numpat2val_3 0 to be 0
 
diff --git a/brat/test/golden/error/vec_length.brat.golden b/brat/test/golden/error/vec_length.brat.golden
index 6fda6b03..b8f5be01 100644
--- a/brat/test/golden/error/vec_length.brat.golden
+++ b/brat/test/golden/error/vec_length.brat.golden
@@ -2,8 +2,5 @@ Error in test/golden/error/vec_length.brat on line 2:
 f(_, _, xs) = xs
               ^^
 
-  Type mismatch when checking xs
-Expected: (a1 :: Vec(VApp VPar Ex checking_check_defs_1_f_f.box_2_lambda_fake_source 0 B0, VPar Ex checking_check_defs_1_f_f.box_2_lambda_fake_source 1))
-But got:  (xs :: Vec(VApp VPar Ex checking_check_defs_1_f_f.box_2_lambda_fake_source 0 B0, 1 + VPar Ex checking_check_defs_1_f_f.box_2_lambda_fake_source 1))
-
+  Unification error: Ex checking_check_defs_1_f_f.box_2_lambda_fake_source 1 is cyclic
 
diff --git a/brat/test/golden/graph/cons.brat.graph b/brat/test/golden/graph/cons.brat.graph
index cc61c7b8..3914b766 100644
--- a/brat/test/golden/graph/cons.brat.graph
+++ b/brat/test/golden/graph/cons.brat.graph
@@ -1,11 +1,29 @@
 Nodes:
-(check_defs_1_three_1_cons,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
-(check_defs_1_three_1_const_1,BratNode (Const 0) [] [("value",Int)])
-(check_defs_1_two_cons,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 1))] [("value",Vec(Int, 2))])
-(check_defs_1_two_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 0))] [("value",Vec(Int, 1))])
-(check_defs_1_two_const_1,BratNode (Const 1) [] [("value",Int)])
-(check_defs_1_two_const_3,BratNode (Const 2) [] [("value",Int)])
-(check_defs_1_two_nil_4,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
+(check_defs_1_three_1_Add_3,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
+(check_defs_1_three_1_buildConst_2,BratNode (Const 2) [] [("value",Nat)])
+(check_defs_1_three_1_buildConst_4,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_three_1_buildConst_5,BratNode (Const []) [] [("value",[])])
+(check_defs_1_three_1_cons_6,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
+(check_defs_1_three_1_const_7,BratNode (Const 0) [] [("value",Int)])
+(check_defs_1_three_1_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_three_1_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_two_Add_3,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
+(check_defs_1_two_buildConst_2,BratNode (Const 1) [] [("value",Nat)])
+(check_defs_1_two_buildConst_4,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_two_buildConst_5,BratNode (Const []) [] [("value",[])])
+(check_defs_1_two_buildConst_10,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_two_buildConst_11,BratNode (Const []) [] [("value",[])])
+(check_defs_1_two_buildConst_15,BratNode (Const []) [] [("value",[])])
+(check_defs_1_two_cons_6,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 1))] [("value",Vec(Int, 2))])
+(check_defs_1_two_cons_12,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 0))] [("value",Vec(Int, 1))])
+(check_defs_1_two_const_7,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_two_const_13,BratNode (Const 2) [] [("value",Int)])
+(check_defs_1_two_nil_16,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
+(check_defs_1_two_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_two_numpat2val_9,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_two_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_two_pat2val_8,BratNode Id [("",[])] [("",[])])
+(check_defs_1_two_pat2val_14,BratNode Id [("",[])] [("",[])])
 (globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (globals_Int_7,BratNode (Constructor Int) [] [("value",[])])
 (globals_Vec_1,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
@@ -16,17 +34,28 @@ Nodes:
 (globals_decl_9_three,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
 
 Wires:
-(Ex check_defs_1_three_1_cons 0,Vec(Int, 3),In globals_decl_9_three 0)
-(Ex check_defs_1_three_1_const_1 0,Int,In check_defs_1_three_1_cons 0)
-(Ex check_defs_1_two_cons 0,Vec(Int, 2),In globals_decl_4_two 0)
-(Ex check_defs_1_two_cons_2 0,Vec(Int, 1),In check_defs_1_two_cons 1)
-(Ex check_defs_1_two_const_1 0,Int,In check_defs_1_two_cons 0)
-(Ex check_defs_1_two_const_3 0,Int,In check_defs_1_two_cons_2 0)
-(Ex check_defs_1_two_nil_4 0,Vec(Int, 0),In check_defs_1_two_cons_2 1)
+(Ex check_defs_1_three_1_Add_3 0,Nat,In check_defs_1_three_1_numpat2val_1 0)
+(Ex check_defs_1_three_1_buildConst_2 0,Nat,In check_defs_1_three_1_Add_3 0)
+(Ex check_defs_1_three_1_buildConst_4 0,Nat,In check_defs_1_three_1_Add_3 1)
+(Ex check_defs_1_three_1_buildConst_5 0,[],In check_defs_1_three_1_pat2val 0)
+(Ex check_defs_1_three_1_cons_6 0,Vec(Int, 3),In globals_decl_9_three 0)
+(Ex check_defs_1_three_1_const_7 0,Int,In check_defs_1_three_1_cons_6 0)
+(Ex check_defs_1_two_Add_3 0,Nat,In check_defs_1_two_numpat2val_1 0)
+(Ex check_defs_1_two_buildConst_10 0,Nat,In check_defs_1_two_numpat2val_9 0)
+(Ex check_defs_1_two_buildConst_11 0,[],In check_defs_1_two_pat2val_8 0)
+(Ex check_defs_1_two_buildConst_15 0,[],In check_defs_1_two_pat2val_14 0)
+(Ex check_defs_1_two_buildConst_2 0,Nat,In check_defs_1_two_Add_3 0)
+(Ex check_defs_1_two_buildConst_4 0,Nat,In check_defs_1_two_Add_3 1)
+(Ex check_defs_1_two_buildConst_5 0,[],In check_defs_1_two_pat2val 0)
+(Ex check_defs_1_two_cons_12 0,Vec(Int, 1),In check_defs_1_two_cons_6 1)
+(Ex check_defs_1_two_cons_6 0,Vec(Int, 2),In globals_decl_4_two 0)
+(Ex check_defs_1_two_const_13 0,Int,In check_defs_1_two_cons_12 0)
+(Ex check_defs_1_two_const_7 0,Int,In check_defs_1_two_cons_6 0)
+(Ex check_defs_1_two_nil_16 0,Vec(Int, 0),In check_defs_1_two_cons_12 1)
 (Ex globals_Int_2 0,[],In globals_Vec_1 0)
 (Ex globals_Int_7 0,[],In globals_Vec_6 0)
 (Ex globals_Vec_1 0,[],In globals___kca_two 0)
 (Ex globals_Vec_6 0,[],In globals___kca_three_5 0)
 (Ex globals_const_3 0,Nat,In globals_Vec_1 1)
 (Ex globals_const_8 0,Nat,In globals_Vec_6 1)
-(Ex globals_decl_4_two 0,Vec(Int, 2),In check_defs_1_three_1_cons 1)
+(Ex globals_decl_4_two 0,Vec(Int, 2),In check_defs_1_three_1_cons_6 1)
diff --git a/brat/test/golden/graph/kernel.brat.graph b/brat/test/golden/graph/kernel.brat.graph
index 26ad580e..eb6a97e5 100644
--- a/brat/test/golden/graph/kernel.brat.graph
+++ b/brat/test/golden/graph/kernel.brat.graph
@@ -1,15 +1,33 @@
 Nodes:
-(check_defs_1_id3_thunk_3_lambda_14,KernelNode (PatternMatch ((TestMatchData Kerny (MatchSequence {matchInputs = [(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_6 0, portName = "a1"},Qubit),(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_6 1, portName = "b1"},Qubit),(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_6 2, portName = "c1"},Qubit)], matchTests = [], matchOutputs = [(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_6 0, portName = "a1"},Qubit),(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_6 1, portName = "b1"},Qubit),(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_6 2, portName = "c1"},Qubit)]}),check_defs_1_id3_thunk_3_lambda.0_rhs_thunk_12) :| [])) [("a1",Qubit),("b1",Qubit),("c1",Qubit)] [("a1",Vec(Qubit, 3))])
-(check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 2))] [("value",Vec(Qubit, 3))])
-(check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons_1,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 1))] [("value",Vec(Qubit, 2))])
-(check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons_2,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 0))] [("value",Vec(Qubit, 1))])
-(check_defs_1_id3_thunk_3_lambda.0_rhs_13_nil_3,KernelNode (Constructor nil) [] [("value",Vec(Qubit, 0))])
-(check_defs_1_id3_thunk_3_lambda.0_rhs/in_10,KernelNode Source [] [("q0",Qubit),("q1",Qubit),("q2",Qubit)])
-(check_defs_1_id3_thunk_3_lambda.0_rhs/out_11,KernelNode Target [("a1",Vec(Qubit, 3))] [])
-(check_defs_1_id3_thunk_3_lambda.0_rhs_thunk_12,BratNode (Box (fromList []) check_defs_1_id3_thunk_3_lambda.0_rhs/in_10 check_defs_1_id3_thunk_3_lambda.0_rhs/out_11) [] [("thunk",{ (q0 :: Qubit), (q1 :: Qubit), (q2 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
-(check_defs_1_id3_thunk_3_lambda.0_setup/in_6,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)])
-(check_defs_1_id3_thunk_3_lambda.0_setup/out_7,KernelNode Target [("a1",Vec(Qubit, 3))] [])
-(check_defs_1_id3_thunk_3_lambda.0_setup_thunk_8,BratNode (Box (fromList []) check_defs_1_id3_thunk_3_lambda.0_setup/in_6 check_defs_1_id3_thunk_3_lambda.0_setup/out_7) [] [("thunk",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
+(check_defs_1_id3_thunk_3_lambda_32,KernelNode (PatternMatch ((TestMatchData Kerny (MatchSequence {matchInputs = [(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_24 0, portName = "a1"},Qubit),(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_24 1, portName = "b1"},Qubit),(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_24 2, portName = "c1"},Qubit)], matchTests = [], matchOutputs = [(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_24 0, portName = "a1"},Qubit),(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_24 1, portName = "b1"},Qubit),(NamedPort {end = Ex check_defs_1_id3_thunk_3_lambda.0_setup/in_24 2, portName = "c1"},Qubit)]}),check_defs_1_id3_thunk_3_lambda.0_rhs_thunk_30) :| [])) [("a1",Qubit),("b1",Qubit),("c1",Qubit)] [("a1",Vec(Qubit, 3))])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_Add_3,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_Add_10,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_2,BratNode (Const 2) [] [("value",Nat)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_4,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_5,BratNode (Const []) [] [("value",[])])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_9,BratNode (Const 1) [] [("value",Nat)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_11,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_12,BratNode (Const []) [] [("value",[])])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_16,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_17,BratNode (Const []) [] [("value",[])])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_20,BratNode (Const []) [] [("value",[])])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_6,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 2))] [("value",Vec(Qubit, 3))])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_13,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 1))] [("value",Vec(Qubit, 2))])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_18,KernelNode (Constructor cons) [("head",Qubit),("tail",Vec(Qubit, 0))] [("value",Vec(Qubit, 1))])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_nil_21,KernelNode (Constructor nil) [] [("value",Vec(Qubit, 0))])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_numpat2val_8,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_numpat2val_15,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_pat2val_7,BratNode Id [("",[])] [("",[])])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_pat2val_14,BratNode Id [("",[])] [("",[])])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_31_pat2val_19,BratNode Id [("",[])] [("",[])])
+(check_defs_1_id3_thunk_3_lambda.0_rhs/in_28,KernelNode Source [] [("q0",Qubit),("q1",Qubit),("q2",Qubit)])
+(check_defs_1_id3_thunk_3_lambda.0_rhs/out_29,KernelNode Target [("a1",Vec(Qubit, 3))] [])
+(check_defs_1_id3_thunk_3_lambda.0_rhs_thunk_30,BratNode (Box (fromList []) check_defs_1_id3_thunk_3_lambda.0_rhs/in_28 check_defs_1_id3_thunk_3_lambda.0_rhs/out_29) [] [("thunk",{ (q0 :: Qubit), (q1 :: Qubit), (q2 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
+(check_defs_1_id3_thunk_3_lambda.0_setup/in_24,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)])
+(check_defs_1_id3_thunk_3_lambda.0_setup/out_25,KernelNode Target [("a1",Vec(Qubit, 3))] [])
+(check_defs_1_id3_thunk_3_lambda.0_setup_thunk_26,BratNode (Box (fromList []) check_defs_1_id3_thunk_3_lambda.0_setup/in_24 check_defs_1_id3_thunk_3_lambda.0_setup/out_25) [] [("thunk",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
 (check_defs_1_id3_thunk/in,KernelNode Source [] [("a1",Qubit),("b1",Qubit),("c1",Qubit)])
 (check_defs_1_id3_thunk/out_1,KernelNode Target [("a1",Vec(Qubit, 3))] [])
 (check_defs_1_id3_thunk_thunk_2,BratNode (Box (fromList []) check_defs_1_id3_thunk/in check_defs_1_id3_thunk/out_1) [] [("thunk",{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) })])
@@ -22,17 +40,28 @@ Nodes:
 (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)) })])
 
 Wires:
-(Ex check_defs_1_id3_thunk/in 0,Qubit,In check_defs_1_id3_thunk_3_lambda_14 0)
-(Ex check_defs_1_id3_thunk/in 1,Qubit,In check_defs_1_id3_thunk_3_lambda_14 1)
-(Ex check_defs_1_id3_thunk/in 2,Qubit,In check_defs_1_id3_thunk_3_lambda_14 2)
-(Ex check_defs_1_id3_thunk_3_lambda.0_rhs/in_10 0,Qubit,In check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons 0)
-(Ex check_defs_1_id3_thunk_3_lambda.0_rhs/in_10 1,Qubit,In check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons_1 0)
-(Ex check_defs_1_id3_thunk_3_lambda.0_rhs/in_10 2,Qubit,In check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons_2 0)
-(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons 0,Vec(Qubit, 3),In check_defs_1_id3_thunk_3_lambda.0_rhs/out_11 0)
-(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons_1 0,Vec(Qubit, 2),In check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons 1)
-(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons_2 0,Vec(Qubit, 1),In check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons_1 1)
-(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_13_nil_3 0,Vec(Qubit, 0),In check_defs_1_id3_thunk_3_lambda.0_rhs_13_cons_2 1)
-(Ex check_defs_1_id3_thunk_3_lambda_14 0,Vec(Qubit, 3),In check_defs_1_id3_thunk/out_1 0)
+(Ex check_defs_1_id3_thunk/in 0,Qubit,In check_defs_1_id3_thunk_3_lambda_32 0)
+(Ex check_defs_1_id3_thunk/in 1,Qubit,In check_defs_1_id3_thunk_3_lambda_32 1)
+(Ex check_defs_1_id3_thunk/in 2,Qubit,In check_defs_1_id3_thunk_3_lambda_32 2)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs/in_28 0,Qubit,In check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_6 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs/in_28 1,Qubit,In check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_13 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs/in_28 2,Qubit,In check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_18 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_Add_10 0,Nat,In check_defs_1_id3_thunk_3_lambda.0_rhs_31_numpat2val_8 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_Add_3 0,Nat,In check_defs_1_id3_thunk_3_lambda.0_rhs_31_numpat2val_1 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_11 0,Nat,In check_defs_1_id3_thunk_3_lambda.0_rhs_31_Add_10 1)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_12 0,[],In check_defs_1_id3_thunk_3_lambda.0_rhs_31_pat2val_7 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_16 0,Nat,In check_defs_1_id3_thunk_3_lambda.0_rhs_31_numpat2val_15 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_17 0,[],In check_defs_1_id3_thunk_3_lambda.0_rhs_31_pat2val_14 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_2 0,Nat,In check_defs_1_id3_thunk_3_lambda.0_rhs_31_Add_3 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_20 0,[],In check_defs_1_id3_thunk_3_lambda.0_rhs_31_pat2val_19 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_4 0,Nat,In check_defs_1_id3_thunk_3_lambda.0_rhs_31_Add_3 1)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_5 0,[],In check_defs_1_id3_thunk_3_lambda.0_rhs_31_pat2val 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_buildConst_9 0,Nat,In check_defs_1_id3_thunk_3_lambda.0_rhs_31_Add_10 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_13 0,Vec(Qubit, 2),In check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_6 1)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_18 0,Vec(Qubit, 1),In check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_13 1)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_6 0,Vec(Qubit, 3),In check_defs_1_id3_thunk_3_lambda.0_rhs/out_29 0)
+(Ex check_defs_1_id3_thunk_3_lambda.0_rhs_31_nil_21 0,Vec(Qubit, 0),In check_defs_1_id3_thunk_3_lambda.0_rhs_31_cons_18 1)
+(Ex check_defs_1_id3_thunk_3_lambda_32 0,Vec(Qubit, 3),In check_defs_1_id3_thunk/out_1 0)
 (Ex check_defs_1_id3_thunk_thunk_2 0,{ (a1 :: Qubit), (b1 :: Qubit), (c1 :: Qubit) -o (a1 :: Vec(Qubit, 3)) },In globals_decl_9_id3 0)
 (Ex globals_Qubit_2 0,[],In globals___kcr__1 0)
 (Ex globals_Qubit_3 0,[],In globals___kcr__1 1)
diff --git a/brat/test/golden/graph/list.brat.graph b/brat/test/golden/graph/list.brat.graph
index de1910c1..2790b2b0 100644
--- a/brat/test/golden/graph/list.brat.graph
+++ b/brat/test/golden/graph/list.brat.graph
@@ -1,22 +1,34 @@
 Nodes:
-(check_defs_1_xs_cons,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
+(check_defs_1_xs_buildConst_1,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_buildConst_5,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_buildConst_9,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_buildConst_13,BratNode (Const []) [] [("value",[])])
 (check_defs_1_xs_cons_2,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
-(check_defs_1_xs_cons_4,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
-(check_defs_1_xs_const_1,BratNode (Const 1) [] [("value",Int)])
-(check_defs_1_xs_const_3,BratNode (Const 2) [] [("value",Int)])
-(check_defs_1_xs_const_5,BratNode (Const 3) [] [("value",Int)])
-(check_defs_1_xs_nil_6,BratNode (Constructor nil) [] [("value",List(Int))])
+(check_defs_1_xs_cons_6,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
+(check_defs_1_xs_cons_10,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
+(check_defs_1_xs_const_3,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_xs_const_7,BratNode (Const 2) [] [("value",Int)])
+(check_defs_1_xs_const_11,BratNode (Const 3) [] [("value",Int)])
+(check_defs_1_xs_nil_14,BratNode (Constructor nil) [] [("value",List(Int))])
+(check_defs_1_xs_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_pat2val_4,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_pat2val_8,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_pat2val_12,BratNode Id [("",[])] [("",[])])
 (globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (globals_List_1,BratNode (Constructor List) [("listValue",[])] [("value",[])])
 (globals_decl_3_xs,BratNode Id [("a1",List(Int))] [("a1",List(Int))])
 
 Wires:
-(Ex check_defs_1_xs_cons 0,List(Int),In globals_decl_3_xs 0)
-(Ex check_defs_1_xs_cons_2 0,List(Int),In check_defs_1_xs_cons 1)
-(Ex check_defs_1_xs_cons_4 0,List(Int),In check_defs_1_xs_cons_2 1)
-(Ex check_defs_1_xs_const_1 0,Int,In check_defs_1_xs_cons 0)
+(Ex check_defs_1_xs_buildConst_1 0,[],In check_defs_1_xs_pat2val 0)
+(Ex check_defs_1_xs_buildConst_13 0,[],In check_defs_1_xs_pat2val_12 0)
+(Ex check_defs_1_xs_buildConst_5 0,[],In check_defs_1_xs_pat2val_4 0)
+(Ex check_defs_1_xs_buildConst_9 0,[],In check_defs_1_xs_pat2val_8 0)
+(Ex check_defs_1_xs_cons_10 0,List(Int),In check_defs_1_xs_cons_6 1)
+(Ex check_defs_1_xs_cons_2 0,List(Int),In globals_decl_3_xs 0)
+(Ex check_defs_1_xs_cons_6 0,List(Int),In check_defs_1_xs_cons_2 1)
+(Ex check_defs_1_xs_const_11 0,Int,In check_defs_1_xs_cons_10 0)
 (Ex check_defs_1_xs_const_3 0,Int,In check_defs_1_xs_cons_2 0)
-(Ex check_defs_1_xs_const_5 0,Int,In check_defs_1_xs_cons_4 0)
-(Ex check_defs_1_xs_nil_6 0,List(Int),In check_defs_1_xs_cons_4 1)
+(Ex check_defs_1_xs_const_7 0,Int,In check_defs_1_xs_cons_6 0)
+(Ex check_defs_1_xs_nil_14 0,List(Int),In check_defs_1_xs_cons_10 1)
 (Ex globals_Int_2 0,[],In globals_List_1 0)
 (Ex globals_List_1 0,[],In globals___kca_xs 0)
diff --git a/brat/test/golden/graph/pair.brat.graph b/brat/test/golden/graph/pair.brat.graph
index ef826479..fab32291 100644
--- a/brat/test/golden/graph/pair.brat.graph
+++ b/brat/test/golden/graph/pair.brat.graph
@@ -1,9 +1,17 @@
 Nodes:
-(check_defs_1_xs_cons,BratNode (Constructor cons) [("head",Int),("tail",[Bool])] [("value",[Int,Bool])])
-(check_defs_1_xs_cons_2,BratNode (Constructor cons) [("head",Bool),("tail",[])] [("value",[Bool])])
-(check_defs_1_xs_const_1,BratNode (Const 1) [] [("value",Int)])
-(check_defs_1_xs_nil_4,BratNode (Constructor nil) [] [("value",[])])
-(check_defs_1_xs_true_3,BratNode (Constructor true) [] [("value",Bool)])
+(check_defs_1_xs_buildConst_2,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_buildConst_3,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_buildConst_8,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_buildConst_9,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_cons_4,BratNode (Constructor cons) [("head",Int),("tail",[Bool])] [("value",[Int,Bool])])
+(check_defs_1_xs_cons_10,BratNode (Constructor cons) [("head",Bool),("tail",[])] [("value",[Bool])])
+(check_defs_1_xs_const_5,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_xs_nil_12,BratNode (Constructor nil) [] [("value",[])])
+(check_defs_1_xs_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_pat2val_1,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_pat2val_6,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_pat2val_7,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_true_11,BratNode (Constructor true) [] [("value",Bool)])
 (globals_Bool_4,BratNode (Constructor Bool) [] [("value",[])])
 (globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (globals_cons_1,BratNode (Constructor cons) [("head",[]),("tail",[])] [("value",[])])
@@ -12,11 +20,15 @@ Nodes:
 (globals_nil_5,BratNode (Constructor nil) [] [("value",[])])
 
 Wires:
-(Ex check_defs_1_xs_cons 0,[Int,Bool],In globals_decl_6_xs 0)
-(Ex check_defs_1_xs_cons_2 0,[Bool],In check_defs_1_xs_cons 1)
-(Ex check_defs_1_xs_const_1 0,Int,In check_defs_1_xs_cons 0)
-(Ex check_defs_1_xs_nil_4 0,[],In check_defs_1_xs_cons_2 1)
-(Ex check_defs_1_xs_true_3 0,Bool,In check_defs_1_xs_cons_2 0)
+(Ex check_defs_1_xs_buildConst_2 0,[],In check_defs_1_xs_pat2val_1 0)
+(Ex check_defs_1_xs_buildConst_3 0,[],In check_defs_1_xs_pat2val 0)
+(Ex check_defs_1_xs_buildConst_8 0,[],In check_defs_1_xs_pat2val_7 0)
+(Ex check_defs_1_xs_buildConst_9 0,[],In check_defs_1_xs_pat2val_6 0)
+(Ex check_defs_1_xs_cons_10 0,[Bool],In check_defs_1_xs_cons_4 1)
+(Ex check_defs_1_xs_cons_4 0,[Int,Bool],In globals_decl_6_xs 0)
+(Ex check_defs_1_xs_const_5 0,Int,In check_defs_1_xs_cons_4 0)
+(Ex check_defs_1_xs_nil_12 0,[],In check_defs_1_xs_cons_10 1)
+(Ex check_defs_1_xs_true_11 0,Bool,In check_defs_1_xs_cons_10 0)
 (Ex globals_Bool_4 0,[],In globals_cons_3 0)
 (Ex globals_Int_2 0,[],In globals_cons_1 0)
 (Ex globals_cons_1 0,[],In globals___kca_xs 0)
diff --git a/brat/test/golden/graph/vec.brat.graph b/brat/test/golden/graph/vec.brat.graph
index 844bd6c8..d6a96b30 100644
--- a/brat/test/golden/graph/vec.brat.graph
+++ b/brat/test/golden/graph/vec.brat.graph
@@ -1,24 +1,53 @@
 Nodes:
-(check_defs_1_xs_cons,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
-(check_defs_1_xs_cons_2,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 1))] [("value",Vec(Int, 2))])
-(check_defs_1_xs_cons_4,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 0))] [("value",Vec(Int, 1))])
-(check_defs_1_xs_const_1,BratNode (Const 0) [] [("value",Int)])
-(check_defs_1_xs_const_3,BratNode (Const 1) [] [("value",Int)])
-(check_defs_1_xs_const_5,BratNode (Const 2) [] [("value",Int)])
-(check_defs_1_xs_nil_6,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
+(check_defs_1_xs_Add_3,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
+(check_defs_1_xs_Add_11,BratNode (ArithNode Add) [("lhs",Nat),("rhs",Nat)] [("value",Nat)])
+(check_defs_1_xs_buildConst_2,BratNode (Const 2) [] [("value",Nat)])
+(check_defs_1_xs_buildConst_4,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_xs_buildConst_5,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_buildConst_10,BratNode (Const 1) [] [("value",Nat)])
+(check_defs_1_xs_buildConst_12,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_xs_buildConst_13,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_buildConst_18,BratNode (Const 0) [] [("value",Nat)])
+(check_defs_1_xs_buildConst_19,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_buildConst_23,BratNode (Const []) [] [("value",[])])
+(check_defs_1_xs_cons_6,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
+(check_defs_1_xs_cons_14,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 1))] [("value",Vec(Int, 2))])
+(check_defs_1_xs_cons_20,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 0))] [("value",Vec(Int, 1))])
+(check_defs_1_xs_const_7,BratNode (Const 0) [] [("value",Int)])
+(check_defs_1_xs_const_15,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_xs_const_21,BratNode (Const 2) [] [("value",Int)])
+(check_defs_1_xs_nil_24,BratNode (Constructor nil) [] [("value",Vec(Int, 0))])
+(check_defs_1_xs_numpat2val_1,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_xs_numpat2val_9,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_xs_numpat2val_17,BratNode Id [("",Nat)] [("",Nat)])
+(check_defs_1_xs_pat2val,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_pat2val_8,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_pat2val_16,BratNode Id [("",[])] [("",[])])
+(check_defs_1_xs_pat2val_22,BratNode Id [("",[])] [("",[])])
 (globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (globals_Vec_1,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
 (globals_const_3,BratNode (Const 3) [] [("value",Nat)])
 (globals_decl_4_xs,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
 
 Wires:
-(Ex check_defs_1_xs_cons 0,Vec(Int, 3),In globals_decl_4_xs 0)
-(Ex check_defs_1_xs_cons_2 0,Vec(Int, 2),In check_defs_1_xs_cons 1)
-(Ex check_defs_1_xs_cons_4 0,Vec(Int, 1),In check_defs_1_xs_cons_2 1)
-(Ex check_defs_1_xs_const_1 0,Int,In check_defs_1_xs_cons 0)
-(Ex check_defs_1_xs_const_3 0,Int,In check_defs_1_xs_cons_2 0)
-(Ex check_defs_1_xs_const_5 0,Int,In check_defs_1_xs_cons_4 0)
-(Ex check_defs_1_xs_nil_6 0,Vec(Int, 0),In check_defs_1_xs_cons_4 1)
+(Ex check_defs_1_xs_Add_11 0,Nat,In check_defs_1_xs_numpat2val_9 0)
+(Ex check_defs_1_xs_Add_3 0,Nat,In check_defs_1_xs_numpat2val_1 0)
+(Ex check_defs_1_xs_buildConst_10 0,Nat,In check_defs_1_xs_Add_11 0)
+(Ex check_defs_1_xs_buildConst_12 0,Nat,In check_defs_1_xs_Add_11 1)
+(Ex check_defs_1_xs_buildConst_13 0,[],In check_defs_1_xs_pat2val_8 0)
+(Ex check_defs_1_xs_buildConst_18 0,Nat,In check_defs_1_xs_numpat2val_17 0)
+(Ex check_defs_1_xs_buildConst_19 0,[],In check_defs_1_xs_pat2val_16 0)
+(Ex check_defs_1_xs_buildConst_2 0,Nat,In check_defs_1_xs_Add_3 0)
+(Ex check_defs_1_xs_buildConst_23 0,[],In check_defs_1_xs_pat2val_22 0)
+(Ex check_defs_1_xs_buildConst_4 0,Nat,In check_defs_1_xs_Add_3 1)
+(Ex check_defs_1_xs_buildConst_5 0,[],In check_defs_1_xs_pat2val 0)
+(Ex check_defs_1_xs_cons_14 0,Vec(Int, 2),In check_defs_1_xs_cons_6 1)
+(Ex check_defs_1_xs_cons_20 0,Vec(Int, 1),In check_defs_1_xs_cons_14 1)
+(Ex check_defs_1_xs_cons_6 0,Vec(Int, 3),In globals_decl_4_xs 0)
+(Ex check_defs_1_xs_const_15 0,Int,In check_defs_1_xs_cons_14 0)
+(Ex check_defs_1_xs_const_21 0,Int,In check_defs_1_xs_cons_20 0)
+(Ex check_defs_1_xs_const_7 0,Int,In check_defs_1_xs_cons_6 0)
+(Ex check_defs_1_xs_nil_24 0,Vec(Int, 0),In check_defs_1_xs_cons_20 1)
 (Ex globals_Int_2 0,[],In globals_Vec_1 0)
 (Ex globals_Vec_1 0,[],In globals___kca_xs 0)
 (Ex globals_const_3 0,Nat,In globals_Vec_1 1)