diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,11 @@
 # Revision history for haskell-candid
 
+## 0.4-- 2022-11-05
+
+* Fix did file parsing bug: Allow underscores in unicode escapes
+* Implement the new subtyping rules from spec version 0.1.4
+  https://github.com/dfinity/candid/pull/311
+
 ## 0.3.2.1 -- 2022-12-01
 
 * GHC-9.2 compatibility
diff --git a/candid.cabal b/candid.cabal
--- a/candid.cabal
+++ b/candid.cabal
@@ -1,6 +1,6 @@
 cabal-version:      >=1.10
 name:               candid
-version:            0.3.2.1
+version:            0.4
 license:            Apache
 license-file:       LICENSE
 maintainer:         mail@joachim-breitner.de
@@ -41,6 +41,7 @@
         Codec.Candid.EncodeTextual
         Codec.Candid.Encode
         Codec.Candid.Infer
+        Codec.Candid.Subtype
         Codec.Candid.Coerce
 
     default-language: Haskell2010
@@ -89,6 +90,7 @@
     hs-source-dirs:   test
     other-modules:
         SpecTests
+        Tests
         THTests
 
     default-language: Haskell2010
diff --git a/src/Codec/Candid.hs b/src/Codec/Candid.hs
--- a/src/Codec/Candid.hs
+++ b/src/Codec/Candid.hs
@@ -1,8 +1,6 @@
 {-|
 
-This module provides preliminary Haskell supprot for decoding and encoding the __Candid__ data format. See <https://github.com/dfinity/candid/blob/master/spec/Candid.md> for the official Candid specification.
-
-__Warning:__ The interface of this library is still in flux, as we are yet learning the best idioms around Candid and Haskell.
+This module provides Haskell support for decoding and encoding the __Candid__ data format. See <https://github.com/dfinity/candid/blob/master/spec/Candid.md> for the official Candid specification.
 
 -}
 
@@ -49,7 +47,6 @@
 {- |
 
 * Generating interface descriptions (.did files) from Haskell functions
-* Future types
 * Parsing the textual representation dynamically against an expected type
 
 -}
@@ -118,6 +115,7 @@
  , unescapeFieldName
  , candidHash
  , Value(..)
+ , isSubtypeOf
 
 -- ** Dynamic use
 
@@ -150,15 +148,18 @@
 import Codec.Candid.Decode
 import Codec.Candid.Encode
 import Codec.Candid.EncodeTextual
+import Codec.Candid.Subtype
 
 -- $setup
 -- >>> :set -dppr-cols=200
 -- >>> import Data.Text (Text)
 -- >>> import qualified Data.Text as T
--- >>> import Data.Void (Void)
+-- >>> import Data.Void (Void, vacuous)
 -- >>> import Prettyprinter (pretty)
 -- >>> import qualified Data.ByteString.Lazy.Char8 as BS
+-- >>> import Numeric.Natural
 -- >>> :set -XScopedTypeVariables
+-- >>> :set -XTypeApplications
 
 {- $haskell_types
 
@@ -169,7 +170,7 @@
 >>> decode (encode ([True, False], Just 100)) == Right ([True, False], Just 100)
 True
 
-Here, no type annotations are needed, the library can infer them from the types of the Haskell values. You can see the Candid types used using `typeDesc` and `seqDesc`:
+Here, no type annotations are needed, the library can infer them from the types of the Haskell values. You can see the Candid types used using `seqDesc` (with `tieKnot`) for an argument sequence, or `typeDesc` for a single type:
 
 >>> :type +d ([True, False], Just 100)
 ([True, False], Just 100) :: ([Bool], Maybe Integer)
@@ -188,6 +189,8 @@
 >>> pretty (typeDesc @(Rec ("bar" .== Maybe Integer .+ "foo" .== [Bool])))
 record {bar : opt int; foo : vec bool}
 
+NB: `typeDesc` cannot work with recursive types, but see `seqDesc` together with `tieKnot`.
+
 -}
 
 {- $own_type
@@ -375,7 +378,7 @@
 
 Sometimes one needs to interact with Candid in a dynamic way, without static type information.
 
-This library allows the parsing and pretty-printing of candid values. The binary value was copied from above:
+This library allows the parsing and pretty-printing of candid values:
 
 >>> import Data.Row
 >>> :set -XDataKinds -XTypeOperators
@@ -401,6 +404,19 @@
 Right (#bar .== Just 100 .+ #foo .== [True,False])
 
 This function does not support the full textual format yet; in particular type annotations can only be used around number literals.
+
+Related to dynamic use is the ability to perform a subtype check, using 'isSubtypeOf' (but you have to set up the arguments correctly first):
+
+>>> isSubtypeOf (vacuous $ typeDesc @Natural) (vacuous $ typeDesc @Integer)
+Right ()
+>>> isSubtypeOf (vacuous $ typeDesc @Integer) (vacuous $ typeDesc @Natural)
+Left "Type int is not a subtype of nat"
+>>> isSubtypeOf (vacuous $ typeDesc @(Rec ("foo" .== [Bool]))) (vacuous $ typeDesc @(Rec ("bar" .== Maybe Integer .+ "foo" .== Maybe [Bool])))
+Right ()
+>>> isSubtypeOf (vacuous $ typeDesc @(Rec ("bar" .== Maybe Integer .+ "foo" .== Maybe [Bool]))) (vacuous $ typeDesc @(Rec ("foo" .== [Bool])))
+Left "Type opt vec bool is not a subtype of vec bool"
+>>> isSubtypeOf (vacuous $ typeDesc @(Rec ("bar" .== Integer))) (vacuous $ typeDesc @(Rec ("foo" .== Integer)))
+Left "Missing record field foo of type int"
 
 -}
 
diff --git a/src/Codec/Candid/Class.hs b/src/Codec/Candid/Class.hs
--- a/src/Codec/Candid/Class.hs
+++ b/src/Codec/Candid/Class.hs
@@ -73,8 +73,7 @@
     -- Decode
     (ts, vs) <- decodeVals b
     -- Coerce to expected type
-    c <- coerceSeqDesc ts (buildSeqDesc (asTypes @(AsTuple a)))
-    vs' <- c vs
+    vs' <- coerceSeqDesc vs ts (buildSeqDesc (asTypes @(AsTuple a)))
     fromCandidVals vs'
 
 -- | Decode (dynamic) values to Haskell type
@@ -106,9 +105,12 @@
 seqDesc :: forall a. CandidArg a => SeqDesc
 seqDesc = buildSeqDesc (asTypes @(AsTuple a))
 
+typeGraph :: forall a. Candid a => Type (Ref TypeRep Type)
+typeGraph = asType @(AsCandid a)
+
 -- | NB: This will loop with recursive types!
 typeDesc :: forall a. Candid a => Type Void
-typeDesc = asType @(AsCandid a) >>= go
+typeDesc = typeGraph @a >>= go
   where go (Ref _ t) = t >>= go
 
 instance Pretty TypeRep where
diff --git a/src/Codec/Candid/Coerce.hs b/src/Codec/Candid/Coerce.hs
--- a/src/Codec/Candid/Coerce.hs
+++ b/src/Codec/Candid/Coerce.hs
@@ -5,9 +5,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 module Codec.Candid.Coerce
   ( coerceSeqDesc
-  , SeqCoercion
   , coerce
-  , Coercion
   )
   where
 
@@ -15,243 +13,159 @@
 import qualified Data.Vector as V
 import qualified Data.ByteString.Lazy as BS
 import qualified Data.Map as M
-import Data.Bifunctor
-import Data.List
-import Data.Tuple
 import Control.Monad.State.Lazy
 import Control.Monad.Except
 
 import Codec.Candid.FieldName
 import Codec.Candid.Types
 import Codec.Candid.TypTable
-
-type SeqCoercion = [Value] -> Either String [Value]
-type Coercion = Value -> Either String Value
+import Codec.Candid.Subtype
 
-coerceSeqDesc :: SeqDesc -> SeqDesc -> Either String SeqCoercion
-coerceSeqDesc sd1 sd2 =
+coerceSeqDesc :: [Value] -> SeqDesc -> SeqDesc -> Either String [Value]
+coerceSeqDesc vs sd1 sd2 =
     unrollTypeTable sd1 $ \ts1 ->
     unrollTypeTable sd2 $ \ts2 ->
-    coerceSeq ts1 ts2
+    coerceSeq vs ts1 ts2
 
 coerceSeq ::
     (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
+    [Value] ->
     [Type (Ref k1 Type)] ->
     [Type (Ref k2 Type)] ->
-    Either String SeqCoercion
-coerceSeq t1 t2 = runM $ goSeq t1 t2
+    Either String [Value]
+coerceSeq vs t1 t2 = runSubTypeM $ goSeq vs t1 t2
 
--- | This function implements the `C[<t> <: <t>]` coercion function from the
--- spec. It returns `Left` if no subtyping relation holds, or `Right c` if it
--- holds, together with a coercion function.
+-- | This function implements the @V : T ~> V' : T'@ relation from the Candid spec.
 --
--- The coercion function itself is not total because the intput value isn’t
--- typed, so we have to cater for errors there. It should not fail if the
--- passed value really is inherently of the input type.
+-- Because values in this library are untyped, we have to pass what we know about
+-- their type down, so that we can do the subtype check upon a reference.
+-- The given type must match the value closely (as it is the case when decoding
+-- from the wire) and this function may behave oddly if @v@ and @t1@ are not related.
 --
--- In a dependently typed language we’d maybe have something like
--- `coerce :: foreach t1 -> foreach t2 -> Either String (t1 -> t2)`
--- instead, and thus return a total function
+-- Morally, this function looks only at @v@ and @t2@. It only needs @t1@ for
+-- refences, and hence needs to take @t2@ apart for the recursive calls.
+-- Practically, it's sometimes more concise to look at t2 instead of v.
 coerce ::
     (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
+    Value ->
     Type (Ref k1 Type) ->
     Type (Ref k2 Type) ->
-    Either String Coercion
-coerce t1 t2 = runM $ memo t1 t2
-
-type Memo k1 k2 =
-    (M.Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
-     M.Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion)
-type M k1 k2 = ExceptT String (State (Memo k1 k2))
-
-runM :: (Ord k1, Ord k2) => M k1 k2 a -> Either String a
-runM act = evalState (runExceptT act) (mempty, mempty)
-
-flipM :: M k1 k2 a -> M k2 k1 a
-flipM (ExceptT (StateT f)) = ExceptT (StateT f')
-  where
-    f' (m1,m2) = second swap <$> f (m2,m1) -- f (m2,m1) >>= \case (r, (m2',m1')) -> pure (r, (m1', m2'))
+    Either String Value
+coerce v t1 t2 = runSubTypeM $ go v t1 t2
 
-memo, go ::
+go ::
     (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
+    Value ->
     Type (Ref k1 Type) ->
     Type (Ref k2 Type) ->
-    M k1 k2 Coercion
+    SubTypeM k1 k2 Value
 
 goSeq ::
     (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
+    [Value] ->
     [Type (Ref k1 Type)] ->
     [Type (Ref k2 Type)] ->
-    M k1 k2 SeqCoercion
-
-
--- Memoization uses lazyiness: When we see a pair for the first time,
--- we optimistically put the resulting coercion into the map.
--- Either the following recursive call will fail (but then this optimistic
--- value was never used), or it will succeed, but then the guess was correct.
-memo t1 t2 = do
-  gets (M.lookup (t1,t2) . fst) >>= \case
-    Just c -> pure c
-    Nothing -> mdo
-        modify (first (M.insert (t1,t2) c))
-        c <- go t1 t2
-        return c
+    SubTypeM k1 k2 [Value]
 
 -- Look through refs
-go (RefT (Ref _ t1)) t2 = memo t1 t2
-go t1 (RefT (Ref _ t2)) = memo t1 t2
+go v (RefT (Ref _ t1)) t2 = go v t1 t2
+go v t1 (RefT (Ref _ t2)) = go v t1 t2
 
 -- Identity coercion for primitive values
-go NatT NatT = pure pure
-go Nat8T Nat8T = pure pure
-go Nat16T Nat16T = pure pure
-go Nat32T Nat32T = pure pure
-go Nat64T Nat64T = pure pure
-go IntT IntT = pure pure
-go Int8T Int8T = pure pure
-go Int16T Int16T = pure pure
-go Int32T Int32T = pure pure
-go Int64T Int64T = pure pure
-go Float32T Float32T = pure pure
-go Float64T Float64T = pure pure
-go BoolT BoolT = pure pure
-go TextT TextT = pure pure
-go NullT NullT = pure pure
-go PrincipalT PrincipalT = pure pure
+go v NatT NatT = pure v
+go v Nat8T Nat8T = pure v
+go v Nat16T Nat16T = pure v
+go v Nat32T Nat32T = pure v
+go v Nat64T Nat64T = pure v
+go v IntT IntT = pure v
+go v Int8T Int8T = pure v
+go v Int16T Int16T = pure v
+go v Int32T Int32T = pure v
+go v Int64T Int64T = pure v
+go v Float32T Float32T = pure v
+go v Float64T Float64T = pure v
+go v BoolT BoolT = pure v
+go v TextT TextT = pure v
+go v NullT NullT = pure v
+go v PrincipalT PrincipalT = pure v
 
 -- Nat <: Int
-go NatT IntT = pure $ \case
-    NatV n -> pure $ IntV (fromIntegral n)
-    v -> throwError $ show $ "Unexpected value" <+> pretty v <+> "while coercing nat <: int"
+go (NatV n) NatT IntT = pure $ IntV (fromIntegral n)
 
 -- t <: reserved
-go _ ReservedT = pure (const (pure ReservedV))
+go _ _ ReservedT = pure ReservedV
 
--- empty <: t
-go EmptyT _ = pure $ \v ->
-    throwError $ show $ "Unexpected value" <+> pretty v <+> "while coercing empty"
+-- empty <: t (actually just a special case of `v :/ t`)
+go v EmptyT _ = throwError $ show $ "Unexpected value" <+> pretty v <+> "while coercing empty"
 
 -- vec t1 <: vec t2
-go (VecT t1) (VecT t2) = do
-    c <- memo t1 t2
-    pure $ \case
-        VecV vs -> VecV <$> mapM c vs
-        v -> throwError $ show $ "Unexpected value" <+> pretty v <+> "while coercing vector"
+go (VecV vs) (VecT t1) (VecT t2) = VecV <$> mapM (\v -> go v t1 t2) vs
 
 -- Option: The normal rule
-go (OptT t1) (OptT t2) = lift (runExceptT (memo t1 t2)) >>= \case
-    Right c -> pure $ \case
-        OptV Nothing -> pure (OptV Nothing)
-        OptV (Just v) -> OptV . Just <$> c v
-        v -> throwError $ show $ "Unexpected value" <+> pretty v <+> "while coercing option"
-    Left _ -> pure (const (pure (OptV Nothing)))
+go (OptV Nothing)  (OptT _) (OptT _) = pure NullV
+go (OptV (Just v)) (OptT t1) (OptT t2) =
+    lift (runExceptT (go v t1 t2)) >>= \case
+        Right v' -> pure (OptV (Just v'))
+        Left _   -> pure (OptV Nothing)
 
 -- Option: The constituent rule
-go t (OptT t2) | not (isOptLike t2) = lift (runExceptT (memo t t2)) >>= \case
-    Right c -> pure $ \v -> OptV . Just <$> c v
-    Left _ -> pure (const (pure (OptV Nothing)))
+go v t1 (OptT t2) | not (isOptLike t2) =
+    lift (runExceptT (go v t1 t2)) >>= \case
+        Right v' -> pure (OptV (Just v'))
+        Left _   -> pure (OptV Nothing)
+
 -- Option: The fallback rule
-go _ (OptT _) = pure (const (pure (OptV Nothing)))
+go _ _ (OptT _) = pure (OptV Nothing)
 
 -- Records
-go (RecT fs1) (RecT fs2) = do
-    let m1 = M.fromList fs1
-    let m2 = M.fromList fs2
-    new_fields <- sequence
-            [ case unRef t of
-                OptT _ -> pure (fn, OptV Nothing)
-                ReservedT -> pure (fn, ReservedV)
-                t -> throwError $ show $ "Missing record field" <+> pretty fn <+> "of type" <+> pretty t
-            | (fn, t) <- M.toList $ m2 M.\\ m1
-            ]
-    field_coercions <- sequence
-            [ do c <- memo t1 t2
-                 pure $ \vm -> case M.lookup fn vm of
-                    Nothing -> throwError $ show $ "Record value lacks field" <+> pretty fn <+> "of type" <+> pretty t1
-                    Just v -> (fn, ) <$> c v
-            | (fn, (t1, t2)) <- M.toList $ M.intersectionWith (,) m1 m2
-            ]
-    pure $ \case
-        TupV ts -> do
-            let vm = M.fromList $ zip [hashedField n | n <- [0..]] ts
-            coerced_fields <- mapM ($ vm) field_coercions
-            return $ RecV $ sortOn fst $ coerced_fields <> new_fields
-        RecV fvs -> do
-            let vm = M.fromList fvs
-            coerced_fields <- mapM ($ vm) field_coercions
-            return $ RecV $ sortOn fst $ coerced_fields <> new_fields
+go rv (RecT fs1) (RecT fs2) = do
+    vm <- case rv of
+        TupV ts -> pure $ M.fromList $ zip [hashedField n | n <- [0..]] ts
+        RecV fvs -> pure $ M.fromList fvs
         v -> throwError $ show $ "Unexpected value" <+> pretty v <+> "while coercing record"
 
+    let m1 = M.fromList fs1
+    fmap RecV $ forM fs2 $ \(fn, t2) -> (fn,) <$>
+      case (M.lookup fn vm, M.lookup fn m1) of
+        (Just v, Just t1) -> go v t1 t2
+        _ -> case unRef t2 of
+            OptT _ -> pure (OptV Nothing)
+            ReservedT -> pure ReservedV
+            t -> throwError $ show $ "Missing record field" <+> pretty fn <+> "of type" <+> pretty t
+
 -- Variants
-go (VariantT fs1) (VariantT fs2) = do
+go (VariantV fn v) (VariantT fs1) (VariantT fs2) = do
     let m1 = M.fromList fs1
     let m2 = M.fromList fs2
-    cm <- M.traverseWithKey (\fn t1 ->
-        case M.lookup fn m2 of
-            Just t2 -> memo t1 t2
-            Nothing -> throwError $ show $ "Missing variant field" <+> pretty fn <+> "of type" <+> pretty t1
-        ) m1
-    pure $ \case
-        VariantV fn v | Just c <- M.lookup fn cm -> VariantV fn <$> c v
-                      | otherwise -> throwError $ show $ "Unexpected variant field" <+> pretty fn
-        v -> throwError $ show $ "Unexpected value" <+> pretty v <+> "while coercing variant"
+    case (M.lookup fn m1, M.lookup fn m2) of
+      (Just t1, Just t2) -> VariantV fn <$> go v t1 t2
+      (Nothing, _) -> throwError $ show $ "Wrongly typed variant missing field " <+> pretty fn
+      (_, Nothing) -> throwError $ show $ "Unexpected variant field" <+> pretty fn
 
 -- Reference types
-go (FuncT mt1) (FuncT mt2) = goMethodType mt1 mt2 >> pure pure
-go (ServiceT meths1) (ServiceT meths2) = do
-    let m1 = M.fromList meths1
-    forM_ meths2 $ \(m, mt2) -> case M.lookup m m1 of
-        Just mt1 -> goMethodType mt1 mt2
-        Nothing -> throwError $ show $ "Missing service method" <+> pretty m <+> "of type" <+> pretty mt2
-    pure pure
+go v t1@(FuncT _) t2@(FuncT _) = isSubtypeOfM t1 t2 >> pure v
+go v t1@(ServiceT _) t2@(ServiceT _) = isSubtypeOfM t1 t2 >> pure v
 
 -- BlobT
-go BlobT BlobT = pure pure
-go (VecT t) BlobT | isNat8 t = pure $ \case
-    VecV vs ->  BlobV . BS.pack . V.toList <$> mapM goNat8 vs
-    v -> throwError $ show $ "Unexpected value" <+> pretty v <+> "while coercing vec nat8 to blob"
+go v BlobT BlobT = pure v
+go (VecV vs) (VecT t) BlobT | isNat8 t = BlobV . BS.pack . V.toList <$> mapM goNat8 vs
    where
     goNat8 (Nat8V n) = pure n
     goNat8 v = throwError $ show $ "Unexpected value" <+> pretty v <+> "while coercing vec nat8 to blob"
-go BlobT (VecT t) | isNat8 t = pure $ \case
-    BlobV b -> return $ VecV $ V.fromList $ map (Nat8V . fromIntegral) $ BS.unpack b
-    v -> throwError $ show $ "Unexpected value" <+> pretty v <+> "while coercing blob to vec nat8"
-
-go t1 t2 = throwError $ show $ "Type" <+> pretty t1 <+> "is not a subtype of" <+> pretty t2
+go (BlobV b) BlobT (VecT t) | isNat8 t = pure $ VecV $ V.fromList $ map (Nat8V . fromIntegral) $ BS.unpack b
 
-goMethodType ::
-    (Pretty k2, Pretty k1, Ord k2, Ord k1) =>
-    MethodType (Ref k1 Type) ->
-    MethodType (Ref k2 Type) ->
-    M k1 k2 ()
-goMethodType (MethodType ta1 tr1 q1 o1) (MethodType ta2 tr2 q2 o2) = do
-    unless (q1 == q2) $ throwError "Methods differ in query annotation"
-    unless (o1 == o2) $ throwError "Methods differ in oneway annotation"
-    void $ flipM $ goSeq ta2 ta1
-    void $ goSeq tr1 tr2
+go v t1 t2 = throwError $ show $ "Cannot coerce " <+> pretty v <+> ":" <+> pretty t1 <+> "to type " <+> pretty t2
 
-goSeq _ []  = pure (const (return []))
-goSeq ts1 (RefT (Ref _ t) : ts) = goSeq ts1 (t:ts)
-goSeq ts1@[] (NullT  : ts) = do
-    cs2 <- goSeq ts1 ts
-    pure $ \_vs -> (NullV :) <$> cs2 []
-goSeq ts1@[] (OptT _ : ts) = do
-    cs2 <- goSeq ts1 ts
-    pure $ \_vs -> (OptV Nothing :) <$> cs2 []
-goSeq ts1@[] (ReservedT : ts) = do
-    cs2 <- goSeq ts1 ts
-    pure $ \_vs -> (ReservedV :) <$> cs2 []
-goSeq [] ts =
-    throwError $ show $ "Argument type list too short, expecting types" <+> pretty ts
-goSeq (t1:ts1) (t2:ts2) = do
-    c1 <- memo t1 t2
-    cs2 <- goSeq ts1 ts2
-    pure $ \case
-        [] -> throwError $ show $ "Expecting value of type:" <+> pretty t1
-        (v:vs) -> do
-            v' <- c1 v
-            vs' <- cs2 vs
-            return (v':vs')
+goSeq _ _ []  = pure []
+goSeq vs ts1 (RefT (Ref _ t) : ts) = goSeq vs ts1 (t:ts)
+goSeq vs@[] ts1@[] (OptT _    : ts) = (OptV Nothing :) <$> goSeq vs ts1 ts
+goSeq vs@[] ts1@[] (ReservedT : ts) = (ReservedV :)    <$> goSeq vs ts1 ts
+goSeq [] [] ts = throwError $ show $ "Argument type list too short, expecting types" <+> pretty ts
+goSeq (v:vs) (t1:ts1) (t2:ts2) = do
+    v' <- go v t1 t2
+    vs' <- goSeq vs ts1 ts2
+    pure $ v' : vs'
+goSeq _ _ _ = throwError $ "Illtyped input to goSeq"
 
 unRef :: Type (Ref a Type) -> Type (Ref a Type)
 unRef (RefT (Ref _ t)) = unRef t
diff --git a/src/Codec/Candid/Decode.hs b/src/Codec/Candid/Decode.hs
--- a/src/Codec/Candid/Decode.hs
+++ b/src/Codec/Candid/Decode.hs
@@ -88,6 +88,12 @@
     PrincipalV <$> decodePrincipal
 
 decodeVal EmptyT = fail "Empty value"
+decodeVal FutureT = do
+    m <- getLEB128Int
+    _n <- getLEB128Int @Natural
+    _ <- G.getLazyByteString m
+    pure FutureV
+
 decodeVal (RefT v) = absurd v
 
 referenceByte :: G.Get ()
@@ -168,7 +174,9 @@
         unless (isOrdered (map fst m)) $
             fail "Service methods not in strict order"
         return (Right m)
-    _ -> fail "Unknown structural type"
+    _ -> do
+        _ <- getLEB128Int >>= G.getLazyByteString
+        return (Left FutureT)
 
 decodeTypRef :: Natural -> G.Get (Type Int)
 decodeTypRef max = do
diff --git a/src/Codec/Candid/Encode.hs b/src/Codec/Candid/Encode.hs
--- a/src/Codec/Candid/Encode.hs
+++ b/src/Codec/Candid/Encode.hs
@@ -185,6 +185,8 @@
 
       PrincipalT -> return $ -24
 
+      FutureT    -> error "Cannot encode a future type"
+
       -- Short-hands
       BlobT -> addCon t $
         -- blob = vec nat8
diff --git a/src/Codec/Candid/Infer.hs b/src/Codec/Candid/Infer.hs
--- a/src/Codec/Candid/Infer.hs
+++ b/src/Codec/Candid/Infer.hs
@@ -42,6 +42,7 @@
 inferTyp (FuncV _ _) = return (FuncT (MethodType [] [] False False)) -- no principal type
 inferTyp (ServiceV _) = return (ServiceT []) -- no principal type
 inferTyp (PrincipalV _) = return PrincipalT
+inferTyp FutureV = return FutureT
 inferTyp (BlobV _) = return BlobT
 inferTyp (AnnV _ t) = return t -- Maybe do type checking?
 
diff --git a/src/Codec/Candid/Parse.hs b/src/Codec/Candid/Parse.hs
--- a/src/Codec/Candid/Parse.hs
+++ b/src/Codec/Candid/Parse.hs
@@ -137,7 +137,7 @@
             _ -> fail $ "Invalid hex string " ++ show raw
 
 hexdigit :: Parser Char
-hexdigit = oneOf "0123456789ABCDEFabcdef"
+hexdigit = oneOf "0123456789ABCDEFabcdef" <|> char '_' *> hexdigit -- slightly too liberal: allows leading _
 
 seqP :: Parser [Type TypeName]
 seqP = parenComma argTypeP
diff --git a/src/Codec/Candid/Subtype.hs b/src/Codec/Candid/Subtype.hs
new file mode 100644
--- /dev/null
+++ b/src/Codec/Candid/Subtype.hs
@@ -0,0 +1,185 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE FlexibleContexts #-}
+module Codec.Candid.Subtype
+  ( isSubtypeOf
+  , SubTypeM
+  , runSubTypeM
+  , isSubtypeOfM
+  )
+  where
+
+import Prettyprinter
+import qualified Data.Map as M
+import Data.Bifunctor
+import Data.Tuple
+import Control.Monad.State.Lazy
+import Control.Monad.Except
+import Control.Monad.Trans.Except
+
+import Codec.Candid.Types
+import Codec.Candid.TypTable
+
+type Memo k1 k2 =
+    (M.Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()),
+     M.Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()))
+
+type SubTypeM k1 k2 = ExceptT String (State (Memo k1 k2))
+
+runSubTypeM :: (Ord k1, Ord k2) => SubTypeM k1 k2 a -> Either String a
+runSubTypeM act = evalState (runExceptT act) (mempty, mempty)
+
+-- | Returns 'Right' if the first argument is a subtype of the second, or
+-- returns 'Left' with an explanation if not
+isSubtypeOf ::
+    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
+    Type (Ref k1 Type) ->
+    Type (Ref k2 Type) ->
+    Either String ()
+isSubtypeOf t1 t2 = runSubTypeM $ isSubtypeOfM t1 t2
+
+isSubtypeOfM ::
+    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
+    Type (Ref k1 Type) ->
+    Type (Ref k2 Type) ->
+    SubTypeM k1 k2 ()
+isSubtypeOfM t1 t2 = memo t1 t2
+
+flipM :: SubTypeM k1 k2 a -> SubTypeM k2 k1 a
+flipM (ExceptT (StateT f)) = ExceptT (StateT f')
+  where
+    f' (m1,m2) = second swap <$> f (m2,m1) -- f (m2,m1) >>= \case (r, (m2',m1')) -> pure (r, (m1', m2'))
+
+memo, go ::
+    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
+    Type (Ref k1 Type) ->
+    Type (Ref k2 Type) ->
+    SubTypeM k1 k2 ()
+
+goSeq ::
+    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
+    [Type (Ref k1 Type)] ->
+    [Type (Ref k2 Type)] ->
+    SubTypeM k1 k2 ()
+
+-- Memoization: When we see a pair for the first time,
+-- we optimistically put 'True' into the map.
+-- Either the following recursive call will fail (but then this optimistic
+-- value wasn't a problem), or it will succeed, but then the guess was correct.
+-- If it fails we put 'False' into it, to as a caching optimization
+memo t1 t2 = do
+  gets (M.lookup (t1,t2) . fst) >>= \case
+    Just r -> except r
+    Nothing -> assume_ok >> (go t1 t2 `catchE` remember_failure)
+  where
+    remember r         = modify (first (M.insert (t1,t2) r))
+    assume_ok          = remember (Right ())
+    remember_failure e = remember (Left e) >> throwError e
+
+-- Look through refs
+go (RefT (Ref _ t1)) t2 = memo t1 t2
+go t1 (RefT (Ref _ t2)) = memo t1 t2
+
+-- Identity coercion for primitive values
+go NatT NatT = pure ()
+go Nat8T Nat8T = pure ()
+go Nat16T Nat16T = pure ()
+go Nat32T Nat32T = pure ()
+go Nat64T Nat64T = pure ()
+go IntT IntT = pure ()
+go Int8T Int8T = pure ()
+go Int16T Int16T = pure ()
+go Int32T Int32T = pure ()
+go Int64T Int64T = pure ()
+go Float32T Float32T = pure ()
+go Float64T Float64T = pure ()
+go BoolT BoolT = pure ()
+go TextT TextT = pure ()
+go NullT NullT = pure ()
+go PrincipalT PrincipalT = pure ()
+
+-- Nat <: Int
+go NatT IntT = pure ()
+
+-- t <: reserved
+go _ ReservedT = pure ()
+
+-- empty <: t
+go EmptyT _ = pure ()
+
+-- vec t1 <: vec t2
+go (VecT t1) (VecT t2) = memo t1 t2
+
+-- Option: very simple
+go _ (OptT _) = pure ()
+
+-- Records
+go (RecT fs1) (RecT fs2) = do
+    let m1 = M.fromList fs1
+    let m2 = M.fromList fs2
+    -- Check missing fields
+    sequence_
+      [ case unRef t of
+          OptT _ -> pure ()
+          ReservedT -> pure ()
+          t -> throwError $ show $ "Missing record field" <+> pretty fn <+> "of type" <+> pretty t
+      | (fn, t) <- M.toList $ m2 M.\\ m1
+      ]
+    -- Check existing fields
+    sequence_ [ memo t1 t2 | (_fn, (t1, t2)) <- M.toList $ M.intersectionWith (,) m1 m2 ]
+
+-- Variants
+go (VariantT fs1) (VariantT fs2) = do
+    let m1 = M.fromList fs1
+    let m2 = M.fromList fs2
+    sequence_
+      [ case M.lookup fn m2 of
+            Just t2 -> memo t1 t2
+            Nothing -> throwError $ show $ "Missing variant field" <+> pretty fn <+> "of type" <+> pretty t1
+      | (fn, t1) <- M.toList m1
+      ]
+
+-- Reference types
+go (FuncT mt1) (FuncT mt2) = goMethodType mt1 mt2
+go (ServiceT meths1) (ServiceT meths2) = do
+    let m1 = M.fromList meths1
+    forM_ meths2 $ \(m, mt2) -> case M.lookup m m1 of
+        Just mt1 -> goMethodType mt1 mt2
+        Nothing -> throwError $ show $ "Missing service method" <+> pretty m <+> "of type" <+> pretty mt2
+
+-- BlobT
+go BlobT BlobT = pure ()
+go (VecT t) BlobT | isNat8 t = pure ()
+go BlobT (VecT t) | isNat8 t = pure ()
+
+-- Final catch-all
+go t1 t2 = throwError $ show $ "Type" <+> pretty t1 <+> "is not a subtype of" <+> pretty t2
+
+goMethodType ::
+    (Pretty k2, Pretty k1, Ord k2, Ord k1) =>
+    MethodType (Ref k1 Type) ->
+    MethodType (Ref k2 Type) ->
+    SubTypeM k1 k2 ()
+goMethodType (MethodType ta1 tr1 q1 o1) (MethodType ta2 tr2 q2 o2) = do
+    unless (q1 == q2) $ throwError "Methods differ in query annotation"
+    unless (o1 == o2) $ throwError "Methods differ in oneway annotation"
+    flipM $ goSeq ta2 ta1
+    goSeq tr1 tr2
+
+goSeq _ []  = pure ()
+goSeq ts1 (RefT (Ref _ t) : ts) = goSeq ts1 (t:ts)
+-- Missing optional arguments are ok
+goSeq ts1@[] (OptT _ : ts) = goSeq ts1 ts
+goSeq ts1@[] (ReservedT : ts) = goSeq ts1 ts
+goSeq [] ts = throwError $ show $ "Argument type list too short, expecting types" <+> pretty ts
+goSeq (t1:ts1) (t2:ts2) = memo t1 t2 >> goSeq ts1 ts2
+
+unRef :: Type (Ref a Type) -> Type (Ref a Type)
+unRef (RefT (Ref _ t)) = unRef t
+unRef t = t
+
+isNat8 :: Type (Ref a Type) -> Bool
+isNat8 (RefT (Ref _ t)) = isNat8 t
+isNat8 Nat8T = True
+isNat8 _ = False
diff --git a/src/Codec/Candid/TH.hs b/src/Codec/Candid/TH.hs
--- a/src/Codec/Candid/TH.hs
+++ b/src/Codec/Candid/TH.hs
@@ -49,7 +49,7 @@
 candidFile :: QuasiQuoter
 candidFile = quoteFile candid
 
--- | This quasi-quoter turns all type definitions of a Canddi file into Haskell types, as one 'Row'. The `service` of the candid file is ignored.
+-- | This quasi-quoter turns all type definitions of a Canddi file into Haskell types, as one 'Row'. The @service@ of the candid file is ignored.
 --
 -- Recursive types are not supported.
 -- 
@@ -89,10 +89,10 @@
 
 -- | Turns all candid type definitions into newtypes
 -- Used, so far, only in the Candid test suite runner
-generateCandidDefs :: [DidDef TypeName] -> Q ([Dec], TypeName -> Q TH.Name)
-generateCandidDefs defs = do
+generateCandidDefs :: T.Text -> [DidDef TypeName] -> Q ([Dec], TypeName -> Q TH.Name)
+generateCandidDefs prefix defs = do
     assocs <- for defs $ \(tn, _) -> do
-        thn <- newName ("Candid_" ++ T.unpack tn)
+        thn <- newName ("Candid_" ++ T.unpack prefix ++ T.unpack tn)
         return (tn, thn)
 
     let m = M.fromList assocs
@@ -102,7 +102,7 @@
     decls <- for defs $ \(tn, t) -> do
           t' <- traverse resolve t
           n <- resolve tn
-          dn <- newName ("Candid_" ++ T.unpack tn)
+          dn <- newName ("Candid_" ++ T.unpack prefix ++ T.unpack tn)
           newtypeD (cxt []) n [] Nothing
             (normalC dn [bangType (bang noSourceUnpackedness noSourceStrictness) (typ t')])
             [derivClause Nothing [conT ''Candid, conT ''Eq, conT ''Show]]
@@ -233,6 +233,7 @@
 typ (VariantT fs) = [t| V.Var $(row [t| (V..==) |] [t| (V..+) |] [t| V.Empty |] fs) |]
 typ (FuncT mt) = [t| FuncRef $(methodType mt) |]
 typ (ServiceT ms) = [t| ServiceRef $(mrow [t| (R..==) |] [t| (R..+) |] [t| R.Empty |] ms) |]
+typ FutureT = fail "Cannot represent a future Candid type as a Haskell type"
 typ (RefT v) = conT v
 
 isTuple :: [(FieldName, b)] -> Bool
diff --git a/src/Codec/Candid/TestExports.hs b/src/Codec/Candid/TestExports.hs
--- a/src/Codec/Candid/TestExports.hs
+++ b/src/Codec/Candid/TestExports.hs
@@ -4,6 +4,8 @@
     ( module Codec.Candid.Parse
     , module Codec.Candid.TH
     , module Codec.Candid.FieldName
+    , module Codec.Candid.TypTable
+    , module Codec.Candid.Class
     ) where
 
 import Codec.Candid.Parse
@@ -23,4 +25,12 @@
 
 import Codec.Candid.FieldName
   ( invertHash
+  )
+
+import Codec.Candid.TypTable
+  ( unrollTypeTable
+  )
+
+import Codec.Candid.Class
+  ( typeGraph
   )
diff --git a/src/Codec/Candid/TypTable.hs b/src/Codec/Candid/TypTable.hs
--- a/src/Codec/Candid/TypTable.hs
+++ b/src/Codec/Candid/TypTable.hs
@@ -81,7 +81,8 @@
 
 -- | This takes a type description and replaces all named types with their definition.
 --
--- This produces an infinite type! Only use this in sufficiently lazy contexts.
+-- This can produce an infinite type! Only use this in sufficiently lazy contexts, or when the
+-- type is known to be not recursive.
 tieKnot :: SeqDesc -> [Type Void]
 tieKnot (SeqDesc m (ts :: [Type k])) = ts'
   where
diff --git a/src/Codec/Candid/Types.hs b/src/Codec/Candid/Types.hs
--- a/src/Codec/Candid/Types.hs
+++ b/src/Codec/Candid/Types.hs
@@ -42,6 +42,8 @@
     -- short-hands
     | BlobT
       -- ^ a short-hand for 'VecT' 'Nat8T'
+    -- future types
+    | FutureT
     -- for recursive types
     | RefT a -- ^ A reference to a named type
   deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
@@ -73,6 +75,7 @@
     ReservedT >>= _ = ReservedT
     EmptyT >>= _ = EmptyT
     BlobT >>= _ = BlobT
+    FutureT >>= _ = FutureT
     PrincipalT >>= _ = PrincipalT
     OptT t >>= f = OptT (t >>= f)
     VecT t >>= f = VecT (t >>= f)
@@ -119,6 +122,7 @@
     pretty (ServiceT s) =
         "service" <+> ":" <+> braces (group (align (vsep $ prettyMeth <$> s)))
     pretty PrincipalT = "principal"
+    pretty FutureT = "future"
 
     prettyList = encloseSep lparen rparen (comma <> space) . map pretty
 
@@ -160,6 +164,7 @@
   | PrincipalV Principal
   | BlobV BS.ByteString
   | AnnV Value (Type Void)
+  | FutureV -- ^ An opaque value of a future type
   deriving (Eq, Ord, Show)
 
 instance Pretty Value where
@@ -195,6 +200,7 @@
   pretty (VariantV f NullV) = "variant" <+> braces (pretty f)
   pretty (VariantV f v) = "variant" <+> braces (pretty f <+> "=" <+> pretty v)
   pretty (AnnV v t) = prettyAnn v t
+  pretty FutureV = "future"
 
   prettyList = encloseSep lparen rparen (comma <> space) . map pretty
 
diff --git a/test/SpecTests.hs b/test/SpecTests.hs
--- a/test/SpecTests.hs
+++ b/test/SpecTests.hs
@@ -48,13 +48,12 @@
           | basename <- files
           , let file = dir </> basename
           , Just name <- pure $ T.stripSuffix ".test.did" (T.pack basename)
-          -- , name /= "construct" -- for now
           ]
   (decls, testGroups) <- fmap unzip $ for candid_tests $ \(name, testfile) -> do
-     (decls, resolve) <- generateCandidDefs (testDefs testfile)
+     (decls, resolve) <- generateCandidDefs name (testDefs testfile)
      tests <- traverse (traverse resolve) (testTests testfile)
      testGroup <-
-        [| testGroup ("File " ++ $(liftString (T.unpack name))) $(listE
+        [| testGroup ("Candid spec test file " ++ $(liftString (T.unpack name))) $(listE
           [ [| testCase name $( case testAssertion of
             CanParse i1 -> [|
                 case $(parseInput i1) of
@@ -98,3 +97,7 @@
        |]) []
   return $ concat decls ++ [d1, d2]
  )
+
+
+
+
diff --git a/test/Tests.hs b/test/Tests.hs
new file mode 100644
--- /dev/null
+++ b/test/Tests.hs
@@ -0,0 +1,454 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedLabels #-}
+
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Tests (tests) where
+
+import qualified Data.Text as T
+import qualified Data.ByteString.Lazy as BS
+import qualified Data.ByteString.Lazy.Char8 as B
+import qualified Data.Vector as V hiding (singleton)
+import Test.Tasty
+import Test.Tasty.HUnit
+import Test.Tasty.SmallCheck
+import qualified Test.Tasty.QuickCheck as QC
+import Test.SmallCheck.Series
+import Data.Void
+import Data.Either
+import GHC.Int
+import GHC.Word
+import Numeric.Natural
+import GHC.Generics (Generic)
+import Prettyprinter
+import Data.Row
+import Data.Proxy
+import qualified Data.Row.Records as R
+import qualified Data.Row.Variants as V
+
+import Codec.Candid
+import Codec.Candid.TestExports
+
+newtype Peano = Peano (Maybe Peano)
+    deriving (Show, Eq)
+    deriving Candid via (Maybe Peano)
+
+peano :: Peano
+peano = Peano $ Just $ Peano $ Just $ Peano $ Just $ Peano Nothing
+
+newtype LinkedList a = LinkedList (Maybe (a, LinkedList a))
+    deriving (Show, Eq)
+    deriving newtype Candid
+
+cons :: a -> LinkedList a -> LinkedList a
+cons x y = LinkedList $ Just (x, y)
+nil :: LinkedList a
+nil = LinkedList Nothing
+
+natList :: LinkedList Natural
+natList = cons 1 (cons 2 (cons 3 (cons 4 nil)))
+
+stringList :: [T.Text]
+stringList = [T.pack "HI", T.pack "Ho"]
+
+newtype ARecord a = ARecord { foo :: a }
+    deriving (Eq, Show, Generic)
+    deriving anyclass (Serial m)
+
+deriving via (AsRecord (ARecord a))
+    instance Candid a => Candid (ARecord a)
+
+data EmptyRecord = EmptyRecord
+    deriving (Eq, Show, Generic, Serial m)
+    deriving Candid via (AsRecord EmptyRecord)
+
+newtype MiddleField a = MiddleField a
+    deriving (Eq, Show)
+
+instance Candid a => Candid (MiddleField a) where
+    type AsCandid (MiddleField a) = Rec ("_1_" .== a)
+    toCandid (MiddleField x) = #_1_ .== x
+    fromCandid r = MiddleField (r .! #_1_)
+
+newtype JustRight a = JustRight a
+    deriving (Eq, Show)
+
+instance Candid a => Candid (JustRight a) where
+    type AsCandid (JustRight a) = Var ("Right" .== a)
+    toCandid (JustRight x) = V.singleton (Label @"Right") x
+    fromCandid = JustRight . snd . V.unSingleton
+
+data SimpleRecord = SimpleRecord { foo :: Bool, bar :: Word8 }
+    deriving (Generic, Eq, Show)
+    deriving (Serial m)
+    deriving Candid via (AsRecord SimpleRecord)
+
+roundTripTest :: forall a. (CandidArg a, Eq a, Show a) => a -> Assertion
+roundTripTest v1 = do
+  let bytes1 = encode v1
+  v2 <- case decode @a bytes1 of
+    Left err -> assertFailure err
+    Right v -> return v
+  assertEqual "values" v1 v2
+
+subTypeRoundTripProp :: forall a b.  (CandidArg a, Serial IO a, Show a, CandidArg b) => TestTree
+subTypeRoundTripProp = testProperty desc $ \v ->
+    isRight $ decode @b (encode @a v)
+  where
+    desc = show $ pretty (tieKnot (seqDesc @a)) <+> "<:" <+> pretty (tieKnot (seqDesc @b))
+
+subTypeRoundTripTest' :: forall a b.
+    (CandidArg a, Eq a, Show a) =>
+    (CandidArg b, Eq b, Show b) =>
+    a -> b -> Assertion
+subTypeRoundTripTest' v1 v2 = do
+  let bytes1 = encode v1
+  v2' <- case decode @b bytes1 of
+    Left err -> assertFailure err
+    Right v -> return v
+  v2 @=? v2'
+
+subTypeRoundTripTest :: forall a b.
+    (CandidArg a, Eq a, Show a) =>
+    (CandidArg b, Eq b, Show b) =>
+    a -> b -> Assertion
+subTypeRoundTripTest v1 v2 = do
+  subTypeRoundTripTest' v1 v2
+  -- now try the other direction
+  let bytes2 = encode v2
+  case decode @a bytes2 of
+    Left _err -> return ()
+    Right _ -> assertFailure "converse subtype test succeeded"
+
+instance Monad m => Serial m T.Text where
+    series = T.pack <$> series
+
+instance (Monad m, Serial m a) => Serial m (V.Vector a) where
+    series = V.fromList <$> series
+
+parseTest :: HasCallStack => String -> DidFile -> TestTree
+parseTest c e = testCase c $
+    case parseDid c of
+        Left err -> assertFailure err
+        Right s -> s @?= e
+
+printTestType :: forall a. (Candid a, HasCallStack) => String -> TestTree
+printTestType e = testCase e $
+    show (pretty (typeDesc @a)) @?= e
+
+printTestSeq :: forall a. (CandidArg a, HasCallStack) => String -> TestTree
+printTestSeq e = testCase e $
+    show (pretty (tieKnot (seqDesc @a))) @?= e
+
+roundTripTestGroup :: String ->
+    (forall a. (CandidArg a, Serial IO a, Show a, Eq a) => a -> Either String a) ->
+    TestTree
+roundTripTestGroup group_desc roundtrip =
+    testGroup ("roundtrip (" <> group_desc <> ")") $ withSomeTypes $ \(Proxy :: Proxy a) ->
+        let desc = show $ pretty (tieKnot (seqDesc @a)) in
+        testProperty desc $ \v ->
+            case roundtrip @a v of
+                Right y | y == v -> Right ("all good" :: String)
+                Right y -> Left $
+                    show v ++ " round-tripped to " ++ show y
+                Left err -> Left $
+                    show v ++ " failed to decode:\n" ++ err
+
+withSomeTypes ::
+    (forall a. (CandidArg a, Serial IO a, Show a, Eq a) => Proxy a -> b) -> [b]
+withSomeTypes mkTest =
+    [ mkTest (Proxy @Bool)
+    , mkTest (Proxy @Natural)
+    , mkTest (Proxy @Word8)
+    , mkTest (Proxy @Word16)
+    , mkTest (Proxy @Word32)
+    , mkTest (Proxy @Word64)
+    , mkTest (Proxy @Integer)
+    , mkTest (Proxy @Int8)
+    , mkTest (Proxy @Int16)
+    , mkTest (Proxy @Int32)
+    , mkTest (Proxy @Int64)
+    , mkTest (Proxy @Float)
+    , mkTest (Proxy @Double)
+    , mkTest (Proxy @T.Text)
+    , mkTest (Proxy @())
+    , mkTest (Proxy @Reserved)
+    , mkTest (Proxy @Principal)
+    , mkTest (Proxy @BS.ByteString)
+    , mkTest (Proxy @(Maybe T.Text))
+    , mkTest (Proxy @(V.Vector T.Text))
+    , mkTest (Proxy @EmptyRecord)
+    , mkTest (Proxy @(ARecord T.Text))
+    , mkTest (Proxy @(Either Bool T.Text))
+    , mkTest (Proxy @SimpleRecord)
+    , mkTest (Proxy @(Rec ("a" .== Bool .+ "b" .== Bool .+ "c" .== Bool)))
+    , mkTest (Proxy @(V.Var ("upgrade" .== () .+ "reinstall" .== () .+ "install" .== ())))
+    , mkTest (Proxy @(FuncRef (Bool, T.Text, AnnFalse, AnnFalse)))
+    , mkTest (Proxy @(FuncRef (Bool, T.Text, AnnTrue, AnnFalse)))
+    , mkTest (Proxy @(FuncRef (Bool, T.Text, AnnFalse, AnnTrue)))
+    , mkTest (Proxy @(ServiceRef Empty))
+    ]
+
+tests :: [TestTree]
+tests =
+  [ testGroup "encode tests"
+    [ testCase "empty" $ encode () @?= B.pack "DIDL\0\0"
+    , testCase "bool" $ encode (Unary True) @?= B.pack "DIDL\0\1\x7e\1"
+    ]
+  , testGroup "decode error message"
+      [ testCase "simple mismatch" $ fromCandidVals @(Unary ()) (toCandidVals True) @?= Left "Cannot coerce true into null"
+      , testCase "missing variant" $ fromCandidVals @(Either () ()) (toCandidVals (V.singleton #foo ())) @?= Left "Unexpected tag foo"
+      , testCase "error in variant" $ fromCandidVals @(Either () ()) (toCandidVals (Left @Bool @() True)) @?= Left "Cannot coerce true into null"
+      ]
+  , testGroup "roundtrip"
+    [ testCase "empty" $ roundTripTest ()
+    , testCase "bool" $ roundTripTest $ Unary True
+    , testCase "simple record 1" $ roundTripTest (ARecord True, False)
+    , testCase "simple record 2" $ roundTripTest (ARecord (100000 :: Natural), False)
+    , testCase "simple variant 1" $ roundTripTest $ Unary (Left True :: Either Bool Bool)
+    , testCase "simple variant 2" $ roundTripTest $ Unary (Right False :: Either Bool Bool)
+    , testCase "nested record 2" $ roundTripTest (ARecord (True,False), False)
+    , testCase "peano" $ roundTripTest $ Unary peano
+    , testCase "lists" $ roundTripTest (natList, stringList)
+    , testCase "custom record" $ roundTripTest $ Unary (SimpleRecord True 42)
+    ]
+  , testGroup "subtype roundtrips"
+    [ testCase "nat/int" $ subTypeRoundTripTest (Unary (42 :: Natural)) (Unary (42 :: Integer))
+    , testCase "null/opt" $ subTypeRoundTripTest (Unary ()) (Unary (Nothing @Integer))
+    , testCase "rec" $ subTypeRoundTripTest (ARecord True, True) (EmptyRecord, True)
+    , testCase "tuple" $ subTypeRoundTripTest ((42::Integer,-42::Integer), 100::Integer) (EmptyRecord, 100::Integer)
+    , testCase "variant" $ subTypeRoundTripTest' (JustRight (42 :: Natural), True) (Right 42 :: Either Bool Natural, True)
+    , testCase "rec/any" $ subTypeRoundTripTest (ARecord True, True) (Reserved, True)
+    , testCase "tuple/any" $ subTypeRoundTripTest ((42::Integer, 42::Natural), True) (Reserved, True)
+    , testCase "tuple/tuple" $ subTypeRoundTripTest ((42::Integer,-42::Integer,True), 100::Integer) ((42::Integer, -42::Integer), 100::Integer)
+    , testCase "tuple/middle" $ subTypeRoundTripTest ((42::Integer,-42::Integer,True), 100::Integer) (MiddleField (-42) :: MiddleField Integer, 100::Integer)
+    , testCase "records" $ subTypeRoundTripTest (Unary (SimpleRecord True 42)) (Unary (ARecord True))
+    ]
+
+  , roundTripTestGroup "Haskell → Candid → Haskell" $ \(v :: a) ->
+        decode @a (encode @a v)
+  , roundTripTestGroup "Haskell → [Value] → Haskell" $ \(v :: a) ->
+        fromCandidVals (toCandidVals @a v)
+  , roundTripTestGroup "Haskell → [Value] → Textual → [Value] → Haskell" $ \(v :: a) ->
+        parseValues (show (pretty (toCandidVals @a v))) >>= fromCandidVals @a
+
+  , testGroup "subtype round trip smallchecks"
+    [ subTypeRoundTripProp @Natural @Natural
+    , subTypeRoundTripProp @(Rec ("Hi" .== Word8 .+ "_1_" .== Word8)) @Reserved
+    , subTypeRoundTripProp @(Rec ("Hi" .== Word8 .+ "_1_" .== Word8)) @(Rec ("Hi" .== Reserved))
+    , subTypeRoundTripProp @(Rec ("Hi" .== Word8 .+ "_1_" .== Word8)) @(Rec ("Hi" .== Word8))
+    , subTypeRoundTripProp @(Rec ("Hi" .== Word8 .+ "_1_" .== Word8)) @(Rec ("_1_" .== Word8))
+    , subTypeRoundTripProp @(Rec ("Hi" .== Word8 .+ "_1_" .== Word8 .+ "_2_" .== Bool)) @(Rec ("_1_" .== Word8))
+    , subTypeRoundTripProp @(Maybe (Rec ("Hi" .== Word8 .+ "_1_" .== Word8 .+ "_0_" .== Bool))) @(Maybe (Bool,Word8))
+    , subTypeRoundTripProp @(Var ("Hi" .== Word8)) @(Var ("Hi" .== Word8 .+ "Ho" .== T.Text))
+    , subTypeRoundTripProp @(Var ("Ho" .== T.Text)) @(Var ("Hi" .== Word8 .+ "Ho" .== T.Text))
+    , subTypeRoundTripProp @Natural @Reserved
+    , subTypeRoundTripProp @BS.ByteString @Reserved
+    , subTypeRoundTripProp @BS.ByteString @(V.Vector Word8)
+    , subTypeRoundTripProp @(V.Vector Word8) @BS.ByteString
+    , subTypeRoundTripProp @Principal @Reserved
+    ]
+
+  , testGroup "subtype test" $
+    [ testGroup "reflexivity" $ concat $ withSomeTypes $ \(Proxy :: Proxy a) ->
+        let td = seqDesc @a in
+        unrollTypeTable td $ \ts ->
+           [ testCase (show (pretty t)) $ assertRight $ t `isSubtypeOf` t | t <- ts ]
+    , testGroup "negative tests"
+      [ let t1 = typeGraph @Integer
+            t2 = typeGraph @Natural
+        in testCase (show (pretty t1) ++ " </: " ++ show (pretty t2)) $
+           assertLeft $ t1 `isSubtypeOf` t2
+      ]
+    ]
+  , testGroup "candid type printing" $
+    [ printTestType @Bool "bool"
+    , printTestType @Integer "int"
+    , printTestType @Natural "nat"
+    , printTestType @Int8 "int8"
+    , printTestType @Word8 "nat8"
+    , printTestType @SimpleRecord "record {bar : nat8; foo : bool}"
+    , printTestType @(JustRight T.Text) "variant {Right : text}"
+    , printTestType @(FuncRef (Bool, Unary (), AnnTrue, AnnFalse)) "func (bool) -> (null) query"
+    , printTestType @(FuncRef (Bool, T.Text, AnnFalse, AnnTrue)) "func (bool) -> (text) oneway"
+    , printTestType @(ServiceRef Empty) "service : {}"
+    , printTestType @(ServiceRef ("foo" .== (Bool, T.Text, AnnFalse, AnnTrue) .+ "bar" .== ((),(),AnnFalse, AnnFalse)))
+        "service : {bar : () -> (); foo : (bool) -> (text) oneway;}"
+    , printTestSeq @() "()"
+    , printTestSeq @(Unary ()) "(null)"
+    , printTestSeq @(Unary (Bool, Bool)) "(record {0 : bool; 1 : bool})"
+    , printTestSeq @((),()) "(null, null)"
+    , printTestSeq @(Bool,Bool) "(bool, bool)"
+    , printTestSeq @(Bool,(Bool, Bool)) "(bool, record {0 : bool; 1 : bool})"
+    , printTestSeq @Bool "(bool)"
+    ]
+  , testGroup "candid value printing" $
+    let t :: Value -> String -> TestTree
+        t v e = testCase e $ show (pretty v) @?= e
+    in
+    [ t (BoolV True) "true"
+    , t (BoolV False) "false"
+    , t (NatV 1) "1"
+    , t (IntV 1) "+1"
+    , t (IntV 0) "+0"
+    , t (IntV (-1)) "-1"
+    , t (Nat8V 1) "(1 : nat8)"
+    , t (RecV [("bar", TextV "baz")]) "record {bar = \"baz\"}"
+    , t (FuncV (Principal "\xde\xad\xbe\xef") "foo") "func \"psokg-ww6vw-7o6\".\"foo\""
+    , t (ServiceV (Principal "\xde\xad\xbe\xef")) "service \"psokg-ww6vw-7o6\""
+    , t (PrincipalV (Principal "")) "principal \"aaaaa-aa\""
+    , t (PrincipalV (Principal "\xab\xcd\x01")) "principal \"em77e-bvlzu-aq\""
+    , t (PrincipalV (Principal "\xde\xad\xbe\xef")) "principal \"psokg-ww6vw-7o6\""
+    ]
+  , testGroup "candid value printing (via binary) " $
+    let t :: forall a. (HasCallStack, CandidArg a) => a -> String -> TestTree
+        t v e = testCase e $ do
+          let bytes = encode v
+          (_, vs) <- assertRight $ decodeVals bytes
+          show (pretty vs) @?= e
+    in
+    [ t True "(true)"
+    , t (SimpleRecord False 42) "(record {bar = (42 : nat8); foo = false})"
+    , t (JustRight (Just (3 :: Natural))) "(variant {Right = opt 3})"
+    , t (JustRight (3 :: Word8)) "(variant {Right = (3 : nat8)})"
+    , t () "()"
+    , t (Unary ()) "(null)"
+    , t (Unary (True, False)) "(record {true; false})"
+    , t (Unary (True, (True, False))) "(record {true; record {true; false}})"
+    , t (#_0_ .== True .+ #_1_ .== False) "(record {true; false})"
+    ]
+
+  , testGroup "dynamic values (AST)" $
+    let t :: forall a. (HasCallStack, CandidArg a, Eq a, Show a) => String -> a -> TestTree
+        t s e = testCase s $ do
+          bytes <- either assertFailure return $ encodeTextual s
+          x <- either assertFailure return $ decode @a bytes
+          x @?= e
+
+        t' :: HasCallStack => String -> TestTree
+        t' s = testCase ("Bad: " <> s) $ do
+          vs <- either assertFailure return $ parseValues s
+          case encodeDynValues vs of
+            Left _err -> return ()
+            Right _ -> assertFailure "Ill-typed value encoded?"
+    in
+    [ t "true" True
+    , t "false" False
+    , t "1" (1 :: Natural)
+    , t "1 : nat8" (1 :: Word8)
+    , t "record { bar = \"baz\" }" (#bar .== ("baz":: T.Text))
+    , t "vec {}" (V.fromList [] :: V.Vector Void)
+    , t "vec {4; +4}" (V.fromList [4 :: Integer,4])
+    , t "vec {4; null : reserved}" (V.fromList [Reserved, Reserved])
+    , t "vec {record {}; record {0 = true}}" (V.fromList [R.empty, R.empty])
+    , t "vec {variant {a = true}; variant {b = null}}"
+        (V.fromList [IsJust #a True, IsJust #b () :: V.Var ("a" V..== Bool V..+ "b" V..== ())])
+    , t "\"hello\"" ("hello" :: T.Text)
+    , t "blob \"hello\"" ("hello" :: BS.ByteString)
+    , t "blob \"\\00\\ff\"" ("\x00\xff" :: BS.ByteString)
+    , t "func \"psokg-ww6vw-7o6\".\"foo\""
+        (FuncRef @((), (), AnnFalse, AnnFalse) (Principal "\xde\xad\xbe\xef") "foo")
+    , t "func \"psokg-ww6vw-7o6\".foo"
+        (FuncRef @((), (), AnnFalse, AnnFalse) (Principal "\xde\xad\xbe\xef") "foo")
+    , t "func \"psokg-ww6vw-7o6\".\"\""
+        (FuncRef @((), (), AnnFalse, AnnFalse) (Principal "\xde\xad\xbe\xef") "")
+    , t "service \"psokg-ww6vw-7o6\""
+        (ServiceRef @Empty (Principal "\xde\xad\xbe\xef"))
+    , t "principal \"psokg-ww6vw-7o6\""
+        (Principal "\xde\xad\xbe\xef")
+
+    , t' "vec {true; 4}"
+    ]
+
+  , testGroup "candid type parsing"
+    [ parseTest "service : {}" $
+      DidFile [] []
+    , parseTest "service : { foo : (text) -> (text) }" $
+      DidFile [] [("foo", MethodType [TextT] [TextT] False False)]
+    , parseTest "service : { foo : (text,) -> (text,); }" $
+      DidFile [] [("foo", MethodType [TextT] [TextT] False False)]
+    , parseTest "service : { foo : (x : text,) -> (y : text,); }" $
+      DidFile [] [("foo", MethodType [TextT] [TextT] False False)]
+    , parseTest "service : { foo : (opt text) -> () }" $
+      DidFile [] [("foo", MethodType [OptT TextT] [] False False) ]
+    , parseTest "service : { foo : (record { text; blob }) -> () }" $
+      DidFile [] [("foo", MethodType [RecT [(hashedField 0, TextT), (hashedField 1, BlobT)]] [] False False) ]
+    , parseTest "service : { foo : (record { x_ : null; 5 : nat8 }) -> () }" $
+      DidFile [] [("foo", MethodType [RecT [("x_", NullT), (hashedField 5, Nat8T)]] [] False False) ]
+    , parseTest "service : { foo : (record { x : null; 5 : nat8 }) -> () }" $
+      DidFile [] [("foo", MethodType [RecT [("x", NullT), (hashedField 5, Nat8T)]] [] False False) ]
+    , parseTest "service : { foo : (text) -> (text) query }" $
+      DidFile [] [("foo", MethodType [TextT] [TextT] True False)]
+    , parseTest "service : { foo : (text) -> (text) oneway }" $
+      DidFile [] [("foo", MethodType [TextT] [TextT] False True)]
+    , parseTest "service : { foo : (text) -> (text) query oneway }" $
+      DidFile [] [("foo", MethodType [TextT] [TextT] True True)]
+    , parseTest "service : { foo : (text) -> (text) oneway query }" $
+      DidFile [] [("foo", MethodType [TextT] [TextT] True True)]
+    , parseTest "service : (opt SomeInit) -> { foo : (text) -> (text) oneway query }" $
+      DidFile [] [("foo", MethodType [TextT] [TextT] True True)]
+    , parseTest "type t = int; service : { foo : (t) -> (t) }" $
+      DidFile [("t", IntT)] [("foo", MethodType [RefT "t"] [RefT "t"] False False)]
+    ]
+  , testProperty "field name escaping round-tripping" $ \e ->
+      let f = either labledField hashedField e in
+      let f' = unescapeFieldName (escapeFieldName f) in
+      f' == f
+  , testGroup "candid hash inversion"
+    [ QC.testProperty "long dictionary name" $
+        let s = "precriticized" in
+        invertHash (candidHash s) QC.=== Just s
+    , QC.testProperty "long capitalized dictionary name" $
+        let s = "Precriticized" in
+        invertHash (candidHash s) QC.=== Just s
+    , QC.testProperty "all hashes find something" $
+        QC.forAll QC.arbitraryBoundedIntegral $ \w ->
+        w >= 32 QC.==> case invertHash w of
+            Nothing -> False
+            Just s -> candidHash s == w
+    ]
+  ]
+
+assertRight :: Either String a -> IO a
+assertRight = either assertFailure pure
+
+assertLeft :: Either String () -> Assertion
+assertLeft = either (const (pure ())) (\() -> assertFailure "unexpected success")
+
+instance Monad m => Serial m BS.ByteString where
+    series = BS.pack <$> series
+
+instance Monad m => Serial m Principal where
+    series = Principal <$> series
+
+instance Monad m => Serial m Reserved where
+    series = Reserved <$ series @m @()
+
+instance Monad m => Serial m (FuncRef mt) where
+    series = FuncRef <$> series <*> series
+
+instance Monad m => Serial m (ServiceRef r) where
+    series = ServiceRef <$> series
+
+instance (Monad m, Forall r (Serial m), AllUniqueLabels r) => Serial m (Rec r) where
+    series = R.fromLabelsA @(Serial m) (\_l -> series)
+
+instance (Monad m, Forall r (Serial m), AllUniqueLabels r) => Serial m (Var r) where
+    series = V.fromLabels @(Serial m) (\_l -> series)
diff --git a/test/test.hs b/test/test.hs
--- a/test/test.hs
+++ b/test/test.hs
@@ -1,445 +1,10 @@
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE DeriveGeneric #-}
-{-# LANGUAGE DerivingVia #-}
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE DuplicateRecordFields #-}
-{-# LANGUAGE OverloadedLabels #-}
-
-{-# OPTIONS_GHC -Wno-orphans #-}
-
-import qualified Data.Text as T
-import qualified Data.ByteString.Lazy as BS
-import qualified Data.ByteString.Lazy.Char8 as B
-import qualified Data.Vector as V hiding (singleton)
 import Test.Tasty
 import Test.Tasty.Ingredients.Rerun
-import Test.Tasty.HUnit
-import Test.Tasty.SmallCheck
-import qualified Test.Tasty.QuickCheck as QC
-import Test.SmallCheck.Series
-import Data.Void
-import Data.Either
-import GHC.Int
-import GHC.Word
-import Numeric.Natural
-import GHC.Generics (Generic)
-import Prettyprinter
-import Data.Row
-import Data.Proxy
-import qualified Data.Row.Records as R
-import qualified Data.Row.Variants as V
 
-import Codec.Candid
-import Codec.Candid.TestExports
-
 import THTests (thTests)
 import SpecTests (specTests)
+import Tests (tests)
 
 main :: IO ()
-main = defaultMainWithRerun tests
-
-newtype Peano = Peano (Maybe Peano)
-    deriving (Show, Eq)
-    deriving Candid via (Maybe Peano)
-
-peano :: Peano
-peano = Peano $ Just $ Peano $ Just $ Peano $ Just $ Peano Nothing
-
-newtype LinkedList a = LinkedList (Maybe (a, LinkedList a))
-    deriving (Show, Eq)
-    deriving newtype Candid
-
-cons :: a -> LinkedList a -> LinkedList a
-cons x y = LinkedList $ Just (x, y)
-nil :: LinkedList a
-nil = LinkedList Nothing
-
-natList :: LinkedList Natural
-natList = cons 1 (cons 2 (cons 3 (cons 4 nil)))
-
-stringList :: [T.Text]
-stringList = [T.pack "HI", T.pack "Ho"]
-
-newtype ARecord a = ARecord { foo :: a }
-    deriving (Eq, Show, Generic)
-    deriving anyclass (Serial m)
-
-deriving via (AsRecord (ARecord a))
-    instance Candid a => Candid (ARecord a)
-
-data EmptyRecord = EmptyRecord
-    deriving (Eq, Show, Generic, Serial m)
-    deriving Candid via (AsRecord EmptyRecord)
-
-newtype MiddleField a = MiddleField a
-    deriving (Eq, Show)
-
-instance Candid a => Candid (MiddleField a) where
-    type AsCandid (MiddleField a) = Rec ("_1_" .== a)
-    toCandid (MiddleField x) = #_1_ .== x
-    fromCandid r = MiddleField (r .! #_1_)
-
-newtype JustRight a = JustRight a
-    deriving (Eq, Show)
-
-instance Candid a => Candid (JustRight a) where
-    type AsCandid (JustRight a) = Var ("Right" .== a)
-    toCandid (JustRight x) = V.singleton (Label @"Right") x
-    fromCandid = JustRight . snd . V.unSingleton
-
-data SimpleRecord = SimpleRecord { foo :: Bool, bar :: Word8 }
-    deriving (Generic, Eq, Show)
-    deriving (Serial m)
-    deriving Candid via (AsRecord SimpleRecord)
-
-roundTripTest :: forall a. (CandidArg a, Eq a, Show a) => a -> Assertion
-roundTripTest v1 = do
-  let bytes1 = encode v1
-  v2 <- case decode @a bytes1 of
-    Left err -> assertFailure err
-    Right v -> return v
-  assertEqual "values" v1 v2
-
-subTypProp :: forall a b.  (CandidArg a, Serial IO a, Show a, CandidArg b) => TestTree
-subTypProp = testProperty desc $ \v ->
-    isRight $ decode @b (encode @a v)
-  where
-    desc = show $ pretty (tieKnot (seqDesc @a)) <+> "<:" <+> pretty (tieKnot (seqDesc @b))
-
-subTypeTest' :: forall a b.
-    (CandidArg a, Eq a, Show a) =>
-    (CandidArg b, Eq b, Show b) =>
-    a -> b -> Assertion
-subTypeTest' v1 v2 = do
-  let bytes1 = encode v1
-  v2' <- case decode @b bytes1 of
-    Left err -> assertFailure err
-    Right v -> return v
-  v2 @=? v2'
-
-subTypeTest :: forall a b.
-    (CandidArg a, Eq a, Show a) =>
-    (CandidArg b, Eq b, Show b) =>
-    a -> b -> Assertion
-subTypeTest v1 v2 = do
-  subTypeTest' v1 v2
-  -- now try the other direction
-  let bytes2 = encode v2
-  case decode @a bytes2 of
-    Left _err -> return ()
-    Right _ -> assertFailure "converse subtype test succeeded"
-
-instance Monad m => Serial m T.Text where
-    series = T.pack <$> series
-
-instance (Monad m, Serial m a) => Serial m (V.Vector a) where
-    series = V.fromList <$> series
-
-parseTest :: HasCallStack => String -> DidFile -> TestTree
-parseTest c e = testCase c $
-    case parseDid c of
-        Left err -> assertFailure err
-        Right s -> s @?= e
-
-printTestType :: forall a. (Candid a, HasCallStack) => String -> TestTree
-printTestType e = testCase e $
-    show (pretty (typeDesc @a)) @?= e
-
-printTestSeq :: forall a. (CandidArg a, HasCallStack) => String -> TestTree
-printTestSeq e = testCase e $
-    show (pretty (tieKnot (seqDesc @a))) @?= e
-
-roundTripTestGroup :: String ->
-    (forall a. (CandidArg a, Serial IO a, Show a, Eq a) => a -> Either String a) ->
-    TestTree
-roundTripTestGroup group_desc roundtrip =
-    withSomeTypes ("roundtrip (" <> group_desc <> ")") $ \(Proxy :: Proxy a) ->
-        let desc = show $ pretty (tieKnot (seqDesc @a)) in
-        testProperty desc $ \v ->
-            case roundtrip @a v of
-                Right y | y == v -> Right ("all good" :: String)
-                Right y -> Left $
-                    show v ++ " round-tripped to " ++ show y
-                Left err -> Left $
-                    show v ++ " failed to decode:\n" ++ err
-
-withSomeTypes ::
-    String ->
-    (forall a. (CandidArg a, Serial IO a, Show a, Eq a) => Proxy a -> TestTree) ->
-    TestTree
-withSomeTypes groupName mkTest =
-    testGroup groupName
-    [ mkTest (Proxy @Bool)
-    , mkTest (Proxy @Natural)
-    , mkTest (Proxy @Word8)
-    , mkTest (Proxy @Word16)
-    , mkTest (Proxy @Word32)
-    , mkTest (Proxy @Word64)
-    , mkTest (Proxy @Integer)
-    , mkTest (Proxy @Int8)
-    , mkTest (Proxy @Int16)
-    , mkTest (Proxy @Int32)
-    , mkTest (Proxy @Int64)
-    , mkTest (Proxy @Float)
-    , mkTest (Proxy @Double)
-    , mkTest (Proxy @T.Text)
-    , mkTest (Proxy @())
-    , mkTest (Proxy @Reserved)
-    , mkTest (Proxy @Principal)
-    , mkTest (Proxy @BS.ByteString)
-    , mkTest (Proxy @(Maybe T.Text))
-    , mkTest (Proxy @(V.Vector T.Text))
-    , mkTest (Proxy @EmptyRecord)
-    , mkTest (Proxy @(ARecord T.Text))
-    , mkTest (Proxy @(Either Bool T.Text))
-    , mkTest (Proxy @SimpleRecord)
-    , mkTest (Proxy @(Rec ("a" .== Bool .+ "b" .== Bool .+ "c" .== Bool)))
-    , mkTest (Proxy @(V.Var ("upgrade" .== () .+ "reinstall" .== () .+ "install" .== ())))
-    , mkTest (Proxy @(FuncRef (Bool, T.Text, AnnFalse, AnnFalse)))
-    , mkTest (Proxy @(FuncRef (Bool, T.Text, AnnTrue, AnnFalse)))
-    , mkTest (Proxy @(FuncRef (Bool, T.Text, AnnFalse, AnnTrue)))
-    , mkTest (Proxy @(ServiceRef Empty))
-    ]
-
-tests :: TestTree
-tests = testGroup "tests"
-  [ specTests
-  , testGroup "encode tests"
-    [ testCase "empty" $ encode () @?= B.pack "DIDL\0\0"
-    , testCase "bool" $ encode (Unary True) @?= B.pack "DIDL\0\1\x7e\1"
-    ]
-  , testGroup "decode error message"
-      [ testCase "simple mismatch" $ fromCandidVals @(Unary ()) (toCandidVals True) @?= Left "Cannot coerce true into null"
-      , testCase "missing variant" $ fromCandidVals @(Either () ()) (toCandidVals (V.singleton #foo ())) @?= Left "Unexpected tag foo"
-      , testCase "error in variant" $ fromCandidVals @(Either () ()) (toCandidVals (Left @Bool @() True)) @?= Left "Cannot coerce true into null"
-      ]
-  , testGroup "roundtrip"
-    [ testCase "empty" $ roundTripTest ()
-    , testCase "bool" $ roundTripTest $ Unary True
-    , testCase "simple record 1" $ roundTripTest (ARecord True, False)
-    , testCase "simple record 2" $ roundTripTest (ARecord (100000 :: Natural), False)
-    , testCase "simple variant 1" $ roundTripTest $ Unary (Left True :: Either Bool Bool)
-    , testCase "simple variant 2" $ roundTripTest $ Unary (Right False :: Either Bool Bool)
-    , testCase "nested record 2" $ roundTripTest (ARecord (True,False), False)
-    , testCase "peano" $ roundTripTest $ Unary peano
-    , testCase "lists" $ roundTripTest (natList, stringList)
-    , testCase "custom record" $ roundTripTest $ Unary (SimpleRecord True 42)
-    ]
-  , testGroup "subtypes"
-    [ testCase "nat/int" $ subTypeTest (Unary (42 :: Natural)) (Unary (42 :: Integer))
-    , testCase "null/opt" $ subTypeTest (Unary ()) (Unary (Nothing @Integer))
-    , testCase "rec" $ subTypeTest (ARecord True, True) (EmptyRecord, True)
-    , testCase "tuple" $ subTypeTest ((42::Integer,-42::Integer), 100::Integer) (EmptyRecord, 100::Integer)
-    , testCase "variant" $ subTypeTest' (JustRight (42 :: Natural), True) (Right 42 :: Either Bool Natural, True)
-    , testCase "rec/any" $ subTypeTest (ARecord True, True) (Reserved, True)
-    , testCase "tuple/any" $ subTypeTest ((42::Integer, 42::Natural), True) (Reserved, True)
-    , testCase "tuple/tuple" $ subTypeTest ((42::Integer,-42::Integer,True), 100::Integer) ((42::Integer, -42::Integer), 100::Integer)
-    , testCase "tuple/middle" $ subTypeTest ((42::Integer,-42::Integer,True), 100::Integer) (MiddleField (-42) :: MiddleField Integer, 100::Integer)
-    , testCase "records" $ subTypeTest (Unary (SimpleRecord True 42)) (Unary (ARecord True))
-    ]
-
-  , roundTripTestGroup "Haskell → Candid → Haskell" $ \(v :: a) ->
-        decode @a (encode @a v)
-  , roundTripTestGroup "Haskell → [Value] → Haskell" $ \(v :: a) ->
-        fromCandidVals (toCandidVals @a v)
-  , roundTripTestGroup "Haskell → [Value] → Textual → [Value] → Haskell" $ \(v :: a) ->
-        parseValues (show (pretty (toCandidVals @a v))) >>= fromCandidVals @a
-
-  , testGroup "subtype smallchecks"
-    [ subTypProp @Natural @Natural
-    , subTypProp @(Rec ("Hi" .== Word8 .+ "_1_" .== Word8)) @Reserved
-    , subTypProp @(Rec ("Hi" .== Word8 .+ "_1_" .== Word8)) @(Rec ("Hi" .== Reserved))
-    , subTypProp @(Rec ("Hi" .== Word8 .+ "_1_" .== Word8)) @(Rec ("Hi" .== Word8))
-    , subTypProp @(Rec ("Hi" .== Word8 .+ "_1_" .== Word8)) @(Rec ("_1_" .== Word8))
-    , subTypProp @(Rec ("Hi" .== Word8 .+ "_1_" .== Word8 .+ "_2_" .== Bool)) @(Rec ("_1_" .== Word8))
-    , subTypProp @(Maybe (Rec ("Hi" .== Word8 .+ "_1_" .== Word8 .+ "_0_" .== Bool))) @(Maybe (Bool,Word8))
-    , subTypProp @(Var ("Hi" .== Word8)) @(Var ("Hi" .== Word8 .+ "Ho" .== T.Text))
-    , subTypProp @(Var ("Ho" .== T.Text)) @(Var ("Hi" .== Word8 .+ "Ho" .== T.Text))
-    , subTypProp @Natural @Reserved
-    , subTypProp @BS.ByteString @Reserved
-    , subTypProp @BS.ByteString @(V.Vector Word8)
-    , subTypProp @(V.Vector Word8) @BS.ByteString
-    , subTypProp @Principal @Reserved
-    ]
-  , testGroup "candid type printing" $
-    [ printTestType @Bool "bool"
-    , printTestType @Integer "int"
-    , printTestType @Natural "nat"
-    , printTestType @Int8 "int8"
-    , printTestType @Word8 "nat8"
-    , printTestType @SimpleRecord "record {bar : nat8; foo : bool}"
-    , printTestType @(JustRight T.Text) "variant {Right : text}"
-    , printTestType @(FuncRef (Bool, Unary (), AnnTrue, AnnFalse)) "func (bool) -> (null) query"
-    , printTestType @(FuncRef (Bool, T.Text, AnnFalse, AnnTrue)) "func (bool) -> (text) oneway"
-    , printTestType @(ServiceRef Empty) "service : {}"
-    , printTestType @(ServiceRef ("foo" .== (Bool, T.Text, AnnFalse, AnnTrue) .+ "bar" .== ((),(),AnnFalse, AnnFalse)))
-        "service : {bar : () -> (); foo : (bool) -> (text) oneway;}"
-    , printTestSeq @() "()"
-    , printTestSeq @(Unary ()) "(null)"
-    , printTestSeq @(Unary (Bool, Bool)) "(record {0 : bool; 1 : bool})"
-    , printTestSeq @((),()) "(null, null)"
-    , printTestSeq @(Bool,Bool) "(bool, bool)"
-    , printTestSeq @(Bool,(Bool, Bool)) "(bool, record {0 : bool; 1 : bool})"
-    , printTestSeq @Bool "(bool)"
-    ]
-  , testGroup "candid value printing" $
-    let t :: Value -> String -> TestTree
-        t v e = testCase e $ show (pretty v) @?= e
-    in
-    [ t (BoolV True) "true"
-    , t (BoolV False) "false"
-    , t (NatV 1) "1"
-    , t (IntV 1) "+1"
-    , t (IntV 0) "+0"
-    , t (IntV (-1)) "-1"
-    , t (Nat8V 1) "(1 : nat8)"
-    , t (RecV [("bar", TextV "baz")]) "record {bar = \"baz\"}"
-    , t (FuncV (Principal "\xde\xad\xbe\xef") "foo") "func \"psokg-ww6vw-7o6\".\"foo\""
-    , t (ServiceV (Principal "\xde\xad\xbe\xef")) "service \"psokg-ww6vw-7o6\""
-    , t (PrincipalV (Principal "")) "principal \"aaaaa-aa\""
-    , t (PrincipalV (Principal "\xab\xcd\x01")) "principal \"em77e-bvlzu-aq\""
-    , t (PrincipalV (Principal "\xde\xad\xbe\xef")) "principal \"psokg-ww6vw-7o6\""
-    ]
-  , testGroup "candid value printing (via binary) " $
-    let t :: forall a. (HasCallStack, CandidArg a) => a -> String -> TestTree
-        t v e = testCase e $ do
-          let bytes = encode v
-          (_, vs) <- either assertFailure return $ decodeVals bytes
-          show (pretty vs) @?= e
-    in
-    [ t True "(true)"
-    , t (SimpleRecord False 42) "(record {bar = (42 : nat8); foo = false})"
-    , t (JustRight (Just (3 :: Natural))) "(variant {Right = opt 3})"
-    , t (JustRight (3 :: Word8)) "(variant {Right = (3 : nat8)})"
-    , t () "()"
-    , t (Unary ()) "(null)"
-    , t (Unary (True, False)) "(record {true; false})"
-    , t (Unary (True, (True, False))) "(record {true; record {true; false}})"
-    , t (#_0_ .== True .+ #_1_ .== False) "(record {true; false})"
-    ]
-
-  , testGroup "dynamic values (AST)" $
-    let t :: forall a. (HasCallStack, CandidArg a, Eq a, Show a) => String -> a -> TestTree
-        t s e = testCase s $ do
-          bytes <- either assertFailure return $ encodeTextual s
-          x <- either assertFailure return $ decode @a bytes
-          x @?= e
-
-        t' :: HasCallStack => String -> TestTree
-        t' s = testCase ("Bad: " <> s) $ do
-          vs <- either assertFailure return $ parseValues s
-          case encodeDynValues vs of
-            Left _err -> return ()
-            Right _ -> assertFailure "Ill-typed value encoded?"
-    in
-    [ t "true" True
-    , t "false" False
-    , t "1" (1 :: Natural)
-    , t "1 : nat8" (1 :: Word8)
-    , t "record { bar = \"baz\" }" (#bar .== ("baz":: T.Text))
-    , t "vec {}" (V.fromList [] :: V.Vector Void)
-    , t "vec {4; +4}" (V.fromList [4 :: Integer,4])
-    , t "vec {4; null : reserved}" (V.fromList [Reserved, Reserved])
-    , t "vec {record {}; record {0 = true}}" (V.fromList [R.empty, R.empty])
-    , t "vec {variant {a = true}; variant {b = null}}"
-        (V.fromList [IsJust #a True, IsJust #b () :: V.Var ("a" V..== Bool V..+ "b" V..== ())])
-    , t "\"hello\"" ("hello" :: T.Text)
-    , t "blob \"hello\"" ("hello" :: BS.ByteString)
-    , t "blob \"\\00\\ff\"" ("\x00\xff" :: BS.ByteString)
-    , t "func \"psokg-ww6vw-7o6\".\"foo\""
-        (FuncRef @((), (), AnnFalse, AnnFalse) (Principal "\xde\xad\xbe\xef") "foo")
-    , t "func \"psokg-ww6vw-7o6\".foo"
-        (FuncRef @((), (), AnnFalse, AnnFalse) (Principal "\xde\xad\xbe\xef") "foo")
-    , t "func \"psokg-ww6vw-7o6\".\"\""
-        (FuncRef @((), (), AnnFalse, AnnFalse) (Principal "\xde\xad\xbe\xef") "")
-    , t "service \"psokg-ww6vw-7o6\""
-        (ServiceRef @Empty (Principal "\xde\xad\xbe\xef"))
-    , t "principal \"psokg-ww6vw-7o6\""
-        (Principal "\xde\xad\xbe\xef")
-
-    , t' "vec {true; 4}"
-    ]
-
-  , testGroup "candid type parsing"
-    [ parseTest "service : {}" $
-      DidFile [] []
-    , parseTest "service : { foo : (text) -> (text) }" $
-      DidFile [] [("foo", MethodType [TextT] [TextT] False False)]
-    , parseTest "service : { foo : (text,) -> (text,); }" $
-      DidFile [] [("foo", MethodType [TextT] [TextT] False False)]
-    , parseTest "service : { foo : (x : text,) -> (y : text,); }" $
-      DidFile [] [("foo", MethodType [TextT] [TextT] False False)]
-    , parseTest "service : { foo : (opt text) -> () }" $
-      DidFile [] [("foo", MethodType [OptT TextT] [] False False) ]
-    , parseTest "service : { foo : (record { text; blob }) -> () }" $
-      DidFile [] [("foo", MethodType [RecT [(hashedField 0, TextT), (hashedField 1, BlobT)]] [] False False) ]
-    , parseTest "service : { foo : (record { x_ : null; 5 : nat8 }) -> () }" $
-      DidFile [] [("foo", MethodType [RecT [("x_", NullT), (hashedField 5, Nat8T)]] [] False False) ]
-    , parseTest "service : { foo : (record { x : null; 5 : nat8 }) -> () }" $
-      DidFile [] [("foo", MethodType [RecT [("x", NullT), (hashedField 5, Nat8T)]] [] False False) ]
-    , parseTest "service : { foo : (text) -> (text) query }" $
-      DidFile [] [("foo", MethodType [TextT] [TextT] True False)]
-    , parseTest "service : { foo : (text) -> (text) oneway }" $
-      DidFile [] [("foo", MethodType [TextT] [TextT] False True)]
-    , parseTest "service : { foo : (text) -> (text) query oneway }" $
-      DidFile [] [("foo", MethodType [TextT] [TextT] True True)]
-    , parseTest "service : { foo : (text) -> (text) oneway query }" $
-      DidFile [] [("foo", MethodType [TextT] [TextT] True True)]
-    , parseTest "service : (opt SomeInit) -> { foo : (text) -> (text) oneway query }" $
-      DidFile [] [("foo", MethodType [TextT] [TextT] True True)]
-    , parseTest "type t = int; service : { foo : (t) -> (t) }" $
-      DidFile [("t", IntT)] [("foo", MethodType [RefT "t"] [RefT "t"] False False)]
-    ]
-  , thTests
-  , testProperty "field name escaping round-tripping" $ \e ->
-      let f = either labledField hashedField e in
-      let f' = unescapeFieldName (escapeFieldName f) in
-      f' == f
-  , testGroup "candid hash inversion"
-    [ QC.testProperty "long dictionary name" $
-        let s = "precriticized" in
-        invertHash (candidHash s) QC.=== Just s
-    , QC.testProperty "long capitalized dictionary name" $
-        let s = "Precriticized" in
-        invertHash (candidHash s) QC.=== Just s
-    , QC.testProperty "all hashes find something" $
-        QC.forAll QC.arbitraryBoundedIntegral $ \w ->
-        w >= 32 QC.==> case invertHash w of
-            Nothing -> False
-            Just s -> candidHash s == w
-    ]
-  ]
-
-instance Monad m => Serial m BS.ByteString where
-    series = BS.pack <$> series
-
-instance Monad m => Serial m Principal where
-    series = Principal <$> series
-
-instance Monad m => Serial m Reserved where
-    series = Reserved <$ series @m @()
-
-instance Monad m => Serial m (FuncRef mt) where
-    series = FuncRef <$> series <*> series
-
-instance Monad m => Serial m (ServiceRef r) where
-    series = ServiceRef <$> series
-
-instance (Monad m, Forall r (Serial m), AllUniqueLabels r) => Serial m (Rec r) where
-    series = R.fromLabelsA @(Serial m) (\_l -> series)
-
-instance (Monad m, Forall r (Serial m), AllUniqueLabels r) => Serial m (Var r) where
-    series = V.fromLabels @(Serial m) (\_l -> series)
+main = defaultMainWithRerun $
+  testGroup "tests" $ tests ++ [specTests, thTests]