diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,9 @@
 # language-ats
 
+## 1.7.1.0
+
+  * Fix a bug in how `val`s were handled in `SATS` files
+
 ## 1.7.0.6
 
   * Fix bug by introducing immorality
diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.18
 name: language-ats
-version: 1.7.0.6
+version: 1.7.1.0
 license: BSD3
 license-file: LICENSE
 copyright: Copyright: (c) 2018-2019 Vanessa McHale
@@ -54,11 +54,11 @@
     build-depends:
         base >=4.9 && <5,
         array -any,
-        recursion >=1.0.0.0,
-        microlens -any,
+        recursion >=2.2.3.0,
+        microlens >=0.3.0.0,
         deepseq -any,
         ansi-wl-pprint >=0.6.8,
-        composition-prelude -any,
+        composition-prelude >=2.0.4.0,
         containers -any,
         transformers -any
 
diff --git a/src/Language/ATS/Parser.y b/src/Language/ATS/Parser.y
--- a/src/Language/ATS/Parser.y
+++ b/src/Language/ATS/Parser.y
@@ -368,8 +368,8 @@
         | Literal { PLiteral $1 }
         | Pattern when Expression { Guarded $2 $3 $1 }
         | at Pattern { AtPattern $1 $2 }
-        | identifier Universals Pattern { UniversalPattern (token_posn $1) (to_string $1) $2 $3 }
-        | identifierSpace Universals Pattern { UniversalPattern (token_posn $1) (to_string $1) $2 $3 }
+        | identifier Universals optional(Pattern) { UniversalPattern (token_posn $1) (to_string $1) $2 $3 }
+        | identifierSpace Universals optional(Pattern) { UniversalPattern (token_posn $1) (to_string $1) $2 $3 }
         | Pattern customOperator Pattern { BinPattern (token_posn $2) (SpecialInfix (token_posn $2) (to_string $2)) $1 $3 }
         | Pattern as Pattern { As $2 $1 $3 }
         | Existential Pattern { ExistentialPattern $1 $2 }
@@ -967,8 +967,9 @@
               : parens(Args) Signature Type plainArrow Expression { StackF $2 $1 $3 $5 }
 
 ValDecl :: { [Declaration AlexPosn] }
-        : val Pattern colon Type eq PreExpression { [ Val (get_addendum $1) (Just $4) $2 $6 ] }
-        | val Pattern eq Expression { [ Val (get_addendum $1) Nothing $2 $4 ] }
+        : val Pattern colon Type eq PreExpression { [ Val (get_addendum $1) (Just $4) (Just $2) (Just $6) ] }
+        | val Pattern eq Expression { [ Val (get_addendum $1) Nothing (Just $2) (Just $4) ] }
+        | val Pattern colon Type { [ Val (get_addendum $1) (Just $4) (Just $2) Nothing ] }
         | ValDecl and Pattern eq Expression { AndDecl Nothing $3 $5 : $1 }
         | extern ValDecl { over _head (Extern $1) $2 }
         | val Pattern eq colon {% left $ Expected $4 "Expression" ":" }
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -227,7 +227,8 @@
         a (TuplePatternF ps)           = parens (patternHelper ps)
         a (BoxTuplePatternF _ ps)      = "'(" <> patternHelper ps <> ")"
         a (AtPatternF _ p)             = "@" <> p
-        a (UniversalPatternF _ n us p) = text n <> prettyArgsU "" "" us <> p
+        a (UniversalPatternF _ n us (Just p)) = text n <> prettyArgsU "" "" us <> p
+        a (UniversalPatternF _ n us Nothing) = text n <> prettyArgsU "" "" us
         a (ExistentialPatternF e p)    = pretty e <> p
         a (AsF _ p p')                 = p <+> "as" <+> p'
         a (BinPatternF _ op p p')      = p <+> pretty op <+> p'
@@ -330,7 +331,7 @@
         a (ArrayTypeF _ t n)               = "@[" <> t <> "][" <> pretty n <> "]"
         a (ProofTypeF _ t t')              = parens (pre' `op` "|" <+> prettyArgsG mempty mempty t')
             where pre' = prettyArgsG mempty mempty t
-                  op = bool (<+>) (<>) ('\n' `elem` showFast pre')
+                  op = if '\n' `elem` showFast pre' then (<>) else (<+>)
         a (ConcreteTypeF e)                = pretty e
         a (TupleF _ ts)                    = parens (mconcat (punctuate ", " (fmap pretty (reverse ts))))
         a (BoxTupleF _ ts)                 = "'(" <> mconcat (punctuate ", " (toList $ fmap pretty (NE.reverse ts))) <> ")"
@@ -521,7 +522,7 @@
 prettyArgsU = prettyArgs' ","
 
 prettyArgs' :: (Pretty a, Functor f, Foldable f) => Doc -> Doc -> Doc -> f a -> Doc
-prettyArgs' = fmap pretty -.*** prettyArgsG'
+prettyArgs' = fmap pretty .@@@ prettyArgsG'
 
 prettyArgs :: (Pretty a, Foldable f, Functor f) => f a -> Doc
 prettyArgs = prettyArgs' ", " "(" ")"
diff --git a/src/Language/ATS/Rewrite.hs b/src/Language/ATS/Rewrite.hs
--- a/src/Language/ATS/Rewrite.hs
+++ b/src/Language/ATS/Rewrite.hs
@@ -25,7 +25,7 @@
 
 rewriteDecl :: Eq a => FixityState a -> Declaration a -> Declaration a
 rewriteDecl st (Extern l d) = Extern l (rewriteDecl st d)
-rewriteDecl st x@Val{} = exprLens st valExpression x
+rewriteDecl st x@Val{} = exprLens st (valExpression._Just) x
 rewriteDecl st x@Var{} = exprLenses st [varExpr1._Just, varExpr2._Just] x
 rewriteDecl st x@PrVal{} = exprStaLens st (prValExpr._Just) x
 rewriteDecl st x@PrVar{} = exprStaLens st (prValExpr._Just) x
diff --git a/src/Language/ATS/Types.hs b/src/Language/ATS/Types.hs
--- a/src/Language/ATS/Types.hs
+++ b/src/Language/ATS/Types.hs
@@ -83,7 +83,7 @@
 data Declaration a = Func { pos :: a, _fun :: Function a }
                    | Impl { implArgs :: Args a, _impl :: Implementation a } -- TODO do something better for implicit universals
                    | ProofImpl { implArgs :: Args a, _impl :: Implementation a }
-                   | Val { add :: Addendum, valT :: Maybe (Type a), valPat :: Pattern a, _valExpression :: Expression a }
+                   | Val { add :: Addendum, valT :: Maybe (Type a), valPat :: Maybe (Pattern a), _valExpression :: Maybe (Expression a) }
                    | StaVal [Universal a] String (Type a)
                    | PrVal { prvalPat :: Pattern a, _prValExpr :: Maybe (StaticExpression a), prValType :: Maybe (Type a) }
                    | PrVar { prvarPat :: Pattern a, _prVarExpr :: Maybe (StaticExpression a), prVarType :: Maybe (Type a) }
@@ -156,7 +156,7 @@
             | AnonymousRecord a (NonEmpty (String, Type a))
             | WhereType a (Type a) String (SortArgs a) (Type a)
             | AddrType a -- ^ @addr@
-            deriving (Eq, Generic, NFData)
+            deriving (Eq, Generic, NFData, Recursive)
 
 data TypeF a x = TupleF a [x]
                | BoxTupleF a (NonEmpty x)
@@ -180,34 +180,10 @@
                | AnonymousRecordF a (NonEmpty (String, x))
                | WhereTypeF a x String (SortArgs a) x
                | AddrTypeF a
-               deriving (Functor)
+               deriving (Functor, Generic)
 
 type instance Base (Type a) = TypeF a
 
-instance Recursive (Type a) where
-    project (Tuple x tys)              = TupleF x tys
-    project (BoxTuple x tys)           = BoxTupleF x tys
-    project (Named n)                  = NamedF n
-    project (Ex e mty)                 = ExF e mty
-    project (ForA u ty)                = ForAF u ty
-    project (Dependent n tys)          = DependentF n tys
-    project (Unconsumed ty)            = UnconsumedF ty
-    project (AsProof ty mty)           = AsProofF ty mty
-    project (FromVT ty)                = FromVTF ty
-    project (MaybeVal ty)              = MaybeValF ty
-    project (AtExpr l ty se)           = AtExprF l ty se
-    project (ArrayType l ty n)         = ArrayTypeF l ty n
-    project (ProofType l tys ty')      = ProofTypeF l tys ty'
-    project (ConcreteType se)          = ConcreteTypeF se
-    project (RefType ty)               = RefTypeF ty
-    project (ViewType l ty)            = ViewTypeF l ty
-    project (FunctionType s ty ty')    = FunctionTypeF s ty ty'
-    project (ImplicitType l)           = ImplicitTypeF l
-    project (ViewLiteral a)            = ViewLiteralF a
-    project (AnonymousRecord l stys)   = AnonymousRecordF l stys
-    project (WhereType l ty s sas ty') = WhereTypeF l ty s sas ty'
-    project (AddrType l)               = AddrTypeF l
-
 -- | A type for @=>@, @=\<cloref1>@, etc.
 data LambdaType a = Plain a
                   | Spear a -- | @=>>@
@@ -233,11 +209,11 @@
                | TuplePattern [Pattern a]
                | BoxTuplePattern a [Pattern a]
                | AtPattern a (Pattern a)
-               | UniversalPattern a String [Universal a] (Pattern a)
+               | UniversalPattern a String [Universal a] (Maybe (Pattern a))
                | ExistentialPattern (Existential a) (Pattern a)
                | As a (Pattern a) (Pattern a)
                | BinPattern a (BinOp a) (Pattern a) (Pattern a) -- ^ For use with e.g. @::@.
-               deriving (Eq, Generic, NFData)
+               deriving (Eq, Generic, NFData, Recursive)
 
 data PatternF a x = PNameF (Name a) [x]
                   | PSumF String x
@@ -248,29 +224,14 @@
                   | TuplePatternF [x]
                   | BoxTuplePatternF a [x]
                   | AtPatternF a x
-                  | UniversalPatternF a String [Universal a] x
+                  | UniversalPatternF a String [Universal a] (Maybe x)
                   | ExistentialPatternF (Existential a) x
                   | AsF a x x
                   | BinPatternF a (BinOp a) x x
-                  deriving (Functor)
+                  deriving (Functor, Generic)
 
 type instance Base (Pattern a) = PatternF a
 
-instance Recursive (Pattern a) where
-    project (PName x ps)                = PNameF x ps
-    project (PSum x p)                  = PSumF x p
-    project (PLiteral e)                = PLiteralF e
-    project (Guarded x e p)             = GuardedF x e p
-    project (Free p)                    = FreeF p
-    project (Proof x ps ps')            = ProofF x ps ps'
-    project (TuplePattern ps)           = TuplePatternF ps
-    project (BoxTuplePattern x ps)      = BoxTuplePatternF x ps
-    project (AtPattern x p)             = AtPatternF x p
-    project (UniversalPattern x s us p) = UniversalPatternF x s us p
-    project (ExistentialPattern e x)    = ExistentialPatternF e x
-    project (As x p p')                 = AsF x p p'
-    project (BinPattern a op p p')      = BinPatternF a op p p'
-
 data Paired a b = Both a b
                 | First a
                 | Second b
@@ -294,7 +255,7 @@
             | View a Addendum -- ^ @view@
             | TupleSort a (Sort a) (Sort a)
             | ArrowSort a (Sort a) (Sort a)
-            deriving (Eq, Generic, NFData)
+            deriving (Eq, Generic, NFData, Recursive)
 
 data SortF a x = NamedSortF String
                | T0pF Addendum
@@ -304,20 +265,10 @@
                | ViewF a Addendum
                | TupleSortF a x x
                | ArrowSortF a x x
-               deriving (Functor)
+               deriving (Functor, Generic)
 
 type instance Base (Sort a) = SortF a
 
-instance Recursive (Sort a) where
-    project (NamedSort s)      = NamedSortF s
-    project (T0p a)            = T0pF a
-    project (Vt0p a)           = Vt0pF a
-    project Addr               = AddrF
-    project (VType x a)        = VTypeF x a
-    project (View x a)         = ViewF x a
-    project (TupleSort x s s') = TupleSortF x s s'
-    project (ArrowSort x s s') = ArrowSortF x s s'
-
 -- | Wrapper for universal quantifiers (refinement types)
 data Universal a = Universal { bound :: [String], typeU :: Maybe (Sort a), prop :: [StaticExpression a] }
     deriving (Eq, Generic, NFData)
@@ -374,7 +325,7 @@
                         | ProofLinearLambda a (LambdaType a) (Pattern a) (StaticExpression a)
                         | WhereStaExp (StaticExpression a) (ATS a)
                         | SParens (StaticExpression a)
-                        deriving (Eq, Generic, NFData)
+                        deriving (Eq, Generic, NFData, Recursive, Corecursive)
 
 data StaticExpressionF a x = StaticValF (Name a)
                            | StaticBinaryF (BinOp a) x x
@@ -394,50 +345,10 @@
                            | ProofLinearLambdaF a (LambdaType a) (Pattern a) x
                            | WhereStaExpF x (ATS a)
                            | SParensF x
-                           deriving (Functor)
+                           deriving (Functor, Generic)
 
 type instance Base (StaticExpression a) = StaticExpressionF a
 
-instance Recursive (StaticExpression a) where
-    project (StaticVal n)               = StaticValF n
-    project (StaticBinary b x x')       = StaticBinaryF b x x'
-    project (StaticHex h)               = StaticHexF h
-    project (StaticInt i)               = StaticIntF i
-    project (SPrecede x x')             = SPrecedeF x x'
-    project (SPrecedeList xs)           = SPrecedeListF xs
-    project (StaticVoid x)              = StaticVoidF x
-    project (Sif e e' e'')              = SifF e e' e''
-    project (SCall n is ts es)          = SCallF n is ts es
-    project (SUnary u x)                = SUnaryF u x
-    project (SLet x ds e)               = SLetF x ds e
-    project (SCase a x ples)            = SCaseF a x ples
-    project (SString s)                 = SStringF s
-    project (Witness a e e')            = WitnessF a e e'
-    project (ProofLambda a l p e)       = ProofLambdaF a l p e
-    project (ProofLinearLambda a l p e) = ProofLinearLambdaF a l p e
-    project (WhereStaExp e ds)          = WhereStaExpF e ds
-    project (SParens e)                 = SParensF e
-
-instance Corecursive (StaticExpression a) where
-    embed (StaticValF n)               = StaticVal n
-    embed (StaticBinaryF b e e')       = StaticBinary b e e'
-    embed (StaticHexF h)               = StaticHex h
-    embed (StaticIntF i)               = StaticInt i
-    embed (SPrecedeF e e')             = SPrecede e e'
-    embed (SPrecedeListF es)           = SPrecedeList es
-    embed (StaticVoidF l)              = StaticVoid l
-    embed (SifF e e' e'')              = Sif e e' e''
-    embed (SCallF n is ts es)          = SCall n is ts es
-    embed (SUnaryF u e)                = SUnary u e
-    embed (SLetF l ds e)               = SLet l ds e
-    embed (SCaseF a x ples)            = SCase a x ples
-    embed (SStringF s)                 = SString s
-    embed (WitnessF l e e')            = Witness l e e'
-    embed (ProofLambdaF a l p e)       = ProofLambda a l p e
-    embed (ProofLinearLambdaF a l p e) = ProofLinearLambda a l p e
-    embed (WhereStaExpF e ds)          = WhereStaExp e ds
-    embed (SParensF e)                 = SParens e
-
 -- | A (possibly effectful) expression.
 data Expression a = Let a (ATS a) (Maybe (Expression a))
                   | VoidLiteral a -- ^ The '()' literal representing inaction.
@@ -498,7 +409,7 @@
                   | ParenExpr a (Expression a)
                   | CommentExpr String (Expression a)
                   | MacroVar a String
-                  deriving (Eq, Generic, NFData)
+                  deriving (Eq, Generic, NFData, Recursive, Corecursive)
 
 data ExpressionF a x = LetF a (ATS a) (Maybe x)
                      | VoidLiteralF a
@@ -545,103 +456,9 @@
                      | ParenExprF a x
                      | CommentExprF String x
                      | MacroVarF a String
-                     deriving (Functor)
+                     deriving (Generic, Functor)
 
 type instance Base (Expression a) = (ExpressionF a)
-
-instance Recursive (Expression a) where
-    project (Let l ds me)                 = LetF l ds me
-    project (VoidLiteral l)               = VoidLiteralF l
-    project (Call n is us mps as)         = CallF n is us mps as
-    project (NamedVal n)                  = NamedValF n
-    project (ListLiteral l s t es)        = ListLiteralF l s t es
-    project (If e e' me)                  = IfF e e' me
-    project (UintLit u)                   = UintLitF u
-    project (FloatLit f)                  = FloatLitF f
-    project (IntLit i)                    = IntLitF i
-    project (HexLit s)                    = HexLitF s
-    project (UnderscoreLit l)             = UnderscoreLitF l
-    project (Lambda l lt p e)             = LambdaF l lt p e
-    project (LinearLambda l lt p e)       = LinearLambdaF l lt p e
-    project (Index l n e)                 = IndexF l n e
-    project (Access l e n)                = AccessF l e n
-    project (StringLit s)                 = StringLitF s
-    project (CharLit c)                   = CharLitF c
-    project (AddrAt l e)                  = AddrAtF l e
-    project (ViewAt l e)                  = ViewAtF l e
-    project (Binary op e e')              = BinaryF op e e'
-    project (Unary op e)                  = UnaryF op e
-    project (IfCase l arms)               = IfCaseF l arms
-    project (Case l k e arms)             = CaseF l k e arms
-    project (RecordValue l recs)          = RecordValueF l recs
-    project (BoxRecordValue l recs)       = BoxRecordValueF l recs
-    project (Precede e e')                = PrecedeF e e'
-    project (ProofExpr a e e')            = ProofExprF a e e'
-    project (TypeSignature e ty)          = TypeSignatureF e ty
-    project (WhereExp e ds)               = WhereExpF e ds
-    project (TupleEx l es)                = TupleExF l es
-    project (BoxTupleEx l es)             = BoxTupleExF l es
-    project (While l e e')                = WhileF l e e'
-    project (WhileStar l us t as e e' ty) = WhileStarF l us t as e e' ty
-    project (For l e e')                  = ForF l e e'
-    project (ForStar l us t as e e')      = ForStarF l us t as e e'
-    project (Actions ds)                  = ActionsF ds
-    project (Begin l e)                   = BeginF l e
-    project (BinList op es)               = BinListF op es
-    project (PrecedeList es)              = PrecedeListF es
-    project (FixAt a s sfun)              = FixAtF a s sfun
-    project (LambdaAt a sfun)             = LambdaAtF a sfun
-    project (LinearLambdaAt a sfun)       = LinearLambdaAtF a sfun
-    project (ParenExpr l e)               = ParenExprF l e
-    project (CommentExpr s e)             = CommentExprF s e
-    project (MacroVar l s)                = MacroVarF l s
-
-instance Corecursive (Expression a) where
-    embed (LetF l ds me)                 = Let l ds me
-    embed (VoidLiteralF l)               = VoidLiteral l
-    embed (CallF n is us mps as)         = Call n is us mps as
-    embed (NamedValF n)                  = NamedVal n
-    embed (ListLiteralF l s t es)        = ListLiteral l s t es
-    embed (IfF e e' me)                  = If e e' me
-    embed (UintLitF u)                   = UintLit u
-    embed (IntLitF i)                    = IntLit i
-    embed (FloatLitF f)                  = FloatLit f
-    embed (HexLitF s)                    = HexLit s
-    embed (UnderscoreLitF l)             = UnderscoreLit l
-    embed (LambdaF l lt p e)             = Lambda l lt p e
-    embed (LinearLambdaF l lt p e)       = LinearLambda l lt p e
-    embed (IndexF l n e)                 = Index l n e
-    embed (AccessF l n e)                = Access l n e
-    embed (StringLitF s)                 = StringLit s
-    embed (CharLitF c)                   = CharLit c
-    embed (AddrAtF l e)                  = AddrAt l e
-    embed (ViewAtF l e)                  = ViewAt l e
-    embed (BinaryF op e e')              = Binary op e e'
-    embed (UnaryF op e)                  = Unary op e
-    embed (IfCaseF l arms)               = IfCase l arms
-    embed (CaseF l k e arms)             = Case l k e arms
-    embed (RecordValueF l recs)          = RecordValue l recs
-    embed (BoxRecordValueF l recs)       = RecordValue l recs
-    embed (PrecedeF e e')                = Precede e e'
-    embed (ProofExprF a e e')            = ProofExpr a e e'
-    embed (TypeSignatureF e ty)          = TypeSignature e ty
-    embed (WhereExpF e ds)               = WhereExp e ds
-    embed (TupleExF l es)                = TupleEx l es
-    embed (BoxTupleExF l es)             = BoxTupleEx l es
-    embed (WhileF l e e')                = While l e e'
-    embed (WhileStarF l us t as e e' ty) = WhileStar l us t as e e' ty
-    embed (ForF l e e')                  = For l e e'
-    embed (ForStarF l us t as e e')      = ForStar l us t as e e'
-    embed (ActionsF ds)                  = Actions ds
-    embed (BeginF l e)                   = Begin l e
-    embed (BinListF op es)               = BinList op es
-    embed (PrecedeListF es)              = PrecedeList es
-    embed (FixAtF a s sfun)              = FixAt a s sfun
-    embed (LambdaAtF a sfun)             = LambdaAt a sfun
-    embed (LinearLambdaAtF a sfun)       = LinearLambdaAt a sfun
-    embed (ParenExprF l e)               = ParenExpr l e
-    embed (CommentExprF s e)             = CommentExpr s e
-    embed (MacroVarF l s)                = MacroVar l s
 
 -- | An 'implement' or 'primplmnt' declaration
 data Implementation a = Implement { pos            :: a
diff --git a/src/Language/ATS/Types/Lens.hs b/src/Language/ATS/Types/Lens.hs
--- a/src/Language/ATS/Types/Lens.hs
+++ b/src/Language/ATS/Types/Lens.hs
@@ -64,7 +64,7 @@
 impl f (ProofImpl x y) = ProofImpl x <$> f y
 impl _ x               = pure x
 
-valExpression :: Traversal' (Declaration a) (Expression a)
+valExpression :: Traversal' (Declaration a) (Maybe (Expression a))
 valExpression f (Val a v p e) = Val a v p <$> f e
 valExpression _ x             = pure x
 
diff --git a/test/data/dlist.out b/test/data/dlist.out
new file mode 100644
--- /dev/null
+++ b/test/data/dlist.out
@@ -0,0 +1,9 @@
+typedef dlist(a: t@ype+) = @{ f = List0(a) -> List0(a) }
+
+fn from_list {a:t@ype} (List0(a)) : dlist(a)
+
+fn to_list {a:t@ype} (dlist(a)) : List0(a)
+
+fn singleton {a:t@ype} (a) : dlist(a)
+
+val empty{a:t@ype}: dlist(a) = 
diff --git a/test/data/dlist.sats b/test/data/dlist.sats
new file mode 100644
--- /dev/null
+++ b/test/data/dlist.sats
@@ -0,0 +1,9 @@
+typedef dlist(a: t@ype+) = @{ f = List0(a) -> List0(a) }
+
+fn from_list {a:t@ype} (List0(a)) : dlist(a)
+
+fn to_list {a:t@ype} (dlist(a)) : List0(a)
+
+fn singleton {a:t@ype} (a) : dlist(a)
+
+val empty {a:t@ype} : dlist(a)
diff --git a/test/data/stack.out b/test/data/stack.out
new file mode 100644
--- /dev/null
+++ b/test/data/stack.out
@@ -0,0 +1,38 @@
+%{#
+#include <stdatomic.h>
+%}
+
+// BASIC APPROACH: we want to instead modify an intermediate stack, which will
+// be swapped with whatever pointer using atomic_compare_swap?
+typedef aptr(l: addr) = $extype "_Atomic void**"
+
+absview pf_free(l: addr)
+
+datavtype pointer_t(a: vt@ype) =
+  | pointer_t of node_t(a)
+  | none_t
+and node_t(a: vt@ype) =
+  | node_t of @{ value = [ l : addr | l > null ] (a @ l, pf_free(l) | aptr(l))
+               , next = pointer_t(a)
+               }
+
+vtypedef stack_t(a: vt@ype) = @{ stack_head = pointer_t(a) }
+
+castfn release_stack {a:vt@ype} (stack_t(a)) : void
+
+fun new {a:vt@ype} (&stack_t(a)? >> stack_t(a)) : void
+
+fun {a:vt@ype} push (&stack_t(a) >> stack_t(a), a) : void
+
+fun {a:vt@ype} pop (&stack_t(a) >> _) : Option_vt(a)
+
+fn atomic_store {a:vt@ype}{ l : addr | l > null }(a? @ l | aptr(l), a) : (a @ l | void) =
+  "mac#"
+
+// FIXME: should this return a pf_free?
+fn atomic_load {a:vt@ype}{ l : addr | l > null }(a @ l, pf_free(l) | aptr(l)) : a =
+  "mac#"
+
+fn amalloc {a:vt@ype}{ sz : int | sz == sizeof(a) }(sz : size_t(sz)) :
+  [ l : addr | l > null ] (a? @ l, pf_free(l) | aptr(l)) =
+  "mac#malloc"