diff --git a/Src/Actor.hs b/Src/Actor.hs
index e2e4375..b57ead4 100644
--- a/Src/Actor.hs
+++ b/Src/Actor.hs
@@ -138,6 +138,7 @@ mangleActors opts rho tm = go tm where
   go tm = case expand tm of
     VX i de -> pure (var i (ga + de))
     AX a de -> pure (atom a (ga + de))
+    GX g a -> (G g $^) <$> go a
     a :%: b -> (%) <$> go a <*> go b
     t :-: o -> Term.contract <$> ((:-:) <$> go t <*> go o)
     t ::: o -> Term.contract <$> ((:::) <$> go t <*> go o)
diff --git a/Src/Actor/Display.hs b/Src/Actor/Display.hs
index 19768d1..7b05694 100644
--- a/Src/Actor/Display.hs
+++ b/Src/Actor/Display.hs
@@ -2,7 +2,7 @@
 
 module Actor.Display where
 
-import Control.Monad.Except
+import Control.Monad (forM)
 
 import qualified Data.Map as Map
 
diff --git a/Src/Bwd.hs b/Src/Bwd.hs
index 599d14d..5bf5c92 100644
--- a/Src/Bwd.hs
+++ b/Src/Bwd.hs
@@ -3,10 +3,14 @@ Description: snoc lists
 -}
 module Bwd where
 
+import Control.Monad (guard)
+import Control.Monad.State
+
 import Data.Map (Map)
-import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
-import Control.Monad.State
+import qualified Data.Map as Map
+
+import GHC.Stack (HasCallStack)
 
 data Bwd x = B0 | Bwd x :< x
   deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
@@ -20,9 +24,10 @@ instance Monoid (Bwd x) where
   mempty = B0
 
 -- | lookup with a more convenient name
-(<!) :: Bwd x -> Int -> x
+(<!) :: HasCallStack => Bwd x -> Int -> x
 (_  :< x) <! 0 = x
 (xs :< _) <! n = xs <! (n - 1)
+_ <! _ = error "Looking up from an empty Bwd"
 
 infixl 4 <><
 
@@ -50,26 +55,30 @@ mapzs f xz = mapzss f xz []
 
 -- | Treat a snoc list as a stack and returns the top.
 -- Warning: incomplete pattern match.
-top :: Bwd x -> x
+top :: HasCallStack => Bwd x -> x
 top (_ :< x) = x
+top _ = error "Taking the top of an empty Bwd"
 
 -- | 'takez' is 'take' but renamed so 'take' can still be used
-takez :: Bwd x -> Int -> Bwd x
+takez :: HasCallStack => Bwd x -> Int -> Bwd x
 takez _ 0 = B0
 takez (xz :< x) w = takez xz (w-1) :< x
+takez _ _ = error "Taking from an empty Bwd"
 
 -- | 'dropz' is 'drop' but renamed so 'drop' can still be used
-dropz :: Bwd x -> Int -> Bwd x
+dropz :: HasCallStack => Bwd x -> Int -> Bwd x
 dropz xz 0 = xz
 dropz (xz :< x) w = dropz xz (w-1)
+dropz _ _ = error "Dropping from an empty Bwd"
 
 -- | singleton snoc list
 singleton :: x -> Bwd x
 singleton x = B0 :< x
 
 -- | matches 'only' singleton, and will fail in not-nice ways otherwise
-only :: Bwd x -> x
+only :: HasCallStack => Bwd x -> x
 only (B0 :< x) = x
+only _ = error "Not a singleton Bwd"
 
 -- | 'focusBy' takes a predicate p and a snoc list, and returns
 -- a pointed cursor into that snoc for the first item that satisfies p
@@ -87,9 +96,10 @@ focus :: Eq x => x -> Bwd x -> Maybe (Bwd x, x, [x])
 focus x = focusBy (\ y -> y <$ guard (x == y))
 
 -- | "curl up" n items from the snoc part onto the list part
-curl :: Int -> (Bwd x, [x]) -> (Bwd x, [x])
+curl :: HasCallStack => Int -> (Bwd x, [x]) -> (Bwd x, [x])
 curl 0 xzs = xzs
 curl n (xz :< x, xs) = curl (n-1) (xz, x : xs)
+curl _ _ = error "Curling from an empty Bwd"
 
 -- | A 'Cursor' is a location in a list (or a snoc list)
 -- Note that it can point to the head or tail, it does not
diff --git a/Src/Command.hs b/Src/Command.hs
index 33744d2..fdebef5 100644
--- a/Src/Command.hs
+++ b/Src/Command.hs
@@ -2,16 +2,16 @@
 
 module Command where
 
+import Control.Monad (when, forM_, guard)
 import Control.Applicative
-import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.State
 
 import Data.Bifunctor (bimap, first)
+import Data.Kind (Type)
 import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
 import Data.Traversable (for)
-import Data.Foldable (asum)
 
 import Actor
 import Actor.Display ()
@@ -45,7 +45,7 @@ import Operator.Eval (HeadUpData' (..))
 import Hide (Hide(..))
 import Scope (Scope(..))
 
-type family DEFNPROTOCOL (ph :: Phase) :: *
+type family DEFNPROTOCOL (ph :: Phase) :: Type
 type instance DEFNPROTOCOL Concrete = ()
 type instance DEFNPROTOCOL Abstract = AProtocol
 
@@ -141,6 +141,7 @@ instance Pretty CCommand where
     Go a -> keyword "exec" <+> pretty a
     Trace ts -> keyword "trace" <+> collapse (BracesList $ map pretty ts)
     Typecheck t ty -> keyword "typecheck" <+> pretty t <+> ":" <+> pretty ty
+    OpBlock _ -> undefined -- TODO
 
 instance Unelab ACommand where
   type UnelabEnv ACommand = Naming
@@ -159,6 +160,7 @@ instance Unelab ACommand where
     Go a -> Go <$> withEnv initDAEnv (unelab a)
     Trace ts -> pure $ Trace ts
     Typecheck t ty -> Typecheck <$> unelab t <*> unelab ty
+    OpBlock t -> error "Unhandled input"
 
 instance Unelab AStatement where
   type UnelabEnv AStatement = ()
@@ -333,12 +335,13 @@ scommand = \case
 
 sopBlock :: [OPENTRY Concrete] -> Elab ([OPENTRY Abstract], Globals)
 sopBlock [] = ([],) <$> asks globals
+sopBlock (DefnOp (_, [], _) : _) = error "Broken invariant"
 sopBlock (DefnOp (rp, opelims@((rpty,_,_):_), rhs) : rest) = do
   -- p : pty0 -[ opelim0 ] : pty1 -[ opelim1 ] ... : ptyn -[ opelimn ] ~> rhs
   (p, opelimz, decls, lhsTy) <- sopelims0 (getRange rp <> getRange rpty) rp opelims
   rhs <- local (setDecls decls) $ stm DontLog lhsTy rhs
   -- this is the outer op being extended
-  let op = case opelimz of (_ :< (_, op, _)) -> op
+  let op = case opelimz of { (_ :< (_, op, _)) -> op; B0 -> error "Broken invariant" }
   let cl = toClause p opelimz rhs
   (bl , gl) <- sopBlock rest
   pure (DefnOp (op, cl) : bl, gl)
@@ -358,6 +361,7 @@ sopelims :: Range
          -> Either RawP (Pat, (ASemanticsDesc, ACTm))
          -> [(RawP, OPERATOR Concrete, [RawP])]
          -> Elab (Pat, Bwd (Pat, OPERATOR Abstract, [Pat]), Decls, ASemanticsDesc)
+sopelims _ _ (Left _) [] = error "Unhandled input"
 sopelims r opelimz (Right (p, (inty, t))) [] = (p,opelimz,,inty) <$> asks declarations
 sopelims r opelimz acc ((rpty, op, args):opelims) = do
   -- We need to worry about freshening up names in operator
@@ -406,6 +410,7 @@ sopelims r opelimz acc ((rpty, op, args):opelims) = do
       (Tele desc (Scope (Hide name) tele))
       (LamP r (Scope (Hide x) rp)) =
       elabUnder (x, desc) $ sparamSemantics binder (namez :< name) tele rp
+    sparamSemantics _ _ _ _ = error "Unhandled input"
 
     -- cf. itms
     spats :: Range
diff --git a/Src/Concrete/Base.hs b/Src/Concrete/Base.hs
index 852147b..03ebfec 100644
--- a/Src/Concrete/Base.hs
+++ b/Src/Concrete/Base.hs
@@ -1,14 +1,16 @@
 {-# LANGUAGE UndecidableInstances #-}
 module Concrete.Base where
 
+import Data.Bifunctor (Bifunctor (..))
 import Data.Function (on)
+import Data.Kind (Type)
 
 import Bwd
 import Format
 import Scope
 import Hide
 import Location
-import Data.Bifunctor (Bifunctor (..))
+
 
 data Variable = Variable
   { variableLoc :: Range
@@ -177,9 +179,9 @@ isSubjectMode :: Mode a -> Bool
 isSubjectMode (Subject _) = True
 isSubjectMode _           = False
 
-type family SYNTAXCAT (ph :: Phase) :: *
+type family SYNTAXCAT (ph :: Phase) :: Type
 
-type family SYNTAXDESC (ph :: Phase) :: *
+type family SYNTAXDESC (ph :: Phase) :: Type
 type instance SYNTAXDESC Concrete = Raw
 type CSyntaxDesc = SYNTAXDESC Concrete
 type ASyntaxDesc = SYNTAXDESC Abstract
@@ -205,6 +207,9 @@ data ContextStack k v = ContextStack
   , valueDesc :: v {- closed semantics desc -}
   } deriving (Show)
 
+instance Functor (ContextStack a) where
+  fmap f (ContextStack k v) = ContextStack k (f v)
+
 instance Bifunctor ContextStack where
   bimap f g (ContextStack k v) = ContextStack (f k) (g v)
 
@@ -237,20 +242,20 @@ instance Show Keyword where
 
 data Phase = Concrete | Elaboration | Abstract
 
-type family JUDGEMENTNAME (ph :: Phase) :: *
-type family CHANNEL (ph :: Phase) :: *
-type family BINDER (ph :: Phase) :: *
-type family ACTORVAR (ph :: Phase) :: *
-type family TERMVAR (ph :: Phase) :: *
-type family TERM (ph :: Phase) :: *
-type family PATTERN (ph :: Phase) :: *
-type family CONNECT (ph :: Phase) :: *
-type family STACK (ph :: Phase) :: *
-type family STACKDESC (ph :: Phase) :: *
-type family SCRUTINEEVAR (ph :: Phase) :: *
-type family SCRUTINEETERM (ph :: Phase) :: *
-type family LOOKEDUP (ph :: Phase) :: *
-type family GUARD (ph :: Phase) :: *
+type family JUDGEMENTNAME (ph :: Phase) :: Type
+type family CHANNEL (ph :: Phase) :: Type
+type family BINDER (ph :: Phase) :: Type
+type family ACTORVAR (ph :: Phase) :: Type
+type family TERMVAR (ph :: Phase) :: Type
+type family TERM (ph :: Phase) :: Type
+type family PATTERN (ph :: Phase) :: Type
+type family CONNECT (ph :: Phase) :: Type
+type family STACK (ph :: Phase) :: Type
+type family STACKDESC (ph :: Phase) :: Type
+type family SCRUTINEEVAR (ph :: Phase) :: Type
+type family SCRUTINEETERM (ph :: Phase) :: Type
+type family LOOKEDUP (ph :: Phase) :: Type
+type family GUARD (ph :: Phase) :: Type
 
 type instance JUDGEMENTNAME Concrete = Variable
 type instance CHANNEL Concrete = Variable
diff --git a/Src/Concrete/Pretty.hs b/Src/Concrete/Pretty.hs
index ae58689..de2b648 100644
--- a/Src/Concrete/Pretty.hs
+++ b/Src/Concrete/Pretty.hs
@@ -73,6 +73,7 @@ instance Pretty RawP where
     LamP _ (Scope x p) -> multiBindP (B0 :< x) p
     ThP _ (thxz, thd) p -> braces (hsep (pretty <$> thxz <>> []) <> pretty thd) <+> pretty p
     UnderscoreP _ -> "_"
+    Irrefutable _ p -> "~" <+> pretty p
 
 prettyCdrP :: RawP -> [Doc Annotations]
 prettyCdrP = \case
diff --git a/Src/Elaboration.hs b/Src/Elaboration.hs
index c0fde82..63f33c0 100644
--- a/Src/Elaboration.hs
+++ b/Src/Elaboration.hs
@@ -1,17 +1,18 @@
 module Elaboration where
 
-import Control.Monad.Except
+import Control.Monad (when, unless, guard, forM)
 import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Writer
 
+import Data.Bitraversable
 import Data.Function
 import Data.List (isPrefixOf)
 import qualified Data.List as List
 import qualified Data.Map as Map
-import qualified Data.Set as Set
 import Data.Maybe
-import Data.Bitraversable
+import Data.Monoid (All(..))
+import qualified Data.Set as Set
 
 import Actor
 import Bwd
@@ -45,6 +46,7 @@ import GHC.Stack.Types (HasCallStack)
 type CPattern = PATTERN Concrete
 type APattern = PATTERN Abstract
 
+dmesg :: a -> b -> b
 dmesg = const id
 
 isSubject :: EScrutinee -> IsSubject' ()
@@ -197,6 +199,7 @@ smacro xz (Op r obj opps) = do
   smacro xz obj
   smacro xz opps
 smacro xz (Guarded r t) = smacro xz t
+smacro _ _ = error "Unsupported arguments"
 
 smacros :: Bwd String -> [Assign] -> Elab (Bwd String)
 smacros xz [] = pure xz
@@ -652,6 +655,7 @@ stm usage desc rt = do
         (tdesc, t) <- itm usage rt
         compatibleInfos (getRange rt) (Known desc) (Known tdesc)
         pure t
+      _ -> error "stm: unsupported argument"
 
 senumortag :: Range -> String -> Raw -> Raw -> Elab ACTm
 senumortag r a es tds = do
@@ -849,6 +853,7 @@ spatBase isSub desc rest rp = do
         elabUnder (x, s) $
 --          local (addHint (getVariable <$> x) (Known s)) $
             spatBase isSub desc (extend rest (getVariable <$> x)) p
+      _ -> error "spatBase: unsupported argument"
 
 isObjVar :: Variable -> Elab (ASemanticsDesc, DB)
 isObjVar p = resolve p >>= \case
@@ -893,8 +898,9 @@ isContextStack stk = resolve stk >>= \case
 channelScope :: Channel -> Elab ObjVars
 channelScope (Channel ch) = do
   ds <- asks declarations
-  case fromJust (focusBy (\ (y, k) -> k <$ guard (ch == y)) ds) of
-    (_, AChannel sc, _) -> pure sc
+  case focusBy (\ (y, k) -> k <$ guard (ch == y)) ds of
+    Just (_, AChannel sc, _) -> pure sc
+    _ -> error "Broken invariant"
 
 steppingChannel :: Range -> Channel
                 -> (Direction -> [AProtocolEntry] -> Elab (a, [AProtocolEntry]))
@@ -921,6 +927,7 @@ close b r ch = do
       _ -> when b $
             -- if we cannot win, we don't care
             throwComplaint r (UnfinishedProtocol ch (Protocol ps))
+    _ -> error "Broken invariant"
   modify (channelDelete ch)
 
 withChannel :: Range -> Direction -> Channel -> AProtocol -> Elab a -> Elab a
@@ -1039,6 +1046,7 @@ sact = \case
         Subject _ -> ((SentAsSubject r ,) <$>) $ asks elabMode >>= \case
           Execution  -> pure Nothing
           Definition -> checkSendableSubject tm
+        Input -> error "Broken invariant"
 
     -- Send
     tm <- during (SendTermElaboration ch tm) $ do
diff --git a/Src/Elaboration/Monad.hs b/Src/Elaboration/Monad.hs
index 613322b..af57374 100644
--- a/Src/Elaboration/Monad.hs
+++ b/Src/Elaboration/Monad.hs
@@ -2,6 +2,7 @@
 {-# OPTIONS_GHC -Wincomplete-patterns #-}
 module Elaboration.Monad where
 
+import Control.Monad (when, guard)
 import Control.Monad.Except
 import Control.Monad.Reader
 import Control.Monad.State
@@ -11,6 +12,7 @@ import Data.List.NonEmpty (NonEmpty)
 import Data.Map (Map)
 import qualified Data.Map as Map
 import Data.Maybe (fromMaybe)
+import Data.Monoid (All)
 
 import Actor
 import Bwd
diff --git a/Src/LaTeX.hs b/Src/LaTeX.hs
index 403973f..3f9c425 100644
--- a/Src/LaTeX.hs
+++ b/Src/LaTeX.hs
@@ -3,10 +3,11 @@
 
 module LaTeX where
 
-import Data.Char (isDigit)
+import Control.Monad.Reader
 
+import Data.Char (isDigit)
 import qualified Data.Map as Map
-import Control.Monad.Reader
+import Data.Maybe (fromMaybe)
 
 import Concrete.Base
 import Text.PrettyPrint.Compact
@@ -112,8 +113,8 @@ instance LaTeX Raw where
       _ -> call False "typosAtom" [text a] -- as atom
     Cons _ p q -> ask >>= \ table -> case expand table d of
       Just (VEnumOrTag _ ts) -> do
-        let At _ a = p
-        let Just ds = lookup a ts
+        let a = case p of { At _ a -> a; _ -> error "Broken invariant" }
+        let ds = fromMaybe (error "Broken invariant") $ lookup a ts
         let qs = asList q
         call False (text (aTag a (length ds))) <$> traverse (uncurry toLaTeX) (zip ds qs) -- as tags
       Just (VCons dp dq) -> do
@@ -136,7 +137,9 @@ instance LaTeX Raw where
       bd <- toLaTeX () x
       pure $ call False "typosScope" [bd, sc]
     Sbst _ bwd raw -> pure ""
+    _ -> undefined -- TODO
 
+test :: IO ()
 test =
   putStrLn $
   let syntaxT = syntaxDesc ["Syntax"] in
diff --git a/Src/Machine/Base.hs b/Src/Machine/Base.hs
index e2a9d23..3cc61ad 100644
--- a/Src/Machine/Base.hs
+++ b/Src/Machine/Base.hs
@@ -4,11 +4,13 @@
 {-# LANGUAGE UndecidableInstances #-}
 module Machine.Base where
 
+import Control.Monad.State
+
+import Data.Kind (Type)
 import qualified Data.Map as Map
+import Data.Maybe (fromMaybe)
 import Data.Set (Set)
 import qualified Data.Set as Set
-import Data.Maybe (fromMaybe)
-import Control.Monad.State
 
 import Actor
 import Actor.Display()
@@ -93,6 +95,7 @@ compareUp dat s t = case (expand (headUp dat s), expand (headUp dat t)) of
   (_, AX{}) -> pure GT
   ((:%:){}, _) -> pure LT
   (_, (:%:){}) -> pure GT
+  _ -> undefined -- TODO
 
 comparesUp :: HeadUpData -> Subst -> Subst -> Maybe Ordering
 comparesUp dat sg sg' = compareUp dat (toTerm sg) (toTerm sg') where
@@ -105,7 +108,7 @@ class Instantiable t where
   normalise :: HeadUpData -> t -> Instantiated t
 
 class Instantiable1 t where
-  type Instantiated1 t :: * -> *
+  type Instantiated1 t :: Type -> Type
   instantiate1 :: StoreF i d -> t a -> Instantiated1 t a
   normalise1 :: HeadUpData -> t a -> Instantiated1 t a
 
@@ -188,6 +191,7 @@ toClause :: Pat -- (obj, ty), eg `['Pair p q] : ['Sigma A \x.B]`
          -> Bwd (Pat, Operator, [Pat]) -- parameter patterns
          -> ACTm -- RHS
          -> Clause
+toClause pobj B0 rhs = error "Broken invariant"
 toClause pobj (ops :< op@(_, opname, _)) rhs = Clause $ toClause' where
  toClause' :: forall m. AClause m
  toClause' opts hnf env targs@((t, ty), args) =
@@ -309,6 +313,7 @@ status fs a d = minimum (actorStatus a : map frameStatus fs)
   frameStatus Binding{} = Done
   frameStatus UnificationProblem{} = StuckOn d
   frameStatus Noted = Done
+  frameStatus (Extended _ _) = Done
 
 data Process l s t
   = Process
diff --git a/Src/Machine/Display.hs b/Src/Machine/Display.hs
index 46f7fce..431f301 100644
--- a/Src/Machine/Display.hs
+++ b/Src/Machine/Display.hs
@@ -109,6 +109,7 @@ instance Display Frame where
       pure $ withANSI [SetColour Background Red]
            $ s <+> "~?" <> brackets date <+> t
     Noted -> pure "Noted"
+    Extended op cl -> pure $ pretty op <+> "+= <fun>"
 
 instance (Show (t Frame), Traversable t, Collapse t, Display0 s)
   => Display (Process log s t) where
diff --git a/Src/Machine/Exec.hs b/Src/Machine/Exec.hs
index 60373ae..518e24f 100644
--- a/Src/Machine/Exec.hs
+++ b/Src/Machine/Exec.hs
@@ -6,6 +6,7 @@ import qualified Data.Set as Set
 import Data.Maybe (fromJust)
 import Unelaboration.Monad (nameSel)
 
+import Control.Monad (when)
 import Control.Monad.Reader
 
 import Alarm
@@ -36,6 +37,7 @@ import System.IO.Unsafe
 import Debug.Trace
 import Operator.Eval
 
+dmesg :: String -> b -> b
 dmesg = trace
 
 lookupRules :: JudgementName -> Bwd Frame -> Maybe (AProtocol, (Channel, AActor))
@@ -243,7 +245,7 @@ unify :: HeadUpData -> Process Shots Store Cursor -> Process Shots Store []
 --unify (Process zf'@(zf :<+>: up@(UnificationProblem s t) : fs) _ _ store a)
 --  | dmesg ("\nunify\n  " ++ show t ++ "\n  " ++ show store ++ "\n  " ++ show a) False = undefined
 unify dat p | debug MachineUnify "" p = undefined
-unify dat p@Process { stack = zf :<+>: UnificationProblem date s t : fs, ..} =
+unify dat p@Process { stack = zf :<+>: UnificationProblem date s t : fs } =
   case (expand (headUp dat s), expand (headUp dat t)) of
     (s, t) | s == t      -> unify dat (p { stack = zf :<+>: fs })
     (a :%: b, a' :%: b') -> unify dat (p { stack = zf :<+>: UnificationProblem date a a' : UnificationProblem date b b' : fs })
@@ -282,6 +284,9 @@ deepCheck dat th tm p =
                   let p' = p { root = root' }
                   let store'' = updateStore m (xm $: sbstI (weeEnd th') *^ th') store'
                   pure ((xm :$) $^ sg', p' { store = store'' })
+    G g rt -> do
+      (t, p) <- deepCheck dat th (CdB rt ph) p
+      pure (G g $^ t, p)
 
 strengthenSbst :: HeadUpData
                -> Th        -- D0 <= D
@@ -313,6 +318,7 @@ solveMeta m (CdB (S0 :^^ _) th) tm p@Process{..} = do
   let dat = mkHeadUpData (p{ stack = let (fs :<+>: _) = stack in fs})
   (tm, p) <- deepCheck dat th tm p
   return (p { store = updateStore m tm store })
+solveMeta _ _ _ _ = error "Broken invariant"
 
 
 connect :: AConnect
@@ -326,10 +332,11 @@ connect ac@(AConnect ch1 th ch2 n) p@Process { stack = zf :< Sent q gd tm :<+>:
                (p { stack = zf <>< fs :<+>: []
                   , actor = aconnect unknown ch1 th ch2 (n-1)})
   where th' = ones (length (globalScope env)) <> th
-connect ac p@Process { stack = zf'@(zf :< Spawnee intf) :<+>: fs, ..}
+connect ac p@Process { stack = zf'@(zf :< Spawnee intf) :<+>: fs }
   = move (p { stack = zf' <>< fs :<+>: []})
 connect ac p@Process { stack = zf :< f :<+>: fs}
   = connect ac (p { stack = zf :<+>: (f:fs) })
+connect _ _ = error "Unhandled input"
 
 send :: Channel -> Maybe Guard -> Term
      -> Process Shots Store Cursor
@@ -340,7 +347,7 @@ send :: Channel -> Maybe Guard -> Term
 --   | debug MachineSend (unwords [ch, show term]) p
 --   = undefined
 
-send ch gd term p@Process { stack = B0 :<+>: fs, ..}
+send ch gd term p@Process { stack = B0 :<+>: fs }
   -- TODO: use the range of the send?
   = let a = Fail unknown [StringPart ("Couldn't find channel " ++ rawChannel ch)]
     in exec (p { stack = B0 <>< fs, actor = a })
@@ -355,7 +362,7 @@ send ch gd term
   in debug MachineSend (pretty ch) p' `seq` exec p'
 send ch gd term
   p@Process { stack = zf'@(zf :< Spawnee (Interface (Hole, q) (rxs@(r, xs), parentP) jd jdp em tr)) :<+>: fs
-            , ..}
+            }
   | ch == q =
   let parentP' = parentP { stack = Sent r gd (xs, term) : stack parentP, store = New }
       stack'   = zf :< Spawnee (Interface (Hole, q) (rxs, parentP') jd jdp em (tr :< term)) <>< fs
diff --git a/Src/Machine/Matching.hs b/Src/Machine/Matching.hs
index 27048cc..f39e9cc 100644
--- a/Src/Machine/Matching.hs
+++ b/Src/Machine/Matching.hs
@@ -131,3 +131,15 @@ instThicken hnf ph t = let tmnf = hnf t in case tmnf of
         (t, rest) -> (s % t, (%) <$> ress <*> rest)
     (x :.: t) -> case instThicken hnf (ph -? True) t of
       (b, resb) -> (x \\ b, (x \\) <$> resb)
+    VX{} -> error "Already handled"
+    _ :$: _ -> error "Already handled"
+    f :-: t -> case instThicken hnf ph f of
+      (f, Left Mismatch) -> (P Oper $^ (f <&> t), Left Mismatch)
+      (f, resf) -> case instThicken hnf ph t of
+        (t, rest) -> (P Oper $^ (f <&> t), (P Oper $^) <$> ((<&>) <$> resf <*> rest))
+    s ::: t -> case instThicken hnf ph s of
+      (s, Left Mismatch) -> (rad s t, Left Mismatch)
+      (s, ress) -> case instThicken hnf ph t of
+        (t, rest) -> (rad s t, rad <$> ress <*> rest)
+    GX g s -> case instThicken hnf ph s of
+      (s, res) -> (G g $^ s, (G g $^) <$> res)
diff --git a/Src/Machine/Trace.hs b/Src/Machine/Trace.hs
index 056d418..a9bdd6b 100644
--- a/Src/Machine/Trace.hs
+++ b/Src/Machine/Trace.hs
@@ -10,6 +10,7 @@ import Data.Bitraversable
 
 import Data.List (intersperse, elemIndex, groupBy, sortBy)
 import Data.Function (on)
+import Data.Kind (Type)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import Data.Maybe (fromMaybe)
@@ -53,7 +54,7 @@ instance (Show e, Show (i ann)) => Show (Trace e i ann) where
     go indt (Node _ i ts) = (indt ++ show i) : concatMap (go (' ':indt)) ts
     go indt (Error _ e)   = [indt ++ show e]
 
-type family ITERM (ph :: Phase) :: *
+type family ITERM (ph :: Phase) :: Type
 type instance ITERM Abstract = Term
 type instance ITERM Concrete = Raw
 
@@ -157,6 +158,9 @@ newtype Series t ann = Series { runSeries :: [(t, ann)] }
 mkSeries :: t -> ann -> Series t ann
 mkSeries t a = Series [(t, a)]
 
+instance Functor (Simple t) where
+  fmap f (Simple t a) = Simple t (f a)
+
 instance Bifunctor Simple where
   bimap f g (Simple t a) = Simple (f t) (g a)
 
@@ -182,6 +186,7 @@ instance LaTeX (Series () (Int, Bool)) where
   toLaTeX d (Series ibs)
     = do let ibss = groupBy ((==) `on` fst) $ sortBy (compare `on` snd) $ map snd ibs
          (ibss, ibs) <- case B0 <>< ibss of
+                          B0 -> error "Broken invariant"
                           ibz :< ibs -> pure (ibz <>> [], ibs)
                           -- Famous last words: trust me that's the only case
          let doc = display1 ibs
@@ -218,6 +223,7 @@ instance (Eq t, LaTeX t) => LaTeX (Series t Int) where
   toLaTeX d (Series tanns)
     = do let tnss = groupBy ((==) `on` fst) $ sortBy (compare `on` snd) tanns
          (tnss, tns) <- case B0 <>< tnss of
+                          B0 -> error "Broken invariant"
                           tnz :< tns -> pure (tnz <>> [], tns)
                           -- Famous last words: trust me that's the only case
          doc <- display1 tns
@@ -228,6 +234,7 @@ instance (Eq t, LaTeX t) => LaTeX (Series t Int) where
 
       where
         display1 :: [(t, Int)] -> LaTeXM (Doc ())
+        display1 [] = error "Broken invariant"
         display1 tns@((t, _) : _) = do
           let ns = map snd tns
           let start = minimum ns
diff --git a/Src/Main.hs b/Src/Main.hs
index 4fee631..cdf6925 100644
--- a/Src/Main.hs
+++ b/Src/Main.hs
@@ -97,6 +97,11 @@ label col lbl opts str =
   ANSI.withANSI (SetColour Background Yellow <$ guard (colours opts)) (lbl ++ ":")
   ++ str
 
+warning :: Options -> String -> String
 warning = label Yellow "Warning"
+
+success :: Options -> String -> String
 success = label Green "Success"
+
+anerror :: Options -> String -> String
 anerror = label Red "Error"
diff --git a/Src/Operator.hs b/Src/Operator.hs
index b401560..f1ffe80 100644
--- a/Src/Operator.hs
+++ b/Src/Operator.hs
@@ -3,6 +3,7 @@ module Operator where
 
 import Control.Applicative
 import Data.Foldable
+import Data.Kind (Type)
 
 import Concrete.Base
 import Concrete.Parse
@@ -73,7 +74,7 @@ scopeSize = length . getObjVars
 -- e.g. ['Pi S \x.T]
 --    - S has a SOT, binding nothing
 --    - T has a SOT, binding x with type S[]
-type family SOT (ph :: Phase) :: *
+type family SOT (ph :: Phase) :: Type
 type instance SOT Concrete = CSOT
 type instance SOT Abstract = ASOT
 
@@ -130,7 +131,10 @@ type AAnOperator = ANOPERATOR Abstract
 newtype Operator = Operator { getOperator :: String }
   deriving (Show, Eq)
 
-type family OPERATOR (ph :: Phase) :: *
+instance Pretty Operator where
+  pretty = pretty . getOperator
+
+type family OPERATOR (ph :: Phase) :: Type
 type instance OPERATOR Concrete = WithRange String
 type instance OPERATOR Abstract = Operator
 
@@ -144,13 +148,13 @@ type AClause m = (Show m, UnelabMeta m)
 newtype Clause = Clause { runClause :: forall m . AClause m }
 
 instance Semigroup Clause where
-  (<>) = mappend
+  cl1 <> cl2 = Clause $ \ opts hd env ops -> case runClause cl2 opts hd env ops of
+    Left ops -> runClause cl1 opts hd env ops
+    Right t -> Right t
 
 instance Monoid Clause where
   mempty = Clause $ \ _ _ _ -> Left
-  mappend cl1 cl2 = Clause $ \ opts hd env ops -> case runClause cl2 opts hd env ops of
-    Left ops -> runClause cl1 opts hd env ops
-    Right t -> Right t
+  mappend = (<>)
 
 instance Show Clause where
   show _ = "<fun>"
@@ -159,7 +163,7 @@ type OPPATTERN ph = (PATTERN ph     -- type acted on
                     , OPERATOR ph   -- operator
                     , [PATTERN ph]) -- parameters
 
-type family DEFNOP (ph :: Phase) :: *
+type family DEFNOP (ph :: Phase) :: Type
 type instance DEFNOP Concrete = (PATTERN Concrete       -- object
                                 , [OPPATTERN Concrete]  -- spine (must be non-empty)
                                 , TERM Concrete)        -- right hand side
diff --git a/Src/Pattern/Coverage.hs b/Src/Pattern/Coverage.hs
index 4d5d373..095466a 100644
--- a/Src/Pattern/Coverage.hs
+++ b/Src/Pattern/Coverage.hs
@@ -24,7 +24,7 @@ import Thin (is1s, scope)
 import Hide (Hide(Hide))
 import Semantics
 import Operator.Eval (HeadUpData')
-import Actor (ActorMeta(..))
+import Actor (ActorMeta)
 import Syntax (SyntaxTable, SyntaxCat, WithSyntaxCat(..))
 
 ------------------------------------------------------------------------------
@@ -282,7 +282,7 @@ missing dat table desc = fmap (`evalState` names) (start desc) where
   -- "a", "b", ..., "z", "a1", "b1", ...
   names :: [String]
   names = concat
-        $ zipWith (map . flip (++)) ("" : map show [1..])
+        $ zipWith (map . flip (++)) ("" : map show [(1 :: Integer)..])
         $ repeat (map pure "abcdefghijklmnopqrstuvwxyz")
 
   freshName :: State [String] String
@@ -312,7 +312,6 @@ missing dat table desc = fmap (`evalState` names) (start desc) where
     in fromList (concatMap toList (enums ++ tagged))
   go (VWildcard _)= (pure $ UnderscoreP unknown) :| []
   go (VSyntaxCat _ _) = (VarP unknown . Variable unknown <$> freshName) :| []
-{- TODO: fill in, neutral case might be impossible
-  go (VNeutral _) = _
+  go (VNeutral _) = undefined -- TODO
   go (VUniverse _) = (pure $ AtP unknown "Semantics") :| []
-  go (VPi _ _) = _ -}
+  go (VPi _ _) = undefined -- TODO
diff --git a/Src/Semantics.hs b/Src/Semantics.hs
index d4440f9..72ad017 100644
--- a/Src/Semantics.hs
+++ b/Src/Semantics.hs
@@ -7,6 +7,7 @@ import Control.Applicative
 import Data.Void
 -- import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Maybe (fromMaybe)
 
 -- import Hide
 import Bwd
@@ -155,7 +156,8 @@ typecheck :: SyntaxTable
           -> Bool
 typecheck table env dat = check where
   check :: Bwd ASemanticsDesc -> ASemanticsDesc -> ACTm -> Bool
-  check ctx ty t = let (Just vty) = expand table dat ty in case Term.expand t of
+  check ctx ty t = let vty = fromMaybe (error "Broken invariant") (expand table dat ty) in
+   case Term.expand t of
     _ | VWildcard _ <- vty -> True
     VX v sc -> ty == var ctx sc v -- should maybe be up to unfolding (which might be undecidable)
     AX a sc -> case vty of
@@ -185,6 +187,7 @@ typecheck table env dat = check where
       VBind cat ty0 -> check (ctx :< atom cat (scope t)) ty0 t0
       VPi ty0 (_, ty1) -> check (ctx :< ty0) ty1 t0
       _ -> False
+    m ::: n -> undefined -- TODO REVERT
     m :$: t0 -> undefined -- TODO REVERT
     GX _ t0 -> check ctx ty t0
 
diff --git a/Src/Syntax.hs b/Src/Syntax.hs
index 537a7ef..67f441c 100644
--- a/Src/Syntax.hs
+++ b/Src/Syntax.hs
@@ -114,6 +114,7 @@ validate table = go where
   go :: Show m => Bwd SyntaxCat -> ASyntaxDesc -> CdB (Tm m) -> Bool
   go env s t@(CdB V th) = reportError s t $ ($ s) $ asRec $ \ a -> a == env <! (dbIndex $ lsb th)
   go env s t = reportError s t $ ($ t) $ flip (maybe bust) (Syntax.expand table s) $ \case
+    VSyntaxCat c -> absurd c
     VAtom -> asAtom $ \ (a,_) -> not (null a)
     VAtomBar as -> asAtom $ \ (a,_) -> not (a `elem` as)
     VNil  -> asAtom $ \ (a,_) -> null a
@@ -185,4 +186,5 @@ validateDesc syns =
              , ("Semantics", wildcard)] -- TODO : change
 
 
+validateIt :: Bool
 validateIt = validateDesc ["Syntax"] (syntaxDesc ["Syntax"])
diff --git a/Src/Syntax/Debug.hs b/Src/Syntax/Debug.hs
index 8019f0a..8d7880c 100644
--- a/Src/Syntax/Debug.hs
+++ b/Src/Syntax/Debug.hs
@@ -8,6 +8,7 @@ import Machine.Display()
 import Unelaboration.Monad (initNaming)
 import Text.PrettyPrint.Compact (render)
 
+printIt :: IO ()
 printIt = putStrLn $ unlines
   [ show validateIt
   , "==="
diff --git a/Src/Term/Mangler.hs b/Src/Term/Mangler.hs
index 0758ea1..c4d7f20 100644
--- a/Src/Term/Mangler.hs
+++ b/Src/Term/Mangler.hs
@@ -2,7 +2,9 @@ module Term.Mangler where
 
 import Control.Monad.Writer
 import Control.Applicative
+
 import qualified Data.Map as Map
+import Data.Monoid (Any(..))
 
 import Thin
 import Hide
@@ -78,6 +80,7 @@ instance Manglable (Tm Meta) where
   mangle mu V = mangV mu
   mangle mu (A a) = pure (atom a (mangTgt mu))
   mangle mu (P k p) = (P k $^) <$> mangle mu p
+  mangle mu (G g p) = (G g $^) <$> mangle mu p
   mangle mu ((Hide x := False) :. t) = (x \\) <$> (weak <$> mangle mu t)
   mangle mu ((Hide x := True) :. t) = (x \\) <$> mangle (mangB mu) t
   mangle mu (m :$ sg) = mangM mu m (mangle mu sg)
diff --git a/Src/Term/Substitution.hs b/Src/Term/Substitution.hs
index ba59d5c..b4f6cf7 100644
--- a/Src/Term/Substitution.hs
+++ b/Src/Term/Substitution.hs
@@ -7,7 +7,10 @@ import Hide
 import Thin
 import Term.Base hiding (expand)
 
+import GHC.Stack (HasCallStack)
+
 -- import Debug.Trace
+track :: a -> b -> b
 track = const id
 -- track = trace
 
@@ -33,7 +36,7 @@ tth@(CdB t th) //^ sgph@(CdB sg ph) =
 --       track "\n" $
        res
 
-(//) :: Tm m -> Sbst m -> Tm m
+(//) :: HasCallStack => Tm m -> Sbst m -> Tm m
 t // (S0 :^^ _) = t
 V // (ST (_ :<>: CdB (_ := t) _) :^^ 0) = t
 P p (CdB tl thl :<>: CdB tr thr) // sg =
@@ -43,6 +46,7 @@ P p (CdB tl thl :<>: CdB tr thr) // sg =
 ((x := b) :. t) // (sg :^^ w) = (x := b) :. (t // (sg :^^ if b then w+1 else w))
 (m :$ rh) // sg = m :$ (rh /// sg)
 (G g t) // sg = G g (t // sg)
+_ // _ = error "Broken invariant"
 
 (///) :: Sbst m -> Sbst m -> Sbst m
 (S0 :^^ _) /// sg = sg
diff --git a/Src/Thin.hs b/Src/Thin.hs
index c18e9c5..d29e1b0 100644
--- a/Src/Thin.hs
+++ b/Src/Thin.hs
@@ -212,10 +212,11 @@ riffle (iz :< i, th) (jz, ph) = case thun th of
   (th, True) -> case (jz, thun ph) of
     (jz :< _, (ph, True)) -> riffle (iz, th) (jz, ph) :< i
     (jz, (ph, False))     -> riffle (iz, th) (jz, ph) :< i
+    _ -> error "Broken invariant"
   (th, False) -> case (jz, thun ph) of
     (jz :< j, (ph, True)) -> riffle (iz, th) (jz, ph) :< j
     (jz, (ph, False))     -> riffle (iz, th) (jz, ph)
-
+    _ -> error "Broken invariant"
 
 -- pullback th ph = (th*ph, ps, ph*th)
 --   o--th*ph-->o
diff --git a/Src/Unelaboration.hs b/Src/Unelaboration.hs
index dba3dc9..4178d22 100644
--- a/Src/Unelaboration.hs
+++ b/Src/Unelaboration.hs
@@ -2,6 +2,7 @@
 
 module Unelaboration where
 
+import Control.Monad (when)
 import Control.Monad.Except
 import Control.Monad.Reader
 
@@ -107,6 +108,7 @@ instance Unelab Pat where
       pure (LamP unknown (Scope (mkBinder . Variable unknown <$> x) p))
     MP m th -> {- TODO: insert ThP -} VarP unknown <$> subunelab m
     HP -> pure (UnderscoreP unknown)
+    GP -> pure (UnderscoreP unknown)
 
 instance Unelab (Pat, AActor) where
   type UnelabEnv (Pat, AActor) = DAEnv
@@ -200,12 +202,14 @@ instance Unelab AScrutinee where
       case v of
         -- Sbst _ _ (Var r m) -> pure (ActorVar r m)
         Var r m -> pure (SubjectVar r m)
+        _ -> error "Broken invariant"
     Pair r s t -> Pair r <$> unelab s <*> unelab t
     Lookup r stk t -> do
       stk <- subunelab stk
       t <- unelab t >>= \case
         -- Sbst _ _ (Var r m) -> pure m
         Var r m -> pure m
+        _ -> error "Broken invariant"
       pure $ Lookup r stk t
     Compare r s t -> Compare r <$> unelab s <*> unelab t
     Term r t -> Term r <$> unelab t
diff --git a/Src/Utils.hs b/Src/Utils.hs
index 1688840..f96e80c 100644
--- a/Src/Utils.hs
+++ b/Src/Utils.hs
@@ -4,6 +4,7 @@ import Data.Set (Set)
 import qualified Data.Set as Set
 import Data.These (These(..))
 
+import Control.Monad (when, unless, liftM2)
 import Control.Monad.State
 
 isAllJustBy :: [a] -> (a -> Maybe b) -> Either a [b]
diff --git a/typos.cabal b/typos.cabal
index 4f7ddbd..e446fde 100644
--- a/typos.cabal
+++ b/typos.cabal
@@ -26,10 +26,24 @@ common haskell
                        StandaloneDeriving,
                        TupleSections,
                        TypeFamilies,
+                       TypeOperators,
                        TypeSynonymInstances
 
+common warnings
+    -- Silence some flags
+    ghc-options:  -Wall
+                  -Wno-name-shadowing
+                  -Wno-noncanonical-monad-instances
+                  -Wno-noncanonical-monoid-instances
+                  -Wno-unused-do-bind
+                  -Wno-unused-local-binds
+                  -Wno-unused-matches
+                  -Wno-unused-top-binds
+                  -Wno-orphans
+                  -Werror=incomplete-patterns
+
 library
-  import:              haskell
+  import:              haskell, warnings
   exposed-modules:     Actor,
                        Actor.Display,
                        Alarm,
@@ -91,10 +105,10 @@ library
   hs-source-dirs:      Src
   default-language:    Haskell2010
   ghc-options:         -Wunused-imports
---                       -fwarn-incomplete-patterns
+                       -fwarn-incomplete-patterns
 
 executable typos
-  import:              haskell
+  import:              haskell, warnings
   main-is:             Src/Main.hs
   build-depends:       base <5
                      , mtl