diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs
index 290225f7..5e551544 100644
--- a/brat/Brat/Checker.hs
+++ b/brat/Brat/Checker.hs
@@ -16,11 +16,12 @@ import Control.Monad.Freer
 import Data.Bifunctor
 import Data.Foldable (for_)
 import Data.Functor (($>), (<&>))
-import Data.List ((\\))
+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.Type.Equality ((:~:)(..))
 import Prelude hiding (filter)
 
@@ -37,6 +38,7 @@ import Brat.FC hiding (end)
 import qualified Brat.FC as FC
 import Brat.Graph
 import Brat.Naming
+import Brat.QualName
 -- import Brat.Search
 import Brat.Syntax.Abstractor (NormalisedAbstractor(..), normaliseAbstractor)
 import Brat.Syntax.Common
@@ -45,7 +47,6 @@ import Brat.Syntax.FuncDecl (FunBody(..))
 import Brat.Syntax.Port (ToEnd, toEnd)
 import Brat.Syntax.Simple
 import Brat.Syntax.Value
-import Brat.UserName
 import Bwd
 import Hasochism
 import Util (zipSameLength)
@@ -59,6 +60,15 @@ standardise k val = eval S0 val >>= (\case
 
 mergeEnvs :: [Env a] -> Checking (Env a)
 mergeEnvs = foldM combineDisjointEnvs M.empty
+ where
+  combineDisjointEnvs :: M.Map QualName v -> M.Map QualName v -> Checking (M.Map QualName v)
+  combineDisjointEnvs l r =
+    let commonKeys = S.intersection (M.keysSet l) (M.keysSet r)
+    in if S.null commonKeys
+       then pure $ M.union l r
+       else typeErr ("Variable(s) defined twice: " ++
+    intercalate "," (map show $ S.toList commonKeys))
+
 
 singletonEnv :: (?my :: Modey m) => String -> (Src, BinderType m) -> Checking (Env (EnvData m))
 singletonEnv x input@(p, ty) = case ?my of
@@ -118,13 +128,13 @@ checkWire Braty (WC fc tm) outputs (dangling, o) (hungry, u) = localFC fc $ do
   let ot = binderToValue Braty o
   let ut = binderToValue Braty u
   if outputs
-    then typeEq (show tm) (Zy :* S0 :* S0) (Star []) ot ut
-    else typeEq (show tm) (Zy :* S0 :* S0) (Star []) ut ot
+    then typeEq (show tm) (Star []) ot ut
+    else typeEq (show tm) (Star []) ut ot
   wire (dangling, ot, hungry)
 checkWire Kerny (WC fc tm) outputs (dangling, ot) (hungry, ut) = localFC fc $ do
   if outputs
-    then typeEq (show tm) (Zy :* S0 :* S0) (Dollar []) ot ut
-    else typeEq (show tm) (Zy :* S0 :* S0) (Dollar []) ut ot
+    then typeEq (show tm) (Dollar []) ot ut
+    else typeEq (show tm) (Dollar []) ut ot
   wire (dangling, ot, hungry)
 
 checkIO :: forall m d k exp act . (CheckConstraints m k, ?my :: Modey m)
@@ -242,9 +252,9 @@ check' (Lambda c@(WC abstFC abst,  body) cs) (overs, unders) = do
           (solToEnv . snd)
         (((), synthOuts), ((), ())) <- localEnv env $ check body ((), ())
         pure synthOuts
+
       sig <- mkSig usedOvers synthOuts
-      patOuts <- checkClauses sig usedOvers
-          ((fst c, WC (fcOf body) (Emb body)) :| cs)
+      patOuts <- checkClauses sig usedOvers ((fst c, WC (fcOf body) (Emb body)) :| cs)
       pure (((), patOuts), (rightOvers, ()))
  where
   -- Invariant: When solToEnv is called, port pulling has already been resolved,
@@ -253,7 +263,7 @@ check' (Lambda c@(WC abstFC abst,  body) cs) (overs, unders) = do
   -- N.B.: Here we update the port names to be the user variable names for nicer
   -- error messages. This mirrors previous behaviour using `abstract`, but is a
   --  bit of a hack. See issue #23.
-  solToEnv :: [(String, (Src, BinderType m))] -> Checking (M.Map UserName (EnvData m))
+  solToEnv :: [(String, (Src, BinderType m))] -> Checking (M.Map QualName (EnvData m))
   solToEnv xs = traverse (uncurry singletonEnv) (portNamesToBoundNames xs) >>= mergeEnvs
 
   portNamesToBoundNames :: [(String, (Src, BinderType m))] -> [(String, (Src, BinderType m))]
@@ -421,7 +431,7 @@ check' (NHole (mnemonic, name)) connectors = do
       let ss = intercalate ", " . fmap show <$> sugg
       pure $ take 5 (ms ++ ss)
 
-    findMatchingNouns :: Checking [[UserName]]
+    findMatchingNouns :: Checking [[QualName]]
     findMatchingNouns = do
       -- TODO
       pure []
@@ -455,7 +465,7 @@ check' tm@(Con vcon vargs) ((), (hungry, ty):unders) = do
       (Kerny, _) -> track "Kerny" $ aux Kerny kclup ty
   pure (((), ()), ((), unders))
  where
-  aux :: Modey m -> (UserName -> UserName -> Checking (CtorArgs m)) -> Val Z -> Checking ()
+  aux :: Modey m -> (QualName -> QualName -> Checking (CtorArgs m)) -> Val Z -> Checking ()
   aux my lup ty = do
     VCon tycon tyargs <- track "In forked aux for check' Con" $ eval S0 ty
     (CArgs pats nFree _ argTypeRo) <- track "forked aux doing lup" $ lup vcon tycon
@@ -487,7 +497,7 @@ check' (Simple tm) ((), (hungry, ty):unders) = do
   case (?my, ty, tm) of
     -- The only SimpleType that checks against a kind is a Nat
     (Braty, Left Nat, Num n) -> do
-      (_, _, [(dangling, _)], _) <- next "" (Const (Num n)) (S0,Some (Zy :* S0))
+      (_, _, [(dangling, _)], _) <- next "const" (Const (Num n)) (S0,Some (Zy :* S0))
                                     R0 (REx ("value", Nat) R0)
       let val = VNum (nConstant (fromIntegral n))
       defineSrc dangling val
@@ -498,17 +508,10 @@ check' (Simple tm) ((), (hungry, ty):unders) = do
     _ -> do
       let vty = biType @m ty
       simpleCheck ?my vty tm
-      (_, _, [(dangling, _)], _) <- anext @m "" (Const tm) (S0,Some (Zy :* S0))
+      (_, _, [(dangling, _)], _) <- anext @m "const" (Const tm) (S0,Some (Zy :* S0))
                                      R0 (RPr ("value", vty) R0)
       wire (dangling, vty, hungry)
       pure (((), ()), ((), unders))
-check' Hope ((), ((tgt, ty):unders)) = case (?my, ty) of
-  (Braty, Left _k) -> do
-    fc <- req AskFC
-    req (ANewHope (toEnd tgt, fc))
-    pure (((), ()), ((), unders))
-  (Braty, Right _ty) -> typeErr "Can only infer kinded things with !"
-  (Kerny, _) -> typeErr "Won't infer kernel typed !"
 check' FanOut ((p, ty):overs, ()) = do
   ty <- eval S0 (binderToValue ?my ty)
   case ty of
@@ -564,8 +567,7 @@ check' FanIn (overs, (tgt, ty):unders) = do
     let k = case my of
           Kerny -> Dollar []
           Braty -> Star []
-    -- ALAN merge conflict merge, I added (Zy :* S0 :* S0) but is it correct??
-    typeEq (show FanIn) (Zy :* S0 :* S0) k elTy (binderToValue my overTy)
+    typeEq (show FanIn) k elTy (binderToValue my overTy)
     let tailTy = TVec elTy (VNum (nConstant (n - 1)))
     (_, [(hungryHead, _), (hungryTail, tailTy)], [(danglingResult, _)], _) <- anext "faninNodes" (Constructor (plain "cons")) (S0, Some (Zy :* S0))
       (RPr ("head", elTy) (RPr ("tail", tailTy) R0) :: Ro m Z Z)
@@ -669,7 +671,13 @@ check' (Of n e) ((), unders) = case ?my of
       (elems, unders, rightUnders) <- getVecs len unders
       pure ((tgt, el):elems, (tgt, ty):unders, rightUnders)
   getVecs _ unders = pure ([], [], unders)
-
+check' Hope ((), (NamedPort hope _, ty):unders) = case (?my, ty) of
+  (Braty, Left _k) -> do
+    fc <- req AskFC
+    req (ANewHope hope fc)
+    pure (((), ()), ((), unders))
+  (Braty, Right _ty) -> typeErr "Can only infer kinded things with !"
+  (Kerny, _) -> typeErr "Won't infer kernel typed !"
 check' tm _ = error $ "check' " ++ show tm
 
 
@@ -730,27 +738,23 @@ checkBody :: (CheckConstraints m UVerb, EvMode m, ?my :: Modey m)
           -> FunBody Term UVerb
           -> CTy m Z -- Function type
           -> Checking Src
-checkBody fnName body cty = case body of
-  NoLhs tm -> do
-    ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns -> do
-      (((), ()), leftovers) <- check tm conns
-      checkConnectorsUsed (fcOf tm, fcOf tm) (show tm) conns leftovers
-    pure src
-  Clauses (c :| cs) -> do
-    fc <- req AskFC
-    ((box, _), _) <- makeBox (fnName ++ ".box") cty $ \conns -> do
-      let tm = Lambda c cs
-      (((), ()), leftovers) <- check (WC fc tm) conns
-      checkConnectorsUsed (bimap fcOf fcOf c) (show tm) conns leftovers
-    pure box
-  Undefined -> err (InternalError "Checking undefined clause")
- where
-  checkConnectorsUsed _ _ _ ([], []) = pure ()
-  checkConnectorsUsed (_, tmFC) tm (_, unders) ([], rightUnders) = localFC tmFC $
-    let numUsed = length unders - length rightUnders in
-     err (TypeMismatch tm (showRow unders) (showRow (take numUsed unders)))
-  checkConnectorsUsed (absFC, _) _ _ (rightOvers, _) = localFC absFC $
-    typeErr ("Inputs " ++ showRow rightOvers ++ " weren't used")
+checkBody fnName body cty = do
+  (tm, (absFC, tmFC)) <- case body of
+    NoLhs tm -> pure (tm, (fcOf tm, fcOf tm))
+    Clauses (c@(abs, tm) :| cs) -> do
+      fc <- req AskFC
+      pure (WC fc (Lambda c cs), (fcOf abs, fcOf tm))
+    Undefined -> err (InternalError "Checking undefined clause")
+  ((src, _), _) <- makeBox (fnName ++ ".box") cty $ \conns@(_, unders) -> do
+    (((), ()), leftovers) <- check tm conns
+    case leftovers of
+      ([], []) -> pure ()
+      ([], rightUnders) -> localFC tmFC $
+        let numUsed = length unders - length rightUnders
+        in err (TypeMismatch (show tm) (showRow unders) (showRow (take numUsed unders)))
+      (rightOvers, _) -> localFC absFC $
+        typeErr ("Inputs " ++ showRow rightOvers ++ " weren't used")
+  pure src
 
 -- Constructs row from a list of ends and types. Uses standardize to ensure that dependency is
 -- detected. Fills in the first bot ends from a stack. The stack grows every time we go under
@@ -814,7 +818,7 @@ kindCheck ((hungry, k@(TypeFor m [])):unders) (Con c arg) = req (TLup (m, c)) >>
         -- the thing we *do* define kindOut as
 
         (_, argUnders, [(kindOut,_)], (_ :<< _va, _)) <-
-          next "" Hypo (S0, Some (Zy :* S0)) aliasArgs (REx ("type",Star []) R0)
+          next "kc_alias" Hypo (S0, Some (Zy :* S0)) aliasArgs (REx ("type",Star []) R0)
         -- arg is a juxtaposition
         (args, emptyUnders) <- kindCheck (second (\(Left k) -> k) <$> argUnders) (unWC arg)
         ensureEmpty "alias args" emptyUnders
@@ -884,7 +888,7 @@ kindCheck unders (Emb (WC fc (Var v))) = localFC fc $ vlup v >>= f unders
   f _ (x:_) = err $ InternalError $ "Kindchecking a row which contains " ++ show x
 -- TODO: Add other operations on numbers
 kindCheck ((hungry, Nat):unders) (Simple (Num n)) | n >= 0 = do
-  (_, _, [(dangling, _)], _) <- next "" (Const (Num n)) (S0,Some (Zy :* S0)) R0 (REx ("value", Nat) R0)
+  (_, _, [(dangling, _)], _) <- next "const" (Const (Num n)) (S0,Some (Zy :* S0)) R0 (REx ("value", Nat) R0)
   let value = VNum (nConstant (fromIntegral n))
   defineTgt hungry value
   defineSrc dangling value
@@ -987,8 +991,8 @@ kindCheckRow' my ez@(ny :* s) env (name, i) ((p, bty):rest) = case (my, bty) of
 
 -- Look for vectors to produce better error messages for mismatched lengths
 -- in terms or patterns.
-detectVecErrors :: UserName  -- Term constructor name
-                -> UserName  -- Type constructor name
+detectVecErrors :: QualName  -- Term constructor name
+                -> QualName  -- Type constructor name
                 -> [Val Z]   -- Type arguments
                 -> [ValPat]  -- Patterns the type arguments are checked against
                 -> Val Z     -- Type
@@ -1095,13 +1099,13 @@ abstractPattern my (dangling, bty) pat@(PCon pcon abst) = case (my, bty) of
   helper :: Modey m
          -> Val Z
          -> TypeKind
-         -> (UserName -> UserName -> Checking (CtorArgs m))
+         -> (QualName -> QualName -> Checking (CtorArgs m))
          -> Checking (Env (EnvData m))
   helper my v k lup = standardise k v >>=
                       throwLeft . unpackTypeConstructor >>=
                       abstractCon my lup
 
-  unpackTypeConstructor :: Val Z -> Either ErrorMsg (UserName, [Val Z])
+  unpackTypeConstructor :: Val Z -> Either ErrorMsg (QualName, [Val Z])
   unpackTypeConstructor (VCon tycon tyargs) = pure (tycon, tyargs)
   unpackTypeConstructor ty = Left (PattErr $ unwords ["Couldn't resolve pattern"
                                                      ,show pat
@@ -1109,8 +1113,8 @@ abstractPattern my (dangling, bty) pat@(PCon pcon abst) = case (my, bty) of
                                                      ,show ty])
 
   abstractCon :: Modey m
-              -> (UserName -> UserName -> Checking (CtorArgs m))
-              -> (UserName, [Val Z])
+              -> (QualName -> QualName -> Checking (CtorArgs m))
+              -> (QualName, [Val Z])
               -> Checking (Env (EnvData m))
   abstractCon my lup (tycon, tyargs) = do
     let ty = VCon tycon tyargs
@@ -1147,15 +1151,15 @@ run ve initStore ns m = do
                 , kconstructors = kernelConstructors
                 , typeConstructors = defaultTypeConstructors
                 , aliasTable = M.empty
-                , hopeSet = M.empty
+                , hopes = M.empty
                 , captureSets = M.empty
                 }
   (a,ctx,(holes, graph)) <- handler (localNS ns m) ctx mempty
   let tyMap = typeMap $ store ctx
-  -- If the hopeSet has any remaining holes with kind Nat, we need to abort.
+  -- 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 e) (hopeSet ctx) of
+  case M.toList $ M.filterWithKey (\e _ -> isNatKinded tyMap (InEnd e)) (hopes ctx) of
     [] -> pure (a, (holes, store ctx, graph, captureSets ctx))
     -- Just use the FC of the first hole while we don't have the capacity to
     -- show multiple error locations
diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs
index f929f17e..f736bafe 100644
--- a/brat/Brat/Checker/Helpers.hs
+++ b/brat/Brat/Checker/Helpers.hs
@@ -1,8 +1,26 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 
-module Brat.Checker.Helpers where
-
-import Brat.Checker.Monad (Checking, CheckingSig(..), captureOuterLocals, err, typeErr, kindArgRows, defineEnd, throwLeft, isSkolem, mkYield)
+module Brat.Checker.Helpers {-(pullPortsRow, pullPortsSig
+                            ,simpleCheck
+                            ,combineDisjointEnvs
+                            ,ensureEmpty, noUnders
+                            ,rowToSig
+                            ,showMode, getVec
+                            ,mkThunkTy
+                            ,wire
+                            ,next, knext, anext
+                            ,kindType, getThunks
+                            ,binderToValue, valueToBinder
+                            ,kConFields
+                            ,defineSrc, defineTgt
+                            ,declareSrc, declareTgt
+                            ,makeBox
+                            ,uncons
+                            ,evalBinder
+                            ,evalSrcRow, evalTgtRow
+                            )-} where
+
+import Brat.Checker.Monad (Checking, CheckingSig(..), captureOuterLocals, defineEnd, err,  kindArgRows, isSkolem, mkYield, throwLeft, typeErr)
 import Brat.Checker.Types
 import Brat.Error (ErrorMsg(..))
 import Brat.Eval (eval, EvMode(..), kindType)
@@ -14,15 +32,16 @@ import Brat.Syntax.Core (Term(..))
 import Brat.Syntax.Simple
 import Brat.Syntax.Port (ToEnd(..))
 import Brat.Syntax.Value
-import Brat.UserName
 import Bwd
 import Hasochism
 import Util (log2)
 
-import Control.Monad.Freer
-import Data.Functor ((<&>))
+import Control.Monad.State.Lazy (StateT(..), runStateT)
+import Control.Monad.Freer (req)
 import Data.Bifunctor
-import Data.List (intercalate)
+import Data.Foldable (foldrM)
+import Data.Functor ((<&>))
+import Data.List (partition)
 import Data.Type.Equality (TestEquality(..), (:~:)(..))
 import qualified Data.Map as M
 import qualified Data.Set as S
@@ -31,7 +50,9 @@ import Prelude hiding (last)
 simpleCheck :: Modey m -> Val Z -> SimpleTerm -> Checking ()
 simpleCheck my ty tm = case (my, ty) of
   (Braty, VApp (VPar e) _) -> do
-    isHope <- req AskHopeSet <&> M.member e
+    isHope <- case e of
+      ExEnd _ -> pure False
+      InEnd e -> req AskHopes <&> M.member e
     if isHope then
       case tm of
         Float _ -> defineEnd e TFloat
@@ -102,43 +123,29 @@ pullPortsRow :: Show ty
              => [PortName]
              -> [(NamedPort e, ty)]
              -> Checking [(NamedPort e, ty)]
-pullPortsRow = pullPorts portName showRow
+pullPortsRow = pullPorts (portName . fst) showRow
 
 pullPortsSig :: Show ty
              => [PortName]
              -> [(PortName, ty)]
              -> Checking [(PortName, ty)]
-pullPortsSig = pullPorts id showSig
+pullPortsSig = pullPorts fst showSig
 
-pullPorts :: forall a ty. Show ty
-          => (a -> PortName) -- A way to get a port name for each element
-          -> ([(a, ty)] -> String) -- A way to print the list
+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
-          -> [(a, ty)]  -- The list to rearrange
-          -> Checking [(a, ty)]
-pullPorts _ _ [] types = pure types
-pullPorts toPort showFn (p:ports) types = do
-  (x, types) <- pull1Port p types
-  (x:) <$> pullPorts toPort showFn ports types
+          -> [a]  -- The list to rearrange
+          -> Checking [a]
+pullPorts toPort showFn to_pull types =
+  -- the "state" here is the things still available to be pulled
+  (\(pulled, rest) -> pulled ++ rest) <$> runStateT (mapM pull1Port to_pull) types
  where
-  pull1Port :: PortName
-            -> [(a, ty)]
-            -> Checking ((a, ty), [(a, ty)])
-  pull1Port p [] = fail $ "Port not found: " ++ p ++ " in " ++ showFn types
-  pull1Port p (x@(a,_):xs)
-   | p == toPort a
-   = if p `elem` (toPort . fst <$> xs)
-     then err (AmbiguousPortPull p (showFn (x:xs)))
-     else pure (x, xs)
-   | otherwise = second (x:) <$> pull1Port p xs
-
-combineDisjointEnvs :: M.Map UserName v -> M.Map UserName v -> Checking (M.Map UserName v)
-combineDisjointEnvs l r =
-  let commonKeys = S.intersection (M.keysSet l) (M.keysSet r)
-  in if S.null commonKeys
-    then Ret $ M.union l r
-    else typeErr ("Variable(s) defined twice: " ++
-      intercalate "," (map show $ S.toList commonKeys))
+  pull1Port :: PortName -> StateT [a] Checking a
+  pull1Port p = StateT $ \available -> case partition ((== p) . toPort) available of
+      ([], _) -> err $ BadPortPull p (showFn available)
+      ([found], remaining) -> pure (found, remaining)
+      (_, _) -> err $ AmbiguousPortPull p (showFn available)
 
 ensureEmpty :: Show ty => String -> [(NamedPort e, ty)] -> Checking ()
 ensureEmpty _ [] = pure ()
@@ -268,111 +275,66 @@ getThunks :: Modey m
                       ,Overs m UVerb
                       )
 getThunks _ [] = pure ([], [], [])
-getThunks Braty row@((src, Right ty):rest) = req AskHopeSet >>= \h -> eval S0 ty >>= \case
-  VApp (VPar e) _ | M.member e h -> mkYield "getThunks" (S.singleton e) >> getThunks Braty row
-  ty -> do
-    (src, VFun Braty (ss :->> ts)) <- vectorise (src, ty)
-    (node, unders, overs, _) <- let ?my = Braty in
-                                  anext "" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts
-    (nodes, unders', overs') <- getThunks Braty rest
-    pure (node:nodes, unders <> unders', overs <> overs')
--- TODO we probably want to check against the HopeSet here too, good to refactor+common-up somehow
-getThunks Kerny row@((src, Right ty):rest) = (eval S0 ty >>= vectorise . (src,)) >>= \case
-  (src, VFun Kerny (ss :->> ts)) -> do
-    (node, unders, overs, _) <- let ?my = Kerny in anext "" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts
-    (nodes, unders', overs') <- getThunks Kerny rest
-    pure (node:nodes, unders <> unders', overs <> overs')
-  -- These shouldn't happen (as this is return value of vectorise - can we return something more specific?)
-  (_, VFun _ _) -> err $ ExpectedThunk (showMode Kerny) (showRow row)
-  v -> typeErr $ "Force called on non-(kernel)-thunk: " ++ show v
+getThunks Braty ((src, Right ty):rest) = do
+  ty <- eval S0 ty
+  (src, ss :->> ts) <- vectorise Braty (src, ty)
+  (node, unders, overs, _) <- let ?my = Braty in
+                                anext "Eval" (Eval (end src)) (S0, Some (Zy :* S0)) ss ts
+  (nodes, unders', overs') <- getThunks Braty rest
+  pure (node:nodes, unders <> unders', overs <> overs')
+getThunks Kerny ((src, Right ty):rest) = do
+  ty <- eval S0 ty
+  (src, ss :->> ts) <- vectorise Kerny (src,ty)
+  (node, unders, overs, _) <- let ?my = Kerny in anext "Splice" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts
+  (nodes, unders', overs') <- getThunks Kerny rest
+  pure (node:nodes, unders <> unders', overs <> overs')
 getThunks Braty ((src, Left (Star args)):rest) = do
   (node, unders, overs) <- case bwdStack (B0 <>< args) of
     Some (_ :* stk) -> do
       let (ri,ro) = kindArgRows stk
-      (node, unders, overs, _) <- next "" (Eval (end src)) (S0, Some (Zy :* S0)) ri ro
+      (node, unders, overs, _) <- next "Eval" (Eval (end src)) (S0, Some (Zy :* S0)) ri ro
       pure (node, unders, overs)
   (nodes, unders', overs') <- getThunks Braty rest
   pure (node:nodes, unders <> unders', overs <> overs')
 getThunks m ro = err $ ExpectedThunk (showMode m) (showRow ro)
 
 -- The type given here should be normalised
-vecLayers :: Val Z -> Checking ([(Src, NumVal (VVar Z))] -- The sizes of the vector layers
-                               ,Some (Modey :* Flip CTy Z) -- The function type at the end
-                               )
-vecLayers (TVec ty (VNum n)) = do
-  src <- mkStaticNum n
-  (layers, fun) <- vecLayers ty
-  pure ((src, n):layers, fun)
-vecLayers (VFun my cty) = pure ([], Some (my :* Flip cty))
-vecLayers ty = typeErr $ "Expected a 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 :: (Src, Val Z) -> Checking (Src, Val Z)
-vectorise (src, ty) = do
-  (layers, Some (my :* Flip cty)) <- vecLayers ty
-  modily my $ mkMapFuns (src, VFun my cty) layers
+vecLayers :: Modey m -> Val Z -> Checking ([(Src, NumVal (VVar Z))] -- The sizes of the vector layers
+                                          ,CTy m Z -- The function type at the end
+                                          )
+vecLayers my ty = req AskHopes >>= \h -> case (my, ty) of
+  (_, (VApp (VPar e) _)) | InEnd ie <- e, M.member ie h ->
+    mkYield "getThunks" (S.singleton e) >> vecLayers my ty
+  (my, (TVec ty (VNum n))) -> do
+    src <- buildNatVal n
+    first ((src, n):) <$> vecLayers my ty
+  (Braty,(VFun Braty cty)) -> pure ([], cty)
+  (Kerny,(VFun Kerny cty)) -> pure ([], cty)
+  (my, ty) -> typeErr $ "Expected a " ++ showMode my ++ "function or vector of functions, got " ++ show ty
+
+vectorise :: forall m. Modey m -> (Src, Val Z) -> Checking (Src, CTy m Z)
+vectorise my (src, ty) = do
+  (layers, cty) <- vecLayers my ty
+  modily my $ foldrM mkMapFun (src, cty) layers
  where
-  mkMapFuns :: (Src, Val Z) -- The input to the mapfun
-            -> [(Src, NumVal (VVar Z))] -- Remaining layers
-            -> Checking (Src, Val Z)
-  mkMapFuns over [] = pure over
-  mkMapFuns (valSrc, ty) ((lenSrc, len):layers) = do
-    (valSrc, ty@(VFun my cty)) <- mkMapFuns (valSrc, ty) layers
+  mkMapFun :: (Src, NumVal (VVar Z)) -- Layer to apply
+            -> (Src, CTy m Z) -- The input to this level of mapfun
+            -> Checking (Src, CTy m Z)
+  mkMapFun (lenSrc, len) (valSrc, cty) = do
     let weak1 = changeVar (Thinning (ThDrop ThNull))
     vecFun <- vectorisedFun len my cty
-    (_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right vecTy)], _) <-
-      next "" MapFun (S0, Some (Zy :* S0))
+    (_, [(lenTgt,_), (valTgt, _)], [(vectorSrc, Right (VFun my' cty))], _) <-
+      next "MapFun" MapFun (S0, Some (Zy :* S0))
       (REx ("len", Nat) (RPr ("value", weak1 ty) R0))
       (RPr ("vector", weak1 vecFun) R0)
     defineTgt lenTgt (VNum len)
     wire (lenSrc, kindType Nat, lenTgt)
     wire (valSrc, ty, valTgt)
-    pure (vectorSrc, vecTy)
+    let vecCTy = case (my,my',cty) of
+          (Braty,Braty,cty) -> cty
+          (Kerny,Kerny,cty) -> cty
+          _ -> error "next returned wrong mode of computation type to that passed in"
+    pure (vectorSrc, vecCTy)
 
   vectorisedFun :: NumVal (VVar Z) -> Modey m -> CTy m Z -> Checking (Val Z)
   vectorisedFun nv my (ss :->> ts) = do
@@ -402,10 +364,10 @@ valueToBinder Braty = Right
 valueToBinder Kerny = id
 
 defineSrc :: Src -> Val Z -> Checking ()
-defineSrc src v = defineEnd (ExEnd (end src)) v
+defineSrc src = defineEnd (ExEnd (end src))
 
 defineTgt :: Tgt -> Val Z -> Checking ()
-defineTgt tgt v = defineEnd (InEnd (end tgt)) v
+defineTgt tgt = defineEnd (InEnd (end tgt))
 
 declareTgt :: Tgt -> Modey m -> BinderType m -> Checking ()
 declareTgt tgt my ty = req (Declare (InEnd (end tgt)) my ty False)
@@ -518,10 +480,103 @@ runArith _ _ _ = Nothing
 
 buildArithOp :: ArithOp -> Checking ((Tgt, Tgt), Src)
 buildArithOp op = do
-  (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next "" (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0)
+  (_, [(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 "" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0)
+  (_, _, [(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
+
+-- 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
+    nDangling <- buildNum n
+    ((lhs,rhs),out) <- buildArithOp Add
+    src <- buildGro gro
+    req $ Wire (end nDangling, TNat, end lhs)
+    req $ Wire (end src, TNat, end rhs)
+    defineSrc out (VNum (nPlus n (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
+    -- Calculate 2^k as `factor`
+    two <- buildNum 2
+    kDangling <- buildNum k
+    ((lhs,rhs),factor) <- buildArithOp Pow
+    req $ Wire (end two, TNat, end lhs)
+    req $ Wire (end kDangling, TNat, end rhs)
+    -- Multiply mono by 2^k
+    ((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
diff --git a/brat/Brat/Checker/Monad.hs b/brat/Brat/Checker/Monad.hs
index 78fe523c..accfba48 100644
--- a/brat/Brat/Checker/Monad.hs
+++ b/brat/Brat/Checker/Monad.hs
@@ -7,9 +7,9 @@ import Brat.Error (Error(..), ErrorMsg(..), dumbErr)
 import Brat.FC (FC)
 import Brat.Graph
 import Brat.Naming (fresh, split, Name, Namespace, FreshMonad(..))
+import Brat.QualName (QualName)
 import Brat.Syntax.Common
 import Brat.Syntax.Value
-import Brat.UserName (UserName)
 import Hasochism
 import Util
 
@@ -54,7 +54,7 @@ data CtxEnv = CtxEnv
   , locals :: VEnv
   }
 
-type HopeSet = M.Map End FC
+type Hopes = M.Map InPort FC
 
 type CaptureSets = M.Map Name VEnv
 
@@ -62,10 +62,10 @@ data Context = Ctx { globalVEnv :: VEnv
                    , store :: Store
                    , constructors :: ConstructorMap Brat
                    , kconstructors :: ConstructorMap Kernel
-                   , typeConstructors :: M.Map (Mode, UserName) [(PortName, TypeKind)]
-                   , aliasTable :: M.Map UserName Alias
+                   , typeConstructors :: M.Map (Mode, QualName) [(PortName, TypeKind)]
+                   , aliasTable :: M.Map QualName Alias
                    -- All the ends here should be targets
-                   , hopeSet :: HopeSet
+                   , hopes :: Hopes
                    , captureSets :: CaptureSets
                    }
 
@@ -82,33 +82,34 @@ data CheckingSig ty where
   Throw   :: Error  -> CheckingSig a
   LogHole :: TypedHole -> CheckingSig ()
   AskFC   :: CheckingSig FC
-  VLup    :: UserName -> CheckingSig (Maybe [(Src, BinderType Brat)])
-  KLup    :: UserName -> CheckingSig (Maybe (Src, BinderType Kernel))
+  VLup    :: QualName -> CheckingSig (Maybe [(Src, BinderType Brat)])
+  KLup    :: QualName -> CheckingSig (Maybe (Src, BinderType Kernel))
   -- Lookup type constructors
-  TLup    :: (Mode, UserName) -> CheckingSig (Maybe [(PortName, TypeKind)])
+  TLup    :: (Mode, QualName) -> CheckingSig (Maybe [(PortName, TypeKind)])
   -- Lookup term constructor - ask whether a constructor builds a certain type
   CLup    :: FC -- File context for error reporting
-          -> UserName -- Value constructor
-          -> UserName  -- Type constructor
+          -> QualName -- Value constructor
+          -> QualName  -- Type constructor
           -> CheckingSig (CtorArgs Brat)
   -- Lookup kernel constructors
   KCLup   :: FC -- File context for error reporting
-          -> UserName -- Value constructor
-          -> UserName  -- Type constructor
+          -> QualName -- Value constructor
+          -> QualName  -- Type constructor
           -> CheckingSig (CtorArgs Kernel)
   -- Lookup an end in the Store
   ELup    :: End -> CheckingSig (Maybe (Val Z))
   -- Lookup an alias in the table
-  ALup    :: UserName -> CheckingSig (Maybe Alias)
-  TypeOf  :: End -> CheckingSig (EndType, Bool)
+  ALup    :: QualName -> CheckingSig (Maybe Alias)
+  TypeOf  :: End -> CheckingSig (EndType, Bool) -- Bool = is-skolem
   AddNode :: Name -> Node -> CheckingSig ()
   Wire    :: Wire -> CheckingSig ()
   KDone   :: CheckingSig ()
   AskVEnv :: CheckingSig CtxEnv
-  Declare :: End -> Modey m -> BinderType m -> Bool -> CheckingSig () -- Bool = is-skole
-  ANewHope :: (End, FC) -> CheckingSig ()
-  AskHopeSet :: CheckingSig HopeSet
-  AddCapture :: Name -> (UserName, [(Src, BinderType Brat)]) -> CheckingSig ()
+  Declare :: End -> Modey m -> BinderType m -> Bool -> CheckingSig () -- Bool = is-skolem
+  ANewHope :: InPort -> FC -> CheckingSig ()
+  AskHopes :: CheckingSig Hopes
+  RemoveHope :: InPort -> CheckingSig ()
+  AddCapture :: Name -> (QualName, [(Src, BinderType Brat)]) -> CheckingSig ()
 
 wrapper :: (forall a. CheckingSig a -> Checking (Maybe a)) -> Checking v -> Checking v
 wrapper _ (Ret v) = Ret v
@@ -122,7 +123,7 @@ 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
 wrapper2 f = wrapper (\s -> pure (f s))
 
-localAlias :: (UserName, Alias) -> Checking v -> Checking v
+localAlias :: (QualName, Alias) -> Checking v -> Checking v
 localAlias (name, alias) = wrapper2 (\case
     ALup u | u == name -> Just (Just alias)
     _ -> Nothing)
@@ -138,13 +139,13 @@ localEnv = case ?my of
   Braty -> localVEnv
   Kerny -> \env m -> localKVar env (m <* req KDone)
 
-localVEnv :: M.Map UserName [(Src, BinderType Brat)] -> Checking v -> Checking v
+localVEnv :: M.Map QualName [(Src, BinderType Brat)] -> Checking v -> Checking v
 localVEnv ext = wrapper (\case
   (VLup x) | j@(Just _) <- M.lookup x ext -> pure $ Just j -- invoke continuation with j
   AskVEnv -> do
     outerEnv <- req AskVEnv
     pure $ Just -- value to return to original continuation
-      (outerEnv { locals = M.union ext (locals outerEnv) })  -- ext shadows local vars                          
+      (outerEnv { locals = M.union ext (locals outerEnv) })  -- ext shadows local vars
   _ -> pure Nothing)
 
 -- runs a computation, but logs (via AddCapture, under the specified Name) uses of outer
@@ -168,27 +169,27 @@ throwLeft :: Either ErrorMsg a -> Checking a
 throwLeft (Right x) = pure x
 throwLeft (Left msg) = err msg
 
-vlup :: UserName -> Checking [(Src, BinderType Brat)]
+vlup :: QualName -> Checking [(Src, BinderType Brat)]
 vlup s = req (VLup s) >>= \case
     Just vty -> pure vty
     Nothing -> err $ VarNotFound (show s)
 
-alup :: UserName -> Checking Alias
+alup :: QualName -> Checking Alias
 alup s = req (ALup s) >>= \case
     Just vty -> pure vty
     Nothing -> err $ VarNotFound (show s)
 
-clup :: UserName -- Value constructor
-     -> UserName  -- Type constructor
+clup :: QualName -- Value constructor
+     -> QualName  -- Type constructor
      -> Checking (CtorArgs Brat)
 clup vcon tycon = req AskFC >>= \fc -> req (CLup fc vcon tycon)
 
-kclup :: UserName -- Value constructor
-      -> UserName  -- Type constructor
+kclup :: QualName -- Value constructor
+      -> QualName  -- Type constructor
       -> Checking (CtorArgs Kernel)
 kclup vcon tycon = req AskFC >>= \fc -> req (KCLup fc vcon tycon)
 
-tlup :: (Mode, UserName) -> Checking [(PortName, TypeKind)]
+tlup :: (Mode, QualName) -> Checking [(PortName, TypeKind)]
 tlup (m, c) = req (TLup (m, c)) >>= \case
   Nothing -> req (TLup (otherMode, c)) >>= \case
     Nothing -> err $ UnrecognisedTypeCon (show c)
@@ -199,7 +200,7 @@ tlup (m, c) = req (TLup (m, c)) >>= \case
     Brat -> Kernel
     Kernel -> Brat
 
-lookupAndUse :: UserName -> KEnv
+lookupAndUse :: QualName -> KEnv
              -> Either Error (Maybe ((Src, BinderType Kernel), KEnv))
 lookupAndUse x kenv = case M.lookup x kenv of
    Nothing -> Right Nothing
@@ -297,8 +298,14 @@ handler (Req s k) ctx g
                 M.lookup tycon tbl
         handler (k args) ctx g
 
-      ANewHope (e, fc) -> handler (k ()) (ctx { hopeSet = M.insert e fc (hopeSet ctx) }) g
-      AskHopeSet -> handler (k (hopeSet ctx)) ctx g
+      ANewHope e fc -> handler (k ()) (ctx { hopes = M.insert e fc (hopes ctx) }) g
+
+      AskHopes -> handler (k (hopes ctx)) ctx g
+
+      RemoveHope e -> let hset = hopes ctx in
+                        if M.member e hset
+                        then handler (k ()) (ctx { hopes = M.delete e hset }) g
+                        else Left (dumbErr (InternalError ("Trying to remove Hope not in set: " ++ show e)))
       AddCapture n (var, ends) ->
         handler (k ()) ctx {captureSets=M.insertWith M.union n (M.singleton var ends) (captureSets ctx)} g
 
@@ -311,19 +318,22 @@ handler (Define end v k) ctx g = let st@Store{typeMap=tm, valueMap=vm} = store c
         -- TODO(1) can we check the value is of the kind declared?
         -- TODO(2) it'd be better to figure out if the end is really Unstuck,
         -- or just awaiting some other end, but that seems overly complex atm, as
-        -- (a) we must be "Unstuck" if the end is Defined to something Skolem *OR* in the HopeSet,
+        -- (a) we must be "Unstuck" if the end is Defined to something Skolem *OR* in the `hopes`,
         -- (b) Numbers are tricky, whether they are stuck or not depends upon the question
         -- (c) since there are no infinite end-creating loops, it's correct (merely inefficient)
         -- to just "have another go".
         Just _ -> let news = News (M.singleton end Unstuck) in
           handler (k news)
             (ctx { store = st { valueMap = M.insert end v vm },
-                hopeSet = M.delete end (hopeSet ctx)
+                hopes = (case end of
+                          ExEnd _ -> id
+                          InEnd e -> M.delete e
+                        ) (hopes ctx)
             }) g
 handler (Yield Unstuck k) ctx g = handler (k mempty) ctx g
 handler (Yield (AwaitingAny ends) _k) ctx _ = Left $ dumbErr $ TypeErr $ unlines $
   ("Typechecking blocked on:":(show <$> S.toList ends))
-  ++ "":"Hopeset is":(show <$> M.keys (hopeSet ctx)) ++ ["Try writing more types! :-)"]
+  ++ "":"Hopeset is":(show <$> M.keys (hopes ctx)) ++ ["Try writing more types! :-)"]
 handler (Fork desc par c) ctx g = handler (thTrace ("Spawning " ++ desc) $ par *> c) ctx g
 
 type Checking = Free CheckingSig
@@ -364,9 +374,6 @@ suppressGraph = wrapper2 (\case
   (Wire _) -> Just ()
   _ -> Nothing)
 
-defineEnd :: End -> Val Z -> Checking ()
-defineEnd e v = Define e v (const (Ret ()))
-
 inLvl :: String -> Checking a -> Checking a
 inLvl prefix c = req (SplitNS prefix) >>= \prefixNamespace -> localNS prefixNamespace c
 
@@ -381,3 +388,6 @@ localNS ns (Define e v k) = Define e v (localNS ns . k)
 localNS ns (Yield st k) = Yield 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)
+
+defineEnd :: End -> Val Z -> Checking ()
+defineEnd e v = Define e v (const (Ret ()))
diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs
index d5c4bece..45acd403 100644
--- a/brat/Brat/Checker/SolveHoles.hs
+++ b/brat/Brat/Checker/SolveHoles.hs
@@ -1,11 +1,10 @@
-module Brat.Checker.SolveHoles (typeEq, buildNatVal, buildNum, invertNatVal) where
+module Brat.Checker.SolveHoles (typeEq, buildNum) where
 
 import Brat.Checker.Monad
 import Brat.Checker.Types (kindForMode)
-import Brat.Checker.Helpers (buildArithOp, buildConst, next)
+import Brat.Checker.Helpers (buildConst, buildNatVal, buildNum)
 import Brat.Error (ErrorMsg(..))
 import Brat.Eval
-import Brat.Graph (NodeType(..))
 import Brat.Syntax.Common
 import Brat.Syntax.Simple (SimpleTerm(..))
 import Brat.Syntax.Value
@@ -15,24 +14,33 @@ import Hasochism
 import Util (zipSameLength)
 
 import Control.Monad (filterM, unless, (>=>))
-import Data.Foldable (traverse_)
+import Data.Bifunctor (second)
+import Data.Foldable (sequenceA_)
 import Data.Functor
 import Data.Maybe (catMaybes)
 import qualified Data.Map as M
 import qualified Data.Set as S
 import Data.Type.Equality (TestEquality(..), (:~:)(..))
 
--- Demand that two things are equal, we're allowed to solve variables in the
--- hope set to make this true.
--- Raises a user error if the vals cannot be made equal.
+-- External interface to typeEq' for closed values only.
 typeEq :: String -- String representation of the term for error reporting
-       -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n
        -> TypeKind -- The kind we're comparing at
-       -> Val n -- Expected
-       -> Val n -- Actual
+       -> Val Z -- Expected
+       -> Val Z -- Actual
        -> Checking ()
-typeEq str stuff@(_ny :* _ks :* sems) k exp act = do
-  hopes <- req AskHopeSet
+typeEq str = typeEq' str (Zy :* S0 :* S0)
+
+-- Demand that two things are equal, we're allowed to solve variables in the
+-- hope set to make this true.
+-- Raises a user error if the vals cannot be made equal.
+typeEq' :: String -- String representation of the term for error reporting
+        -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n
+        -> TypeKind -- The kind we're comparing at
+        -> Val n -- Expected
+        -> Val n -- Actual
+        -> Checking ()
+typeEq' str stuff@(_ny :* _ks :* sems) k exp act = do
+  hopes <- req AskHopes
   exp <- sem sems exp
   act <- sem sems act
   typeEqEta str stuff hopes k exp act
@@ -44,59 +52,59 @@ 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
-          -> HopeSet -- The hope set
+          -> Hopes -- A map from the hope set to corresponding FCs
           -> TypeKind -- The kind we're comparing at
           -> Sem -- Expected
           -> Sem -- Actual
           -> Checking ()
-typeEqEta tm (lvy :* kz :* sems) hopeSet (TypeFor m ((_, k):ks)) exp act = do
+typeEqEta tm (lvy :* kz :* sems) hopes (TypeFor m ((_, k):ks)) exp act = do
   -- Higher kinded things
   let nextSem = semLvl lvy
   let xz = B0 :< nextSem
   exp <- applySem exp xz
   act <- applySem act xz
-  typeEqEta tm (Sy lvy :* (kz :<< k) :* (sems :<< nextSem)) hopeSet (TypeFor m ks) exp act
+  typeEqEta tm (Sy lvy :* (kz :<< k) :* (sems :<< nextSem)) hopes (TypeFor m ks) exp act
 -- Not higher kinded - check for flex terms
 -- (We don't solve under binders for now, so we only consider Zy here)
--- "easy" flex cases
-typeEqEta _tm (Zy :* _ks :* _sems) hopeSet k (SApp (SPar e) B0) act
-  | M.member e hopeSet = solveHope k e act
-typeEqEta _tm (Zy :* _ks :* _sems) hopeSet k exp (SApp (SPar e) B0)
-  | M.member e hopeSet = solveHope k e exp
-typeEqEta _ (Zy :* _ :* _) hopeSet Nat exp act
-  | Just (SPar e) <- isNumVar exp, M.member e hopeSet = solveHope Nat e act
-  | Just (SPar e) <- isNumVar act, M.member e hopeSet = solveHope Nat e exp
--- harder cases, neither is in the hopeSet, so we can't define it ourselves
-typeEqEta tm stuff@(ny :* _ks :* _sems) hopeSet k exp act = do
+-- 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
+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
+  | 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
   act <- quote ny act
   let ends = catMaybes $ [exp,act] <&> getEnd
-  unless (not $ any (flip M.member hopeSet) ends) $ typeErr "ends were in hopeset"
+  unless (not $ any (flip M.member hopes) [ie | InEnd ie <- ends]) $ typeErr "ends were in hopeset"
   filterM (isSkolem >=> pure . not) ends >>= \case
     [] -> typeEqRigid tm stuff k exp act -- easyish, both rigid i.e. already defined
     [e1, e2] | e1 == e2 -> pure () -- trivially same, even if they're both still yet-to-be-defined
     es -> -- tricky: must wait for one or other to become more defined
-      mkYield "typeEqEta" (S.fromList es) >> typeEq tm stuff k exp act
+      mkYield "typeEqEta" (S.fromList es) >> typeEq' tm stuff k exp act
  where
   getEnd (VApp (VPar e) _) = Just e
   getEnd (VNum n) = getNumVar n
   getEnd _ = Nothing
 
--- This will update the hopeSet, potentially invalidating things that have been eval'd
+-- This will update the `hopes` set, potentially invalidating things that have
+-- been eval'd.
 -- The Sem is closed, for now.
--- TODO: This needs to update the BRAT graph with the solution.
-solveHope :: TypeKind -> End -> Sem -> Checking ()
-solveHope k e v = quote Zy v >>= \v -> case doesntOccur e v of
-  Right () -> defineEnd e v >> do
+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) -> buildNatVal v
       (Nat, _) -> err $ InternalError "Head of Nat wasn't a VNum"
       _ -> buildConst Unit TUnit
-    let InEnd i = e
-    req $ Wire (end dangling, kindType k, i)
-    pure ()
+    req (Wire (end dangling, kindType k, hope))
+    req (RemoveHope hope)
   Left msg -> case v of
-    VApp (VPar e') B0 | e == e' -> pure ()
+    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.
@@ -104,7 +112,7 @@ solveHope k e v = quote Zy v >>= \v -> case doesntOccur e v of
 
 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
+typeEqs tm stuff (k:ks) (exp:exps) (act:acts) = typeEqs tm stuff ks exps acts <* typeEq' tm stuff k exp act
 typeEqs _ _ _ _ _ = typeErr "arity mismatch"
 
 typeEqRow :: Modey m
@@ -113,11 +121,12 @@ typeEqRow :: Modey m
           -> Ro m lv top0
           -> Ro m lv top1
           -> Either ErrorMsg (Some ((Ny :* Stack Z TypeKind :* Stack Z Sem) -- The new stack of kinds and fresh level
-                                   :* (((:~:) top0) :* ((:~:) top1))) -- Proofs both input rows have same length (quantified over by Some)
+                                   :* ((:~:) top0 :* (:~:) top1)) -- Proofs both input rows have same length (quantified over by Some)
                              ,[Checking ()] -- subproblems to run in parallel
                              )
 typeEqRow _ _ stuff R0 R0 = pure (Some (stuff :* (Refl :* Refl)), [])
-typeEqRow m tm stuff (RPr (_,ty1) ro1) (RPr (_,ty2) ro2) = typeEqRow m tm stuff ro1 ro2 <&> \(res, probs) -> (res, (typeEq tm stuff (kindForMode m) ty1 ty2):probs)
+typeEqRow m tm stuff (RPr (_,ty1) ro1) (RPr (_,ty2) ro2) = typeEqRow m tm stuff ro1 ro2 <&> second
+  ((:) (typeEq' tm stuff (kindForMode m) ty1 ty2))
 typeEqRow m tm (ny :* kz :* semz) (REx (_,k1) ro1) (REx (_,k2) ro2) | k1 == k2 = typeEqRow m tm (Sy ny :* (kz :<< k1) :* (semz :<< semLvl ny)) ro1 ro2
 typeEqRow _ _ _ _ _ = Left $ TypeErr "Mismatched rows"
 
@@ -151,98 +160,11 @@ typeEqRigid tm lvkz (TypeFor m []) (VCon c args) (VCon c' args') | c == c' =
 typeEqRigid tm lvkz (Star []) (VFun m0 (ins0 :->> outs0)) (VFun m1 (ins1 :->> outs1)) | Just Refl <- testEquality m0 m1 = do
   probs :: [Checking ()] <- throwLeft $ typeEqRow m0 tm lvkz ins0 ins1 >>= \case -- this is in Either ErrorMsg
         (Some (lvkz :* (Refl :* Refl)), ps1) -> typeEqRow m0 tm lvkz outs0 outs1 <&> (ps1++) . snd
-  traverse_ id probs -- uses Applicative (unlike sequence_ which uses Monad), hence parallelized
+  sequenceA_ probs -- uses Applicative (unlike sequence_ which uses Monad), hence parallelized
 typeEqRigid tm lvkz (TypeFor _ []) (VSum m0 rs0) (VSum m1 rs1)
   | Just Refl <- testEquality m0 m1 = case zipSameLength rs0 rs1 of
       Nothing -> typeErr "Mismatched sum lengths"
-      Just rs -> traverse eqVariant rs >>= (traverse_ id . concat)
+      Just rs -> traverse eqVariant rs >>= (sequenceA_ . concat)
  where
-  eqVariant (Some r0, Some r1) = throwLeft $ (snd <$> typeEqRow m0 tm lvkz r0 r1)
+  eqVariant (Some r0, Some r1) = throwLeft (snd <$> typeEqRow m0 tm lvkz r0 r1)
 typeEqRigid tm _ _ v0 v1 = err $ TypeMismatch tm (show v0) (show v1)
-
-wire :: (Src, Val Z, Tgt) -> Checking ()
-wire (src, ty, tgt) = req $ Wire (end src, ty, end tgt)
-
-buildNum :: Integer -> Checking Src
-buildNum n = buildConst (Num (fromIntegral n)) TNat
-
-
--- Generate wiring to produce a dynamic instance of the numval argument
-buildNatVal :: NumVal (VVar Z) -> Checking Src
-buildNatVal nv@(NumValue n gro) = case n of
-  0 -> buildGro gro
-  n -> do
-    nDangling <- buildNum n
-    ((lhs,rhs),out) <- buildArithOp Add
-    src <- buildGro gro
-    wire (nDangling, TNat, lhs)
-    wire (src, TNat, rhs)
-    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 0 mono) = buildMono mono
-  buildSM (StrictMono k mono) = do
-    -- Calculate 2^k as `factor`
-    two <- buildNum 2
-    kDangling <- buildNum k
-    ((lhs,rhs),factor) <- buildArithOp Pow
-    wire (two, TNat, lhs)
-    wire (kDangling, TNat, rhs)
-    -- Multiply mono by 2^k
-    ((lhs,rhs),out) <- buildArithOp Mul
-    monoDangling <- buildMono mono
-    wire (factor, TNat, lhs)
-    wire (monoDangling, TNat, rhs)
-    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
-    wire (two, TNat, lhs)
-    wire (dangling, TNat, rhs)
-    -- Then subtract 1
-    one <- buildNum 1
-    ((lhs,rhs),out) <- buildArithOp Sub
-    wire (outPlus1, TNat, lhs)
-    wire (one, TNat, rhs)
-    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
-    wire (upSrc, TNat, rhs)
-    tgt <- invertGro gro
-    wire (out, TNat, 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
-      wire (out, TNat, tgt)
-      wire (divisor, TNat, rhs)
-      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
-    wire (llufSrc, TNat, tgt)
-    pure llufTgt
diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs
index 2640b264..8b76a948 100644
--- a/brat/Brat/Checker/SolvePatterns.hs
+++ b/brat/Brat/Checker/SolvePatterns.hs
@@ -2,7 +2,6 @@ module Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve)
 
 import Brat.Checker.Monad
 import Brat.Checker.Helpers
-import Brat.Checker.SolveHoles (buildNatVal, invertNatVal)
 import Brat.Checker.Types (EndType(..))
 import Brat.Constructors
 import Brat.Constructors.Patterns
@@ -13,7 +12,7 @@ import Brat.Syntax.Abstractor
 import Brat.Syntax.Common
 import Brat.Syntax.Simple
 import Brat.Syntax.Value
-import Brat.UserName
+import Brat.QualName
 import Bwd
 import Control.Monad.Freer
 import Hasochism
@@ -133,7 +132,7 @@ typeOfEnd my e = (req (TypeOf e) <&> fst) >>= \case
 solveConstructor :: EvMode m
                  => Modey m
                  -> Src
-                 -> (UserName, Abstractor)
+                 -> (QualName, Abstractor)
                  -> Val Z
                  -> Problem
                  -> Checking ([(Src, PrimTest (BinderType m))]
@@ -143,7 +142,7 @@ solveConstructor my src (c, abs) ty p = do
   (CArgs pats _ patRo argRo, (tycon, tyargs)) <- lookupConstructor my c ty
   -- Create a row of hypothetical kinds which contextualise the arguments to the
   -- constructor.
-  -- These need to be Tgts because we don't know how to compute them dynamically/
+  -- These need to be Tgts because we don't know how to compute them dynamically
   (_, _, _, stuff) <- next "type_args" Hypo (S0, Some (Zy :* S0)) patRo R0
   (node, _, patArgWires, _) <- let ?my = my in anext "val_args" Hypo stuff R0 argRo
   trackM ("Constructor " ++ show c ++ "; type " ++ show ty)
@@ -208,32 +207,31 @@ instantiateMeta e val = do
 solveNumMeta :: End -> NumVal (VVar Z) -> Checking ()
 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 _)]) -> do
+ (ExEnd src,  [VPar (InEnd _tgt)]) -> do
    -- Compute the value of the `tgt` variable from the known `src` value by inverting nv
    tgtSrc <- invertNatVal nv
-   defineSrc (NamedPort src "") (VNum (nVar (VPar (toEnd tgtSrc))))
+   instantiateMeta (ExEnd src) (VNum (nVar (VPar (toEnd tgtSrc))))
    wire (NamedPort src "", TNat, tgtSrc)
 
- (ExEnd src, _) -> defineSrc (NamedPort src "") (VNum nv)
+ (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))))
-   defineTgt (NamedPort weeTgt "") (VNum (nVar (VPar (toEnd idSrc))))
+   instantiateMeta (InEnd weeTgt) (VNum (nVar (VPar (toEnd idSrc))))
    wire (idSrc, TNat, NamedPort weeTgt "")
-   let nv' = fmap (const (VPar (toEnd idSrc))) nv
+   let nv' = fmap (const (VPar (toEnd idSrc))) nv -- weeTgt is the only thing to replace
    bigSrc <- buildNatVal nv'
-   defineTgt (NamedPort bigTgt "") (VNum nv')
+   instantiateMeta (InEnd bigTgt) (VNum nv')
    wire (bigSrc, TNat, NamedPort bigTgt "")
 
  -- RHS is constant or Src, wire it into tgt
  (InEnd tgt,  _) -> do
    src <- buildNatVal nv
-   defineTgt (NamedPort tgt "") (VNum nv)
+   instantiateMeta (InEnd tgt) (VNum nv)
    wire (src, TNat, NamedPort tgt "")
-
  where
   vars :: NumVal a -> [a]
   vars = foldMap pure
@@ -280,18 +278,22 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro)
   --   2^k * x
   -- = 2^k * (y + 1)
   -- = 2^k + 2^k * y
-  demandSucc (StrictMono _ (Linear (VPar (ExEnd _)))) = error "Todo..." {-do
-    -- This is sus because we don't have any tgt?
-    ySrc <- invertNatVal (NamedPort x "") (NumValue 1 (StrictMonoFun sm))
-    let y = nVar (VPar (toEnd ySrc))
-    solveNumMeta (ExEnd x) (nPlus 1 y)
-    pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k y
-  -}
-
-  demandSucc sm@(StrictMono k (Linear (VPar (InEnd weeEnd)))) = do
-    bigEnd <- invertNatVal (NumValue 1 (StrictMonoFun sm))
-    solveNumMeta (toEnd bigEnd) (NumValue 0 (StrictMonoFun sm))
-    pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k (nVar (VPar (InEnd weeEnd)))
+  demandSucc (StrictMono k (Linear (VPar (ExEnd x)))) = do
+    (_, [(yTgt, _)], [(ySrc, _)], _) <-
+      next "yId" Id (S0, Some (Zy :* S0)) (REx ("value", Nat) R0) (REx ("value", Nat) R0)
+
+    defineSrc ySrc (VNum (nVar (VPar (toEnd yTgt))))
+    instantiateMeta (ExEnd x) (VNum (nPlus 1 (nVar (VPar (toEnd yTgt)))))
+    pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k (nVar (VPar (toEnd ySrc)))
+  --   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 (InEnd x)))) = do
+    (_, [(y,_)], _, _) <- anext "y" Hypo (S0, Some (Zy :* S0)) (REx ("", Nat) R0) R0
+    yPlus1 <- invertNatVal (nPlus 1 (nVar (VPar (toEnd y))))
+    solveNumMeta (InEnd x) (nVar (VPar (toEnd yPlus1)))
+    pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k (nVar (VPar (toEnd y)))
 
   --   2^k * full(n + 1)
   -- = 2^k * (1 + 2 * full(n))
@@ -325,7 +327,8 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro)
     -- 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 _)) -> do
+      -- TODO: Why aren't we using `out`??
+      Linear (VPar (ExEnd _out)) -> do
         -- compute (/2) . (-1)
         doubTgt <- invertNatVal (NumValue 1 (StrictMonoFun (StrictMono 1 mono)))
         let [VPar (InEnd halfTgt)] = foldMap pure mono
@@ -371,17 +374,17 @@ argProblems srcs na p = argProblemsWithLeftovers srcs na p >>= \case
   _ -> err $ UnificationError "Pattern doesn't match expected length for constructor args"
 
 argProblemsWithLeftovers :: [Src] -> NormalisedAbstractor -> Problem -> Checking (Problem, [Src])
-argProblemsWithLeftovers srcs (NA (APull ps abs)) p = pullPorts portName show ps (map (, ()) srcs) >>= \srcs -> argProblemsWithLeftovers (fst <$> srcs) (NA abs) p
+argProblemsWithLeftovers srcs (NA (APull ps abs)) p = pullPorts portName show ps srcs >>= \srcs -> argProblemsWithLeftovers srcs (NA abs) p
 argProblemsWithLeftovers (src:srcs) na p | Just (pat, na) <- unconsNA na = first ((src, pat):) <$> argProblemsWithLeftovers srcs na p
 argProblemsWithLeftovers srcs (NA AEmpty) p = pure (p, srcs)
 argProblemsWithLeftovers [] abst _ = err $ NothingToBind (show abst)
 
 lookupConstructor :: Modey m
-                  -> UserName -- A value constructor
+                  -> QualName -- A value constructor
                   -> Val Z    -- A corresponding type to normalise
                   -- TODO: Something with this m
                   -> Checking (CtorArgs m -- The needed args to the value constructor
-                              ,(UserName, [Val Z])  -- The type constructor we normalised and its args
+                              ,(QualName, [Val Z])  -- The type constructor we normalised and its args
                               )
 lookupConstructor my c ty = eval S0 ty >>= \case
   (VCon tycon args) -> (,(tycon, args)) <$> case my of
diff --git a/brat/Brat/Checker/Types.hs b/brat/Brat/Checker/Types.hs
index 69d2748f..9f37e6a3 100644
--- a/brat/Brat/Checker/Types.hs
+++ b/brat/Brat/Checker/Types.hs
@@ -15,9 +15,9 @@ module Brat.Checker.Types (Overs, Unders
 import Brat.Checker.Quantity
 import Brat.FC (FC)
 import Brat.Naming (Name)
+import Brat.QualName (QualName)
 import Brat.Syntax.Common
 import Brat.Syntax.Value
-import Brat.UserName (UserName)
 import Hasochism (N(..))
 
 import Data.Kind (Type)
@@ -54,7 +54,7 @@ type family EnvData (m :: Mode) where
   EnvData Brat = [(Src, BinderType Brat)]
   EnvData Kernel = (Quantity, (Src, BinderType Kernel))
 
-type Env e = M.Map UserName e
+type Env e = M.Map QualName e
 type VEnv = Env (EnvData Brat)
 type KEnv = Env (EnvData Kernel)
 
diff --git a/brat/Brat/Compile/Hugr.hs b/brat/Brat/Compile/Hugr.hs
index d7199dd6..cf6fbf10 100644
--- a/brat/Brat/Compile/Hugr.hs
+++ b/brat/Brat/Compile/Hugr.hs
@@ -16,11 +16,11 @@ import Brat.Checker.Types (Store(..), VEnv)
 import Brat.Eval (eval, evalCTy, kindType)
 import Brat.Graph hiding (lookupNode)
 import Brat.Naming
+import Brat.QualName
 import Brat.Syntax.Port
 import Brat.Syntax.Common
 import Brat.Syntax.Simple (SimpleTerm)
 import Brat.Syntax.Value
-import Brat.UserName
 import Bwd
 import Control.Monad.Freer
 import Data.Hugr
@@ -491,7 +491,7 @@ compileWithInputs parent name = gets compiled >>= (\case
       addNode "Replicate" (OpCustom (CustomOp parent "BRAT" "Replicate" sig [TAType elemTy]))
     x -> error $ show x ++ " should have been compiled outside of compileNode"
 
-compileConstructor :: NodeId -> UserName -> UserName -> FunctionType -> Compile NodeId
+compileConstructor :: NodeId -> QualName -> QualName -> FunctionType -> Compile NodeId
 compileConstructor parent tycon con sig
   | Just b <- isBool con = do
       -- A boolean value is a tag which takes no inputs and produces an empty tuple
@@ -501,7 +501,7 @@ compileConstructor parent tycon con sig
   | otherwise = let name = "Constructor " ++ show tycon ++ "::" ++ show con in
                   addNode name (constructorOp parent tycon con sig)
  where
-  isBool :: UserName -> Maybe Bool
+  isBool :: QualName -> Maybe Bool
   isBool CFalse = Just False
   isBool CTrue = Just True
   isBool _ = Nothing
@@ -782,7 +782,7 @@ compilePrimTest parent port@(_, ty) (PrimLitTest tm) = do
            [port, loadPort]
            [sumOut]
 
-constructorOp :: NodeId -> UserName -> UserName -> FunctionType -> HugrOp NodeId
+constructorOp :: NodeId -> QualName -> QualName -> FunctionType -> HugrOp NodeId
 constructorOp parent tycon c sig = OpCustom (CustomOp parent "BRAT" ("Ctor::" ++ show tycon ++ "::" ++ show c) sig [])
 
 undoPrimTest :: NodeId
@@ -863,7 +863,7 @@ compileModule venv = do
     addEdge (fst wire, Port output 0)
 
   -- top-level decls that are not Prims. RHS is the brat idNode
-  decls :: [(UserName, Name)]
+  decls :: [(QualName, Name)]
   decls = do -- in list monad, no Compile here
             (fnName, wires) <- M.toList venv
             let (Ex idNode _) = end (fst $ head wires) -- would be better to check same for all rather than just head
diff --git a/brat/Brat/Constructors.hs b/brat/Brat/Constructors.hs
index bd3656fe..16b196bc 100644
--- a/brat/Brat/Constructors.hs
+++ b/brat/Brat/Constructors.hs
@@ -3,9 +3,9 @@ module Brat.Constructors where
 import qualified Data.Map as M
 
 import Brat.Constructors.Patterns
+import Brat.QualName (QualName, plain)
 import Brat.Syntax.Common
 import Brat.Syntax.Value
-import Brat.UserName (UserName, plain)
 import Bwd
 import Hasochism (N(..), Ny(..))
 
@@ -20,8 +20,8 @@ data CtorArgs m where
         -> CtorArgs m
 
 type ConstructorMap m
-  = M.Map UserName  -- The name of a constructor "C"
-    (M.Map UserName -- The name of the type we're checking against "Ty"
+  = M.Map QualName  -- The name of a constructor "C"
+    (M.Map QualName -- The name of the type we're checking against "Ty"
      (CtorArgs m)
     )
 
@@ -125,7 +125,7 @@ kernelConstructors = M.fromList
   ,(CFalse, M.fromList [(CBit, CArgs [] Zy R0 R0)])
   ]
 
-defaultTypeConstructors :: M.Map (Mode, UserName) [(PortName, TypeKind)]
+defaultTypeConstructors :: M.Map (Mode, QualName) [(PortName, TypeKind)]
 defaultTypeConstructors = M.fromList
   [((Brat, COption), [("value", Star [])])
   ,((Brat, CList),   [("listValue", Star [])])
@@ -149,7 +149,7 @@ defaultTypeConstructors = M.fromList
 -- TODO: Make type aliases more flexible. Allow different patterns and allow Nat
 -- kinds. Allow port pulling when applying them
 -- TODO: Aliases for kernel types
-typeAliases :: M.Map UserName (Modey m, [ValPat], BinderType m)
+typeAliases :: M.Map QualName (Modey m, [ValPat], BinderType m)
 typeAliases = M.empty
 {- Here is an example, for `type Vec5(X) = Vec(X, n)`:
 M.fromList $
@@ -160,7 +160,7 @@ M.fromList $
 -}
 -}
 
-natConstructors :: M.Map UserName (Maybe NumPat, NumVal (VVar Z) -> NumVal (VVar Z))
+natConstructors :: M.Map QualName (Maybe NumPat, NumVal (VVar Z) -> NumVal (VVar Z))
 natConstructors = M.fromList
   [(plain "succ", (Just (NP1Plus NPVar)
                   ,nPlus 1))
diff --git a/brat/Brat/Constructors/Patterns.hs b/brat/Brat/Constructors/Patterns.hs
index 40d923a6..1388d159 100644
--- a/brat/Brat/Constructors/Patterns.hs
+++ b/brat/Brat/Constructors/Patterns.hs
@@ -1,9 +1,9 @@
 module Brat.Constructors.Patterns where
 
-import Brat.UserName
+import Brat.QualName
 
 pattern CSucc, CDoub, CNil, CCons, CSome, CNone, CTrue, CFalse, CZero, CSnoc,
-        CConcatEqEven, CConcatEqOdd, CRiffle :: UserName
+        CConcatEqEven, CConcatEqOdd, CRiffle :: QualName
 pattern CSucc = PrefixName [] "succ"
 pattern CDoub = PrefixName [] "doub"
 pattern CNil = PrefixName [] "nil"
@@ -18,7 +18,7 @@ pattern CConcatEqEven = PrefixName [] "concatEqEven"
 pattern CConcatEqOdd = PrefixName [] "concatEqOdd"
 pattern CRiffle = PrefixName [] "riffle"
 
-pattern CList, CVec, CNat, CInt, COption, CBool, CBit, CFloat, CString :: UserName
+pattern CList, CVec, CNat, CInt, COption, CBool, CBit, CFloat, CString :: QualName
 pattern CList = PrefixName [] "List"
 pattern CVec = PrefixName [] "Vec"
 pattern CNat = PrefixName [] "Nat"
@@ -29,6 +29,6 @@ pattern CBit = PrefixName [] "Bit"
 pattern CFloat = PrefixName [] "Float"
 pattern CString = PrefixName [] "String"
 
-pattern CQubit, CMoney :: UserName
+pattern CQubit, CMoney :: QualName
 pattern CQubit = PrefixName [] "Qubit"
 pattern CMoney = PrefixName [] "Money"
diff --git a/brat/Brat/Error.hs b/brat/Brat/Error.hs
index 9ec092cc..fc8a841f 100644
--- a/brat/Brat/Error.hs
+++ b/brat/Brat/Error.hs
@@ -9,6 +9,7 @@ module Brat.Error (ParseError(..)
                   ) where
 
 import Brat.FC
+import Brat.Syntax.Port (PortName)
 
 import Data.List (intercalate)
 import System.Exit
@@ -60,8 +61,8 @@ data ErrorMsg
  | FileNotFound String [String]
  | SymbolNotFound String String
  | InternalError String
- | AmbiguousPortPull String String
- | BadPortPull String
+ | AmbiguousPortPull PortName String
+ | BadPortPull PortName String
  | VConNotFound String
  | TyConNotFound String String
  | MatchingOnTypes
@@ -78,11 +79,11 @@ data ErrorMsg
  | UnreachableBranch
  | UnrecognisedTypeCon String
  | WrongModeForType String
- | RemainingNatHopes [String]
  -- For thunks which don't address enough inputs, or produce enough outputs.
  -- The argument is the row of unused connectors
  | ThunkLeftOvers String
  | ThunkLeftUnders String
+ | RemainingNatHopes [String]
 
 instance Show ErrorMsg where
   show (TypeErr x) = "Type error: " ++ x
@@ -140,7 +141,7 @@ instance Show ErrorMsg where
   show (SymbolNotFound s i) = "Symbol `" ++ s ++ "` not found in `" ++ i ++ "`"
   show (InternalError x) = "Internal error: " ++ x
   show (AmbiguousPortPull p row) = "Port " ++ p ++ " is ambiguous in " ++ row
-  show (BadPortPull x) = "Port " ++ x ++ " can't be pulled because it depends on a previous port"
+  show (BadPortPull p row) = "Port not found: " ++ p ++ " in " ++ row
   show (VConNotFound x) = "Value constructor not recognised: " ++ x
   show (TyConNotFound ty v) = show v ++ " is not a valid constructor for type " ++ ty
   show MatchingOnTypes = "Trying to pattern match on a type"
@@ -164,11 +165,9 @@ instance Show ErrorMsg where
   -- TODO: Make all of these use existing errors
   show (UnificationError str) = "Unification error: " ++ str
   show UnreachableBranch = "Branch cannot be reached"
-  show (RemainingNatHopes hs) = unlines ("Expected to work out values for these holes:":indent (indent hs))
   show (ThunkLeftOvers overs) = "Expected function to address all inputs, but " ++ overs ++ " wasn't used"
   show (ThunkLeftUnders unders) = "Expected function to return additional values of type: " ++ unders
-
-indent = fmap ("  " ++)
+  show (RemainingNatHopes hs) = unlines ("Expected to work out values for these holes:":(("    " ++) <$> hs))
 
 data Error = Err { fc  :: Maybe FC
                  , msg :: ErrorMsg
diff --git a/brat/Brat/Eval.hs b/brat/Brat/Eval.hs
index f65f67b8..ed2b3574 100644
--- a/brat/Brat/Eval.hs
+++ b/brat/Brat/Eval.hs
@@ -23,9 +23,9 @@ module Brat.Eval (EvMode(..)
 import Brat.Checker.Monad
 import Brat.Checker.Types (EndType(..), kindForMode)
 import Brat.Error (ErrorMsg(..))
+import Brat.QualName (plain)
 import Brat.Syntax.Common
 import Brat.Syntax.Value
-import Brat.UserName (plain)
 import Control.Monad.Freer
 import Bwd
 import Hasochism
@@ -257,10 +257,7 @@ eqWorker tm lvkz (TypeFor _ []) (SSum m0 stk0 rs0) (SSum m1 stk1 rs1)
       Just rs -> traverse eqVariant rs <&> sequence_
  where
   eqVariant (Some r0, Some r1) = eqRowTest m0 tm lvkz (stk0,r0) (stk1,r1) <&> dropRight
-eqWorker tm _ _ s0 s1 = do
-  v0 <- quote Zy s0
-  v1 <- quote Zy s1
-  pure . Left $ TypeMismatch tm (show v0) (show v1)
+eqWorker tm _ _ v0 v1 = pure . Left $ TypeMismatch tm (show v0) (show v1)
 
 -- Type rows have bot0,bot1 dangling de Bruijn indices, which we instantiate with
 -- de Bruijn levels. As we go under binders in these rows, we add to the scope's
diff --git a/brat/Brat/Graph.hs b/brat/Brat/Graph.hs
index e4d7a787..62c4619b 100644
--- a/brat/Brat/Graph.hs
+++ b/brat/Brat/Graph.hs
@@ -3,10 +3,10 @@
 module Brat.Graph where
 
 import Brat.Naming
+import Brat.QualName
 import Brat.Syntax.Common
 import Brat.Syntax.Simple
 import Brat.Syntax.Value
-import Brat.UserName
 
 import Hasochism (N(..))
 
@@ -46,8 +46,8 @@ data NodeType :: Mode -> Type where
                   )
                -> NodeType a
   Hypo :: NodeType a  -- Hypothesis for type checking
-  Constructor :: UserName -> NodeType a
-  Selector :: UserName -> NodeType a -- TODO: Get rid of this in favour of pattern matching
+  Constructor :: QualName -> NodeType a
+  Selector :: QualName -> NodeType a -- TODO: Get rid of this in favour of pattern matching
   ArithNode :: ArithOp -> NodeType Brat
   Replicate :: NodeType Brat
   MapFun :: NodeType a
@@ -77,8 +77,8 @@ deriving instance Show ty => Show (MatchSequence ty)
 
 data PrimTest ty
   = PrimCtorTest
-      UserName      -- the data constructor
-      UserName      -- the type constructor
+      QualName      -- the data constructor
+      QualName      -- the type constructor
       -- (CtorArgs m)  -- (hope we don't need) its entry in the constructor table
       Name          -- the name of the node which "outputs" the data packed inside
       [(Src, ty)]  -- ...these sources for extracted data descend
diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs
index aff2d736..73449f50 100644
--- a/brat/Brat/Load.hs
+++ b/brat/Brat/Load.hs
@@ -20,7 +20,7 @@ import Brat.Syntax.Core
 import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..), Locality(..))
 import Brat.Syntax.Raw
 import Brat.Syntax.Value
-import Brat.UserName
+import Brat.QualName
 import Util (duplicates,duplicatesWith)
 import Hasochism
 
@@ -47,7 +47,7 @@ type FlatMod = ((FEnv, String) -- data at the node: declarations, and file conte
 
 -- Result of checking/compiling a module
 type VMod = (VEnv
-            ,[(UserName, VDecl)] -- all symbols from all modules
+            ,[(QualName, VDecl)] -- all symbols from all modules
             ,[TypedHole]          -- for just the last module
             ,Store  -- Ends declared & defined in the module
             ,Graph  -- all functions in this module, nodes identified from first VEnv
@@ -115,9 +115,9 @@ checkDecl pre (VDecl FuncDecl{..}) to_define = (fnName -!) $ localFC fnLoc $ do
   uname = PrefixName pre fnName
   name = show uname
 
-loadAlias :: TypeAlias -> Checking (UserName, Alias)
+loadAlias :: TypeAlias -> Checking (QualName, Alias)
 loadAlias (TypeAlias fc name args body) = localFC fc $ do
-  (_, [(hhungry, Left k)], _, _) <- next "" Hypo (S0,Some (Zy :* S0)) (REx ("type", Star args) R0) R0
+  (_, [(hhungry, Left k)], _, _) <- next "load_alias" Hypo (S0,Some (Zy :* S0)) (REx ("type", Star args) R0) R0
   let abs = WC fc $ foldr ((:||:) . APat . Bind . fst) AEmpty args
   ([v], unders) <- kindCheck [(hhungry, k)] $ Th (WC fc (Lambda (abs, WC fc body) []))
   ensureEmpty "loadAlias unders" unders
@@ -127,7 +127,7 @@ withAliases :: [TypeAlias] -> Checking a -> Checking a
 withAliases [] m = m
 withAliases (a:as) m = loadAlias a >>= \a -> localAlias a $ withAliases as m
 
-loadStmtsWithEnv :: Namespace -> (VEnv, [(UserName, VDecl)], Store) -> (FilePath, Prefix, FEnv, String) -> Either SrcErr VMod
+loadStmtsWithEnv :: Namespace -> (VEnv, [(QualName, VDecl)], Store) -> (FilePath, Prefix, FEnv, String) -> Either SrcErr VMod
 loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addSrcContext fname cts $ do
   -- hacky mess - cleanup!
   (decls, aliases) <- desugarEnv =<< elabEnv stmts
@@ -169,9 +169,9 @@ loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addS
     pure $ assert (M.null remaining) () -- all to_defines were defined
   pure (venv, oldDecls <> vdecls, holes, oldEndData <> newEndData, kcGraph <> graph, capSets)
  where
-  checkDecl' :: M.Map UserName [(Tgt, BinderType Brat)]
-             -> (UserName, VDecl)
-             -> Checking (M.Map UserName [(Tgt, BinderType Brat)])
+  checkDecl' :: M.Map QualName [(Tgt, BinderType Brat)]
+             -> (QualName, VDecl)
+             -> Checking (M.Map QualName [(Tgt, BinderType Brat)])
   checkDecl' to_define (name, decl) =
     -- Get the decl out of the map, and delete it from things to define
     case M.updateLookupWithKey (\_ _ -> Nothing) name to_define of
@@ -237,7 +237,7 @@ loadFiles ns (cwd :| extraDirs) fname contents = do
         cts <- lift $ readFile file
         depGraph visited' imp' cts
 
-    getStmts :: ((FEnv, String), Import, [Import]) -> (UserName, Prefix, FEnv, String)
+    getStmts :: ((FEnv, String), Import, [Import]) -> (QualName, Prefix, FEnv, String)
     getStmts (((decls, ts), cts), Import (WC _ pn@(PrefixName ps name)) qual alias sel, _) =
       let prefix = case (qual, alias) of (True, Nothing) -> ps ++ [name]
                                          (False, Nothing) -> []
@@ -262,13 +262,13 @@ loadFiles ns (cwd :| extraDirs) fname contents = do
         (WC fc dupl:_) -> throwError $ Err (Just fc) (NameClash ("Alias not unique: " ++ show dupl))
         [] -> pure ()
 
-    findFile :: UserName -> ExceptT SrcErr IO String
+    findFile :: QualName -> ExceptT SrcErr IO String
     findFile uname = let possibleLocations = [nameToFile dir uname | dir <- cwd:extraDirs] in
                        filterM (lift . doesFileExist) possibleLocations >>= \case
       [] -> throwError $ addSrcName (show uname) $ dumbErr (FileNotFound (show uname) possibleLocations)
       (x:_) -> pure x
 
-    nameToFile :: FilePath -> UserName -> String
+    nameToFile :: FilePath -> QualName -> String
     nameToFile dir (PrefixName ps file) = dir </> foldr (</>) file ps ++ ".brat"
 
 checkNoCycles :: [(Int, FlatMod)] -> Either SrcErr ()
diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs
index 1f546055..91e78339 100644
--- a/brat/Brat/Parser.hs
+++ b/brat/Brat/Parser.hs
@@ -6,6 +6,7 @@ import Brat.FC
 import Brat.Lexer (lex)
 import Brat.Lexer.Token (Keyword(..), Token(..), Tok(..))
 import qualified Brat.Lexer.Token as Lexer
+import Brat.QualName ( plain, QualName(..) )
 import Brat.Syntax.Abstractor
 import Brat.Syntax.Common hiding (end)
 import qualified Brat.Syntax.Common as Syntax
@@ -13,7 +14,6 @@ import Brat.Syntax.FuncDecl (FuncDecl(..), Locality(..))
 import Brat.Syntax.Concrete
 import Brat.Syntax.Raw
 import Brat.Syntax.Simple
-import Brat.UserName ( plain, UserName(..) )
 import Brat.Elaborator
 import Util ((**^))
 
@@ -84,13 +84,15 @@ simpleName = token0 $ \case
   Ident str -> Just str
   _ -> Nothing
 
-qualifiedName :: Parser UserName
-qualifiedName = (<?> "qualified name") . token0 $ \case
-  QualifiedId prefix str -> Just (PrefixName (toList prefix) str)
-  _ -> Nothing
+qualName :: Parser QualName
+qualName = (<?> "name") $ try qualifiedName <|> (PrefixName [] <$> simpleName)
+ where
+  qualifiedName :: Parser QualName
+  qualifiedName = (<?> "qualified name") . token0 $ \case
+    QualifiedId prefix str -> Just (PrefixName (toList prefix) str)
+    _ -> Nothing
+
 
-userName :: Parser UserName
-userName = (<?> "name") $ try qualifiedName <|> (PrefixName [] <$> simpleName)
 
 round :: Parser a -> Parser a
 round p = label "(...)" $ match LParen *> p <* match RParen
@@ -125,7 +127,7 @@ string = token0 $ \case
   _ -> Nothing
 
 var :: Parser Flat
-var = FVar <$> userName
+var = FVar <$> qualName
 
 port = simpleName
 
@@ -514,6 +516,7 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr]
               <|> match Underscore $> FUnderscore
               <|> match Bang $> FHope
               <|> match Pipe $> FIdentity
+              <|> match Bang $> FHope
 
 
 cnoun :: Parser Flat -> Parser (WC (Raw 'Chk 'Noun))
@@ -610,7 +613,7 @@ pimport :: Parser Import
 pimport = do
   o <- open
   kmatch KImport
-  x <- withFC userName
+  x <- withFC qualName
   a <- alias
   Import x (not o) a <$> selection
  where
@@ -644,10 +647,10 @@ pstmt = ((comment <?> "comment")                 <&> \_ -> ([] , []))
   alias = withFC aliasContents <&>
           \(WC fc (name, args, ty)) -> TypeAlias fc name args ty
 
-  aliasContents :: Parser (UserName, [(String, TypeKind)], RawVType)
+  aliasContents :: Parser (QualName, [(String, TypeKind)], RawVType)
   aliasContents = do
     match (K KType)
-    alias <- userName
+    alias <- qualName
     args <- option [] $ round (simpleName `sepBy` match Comma)
 {- future stuff
     args <- option [] $ round $ (`sepBy` (match Comma)) $ do
diff --git a/brat/Brat/UserName.hs b/brat/Brat/QualName.hs
similarity index 56%
rename from brat/Brat/UserName.hs
rename to brat/Brat/QualName.hs
index 88ec5093..dca5df22 100644
--- a/brat/Brat/UserName.hs
+++ b/brat/Brat/QualName.hs
@@ -1,15 +1,14 @@
-module Brat.UserName where
+module Brat.QualName where
 
 import Data.List (intercalate)
 
 type Prefix = [String]
 
-data UserName
-  = PrefixName Prefix String
+data QualName = PrefixName Prefix String
   deriving (Eq, Ord)
 
-instance Show UserName where
+instance Show QualName where
   show (PrefixName ps file) = intercalate "." (ps ++ [file])
 
-plain :: String -> UserName
+plain :: String -> QualName
 plain = PrefixName []
diff --git a/brat/Brat/Search.hs b/brat/Brat/Search.hs
index 94254ef8..96dbbc42 100644
--- a/brat/Brat/Search.hs
+++ b/brat/Brat/Search.hs
@@ -2,11 +2,11 @@ module Brat.Search (vsearch) where
 
 import Brat.Constructors (CtorArgs(..), defaultConstructors)
 import Brat.FC
+import Brat.QualName
 import Brat.Syntax.Core
 import Brat.Syntax.Common
 import Brat.Syntax.Value
 import Brat.Syntax.Simple
-import Brat.UserName
 import Hasochism
 
 import Control.Monad (guard)
diff --git a/brat/Brat/Syntax/Abstractor.hs b/brat/Brat/Syntax/Abstractor.hs
index 91e96d35..c89e8a83 100644
--- a/brat/Brat/Syntax/Abstractor.hs
+++ b/brat/Brat/Syntax/Abstractor.hs
@@ -1,13 +1,13 @@
 module Brat.Syntax.Abstractor where
 
+import Brat.QualName
 import Brat.Syntax.Port
 import Brat.Syntax.Simple
-import Brat.UserName
 
 -- Ways to bind one thing
 data Pattern
  = Bind String
- | PCon UserName Abstractor
+ | PCon QualName Abstractor
  | Lit SimpleTerm
  | DontCare
  deriving Eq
diff --git a/brat/Brat/Syntax/Common.hs b/brat/Brat/Syntax/Common.hs
index 067728c5..1cc09503 100644
--- a/brat/Brat/Syntax/Common.hs
+++ b/brat/Brat/Syntax/Common.hs
@@ -41,9 +41,9 @@ module Brat.Syntax.Common (PortName,
                           ) where
 
 import Brat.FC
+import Brat.QualName
 import Brat.Syntax.Abstractor
 import Brat.Syntax.Port
-import Brat.UserName
 
 import Data.Bifunctor (first)
 import Data.List (intercalate)
@@ -164,7 +164,7 @@ instance Semigroup (CType' (PortName, ty)) where
   (ss :-> ts) <> (us :-> vs) = (ss <> us) :-> (ts <> vs)
 
 data Import
-  = Import { importName :: WC UserName
+  = Import { importName :: WC QualName
            , importQualified :: Bool
            , importAlias :: Maybe (WC String)
            , importSelection :: ImportSelection
diff --git a/brat/Brat/Syntax/Concrete.hs b/brat/Brat/Syntax/Concrete.hs
index 3a28d926..3e07bb44 100644
--- a/brat/Brat/Syntax/Concrete.hs
+++ b/brat/Brat/Syntax/Concrete.hs
@@ -3,11 +3,11 @@ module Brat.Syntax.Concrete where
 import Data.List.NonEmpty
 
 import Brat.FC
+import Brat.QualName
 import Brat.Syntax.Common
 import Brat.Syntax.FuncDecl (FuncDecl(..))
 import Brat.Syntax.Raw
 import Brat.Syntax.Simple
-import Brat.UserName
 
 data FBody
   = FClauses (NonEmpty (WC Abstractor, WC Flat))
@@ -21,7 +21,7 @@ type FEnv = ([FDecl], [RawAlias])
 
 
 data Flat
- = FVar UserName
+ = FVar QualName
  | FHope
  | FApp (WC Flat) (WC Flat)
  | FJuxt (WC Flat) (WC Flat)
@@ -36,7 +36,7 @@ data Flat
  | FLetIn (WC Abstractor) (WC Flat) (WC Flat)
  | FSimple SimpleTerm
  | FHole String
- | FCon UserName (WC Flat)
+ | FCon QualName (WC Flat)
  | FEmpty
  | FPull [PortName] (WC Flat)
  -- We can get away with not elaborating type signatures in the short term
diff --git a/brat/Brat/Syntax/Core.hs b/brat/Brat/Syntax/Core.hs
index e6e9908a..c9dbd046 100644
--- a/brat/Brat/Syntax/Core.hs
+++ b/brat/Brat/Syntax/Core.hs
@@ -15,10 +15,10 @@ import Brat.Constructors.Patterns (pattern CCons,
                                    pattern CRiffle)
 import Brat.FC
 import Brat.Naming
+import Brat.QualName
 import Brat.Syntax.Common
 import Brat.Syntax.FuncDecl
 import Brat.Syntax.Simple
-import Brat.UserName
 
 import Data.Kind (Type)
 import Data.Maybe (fromJust)
@@ -47,9 +47,9 @@ data Term :: Dir -> Kind -> Type where
   Emb      :: WC (Term Syn k) -> Term Chk k
   Forget   :: WC (Term d KVerb) -> Term d UVerb
   Pull     :: [PortName] -> WC (Term Chk k) -> Term Chk k
-  Var      :: UserName -> Term Syn Noun  -- Look up in noun (value) env
-  Hope     :: Term Chk Noun
+  Var      :: QualName -> Term Syn Noun  -- Look up in noun (value) env
   Identity :: Term Syn UVerb
+  Hope     :: Term Chk Noun
   Arith    :: ArithOp -> WC (Term Chk Noun) -> WC (Term Chk Noun) -> Term Chk Noun
   Of       :: WC (Term Chk Noun) -> WC (Term d Noun) -> Term d Noun
 
@@ -65,7 +65,7 @@ data Term :: Dir -> Kind -> Type where
   -- In `Syn`, for now, the first clause provides the type.
   Lambda   :: (WC Abstractor, WC (Term d Noun)) -> [(WC Abstractor, WC (Term Chk Noun))] -> Term d UVerb
   -- Type constructors
-  Con      :: UserName -> WC (Term Chk Noun) -> Term Chk Noun
+  Con      :: QualName -> WC (Term Chk Noun) -> Term Chk Noun
   -- Brat function types
   C        :: CType' (PortName, KindOr (Term Chk Noun)) -> Term Chk Noun
   -- Kernel types
@@ -114,9 +114,10 @@ instance Show (Term d k) where
                           ,"of"
                           ,bracket POf e
                           ]
+
   show (Var x) = show x
-  show Hope = "!"
   show Identity = "|"
+  show Hope = "!"
   -- Nested applications should be bracketed too, hence 4 instead of 3
   show (fun :$: arg) = bracket PApp fun ++ ('(' : show arg ++ ")")
   show (tm ::: ty) = bracket PAnn tm ++ " :: " ++ show ty
diff --git a/brat/Brat/Syntax/Raw.hs b/brat/Brat/Syntax/Raw.hs
index ed2b22ce..62934f1b 100644
--- a/brat/Brat/Syntax/Raw.hs
+++ b/brat/Brat/Syntax/Raw.hs
@@ -18,11 +18,11 @@ import Brat.Constructors
 import Brat.Error
 import Brat.FC hiding (end)
 import Brat.Naming
+import Brat.QualName
 import Brat.Syntax.Common
 import Brat.Syntax.Core
 import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..))
 import Brat.Syntax.Simple
-import Brat.UserName
 import Util (names, (**^))
 
 type family TypeOf (k :: Kind) :: Type where
@@ -36,11 +36,11 @@ type RawIO = TypeRowElem (KindOr RawVType)
 type RawCType = CType' RawIO
 type RawKType = CType' (TypeRowElem RawVType)
 
-data TypeAliasF tm = TypeAlias FC UserName [(PortName,TypeKind)] tm deriving Show
+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 UserName TypeAlias
+type TypeAliasTable = M.Map QualName TypeAlias
 
 type RawEnv = ([RawFuncDecl], [RawAlias], TypeAliasTable)
 type RawFuncDecl = FuncDecl [RawIO] (FunBody Raw Noun)
@@ -69,16 +69,16 @@ data Raw :: Dir -> Kind -> Type where
   REmb      :: WC (Raw Syn k) -> Raw Chk k
   RForget   :: WC (Raw d KVerb) -> Raw d UVerb
   RPull     :: [PortName] -> WC (Raw Chk k) -> Raw Chk k
-  RVar      :: UserName -> Raw Syn Noun
-  RHope     :: Raw Chk Noun
+  RVar      :: QualName -> Raw Syn Noun
   RIdentity :: Raw Syn UVerb
+  RHope     :: Raw Chk Noun
   RArith    :: ArithOp -> WC (Raw Chk Noun) -> WC (Raw Chk Noun) -> Raw Chk Noun
   ROf       :: WC (Raw Chk Noun) -> WC (Raw d Noun) -> Raw d Noun
   (:::::)   :: WC (Raw Chk Noun) -> [RawIO] -> Raw Syn Noun
   (::-::)   :: WC (Raw Syn k) -> WC (Raw d UVerb) -> Raw d k -- vertical juxtaposition (diagrammatic composition)
   (::$::)   :: WC (Raw d KVerb) -> WC (Raw Chk k) -> Raw d k -- Eval with ChkRaw n argument
   RLambda   :: (WC Abstractor, WC (Raw d Noun)) -> [(WC Abstractor, WC (Raw Chk Noun))] -> Raw d UVerb
-  RCon      :: UserName -> WC (Raw Chk Noun) -> Raw Chk Noun
+  RCon      :: QualName -> WC (Raw Chk Noun) -> Raw Chk Noun
   -- Function types
   RFn       :: RawCType -> Raw Chk Noun
   -- Kernel types
@@ -132,7 +132,7 @@ instance Show (Raw d k) where
   show RFanIn = "[\\/]"
   show (ROf n e) = "(" ++ show n ++ " of " ++ show e ++ ")"
 
-type Desugar = StateT Namespace (ReaderT (RawEnv, Bwd UserName) (Except Error))
+type Desugar = StateT Namespace (ReaderT (RawEnv, Bwd QualName) (Except Error))
 
 -- instance {-# OVERLAPPING #-} MonadFail Desugar where
 instance {-# OVERLAPPING #-} MonadFail Desugar where
@@ -152,13 +152,13 @@ splitM s = do
   put newRoot
   pure ns'
 
-isConstructor :: UserName -> Desugar Bool
+isConstructor :: QualName -> Desugar Bool
 isConstructor c = pure (c `member` defaultConstructors
                         || (Brat, c) `member` defaultTypeConstructors
                         || (Kernel, c) `member` defaultTypeConstructors
                         || c `member` natConstructors)
 
-isAlias :: UserName -> Desugar Bool
+isAlias :: QualName -> Desugar Bool
 isAlias name = do
   aliases <- asks (thd3 . fst)
   pure $ M.member name aliases
@@ -262,7 +262,7 @@ instance Desugarable (CType' (TypeRowElem RawVType)) where
     ts <- traverse desugar' (addNames ts)
     pure (ss :-> ts)
 
-isConOrAlias :: UserName -> Desugar Bool
+isConOrAlias :: QualName -> Desugar Bool
 isConOrAlias c = do
   con <- isConstructor c
   ali <- isAlias c
diff --git a/brat/Brat/Syntax/Value.hs b/brat/Brat/Syntax/Value.hs
index ba943289..20b7c54b 100644
--- a/brat/Brat/Syntax/Value.hs
+++ b/brat/Brat/Syntax/Value.hs
@@ -23,10 +23,10 @@ module Brat.Syntax.Value {-(VDecl
                          )-} where
 
 import Brat.Error
+import Brat.QualName
 import Brat.Syntax.Common
 import Brat.Syntax.Core (Term (..))
 import Brat.Syntax.FuncDecl (FunBody, FuncDecl(..))
-import Brat.UserName
 import Bwd
 import Hasochism
 
@@ -154,7 +154,7 @@ instance Eq (VVar n) where
 -- Contains Inx's up to n-1, no Lvl's
 data Val :: N -> Type where
   VNum :: NumVal (VVar n) -> Val n
-  VCon :: UserName -> [Val n] -> Val n
+  VCon :: QualName -> [Val n] -> Val n
   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
@@ -166,7 +166,7 @@ data SVar = SPar End | SLvl Int
 -- Semantic value, used internally by normalization; contains Lvl's but no Inx's
 data Sem where
   SNum :: NumVal SVar -> Sem
-  SCon :: UserName -> [Sem] -> Sem
+  SCon :: QualName -> [Sem] -> Sem
   -- Second is just body, we do NOT substitute under the binder,
   -- instead we stash Sem's for each free DeBruijn index into the first member:
   SLam :: Stack Z Sem n -> Val (S n) -> Sem
@@ -401,7 +401,7 @@ instance EvenOrOdd Monotone where
 
 data ValPat
  = VPVar
- | VPCon UserName [ValPat]
+ | VPCon QualName [ValPat]
  | VPNum NumPat
  deriving Show
 
diff --git a/brat/Brat/Unelaborator.hs b/brat/Brat/Unelaborator.hs
index 51d85041..5ff57492 100644
--- a/brat/Brat/Unelaborator.hs
+++ b/brat/Brat/Unelaborator.hs
@@ -38,6 +38,7 @@ 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 _ _ Identity = FIdentity
+unelab _ _ Hope = FHope
 unelab _ _ FanIn = FFanIn
 unelab _ _ FanOut = FFanOut
 
@@ -67,6 +68,7 @@ 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 Identity = RIdentity
+toRaw Hope = RHope
 toRaw FanIn = RFanIn
 toRaw FanOut = RFanOut
 
diff --git a/brat/brat.cabal b/brat/brat.cabal
index 424ae447..a7d22664 100644
--- a/brat/brat.cabal
+++ b/brat/brat.cabal
@@ -78,12 +78,12 @@ library
                        Brat.Parser,
                        Brat.Search,
                        Brat.Elaborator,
+                       Brat.QualName,
                        Brat.Syntax.Abstractor,
                        Brat.Syntax.Concrete,
                        Brat.Syntax.FuncDecl,
                        Brat.Syntax.Port,
                        Brat.Syntax.Simple,
-                       Brat.UserName,
                        Bwd,
                        Control.Monad.Freer,
                        Data.Hugr,
diff --git a/brat/examples/infer.brat b/brat/examples/infer.brat
index c0996697..fd87dcfc 100644
--- a/brat/examples/infer.brat
+++ b/brat/examples/infer.brat
@@ -15,4 +15,4 @@ repeat(_, succ(_), x) = x ,- repeat(!, !, x) -- X can be inferred from x but n c
 
 mapFirst(X :: *, Y :: *, { X -> Y}, n :: #, Vec(X, n)) -> Vec(Y, n)
 mapFirst(_, _, _, _, []) = []
-mapFirst(_, _, f, succ(_), x ,- _) = repeat(!, !, f(x)) -- first ! (X) is second _ (Y)
\ No newline at end of file
+mapFirst(_, _, f, succ(_), x ,- _) = repeat(!, !, f(x)) -- first ! (X) is second _ (Y)
diff --git a/brat/examples/unified.brat b/brat/examples/unified.brat
index f04c167a..cabab3e0 100644
--- a/brat/examples/unified.brat
+++ b/brat/examples/unified.brat
@@ -28,3 +28,10 @@ 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(_, n, xsl =, x ,= xsr) = xsl =, x ,= xsr
+
+-- 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/Main.hs b/brat/test/Main.hs
index ca8f4b88..84a659af 100644
--- a/brat/test/Main.hs
+++ b/brat/test/Main.hs
@@ -18,7 +18,7 @@ import Test.TypeArith
 import Brat.Checker.Monad
 import Brat.Syntax.Common
 import Brat.Syntax.Value
-import Brat.UserName
+import Brat.QualName
 import Brat.Error
 import Control.Monad.Freer
 import qualified Data.Set as S
diff --git a/brat/test/Test/Compile/Hugr.hs b/brat/test/Test/Compile/Hugr.hs
index 11de7093..ef24aa26 100644
--- a/brat/test/Test/Compile/Hugr.hs
+++ b/brat/test/Test/Compile/Hugr.hs
@@ -38,6 +38,7 @@ nonCompilingExamples = expectedCheckingFails ++ expectedParsingFails ++
   ,"fanout" -- Contains Selectors
   ,"vectorise" -- Generates MapFun nodes which aren't implemented yet
   ,"batcher-merge-sort" -- Generates MapFun nodes which aren't implemented yet
+  ,"infer" -- Generates `Pow` nodes which aren't implemented yet
   -- Victims of #13
   ,"arith"
   ,"cqcconf"
diff --git a/brat/test/Test/Elaboration.hs b/brat/test/Test/Elaboration.hs
index 0b9ab7e3..ac6d4f1f 100644
--- a/brat/test/Test/Elaboration.hs
+++ b/brat/test/Test/Elaboration.hs
@@ -2,7 +2,7 @@ module Test.Elaboration (elaborationTests) where
 
 import Brat.Elaborator
 import Brat.Error (showError)
-import Brat.UserName (plain)
+import Brat.QualName (plain)
 import Brat.Syntax.Concrete
 import Brat.Syntax.Common
 import Brat.Syntax.Raw (kind, dir)
diff --git a/brat/test/Test/Substitution.hs b/brat/test/Test/Substitution.hs
index 7d50c86f..25aaed93 100644
--- a/brat/test/Test/Substitution.hs
+++ b/brat/test/Test/Substitution.hs
@@ -9,9 +9,9 @@ import Brat.Checker.SolveHoles
 import Brat.Checker.Types
 import Brat.Error
 import Brat.Naming
+import Brat.QualName
 import Brat.Syntax.Common
 import Brat.Syntax.Value
-import Brat.UserName
 import Bwd
 import Control.Monad.Freer
 import Hasochism
diff --git a/brat/test/Test/Syntax/Let.hs b/brat/test/Test/Syntax/Let.hs
index 7fe336e5..bd748872 100644
--- a/brat/test/Test/Syntax/Let.hs
+++ b/brat/test/Test/Syntax/Let.hs
@@ -5,17 +5,17 @@ module Test.Syntax.Let where
 import Brat.Error (showError)
 import Brat.Checker
 import Brat.FC
+import Brat.QualName
 import Brat.Syntax.Common
 import Brat.Syntax.Core
 import Brat.Syntax.Simple
 import Brat.Syntax.Value
-import Brat.UserName
 import Test.Util (runEmpty)
 
 import Data.String
 import Test.Tasty.HUnit
 
-instance IsString UserName where
+instance IsString QualName where
   fromString = PrefixName []
 
 instance IsString Abstractor where
diff --git a/brat/test/golden/error/remaining_hopes.brat b/brat/test/golden/error/remaining_hopes.brat
new file mode 100644
index 00000000..164b8190
--- /dev/null
+++ b/brat/test/golden/error/remaining_hopes.brat
@@ -0,0 +1,5 @@
+f(n :: #) -> Nat
+f(n) = n
+
+g :: Nat
+g = f(!)
diff --git a/brat/test/golden/error/remaining_hopes.brat.golden b/brat/test/golden/error/remaining_hopes.brat.golden
new file mode 100644
index 00000000..80d15436
--- /dev/null
+++ b/brat/test/golden/error/remaining_hopes.brat.golden
@@ -0,0 +1,8 @@
+Error in test/golden/error/remaining_hopes.brat on line 5:
+g = f(!)
+     ^^^
+
+  Expected to work out values for these holes:
+    In checking_check_defs_1_g_1_Eval 0
+
+
diff --git a/brat/test/golden/graph/addN.brat.graph b/brat/test/golden/graph/addN.brat.graph
index b653f383..31b411ac 100644
--- a/brat/test/golden/graph/addN.brat.graph
+++ b/brat/test/golden/graph/addN.brat.graph
@@ -1,6 +1,6 @@
 Nodes:
 (check_defs_1_addN_addN.box_2_lambda_11,BratNode (PatternMatch ((TestMatchData Braty (MatchSequence {matchInputs = [(NamedPort {end = Ex check_defs_1_addN_addN.box_2_lambda.0_setup/in_3 0, portName = "inp"},Int)], matchTests = [], matchOutputs = [(NamedPort {end = Ex check_defs_1_addN_addN.box_2_lambda.0_setup/in_3 0, portName = "inp"},Int)]}),check_defs_1_addN_addN.box_2_lambda.0_rhs_thunk_10) :| [])) [("inp",Int)] [("out",Int)])
-(check_defs_1_addN_addN.box_2_lambda.0_rhs_9_,BratNode (Eval (Ex globals_prim_8_add 0)) [("a",Int),("b",Int)] [("c",Int)])
+(check_defs_1_addN_addN.box_2_lambda.0_rhs_9_Eval,BratNode (Eval (Ex globals_prim_8_add 0)) [("a",Int),("b",Int)] [("c",Int)])
 (check_defs_1_addN_addN.box_2_lambda.0_rhs/in_7,BratNode Source [] [("n",Int)])
 (check_defs_1_addN_addN.box_2_lambda.0_rhs/out_8,BratNode Target [("out",Int)] [])
 (check_defs_1_addN_addN.box_2_lambda.0_rhs_thunk_10,BratNode (Box (fromList []) check_defs_1_addN_addN.box_2_lambda.0_rhs/in_7 check_defs_1_addN_addN.box_2_lambda.0_rhs/out_8) [] [("thunk",{ (n :: Int) -> (out :: Int) })])
@@ -22,8 +22,8 @@ Nodes:
 
 Wires:
 (Ex check_defs_1_addN_addN.box/in 0,Int,In check_defs_1_addN_addN.box_2_lambda_11 0)
-(Ex check_defs_1_addN_addN.box_2_lambda.0_rhs/in_7 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs_9_ 0)
-(Ex check_defs_1_addN_addN.box_2_lambda.0_rhs_9_ 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs/out_8 0)
+(Ex check_defs_1_addN_addN.box_2_lambda.0_rhs/in_7 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs_9_Eval 0)
+(Ex check_defs_1_addN_addN.box_2_lambda.0_rhs_9_Eval 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs/out_8 0)
 (Ex check_defs_1_addN_addN.box_2_lambda_11 0,Int,In check_defs_1_addN_addN.box/out_1 0)
 (Ex check_defs_1_addN_addN.box_thunk_3 0,{ (inp :: Int) -> (out :: Int) },In globals_decl_13_addN 0)
 (Ex globals_Int_1 0,[],In globals___kcr_N 0)
@@ -32,4 +32,4 @@ Wires:
 (Ex globals_Int_5 0,[],In globals___kcc_4 0)
 (Ex globals_Int_6 0,[],In globals___kcc_4 1)
 (Ex globals_Int_7 0,[],In globals___kcc_4 2)
-(Ex globals_prim_2_N 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs_9_ 1)
+(Ex globals_prim_2_N 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs_9_Eval 1)
diff --git a/brat/test/golden/graph/addN2.brat.graph b/brat/test/golden/graph/addN2.brat.graph
index 70642c12..e23d7824 100644
--- a/brat/test/golden/graph/addN2.brat.graph
+++ b/brat/test/golden/graph/addN2.brat.graph
@@ -1,6 +1,6 @@
 Nodes:
 (check_defs_1_addN_addN.box_2_lambda_11,BratNode (PatternMatch ((TestMatchData Braty (MatchSequence {matchInputs = [(NamedPort {end = Ex check_defs_1_addN_addN.box_2_lambda.0_setup/in_3 0, portName = "inp"},Int)], matchTests = [], matchOutputs = [(NamedPort {end = Ex check_defs_1_addN_addN.box_2_lambda.0_setup/in_3 0, portName = "inp"},Int)]}),check_defs_1_addN_addN.box_2_lambda.0_rhs_thunk_10) :| [])) [("inp",Int)] [("out",Int)])
-(check_defs_1_addN_addN.box_2_lambda.0_rhs_9_,BratNode (Eval (Ex globals_prim_8_add 0)) [("a",Int),("b",Int)] [("c",Int)])
+(check_defs_1_addN_addN.box_2_lambda.0_rhs_9_Eval,BratNode (Eval (Ex globals_prim_8_add 0)) [("a",Int),("b",Int)] [("c",Int)])
 (check_defs_1_addN_addN.box_2_lambda.0_rhs/in_7,BratNode Source [] [("n",Int)])
 (check_defs_1_addN_addN.box_2_lambda.0_rhs/out_8,BratNode Target [("out",Int)] [])
 (check_defs_1_addN_addN.box_2_lambda.0_rhs_thunk_10,BratNode (Box (fromList []) check_defs_1_addN_addN.box_2_lambda.0_rhs/in_7 check_defs_1_addN_addN.box_2_lambda.0_rhs/out_8) [] [("thunk",{ (n :: Int) -> (out :: Int) })])
@@ -22,8 +22,8 @@ Nodes:
 
 Wires:
 (Ex check_defs_1_addN_addN.box/in 0,Int,In check_defs_1_addN_addN.box_2_lambda_11 0)
-(Ex check_defs_1_addN_addN.box_2_lambda.0_rhs/in_7 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs_9_ 0)
-(Ex check_defs_1_addN_addN.box_2_lambda.0_rhs_9_ 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs/out_8 0)
+(Ex check_defs_1_addN_addN.box_2_lambda.0_rhs/in_7 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs_9_Eval 0)
+(Ex check_defs_1_addN_addN.box_2_lambda.0_rhs_9_Eval 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs/out_8 0)
 (Ex check_defs_1_addN_addN.box_2_lambda_11 0,Int,In check_defs_1_addN_addN.box/out_1 0)
 (Ex check_defs_1_addN_addN.box_thunk_3 0,{ (inp :: Int) -> (out :: Int) },In globals_decl_13_addN 0)
 (Ex globals_Int_1 0,[],In globals___kcr_N 0)
@@ -32,4 +32,4 @@ Wires:
 (Ex globals_Int_5 0,[],In globals___kcc_4 0)
 (Ex globals_Int_6 0,[],In globals___kcc_4 1)
 (Ex globals_Int_7 0,[],In globals___kcc_4 2)
-(Ex globals_prim_2_N 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs_9_ 1)
+(Ex globals_prim_2_N 0,Int,In check_defs_1_addN_addN.box_2_lambda.0_rhs_9_Eval 1)
diff --git a/brat/test/golden/graph/cons.brat.graph b/brat/test/golden/graph/cons.brat.graph
index 3da7e8a1..cc61c7b8 100644
--- a/brat/test/golden/graph/cons.brat.graph
+++ b/brat/test/golden/graph/cons.brat.graph
@@ -1,32 +1,32 @@
 Nodes:
-(check_defs_1_three_1__1,BratNode (Const 0) [] [("value",Int)])
 (check_defs_1_three_1_cons,BratNode (Constructor cons) [("head",Int),("tail",Vec(Int, 2))] [("value",Vec(Int, 3))])
-(check_defs_1_two__1,BratNode (Const 1) [] [("value",Int)])
-(check_defs_1_two__3,BratNode (Const 2) [] [("value",Int)])
+(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))])
-(globals__3,BratNode (Const 2) [] [("value",Nat)])
-(globals__8,BratNode (Const 3) [] [("value",Nat)])
 (globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (globals_Int_7,BratNode (Constructor Int) [] [("value",[])])
 (globals_Vec_1,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
 (globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
+(globals_const_3,BratNode (Const 2) [] [("value",Nat)])
+(globals_const_8,BratNode (Const 3) [] [("value",Nat)])
 (globals_decl_4_two,BratNode Id [("a1",Vec(Int, 2))] [("a1",Vec(Int, 2))])
 (globals_decl_9_three,BratNode Id [("a1",Vec(Int, 3))] [("a1",Vec(Int, 3))])
 
 Wires:
-(Ex check_defs_1_three_1__1 0,Int,In check_defs_1_three_1_cons 0)
 (Ex check_defs_1_three_1_cons 0,Vec(Int, 3),In globals_decl_9_three 0)
-(Ex check_defs_1_two__1 0,Int,In check_defs_1_two_cons 0)
-(Ex check_defs_1_two__3 0,Int,In check_defs_1_two_cons_2 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 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__3 0,Nat,In globals_Vec_1 1)
-(Ex globals__8 0,Nat,In globals_Vec_6 1)
+(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)
diff --git a/brat/test/golden/graph/kernel.brat.graph b/brat/test/golden/graph/kernel.brat.graph
index 9544c538..26ad580e 100644
--- a/brat/test/golden/graph/kernel.brat.graph
+++ b/brat/test/golden/graph/kernel.brat.graph
@@ -13,12 +13,12 @@ Nodes:
 (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)) })])
-(globals__8,BratNode (Const 3) [] [("value",Nat)])
 (globals_Qubit_2,BratNode (Constructor Qubit) [] [("value",[])])
 (globals_Qubit_3,BratNode (Constructor Qubit) [] [("value",[])])
 (globals_Qubit_4,BratNode (Constructor Qubit) [] [("value",[])])
 (globals_Qubit_7,BratNode (Constructor Qubit) [] [("value",[])])
 (globals_Vec_6,BratNode (Constructor Vec) [("X",[]),("n",Nat)] [("value",[])])
+(globals_const_8,BratNode (Const 3) [] [("value",Nat)])
 (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:
@@ -39,4 +39,4 @@ Wires:
 (Ex globals_Qubit_4 0,[],In globals___kcr__1 2)
 (Ex globals_Qubit_7 0,[],In globals_Vec_6 0)
 (Ex globals_Vec_6 0,[],In globals___kcr__5 0)
-(Ex globals__8 0,Nat,In globals_Vec_6 1)
+(Ex globals_const_8 0,Nat,In globals_Vec_6 1)
diff --git a/brat/test/golden/graph/list.brat.graph b/brat/test/golden/graph/list.brat.graph
index 255e1de0..de1910c1 100644
--- a/brat/test/golden/graph/list.brat.graph
+++ b/brat/test/golden/graph/list.brat.graph
@@ -1,22 +1,22 @@
 Nodes:
-(check_defs_1_xs__1,BratNode (Const 1) [] [("value",Int)])
-(check_defs_1_xs__3,BratNode (Const 2) [] [("value",Int)])
-(check_defs_1_xs__5,BratNode (Const 3) [] [("value",Int)])
 (check_defs_1_xs_cons,BratNode (Constructor cons) [("head",Int),("tail",List(Int))] [("value",List(Int))])
 (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))])
 (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__1 0,Int,In check_defs_1_xs_cons 0)
-(Ex check_defs_1_xs__3 0,Int,In check_defs_1_xs_cons_2 0)
-(Ex check_defs_1_xs__5 0,Int,In check_defs_1_xs_cons_4 0)
 (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_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 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/num.brat.graph b/brat/test/golden/graph/num.brat.graph
index 27521a96..e9645cc6 100644
--- a/brat/test/golden/graph/num.brat.graph
+++ b/brat/test/golden/graph/num.brat.graph
@@ -1,7 +1,7 @@
 Nodes:
-(check_defs_1_m_1__1,BratNode (Const -3) [] [("value",Int)])
+(check_defs_1_m_1_const_1,BratNode (Const -3) [] [("value",Int)])
 (check_defs_1_m_1_doub,BratNode (Constructor doub) [("value",Int)] [("value",Int)])
-(check_defs_1_n__1,BratNode (Const 2) [] [("value",Nat)])
+(check_defs_1_n_const_1,BratNode (Const 2) [] [("value",Nat)])
 (check_defs_1_n_succ,BratNode (Constructor succ) [("value",Nat)] [("value",Nat)])
 (globals_Int_4,BratNode (Constructor Int) [] [("value",[])])
 (globals_Nat_1,BratNode (Constructor Nat) [] [("value",[])])
@@ -9,9 +9,9 @@ Nodes:
 (globals_decl_5_m,BratNode Id [("a1",Int)] [("a1",Int)])
 
 Wires:
-(Ex check_defs_1_m_1__1 0,Int,In check_defs_1_m_1_doub 0)
+(Ex check_defs_1_m_1_const_1 0,Int,In check_defs_1_m_1_doub 0)
 (Ex check_defs_1_m_1_doub 0,Int,In globals_decl_5_m 0)
-(Ex check_defs_1_n__1 0,Nat,In check_defs_1_n_succ 0)
+(Ex check_defs_1_n_const_1 0,Nat,In check_defs_1_n_succ 0)
 (Ex check_defs_1_n_succ 0,Nat,In globals_decl_2_n 0)
 (Ex globals_Int_4 0,[],In globals___kca_m_3 0)
 (Ex globals_Nat_1 0,[],In globals___kca_n 0)
diff --git a/brat/test/golden/graph/one.brat.graph b/brat/test/golden/graph/one.brat.graph
index 0e93fcd8..2a7e1081 100644
--- a/brat/test/golden/graph/one.brat.graph
+++ b/brat/test/golden/graph/one.brat.graph
@@ -1,8 +1,8 @@
 Nodes:
-(check_defs_1_one_,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_one_const,BratNode (Const 1) [] [("value",Int)])
 (globals_Int_1,BratNode (Constructor Int) [] [("value",[])])
 (globals_decl_2_one,BratNode Id [("n",Int)] [("n",Int)])
 
 Wires:
-(Ex check_defs_1_one_ 0,Int,In globals_decl_2_one 0)
+(Ex check_defs_1_one_const 0,Int,In globals_decl_2_one 0)
 (Ex globals_Int_1 0,[],In globals___kca_one 0)
diff --git a/brat/test/golden/graph/pair.brat.graph b/brat/test/golden/graph/pair.brat.graph
index 42192ce4..ef826479 100644
--- a/brat/test/golden/graph/pair.brat.graph
+++ b/brat/test/golden/graph/pair.brat.graph
@@ -1,7 +1,7 @@
 Nodes:
-(check_defs_1_xs__1,BratNode (Const 1) [] [("value",Int)])
 (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)])
 (globals_Bool_4,BratNode (Constructor Bool) [] [("value",[])])
@@ -12,9 +12,9 @@ Nodes:
 (globals_nil_5,BratNode (Constructor nil) [] [("value",[])])
 
 Wires:
-(Ex check_defs_1_xs__1 0,Int,In check_defs_1_xs_cons 0)
 (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 globals_Bool_4 0,[],In globals_cons_3 0)
diff --git a/brat/test/golden/graph/rx.brat.graph b/brat/test/golden/graph/rx.brat.graph
index 5f241723..14afc93b 100644
--- a/brat/test/golden/graph/rx.brat.graph
+++ b/brat/test/golden/graph/rx.brat.graph
@@ -1,6 +1,6 @@
 Nodes:
 (check_defs_1_main_2_thunk_3_lambda_11,KernelNode (PatternMatch ((TestMatchData Kerny (MatchSequence {matchInputs = [(NamedPort {end = Ex check_defs_1_main_2_thunk_3_lambda.0_setup/in_3 0, portName = "a"},Qubit)], matchTests = [], matchOutputs = [(NamedPort {end = Ex check_defs_1_main_2_thunk_3_lambda.0_setup/in_3 0, portName = "a"},Qubit)]}),check_defs_1_main_2_thunk_3_lambda.0_rhs_thunk_9) :| [])) [("a",Qubit)] [("b",Qubit)])
-(check_defs_1_main_2_thunk_3_lambda.0_rhs_10_,KernelNode (Splice (Ex globals_decl_18_xish 0)) [("rxa",Qubit)] [("rxb",Qubit)])
+(check_defs_1_main_2_thunk_3_lambda.0_rhs_10_Splice,KernelNode (Splice (Ex globals_decl_18_xish 0)) [("rxa",Qubit)] [("rxb",Qubit)])
 (check_defs_1_main_2_thunk_3_lambda.0_rhs/in_7,KernelNode Source [] [("q",Qubit)])
 (check_defs_1_main_2_thunk_3_lambda.0_rhs/out_8,KernelNode Target [("b",Qubit)] [])
 (check_defs_1_main_2_thunk_3_lambda.0_rhs_thunk_9,BratNode (Box (fromList []) check_defs_1_main_2_thunk_3_lambda.0_rhs/in_7 check_defs_1_main_2_thunk_3_lambda.0_rhs/out_8) [] [("thunk",{ (q :: Qubit) -o (b :: Qubit) })])
@@ -10,11 +10,11 @@ Nodes:
 (check_defs_1_main_2_thunk/in,KernelNode Source [] [("a",Qubit)])
 (check_defs_1_main_2_thunk/out_1,KernelNode Target [("b",Qubit)] [])
 (check_defs_1_main_2_thunk_thunk_2,BratNode (Box (fromList []) check_defs_1_main_2_thunk/in check_defs_1_main_2_thunk/out_1) [] [("thunk",{ (a :: Qubit) -o (b :: Qubit) })])
-(check_defs_1_nums_,BratNode (Const 1) [] [("value",Int)])
-(check_defs_1_nums__1,BratNode (Const 2) [] [("value",Int)])
-(check_defs_1_nums__2,BratNode (Const 3) [] [("value",Int)])
-(check_defs_1_xish_1_,BratNode (Eval (Ex globals_prim_7_Rx 0)) [("th",Float)] [("a1",{ (rxa :: Qubit) -o (rxb :: Qubit) })])
-(check_defs_1_xish_1__1,BratNode (Const 30.0) [] [("value",Float)])
+(check_defs_1_nums_const,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_nums_const_1,BratNode (Const 2) [] [("value",Int)])
+(check_defs_1_nums_const_2,BratNode (Const 3) [] [("value",Int)])
+(check_defs_1_xish_1_Eval,BratNode (Eval (Ex globals_prim_7_Rx 0)) [("th",Float)] [("a1",{ (rxa :: Qubit) -o (rxb :: Qubit) })])
+(check_defs_1_xish_1_const_1,BratNode (Const 30.0) [] [("value",Float)])
 (globals_Float_2,BratNode (Constructor Float) [] [("value",[])])
 (globals_Int_9,BratNode (Constructor Int) [] [("value",[])])
 (globals_Int_10,BratNode (Constructor Int) [] [("value",[])])
@@ -32,15 +32,15 @@ Nodes:
 
 Wires:
 (Ex check_defs_1_main_2_thunk/in 0,Qubit,In check_defs_1_main_2_thunk_3_lambda_11 0)
-(Ex check_defs_1_main_2_thunk_3_lambda.0_rhs/in_7 0,Qubit,In check_defs_1_main_2_thunk_3_lambda.0_rhs_10_ 0)
-(Ex check_defs_1_main_2_thunk_3_lambda.0_rhs_10_ 0,Qubit,In check_defs_1_main_2_thunk_3_lambda.0_rhs/out_8 0)
+(Ex check_defs_1_main_2_thunk_3_lambda.0_rhs/in_7 0,Qubit,In check_defs_1_main_2_thunk_3_lambda.0_rhs_10_Splice 0)
+(Ex check_defs_1_main_2_thunk_3_lambda.0_rhs_10_Splice 0,Qubit,In check_defs_1_main_2_thunk_3_lambda.0_rhs/out_8 0)
 (Ex check_defs_1_main_2_thunk_3_lambda_11 0,Qubit,In check_defs_1_main_2_thunk/out_1 0)
 (Ex check_defs_1_main_2_thunk_thunk_2 0,{ (a :: Qubit) -o (b :: Qubit) },In globals_decl_24_main 0)
-(Ex check_defs_1_nums_ 0,Int,In globals_decl_12_nums 0)
-(Ex check_defs_1_nums__1 0,Int,In globals_decl_12_nums 1)
-(Ex check_defs_1_nums__2 0,Int,In globals_decl_12_nums 2)
-(Ex check_defs_1_xish_1_ 0,{ (rxa :: Qubit) -o (rxb :: Qubit) },In globals_decl_18_xish 0)
-(Ex check_defs_1_xish_1__1 0,Float,In check_defs_1_xish_1_ 0)
+(Ex check_defs_1_nums_const 0,Int,In globals_decl_12_nums 0)
+(Ex check_defs_1_nums_const_1 0,Int,In globals_decl_12_nums 1)
+(Ex check_defs_1_nums_const_2 0,Int,In globals_decl_12_nums 2)
+(Ex check_defs_1_xish_1_Eval 0,{ (rxa :: Qubit) -o (rxb :: Qubit) },In globals_decl_18_xish 0)
+(Ex check_defs_1_xish_1_const_1 0,Float,In check_defs_1_xish_1_Eval 0)
 (Ex globals_Float_2 0,[],In globals___kcc_1 0)
 (Ex globals_Int_10 0,[],In globals___kca_nums_8 1)
 (Ex globals_Int_11 0,[],In globals___kca_nums_8 2)
diff --git a/brat/test/golden/graph/two.brat.graph b/brat/test/golden/graph/two.brat.graph
index a85f418b..cdb6a0c8 100644
--- a/brat/test/golden/graph/two.brat.graph
+++ b/brat/test/golden/graph/two.brat.graph
@@ -1,7 +1,7 @@
 Nodes:
-(check_defs_1_one_,BratNode (Const 1) [] [("value",Int)])
-(check_defs_1_two_1_,BratNode (Eval (Ex globals_prim_5_add 0)) [("a",Int),("b",Int)] [("c",Int)])
-(check_defs_1_two_1__1,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_one_const,BratNode (Const 1) [] [("value",Int)])
+(check_defs_1_two_1_Eval,BratNode (Eval (Ex globals_prim_5_add 0)) [("a",Int),("b",Int)] [("c",Int)])
+(check_defs_1_two_1_const_1,BratNode (Const 1) [] [("value",Int)])
 (globals_Int_2,BratNode (Constructor Int) [] [("value",[])])
 (globals_Int_3,BratNode (Constructor Int) [] [("value",[])])
 (globals_Int_4,BratNode (Constructor Int) [] [("value",[])])
@@ -12,12 +12,12 @@ Nodes:
 (globals_prim_5_add,BratNode (Prim ("","add")) [] [("thunk",{ (a :: Int), (b :: Int) -> (c :: Int) })])
 
 Wires:
-(Ex check_defs_1_one_ 0,Int,In globals_decl_8_one 0)
-(Ex check_defs_1_two_1_ 0,Int,In globals_decl_11_two 0)
-(Ex check_defs_1_two_1__1 0,Int,In check_defs_1_two_1_ 0)
+(Ex check_defs_1_one_const 0,Int,In globals_decl_8_one 0)
+(Ex check_defs_1_two_1_Eval 0,Int,In globals_decl_11_two 0)
+(Ex check_defs_1_two_1_const_1 0,Int,In check_defs_1_two_1_Eval 0)
 (Ex globals_Int_10 0,[],In globals___kca_two_9 0)
 (Ex globals_Int_2 0,[],In globals___kcc_1 0)
 (Ex globals_Int_3 0,[],In globals___kcc_1 1)
 (Ex globals_Int_4 0,[],In globals___kcc_1 2)
 (Ex globals_Int_7 0,[],In globals___kca_one_6 0)
-(Ex globals_decl_8_one 0,Int,In check_defs_1_two_1_ 1)
+(Ex globals_decl_8_one 0,Int,In check_defs_1_two_1_Eval 1)
diff --git a/brat/test/golden/graph/vec.brat.graph b/brat/test/golden/graph/vec.brat.graph
index 100f9489..844bd6c8 100644
--- a/brat/test/golden/graph/vec.brat.graph
+++ b/brat/test/golden/graph/vec.brat.graph
@@ -1,24 +1,24 @@
 Nodes:
-(check_defs_1_xs__1,BratNode (Const 0) [] [("value",Int)])
-(check_defs_1_xs__3,BratNode (Const 1) [] [("value",Int)])
-(check_defs_1_xs__5,BratNode (Const 2) [] [("value",Int)])
 (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))])
-(globals__3,BratNode (Const 3) [] [("value",Nat)])
 (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__1 0,Int,In check_defs_1_xs_cons 0)
-(Ex check_defs_1_xs__3 0,Int,In check_defs_1_xs_cons_2 0)
-(Ex check_defs_1_xs__5 0,Int,In check_defs_1_xs_cons_4 0)
 (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 globals_Int_2 0,[],In globals_Vec_1 0)
 (Ex globals_Vec_1 0,[],In globals___kca_xs 0)
-(Ex globals__3 0,Nat,In globals_Vec_1 1)
+(Ex globals_const_3 0,Nat,In globals_Vec_1 1)
diff --git a/brat/test/golden/kernel/kernel_application.brat.golden b/brat/test/golden/kernel/kernel_application.brat.golden
index ed0aa8bf..af09def9 100644
--- a/brat/test/golden/kernel/kernel_application.brat.golden
+++ b/brat/test/golden/kernel/kernel_application.brat.golden
@@ -2,7 +2,5 @@ Error in test/golden/kernel/kernel_application.brat on line 16:
 rotate = { q => maybeRotate(true) }
                 ^^^^^^^^^^^
 
-  Expected function to be a (kernel) thunk, but found:
-  (thunk :: { (a1 :: Bool) -> (a1 :: { (a1 :: Qubit) -o (a1 :: Qubit) }) })
-
+  Type error: Expected a (kernel) function or vector of functions, got { (a1 :: Bool) -> (a1 :: { (a1 :: Qubit) -o (a1 :: Qubit) }) }