diff --git a/brat/Brat/Checker.hs b/brat/Brat/Checker.hs
index 3b317be0..8a0ecd94 100644
--- a/brat/Brat/Checker.hs
+++ b/brat/Brat/Checker.hs
@@ -38,6 +38,7 @@ import Brat.Naming
 import Brat.QualName
 -- import Brat.Search
 import Brat.Syntax.Abstractor (NormalisedAbstractor(..), normaliseAbstractor)
+import Brat.Syntax.CircuitProperties (CircuitProperties(..), Properties)
 import Brat.Syntax.Common
 import Brat.Syntax.Core
 import Brat.Syntax.FuncDecl (FunBody(..))
@@ -174,6 +175,7 @@ check :: (CheckConstraints m k
          ,EvMode m
          ,TensorOutputs (Outputs m d)
          ,?my :: Modey m
+         ,?props :: Properties m
          , DIRY d)
       => WC (Term d k)
       -> ChkConnectors m d k
@@ -186,6 +188,7 @@ check' :: forall m d k
           ,EvMode m
           ,TensorOutputs (Outputs m d)
           ,?my :: Modey m
+          ,?props :: Properties m
           , DIRY d)
        => Term d k
        -> ChkConnectors m d k
@@ -218,7 +221,7 @@ check' (Lambda c@(WC abstFC abst,  body) cs) (overs, unders) = do
       -- We'll check the first variant against a Hypo node (omitted from compilation)
       -- to work out how many overs/unders it needs, and then check it again (in Chk)
       -- with the other clauses, as part of the body.
-      (ins :->> outs) <- mkSig usedOvers unders
+      (FunTy _ ins outs) <- mkSig usedOvers unders
       (allFakeUnders, rightFakeUnders, tgtMap) <- suppressHoles $ suppressGraph $ do
         (_, [], fakeOvers, fakeAcc) <- anext "lambda_fake_source" Hypo (S0, Some (Zy :* S0)) R0 ins
         -- Hypo `check` calls need an environment, even just to compute leftovers;
@@ -264,10 +267,11 @@ check' (Lambda c@(WC abstFC abst,  body) cs) (overs, unders) = do
   portNamesToBoundNames :: [(String, (Src, BinderType m))] -> [(String, (Src, BinderType m))]
   portNamesToBoundNames = fmap (\(n, (src, ty)) -> (n, (NamedPort (end src) n, ty)))
 
-  mkSig :: ToEnd t => [(Src, BinderType m)] -> [(NamedPort t, BinderType m)] -> Checking (CTy m Z)
+  mkSig :: ToEnd t => [(Src, BinderType m)] -> [(NamedPort t, BinderType m)] -> Checking (FunTy m Z)
   mkSig overs unders = rowToRo ?my (retuple <$> overs) S0 >>=
     \(Some (inRo :* endz)) -> rowToRo ?my (retuple <$> unders) endz >>=
-      \(Some (outRo :* _)) -> pure (inRo :->> outRo)
+      \(Some (outRo :* _)) -> pure (FunTy ?props inRo outRo)
+
 
   retuple (NamedPort e p, ty) = (p, e, ty)
 
@@ -275,7 +279,7 @@ check' (Lambda c@(WC abstFC abst,  body) cs) (overs, unders) = do
     Nothing -> err $ InternalError "Trying to wire up different sized lists of wires"
     Just conns -> traverse (\((src, ty), (tgt, _)) -> wire (src, binderToValue ?my ty, tgt)) conns
 
-  checkClauses cty@(ins :->> outs) overs all_cs = do
+  checkClauses cty@(FunTy _ ins outs) overs all_cs = do
     let clauses = NE.zip (NE.fromList [0..]) all_cs <&>
             \(i, (abs, tm)) -> Clause i (normaliseAbstractor <$> abs) tm
     clauses <- traverse (checkClause ?my "lambda" cty) clauses
@@ -289,7 +293,7 @@ check' (Pull ports t) (overs, unders) = do
   unders <- pullPortsRow ports unders
   check t (overs, unders)
 check' (t ::: outs) (overs, ()) | Braty <- ?my = do
-  (ins :->> outs) :: CTy Brat Z <- kindCheckAnnotation Braty ":::" outs
+  (ins :->> outs) :: FunTy Brat Z <- kindCheckAnnotation Braty () ":::" outs
   (_, hungries, danglies, _) <- next "id" Id (S0,Some (Zy :* S0)) ins outs
   ((), leftOvers) <- noUnders $ check t (overs, hungries)
   pure (((), danglies), (leftOvers, ()))
@@ -312,13 +316,13 @@ check' (Th tm) ((), u@(hungry, ty):unders) = case (?my, ty) of
   checkThunk :: forall m. (CheckConstraints m UVerb, EvMode m)
            => Modey m
            -> String
-           -> CTy m Z
+           -> FunTy m Z
            -> WC (Term Chk UVerb)
            -> Checking Src
-  checkThunk m name cty tm = do
+  checkThunk m name cty@(FunTy props _ _) tm = do
     ((dangling, _), ()) <- let ?my = m in makeBox name cty $
       \(thOvers, thUnders) -> do
-        (((), ()), leftovers) <- check tm (thOvers, thUnders)
+        (((), ()), leftovers) <- let ?props = props in check tm (thOvers, thUnders)
         case leftovers of
           ([], []) -> pure ()
           ([], unders) -> err (ThunkLeftUnders (showRow unders))
@@ -332,34 +336,38 @@ check' (TypedTh t) ((), ()) = case ?my of
   Braty -> do
     -- but the computation in it could be either Brat or Kern
     brat <- catchErr $ check t ((), ())
-    kern <- catchErr $ let ?my = Kerny in check t ((), ())
+    -- TODO: What if the programmer intends a less strict kernel type?
+    let props = PControllable
+    kern <- catchErr $ let ?my = Kerny in let ?props = props in check t ((), ())
     case (brat, kern) of
       (Left e, Left _) -> req $ Throw e -- pick an error arbitrarily
       -- I don't believe that there is any syntax that could synthesize
       -- both a classical type and a kernel type, but just in case:
       -- (pushing down Emb(TypedTh(v)) to Thunk(Emb+Forget(v)) would help in Checkable cases)
       (Right _, Right _) -> typeErr "TypedTh could be either Brat or Kernel"
-      (Left _, Right (conns, ((), ()))) -> let ?my = Kerny in createThunk conns
-      (Right (conns, ((), ())), Left _) -> createThunk conns
+      (Left _, Right (conns, ((), ()))) -> let ?my = Kerny in createThunk props conns
+      (Right (conns, ((), ())), Left _) -> createThunk () conns
  where
   createThunk :: (CheckConstraints m2 Noun, ?my :: Modey m2, EvMode m2)
-              => SynConnectors m2 Syn KVerb
+              => Properties m2
+              -> SynConnectors m2 Syn KVerb
               -> Checking (SynConnectors Brat Syn Noun
                           ,ChkConnectors Brat Syn Noun)
-  createThunk (ins, outs) = do
+  createThunk ps (ins, outs) = do
     Some (ez :* inR) <- mkArgRo ?my S0 (first (fmap toEnd) <$> ins)
     Some (_ :* outR) <- mkArgRo ?my ez (first (fmap toEnd) <$> outs)
-    (thunkOut, ()) <- makeBox "thunk" (inR :->> outR) $
+    (thunkOut, ()) <- makeBox "thunk" (FunTy ps inR outR) $
         \(thOvers, thUnders) -> do
           -- if these ensureEmpty's fail then its a bug!
           checkInputs t thOvers ins >>= ensureEmpty "TypedTh inputs"
           checkOutputs t thUnders outs >>= ensureEmpty "TypedTh outputs"
     pure (((), [thunkOut]), ((), ()))
 check' (Force th) ((), ()) = do
-  (((), outs), ((), ())) <- let ?my = Braty in check th ((), ())
+  (((), outs), ((), ())) <- let ?my = Braty in let ?props = () in check th ((), ())
   -- pull a bunch of thunks (only!) out of here
-  (_, thInputs, thOutputs) <- getThunks ?my outs
+  (_, thInputs, thOutputs) <- getThunks ?my ?props outs
   pure ((thInputs, thOutputs), ((), ()))
+
 check' (Forget kv) (overs, unders) = do
   ((ins, outs), ((), rightUnders)) <- check kv ((), unders)
   leftOvers <- checkInputs kv overs ins
@@ -384,9 +392,9 @@ check' (Arith op l r) ((), u@(hungry, ty):unders) = case (?my, ty) of
     let inRo = RPr ("left", ty) $ RPr ("right", ty) R0
     let outRo = RPr ("out", ty) R0
     (_, [lunders, runders], [(dangling, _)], _) <- next (show op) (ArithNode op) (S0, Some $ Zy :* S0) inRo outRo
-    (((), ()), ((), leftUnders)) <- check l ((), [lunders])
+    (((), ()), ((), leftUnders)) <- let ?props = () in check l ((), [lunders])
     ensureEmpty "arith unders" leftUnders
-    (((), ()), ((), leftUnders)) <- check r ((), [runders])
+    (((), ()), ((), leftUnders)) <- let ?props = () in check r ((), [runders])
     ensureEmpty "arith unders" leftUnders
     wire (dangling, ty, hungry)
     pure (((), ()), ((), unders))
@@ -684,13 +692,13 @@ data Clause = Clause
 -- refined overs)
 checkClause :: forall m. (CheckConstraints m UVerb, EvMode m) => Modey m
             -> String
-            -> CTy m Z
+            -> FunTy m Z
             -> Clause
             -> Checking
                ( TestMatchData m -- TestMatch data (LHS)
                , Name   -- Function node (RHS)
                )
-checkClause my fnName cty clause = modily my $ do
+checkClause my fnName cty@(FunTy props _ _) clause = modily my $ do
   let clauseName = fnName ++ "." ++ show (index clause)
 
   -- First, we check the patterns on the LHS. This requires some overs,
@@ -708,14 +716,14 @@ checkClause my fnName cty clause = modily my $ do
     Some (_ :* outRo) <- mkArgRo my patEz (first (fmap toEnd) <$> unders)
     let match = TestMatchData my $ MatchSequence overs tests (snd <$> sol)
     let vars = fst <$> sol
-    pure (vars, match, patRo :->> outRo)
+    pure (vars, match, FunTy props patRo outRo)
 
   -- Now actually make a box for the RHS and check it
   ((boxPort, _ty), _) <- let ?my = my in makeBox (clauseName ++ "_rhs") rhsCty $ \(rhsOvers, rhsUnders) -> do
     let abstractor = foldr ((:||:) . APat . Bind) AEmpty vars
     let ?my = my in do
       env <- abstractAll rhsOvers abstractor
-      localEnv env $ check @m (rhs clause) ((), rhsUnders)
+      localEnv env $ let ?props = props in check @m (rhs clause) ((), rhsUnders)
   let NamedPort {end=Ex rhsNode _} = boxPort
   pure (match, rhsNode)
 
@@ -724,9 +732,9 @@ checkClause my fnName cty clause = modily my $ do
 checkBody :: (CheckConstraints m UVerb, EvMode m, ?my :: Modey m)
           => String -- The function name
           -> FunBody Term UVerb
-          -> CTy m Z -- Function type
+          -> FunTy m Z -- Function type
           -> Checking Src
-checkBody fnName body cty = do
+checkBody fnName body cty@(FunTy props _ _) = do
   (tm, (absFC, tmFC)) <- case body of
     NoLhs tm -> pure (tm, (fcOf tm, fcOf tm))
     Clauses (c@(abs, tm) :| cs) -> do
@@ -734,7 +742,7 @@ checkBody fnName body cty = do
       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
+    (((), ()), leftovers) <- let ?props = props in check tm conns
     case leftovers of
       ([], []) -> pure ()
       ([], rightUnders) -> localFC tmFC $
@@ -825,14 +833,14 @@ kindCheck ((hungry, Star []):unders) (C (ss :-> ts)) = do
         let val = VFun Braty (inRo :->> outRo)
         defineTgt hungry val
         pure ([val], unders)
-kindCheck ((hungry, Star []):unders) (K (ss :-> ts)) = do
+kindCheck ((hungry, Star []):unders) (K ps (ss :-> ts)) = do
   -- N.B. Kernels can't bind so we don't need to pass around a stack of ends
   ss <- kindCheckRow Kerny "" ss
   ts <- kindCheckRow Kerny "" ts
   case (ss, ts) of
     (Some ss, Some ts) -> case kernelNoBind ss of
       Refl -> do
-        let val = VFun Kerny (ss :->> ts)
+        let val = VFun Kerny (FunTy ps ss ts)
         defineTgt hungry val
         pure ([val], unders)
 
@@ -930,10 +938,11 @@ kindCheckRow my name r = do
 -- Checks that an annotation is a valid row, returning the
 -- evaluation of the type of an Id node passing through such values
 kindCheckAnnotation :: Modey m
+                    -> Properties m
                     -> String -- for node name
                     -> [(PortName, ThunkRowType m)]
-                    -> Checking (CTy m Z)
-kindCheckAnnotation my name outs = do
+                    -> Checking (FunTy m Z)
+kindCheckAnnotation my ps name outs = do
   trackM "kca"
   name <- req (Fresh $ "__kca_" ++ name)
   kindCheckRow' my (Zy :* S0) M.empty (name, 0) outs >>= \case
@@ -944,7 +953,7 @@ kindCheckAnnotation my name outs = do
       -- but persuades the Haskell typechecker it's ok to use the copy
       -- as return types (that happen not to mention the argument types).
       case varChangerThroughRo (ParToInx (AddZ n) s) ins of
-        Some (_ :* outs) -> pure (ins :->> outs)
+        Some (_ :* outs) -> pure (FunTy ps ins outs)
 
 kindCheckRow' :: forall m n
                . Modey m
diff --git a/brat/Brat/Checker/Helpers.hs b/brat/Brat/Checker/Helpers.hs
index 9b0871e5..2d3b8419 100644
--- a/brat/Brat/Checker/Helpers.hs
+++ b/brat/Brat/Checker/Helpers.hs
@@ -6,7 +6,6 @@ module Brat.Checker.Helpers {-(pullPortsRow, pullPortsSig
                             ,ensureEmpty, noUnders
                             ,rowToSig
                             ,showMode, getVec
-                            ,mkThunkTy
                             ,wire
                             ,next, knext, anext
                             ,kindType, getThunks
@@ -27,7 +26,8 @@ import Brat.Eval (eval, EvMode(..), kindType)
 import Brat.FC (FC)
 import Brat.Graph (Node(..), NodeType(..))
 import Brat.Naming (Name, FreshMonad(..))
-import Brat.Syntax.Common
+import Brat.Syntax.CircuitProperties (CircuitProperties(..), Properties)
+import Brat.Syntax.Common hiding (pattern PNone)
 import Brat.Syntax.Core (Term(..))
 import Brat.Syntax.Simple
 import Brat.Syntax.Port (ToEnd(..))
@@ -36,6 +36,7 @@ import Bwd
 import Hasochism
 import Util (log2)
 
+import Control.Monad (when)
 import Control.Monad.State.Lazy (StateT(..), runStateT)
 import Control.Monad.Freer (req)
 import Data.Bifunctor
@@ -149,15 +150,6 @@ type family ThunkRowType (m :: Mode) where
   ThunkRowType Brat = KindOr (Term Chk Noun)
   ThunkRowType Kernel = Term Chk Noun
 
-mkThunkTy :: Modey m
-          -> ThunkFCType m
-          -> [(PortName, ThunkRowType m)]
-          -> [(PortName, ThunkRowType m)]
-          -> Term Chk Noun
--- mkThunkTy Braty fc ss ts = C (WC fc (ss :-> ts))
-mkThunkTy Braty _ ss ts = C (ss :-> ts)
-mkThunkTy Kerny () ss ts = K (ss :-> ts)
-
 anext :: forall m i j k
        . EvMode m
       => String
@@ -238,38 +230,56 @@ wire (src, ty, tgt) = do
 -- This is the dual notion to the overs and unders used for typechecking against
 -- Hence, we return them here in the opposite order to `check`'s connectors
 getThunks :: Modey m
+          -> Properties m
           -> [(Src, BinderType Brat)] -- A row of 0 or more function types in the same mode
           -> Checking ([Name]
                       ,Unders m Chk
                       ,Overs m UVerb
                       )
-getThunks _ [] = pure ([], [], [])
-getThunks Braty ((src, Right ty):rest) = do
+getThunks _ _ [] = pure ([], [], [])
+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
+  (nodes, unders', overs') <- getThunks Braty () rest
   pure (node:nodes, unders <> unders', overs <> overs')
-getThunks Kerny ((src, Right ty):rest) = do
+getThunks Kerny expectedProps ((src, Right ty):rest) = do
   ty <- eval S0 ty
-  (src, ss :->> ts) <- vectorise Kerny (src,ty)
+  (src, sig@(FunTy props ss ts)) <- vectorise Kerny (src,ty)
+  when (props < expectedProps)
+    (err (TypeErr (unwords ["Expected all kernel types to be"
+                           ,expected expectedProps
+                           ,"but kernel with signature"
+                           ,show sig
+                           ,"was"
+                           ,actual props
+                           ])))
   (node, unders, overs, _) <- let ?my = Kerny in anext "Splice" (Splice (end src)) (S0, Some (Zy :* S0)) ss ts
-  (nodes, unders', overs') <- getThunks Kerny rest
+  (nodes, unders', overs') <- getThunks Kerny props rest
   pure (node:nodes, unders <> unders', overs <> overs')
-getThunks Braty ((src, Left (Star args)):rest) = do
+ where
+  expected PControllable = "controllable and reversible"
+  expected PReversible = "reversible"
+  expected _ = undefined
+
+  actual PNone = "neither"
+  actual PReversible = "just reversible, not controllable"
+  actual _ = undefined
+
+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" (Eval (end src)) (S0, Some (Zy :* S0)) ri ro
       pure (node, unders, overs)
-  (nodes, unders', overs') <- getThunks Braty rest
+  (nodes, unders', overs') <- getThunks Braty () rest
   pure (node:nodes, unders <> unders', overs <> overs')
-getThunks m ro = err $ ExpectedThunk (showMode m) (showRow ro)
+getThunks m _ ro = err $ ExpectedThunk (showMode m) (showRow ro)
 
 -- The type given here should be normalised
 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
+                                          ,FunTy m Z -- The function type at the end
                                           )
 vecLayers my (TVec ty (VNum n)) = do
   src <- mkStaticNum n
@@ -324,14 +334,14 @@ mkStaticNum n@(NumValue c gro) = do
     wire (oneSrc, TNat, rhs)
     pure src
 
-vectorise :: forall m. Modey m -> (Src, Val Z) -> Checking (Src, CTy m Z)
+vectorise :: forall m. Modey m -> (Src, Val Z) -> Checking (Src, FunTy m Z)
 vectorise my (src, ty) = do
   (layers, cty) <- vecLayers my ty
   modily my $ foldrM mkMapFun (src, cty) layers
  where
   mkMapFun :: (Src, NumVal (VVar Z)) -- Layer to apply
-            -> (Src, CTy m Z) -- The input to this level of mapfun
-            -> Checking (Src, CTy m Z)
+            -> (Src, FunTy m Z) -- The input to this level of mapfun
+            -> Checking (Src, FunTy m Z)
   mkMapFun (lenSrc, len) (valSrc, cty) = do
     let weak1 = changeVar (Thinning (ThDrop ThNull))
     vecFun <- vectorisedFun len my cty
@@ -342,17 +352,17 @@ vectorise my (src, ty) = do
     defineTgt lenTgt (VNum len)
     wire (lenSrc, kindType Nat, lenTgt)
     wire (valSrc, ty, valTgt)
-    let vecCTy = case (my,my',cty) of
+    let vecFunTy = 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)
+    pure (vectorSrc, vecFunTy)
 
-  vectorisedFun :: NumVal (VVar Z) -> Modey m -> CTy m Z -> Checking (Val Z)
-  vectorisedFun nv my (ss :->> ts) = do
+  vectorisedFun :: NumVal (VVar Z) -> Modey m -> FunTy m Z -> Checking (Val Z)
+  vectorisedFun nv my (FunTy ps ss ts) = do
     (ss', ny) <- vectoriseRo True nv Zy ss
     (ts', _)  <- vectoriseRo False nv ny ts
-    pure $ modily my $ VFun my (ss' :->> ts')
+    pure $ modily my $ VFun my (FunTy ps ss' ts')
 
   -- We don't allow existentials in vectorised functions, so the boolean says
   -- whether we are in the input row and can allow binding
@@ -394,10 +404,10 @@ declareTgt tgt my ty = req (Declare (InEnd (end tgt)) my ty)
 -- Build a box corresponding to the inside of a thunk
 makeBox :: (?my :: Modey m, EvMode m)
         => String -- A label for the nodes we create
-        -> CTy m Z
+        -> FunTy m Z
         -> ((Overs m UVerb, Unders m Chk) -> Checking a) -- checks + builds the body using srcs/tgts from the box
         -> Checking ((Src, BinderType Brat), a)
-makeBox name cty@(ss :->> ts) body = do
+makeBox name cty@(FunTy _ ss ts) body = do
   (src, _, overs, ctx) <- anext (name ++ "/in") Source (S0, Some (Zy :* S0)) R0 ss
   (tgt, unders, _, _) <- anext (name ++ "/out") Target ctx ts R0
   case (?my, body) of
diff --git a/brat/Brat/Checker/SolveHoles.hs b/brat/Brat/Checker/SolveHoles.hs
index d26361dd..fd74afa7 100644
--- a/brat/Brat/Checker/SolveHoles.hs
+++ b/brat/Brat/Checker/SolveHoles.hs
@@ -5,6 +5,7 @@ import Brat.Checker.Monad
 import Brat.Checker.Types (kindForMode)
 import Brat.Error (ErrorMsg(..))
 import Brat.Eval
+import Brat.Syntax.CircuitProperties (eqProps)
 import Brat.Syntax.Common
 import Brat.Syntax.Simple (SimpleTerm(..))
 import Brat.Syntax.Value
@@ -159,7 +160,9 @@ typeEqRigid tm lvkz (TypeFor m []) (VCon c args) (VCon c' args') | c == c' =
         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
+typeEqRigid tm lvkz (Star []) (VFun m0 (FunTy ps0 ins0 outs0)) (VFun m1 (FunTy ps1 ins1 outs1))
+ | Just Refl <- testEquality m0 m1
+ , eqProps m0 ps0 ps1 = 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
diff --git a/brat/Brat/Checker/SolvePatterns.hs b/brat/Brat/Checker/SolvePatterns.hs
index 7339157d..48e3261f 100644
--- a/brat/Brat/Checker/SolvePatterns.hs
+++ b/brat/Brat/Checker/SolvePatterns.hs
@@ -24,6 +24,8 @@ import Data.Maybe (fromJust)
 import Data.Type.Equality ((:~:)(..), testEquality)
 import Brat.Syntax.Port (toEnd)
 
+--import Debug.Trace
+
 -- Refine clauses from function definitions (and potentially future case statements)
 -- by processing each one in sequence. This will involve repeating tests for various
 -- branches, the removal of which is a future optimisation.
@@ -203,6 +205,7 @@ instantiateMeta e val = do
 -- Things which are dynamically unknown must be Tgts - information flows from Srcs
 -- ...But we don't need to do any wiring here, right?
 unifyNum :: NumVal (VVar Z) -> NumVal (VVar Z) -> Checking ()
+--unifyNum nv nv' | trace ("unifyNum\n " ++ show nv ++ "\n " ++ show nv') False = undefined
 unifyNum (NumValue lup lgro) (NumValue rup rgro)
   | lup <= rup = lhsFun00 lgro (NumValue (rup - lup) rgro)
   | otherwise  = lhsFun00 rgro (NumValue (lup - rup) lgro)
diff --git a/brat/Brat/Compile/Hugr.hs b/brat/Brat/Compile/Hugr.hs
index 67f6413b..477572c5 100644
--- a/brat/Brat/Compile/Hugr.hs
+++ b/brat/Brat/Compile/Hugr.hs
@@ -13,7 +13,7 @@ import Brat.Constructors.Patterns (pattern CFalse, pattern CTrue)
 import Brat.Checker.Monad (track, trackM, CheckingSig(..))
 import Brat.Checker.Helpers (binderToValue)
 import Brat.Checker.Types (Store(..), VEnv)
-import Brat.Eval (eval, evalCTy, kindType)
+import Brat.Eval (eval, evalFunTy, kindType)
 import Brat.Graph hiding (lookupNode)
 import Brat.Naming
 import Brat.QualName
@@ -137,10 +137,11 @@ runCheckingInCompile (Req _ _) = error "Compile monad found a command it can't h
 
 -- To be called on top-level signatures which are already Inx-closed, but not
 -- necessarily normalised.
-compileSig :: Modey m -> CTy m Z -> Compile ([HugrType], [HugrType])
-compileSig my cty = runCheckingInCompile (evalCTy S0 my cty) <&> (\(ss :->> ts) -> (compileRo ss, compileRo ts))
+compileSig :: Modey m -> FunTy m Z -> Compile ([HugrType], [HugrType])
+compileSig my cty = do
+  runCheckingInCompile (evalFunTy S0 my cty) <&> compileFunTy
 
-compileCTy (ss :->> ts) = PolyFuncType [] (FunctionType (compileRo ss) (compileRo ts) bratExts)
+compileFunTy (FunTy _ ss ts) = (compileRo ss, compileRo ts)
 
 compileRo :: Ro m i j -- The Ro that we're processing
           -> [HugrType]       -- The hugr type of the row
@@ -169,7 +170,7 @@ compileType (TList el)  = hugrList (compileType el)
 -- All variables are of kind `TypeFor m xs`, we already checked in `kindCheckRow`
 compileType (VApp _ _) = htTuple []
 -- VFun is already evaluated here, so we don't need to call `compileSig`
-compileType (VFun _ cty) = HTFunc $ compileCTy cty
+compileType (VFun _ cty) = let (ins, outs) = compileFunTy cty in HTFunc (PolyFuncType [] (FunctionType ins outs bratExts))
 compileType ty = error $ "todo: compile type " ++ show ty
 
 compileGraphTypes :: Traversable t => t (Val Z) -> Compile (t HugrType)
@@ -539,7 +540,7 @@ compileConstDfg parent desc (inTys, outTys) contents = do
 -- Brat computations may capture some local variables. Thus, we need
 -- to lambda-lift, producing (as results) a Partial node and a list of
 -- extra arguments i.e. the captured values
-compileBratBox :: NodeId -> Name -> (VEnv, Name, Name) -> CTy Brat Z -> Compile (NodeId, [(PortId NodeId, Int)])
+compileBratBox :: NodeId -> Name -> (VEnv, Name, Name) -> FunTy Brat Z -> Compile (NodeId, [(PortId NodeId, Int)])
 compileBratBox parent name (venv, src, tgt) cty = do
   -- we'll "Partial" over every value in the environment.
   -- (TODO in the future capture which ones are actually used in the sub-hugr. We may need
@@ -571,7 +572,7 @@ compileBratBox parent name (venv, src, tgt) cty = do
   pure (partialNode, zip (map fromJust edge_srcs) [1..])
     -- error on Nothing, the Partial is expecting a value
 
-compileKernBox :: NodeId -> Name -> (NodeId -> Compile ()) -> CTy Kernel Z -> Compile TypedPort
+compileKernBox :: NodeId -> Name -> (NodeId -> Compile ()) -> FunTy Kernel Z -> Compile TypedPort
 compileKernBox parent name contents cty = do
   -- compile kernel nodes only into a Hugr with "Holes"
   -- when we see a Splice, we'll record the func-port onto a list
diff --git a/brat/Brat/Elaborator.hs b/brat/Brat/Elaborator.hs
index 5a4ed219..df65a0b8 100644
--- a/brat/Brat/Elaborator.hs
+++ b/brat/Brat/Elaborator.hs
@@ -188,7 +188,7 @@ elaborate' (FOf n e) = do
   e <- assertNoun e
   pure $ SomeRaw' (ROf n e)
 elaborate' (FFn cty) = pure $ SomeRaw' (RFn cty)
-elaborate' (FKernel sty) = pure $ SomeRaw' (RKernel sty)
+elaborate' (FKernel ps sty) = pure $ SomeRaw' (RKernel ps sty)
 elaborate' FIdentity = pure $ SomeRaw' RIdentity
 -- We catch underscores in the top-level elaborate so this case
 -- should never be triggered
diff --git a/brat/Brat/Eval.hs b/brat/Brat/Eval.hs
index 3625c80b..82d19225 100644
--- a/brat/Brat/Eval.hs
+++ b/brat/Brat/Eval.hs
@@ -9,7 +9,7 @@ module Brat.Eval (EvMode(..)
                  ,sem
                  ,semLvl
                  ,doesntOccur
-                 ,evalCTy
+                 ,evalFunTy
                  ,eqTest
                  ,getNum
                  ,kindEq
@@ -24,6 +24,7 @@ import Brat.Checker.Monad
 import Brat.Checker.Types (EndType(..), kindForMode)
 import Brat.Error (ErrorMsg(..))
 import Brat.QualName (plain)
+import Brat.Syntax.CircuitProperties (eqProps)
 import Brat.Syntax.Common
 import Brat.Syntax.Value
 import Control.Monad.Freer (req)
@@ -71,11 +72,11 @@ numVal val = error $ "Found a " ++ show val ++ " at Nat kind"
 eval :: Stack Z Sem n -> Val n -> Checking (Val Z)
 eval stk v = sem stk v >>= quote Zy
 
-evalCTy :: Stack Z Sem n
-        -> Modey m
-        -> CTy m n
-        -> Checking (CTy m Z)
-evalCTy stk my = quoteCTy Zy my stk
+evalFunTy :: Stack Z Sem n
+          -> Modey m
+          -> FunTy m n
+          -> Checking (FunTy m Z)
+evalFunTy stk my = quoteFunTy Zy my stk
 
 sem :: Stack Z Sem n -- An environment for looking up VInxs
     -> Val n         -- The thing we're evaluating
@@ -122,13 +123,13 @@ quote lvy (SCon nm args) = VCon nm <$> traverse (quote lvy) args
 quote lvy (SLam stk body) = do
   body <- sem (stk :<< semLvl lvy) body
   VLam <$> quote (Sy lvy) body
-quote lvy (SFun my ga cty) = VFun my <$> quoteCTy lvy my ga cty
+quote lvy (SFun my ga cty) = VFun my <$> quoteFunTy lvy my ga cty
 quote lvy (SApp f vz) = VApp (quoteVar lvy f) <$> traverse (quote lvy) vz
 
-quoteCTy :: Ny lv -> Modey m -> Stack Z Sem n -> CTy m n -> Checking (CTy m lv)
-quoteCTy lvy my ga (ins :->> outs) = quoteRo my ga ins lvy >>= \case
+quoteFunTy :: Ny lv -> Modey m -> Stack Z Sem n -> FunTy m n -> Checking (FunTy m lv)
+quoteFunTy lvy my ga (FunTy ps ins outs) = quoteRo my ga ins lvy >>= \case
   (ga', Some (ins' :* lvy')) -> quoteRo my ga' outs lvy' >>= \case
-    (_, Some (outs' :* _)) -> pure (ins' :->> outs')
+    (_, Some (outs' :* _)) -> pure (FunTy ps ins' outs')
 
 -- first number is next Lvl to use in Value
 --         require every Lvl in Sem is < n (converted by n - 1 - lvl), else must fail at runtime
@@ -242,10 +243,16 @@ eqWorker tm lvkz (TypeFor m []) (SCon c args) (SCon c' args') | c == c' =
         Just ks -> eqTests tm lvkz (snd <$> ks) args args'
         Nothing -> pure . Left . TypeErr $ "Type constructor " ++ show c
                         ++ " undefined " ++ " at kind " ++ show (TypeFor m [])
-eqWorker tm lvkz (Star []) (SFun m0 stk0 (ins0 :->> outs0)) (SFun m1 stk1 (ins1 :->> outs1)) | Just Refl <- testEquality m0 m1 =
-  eqRowTest m0 tm lvkz (stk0,ins0) (stk1,ins1) >>= \case
-    Left msg -> pure (Left msg)
-    Right (Some lvkz, stk0, stk1) -> eqRowTest m0 tm lvkz (stk0, outs0) (stk1, outs1) <&> dropRight
+eqWorker tm lvkz (Star []) (SFun m0 stk0 (FunTy ps0 ins0 outs0)) (SFun m1 stk1 (FunTy ps1 ins1 outs1))
+ -- Give nice error for kind mismatch
+  | Just Refl <- testEquality m0 m1
+  = if eqProps m0 ps0 ps1
+    then eqRowTest m0 tm lvkz (stk0,ins0) (stk1,ins1) >>= \case
+      Left msg -> pure (Left msg)
+      Right (Some lvkz, stk0, stk1) -> eqRowTest m0 tm lvkz (stk0, outs0) (stk1, outs1) <&> dropRight
+    -- TODO: Better error message
+    else pure (Left (TypeErr "Kernels had different properties"))
+
 eqWorker tm lvkz (TypeFor _ []) (SSum m0 stk0 rs0) (SSum m1 stk1 rs1)
   | Just Refl <- testEquality m0 m1 = case zipSameLength rs0 rs1 of
       Nothing -> pure (Left (TypeErr "Mismatched sum lengths"))
@@ -256,7 +263,7 @@ 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
--- environments, which we return at the end for eqCType.
+-- environments, which we return at the end for eqFunType.
 eqRowTest :: Modey m
           -> String -- The term we complain about in errors
           -> (Ny :* Stack Z TypeKind) lv -- Next available level, the kinds of existing levels
@@ -312,7 +319,7 @@ doesntOccur e (VApp var args) = case var of
   _ -> 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
+doesntOccur e (VFun my (FunTy _ ins outs)) = case my of
   Braty -> doesntOccurRo my e ins *> doesntOccurRo my e outs
   Kerny -> doesntOccurRo my e ins *> doesntOccurRo my e outs
 
diff --git a/brat/Brat/Load.hs b/brat/Brat/Load.hs
index 56f65efc..52d6baa9 100644
--- a/brat/Brat/Load.hs
+++ b/brat/Brat/Load.hs
@@ -67,7 +67,9 @@ checkDecl pre (VDecl FuncDecl{..}) to_define = (fnName -!) $ localFC fnLoc $ do
     -- We must have a row of nouns as the definition
     Nothing -> case fnBody of
       NoLhs body -> do
-        (((), ()), ((), rightUnders)) <- let ?my = Braty in check body ((), to_define)
+        (((), ()), ((), rightUnders)) <- let ?my = Braty
+                                             ?props = ()
+                                         in  check body ((), to_define)
         case rightUnders of
           [] -> pure ()
           _ -> localFC (fcOf body) $
@@ -92,20 +94,20 @@ checkDecl pre (VDecl FuncDecl{..}) to_define = (fnName -!) $ localFC fnLoc $ do
             Kerny -> wire (box_out, VFun my cty, thunk_in)
           [] -> err $ ExpectedThunk (showMode my) "No body"
           row -> err $ ExpectedThunk (showMode my) (showRow row)
-      Left body -> let ?my = Braty in check body ((), to_define) $> ()
+      Left body -> let ?my = Braty in let ?props = () in check body ((), to_define) $> ()
  where
   getClauses :: FunBody Term Noun
-             -> (Modey m, CTy m Z)
+             -> (Modey m, FunTy m Z)
              -> Checking (Either
                           (WC (Term Chk Noun))
-                          (Some (Modey :* Flip CTy Z), FunBody Term UVerb)
+                          (Some (Modey :* Flip FunTy Z), FunBody Term UVerb)
                          )
   getClauses (ThunkOf (WC _ verb)) (my, cty) = pure (Right (Some (my :* Flip cty), verb))
   getClauses (NoLhs rhs) _ = pure (Left rhs)
   getClauses Undefined _ = err (InternalError "No body in `checkDecl`")
 
 
-  getFunTy :: Some (Ro m Z) -> Checking (Maybe (Some (Modey :* Flip CTy Z)))
+  getFunTy :: Some (Ro m Z) -> Checking (Maybe (Some (Modey :* Flip FunTy Z)))
   getFunTy (Some (RPr (_, VFun my cty) R0)) = pure $ Just (Some (my :* Flip cty))
   getFunTy (Some R0) = err $ EmptyRow name
   getFunTy _ = pure Nothing
@@ -145,7 +147,7 @@ loadStmtsWithEnv ns (venv, oldDecls, oldEndData) (fname, pre, stmts, cts) = addS
                         Local -> do
                           -- kindCheckAnnotation gives the signature of an Id node,
                           -- hence ins == outs (modulo haskell's knowledge about their scopes)
-                          ins :->> outs <- kindCheckAnnotation Braty (show name) (fnSig d)
+                          ins :->> outs <- kindCheckAnnotation Braty () (show name) (fnSig d)
                           pure (Id, ins :->> outs, Some ins, "decl")
                         Extern sym -> do
                           (Some outs) <- kindCheckRow Braty (show name) (fnSig d)
diff --git a/brat/Brat/Parser.hs b/brat/Brat/Parser.hs
index 1b0e6513..7bd3546b 100644
--- a/brat/Brat/Parser.hs
+++ b/brat/Brat/Parser.hs
@@ -8,8 +8,9 @@ import Brat.Lexer.Bracketed (BToken(..), brackets)
 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 Brat.Syntax.Abstractor hiding (PNone)
+import Brat.Syntax.CircuitProperties (CircuitProperties(..))
+import Brat.Syntax.Common hiding (PNone, end)
 import qualified Brat.Syntax.Common as Syntax
 import Brat.Syntax.FuncDecl (FuncDecl(..), Locality(..))
 import Brat.Syntax.Concrete
@@ -28,7 +29,7 @@ import Data.List (intercalate, uncons)
 import Data.List.HT (chop, viewR)
 import Data.List.NonEmpty (toList, NonEmpty(..), nonEmpty)
 import qualified Data.List.NonEmpty as NE
-import Data.Maybe (fromJust, fromMaybe)
+import Data.Maybe (fromJust, isJust, fromMaybe, maybeToList)
 import Data.Set (empty)
 import Prelude hiding (lex, round)
 import Text.Megaparsec hiding (Pos, Token, State, empty, match, ParseError, parse)
@@ -305,6 +306,22 @@ rawIO' tyP = rowElem `sepBy` void (try comma)
        Just (WC _ p) -> Named p <$> tyP
        Nothing -> Anon <$> tyP
 
+functionType :: Parser RawVType
+functionType = try ctype <|> kernel
+ where
+  ctype = do
+    ins <- inBrackets Paren $ rawIO
+    match Arrow
+    outs <- rawIO
+    pure (RFn (ins :-> outs))
+
+  kernel = do
+    ins <- inBrackets Paren $ rawIO' (unWC <$> vtype)
+    match Lolly
+    isWeird <- isJust <$> optional (match Hash)
+    outs <- rawIO' (unWC <$> vtype)
+    pure (RKernel (if isWeird then PNone else PControllable) (ins :-> outs))
+
 spanningFC :: TypeRow (WC ty) -> Parser (WC (TypeRow ty))
 spanningFC [] = customFailure (Custom "Internal: RawIO shouldn't be empty")
 spanningFC [x] = pure (WC (fcOf $ forgetPortName x) [unWC <$> x])
@@ -350,8 +367,9 @@ cthunk = try bratFn <|> try kernel <|> thunk
   kernel = inBracketsFC Brace $ do
     ss <- rawIO' (unWC <$> vtype)
     match Lolly
+    isWeird <- isJust <$> optional (match Hash)
     ts <- rawIO' (unWC <$> vtype)
-    pure $ FKernel (ss :-> ts)
+    pure (FKernel (if isWeird then PNone else PControllable) (ss :-> ts))
 
 
   -- Explicit lambda or brace section
@@ -623,7 +641,7 @@ decl = do
     where
       is_fun_ty :: RawVType -> Bool
       is_fun_ty (RFn _) = True
-      is_fun_ty (RKernel _) = True
+      is_fun_ty (RKernel _ _) = True
       is_fun_ty _ = False
 
       declClauses :: String -> Parser (WC FBody)
@@ -779,7 +797,7 @@ declSignature = try nDecl <|> vDecl where
  vDecl = functionSignature <&> fmap (\ty -> [Named "thunk" (Right ty)])
 
  functionSignature :: Parser (WC RawVType)
- functionSignature = try (fmap RFn <$> ctype) <|> (fmap RKernel <$> kernel)
+ functionSignature = try (fmap RFn <$> ctype) <|> (fmap (RKernel _) <$> kernel)
   where
    ctype :: Parser (WC RawCType)
    ctype = do
diff --git a/brat/Brat/Search.hs b/brat/Brat/Search.hs
index 96dbbc42..975dbc61 100644
--- a/brat/Brat/Search.hs
+++ b/brat/Brat/Search.hs
@@ -89,7 +89,7 @@ tokenValues fc (VFun Braty (ss :->> ts)) =
   outputsNonBinding (REx _ _) = []
 
 
-tokenValues fc (VFun Kerny (ss :->> ts)) =
+tokenValues fc (VFun Kerny (FunTy _ ss ts)) =
   [ Th (WC fc (Lambda (WC fc abs, WC fc t) [])) | t <- rhs ]
  where
   abs = binders (rowLen ss)
diff --git a/brat/Brat/Syntax/Concrete.hs b/brat/Brat/Syntax/Concrete.hs
index 3e07bb44..e09bd528 100644
--- a/brat/Brat/Syntax/Concrete.hs
+++ b/brat/Brat/Syntax/Concrete.hs
@@ -4,6 +4,7 @@ import Data.List.NonEmpty
 
 import Brat.FC
 import Brat.QualName
+import Brat.Syntax.CircuitProperties (CircuitProperties)
 import Brat.Syntax.Common
 import Brat.Syntax.FuncDecl (FuncDecl(..))
 import Brat.Syntax.Raw
@@ -41,7 +42,7 @@ data Flat
  | FPull [PortName] (WC Flat)
  -- We can get away with not elaborating type signatures in the short term
  | FFn RawCType
- | FKernel RawKType
+ | FKernel CircuitProperties RawKType
  | FUnderscore
  | FPass
  | FFanOut
diff --git a/brat/Brat/Syntax/Core.hs b/brat/Brat/Syntax/Core.hs
index c9dbd046..f495c94a 100644
--- a/brat/Brat/Syntax/Core.hs
+++ b/brat/Brat/Syntax/Core.hs
@@ -16,6 +16,7 @@ import Brat.Constructors.Patterns (pattern CCons,
 import Brat.FC
 import Brat.Naming
 import Brat.QualName
+import Brat.Syntax.CircuitProperties
 import Brat.Syntax.Common
 import Brat.Syntax.FuncDecl
 import Brat.Syntax.Simple
@@ -69,7 +70,7 @@ data Term :: Dir -> Kind -> Type where
   -- Brat function types
   C        :: CType' (PortName, KindOr (Term Chk Noun)) -> Term Chk Noun
   -- Kernel types
-  K        :: CType' (PortName, Term Chk Noun) -> Term Chk Noun
+  K        :: Properties Kernel ->  CType' (PortName, Term Chk Noun) -> Term Chk Noun
   FanOut   :: Term Syn UVerb
   FanIn    :: Term Chk UVerb
 
@@ -137,7 +138,7 @@ instance Show (Term d k) where
     prettyPat _ = Nothing
 
   show (C f) = "{" ++ show f ++ "}"
-  show (K (ss :-> ts)) = "{" ++ showSig ss ++ " -o " ++ showSig ts ++ "}"
+  show (K _ (ss :-> ts)) = "{" ++ showSig ss ++ " -o " ++ showSig ts ++ "}"
   show FanOut = "[/\\]"
   show FanIn = "[\\/]"
 
diff --git a/brat/Brat/Syntax/Raw.hs b/brat/Brat/Syntax/Raw.hs
index 62934f1b..c73ed412 100644
--- a/brat/Brat/Syntax/Raw.hs
+++ b/brat/Brat/Syntax/Raw.hs
@@ -19,6 +19,7 @@ import Brat.Error
 import Brat.FC hiding (end)
 import Brat.Naming
 import Brat.QualName
+import Brat.Syntax.CircuitProperties
 import Brat.Syntax.Common
 import Brat.Syntax.Core
 import Brat.Syntax.FuncDecl (FunBody(..), FuncDecl(..))
@@ -82,7 +83,7 @@ data Raw :: Dir -> Kind -> Type where
   -- Function types
   RFn       :: RawCType -> Raw Chk Noun
   -- Kernel types
-  RKernel   :: RawKType -> Raw Chk Noun
+  RKernel   :: Properties Kernel -> RawKType -> Raw Chk Noun
   RFanOut   :: Raw Syn UVerb
   RFanIn    :: Raw Chk UVerb
 
@@ -127,7 +128,7 @@ instance Show (Raw d k) where
     showClause (abs, bod) = show abs ++ " => " ++ show bod
   show (RCon c xs) = "Con(" ++ show c ++ "(" ++ show xs ++ "))"
   show (RFn cty) = show cty
-  show (RKernel cty) = show cty
+  show (RKernel _ cty) = show cty
   show RFanOut = "[/\\]"
   show RFanIn = "[\\/]"
   show (ROf n e) = "(" ++ show n ++ " of " ++ show e ++ ")"
@@ -246,7 +247,7 @@ instance (Kindable k) => Desugarable (Raw d k) where
   desugar' (RLet abs thing body) = Let abs <$> desugar thing <*> desugar body
   desugar' (RCon c arg) = Con c <$> desugar arg
   desugar' (RFn cty) = C <$> desugar' cty
-  desugar' (RKernel cty) = K <$> desugar' cty
+  desugar' (RKernel props cty) = K props <$> desugar' cty
   desugar' RFanOut = pure FanOut
   desugar' RFanIn = pure FanIn
   desugar' (ROf n e) = Of <$> desugar n <*> desugar e
diff --git a/brat/Brat/Syntax/Value.hs b/brat/Brat/Syntax/Value.hs
index 4bc71fcd..a3a04939 100644
--- a/brat/Brat/Syntax/Value.hs
+++ b/brat/Brat/Syntax/Value.hs
@@ -24,7 +24,8 @@ module Brat.Syntax.Value {-(VDecl
 
 import Brat.Error
 import Brat.QualName
-import Brat.Syntax.Common
+import Brat.Syntax.CircuitProperties
+import Brat.Syntax.Common hiding (pattern PNone)
 import Brat.Syntax.Core (Term (..))
 import Brat.Syntax.FuncDecl (FunBody, FuncDecl(..))
 import Bwd
@@ -156,7 +157,7 @@ data Val :: N -> Type where
   VNum :: NumVal (VVar 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
+  VFun :: MODEY m => Modey m -> FunTy m n -> Val n
   VApp :: VVar n -> Bwd (Val n) -> Val n
 
 -- Define a naive version of equality, which only says whether the data
@@ -171,8 +172,8 @@ instance Eq (Val n) where
   (VApp v zx) == (VApp w zy) = v == w && zx == zy
   _ == _ =  False
 
-instance MODEY m => Eq (CTy m i) where
-  (ss :->> ts) == (us :->> vs) = case roEq (modey @m) ss us of
+instance MODEY m => Eq (FunTy m i) where
+  (FunTy ps ss ts) == (FunTy qs us vs) = ((eqProps (modey @m) ps qs) &&) $ case roEq (modey @m) ss us of
                                    Just Refl -> isJust (roEq (modey @m) ts vs)
                                    Nothing -> False
    where
@@ -194,17 +195,21 @@ data Sem where
   -- 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
-  SFun :: MODEY m => Modey m -> Stack Z Sem n -> CTy m n -> Sem
+  SFun :: MODEY m => Modey m -> Stack Z Sem n -> FunTy m n -> Sem
   SApp :: SVar -> Bwd Sem -> Sem
   -- Sum types, stash like SLam (shared between all variants)
   SSum :: MODEY m => Modey m -> Stack Z Sem n -> [Some (Ro m n)] -> Sem
 deriving instance Show Sem
 
-data CTy :: Mode -> N -> Type where
-  (:->>) :: Ro m i j -> Ro m j k -> CTy m i
+data FunTy :: Mode -> N -> Type where
+  FunTy :: Properties m -> Ro m i j -> Ro m j k -> FunTy m i
 
-instance MODEY m => Show (CTy m n) where
-  show (ri :->> ro) = unwords [show ri, arrow, show ro]
+pattern (:->>) :: Ro Brat i j -> Ro Brat j k -> FunTy Brat i
+pattern ss :->> ts = FunTy () ss ts
+
+instance MODEY m => Show (FunTy m n) where
+  -- Properties don't exist in the surface syntax, so hide them from the user here.
+  show (FunTy _ ri ro) = unwords [show ri, arrow, show ro]
    where
     arrow = case modey :: Modey m of
       Braty -> "->"
@@ -560,10 +565,10 @@ varChangerThroughRo vc {- src -> tgt -} (REx pk ro {- S src' -> src'' -})
   = case varChangerThroughRo (weakenVC vc) ro of
         Some (vc {- src'' -> tgt'' -} :* ro {- S tgt' -> tgt'' -}) -> Some (vc :* REx pk ro)
 
-instance DeBruijn (CTy m) where
-  changeVar (vc {- srcIn -> tgtIn -}) (ri {- srcIn -> srcMid -} :->> ro {- srcMid -> srcOut -}) = case varChangerThroughRo vc ri of
+instance DeBruijn (FunTy m) where
+  changeVar (vc {- srcIn -> tgtIn -}) (FunTy ps ri {- srcIn -> srcMid -} ro {- srcMid -> srcOut -}) = case varChangerThroughRo vc ri of
     Some {- tgtMid -} (vc {- srcMid -> tgtMid -} :* ri {- tgtIn -> tgtMid -}) -> case varChangerThroughRo vc ro of
-      Some {- tgtOut -} (_vc {- srcOut -> tgtOut -} :* ro {- tgtMid -> tgtOut -}) -> ri :->> ro
+      Some {- tgtOut -} (_vc {- srcOut -> tgtOut -} :* ro {- tgtMid -> tgtOut -}) -> FunTy ps ri ro
 
 kernelNoBind :: Ro Kernel bot top -> bot :~: top
 kernelNoBind R0 = Refl
@@ -588,7 +593,7 @@ data KernelVal :: N -> Type where
   KCons :: KernelVal n -> KernelVal n -> KernelVal n
 deriving instance Show (KernelVal n)
 
-type FunVal m = CTy m Z
+type FunVal m = FunTy m Z
 --value :: Modey m -> FunVal m -> Val Z
 --value = VFun
 
diff --git a/brat/Brat/Unelaborator.hs b/brat/Brat/Unelaborator.hs
index 5ff57492..f2ce7148 100644
--- a/brat/Brat/Unelaborator.hs
+++ b/brat/Brat/Unelaborator.hs
@@ -36,7 +36,7 @@ unelab dy ky (f :$: s) = FApp (unelab dy KVerby <$> f) (unelab Chky ky <$> s)
 unelab dy _ (Lambda (abs,rhs) cs) = FLambda ((abs, unelab dy Nouny <$> rhs) :| (second (fmap (unelab Chky Nouny)) <$> cs))
 unelab _ _ (Con c args) = FCon c (unelab Chky Nouny <$> args)
 unelab _ _ (C (ss :-> ts)) = FFn (toRawRo ss :-> toRawRo ts)
-unelab _ _ (K cty) = FKernel $ fmap (\(p, ty) -> Named p (toRaw ty)) cty
+unelab _ _ (K ps cty) = FKernel ps $ fmap (\(p, ty) -> Named p (toRaw ty)) cty
 unelab _ _ Identity = FIdentity
 unelab _ _ Hope = FHope
 unelab _ _ FanIn = FFanIn
@@ -66,7 +66,7 @@ toRaw (f :$: s) = (toRaw <$> f) ::$:: (toRaw <$> s)
 toRaw (Lambda (abs,rhs) cs) = RLambda (abs, toRaw <$> rhs) (second (fmap toRaw) <$> cs)
 toRaw (Con c args) = RCon c (toRaw <$> args)
 toRaw (C (ss :-> ts)) = RFn (toRawRo ss :-> toRawRo ts)
-toRaw (K cty) = RKernel $ (\(p, ty) -> Named p (toRaw ty)) <$> cty
+toRaw (K ps cty) = RKernel ps $ (\(p, ty) -> Named p (toRaw ty)) <$> cty
 toRaw Identity = RIdentity
 toRaw Hope = RHope
 toRaw FanIn = RFanIn
diff --git a/brat/brat.cabal b/brat/brat.cabal
index 3873bcf1..199105b8 100644
--- a/brat/brat.cabal
+++ b/brat/brat.cabal
@@ -82,6 +82,7 @@ library
                        Brat.Elaborator,
                        Brat.QualName,
                        Brat.Syntax.Abstractor,
+                       Brat.Syntax.CircuitProperties,
                        Brat.Syntax.Concrete,
                        Brat.Syntax.FuncDecl,
                        Brat.Syntax.Port,
diff --git a/brat/examples/lib/kernel.brat b/brat/examples/lib/kernel.brat
index 32ea5864..a77edcaa 100644
--- a/brat/examples/lib/kernel.brat
+++ b/brat/examples/lib/kernel.brat
@@ -18,8 +18,8 @@ ext "tket.CRy" CRy(Float) -> { Qubit, Qubit -o Qubit, Qubit }
 ext "tket.CRz" CRz(Float) -> { Qubit, Qubit -o Qubit, Qubit }
 ext "tket.M" M :: { Qubit -o Bit }
 
-ext "builtin.measure" measure :: { Qubit -o q::Money, b::Bit }
-ext "builtin.fresh" fresh :: { Money -o Qubit }
+ext "builtin.measure" measure :: { Qubit -o# q::Money, b::Bit }
+ext "builtin.fresh" fresh :: { Money -o# Qubit }
 
 uncons(n :: #) -> { Vec(Qubit, succ(n)) -o Qubit, Vec(Qubit, n) }
 uncons(_) = { cons(q, qs) => q, qs }
diff --git a/brat/test/Test/Search.hs b/brat/test/Test/Search.hs
index 0c872f8a..6614a7fc 100644
--- a/brat/test/Test/Search.hs
+++ b/brat/test/Test/Search.hs
@@ -6,6 +6,7 @@ import Brat.Checker (check)
 import Brat.FC
 import Brat.Naming
 import Brat.Search (vsearch)
+import Brat.Syntax.CircuitProperties (CircuitProperties(..))
 import Brat.Syntax.Common
 import Hasochism (N(..))
 import Util (names)
@@ -40,14 +41,14 @@ arbitrarySValue d = case d of
 
 
 instance Arbitrary (Val Z) where
-  arbitrary = chooseInt bounds >>= \n -> row n maxDepth <&> \r -> VFun Kerny (r :->> r)
+  arbitrary = chooseInt bounds >>= \n -> row n maxDepth <&> \r -> VFun Kerny (FunTy PControllable r r)
 
 tokensTypecheck :: Val Z -> Bool
 tokensTypecheck kty =
   let kernels = vsearch fc kty in
     case kernels of
       [] -> False
-      (k:_) -> case runEmpty (let ?my = Braty in check (WC fc k) ((), [(NamedPort (In src 0) "fun", Right kty)])) of
+      (k:_) -> case runEmpty (let ?my = Braty in let ?props = () in check (WC fc k) ((), [(NamedPort (In src 0) "fun", Right kty)])) of
           Right ((((), ()), ((), unders)), _) -> null unders
           Left _ -> False
  where
diff --git a/brat/test/Test/Syntax/Let.hs b/brat/test/Test/Syntax/Let.hs
index bd748872..2cf314fd 100644
--- a/brat/test/Test/Syntax/Let.hs
+++ b/brat/test/Test/Syntax/Let.hs
@@ -34,7 +34,7 @@ test = testCase "let" $
         )
         (dummyFC (Var "x"))
       conn = ((), ())
-  in case fst <$> runEmpty (let ?my = Braty in check (dummyFC tm) conn) of
+  in case fst <$> runEmpty (let ?my = Braty in let ?props = () in check (dummyFC tm) conn) of
        Right (((), [(_, Right TInt)]), ((), ())) -> pure ()
        Right (((), outs), ((), ())) -> assertFailure (show outs)
        Left err -> assertFailure (showError err)