diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs
index ffee325f..3b317be0 100644
--- a/brat/Brat/Checker.hs
+++ b/brat/Brat/Checker.hs
@@ -25,6 +25,7 @@ import Prelude hiding (filter)
 import Brat.Checker.Helpers
 import Brat.Checker.Monad
 import Brat.Checker.Quantity
+import Brat.Checker.SolveHoles (typeEq)
 import Brat.Checker.SolvePatterns (argProblems, argProblemsWithLeftovers, solve)
 import Brat.Checker.Types
 import Brat.Constructors
@@ -659,7 +660,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
 
 
@@ -1124,7 +1131,7 @@ run :: VEnv
     -> Namespace
     -> Checking a
     -> Either Error (a, ([TypedHole], Store, Graph))
-run ve initStore ns m =
+run ve initStore ns m = do
   let ctx = Ctx { globalVEnv = ve
                 , store = initStore
                 -- TODO: fill with default constructors
@@ -1132,5 +1139,19 @@ run ve initStore ns m =
                 , kconstructors = kernelConstructors
                 , typeConstructors = defaultTypeConstructors
                 , aliasTable = M.empty
-                } in
-    (\(a,ctx,(holes, graph)) -> (a, (holes, store ctx, graph))) <$> handler (localNS ns m) ctx mempty
+                , hopes = M.empty
+                }
+  (a,ctx,(holes, graph)) <- handler (localNS ns m) ctx mempty
+  let tyMap = typeMap $ store ctx
+  -- If the `hopes` set has any remaining holes with kind Nat, we need to abort.
+  -- Even though we didn't need them for typechecking problems, our runtime
+  -- behaviour depends on the values of the holes, which we can't account for.
+  case M.toList $ M.filterWithKey (\e _ -> isNatKinded tyMap (InEnd e)) (hopes ctx) of
+    [] -> pure (a, (holes, store ctx, graph))
+    -- Just use the FC of the first hole while we don't have the capacity to
+    -- show multiple error locations
+    hs@((_,fc):_) -> Left $ Err (Just fc) (RemainingNatHopes (show . fst <$> hs))
+ where
+  isNatKinded tyMap e = case tyMap M.! e of
+    EndType Braty (Left Nat) -> True
+    _ -> False
diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs
index f58ac827..5c33437b 100644
--- a/brat/Brat/Checker/Helpers.hs
+++ b/brat/Brat/Checker/Helpers.hs
@@ -272,58 +272,12 @@ vecLayers :: Modey m -> Val Z -> Checking ([(Src, NumVal (VVar Z))] -- The sizes
                                           ,CTy m Z -- The function type at the end
                                           )
 vecLayers my (TVec ty (VNum n)) = do
-  src <- mkStaticNum n
+  src <- buildNatVal n
   first ((src, n):) <$> vecLayers my ty
 vecLayers Braty (VFun Braty cty) = pure ([], cty)
 vecLayers Kerny (VFun Kerny cty) = pure ([], cty)
 vecLayers my ty = typeErr $ "Expected a " ++ showMode my ++ "function or vector of functions, got " ++ show ty
 
-mkStaticNum :: NumVal (VVar Z) -> Checking Src
-mkStaticNum n@(NumValue c gro) = do
-  (_, [], [(constSrc,_)], _) <- next "const" (Const (Num (fromIntegral c))) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
-  src <- case gro of
-    Constant0 -> pure constSrc
-    StrictMonoFun sm -> do
-      (_, [(lhs,_),(rhs,_)], [(src,_)], _) <- next "add_const" (ArithNode Add) (S0, Some (Zy :* S0))
-                                              (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0))
-                                              (RPr ("value", TNat) R0)
-      smSrc <- mkStrictMono sm
-      wire (constSrc, TNat, lhs)
-      wire (smSrc, TNat, rhs)
-      pure src
-  defineSrc src (VNum n)
-  pure src
- where
-  mkStrictMono :: StrictMono (VVar Z) -> Checking Src
-  mkStrictMono (StrictMono k mono) = do
-    (_, [], [(constSrc,_)], _) <- next "2^k" (Const (Num (2^k))) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
-    (_, [(lhs,_),(rhs,_)], [(src,_)], _) <- next "mult_const" (ArithNode Mul) (S0, Some (Zy :* S0))
-                                            (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0))
-                                            (RPr ("value", TNat) R0)
-    monoSrc <- mkMono mono
-    wire (constSrc, TNat, lhs)
-    wire (monoSrc, TNat, rhs)
-    pure src
-
-  mkMono :: Monotone (VVar Z) -> Checking Src
-  mkMono (Linear (VPar (ExEnd e))) = pure (NamedPort e "mono")
-  mkMono (Full sm) = do
-    (_, [], [(twoSrc,_)], _) <- next "2" (Const (Num 2)) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
-    (_, [(lhs,_),(rhs,_)], [(powSrc,_)], _) <- next "2^" (ArithNode Pow) (S0, Some (Zy :* S0))
-                                               (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0))
-                                               (RPr ("value", TNat) R0)
-    smSrc <- mkStrictMono sm
-    wire (twoSrc, TNat, lhs)
-    wire (smSrc, TNat, rhs)
-
-    (_, [], [(oneSrc,_)], _) <- next "1" (Const (Num 1)) (S0, Some (Zy :* S0)) R0 (RPr ("value", TNat) R0)
-    (_, [(lhs,_),(rhs,_)], [(src,_)], _) <- next "n-1" (ArithNode Sub) (S0, Some (Zy :* S0))
-                                            (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0))
-                                            (RPr ("value", TNat) R0)
-    wire (powSrc, TNat, lhs)
-    wire (oneSrc, TNat, rhs)
-    pure src
-
 vectorise :: forall m. Modey m -> (Src, Val Z) -> Checking (Src, CTy m Z)
 vectorise my (src, ty) = do
   (layers, cty) <- vecLayers my ty
@@ -492,3 +446,106 @@ runArith (NumValue upl grol) Pow (NumValue upr gror)
  -- 2^(2^k * upr) + 2^(2^k * upr) * (full(2^(k + k') * mono))
  = pure $ NumValue (upl ^ upr) (StrictMonoFun (StrictMono (l * upr) (Full (StrictMono (k + k') mono))))
 runArith _ _ _ = Nothing
+
+buildArithOp :: ArithOp -> Checking ((Tgt, Tgt), Src)
+buildArithOp op = do
+  (_, [(lhs,_), (rhs,_)], [(out,_)], _) <- next (show op) (ArithNode op) (S0, Some (Zy :* S0)) (RPr ("lhs", TNat) (RPr ("rhs", TNat) R0)) (RPr ("value", TNat) R0)
+  pure ((lhs, rhs), out)
+
+buildConst :: SimpleTerm -> Val Z -> Checking Src
+buildConst tm ty = do
+  (_, _, [(out,_)], _) <- next "buildConst" (Const tm) (S0, Some (Zy :* S0)) R0 (RPr ("value", ty) R0)
+  pure out
+
+buildNum :: Integer -> Checking Src
+buildNum n = buildConst (Num (fromIntegral n)) TNat
+
+-- 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 e993711b..cb9fd015 100644
--- a/brat/Brat/Checker/Monad.hs
+++ b/brat/Brat/Checker/Monad.hs
@@ -50,12 +50,16 @@ data CtxEnv = CtxEnv
   , locals :: VEnv
   }
 
+type Hopes = M.Map InPort FC
+
 data Context = Ctx { globalVEnv :: VEnv
                    , store :: Store
                    , constructors :: ConstructorMap Brat
                    , kconstructors :: ConstructorMap Kernel
                    , typeConstructors :: M.Map (Mode, QualName) [(PortName, TypeKind)]
                    , aliasTable :: M.Map QualName Alias
+                   -- All the ends here should be targets
+                   , hopes :: Hopes
                    }
 
 data CheckingSig ty where
@@ -89,6 +93,9 @@ data CheckingSig ty where
   AskVEnv :: CheckingSig CtxEnv
   Declare :: End -> Modey m -> BinderType m -> CheckingSig ()
   Define  :: End -> Val Z -> CheckingSig ()
+  ANewHope :: InPort -> FC -> CheckingSig ()
+  AskHopes :: CheckingSig Hopes
+  RemoveHope :: InPort -> CheckingSig ()
 
 localAlias :: (QualName, Alias) -> Checking v -> Checking v
 localAlias _ (Ret v) = Ret v
@@ -267,6 +274,15 @@ handler (Req s k) ctx g
                 M.lookup tycon tbl
         handler (k args) ctx g
 
+      ANewHope e fc -> handler (k ()) (ctx { hopes = M.insert e fc (hopes ctx) }) g
+
+      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)))
+
 type Checking = Free CheckingSig
 
 instance Semigroup a => Semigroup (Checking a) where
diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs
new file mode 100644
index 00000000..801ec0fe
--- /dev/null
+++ b/brat/Brat/Checker/SolveHoles.hs
@@ -0,0 +1,160 @@
+module Brat.Checker.SolveHoles (typeEq, buildNum) where
+
+import Brat.Checker.Monad
+import Brat.Checker.Types (kindForMode)
+import Brat.Checker.Helpers (buildConst, buildNatVal, buildNum)
+import Brat.Error (ErrorMsg(..))
+import Brat.Eval
+import Brat.Syntax.Common
+import Brat.Syntax.Simple (SimpleTerm(..))
+import Brat.Syntax.Value
+import Control.Monad.Freer
+import Bwd
+import Hasochism
+import Util (zipSameLength)
+
+import Data.Bifunctor (second)
+import Data.Foldable (sequenceA_)
+import Data.Functor
+import qualified Data.Map as M
+import Data.Type.Equality (TestEquality(..), (:~:)(..))
+
+-- External interface to typeEq' for closed values only.
+typeEq :: String -- String representation of the term for error reporting
+       -> TypeKind -- The kind we're comparing at
+       -> Val Z -- Expected
+       -> Val Z -- Actual
+       -> Checking ()
+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
+
+isNumVar :: Sem -> Maybe SVar
+isNumVar (SNum (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear v))))) = Just v
+isNumVar _ = Nothing
+
+-- Presumes that the hope set and the two `Sem`s are up to date.
+typeEqEta :: String -- String representation of the term for error reporting
+          -> (Ny :* Stack Z TypeKind :* Stack Z Sem) n
+          -> 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) 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)) 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)
+-- 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
+  case [e | (VApp (VPar (InEnd e)) _) <- [exp,act], M.member e hopes] of
+    [] -> typeEqRigid tm stuff k exp act
+    [e1, e2] | e1 == e2 -> pure () -- trivially same, even if both still yet-to-be-defined
+    _es -> error "TODO: must wait for one or the other to become more defined"
+
+-- This will update the `hopes` set, potentially invalidating things that have
+-- been eval'd.
+-- The Sem is closed, for now.
+solveHope :: TypeKind -> InPort -> Sem -> Checking ()
+solveHope k hope v = quote Zy v >>= \v -> case doesntOccur (InEnd hope) v of
+  Right () -> do
+    defineEnd (InEnd hope) v
+    dangling <- case (k, v) of
+      (Nat, VNum v) -> buildNatVal v
+      (Nat, _) -> err $ InternalError "Head of Nat wasn't a VNum"
+      _ -> buildConst Unit TUnit
+    req (Wire (end dangling, kindType k, hope))
+    req (RemoveHope hope)
+  Left msg -> case v of
+    VApp (VPar (InEnd end)) B0 | hope == end -> pure ()
+    -- TODO: Not all occurrences are toxic. The end could be in an argument
+    -- to a hoping variable which isn't used.
+    -- E.g. h1 = h2 h1 - this is valid if h2 is the identity, or ignores h1.
+    _ -> err msg
+
+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 _ _ _ _ _ = typeErr "arity mismatch"
+
+typeEqRow :: Modey m
+          -> String -- The term we complain about in errors
+          -> (Ny :* Stack Z TypeKind :* Stack Z Sem) lv -- Next available level, the kinds of existing levels
+          -> 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)
+                             ,[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 <&> 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"
+
+-- Calls to typeEqRigid *must* start with rigid types to ensure termination
+typeEqRigid :: 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 ()
+typeEqRigid tm (_ :* _ :* semz) Nat exp act = do
+  -- TODO: What if there's hope in the numbers?
+  exp <- sem semz exp
+  act <- sem semz act
+  if getNum exp == getNum act
+  then pure ()
+  else err $ TypeMismatch tm (show exp) (show act)
+typeEqRigid tm stuff@(_ :* kz :* _) (TypeFor m []) (VApp f args) (VApp f' args') | f == f' =
+  svKind f >>= \case
+    TypeFor m' ks | m == m' -> typeEqs tm stuff (snd <$> ks) (args <>> []) (args' <>> [])
+      -- pattern should always match
+    _ -> err $ InternalError "quote gave a surprising result"
+ where
+  svKind (VPar e) = kindOf (VPar e)
+  svKind (VInx n) = pure $ proj kz n
+typeEqRigid tm lvkz (TypeFor m []) (VCon c args) (VCon c' args') | c == c' =
+  req (TLup (m, c)) >>= \case
+        Just ks -> typeEqs tm lvkz (snd <$> ks) args args'
+        Nothing -> err $ TypeErr $ "Type constructor " ++ show c
+                        ++ " undefined " ++ " at kind " ++ show (TypeFor m [])
+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
+  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 >>= (sequenceA_ . concat)
+ where
+  eqVariant (Some r0, Some r1) = throwLeft (snd <$> typeEqRow m0 tm lvkz r0 r1)
+typeEqRigid tm _ _ v0 v1 = err $ TypeMismatch tm (show v0) (show v1)
diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs
index d9034655..cd76efd3 100644
--- a/brat/Brat/Checker/SolvePatterns.hs
+++ b/brat/Brat/Checker/SolvePatterns.hs
@@ -19,7 +19,6 @@ import Hasochism
 
 import Control.Monad (unless)
 import Data.Bifunctor (first)
-import Data.Foldable (for_, traverse_)
 import qualified Data.Map as M
 import Data.Maybe (fromJust)
 import Data.Type.Equality ((:~:)(..), testEquality)
@@ -78,7 +77,7 @@ solve my ((src, Lit tm):p) = do
     (Braty, Left Nat)
       | Num n <- tm -> do
           unless (n >= 0) $ typeErr "Negative Nat kind"
-          unifyNum (nConstant (fromIntegral n)) (nVar (VPar (ExEnd (end src))))
+          unifyNum (nConstant (fromIntegral n)) (nVar (VPar (toEnd src)))
     (Braty, Right ty) -> do
       throwLeft (simpleCheck Braty ty tm)
     _ -> typeErr $ "Literal " ++ show tm ++ " isn't valid at this type"
@@ -97,7 +96,7 @@ solve my ((src, PCon c abs):p) = do
       -- Special case for 0, so that we can call `unifyNum` instead of pattern
       -- matching using what's returned from `natConstructors`
       PrefixName [] "zero" -> do
-        unifyNum (nVar (VPar (ExEnd (end src)))) nZero
+        unifyNum (nVar (VPar (toEnd src))) nZero
         p <- argProblems [] (normaliseAbstractor abs) p
         (tests, sol) <- solve my p
         pure ((src, PrimLitTest (Num 0)):tests, sol)
@@ -108,7 +107,7 @@ solve my ((src, PCon c abs):p) = do
             (REx ("inner", Nat) R0)
           unifyNum
            (nVar (VPar (ExEnd (end src))))
-           (relationToInner (nVar (VPar (ExEnd (end dangling)))))
+           (relationToInner (nVar (VPar (toEnd dangling))))
           p <- argProblems [dangling] (normaliseAbstractor abs) p
           (tests, sol) <- solve my p
           -- When we get @-patterns, we shouldn't drop this anymore
@@ -198,39 +197,42 @@ instantiateMeta e val = do
   throwLeft (doesntOccur e val)
   defineEnd e val
 
-
--- Be conservative, fail if in doubt. Not dangerous like being wrong while succeeding
--- We can have bogus failures here because we're not normalising under lambdas
--- N.B. the value argument is normalised.
-doesntOccur :: End -> Val n -> Either ErrorMsg ()
-doesntOccur e (VNum nv) = for_ (getNumVar nv) (collision e)
+-- Solve a Nat kinded metavariable. Unlike `instantiateMeta`, this function also
+-- makes the dynamic wiring for a metavariable. This only needs to happen for
+-- numbers because they have nontrivial runtime behaviour.
+--
+-- We assume that the caller has done the occurs check and rules out trivial equations.
+solveNumMeta :: End -> NumVal (VVar Z) -> Checking ()
+solveNumMeta e nv = case (e, vars nv) of
+ -- Compute the thing that the rhs should be based on the src, and instantiate src to that
+ (ExEnd src,  [VPar (InEnd _tgt)]) -> do
+   -- Compute the value of the `tgt` variable from the known `src` value by inverting nv
+   tgtSrc <- invertNatVal nv
+   instantiateMeta (ExEnd src) (VNum (nVar (VPar (toEnd tgtSrc))))
+   wire (NamedPort src "", TNat, tgtSrc)
+
+ (ExEnd src, _) -> instantiateMeta (ExEnd src) (VNum nv)
+
+ -- Both targets, we need to create the thing that they both derive from
+ (InEnd bigTgt, [VPar (InEnd weeTgt)]) -> do
+   (_, [(idTgt, _)], [(idSrc, _)], _) <- anext "numval id" Id (S0, Some (Zy :* S0))
+                                         (REx ("n", Nat) R0) (REx ("n", Nat) R0)
+   defineSrc idSrc (VNum (nVar (VPar (toEnd idTgt))))
+   instantiateMeta (InEnd weeTgt) (VNum (nVar (VPar (toEnd idSrc))))
+   wire (idSrc, TNat, NamedPort weeTgt "")
+   let nv' = fmap (const (VPar (toEnd idSrc))) nv -- weeTgt is the only thing to replace
+   bigSrc <- buildNatVal nv'
+   instantiateMeta (InEnd bigTgt) (VNum nv')
+   wire (bigSrc, TNat, NamedPort bigTgt "")
+
+ -- RHS is constant or Src, wire it into tgt
+ (InEnd tgt,  _) -> do
+   src <- buildNatVal nv
+   instantiateMeta (InEnd tgt) (VNum nv)
+   wire (src, TNat, NamedPort tgt "")
  where
-  getNumVar :: NumVal (VVar n) -> Maybe End
-  getNumVar (NumValue _ (StrictMonoFun (StrictMono _ mono))) = case mono of
-    Linear v -> case v of
-      VPar e -> Just e
-      _ -> Nothing
-    Full sm -> getNumVar (numValue sm)
-  getNumVar _ = Nothing
-doesntOccur e (VApp var args) = case var of
-  VPar e' -> collision e e' *> traverse_ (doesntOccur e) args
-  _ -> pure ()
-doesntOccur e (VCon _ args) = traverse_ (doesntOccur e) args
-doesntOccur e (VLam body) = doesntOccur e body
-doesntOccur e (VFun my (ins :->> outs)) = case my of
-  Braty -> doesntOccurRo my e ins *> doesntOccurRo my e outs
-  Kerny -> doesntOccurRo my e ins *> doesntOccurRo my e outs
-doesntOccur e (VSum my rows) = traverse_ (\(Some ro) -> doesntOccurRo my e ro) rows
-
-collision :: End -> End -> Either ErrorMsg ()
-collision e v | e == v = Left . UnificationError $
-                         show e ++ " is cyclic"
-              | otherwise = pure ()
-
-doesntOccurRo :: Modey m -> End -> Ro m i j -> Either ErrorMsg ()
-doesntOccurRo _ _ R0 = pure ()
-doesntOccurRo my e (RPr (_, ty) ro) = doesntOccur e ty *> doesntOccurRo my e ro
-doesntOccurRo Braty e (REx _ ro) = doesntOccurRo Braty e ro
+  vars :: NumVal a -> [a]
+  vars = foldMap pure
 
 -- Need to keep track of which way we're solving - which side is known/unknown
 -- Things which are dynamically unknown must be Tgts - information flows from Srcs
@@ -251,11 +253,9 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro)
     lhsStrictMono (StrictMono (n - 1) mono) num
 
   lhsMono :: Monotone (VVar Z) -> NumVal (VVar Z) -> Checking ()
-  lhsMono (Linear v) num = case v of
-    VPar e -> instantiateMeta e (VNum num)
-    _ -> case num of -- our only hope is to instantiate the RHS
-      NumValue 0 (StrictMonoFun (StrictMono 0 (Linear (VPar (ExEnd e))))) -> instantiateMeta (toEnd e) (VNum (nVar v))
-      _ -> err . UnificationError $ "Couldn't instantiate variable " ++ show v
+  lhsMono (Linear v) (NumValue 0 (StrictMonoFun (StrictMono 0 (Linear v')))) | v == v' = pure ()
+  lhsMono (Linear (VPar e)) num = throwLeft (doesntOccur e (VNum num)) *>
+                                  solveNumMeta e num
   lhsMono (Full sm) (NumValue 0 (StrictMonoFun (StrictMono 0 (Full sm'))))
     = lhsStrictMono sm (NumValue 0 (StrictMonoFun sm'))
   lhsMono m@(Full _) (NumValue 0 gro) = lhsFun00 gro (NumValue 0 (StrictMonoFun (StrictMono 0 m)))
@@ -266,7 +266,7 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro)
   demand0 :: NumVal (VVar Z) -> Checking ()
   demand0 (NumValue 0 Constant0) = pure ()
   demand0 n@(NumValue 0 (StrictMonoFun (StrictMono _ mono))) = case mono of
-    Linear (VPar e) -> instantiateMeta e (VNum (nConstant 0))
+    Linear (VPar e) -> solveNumMeta e (nConstant 0)
     Full sm -> demand0 (NumValue 0 (StrictMonoFun sm))
     _ -> err . UnificationError $ "Couldn't force " ++ show n ++ " to be 0"
   demand0 n = err . UnificationError $ "Couldn't force " ++ show n ++ " to be 0"
@@ -276,9 +276,23 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro)
   --   2^k * x
   -- = 2^k * (y + 1)
   -- = 2^k + 2^k * y
-  demandSucc (StrictMono k (Linear (VPar (ExEnd out)))) = do
-    y <- mkPred out
-    pure $ nPlus ((2 ^ k) - 1) $ n2PowTimes k y
+  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))
   -- = 2^k + 2^(k + 1) * full(n)
@@ -297,53 +311,39 @@ unifyNum (NumValue lup lgro) (NumValue rup rgro)
     evenGro Constant0 = pure Constant0
     evenGro (StrictMonoFun (StrictMono 0 mono)) = case mono of
       Linear (VPar (ExEnd out)) -> do
-        half <- mkHalf out
+        half <- invertNatVal (NumValue 0 (StrictMonoFun (StrictMono 1 mono)))
+        solveNumMeta (ExEnd out) (n2PowTimes 1 (nVar (VPar (toEnd half))))
         pure (StrictMonoFun (StrictMono 0 (Linear (VPar (toEnd half)))))
-      Linear _ -> err . UnificationError $ "Can't force " ++ show n ++ " to be even"
+      Linear (VPar (InEnd tgt)) -> do
+        halfTgt <- buildNatVal (NumValue 0 (StrictMonoFun (StrictMono 1 (Linear (VPar (toEnd tgt))))))
+        let half = nVar (VPar (toEnd halfTgt))
+        solveNumMeta (InEnd tgt) (n2PowTimes 1 half)
+        pure (StrictMonoFun (StrictMono 0 (Linear (VPar (toEnd halfTgt)))))
       Full sm -> StrictMonoFun sm <$ demand0 (NumValue 0 (StrictMonoFun sm))
     evenGro (StrictMonoFun (StrictMono n mono)) = pure (StrictMonoFun (StrictMono (n - 1) mono))
 
     -- Check a numval is odd, and return its rounded down half
     oddGro :: Fun00 (VVar Z) -> Checking (NumVal (VVar Z))
     oddGro (StrictMonoFun (StrictMono 0 mono)) = case mono of
-      Linear (VPar (ExEnd out)) -> mkPred out >>= demandEven
-      Linear _ -> err . UnificationError $ "Can't force " ++ show n ++ " to be even"
+      -- 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
+        solveNumMeta (toEnd doubTgt) (nPlus 1 (n2PowTimes 1 (nVar (VPar (toEnd halfTgt)))))
+        pure (nVar (VPar (toEnd halfTgt)))
+      Linear (VPar (InEnd weeTgt)) -> do
+        -- compute (/2) . (-1)
+        bigTgt <- invertNatVal (NumValue 1 (StrictMonoFun (StrictMono 1 (Linear (VPar (toEnd weeTgt))))))
+        let flooredHalf = nVar (VPar (toEnd weeTgt))
+        solveNumMeta (toEnd bigTgt) (nPlus 1 (n2PowTimes 1 flooredHalf))
+        pure flooredHalf
+
       -- full(n + 1) = 1 + 2 * full(n)
       -- hence, full(n) is the rounded down half
       Full sm -> nFull <$> demandSucc sm
     oddGro _ = err . UnificationError $ "Can't force " ++ show n ++ " to be even"
 
-  -- Add dynamic logic to compute half of a variable.
-  mkHalf :: OutPort -> Checking Src
-  mkHalf out = do
-    (_, [], [(const2,_)], _) <- next "const2" (Const (Num 2)) (S0, Some (Zy :* S0))
-                                R0
-                                (RPr ("value", TNat) R0)
-    (_, [(lhs,_),(rhs,_)], [(half,_)], _) <- next "div2" (ArithNode Div) (S0, Some (Zy :* S0))
-                                             (RPr ("left", TNat) (RPr ("right", TNat) R0))
-                                             (RPr ("out", TNat) R0)
-    wire (NamedPort out "numerator", TNat, lhs)
-    wire (const2, TNat, rhs)
-    req $ Define (toEnd out) (VNum (n2PowTimes 1 (nVar (VPar (toEnd half)))))
-    pure half
-
-
-  -- Add dynamic logic to compute the predecessor of a variable, and return that
-  -- predecessor.
-  -- The variable must be a non-zero nat!!
-  mkPred :: OutPort -> Checking (NumVal (VVar Z))
-  mkPred out = do
-    (_, [], [(const1,_)], _) <- next "const1" (Const (Num 1)) (S0, Some (Zy :* S0))
-                                R0
-                                (RPr ("value", TNat) R0)
-    (_, [(lhs,_),(rhs,_)], [(pred,_)], _) <- next "minus1" (ArithNode Sub) (S0, Some (Zy :* S0))
-                                             (RPr ("left", TNat) (RPr ("right", TNat) R0))
-                                             (RPr ("out", TNat) R0)
-    wire (NamedPort out "", TNat, lhs)
-    wire (const1, TNat, rhs)
-    req $ Define (ExEnd out) (VNum (nPlus 1 (nVar (VPar (toEnd pred)))))
-    pure (nVar (VPar (toEnd pred)))
-
 -- The variable must be a non-zero nat!!
 patVal :: ValPat -> [End] -> (Val Z, [End])
 -- Nat variables will only be found in a `NumPat`, not a `ValPat`
diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs
index da34e09b..5a4ed219 100644
--- a/brat/Brat/Elaborator.hs
+++ b/brat/Brat/Elaborator.hs
@@ -91,6 +91,7 @@ elaborate (WC fc x) = do
 
 elaborate' :: Flat -> Either Error SomeRaw'
 elaborate' (FVar x) = pure $ SomeRaw' (RVar x)
+elaborate' FHope = pure $ SomeRaw' RHope
 elaborate' (FArith op a b) = do
   (SomeRaw a) <- elaborate a
   (SomeRaw b) <- elaborate b
diff --git a/brat/Brat/Error.hs b/brat/Brat/Error.hs
index f34dba14..fc8a841f 100644
--- a/brat/Brat/Error.hs
+++ b/brat/Brat/Error.hs
@@ -83,6 +83,7 @@ data ErrorMsg
  -- The argument is the row of unused connectors
  | ThunkLeftOvers String
  | ThunkLeftUnders String
+ | RemainingNatHopes [String]
 
 instance Show ErrorMsg where
   show (TypeErr x) = "Type error: " ++ x
@@ -166,7 +167,7 @@ instance Show ErrorMsg where
   show UnreachableBranch = "Branch cannot be reached"
   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
-
+  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 52fff0e8..f9ae33d3 100644
--- a/brat/Brat/Eval.hs
+++ b/brat/Brat/Eval.hs
@@ -4,22 +4,27 @@ module Brat.Eval (EvMode(..)
                  ,ValPat(..)
                  ,NumPat(..)
                  ,apply
+                 ,applySem
                  ,eval
                  ,sem
+                 ,semLvl
+                 ,doesntOccur
                  ,evalCTy
                  ,eqTest
+                 ,getNum
                  ,kindEq
+                 ,kindOf
                  ,kindType
                  ,numVal
-                 ,typeEq
+                 ,quote
                  ) where
 
 import Brat.Checker.Monad
 import Brat.Checker.Types (EndType(..), kindForMode)
 import Brat.Error (ErrorMsg(..))
 import Brat.QualName (plain)
-import Brat.Syntax.Value
 import Brat.Syntax.Common
+import Brat.Syntax.Value
 import Control.Monad.Freer (req)
 import Bwd
 import Hasochism
@@ -29,6 +34,7 @@ import Data.Bifunctor (second)
 import Data.Functor
 import Data.Kind (Type)
 import Data.Type.Equality (TestEquality(..), (:~:)(..))
+import Data.Foldable (traverse_)
 
 kindType :: TypeKind -> Val Z
 kindType Nat = TNat
@@ -191,14 +197,8 @@ kindOf (VPar e) = req (TypeOf e) >>= \case
     Kerny -> show ty
 kindOf (VInx n) = case n of {}
 
--- We should have made sure that the two values share the given kind
-typeEq :: String -- String representation of the term for error reporting
-   -> TypeKind -- The kind we're comparing at
-   -> Val Z -- Expected
-   -> Val Z -- Actual
-   -> Checking ()
-typeEq str k exp act = eqTest str k exp act >>= throwLeft
-
+-------- for SolvePatterns usage: not allowed to solve hopes,
+-- and if pattern insoluble, it's not a type error (it's a "pattern match case unreachable")
 eqTest :: String -- String representation of the term for error reporting
        -> TypeKind -- The kind we're comparing at
        -> Val Z -- Expected
@@ -256,10 +256,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
@@ -300,3 +297,36 @@ eqTests tm lvkz = go
     Left e -> pure $ Left e
   go _ us vs = pure . Left . TypeErr $ "Arity mismatch in type constructor arguments:\n  "
                    ++ show us ++ "\n  " ++ show vs
+
+-- Be conservative, fail if in doubt. Not dangerous like being wrong while succeeding
+-- We can have bogus failures here because we're not normalising under lambdas
+-- N.B. the value argument is normalised.
+doesntOccur :: End -> Val n -> Either ErrorMsg ()
+doesntOccur e (VNum nv) = traverse_ (collision e) (getNumVar nv)
+ where
+  getNumVar :: NumVal (VVar n) -> Maybe End
+  getNumVar (NumValue _ (StrictMonoFun (StrictMono _ mono))) = case mono of
+    Linear v -> case v of
+      VPar e -> Just e
+      _ -> Nothing
+    Full sm -> getNumVar (numValue sm)
+  getNumVar _ = Nothing
+doesntOccur e (VApp var args) = case var of
+  VPar e' -> collision e e' *> traverse_ (doesntOccur e) args
+  _ -> pure ()
+doesntOccur e (VCon _ args) = traverse_ (doesntOccur e) args
+doesntOccur e (VLam body) = doesntOccur e body
+doesntOccur e (VFun my (ins :->> outs)) = case my of
+  Braty -> doesntOccurRo my e ins *> doesntOccurRo my e outs
+  Kerny -> doesntOccurRo my e ins *> doesntOccurRo my e outs
+doesntOccur e (VSum my rows) = traverse_ (\(Some ro) -> doesntOccurRo my e ro) rows
+
+collision :: End -> End -> Either ErrorMsg ()
+collision e v | e == v = Left . UnificationError $
+                         show e ++ " is cyclic"
+              | otherwise = pure ()
+
+doesntOccurRo :: Modey m -> End -> Ro m i j -> Either ErrorMsg ()
+doesntOccurRo _ _ R0 = pure ()
+doesntOccurRo my e (RPr (_, ty) ro) = doesntOccur e ty *> doesntOccurRo my e ro
+doesntOccurRo Braty e (REx _ ro) = doesntOccurRo Braty e ro
diff --git a/brat/Brat/Lexer/Flat.hs b/brat/Brat/Lexer/Flat.hs
index 1f41d5ba..30fd6f62 100644
--- a/brat/Brat/Lexer/Flat.hs
+++ b/brat/Brat/Lexer/Flat.hs
@@ -87,6 +87,7 @@ tok = try (char '(' $> LParen)
       <|> try (string "-" $> Minus)
       <|> try (string "$" $> Dollar)
       <|> try (string "|" $> Pipe)
+      <|> try (string "!" $> Bang)
       <|> try (K <$> try keyword)
       <|> try qualified
       <|> Ident <$> ident
diff --git a/brat/Brat/Lexer/Token.hs b/brat/Brat/Lexer/Token.hs
index d5f8842b..80dca83b 100644
--- a/brat/Brat/Lexer/Token.hs
+++ b/brat/Brat/Lexer/Token.hs
@@ -43,6 +43,7 @@ data Tok
  | Dollar
  | Underscore
  | Pipe
+ | Bang
  | Cons
  | Snoc
  | ConcatEqEven
@@ -88,6 +89,7 @@ instance Show Tok where
   show Dollar = "$"
   show Underscore = "_"
   show Pipe = "|"
+  show Bang = "!"
   show Cons = ",-"
   show Snoc = "-,"
   show ConcatEqEven = "=,="
diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs
index 494f193b..087a406a 100644
--- a/brat/Brat/Parser.hs
+++ b/brat/Brat/Parser.hs
@@ -515,6 +515,7 @@ expr' p = choice $ (try . getParser <$> enumFrom p) ++ [atomExpr]
               <|> var
               <|> match Underscore $> FUnderscore
               <|> match Pipe $> FIdentity
+              <|> match Bang $> FHope
 
 
 cnoun :: Parser Flat -> Parser (WC (Raw 'Chk 'Noun))
diff --git a/brat/Brat/Syntax/Common.hs b/brat/Brat/Syntax/Common.hs
index dacd8d1b..622c598d 100644
--- a/brat/Brat/Syntax/Common.hs
+++ b/brat/Brat/Syntax/Common.hs
@@ -111,7 +111,7 @@ instance Eq ty => Eq (TypeRowElem ty) where
   Anon ty == Anon ty' = ty == ty'
 
 data TypeKind = TypeFor Mode [(PortName, TypeKind)] | Nat | Row
-  deriving (Eq, Show)
+  deriving (Eq, Ord, Show)
 
 pattern Star, Dollar :: [(PortName, TypeKind)] -> TypeKind
 pattern Star ks = TypeFor Brat ks
diff --git a/brat/Brat/Syntax/Concrete.hs b/brat/Brat/Syntax/Concrete.hs
index d2d567f6..3e07bb44 100644
--- a/brat/Brat/Syntax/Concrete.hs
+++ b/brat/Brat/Syntax/Concrete.hs
@@ -22,6 +22,7 @@ type FEnv = ([FDecl], [RawAlias])
 
 data Flat
  = FVar QualName
+ | FHope
  | FApp (WC Flat) (WC Flat)
  | FJuxt (WC Flat) (WC Flat)
  | FThunk (WC Flat)
diff --git a/brat/Brat/Syntax/Core.hs b/brat/Brat/Syntax/Core.hs
index d3c30cff..c9dbd046 100644
--- a/brat/Brat/Syntax/Core.hs
+++ b/brat/Brat/Syntax/Core.hs
@@ -49,6 +49,7 @@ data Term :: Dir -> Kind -> Type where
   Pull     :: [PortName] -> WC (Term Chk k) -> Term Chk k
   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
 
@@ -113,8 +114,10 @@ instance Show (Term d k) where
                           ,"of"
                           ,bracket POf e
                           ]
+
   show (Var x) = show x
   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 ca26fa79..62934f1b 100644
--- a/brat/Brat/Syntax/Raw.hs
+++ b/brat/Brat/Syntax/Raw.hs
@@ -71,6 +71,7 @@ data Raw :: Dir -> Kind -> Type where
   RPull     :: [PortName] -> WC (Raw Chk k) -> Raw Chk k
   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
@@ -102,6 +103,7 @@ instance Show (Raw d k) where
     = unwords ["let", show abs, "=", show xs, "in", show body]
   show (RNHole name) = '?':name
   show (RVHole name) = '?':name
+  show RHope = "!"
   show (RSimple tm) = show tm
   show RPass = show "pass"
   show REmpty = "()"
@@ -201,6 +203,7 @@ instance (Kindable k) => Desugarable (Raw d k) where
   -- TODO: holes need to know their arity for type checking
   desugar' (RNHole strName) = NHole . (strName,) <$> freshM strName
   desugar' (RVHole strName) = VHole . (strName,) <$> freshM strName
+  desugar' RHope = pure Hope
   desugar' RPass = pure Pass
   desugar' (RSimple simp) = pure $ Simple simp
   desugar' REmpty = pure Empty
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 58a29efa..a7d22664 100644
--- a/brat/brat.cabal
+++ b/brat/brat.cabal
@@ -66,6 +66,7 @@ library
                        Brat.Checker.Helpers,
                        Brat.Checker.Helpers.Nodes,
                        Brat.Checker.Monad,
+                       Brat.Checker.SolveHoles,
                        Brat.Checker.SolvePatterns,
                        Brat.Checker.Types,
                        Brat.Compile.Hugr,
diff --git a/brat/examples/infer.brat b/brat/examples/infer.brat
new file mode 100644
index 00000000..dacdb0a7
--- /dev/null
+++ b/brat/examples/infer.brat
@@ -0,0 +1,7 @@
+map(X :: *, Y :: *, { X -> Y }, List(X)) -> List(Y)
+map(_, _, _, []) = []
+map(_, _, f, x ,- xs) = f(x) ,- map(!, !, f, xs)
+
+mapVec(X :: *, Y :: *, { X -> Y }, n :: #, Vec(X, n)) -> Vec(Y, n)
+mapVec(_, _, _, _, []) = []
+mapVec(_, _, f, _, x ,- xs) = f(x) ,- mapVec(!, !, f, !, xs)
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/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/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
+
+