diff --git a/bench/Main.hs b/bench/Main.hs
index d89b201..ba1d5de 100644
--- a/bench/Main.hs
+++ b/bench/Main.hs
@@ -7,7 +7,7 @@ import           Test.QuickCheck
 
 -- A couple of functions for checking the output of generators
 progNodes :: Program f -> Int
-progNodes = stmtsNodes . unProgram
+progNodes = stmtsNodes . _programStatements
 
 stmtsNodes :: Statements f -> Int
 stmtsNodes = sum . map stmtNodes . unStatements
@@ -24,7 +24,7 @@ exprNodes (EAppBinOp _ e1 e2) = 1 + exprNodes e1 + exprNodes e2
 exprNodes (EIf e e1 e2)       = 1 + exprNodes e + exprNodes e1 + exprNodes e2
 
 progDepth :: Program f -> Int
-progDepth = stmtsDepth . unProgram
+progDepth = stmtsDepth . _programStatements
 
 stmtsDepth :: Statements f -> Int
 stmtsDepth = maximum . (0:) . map stmtDepth . unStatements
diff --git a/common/TinyLang/Environment.hs b/common/TinyLang/Environment.hs
index aff2f7a..89c856b 100644
--- a/common/TinyLang/Environment.hs
+++ b/common/TinyLang/Environment.hs
@@ -11,6 +11,8 @@ module TinyLang.Environment
     , fromUniques
     , fromVars
     , toUniques
+    , elems
+    , intersection
     ) where
 
 import           TinyLang.Prelude
@@ -58,3 +60,9 @@ fromVars = toEnvBy $ uncurry insertVar
 
 toUniques :: Env a -> [(Unique, a)]
 toUniques = map (first Unique) . IntMap.toList . unEnv
+
+elems :: Env a -> [a]
+elems =  IntMap.elems . unEnv
+
+intersection :: Env a -> Env b -> Env a
+intersection a b = Env $ IntMap.intersection (unEnv a) (unEnv b)
diff --git a/common/TinyLang/Generator.hs b/common/TinyLang/Generator.hs
deleted file mode 100644
index 1bcfa3b..0000000
--- a/common/TinyLang/Generator.hs
+++ /dev/null
@@ -1,69 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-orphans #-}
-
-module TinyLang.Generator
-    (
-     makeVars,
-     defaultVars,
-     arbitraryVar
-    ) where
-
-import           TinyLang.Environment
-import           TinyLang.Var
-
-import qualified Data.IntMap.Strict   as IntMap
-import           Test.QuickCheck
-
-{-|
-  We can't use String as the type of variable names in generators for
-  expressions because then it's probable that the variables occurring
-  in a randomly generated expression will all be distinct, which is
-  unrealistic. Also we have to conform to the concrete syntax, and
-  deal sensibly with Unique IDs in some way.
-
-  To deal with these issues we parameterise the expression generator
-  over a list of Vars, and the variables appearing in the expression
-  will be chosen uniformly from this list using QuickCheck's
-  'elements'.  It's OK to have repeated variables: the more often a
-  variable appears in the list, the more often it's likely to appear
-  in a random expression (but note that repeated Vars should be exactly
-  the same, including the Uniqe ID).
-
-  Variable names should be of the form [a-z][a-z0-9_]* if they're going
-  to be printed and fed to the parser.
--}
-
-type VarName = String
-
--- | A convenience method to convert a list of Strings into a list of
--- Vars. The variables are given unique serial numbers 0,1,2,...,
--- which means that multiple occurrences of the same name will yield
--- different Vars: this may or may not be what you want.
-makeVars :: [VarName] -> [Var]
-makeVars = zipWith (\index name -> Var (Unique index) name) [0..]
-
--- | A list of default variables for convenience.
-defaultVars :: [Var]
-defaultVars = makeVars ["a", "b", "c", "d", "e", "f", "g", "h"]
-
--- | Generator for variables, choosing from the given list.
-arbitraryVar :: [Var] -> Gen Var
-arbitraryVar = elements
-
--- Generates an arbitrary environment that
---
--- 1. likely contains values for some likely small prefix of 'defaultVars'
--- 2. contains values for some sublist of 'defaultVars'
--- 3. contains values for some arbitrary variables
-instance Arbitrary a => Arbitrary (Env a) where
-    arbitrary = do
-        let len = length defaultVars
-            varsToUniques = map (unUnique . _varUniq)
-        prefixSize <- frequency $ map (\i -> (len - i, choose (0, i))) [0 .. len]
-        let preUniques = varsToUniques $ take prefixSize defaultVars
-        defUniques <- varsToUniques <$> sublistOf defaultVars
-        arbUniques <- map abs <$> arbitrary
-        let allUniques = preUniques ++ defUniques ++ arbUniques
-        uniquesWithVars <- traverse (\i -> (,) i <$> arbitrary) allUniques
-        return . Env $ IntMap.fromList uniquesWithVars
-
-    shrink = map (Env . IntMap.fromList) . shrink . IntMap.toList . unEnv
diff --git a/field/TinyLang/Field/Core.hs b/field/TinyLang/Field/Core.hs
index 347a4f2..fe10f50 100644
--- a/field/TinyLang/Field/Core.hs
+++ b/field/TinyLang/Field/Core.hs
@@ -5,6 +5,7 @@ module TinyLang.Field.Core
     , Statements (..)
     ) where
 
+import           Data.Bifunctor
 import           GHC.Generics
 import           Quiet
 
@@ -14,6 +15,15 @@ newtype Statements stmt = Statements { unStatements :: [stmt] }
     deriving (Show) via (Quiet (Statements stmt))
 
 -- | Basic wrapper of program
-newtype Program stmt = Program { unProgram :: Statements stmt }
-    deriving (Generic, Eq, Functor, Foldable, Traversable)
-    deriving (Show) via (Quiet (Program stmt))
+data Program var stmt = Program
+    { _programExts :: [var]
+    , _programStatements :: Statements stmt
+    }
+    deriving (Eq, Foldable, Traversable, Functor)
+
+instance Bifunctor Program where
+    bimap f g (Program exts stmts) = Program (fmap f exts) (fmap g stmts)
+
+-- NOTE:  Adding explicit Show instance to avoid record syntax
+instance (Show var, Show stmt) => Show (Program var stmt) where
+    show (Program exts stmts) = "Program " ++ show exts ++ " " ++ show stmts
diff --git a/field/TinyLang/Field/Evaluator.hs b/field/TinyLang/Field/Evaluator.hs
index 666df3c..4a5a356 100644
--- a/field/TinyLang/Field/Evaluator.hs
+++ b/field/TinyLang/Field/Evaluator.hs
@@ -36,8 +36,6 @@ module TinyLang.Field.Evaluator
     , normStatement
     , normStatements
     , normProgram
-    , instStatement
-    , instExpr
     ) where
 
 import           Prelude                          hiding (div)
@@ -193,7 +191,7 @@ evalBinOp BAt x y = asIntegerEval x >>= fmap (UniConst Bool) . flip atEval y . f
 -- | Evaluate a program
 evalProgram :: (Monad m, Eq f, Field f, AsInteger f)
     => Program f -> EvalT f m ()
-evalProgram = flip evalStatements (pure ()) . unProgram
+evalProgram = flip evalStatements (pure ()) . _programStatements
 
 -- TODO:  Verify whether it is acutally right fold
 evalStatements :: (Monad m, Eq f, Field f, AsInteger f)
@@ -263,7 +261,7 @@ denoteExpr = fmap denoteUniConst . evalExprUni
 -- | A recursive normalizer for programs.
 normProgram :: (Monad m, Eq f, Field f, AsInteger f)
     => Program f -> EvalT f m (Program f)
-normProgram (Program stmts) = normStatements stmts (pure . Program)
+normProgram (Program exts stmts) = normStatements stmts (pure . Program exts)
 
 -- | A recursive normalizer for statements
 normStatements :: (Monad m, Eq f, Field f, AsInteger f)
@@ -314,7 +312,7 @@ normExpr (EAppUnOp op e) = do
     case eN of
         EConst (UniConst _ x) -> EConst <$> evalUnOp op x
         _ -> return $ EAppUnOp op eN
-normExpr(EAppBinOp op e1 e2) = do
+normExpr (EAppBinOp op e1 e2) = do
     e1N <- normExpr e1
     e2N <- normExpr e2
     case (e1N, e2N) of
@@ -323,24 +321,3 @@ normExpr(EAppBinOp op e1 e2) = do
         _ ->
             return $ EAppBinOp op e1N e2N
 
--- | Instantiate some of the variables of a statement with values.
-instStatement :: Monad m => Statement f -> EvalT f m (Statement f)
-instStatement (ELet uniVar def)             = ELet uniVar <$> instExpr def
-instStatement (EAssert expr)                = EAssert <$> instExpr expr
-
-instStatements :: Monad m => Statements f -> EvalT f m (Statements f)
-instStatements = traverse instStatement
-
--- | Instantiate some of the variables of an expression with values.
-instExpr :: Monad m => Expr f a -> EvalT f m (Expr f a)
-instExpr expr@(EConst _) = return expr
-instExpr expr@(EVar uniVar@(UniVar uni var)) = do
-    env <- ask
-    case lookupVar var env of
-        Nothing -> return expr
-        Just (Some uniConst@(UniConst uni' _)) -> do
-            let err = throwError . TypeMismatchEvalError $ TypeMismatch uniVar uniConst
-            withGeqUni uni uni' err $ return $ EConst uniConst
-instExpr (EIf e e1 e2) = EIf <$> instExpr e <*> instExpr e1 <*> instExpr e2
-instExpr (EAppUnOp op e) = EAppUnOp op <$> instExpr e
-instExpr (EAppBinOp op e1 e2) = EAppBinOp op <$> instExpr e1 <*> instExpr e2
diff --git a/field/TinyLang/Field/Generator.hs b/field/TinyLang/Field/Generator.hs
index 4b041a0..dfdd191 100644
--- a/field/TinyLang/Field/Generator.hs
+++ b/field/TinyLang/Field/Generator.hs
@@ -27,6 +27,7 @@ import           TinyLang.Prelude
 
 import           TinyLang.Field.Evaluator
 import           TinyLang.Field.Typed.Core
+import           TinyLang.Field.UniConst          (mkSomeUniVar)
 
 import qualified Data.IntMap.Strict               as IntMap
 import           Data.Kind
@@ -34,7 +35,7 @@ import qualified Data.Vector                      as Vector
 import           QuickCheck.GenT
 import           Test.QuickCheck                  (Arbitrary, Gen, arbitrary,
                                                    arbitrarySizedBoundedIntegral,
-                                                   shrink, shrinkList)
+                                                   shrink, shrinkList, sublistOf)
 import           Test.QuickCheck.Instances.Vector ()
 
 
@@ -65,10 +66,6 @@ uniVars =
     mapMaybe $ forget $ \uniVar@(UniVar uni _) ->
         withGeqUni uni (knownUni @f @a) Nothing $ Just uniVar
 
--- | Choose a variable of a particular type.
-chooseUniVar :: (KnownUni f a, MonadGen m) => Vars f -> m (UniVar f a)
-chooseUniVar = elements . uniVars
-
 -- The next function is concerned with generating fresh variables
 -- for use in let-expressions.  We generate names with a prefix from a-z
 -- and with a fresh drawn from a supply.
@@ -106,23 +103,34 @@ adjustUniquesForVars :: MonadSupply m => Vars f -> m ()
 adjustUniquesForVars =
     supplyFromAtLeast . freeUniqueFoldable . map (forget $ _varUniq . _uniVarVar)
 
--- | The variables used by our generators by default.
-defaultVars :: Vars f
-defaultVars = runSupply $ do
-    let make uni name = Some . UniVar uni <$> freshVar name
-    fieldVars  <- traverse (make Field ) ["x", "y", "z", "p", "q", "r", "s", "t"]
-    boolVars   <- traverse (make Bool  ) ["?a", "?b", "?c", "?d", "?e", "?f", "?g", "?h"]
-    vectorVars <- traverse (make Vector) ["#q", "#r", "#s", "#t", "#u", "#v", "#w"]
-    return $ fieldVars ++ boolVars ++ vectorVars
 
 -- | A wrapper around @UniVar f a@ provided for its @Arbitrary@ instance that allows to generate
 -- variables from the default set of them.
-newtype DefaultUniVar f a = DefaultUniVar
-    { unDefaultUniVar :: UniVar f a
+
+defaultIdents :: [String]
+defaultIdents = concat . transpose $ [fieldIdents, boolIdents, vectorIdents] where
+        fieldIdents   = ["x", "y", "z", "p", "q", "r", "s", "t"]
+        boolIdents    = ["?a", "?b", "?c", "?d", "?e", "?f", "?g", "?h"]
+        vectorIdents  = ["#q", "#r", "#s", "#t", "#u", "#v", "#w"]
+
+newtype Default a = Default
+    { unDefault :: a
     }
+    deriving (Show, Eq, Functor, Foldable, Traversable)
+
+-- type DefaultUniVar f a    = Default (UniVar f a)
+type DefaultVars          = Default [Var]
+type DefaultSomeUniVars f = Default (Vars f)
+
+instance Arbitrary DefaultVars where
+    arbitrary = do
+        vars <- sublistOf $ defaultIdents
+        pure . Default $ runSupply $ traverse freshVar vars
+
+instance Arbitrary (DefaultSomeUniVars f) where
+    arbitrary =  (fmap . fmap . fmap) mkSomeUniVar arbitrary
+
 
-instance KnownUni f a => Arbitrary (DefaultUniVar f a) where
-    arbitrary = DefaultUniVar <$> chooseUniVar defaultVars
 
 -- | Generate a universe and feed it to the continuation.
 withOneOfUnis :: MonadGen m => (forall a. KnownUni f a => Uni f a -> m b) -> m b
@@ -233,9 +241,12 @@ arbitraryBinOpRing = elements [Add, Sub, Mul]
 groundArbitraryFreqs :: (Field f, Arbitrary f, KnownUni f a, MonadGen m)
     => Vars f -> [(Int, m (Expr f a))]
 groundArbitraryFreqs vars =
-    [ (1, EConst <$> arbitraryM)
-    , (2, EVar   <$> chooseUniVar vars)
-    ]
+    -- NOTE:  check if there are available variables in the context
+    case uniVars vars of
+        [] -> [(1, EConst <$> arbitraryM)]
+        uVars -> [ (1, EConst <$> arbitraryM)
+                 , (2, EVar   <$> elements uVars)
+                 ]
 
 newtype SGenT f (m :: Type -> Type) a =
     SGen { unSGenT :: GenT (SupplyT (StateT (Vars f) m)) a }
@@ -288,7 +299,7 @@ boundedArbitraryStmt size
                                let vars' = Some uniVar : vars
                                    size' = size - 1
                                put vars'
-                               ELet uniVar <$> boundedArbitraryExpr vars' size')
+                               ELet uniVar <$> boundedArbitraryExpr vars size')
                      -- Generate a completely random assertion (unlikely to hold)
                      , (1, do
                                vars <- get
@@ -311,6 +322,7 @@ boundedArbitraryStmt size
 boundedArbitraryExpr :: forall m f a. (Field f, Arbitrary f, KnownUni f a, MonadGen m, MonadSupply m)
     => Vars f -> Int -> m (Expr f a)
 boundedArbitraryExpr vars size
+    -- TODO: A case when there are no variables in context
     | size <= 1 = frequency $ groundArbitraryFreqs vars
     | otherwise = frequency everything where
         everything = groundArbitraryFreqs vars ++ expressions ++ comparisons (size `Prelude.div` 2)
@@ -358,7 +370,7 @@ boundedArbitraryExprI
 boundedArbitraryExprI _    size | size <= 1 = EConst <$> arbitraryValI
 boundedArbitraryExprI vars size             = frequency
     [ (1, EConst <$> arbitraryValI)
-    , (0, EVar   <$> chooseUniVar vars)
+    -- , (0, EVar   <$> chooseUniVar vars)
       {- TODO:  Check for Haddock post lts-13.26
          NOTE.  If we allow variables here we won't generally know in
          advance that they'll have integer values, so there
@@ -416,16 +428,35 @@ defaultUniConst =
     where
         uni = knownUni @f @a
 
+-- TODO:  Not sure how to use it effecively yet
+-- genExts :: Statements f -> [Var]
+-- genExts stmts = runSupply $ traverse (freshVar . _varSigName) sigs where
+--     sigs = elems $ progFreeVarSigs (Program mempty stmts)
+
+-- NOTE: We only create closed programs for now
 instance (Field f, Arbitrary f) => Arbitrary (Program f) where
-    arbitrary = Program <$> arbitrary
-    shrink    = fmap Program . shrink . unProgram
+    arbitrary = do
+        exts  <- unDefault <$> arbitrary
+        let someUniVars = fmap mkSomeUniVar exts
+        stmts <- runSGen someUniVars $ sized $ \size -> do
+                     adjustUniquesForVars someUniVars
+                     boundedArbitraryStmts size
+        -- NOTE: we should not use arbitrary instance for Statements f directly,
+        -- as it can generate a statement that contains free variables.
+        pure $ Program exts stmts
+
+    shrink (Program exts stmts) =
+        fmap (uncurry Program) $
+            -- [ (vars', stmts)  | vars'  <- shrinkList (const []) vars ] ++
+            [ (exts , stmts') | stmts' <- shrink stmts ]
 
 instance (Field f, Arbitrary f) => Arbitrary (Statements f) where
-    arbitrary = runSGen vars stmtsGen where
-        vars = defaultVars
-        stmtsGen = sized $ \size -> do
-            adjustUniquesForVars vars
-            boundedArbitraryStmts size
+    arbitrary = do
+        vars <- unDefault <$> arbitrary
+        let stmtsGen = sized $ \size -> do
+                adjustUniquesForVars vars
+                boundedArbitraryStmts size
+        runSGen vars stmtsGen
 
     shrink (Statements stmts) =
             Statements <$> concat
@@ -478,7 +509,7 @@ instance (Field f, Arbitrary f) => Arbitrary (Statement f) where
 
 instance (KnownUni f a, Field f, Arbitrary f) => Arbitrary (Expr f a) where
     arbitrary = runSupplyGenT . sized $ \size -> do
-        let vars = defaultVars
+        vars <- liftGen $ unDefault <$> arbitrary
         adjustUniquesForVars vars
         boundedArbitraryExpr vars size
 
@@ -505,6 +536,13 @@ genEnvFromVarSigs =
     traverse $ \(VarSig _ (uni :: Uni f a)) ->
         Some <$> withKnownUni uni (arbitrary :: Gen (UniConst f a))
 
+genInputEnvFromExts :: (Field f, Arbitrary f) => [Var] -> Gen (Env (SomeUniConst f))
+genInputEnvFromExts vars = fromVars . zip vars <$> consts where
+    consts = for vars $ \ tVar ->
+        case uniOfVar . _varName $ tVar of
+            Some (uni :: Uni f a) ->
+                Some <$> withKnownUni uni (arbitrary :: Gen (UniConst f a))
+
 -- | Generate a random ProgramWithEnv.  Note that you can say things like
 -- "generate (resize 1000 arbitrary :: Gen (ProgramWithEnv F17))" to get bigger
 -- expressions. There's no means provided to generate things over non-default
@@ -512,8 +550,8 @@ genEnvFromVarSigs =
 instance (Field f, Arbitrary f) => Arbitrary (ProgramWithEnv f) where
     arbitrary = do
         prog <- arbitrary
-        vals <- genEnvFromVarSigs . progFreeVarSigs $ prog
+        vals <- genInputEnvFromExts . _programExts $ prog
         return $ ProgramWithEnv prog vals
-    shrink (ProgramWithEnv prog (Env vals)) =
+    shrink (ProgramWithEnv prog vals) =
         flip map (shrink prog) $ \shrunk ->
-            ProgramWithEnv shrunk . Env . IntMap.intersection vals . unEnv $ progFreeVarSigs shrunk
+            ProgramWithEnv shrunk . intersection vals $ progFreeVarSigs shrunk
diff --git a/field/TinyLang/Field/Printer.hs b/field/TinyLang/Field/Printer.hs
index 4f316ef..6f7398d 100644
--- a/field/TinyLang/Field/Printer.hs
+++ b/field/TinyLang/Field/Printer.hs
@@ -78,7 +78,9 @@ stmtsToString :: TextField f => PrintStyle -> (Statements f) -> String
 stmtsToString ps = unlines . (map (stmtToString ps)) . unStatements
 
 progToString :: TextField f => PrintStyle -> Program f -> String
-progToString ps = stmtsToString ps . unProgram
+progToString ps (Program exts stmts) = unlines vars ++ stmtsToString ps stmts
+    where
+        vars = fmap (\ext -> "ext " ++ toStringVar ps ext ++ ";") exts
 
 -- Main function
 exprToString :: TextField f => PrintStyle -> Expr f a -> String
diff --git a/field/TinyLang/Field/Raw/Core.hs b/field/TinyLang/Field/Raw/Core.hs
index 2404fd0..216781e 100644
--- a/field/TinyLang/Field/Raw/Core.hs
+++ b/field/TinyLang/Field/Raw/Core.hs
@@ -9,7 +9,7 @@ module TinyLang.Field.Raw.Core
     , Statement(..)
     , Program
     , pattern C.Program
-    , C.unProgram
+    , C._programStatements
     , Statements
     , pattern C.Statements
     , C.unStatements
@@ -30,7 +30,7 @@ import           Quiet
 type Identifier = String
 
 newtype Var = Var { unVar :: Identifier }
-    deriving (Eq, Generic)
+    deriving (Eq, Generic, Ord)
     deriving (Show) via (Quiet Var)
 
 {-| In our AST we have the following
@@ -50,8 +50,8 @@ statement level; the operations acting on statement level are not necessarily
 mappable over a list of statements.
 -}
 
-type Program v f    = C.Program    (Statement v f)
-type Statements v f = C.Statements (Statement v f)
+type Program v f    = C.Program    v (Statement v f)
+type Statements v f = C.Statements   (Statement v f)
 
 data Statement v f
     = ELet    v          (Expr v f)
diff --git a/field/TinyLang/Field/Raw/Parser.hs b/field/TinyLang/Field/Raw/Parser.hs
index ce256be..eb44a7e 100644
--- a/field/TinyLang/Field/Raw/Parser.hs
+++ b/field/TinyLang/Field/Raw/Parser.hs
@@ -49,6 +49,7 @@ keyword ::=
     "field"
     "bool"
     "vector"
+    "ext"
 @
 
 == Types/Universes
@@ -133,9 +134,6 @@ prefix-op ::=
 
 == Statement
 
-Program are a bit odd at the moment, as they are neither
-expressions nor the usual statements.
-
 @
 statement ::=
     "let" var "=" expr
@@ -143,8 +141,24 @@ statement ::=
     "for" var "=" int-literal "to" int-literal "do" statements "end"
 
 statements ::=
-    (statement (";" statement)*)?
+    (statement ";")*
+@
+
+== Program
+
+A program is a list of external declarations followed by statements.
+
 @
+program ::=
+    ext-decls statements
+
+ext-decls ::=
+    (ext-decl ";")*
+
+ext-decl ::=
+    "ext" var
+@
+
 
 == Operator Precedence
 
@@ -220,6 +234,7 @@ keywords =
     , "for", "do", "end"
     , "if", "then", "else"
     , "bool", "field", "vector"
+    , "ext"
     ]
 
 isKeyword :: String -> Bool
@@ -367,6 +382,12 @@ pStatement =
               <*   keyword "end"
     ]
 
+pExtDecl :: ParserT m Var
+pExtDecl = keyword "ext" *> pVar
+
+pExtDecls :: ParserT m [Var]
+pExtDecls = many (pExtDecl <* symbol ";")
+
 pStatements :: Field f => ParserT m (RawStatements f)
 pStatements =
     choice
@@ -376,7 +397,7 @@ pStatements =
     ]
 
 pProgram :: Field f => ParserT m (RawProgram f)
-pProgram = Program <$> pStatements
+pProgram = Program <$> pExtDecls <*> pStatements
 
 pTop :: Field f => ParserT m (RawProgram f)
 pTop = top pProgram
diff --git a/field/TinyLang/Field/Rename.hs b/field/TinyLang/Field/Rename.hs
index c3f0871..df490c9 100644
--- a/field/TinyLang/Field/Rename.hs
+++ b/field/TinyLang/Field/Rename.hs
@@ -9,9 +9,14 @@ import           TinyLang.Field.Typed.Core
 import           Control.Monad.Cont
 
 renameProgram :: MonadSupply m => Program f -> m (Program f)
-renameProgram (Program stmts) = do
-    stmtsSupplyFromAtLeastFree stmts
-    Program <$> runRenameM (withRenamedStatementsM stmts pure)
+renameProgram prog@(Program exts stmts) = do
+    -- NOTE:  We are not sure if we need to handle Programs with free variables.
+    -- NOTE:  Compiler will run a renaming step before compilation anyways.
+    progSupplyFromAtLeastFree prog
+    runRenameM $
+        runContT (traverse (ContT . withFreshenedVar) exts) $ \ rVars ->
+            withRenamedStatementsM stmts $ \ rStmts ->
+                pure $ Program rVars rStmts
 
 type RenameM = ReaderT (Env Unique) Supply
 
diff --git a/field/TinyLang/Field/Typed/Core.hs b/field/TinyLang/Field/Typed/Core.hs
index e76ad06..431c352 100644
--- a/field/TinyLang/Field/Typed/Core.hs
+++ b/field/TinyLang/Field/Typed/Core.hs
@@ -10,6 +10,7 @@ module TinyLang.Field.Typed.Core
     , KnownUni (..)
     , UniConst (..)
     , UniVar (..)
+    , uniOfVar
     , SomeUniConst
     , SomeUniVar
     , SomeUniExpr
@@ -21,7 +22,8 @@ module TinyLang.Field.Typed.Core
     , C.unStatements
     , Program
     , pattern C.Program
-    , C.unProgram
+    , C._programStatements
+    , C._programExts
     , Expr (..)
     , withUnOpUnis
     , withBinOpUnis
@@ -29,15 +31,9 @@ module TinyLang.Field.Typed.Core
     , withKnownUni
     , VarSig (..)
     , ScopedVarSigs (..)
-    -- , stmtVarSigs
-    -- , stmtFreeVarSigs
-    -- , stmtsFreeVarSigs
     , progFreeVarSigs
-    -- , exprVarSigs
-    -- , exprFreeVarSigs
-    -- , exprSupplyFromAtLeastFree
-    -- , stmtSupplyFromAtLeastFree
-    , stmtsSupplyFromAtLeastFree
+    , progExtVarSigs
+    , progSupplyFromAtLeastFree
     , uniOfExpr
     ) where
 
@@ -51,19 +47,7 @@ import           TinyLang.Field.Existential
 import           TinyLang.Field.UniConst
 import           TinyLang.Var               as Var
 
--- Needed for the sake of symmetry with 'UniConst'.
-data UniVar f a = UniVar
-    { _uniVarUni :: Uni f a
-    , _uniVarVar :: Var
-    } deriving (Show)
-
--- -- TODO: We can can unify the two above by the following data type. Should we do that?
--- data Inhabits f a b = Inhabits
---     { _inhabitsUni :: Uni f a
---     , _inhabitsVal :: b
---     }
 
-type SomeUniVar f = Some (UniVar f)
 type SomeUniExpr f = SomeOf (Uni f) (Expr f)
 
 data UnOp f a b where
@@ -89,8 +73,8 @@ data BinOp f a b c where
     BAt :: BinOp f (AField f) (Vector Bool) Bool
 
 
-type Program    f = C.Program    (Statement f)
-type Statements f = C.Statements (Statement f)
+type Program    f = C.Program    Var (Statement f)
+type Statements f = C.Statements     (Statement f)
 
 data Statement f where
     ELet    :: UniVar f a -> Expr f a -> Statement f
@@ -128,7 +112,6 @@ deriving instance Eq   (BinOp f a b c)
 deriving instance TextField f => Show (Statement f)
 deriving instance TextField f => Show (Expr f a)
 
-
 deriving instance TextField f => Show (SomeUniExpr f)
 
 withUnOpUnis :: UnOp f a b -> (Uni f a -> Uni f b -> c) -> c
@@ -177,16 +160,6 @@ withGeqBinOp binOp1 binOp2 z y =
     withGeqUni resUni1  resUni2  z $
         if binOp1 /= binOp2 then z else y
 
--- This doesn't type check:
---
--- > UniConst _ x1 == UniConst _ x2 = x1 == x2
---
--- because it requires the type of @x1@ and @x2@ to have an @Eq@ instance.
--- We could provide a similar to 'withGeqUni' combinator that can handle this situation,
--- but then it's easier to just pattern match on universes.
-instance Eq f => Eq (UniVar f a) where
-    UniVar _ v1 == UniVar _ v2 = v1 == v2
-
 instance Eq f => Eq (Statement f) where
     ELet (UniVar u1 v1) d1 == ELet (UniVar u2 v2) d2 =
         withGeqUni u1 u2 False $ v1 == v2 && d1 == d2
@@ -233,8 +206,8 @@ data ScopedVarSigs f = ScopedVarSigs
     } deriving (Show)
 
 -- | Add variable to the set of bound variables
-bindVar :: UniVar f a -> State (ScopedVarSigs f) ()
-bindVar (UniVar uni (Var uniq name)) =
+bindUniVar :: UniVar f a -> State (ScopedVarSigs f) ()
+bindUniVar (UniVar uni (Var uniq name)) =
     modify $ \(ScopedVarSigs free bound) ->
         let sig    = VarSig name uni
             bound' = insertUnique uniq sig bound
@@ -266,12 +239,21 @@ isTracked (UniVar uni (Var uniq name)) = do
                                                   , "'"]
                 Nothing -> False
 
+progVS :: Program f -> State (ScopedVarSigs f) ()
+progVS (C.Program exts stmts) = do
+    traverse_ extVS exts
+    traverse_ stmtVS stmts
+
+extVS :: Var -> State (ScopedVarSigs f) ()
+extVS var = case mkSomeUniVar var of
+    Some uniVar -> bindUniVar uniVar
+
 -- | Gather VarSigs for a statement
 stmtVS :: Statement f -> State (ScopedVarSigs f) ()
 stmtVS (EAssert expr)    = exprVS expr
 stmtVS (ELet uniVar def) = do
     exprVS def
-    bindVar uniVar
+    bindUniVar uniVar
 
 -- | Gather VarSigs for an expression
 exprVS :: Expr f a -> State (ScopedVarSigs f) ()
@@ -296,11 +278,16 @@ execSVS s = execState s $ ScopedVarSigs mempty mempty
 progFreeVarSigs :: Program f -> Env (VarSig f)
 progFreeVarSigs = _scopedVarSigsFree . execSVS . traverse_ stmtVS
 
-stmtsSupplyFromAtLeastFree :: MonadSupply m => Statements f -> m ()
-stmtsSupplyFromAtLeastFree =
+-- | Return ext variable signatures for a given program
+progExtVarSigs :: Program f -> Env (VarSig f)
+progExtVarSigs (C.Program exts _) = _scopedVarSigsBound . execSVS . traverse_ extVS $ exts
+
+
+progSupplyFromAtLeastFree :: MonadSupply m => Program f -> m ()
+progSupplyFromAtLeastFree =
     supplyFromAtLeast
     . freeUniqueIntMap
     . unEnv
     . _scopedVarSigsFree
     . execSVS
-    . traverse_ stmtVS
+    . progVS
diff --git a/field/TinyLang/Field/Typed/Parser.hs b/field/TinyLang/Field/Typed/Parser.hs
index 8215731..c94992e 100644
--- a/field/TinyLang/Field/Typed/Parser.hs
+++ b/field/TinyLang/Field/Typed/Parser.hs
@@ -8,9 +8,7 @@ For the new API please refer to "TinyLang.Field.Raw.Parser".
 
 -}
 module TinyLang.Field.Typed.Parser
-    ( parseScopedProgram
-    , parseProgram
-    , parseScopedProgramFrom
+    ( parseProgram
     , parseProgramFrom
     ) where
 
@@ -24,40 +22,21 @@ import           TinyLang.Field.Typed.Core
 import           TinyLang.Field.Typed.TypeChecker
 import           TinyLang.ParseUtils
 
-import qualified Data.IntMap.Strict               as IntMap
-import qualified Data.IntSet                      as IntSet
-import qualified Data.Map.Strict                  as Map
-
-instance TextField f => IsString (Scoped (Program f)) where
-    fromString = either error id . runSupplyT . parseScopedProgram
-
 instance TextField f => IsString (Program f) where
-    fromString = _scopedValue <$> fromString
+    fromString = either error id . runSupplyT . parseProgram
 
 -- | Parse a @String@ and return @Either@ an error message or an @Program@ of some type.
 -- If the result is an error, then return the latest 'Scope', otherwise return the 'Scope'
 -- consisting of all free variables of the expression.
-parseScopedProgramFrom
-    :: forall f m. (MonadError String m, MonadSupply m, TextField f)
-    => String -> String -> m (Scoped (Program f))
-parseScopedProgramFrom fileName str = do
-    progRaw <- parseString (pTop @f) fileName str
-    Scoped scopeTotal progTyped <- typeProgram progRaw
-    progTypedRen <- renameProgram progTyped
-    let indicesFree = IntMap.keysSet . unEnv $ progFreeVarSigs progTypedRen
-        isFree var = unUnique (_varUniq var) `IntSet.member` indicesFree
-        scopeFree = Map.filter isFree scopeTotal
-    return $ Scoped scopeFree progTypedRen
 
 parseProgramFrom
     :: forall f m. (MonadError String m, MonadSupply m, TextField f)
     => String -> String -> m (Program f)
-parseProgramFrom fileName = fmap _scopedValue . parseScopedProgramFrom fileName
+parseProgramFrom fileName str = do
+    progRaw <- parseString (pTop @f) fileName str
+    progTyped <- typeProgram progRaw
+    renameProgram progTyped
 
-parseScopedProgram
-    :: forall f m. (MonadError String m, MonadSupply m, TextField f)
-    => String -> m (Scoped (Program f))
-parseScopedProgram = parseScopedProgramFrom ""
 
 -- | Convenience version of @parseScopedProgram'@ with an empty file name.
 parseProgram
diff --git a/field/TinyLang/Field/Typed/TypeChecker.hs b/field/TinyLang/Field/Typed/TypeChecker.hs
index b4d53bb..79c9890 100644
--- a/field/TinyLang/Field/Typed/TypeChecker.hs
+++ b/field/TinyLang/Field/Typed/TypeChecker.hs
@@ -14,24 +14,13 @@ Potential resources:
 -}
 
 module TinyLang.Field.Typed.TypeChecker
-    ( Scope
-    , MonadScope
-    , Scoped (..)
-    , TypeCheckError
+    ( TypeCheckError
     , MonadTypeError
     , MonadTypeChecker
     , TypeCheckerT(..)
     , TypeChecker
     , runTypeChecker
-    , typeCheck
-    , checkType
     , typeProgram
-    , inferExpr
-    , checkExpr
-    , inferUniVar
-    , checkUniVar
-    , checkStatement
-    , checkProgram
     )
     where
 
@@ -44,107 +33,94 @@ import qualified TinyLang.Field.Typed.Core  as T
 import           TinyLang.Field.UniConst
 import           TinyLang.Var
 
+import           Control.Monad.Cont
+-- import qualified Data.Set                   as Set
 import           Data.Kind
 import qualified Data.Map.Strict            as Map
 import qualified Data.String.Interpolate    as QQ
 
--- | 'Scope' maps names onto 'Var's.
-type Scope = Map String Var
-type MonadScope = MonadState Scope
+{-| == Utility Type Aliases or Constraints
+-}
 
-data Scoped a = Scoped
-    { _scopedScope :: Map String Var
-    , _scopedValue :: a
-    } deriving (Functor, Foldable, Traversable)
+type TypeCheckError        = String
+type MonadTypeError   m    = MonadError TypeCheckError m
+type MonadTypeChecker m f  = ( MonadSupply m
+                             , MonadTypeError m
+                             , MonadReader TyEnv m
+                             )
 
-{-| == Utility Type Aliases or Constraints
+{-| == Type Environments
 -}
 
-type TypeCheckError     = String
-type MonadTypeError   m = MonadError TypeCheckError m
-type MonadTypeChecker m = ( MonadSupply m
-                          , MonadScope m
-                          , MonadTypeError m
-                          )
+-- TODO: Can be parameterised later
+type TyEnv = Map R.Var T.Var
+
 
 {-| @TypeChecker@ Transformer
 -}
-newtype TypeCheckerT e (m :: Type -> Type) a =
-    TypeChecker { runTypeCheckerT :: (ExceptT e (StateT Scope (SupplyT m))) a }
+newtype TypeCheckerT (m :: Type -> Type) a =
+    TypeChecker { runTypeCheckerT :: (ExceptT TypeCheckError (ReaderT TyEnv (SupplyT m))) a }
     deriving newtype ( Monad
                      , Functor
                      , Applicative
-                     , MonadError e
+                     , MonadError TypeCheckError
                      , MonadSupply
-                     , MonadScope
+                     , MonadReader TyEnv
                      )
 
 {-| A simple type checker
 -}
-type TypeChecker = TypeCheckerT TypeCheckError Identity
+type TypeChecker = TypeCheckerT Identity
 
 {-| Run a type checker function. Note that if there are several variables with the same textual name
 then the resulting scope will only contain the last one.
 -}
-runTypeChecker :: (MonadError TypeCheckError m, MonadSupply m) => TypeChecker a -> m (Scoped a)
+runTypeChecker :: (MonadError TypeCheckError m, MonadSupply m) => TypeChecker a -> m a
 runTypeChecker typeChecker =
-    liftSupply (runStateT (runExceptT $ runTypeCheckerT typeChecker) mempty)
-        >>= \(errOrRes, scope) -> Scoped scope <$> liftEither errOrRes
+    liftSupply ( flip runReaderT mempty
+               . runExceptT
+               . runTypeCheckerT
+               $ typeChecker
+               )
+        >>= liftEither
 
 {-|
 -}
-typeCheck
-    :: (MonadError TypeCheckError m, MonadSupply m, TextField f)
-    => R.Expr R.Var f -> m (Scoped (T.SomeUniExpr f))
-typeCheck = runTypeChecker . inferExpr
-
-{-|
--}
-typeProgram
-    :: (MonadError TypeCheckError m, MonadSupply m, TextField f)
-    => R.Program R.Var f -> m (Scoped (T.Program f))
+typeProgram ::
+    (MonadError TypeCheckError m, MonadSupply m, TextField f)
+    => R.Program R.Var f -> m (T.Program f)
 typeProgram = runTypeChecker . checkProgram
 
-{-|
+{-| Add a variable to type environment
 -}
-checkType
-    :: (MonadError TypeCheckError m, MonadSupply m, TextField f, KnownUni f a)
-    => R.Expr R.Var f -> m (Scoped (T.Expr f a))
-checkType = runTypeChecker . checkExpr
-
-{-| Look up a variable name. If we've already seen it, return the corresponding Var;
-otherwise, increase the Unique counter and use it to construct a new Var.
--}
-makeVar :: (MonadSupply m, MonadScope m) => String -> m Var
-makeVar name = do
-    vars <- get
-    case Map.lookup name vars of
-        Just var -> pure var
-        Nothing  -> do
-            var <- freshVar name
-            put $ Map.insert name var vars
-            pure var
-
-mkSomeUniVar :: forall f. T.Var -> T.SomeUniVar f
-mkSomeUniVar var
-    | '?':_ <- _varName var = Some $ T.UniVar Bool   var
-    | '#':_ <- _varName var = Some $ T.UniVar Vector var
-    | otherwise             = Some $ T.UniVar Field  var
+-- NOTE:  At the moment this mimics the old scope
+-- TODO:  Discuss wether we should add an env on top of @withVar@ or not.
+withVar :: (Monad m) => R.Var -> forall r. (T.Var -> TypeCheckerT m r) -> TypeCheckerT m r
+withVar var kont = do
+    tyEnv <- ask
+    case Map.lookup var tyEnv of
+        Just tVar -> kont tVar
+        Nothing -> do
+            tVar <- freshVar . R.unVar $ var
+            local (Map.insert var tVar) $ kont tVar
 
 {-| Type inference for variables
 -}
-inferUniVar
-    :: forall m f. (MonadSupply m, MonadScope m) => R.Var -> m (T.SomeUniVar f)
-inferUniVar = fmap mkSomeUniVar . makeVar . R.unVar
-
+inferUniVar :: (Monad m) => R.Var -> TypeCheckerT m (T.SomeUniVar f)
+inferUniVar var = do
+    tyEnv <- ask
+    case Map.lookup var tyEnv of
+        Just tVar -> pure . mkSomeUniVar $ tVar
+        Nothing -> throwError $ unboundVariable var tyEnv
+       
 {-| Type inference for expressions
 -}
-inferExpr
-    :: forall m f. (MonadTypeChecker m, TextField f)
-    => R.Expr R.Var f -> m (T.SomeUniExpr f)
+inferExpr ::
+    forall m f. (Monad m, TextField f)
+    => R.Expr R.Var f -> TypeCheckerT m (T.SomeUniExpr f)
 inferExpr (R.EConst (Some c@(T.UniConst uni _))) =
     pure $ SomeOf uni $ T.EConst c
-inferExpr (R.EVar   v) = do
+inferExpr (R.EVar v) = do
     Some uniVar@(T.UniVar uni _) <- inferUniVar v
     pure $ SomeOf uni $ T.EVar uniVar
 inferExpr (R.EAppBinOp rBinOp l m) =
@@ -158,18 +134,14 @@ inferExpr (R.EIf l m n) = do
     SomeOf uni tM <- inferExpr m
     tN <- T.withKnownUni uni $ checkExpr n
     pure $ SomeOf uni $ T.EIf tL tM tN
-inferExpr (R.ETypeAnn u m) =
-    case u of
-        Some uni -> T.withKnownUni uni $ SomeOf uni <$> checkExpr m
+inferExpr (R.ETypeAnn (Some uni) m) =
+    T.withKnownUni uni $ SomeOf uni <$> checkExpr m
 
 {-| Mapping from Raw UnOp to Typed UnOp
 -}
-withTypedBinOp
-    :: forall f r.
-       R.BinOp
-    -> (forall a b c. ( KnownUni f a, KnownUni f b, KnownUni f c)
-        => T.BinOp f a b c -> r)
-    -> r
+withTypedBinOp ::
+    forall f r.
+    R.BinOp -> (forall a b c. ( KnownUni f a, KnownUni f b, KnownUni f c) => T.BinOp f a b c -> r) -> r
 withTypedBinOp R.Or  k = k T.Or
 withTypedBinOp R.And k = k T.And
 withTypedBinOp R.Xor k = k T.Xor
@@ -186,33 +158,20 @@ withTypedBinOp R.BAt k = k T.BAt
 
 {-| Mapping from Raw UnOp to Typed UnOp
 -}
-withTypedUnOp
-    :: forall f r.
-       R.UnOp
-    -> (forall a b. (KnownUni f a, KnownUni f b)
-        => T.UnOp f a b -> r)
-    -> r
+withTypedUnOp ::
+    forall f r.
+    R.UnOp -> (forall a b. (KnownUni f a, KnownUni f b) => T.UnOp f a b -> r) -> r
 withTypedUnOp R.Not  k = k T.Not
 withTypedUnOp R.Neq0 k = k T.Neq0
 withTypedUnOp R.Neg  k = k T.Neg
 withTypedUnOp R.Inv  k = k T.Inv
 withTypedUnOp R.Unp  k = k T.Unp
 
-{-| Type checking for variables
--}
-checkUniVar
-    :: forall m f a. (MonadTypeChecker m)
-    => Uni f a -> R.Var -> m (T.UniVar f a)
-checkUniVar uni iden = do
-    Some uniVar@(T.UniVar varUni _) <- inferUniVar iden
-    let uniMismatch = typeMismatch uniVar uni varUni
-    withGeqUniM uni varUni uniMismatch uniVar
-
 {-| Type checking for expressions
 -}
-checkExpr
-    :: forall m f a. (MonadTypeChecker m, TextField f, KnownUni f a)
-    => R.Expr R.Var f -> m (T.Expr f a)
+checkExpr ::
+    forall m f a. (Monad m, TextField f, KnownUni f a)
+    => R.Expr R.Var f -> TypeCheckerT m (T.Expr f a)
 checkExpr (R.EIf l m n) = T.EIf <$> checkExpr l <*> checkExpr m <*> checkExpr n
 checkExpr m = do
     SomeOf mUni tM <- inferExpr m
@@ -220,39 +179,51 @@ checkExpr m = do
     let uniMismatch = typeMismatch tM uni mUni
     withGeqUniM uni mUni uniMismatch tM
 
--- TODO:  Figure how to optimise
-checkProgram
-    :: forall m f. (MonadTypeChecker m, TextField f)
-    => R.Program R.Var f -> m (T.Program f)
-checkProgram (R.Program (R.Statements stmts)) =
-    T.Program . T.Statements <$> foldMapA checkStatement stmts
+checkProgram ::
+    forall m f. (Monad m, TextField f)
+    => R.Program R.Var f -> TypeCheckerT m (T.Program f)
+checkProgram (R.Program exts stmts) =
+    runContT (traverse (ContT . withVar) exts) $ \tVars -> checkStatements stmts (pure . T.Program tVars)
 
+checkStatements ::
+    forall m f. (Monad m , TextField f)
+    => R.Statements R.Var f -> forall r. (T.Statements f -> TypeCheckerT m r) -> TypeCheckerT m r
+checkStatements (R.Statements stmts) kont =
+    runContT (foldMapA (ContT . checkStatement) stmts) $ kont . T.Statements
 
 {-| Type checking judgement for statements of form
 -}
-checkStatement
-    :: forall m f. (MonadTypeChecker m, TextField f)
-    => R.Statement R.Var f -> m [T.Statement f]
-checkStatement (R.ELet var m) = do
-    Some uniVar@(T.UniVar uni _) <- inferUniVar var
-    T.withKnownUni uni $ (:[]) . T.ELet uniVar <$> checkExpr m
-checkStatement (R.EAssert m) =
-    (:[]) . T.EAssert <$> checkExpr m
--- TODO:  Inject var into environment of stmts
-checkStatement (R.EFor var start end stmts) =
-    foldMapA iter [start .. end]
-    where iter i = do
-              tVar <- makeVar $ R.unVar var
-              let uVar = T.UniVar Field tVar
-              tStmts <- foldMapA checkStatement stmts
-              pure $ T.ELet uVar (T.EConst . fromIntegral $ i) : tStmts
+checkStatement ::
+    forall m f. (Monad m , TextField f)
+    => R.Statement R.Var f -> forall r. ([T.Statement f] -> TypeCheckerT m r) -> TypeCheckerT m r
+checkStatement (R.ELet var m) kont =
+    case uniOfVar . R.unVar $ var of
+        Some uni -> do
+                tM <- T.withKnownUni uni $ checkExpr m
+                withVar var $ \ tVar -> kont [T.ELet (UniVar uni tVar) tM]
+checkStatement (R.EAssert m) kont = do
+    tM <- checkExpr m
+    kont [T.EAssert tM]
+checkStatement (R.EFor var start end stmts) kont = do
+    runContT (foldMapA (ContT . iter) [start .. end]) kont where
+        iter i ikont = withVar var $ \ tVar ->
+            checkStatements stmts $ \ (T.Statements tStmts) -> do
+                let uVar = T.UniVar Field tVar
+                ikont $ T.ELet uVar (T.EConst . fromIntegral $ i) : tStmts
 
 {-| Error message for a failed type equality
 -}
-typeMismatch
-    :: forall a b c. (Show a, Show b, Show c)  => a -> b -> c -> TypeCheckError
+typeMismatch ::
+    forall a b c. (Show a, Show b, Show c)
+    => a -> b -> c -> TypeCheckError
 typeMismatch expr expected found =
     [QQ.i|error: Universe mismatch for expression:
            #{show expr}
          Expected: #{show expected}
          Found:    #{show found}|]
+
+unboundVariable :: R.Var -> TyEnv -> TypeCheckError
+unboundVariable var tyEnv =
+    [QQ.i|error: Unbound variable:
+           #{R.unVar var}
+         Environment: #{show tyEnv}|]
diff --git a/field/TinyLang/Field/UniConst.hs b/field/TinyLang/Field/UniConst.hs
index e07c066..e251150 100644
--- a/field/TinyLang/Field/UniConst.hs
+++ b/field/TinyLang/Field/UniConst.hs
@@ -1,12 +1,16 @@
 module TinyLang.Field.UniConst
     ( Uni(..)
     , UniConst(..)
+    , UniVar(..)
     , SomeUniConst
+    , SomeUniVar
     , SomeUni
     , KnownUni
     , knownUni
     , withGeqUni
     , withGeqUniM
+    , mkSomeUniVar
+    , uniOfVar
     ) where
 
 import           Data.Field
@@ -61,14 +65,28 @@ data UniVar f a = UniVar
 --     }
 
 type SomeUniConst f = Some (UniConst f)
-type SomeUni f = Some (Uni f)
+type SomeUniVar f   = Some (UniVar f)
+type SomeUni f      = Some (Uni f)
 
 
 -- instances
 
 deriving instance Show (Uni f a)
 deriving instance Eq   (Uni f a)
+
 deriving instance Show (UniVar f a)
+deriving instance Show (SomeUniVar f)
+
+-- This doesn't type check:
+--
+-- > UniConst _ x1 == UniConst _ x2 = x1 == x2
+--
+-- because it requires the type of @x1@ and @x2@ to have an @Eq@ instance.
+-- We could provide a similar to 'withGeqUni' combinator that can handle this situation,
+-- but then it's easier to just pattern match on universes.
+instance Eq f => Eq (UniVar f a) where
+    UniVar _ v1 == UniVar _ v2 = v1 == v2
+
 
 mapUniConst :: (a -> a) -> UniConst f a -> UniConst f a
 mapUniConst f (UniConst uni x) = UniConst uni $ f x
@@ -130,3 +148,13 @@ instance Eq f => Eq (UniConst f a) where
     UniConst Bool   bool1 == UniConst Bool   bool2 = bool1 == bool2
     UniConst Field  el1   == UniConst Field  el2   = el1 == el2
     UniConst Vector vec1  == UniConst Vector vec2  = vec1 == vec2
+
+uniOfVar :: forall f. String -> SomeUni f
+uniOfVar name
+    | '?':_ <- name = Some Bool
+    | '#':_ <- name = Some Vector
+    | otherwise     = Some Field
+
+mkSomeUniVar :: forall f. Var -> SomeUniVar f
+mkSomeUniVar var = case uniOfVar . _varName $ var of
+                       Some uni -> Some $ UniVar uni var
diff --git a/hie.yaml b/hie.yaml
new file mode 100644
index 0000000..07d9eab
--- /dev/null
+++ b/hie.yaml
@@ -0,0 +1,12 @@
+cradle:
+  stack:
+    - path: "library"
+      component: "tiny-lang:lib"
+    - path: "common"
+      component: "tiny-lang:lib"
+    - path: "field"
+      component: "tiny-lang:lib"
+    - path: "./test"
+      component: "tiny-lang:tiny-lang-test"
+    - path: "./bench"
+      component: "tiny-lang:bench-generators"
diff --git a/test/Field/Raw/golden/00-bool-literals.golden b/test/Field/Raw/golden/00-bool-literals.golden
index 29d1b5b..361d2dc 100644
--- a/test/Field/Raw/golden/00-bool-literals.golden
+++ b/test/Field/Raw/golden/00-bool-literals.golden
@@ -1 +1 @@
-Program (Statements [ELet (Var "?false") (EConst (Some (UniConst Bool False))),ELet (Var "?true") (EConst (Some (UniConst Bool True)))])
\ No newline at end of file
+Program [] Statements [ELet (Var "?false") (EConst (Some (UniConst Bool False))),ELet (Var "?true") (EConst (Some (UniConst Bool True)))]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/01-field-literals.golden b/test/Field/Raw/golden/01-field-literals.golden
index 6840a71..ef66e7f 100644
--- a/test/Field/Raw/golden/01-field-literals.golden
+++ b/test/Field/Raw/golden/01-field-literals.golden
@@ -1 +1 @@
-Program (Statements [ELet (Var "zero") (EConst (Some 0)),ELet (Var "one") (EConst (Some 1)),ELet (Var "two") (EConst (Some 2)),ELet (Var "half") (EAppBinOp Div (EConst (Some 1)) (EConst (Some 2))),ELet (Var "third") (EAppBinOp Div (EConst (Some 1)) (EConst (Some 3)))])
\ No newline at end of file
+Program [] Statements [ELet (Var "zero") (EConst (Some 0)),ELet (Var "one") (EConst (Some 1)),ELet (Var "two") (EConst (Some 2)),ELet (Var "half") (EAppBinOp Div (EConst (Some 1)) (EConst (Some 2))),ELet (Var "third") (EAppBinOp Div (EConst (Some 1)) (EConst (Some 3)))]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/02-vector-literals.golden b/test/Field/Raw/golden/02-vector-literals.golden
index a18193a..28f346d 100644
--- a/test/Field/Raw/golden/02-vector-literals.golden
+++ b/test/Field/Raw/golden/02-vector-literals.golden
@@ -1 +1 @@
-Program (Statements [ELet (Var "#one") (EConst (Some (UniConst Vector [True]))),ELet (Var "#two") (EConst (Some (UniConst Vector [True,False]))),ELet (Var "#three") (EConst (Some (UniConst Vector [True,False,True]))),ELet (Var "#four") (EConst (Some (UniConst Vector [True,False,True,False])))])
\ No newline at end of file
+Program [] Statements [ELet (Var "#one") (EConst (Some (UniConst Vector [True]))),ELet (Var "#two") (EConst (Some (UniConst Vector [True,False]))),ELet (Var "#three") (EConst (Some (UniConst Vector [True,False,True]))),ELet (Var "#four") (EConst (Some (UniConst Vector [True,False,True,False])))]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/03-lexer-whitespace.golden b/test/Field/Raw/golden/03-lexer-whitespace.golden
index 7be2c07..fab2fcc 100644
--- a/test/Field/Raw/golden/03-lexer-whitespace.golden
+++ b/test/Field/Raw/golden/03-lexer-whitespace.golden
@@ -1 +1 @@
-Program (Statements [ELet (Var "x") (EAppBinOp Div (EConst (Some 1)) (EConst (Some 2)))])
\ No newline at end of file
+Program [] Statements [ELet (Var "x") (EAppBinOp Div (EConst (Some 1)) (EConst (Some 2)))]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/04-lexer-whitespace.golden b/test/Field/Raw/golden/04-lexer-whitespace.golden
index fb1b82b..a595e5c 100644
--- a/test/Field/Raw/golden/04-lexer-whitespace.golden
+++ b/test/Field/Raw/golden/04-lexer-whitespace.golden
@@ -1 +1 @@
-Program (Statements [EAssert (EConst (Some (UniConst Bool True)))])
\ No newline at end of file
+Program [] Statements [EAssert (EConst (Some (UniConst Bool True)))]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/05-lexer-whitespace.golden b/test/Field/Raw/golden/05-lexer-whitespace.golden
index 68f049a..fd4796c 100644
--- a/test/Field/Raw/golden/05-lexer-whitespace.golden
+++ b/test/Field/Raw/golden/05-lexer-whitespace.golden
@@ -1 +1 @@
-Program (Statements [EFor (Var "i") 0 100 (Statements [EAssert (EConst (Some (UniConst Bool True)))]),EAssert (EConst (Some (UniConst Bool True)))])
\ No newline at end of file
+Program [] Statements [EFor (Var "i") 0 100 (Statements [EAssert (EConst (Some (UniConst Bool True)))]),EAssert (EConst (Some (UniConst Bool True)))]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/06-operator-precedence.field b/test/Field/Raw/golden/06-operator-precedence.field
index 7d6d65c..7d0ab46 100644
--- a/test/Field/Raw/golden/06-operator-precedence.field
+++ b/test/Field/Raw/golden/06-operator-precedence.field
@@ -1,3 +1,12 @@
+ext a;
+ext b;
+ext c;
+ext d;
+ext e;
+ext f;
+ext g;
+ext h;
+
 assert
 	  a * b
 	- c * d
@@ -10,4 +19,4 @@ xor
     >=
 	  e / f
 	+ g / h
-;
\ No newline at end of file
+;
diff --git a/test/Field/Raw/golden/06-operator-precedence.golden b/test/Field/Raw/golden/06-operator-precedence.golden
index d2ecb39..f75c781 100644
--- a/test/Field/Raw/golden/06-operator-precedence.golden
+++ b/test/Field/Raw/golden/06-operator-precedence.golden
@@ -1 +1 @@
-Program (Statements [EAssert (EAppBinOp Xor (EAppBinOp FEq (EAppBinOp Sub (EAppBinOp Mul (EVar (Var "a")) (EVar (Var "b"))) (EAppBinOp Mul (EVar (Var "c")) (EVar (Var "d")))) (EAppBinOp Add (EAppBinOp Div (EVar (Var "e")) (EVar (Var "f"))) (EAppBinOp Div (EVar (Var "g")) (EVar (Var "h"))))) (EAppBinOp FGe (EAppBinOp Sub (EAppBinOp Mul (EVar (Var "a")) (EVar (Var "b"))) (EAppBinOp Mul (EVar (Var "c")) (EVar (Var "d")))) (EAppBinOp Add (EAppBinOp Div (EVar (Var "e")) (EVar (Var "f"))) (EAppBinOp Div (EVar (Var "g")) (EVar (Var "h"))))))])
\ No newline at end of file
+Program [Var "a",Var "b",Var "c",Var "d",Var "e",Var "f",Var "g",Var "h"] Statements [EAssert (EAppBinOp Xor (EAppBinOp FEq (EAppBinOp Sub (EAppBinOp Mul (EVar (Var "a")) (EVar (Var "b"))) (EAppBinOp Mul (EVar (Var "c")) (EVar (Var "d")))) (EAppBinOp Add (EAppBinOp Div (EVar (Var "e")) (EVar (Var "f"))) (EAppBinOp Div (EVar (Var "g")) (EVar (Var "h"))))) (EAppBinOp FGe (EAppBinOp Sub (EAppBinOp Mul (EVar (Var "a")) (EVar (Var "b"))) (EAppBinOp Mul (EVar (Var "c")) (EVar (Var "d")))) (EAppBinOp Add (EAppBinOp Div (EVar (Var "e")) (EVar (Var "f"))) (EAppBinOp Div (EVar (Var "g")) (EVar (Var "h"))))))]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/07-operator-precedence.field b/test/Field/Raw/golden/07-operator-precedence.field
index 642d66f..8d2d9a6 100644
--- a/test/Field/Raw/golden/07-operator-precedence.field
+++ b/test/Field/Raw/golden/07-operator-precedence.field
@@ -1,3 +1,6 @@
+ext a;
+ext b;
+
 assert
 (neg a and b) <= (neg (a and b))
-;
\ No newline at end of file
+;
diff --git a/test/Field/Raw/golden/07-operator-precedence.golden b/test/Field/Raw/golden/07-operator-precedence.golden
index 7ad8dde..30d8c79 100644
--- a/test/Field/Raw/golden/07-operator-precedence.golden
+++ b/test/Field/Raw/golden/07-operator-precedence.golden
@@ -1 +1 @@
-Program (Statements [EAssert (EAppBinOp FLe (EAppBinOp And (EAppUnOp Neg (EVar (Var "a"))) (EVar (Var "b"))) (EAppUnOp Neg (EAppBinOp And (EVar (Var "a")) (EVar (Var "b")))))])
\ No newline at end of file
+Program [Var "a",Var "b"] Statements [EAssert (EAppBinOp FLe (EAppBinOp And (EAppUnOp Neg (EVar (Var "a"))) (EVar (Var "b"))) (EAppUnOp Neg (EAppBinOp And (EVar (Var "a")) (EVar (Var "b")))))]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/08-operator-precedence.field b/test/Field/Raw/golden/08-operator-precedence.field
index 3a579ed..daa1837 100644
--- a/test/Field/Raw/golden/08-operator-precedence.field
+++ b/test/Field/Raw/golden/08-operator-precedence.field
@@ -1,4 +1,8 @@
+ext a;
+ext b;
+ext c;
+
 assert
     a + b [c] == a + (b [c])
 and a + b [c] <= (a + b) [c]
-;
\ No newline at end of file
+;
diff --git a/test/Field/Raw/golden/08-operator-precedence.golden b/test/Field/Raw/golden/08-operator-precedence.golden
index 775a093..3d75b7a 100644
--- a/test/Field/Raw/golden/08-operator-precedence.golden
+++ b/test/Field/Raw/golden/08-operator-precedence.golden
@@ -1 +1 @@
-Program (Statements [EAssert (EAppBinOp And (EAppBinOp FEq (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b")))) (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b"))))) (EAppBinOp FLe (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b")))) (EAppBinOp BAt (EVar (Var "c")) (EAppBinOp Add (EVar (Var "a")) (EVar (Var "b"))))))])
\ No newline at end of file
+Program [Var "a",Var "b",Var "c"] Statements [EAssert (EAppBinOp And (EAppBinOp FEq (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b")))) (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b"))))) (EAppBinOp FLe (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b")))) (EAppBinOp BAt (EVar (Var "c")) (EAppBinOp Add (EVar (Var "a")) (EVar (Var "b"))))))]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/09-for-loop.golden b/test/Field/Raw/golden/09-for-loop.golden
index 3e3eb4c..5435347 100644
--- a/test/Field/Raw/golden/09-for-loop.golden
+++ b/test/Field/Raw/golden/09-for-loop.golden
@@ -1 +1 @@
-Program (Statements [EFor (Var "i") 0 0 (Statements [])])
\ No newline at end of file
+Program [] Statements [EFor (Var "i") 0 0 (Statements [])]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/10-for-loop.golden b/test/Field/Raw/golden/10-for-loop.golden
index 360f494..ab01183 100644
--- a/test/Field/Raw/golden/10-for-loop.golden
+++ b/test/Field/Raw/golden/10-for-loop.golden
@@ -1 +1 @@
-Program (Statements [EFor (Var "i") 1 2 (Statements [ELet (Var "i'") (EVar (Var "i")),EFor (Var "j") 2 3 (Statements [ELet (Var "k") (EAppBinOp Mul (EVar (Var "i")) (EVar (Var "j"))),EAssert (EAppBinOp FEq (EVar (Var "k")) (EAppBinOp Mul (EVar (Var "i'")) (EVar (Var "j"))))]),ELet (Var "p") (EVar (Var "i")),EFor (Var "l") 1 2 (Statements [ELet (Var "p") (EAppBinOp Mul (EVar (Var "p")) (EVar (Var "l")))])])])
\ No newline at end of file
+Program [] Statements [EFor (Var "i") 1 2 (Statements [ELet (Var "i'") (EVar (Var "i")),EFor (Var "j") 2 3 (Statements [ELet (Var "k") (EAppBinOp Mul (EVar (Var "i")) (EVar (Var "j"))),EAssert (EAppBinOp FEq (EVar (Var "k")) (EAppBinOp Mul (EVar (Var "i'")) (EVar (Var "j"))))]),ELet (Var "p") (EVar (Var "i")),EFor (Var "l") 1 2 (Statements [ELet (Var "p") (EAppBinOp Mul (EVar (Var "p")) (EVar (Var "l")))])])]
\ No newline at end of file
diff --git a/test/Field/Raw/golden/11-everything.field b/test/Field/Raw/golden/11-everything.field
index 851ad35..49e2f53 100644
--- a/test/Field/Raw/golden/11-everything.field
+++ b/test/Field/Raw/golden/11-everything.field
@@ -1,13 +1,19 @@
+ext e;
+ext ?e;
+ext #e;
+
 let ?a = T;
 let ?b = F;
 let #v = {T, F, T};
 let ?or = ?a or ?b;
+let ?ore = ?a or ?e;
 let ?and = ?or or ?b;
 let ?xor = ?and or ?or;
 let f = 0;
 let g = 1;
 let h = 2;
 let ?feq = g == f;
+let ?feqe = e == f;
 let ?fle = h <= f;
 let ?flt = f < g;
 let ?fge = g >= h;
@@ -17,6 +23,7 @@ let sub = g - h;
 let mul = h * f;
 let div = f / g;
 let ?bat = #v[f];
+let ?bate = #e[f];
 let ?not = not ?a;
 let ?neq0 = neq0 f;
 let neg' = neg g;
@@ -28,4 +35,4 @@ for j = 0 to 2 do end;
 let ?if = if T then T else T;
 let asf = 1 : field;
 let ?as = T : bool;
-let #as = { T } : vector;
\ No newline at end of file
+let #as = { T } : vector;
diff --git a/test/Field/Raw/golden/11-everything.golden b/test/Field/Raw/golden/11-everything.golden
index 9602863..fe6bdf3 100644
--- a/test/Field/Raw/golden/11-everything.golden
+++ b/test/Field/Raw/golden/11-everything.golden
@@ -1 +1 @@
-Program (Statements [ELet (Var "?a") (EConst (Some (UniConst Bool True))),ELet (Var "?b") (EConst (Some (UniConst Bool False))),ELet (Var "#v") (EConst (Some (UniConst Vector [True,False,True]))),ELet (Var "?or") (EAppBinOp Or (EVar (Var "?a")) (EVar (Var "?b"))),ELet (Var "?and") (EAppBinOp Or (EVar (Var "?or")) (EVar (Var "?b"))),ELet (Var "?xor") (EAppBinOp Or (EVar (Var "?and")) (EVar (Var "?or"))),ELet (Var "f") (EConst (Some 0)),ELet (Var "g") (EConst (Some 1)),ELet (Var "h") (EConst (Some 2)),ELet (Var "?feq") (EAppBinOp FEq (EVar (Var "g")) (EVar (Var "f"))),ELet (Var "?fle") (EAppBinOp FLe (EVar (Var "h")) (EVar (Var "f"))),ELet (Var "?flt") (EAppBinOp FLt (EVar (Var "f")) (EVar (Var "g"))),ELet (Var "?fge") (EAppBinOp FGe (EVar (Var "g")) (EVar (Var "h"))),ELet (Var "?fgt") (EAppBinOp FGt (EVar (Var "h")) (EVar (Var "f"))),ELet (Var "add") (EAppBinOp Add (EVar (Var "f")) (EVar (Var "g"))),ELet (Var "sub") (EAppBinOp Sub (EVar (Var "g")) (EVar (Var "h"))),ELet (Var "mul") (EAppBinOp Mul (EVar (Var "h")) (EVar (Var "f"))),ELet (Var "div") (EAppBinOp Div (EVar (Var "f")) (EVar (Var "g"))),ELet (Var "?bat") (EAppBinOp BAt (EVar (Var "f")) (EVar (Var "#v"))),ELet (Var "?not") (EAppUnOp Not (EVar (Var "?a"))),ELet (Var "?neq0") (EAppUnOp Neq0 (EVar (Var "f"))),ELet (Var "neg'") (EAppUnOp Neg (EVar (Var "g"))),ELet (Var "inv'") (EAppUnOp Inv (EVar (Var "h"))),ELet (Var "#unpack") (EAppUnOp Unp (EVar (Var "h"))),ELet (Var "?let") (EConst (Some (UniConst Bool True))),EAssert (EConst (Some (UniConst Bool True))),EFor (Var "j") 0 2 (Statements []),ELet (Var "?if") (EIf (EConst (Some (UniConst Bool True))) (EConst (Some (UniConst Bool True))) (EConst (Some (UniConst Bool True)))),ELet (Var "asf") (ETypeAnn (Some Field) (EConst (Some 1))),ELet (Var "?as") (ETypeAnn (Some Bool) (EConst (Some (UniConst Bool True)))),ELet (Var "#as") (ETypeAnn (Some Vector) (EConst (Some (UniConst Vector [True]))))])
\ No newline at end of file
+Program [Var "e",Var "?e",Var "#e"] Statements [ELet (Var "?a") (EConst (Some (UniConst Bool True))),ELet (Var "?b") (EConst (Some (UniConst Bool False))),ELet (Var "#v") (EConst (Some (UniConst Vector [True,False,True]))),ELet (Var "?or") (EAppBinOp Or (EVar (Var "?a")) (EVar (Var "?b"))),ELet (Var "?ore") (EAppBinOp Or (EVar (Var "?a")) (EVar (Var "?e"))),ELet (Var "?and") (EAppBinOp Or (EVar (Var "?or")) (EVar (Var "?b"))),ELet (Var "?xor") (EAppBinOp Or (EVar (Var "?and")) (EVar (Var "?or"))),ELet (Var "f") (EConst (Some 0)),ELet (Var "g") (EConst (Some 1)),ELet (Var "h") (EConst (Some 2)),ELet (Var "?feq") (EAppBinOp FEq (EVar (Var "g")) (EVar (Var "f"))),ELet (Var "?feqe") (EAppBinOp FEq (EVar (Var "e")) (EVar (Var "f"))),ELet (Var "?fle") (EAppBinOp FLe (EVar (Var "h")) (EVar (Var "f"))),ELet (Var "?flt") (EAppBinOp FLt (EVar (Var "f")) (EVar (Var "g"))),ELet (Var "?fge") (EAppBinOp FGe (EVar (Var "g")) (EVar (Var "h"))),ELet (Var "?fgt") (EAppBinOp FGt (EVar (Var "h")) (EVar (Var "f"))),ELet (Var "add") (EAppBinOp Add (EVar (Var "f")) (EVar (Var "g"))),ELet (Var "sub") (EAppBinOp Sub (EVar (Var "g")) (EVar (Var "h"))),ELet (Var "mul") (EAppBinOp Mul (EVar (Var "h")) (EVar (Var "f"))),ELet (Var "div") (EAppBinOp Div (EVar (Var "f")) (EVar (Var "g"))),ELet (Var "?bat") (EAppBinOp BAt (EVar (Var "f")) (EVar (Var "#v"))),ELet (Var "?bate") (EAppBinOp BAt (EVar (Var "f")) (EVar (Var "#e"))),ELet (Var "?not") (EAppUnOp Not (EVar (Var "?a"))),ELet (Var "?neq0") (EAppUnOp Neq0 (EVar (Var "f"))),ELet (Var "neg'") (EAppUnOp Neg (EVar (Var "g"))),ELet (Var "inv'") (EAppUnOp Inv (EVar (Var "h"))),ELet (Var "#unpack") (EAppUnOp Unp (EVar (Var "h"))),ELet (Var "?let") (EConst (Some (UniConst Bool True))),EAssert (EConst (Some (UniConst Bool True))),EFor (Var "j") 0 2 (Statements []),ELet (Var "?if") (EIf (EConst (Some (UniConst Bool True))) (EConst (Some (UniConst Bool True))) (EConst (Some (UniConst Bool True)))),ELet (Var "asf") (ETypeAnn (Some Field) (EConst (Some 1))),ELet (Var "?as") (ETypeAnn (Some Bool) (EConst (Some (UniConst Bool True)))),ELet (Var "#as") (ETypeAnn (Some Vector) (EConst (Some (UniConst Vector [True]))))]
\ No newline at end of file
diff --git a/test/Field/Renaming.hs b/test/Field/Renaming.hs
index 966e6d7..dc15ea6 100644
--- a/test/Field/Renaming.hs
+++ b/test/Field/Renaming.hs
@@ -7,17 +7,14 @@
 
 module Field.Renaming
     ( test_free_variables
-    , test_renaming
     ) where
 
 -- import           TinyLang.Prelude
 
 import           TinyLang.Field.Typed.Core
-import           TinyLang.Field.Typed.Parser
-import           TinyLang.Field.Rename
-import           TinyLang.Field.Printer
+-- NOTE:  Importing IsString Typed.Core
+import           TinyLang.Field.Typed.Parser ()
 
-import qualified Data.String.Interpolate.IsString as QQ
 import           Test.Tasty
 import           Test.Tasty.HUnit
 
@@ -25,29 +22,29 @@ test_free_variables :: TestTree
 test_free_variables = testGroup "free variables"
     [   testGroup "let binding"
         [ testCase "should not bind variable before" $
-            assertNonEmptyEnv $ freeVars "assert x == 1; let x = 1;"
+            assertNonEmptyEnv $ freeVars "ext x; assert x == 1; let x = 1;"
         , testCase "should not bind variable in the definition" $
-            assertNonEmptyEnv $ freeVars "let x = x;"
-        , testCase "shoud bind its variable after" $
+            assertNonEmptyEnv $ freeVars "ext x; let x = x;"
+        , testCase "should bind its variable after" $
             emptyEnv @=? freeVars "let x = 1; assert x == 1;"
         ]
     ,   testGroup "assert statement"
         [ testCase "should make variable free" $
-            assertNonEmptyEnv $ freeVars "assert ?x;"
+            assertNonEmptyEnv $ freeVars "ext ?x; assert ?x;"
         ]
     ,   testGroup "for loop"
         [ testCase "should not bind variable before" $
-            assertNonEmptyEnv $ freeVars "assert x == 1; for x = 0 to 0 do end;"
+            assertNonEmptyEnv $ freeVars "ext x; assert x == 1; for x = 0 to 0 do end;"
         , testCase "shoud bind its variable in body" $
             emptyEnv @=? freeVars "for x = 0 to 0 do assert x == 0; end;"
         , testCase "should bind its variable after body" $
-            emptyEnv @=? freeVars "for x = 0 to 0 do end; assert x == 1;"
+            emptyEnv @=? freeVars "ext x; for x = 0 to 0 do end; assert x == 1;"
         ]
     ] where
         freeVars = progFreeVarSigs @(AField Rational)
         emptyEnv = Env mempty
         assertNonEmptyEnv = assertBool "set of free vars should not be empty" . (emptyEnv /=)
 
--- TODO:  Add more tests
-test_renaming :: TestTree
-test_renaming = testGroup "renamings" []
+-- -- TODO:  Add more tests
+-- test_renaming :: TestTree
+-- test_renaming = testGroup "renamings" []
diff --git a/test/Field/Textual.hs b/test/Field/Textual.hs
index 1b1b331..0dbef75 100644
--- a/test/Field/Textual.hs
+++ b/test/Field/Textual.hs
@@ -72,33 +72,33 @@ data Binding f = forall a. Binding (UniVar f a) (Expr f a)
 
 deriving instance TextField f => Show (Binding f)
 
-instance (Field f, Arbitrary f) => Arbitrary (Binding f) where
-    arbitrary =
-        withOneOfUnis $ \(_ :: Uni f a) ->
-            Binding @f @a . unDefaultUniVar <$> arbitrary <*> arbitrary
-
-prop_nested_let
-    :: forall f. (Eq f, TextField f)
-    => [Binding f] -> Either String ()
-prop_nested_let bindings = prop_prog_roundtrip $ Program $ Statements $ map bind bindings where
-    bind :: Binding f -> Statement f
-    bind (Binding uniVar body) = ELet uniVar body
+-- instance (Field f, Arbitrary f) => Arbitrary (Binding f) where
+--     arbitrary =
+--         withOneOfUnis $ \(_ :: Uni f a) ->
+--             Binding @f @a . unDefault <$> arbitrary <*> arbitrary
+
+-- prop_nested_let
+--     :: forall f. (Eq f, TextField f)
+--     => [Binding f] -> Either String ()
+-- prop_nested_let bindings = prop_prog_roundtrip $ Program mempty $ Statements $ map bind bindings where
+--     bind :: Binding f -> Statement f
+--     bind (Binding uniVar body) = ELet uniVar body
 
 test_checkParseGeneric :: TestTree
 test_checkParseGeneric =
     testProperty "checkParseGeneric2" $
         withMaxSuccess 1000 . property $ prop_prog_roundtrip @JJ.F
 
-test_checkParseNestedLets :: TestTree
-test_checkParseNestedLets =
-    testProperty "checkParseNestedLets" $
-        withMaxSuccess 100 . property $ prop_nested_let @F17
+-- test_checkParseNestedLets :: TestTree
+-- test_checkParseNestedLets =
+--     testProperty "checkParseNestedLets" $
+--         withMaxSuccess 100 . property $ prop_nested_let @F17
 
 test_printerParserRoundtrip :: TestTree
 test_printerParserRoundtrip =
     testGroup "printerParserRoundtrip"
         [ test_checkParseGeneric
-        , test_checkParseNestedLets
+        -- , test_checkParseNestedLets
         ]
 
 test_textual :: TestTree
diff --git a/test/Field/Typed/golden/00-constants.golden b/test/Field/Typed/golden/00-constants.golden
index ce0b187..5b46535 100644
--- a/test/Field/Typed/golden/00-constants.golden
+++ b/test/Field/Typed/golden/00-constants.golden
@@ -1 +1 @@
-Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?true_4}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?false_5}) (EConst (UniConst Bool False)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_6}) (EConst 0),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_7}) (EConst (UniConst Vector [True]))])
\ No newline at end of file
+Program [] Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?true_4}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?false_5}) (EConst (UniConst Bool False)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_6}) (EConst 0),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_7}) (EConst (UniConst Vector [True]))]
\ No newline at end of file
diff --git a/test/Field/Typed/golden/01-variables.field b/test/Field/Typed/golden/01-variables.field
index 56820ab..96cadd1 100644
--- a/test/Field/Typed/golden/01-variables.field
+++ b/test/Field/Typed/golden/01-variables.field
@@ -1,3 +1,6 @@
+ext i;
+ext ?i;
+ext #i;
 let ?bool    = ?i;
 let field'   = i;
-let #vector  = #i;
\ No newline at end of file
+let #vector  = #i;
diff --git a/test/Field/Typed/golden/01-variables.golden b/test/Field/Typed/golden/01-variables.golden
index 76a6524..5b47dd9 100644
--- a/test/Field/Typed/golden/01-variables.golden
+++ b/test/Field/Typed/golden/01-variables.golden
@@ -1 +1 @@
-Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bool_6}) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?i_1})),ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_7}) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = i_3})),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_8}) (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #i_5}))])
\ No newline at end of file
+Program [i_6,?i_7,#i_8] Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bool_9}) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?i_7})),ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_10}) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = i_6})),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_11}) (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #i_8}))]
\ No newline at end of file
diff --git a/test/Field/Typed/golden/02-binops.golden b/test/Field/Typed/golden/02-binops.golden
index 36a2b1e..7652b23 100644
--- a/test/Field/Typed/golden/02-binops.golden
+++ b/test/Field/Typed/golden/02-binops.golden
@@ -1 +1 @@
-Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_13}) (EAppBinOp Or (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_14}) (EAppBinOp And (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?xor_15}) (EAppBinOp Xor (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?feq_16}) (EAppBinOp FEq (EConst 0) (EConst 0)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fle_17}) (EAppBinOp FLe (EConst 0) (EConst 1)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?flt_18}) (EAppBinOp FLt (EConst 0) (EConst 1)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fge_19}) (EAppBinOp FGe (EConst 1) (EConst 0)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fgt_20}) (EAppBinOp FGt (EConst 1) (EConst 0)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = add_21}) (EAppBinOp Add (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = sub_22}) (EAppBinOp Sub (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = mul_23}) (EAppBinOp Mul (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = div_24}) (EAppBinOp Div (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bat_25}) (EAppBinOp BAt (EConst 0) (EConst (UniConst Vector [True])))])
\ No newline at end of file
+Program [] Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_13}) (EAppBinOp Or (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_14}) (EAppBinOp And (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?xor_15}) (EAppBinOp Xor (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?feq_16}) (EAppBinOp FEq (EConst 0) (EConst 0)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fle_17}) (EAppBinOp FLe (EConst 0) (EConst 1)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?flt_18}) (EAppBinOp FLt (EConst 0) (EConst 1)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fge_19}) (EAppBinOp FGe (EConst 1) (EConst 0)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fgt_20}) (EAppBinOp FGt (EConst 1) (EConst 0)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = add_21}) (EAppBinOp Add (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = sub_22}) (EAppBinOp Sub (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = mul_23}) (EAppBinOp Mul (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = div_24}) (EAppBinOp Div (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bat_25}) (EAppBinOp BAt (EConst 0) (EConst (UniConst Vector [True])))]
\ No newline at end of file
diff --git a/test/Field/Typed/golden/03-unops.golden b/test/Field/Typed/golden/03-unops.golden
index fd2798f..720e6d7 100644
--- a/test/Field/Typed/golden/03-unops.golden
+++ b/test/Field/Typed/golden/03-unops.golden
@@ -1 +1 @@
-Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?not_5}) (EAppUnOp Not (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?neq0_6}) (EAppUnOp Neq0 (EConst 0)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = neg'_7}) (EAppUnOp Neg (EConst 0)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = inv'_8}) (EAppUnOp Inv (EConst 0)),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #unpack_9}) (EAppUnOp Unp (EConst 1))])
\ No newline at end of file
+Program [] Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?not_5}) (EAppUnOp Not (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?neq0_6}) (EAppUnOp Neq0 (EConst 0)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = neg'_7}) (EAppUnOp Neg (EConst 0)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = inv'_8}) (EAppUnOp Inv (EConst 0)),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #unpack_9}) (EAppUnOp Unp (EConst 1))]
\ No newline at end of file
diff --git a/test/Field/Typed/golden/04-statements.golden b/test/Field/Typed/golden/04-statements.golden
index 1e82855..afdabb0 100644
--- a/test/Field/Typed/golden/04-statements.golden
+++ b/test/Field/Typed/golden/04-statements.golden
@@ -1 +1 @@
-Program (Statements [ELet (UniVar {_uniVarUni = Field, _uniVarVar = x_1}) (EConst 1),EAssert (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = x_2}) (EConst 1)])
\ No newline at end of file
+Program [] Statements [ELet (UniVar {_uniVarUni = Field, _uniVarVar = x_1}) (EConst 1),EAssert (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = x_2}) (EConst 1)]
\ No newline at end of file
diff --git a/test/Field/Typed/golden/05-ifs.golden b/test/Field/Typed/golden/05-ifs.golden
index b389105..d468b9d 100644
--- a/test/Field/Typed/golden/05-ifs.golden
+++ b/test/Field/Typed/golden/05-ifs.golden
@@ -1 +1 @@
-Program (Statements [ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_3}) (EIf (EConst (UniConst Bool True)) (EConst 0) (EConst 0)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bool_4}) (EIf (EConst (UniConst Bool True)) (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_5}) (EIf (EConst (UniConst Bool True)) (EConst (UniConst Vector [True])) (EConst (UniConst Vector [True])))])
\ No newline at end of file
+Program [] Statements [ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_3}) (EIf (EConst (UniConst Bool True)) (EConst 0) (EConst 0)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bool_4}) (EIf (EConst (UniConst Bool True)) (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_5}) (EIf (EConst (UniConst Bool True)) (EConst (UniConst Vector [True])) (EConst (UniConst Vector [True])))]
\ No newline at end of file
diff --git a/test/Field/Typed/golden/06-anns.golden b/test/Field/Typed/golden/06-anns.golden
index edde8c8..dc66d97 100644
--- a/test/Field/Typed/golden/06-anns.golden
+++ b/test/Field/Typed/golden/06-anns.golden
@@ -1 +1 @@
-Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bool_3}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_4}) (EConst 1),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_5}) (EConst (UniConst Vector [True]))])
\ No newline at end of file
+Program [] Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bool_3}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_4}) (EConst 1),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_5}) (EConst (UniConst Vector [True]))]
\ No newline at end of file
diff --git a/test/Field/Typed/golden/07-everything.field b/test/Field/Typed/golden/07-everything.field
index 09e6c96..978f827 100644
--- a/test/Field/Typed/golden/07-everything.field
+++ b/test/Field/Typed/golden/07-everything.field
@@ -1,3 +1,6 @@
+ext ?i;
+ext i;
+ext #i;
 let ?a = T;
 let ?b = F;
 let #v = {T, F, T};
@@ -31,4 +34,4 @@ for j = 0 to 2 do end;
 let ?if = if T then T else T;
 let asf = 1 : field;
 let ?as = T : bool;
-let #as = { T } : vector;
\ No newline at end of file
+let #as = { T } : vector;
diff --git a/test/Field/Typed/golden/07-everything.golden b/test/Field/Typed/golden/07-everything.golden
index a6b87b0..b017ec1 100644
--- a/test/Field/Typed/golden/07-everything.golden
+++ b/test/Field/Typed/golden/07-everything.golden
@@ -1 +1 @@
-Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_36}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_37}) (EConst (UniConst Bool False)),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #v_38}) (EConst (UniConst Vector [True,False,True])),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?e_39}) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?i_4})),ELet (UniVar {_uniVarUni = Field, _uniVarVar = e_40}) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = i_6})),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #e_41}) (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #i_8})),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_42}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_36})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_37}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_43}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_42})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_37}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?xor_44}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_43})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_42}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = f_45}) (EConst 0),ELet (UniVar {_uniVarUni = Field, _uniVarVar = g_46}) (EConst 1),ELet (UniVar {_uniVarUni = Field, _uniVarVar = h_47}) (EConst 2),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?feq_48}) (EAppBinOp FEq (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fle_49}) (EAppBinOp FLe (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?flt_50}) (EAppBinOp FLt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fge_51}) (EAppBinOp FGe (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fgt_52}) (EAppBinOp FGt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = add_53}) (EAppBinOp Add (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = sub_54}) (EAppBinOp Sub (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = mul_55}) (EAppBinOp Mul (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = div_56}) (EAppBinOp Div (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bat_57}) (EAppBinOp BAt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45})) (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #v_38}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?not_58}) (EAppUnOp Not (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_36}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?neq0_59}) (EAppUnOp Neq0 (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = neg'_60}) (EAppUnOp Neg (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = inv'_61}) (EAppUnOp Inv (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47}))),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #unpack_62}) (EAppUnOp Unp (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?let_63}) (EConst (UniConst Bool True)),EAssert (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = j_64}) (EConst 0),ELet (UniVar {_uniVarUni = Field, _uniVarVar = j_65}) (EConst 1),ELet (UniVar {_uniVarUni = Field, _uniVarVar = j_66}) (EConst 2),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?if_67}) (EIf (EConst (UniConst Bool True)) (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = asf_68}) (EConst 1),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?as_69}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #as_70}) (EConst (UniConst Vector [True]))])
\ No newline at end of file
+Program [?i_36,i_37,#i_38] Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_39}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_40}) (EConst (UniConst Bool False)),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #v_41}) (EConst (UniConst Vector [True,False,True])),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?e_42}) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?i_36})),ELet (UniVar {_uniVarUni = Field, _uniVarVar = e_43}) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = i_37})),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #e_44}) (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #i_38})),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_45}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_39})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_40}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_46}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_45})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_40}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?xor_47}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_46})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_45}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = f_48}) (EConst 0),ELet (UniVar {_uniVarUni = Field, _uniVarVar = g_49}) (EConst 1),ELet (UniVar {_uniVarUni = Field, _uniVarVar = h_50}) (EConst 2),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?feq_51}) (EAppBinOp FEq (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_49})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_48}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fle_52}) (EAppBinOp FLe (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_50})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_48}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?flt_53}) (EAppBinOp FLt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_48})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_49}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fge_54}) (EAppBinOp FGe (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_49})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_50}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fgt_55}) (EAppBinOp FGt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_50})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_48}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = add_56}) (EAppBinOp Add (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_48})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_49}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = sub_57}) (EAppBinOp Sub (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_49})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_50}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = mul_58}) (EAppBinOp Mul (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_50})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_48}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = div_59}) (EAppBinOp Div (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_48})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_49}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bat_60}) (EAppBinOp BAt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_48})) (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #v_41}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?not_61}) (EAppUnOp Not (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_39}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?neq0_62}) (EAppUnOp Neq0 (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_48}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = neg'_63}) (EAppUnOp Neg (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_49}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = inv'_64}) (EAppUnOp Inv (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_50}))),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #unpack_65}) (EAppUnOp Unp (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_50}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?let_66}) (EConst (UniConst Bool True)),EAssert (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = j_67}) (EConst 0),ELet (UniVar {_uniVarUni = Field, _uniVarVar = j_68}) (EConst 1),ELet (UniVar {_uniVarUni = Field, _uniVarVar = j_69}) (EConst 2),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?if_70}) (EIf (EConst (UniConst Bool True)) (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = asf_71}) (EConst 1),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?as_72}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #as_73}) (EConst (UniConst Vector [True]))]
\ No newline at end of file
diff --git a/test/Field/golden/01-uniques.field b/test/Field/golden/01-uniques.field
index 1840396..0955d12 100644
--- a/test/Field/golden/01-uniques.field
+++ b/test/Field/golden/01-uniques.field
@@ -1,3 +1,6 @@
+ext a;
+ext b;
+ext a;
 let a = a;
 let a = a;
 for a = 1 to 2 do
diff --git a/test/Field/golden/01-uniques.golden b/test/Field/golden/01-uniques.golden
index 79f055d..beb0837 100644
--- a/test/Field/golden/01-uniques.golden
+++ b/test/Field/golden/01-uniques.golden
@@ -1,10 +1,13 @@
-let a_1 = a_0;
-let a_2 = a_1;
-let a_3 = 1;
-let a_4 = a_3;
+ext a_2;
+ext b_3;
+ext a_4;
 let a_5 = a_4;
-let a_6 = 2;
-let a_7 = a_6;
+let a_6 = a_5;
+let a_7 = 1;
 let a_8 = a_7;
 let a_9 = a_8;
-let a_10 = a_9;
+let a_10 = 2;
+let a_11 = a_10;
+let a_12 = a_11;
+let a_13 = a_12;
+let a_14 = a_13;
diff --git a/test/Field/golden/03-issue-76.field b/test/Field/golden/03-issue-76.field
new file mode 100644
index 0000000..0b2b75a
--- /dev/null
+++ b/test/Field/golden/03-issue-76.field
@@ -0,0 +1,5 @@
+ext x;
+for z = 0 to -1 do
+    let x = x;
+end;
+let y = if (0 == x) then 0 else 0;
diff --git a/test/Field/golden/03-issue-76.golden b/test/Field/golden/03-issue-76.golden
new file mode 100644
index 0000000..260061f
--- /dev/null
+++ b/test/Field/golden/03-issue-76.golden
@@ -0,0 +1,2 @@
+ext x_2;
+let y_3 = if (0 == x_2) then 0 else 0;
diff --git a/test/Field/golden/04-ext-and-for.field b/test/Field/golden/04-ext-and-for.field
new file mode 100644
index 0000000..1ccfa65
--- /dev/null
+++ b/test/Field/golden/04-ext-and-for.field
@@ -0,0 +1,6 @@
+ext i;
+assert i > 0;
+for i = 1 to 2 do
+    assert i > 0;
+end;
+assert i > 0;
diff --git a/test/Field/golden/04-ext-and-for.golden b/test/Field/golden/04-ext-and-for.golden
new file mode 100644
index 0000000..404c9b5
--- /dev/null
+++ b/test/Field/golden/04-ext-and-for.golden
@@ -0,0 +1,7 @@
+ext i_1;
+assert i_1 > 0;
+let i_2 = 1;
+assert i_2 > 0;
+let i_3 = 2;
+assert i_3 > 0;
+assert i_3 > 0;
diff --git a/test/Main.hs b/test/Main.hs
index e588c8e..f08bc8a 100644
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -2,7 +2,7 @@ module Main where
 
 import qualified Field.Axioms        as Field (test_fields)
 import qualified Field.Raw.Textual   as Raw (gen_test_parsing)
-import qualified Field.Renaming      as Field (test_renaming, test_free_variables)
+import qualified Field.Renaming      as Field (test_free_variables)
 import qualified Field.Textual       as Field (gen_test_roundtrip, test_textual)
 import qualified Field.Typed.Textual as Field (gen_test_typechecking)
 
@@ -12,7 +12,6 @@ test_all :: IO TestTree
 test_all =
     testGroup "all" <$> sequence
         [ pure Field.test_free_variables
-        , pure Field.test_renaming
         -- Old tests
         , pure Field.test_fields
         , pure Field.test_textual
diff --git a/tiny-lang.cabal b/tiny-lang.cabal
index 85b7b0f..9837b59 100644
--- a/tiny-lang.cabal
+++ b/tiny-lang.cabal
@@ -19,7 +19,6 @@ library
         Data.Field
         Data.Field.F17
         TinyLang.Environment
-        TinyLang.Generator
         TinyLang.ParseUtils
         TinyLang.Prelude
         TinyLang.Var