diff --git a/src/Grace/Context.hs b/src/Grace/Context.hs
index 5507d36..f9134a9 100644
--- a/src/Grace/Context.hs
+++ b/src/Grace/Context.hs
@@ -10,12 +10,14 @@
 module Grace.Context
     ( -- * Types
       Entry(..)
-    , Context
+    , Context(..)
       -- * Utilities
+    , _Entries
     , lookup
     , splitOnUnsolvedType
     , splitOnUnsolvedFields
     , splitOnUnsolvedAlternatives
+    , uniqueVariableId
     , discardUpTo
     , solveType
     , solveRecord
@@ -23,18 +25,22 @@ module Grace.Context
     , complete
     ) where
 
+import Control.Lens.Lens (Lens', lens)
+import Control.Lens.Tuple (_1, _2)
+import Control.Lens.Zoom (zoom)
+import Control.Monad.State.Strict (State)
 import Data.Text (Text)
 import Grace.Domain (Domain)
 import Grace.Existential (Existential)
-import Grace.Monotype (Monotype)
+import Grace.Monotype (Monotype, VariableId(..))
 import Grace.Pretty (Pretty(..), label, operator, punctuation)
 import Grace.Type (Type)
 import Prelude hiding (lookup)
 import Prettyprinter (Doc)
 import Prettyprinter.Render.Terminal (AnsiStyle)
 
-import qualified Control.Monad as Monad
 import qualified Control.Monad.State.Strict as State
+import qualified Data.Map as Map
 import qualified Grace.Domain as Domain
 import qualified Grace.Existential as Existential
 import qualified Grace.Monotype as Monotype
@@ -50,7 +56,7 @@ import qualified Prettyprinter as Pretty
 
 -- | An element of the `Context` list
 data Entry s
-    = Variable Domain Text
+    = Variable Domain VariableId
     -- ^ Universally quantified variable
     --
     -- >>> pretty @(Entry ()) (Variable Domain.Type "a")
@@ -120,7 +126,7 @@ data Entry s
 instance Pretty (Entry s) where
     pretty = prettyEntry
 
-{-| A `Context` is an ordered list of `Entry`s
+{-| A `Context` is an ordered list of `Entry`s with a Map of occupied `VariableId`s
 
     Note that this representation stores the `Context` entries in reverse
     order, meaning that the beginning of the list represents the entries that
@@ -147,7 +153,11 @@ instance Pretty (Entry s) where
       in the context past a certain entry to reflect the end of their
       \"lifetime\"
 -}
-type Context s = [Entry s]
+data Context s = Context [Entry s] (Map.Map Text Int)
+    deriving Show
+
+_Entries :: Lens' (Context s) [Entry s]
+_Entries = lens (\(Context x _) -> x) (\(Context _ y) x -> Context x y)
 
 prettyEntry :: Entry s -> Doc AnsiStyle
 prettyEntry (Variable domain a) =
@@ -246,8 +256,8 @@ prettyAlternativeType (k, τ) =
     >>> pretty @(Type ()) (solveType [ UnsolvedType 1, SolvedType 0 (Monotype.Scalar Monotype.Bool) ] original)
     Bool
 -}
-solveType :: Context s -> Type s -> Type s
-solveType context type_ = foldl snoc type_ context
+solveType :: [Entry s] -> Type s -> Type s
+solveType entries type_ = foldl snoc type_ entries
   where
     snoc t (SolvedType         a τ) = Type.solveType         a τ t
     snoc t (SolvedFields       a r) = Type.solveFields       a r t
@@ -267,18 +277,17 @@ solveType context type_ = foldl snoc type_ context
     >>> pretty @(Record ()) (solveRecord [ entry ] original)
     { x: Bool }
 -}
-solveRecord :: Context s -> Type.Record s -> Type.Record s
-solveRecord context oldFields = newFields
+solveRecord :: [Entry s] -> Type.Record s -> Type.Record s
+solveRecord entries oldFields = newFields
   where
     location =
         error "Grace.Context.solveRecord: Internal error - Missing location field"
 
     -- TODO: Come up with total solution
     Type.Record{ fields = newFields } =
-        solveType context Type.Record{ fields = oldFields, .. }
+        solveType entries Type.Record{ fields = oldFields, .. }
 
-{-| Substitute a t`Type.Union` using the solved entries of a `Context`
-    `Context`
+{-| Substitute a `Type.Union` using the solved entries of a `Context`
 
     >>> original = Type.Alternatives [("A", Type.Scalar () Monotype.Bool)] (Monotype.UnsolvedAlternatives 0)
     >>> pretty @(Union ()) original
@@ -291,15 +300,21 @@ solveRecord context oldFields = newFields
     >>> pretty @(Union ()) (solveUnion [ entry ] original)
     < A: Bool >
 -}
-solveUnion :: Context s -> Type.Union s -> Type.Union s
-solveUnion context oldAlternatives = newAlternatives
+solveUnion :: [Entry s] -> Type.Union s -> Type.Union s
+solveUnion entries oldAlternatives = newAlternatives
   where
     location =
         error "Grace.Context.solveUnion: Internal error - Missing location field"
 
     -- TODO: Come up with total solution
     Type.Union{ alternatives = newAlternatives } =
-        solveType context Type.Union{ alternatives = oldAlternatives, .. }
+        solveType entries Type.Union{ alternatives = oldAlternatives, .. }
+
+{-| Create an unique `VariableId` out of `Text` given a `Map` of existing variables -}
+uniqueVariableId :: Text -> Int -> State (Map.Map Text Int) VariableId
+uniqueVariableId name atLeast = State.state (\m ->
+    let newId = max atLeast $ maybe 0 (+1) (Map.lookup name m) in
+    (VariableId name newId, Map.insert name newId m))
 
 {-| This function is used at the end of the bidirectional type-checking
     algorithm to complete the inferred type by:
@@ -312,79 +327,54 @@ solveUnion context oldAlternatives = newAlternatives
     >>> pretty @(Type ()) original
     b? -> a?
 
-    >>> pretty @(Type ()) (complete [ UnsolvedType 1, SolvedType 0 (Monotype.Scalar Monotype.Bool) ] original)
-    forall (a : Type) . a -> Bool
+    >>> context = Context [ UnsolvedType 1, SolvedType 0 (Monotype.Scalar Monotype.Bool) ] (Map.fromList [ ("a", 3) ])
+    >>> pretty @(Type ()) (complete context original)
+    forall (a3 : Type) . a3 -> Bool
 -}
 complete :: Context s -> Type s -> Type s
-complete context type0 = do
-    State.evalState (Monad.foldM snoc type0 context) 0
+complete (Context entries variables) =
+    applyUpdates $ State.evalState (traverse updateFor $ reverse entries) (variables, 0)
   where
-    numUnsolved = fromIntegral (length (filter predicate context)) - 1
-      where
-        predicate (UnsolvedType         _) = True
-        predicate (UnsolvedFields       _) = True
-        predicate (UnsolvedAlternatives _) = True
-        predicate  _                       = False
-
-    snoc t (SolvedType         a τ) = do return (Type.solveType         a τ t)
-    snoc t (SolvedFields       a r) = do return (Type.solveFields       a r t)
-    snoc t (SolvedAlternatives a r) = do return (Type.solveAlternatives a r t)
-    snoc t (UnsolvedType a) | a `Type.typeFreeIn` t = do
-        n <- State.get
-
-        State.put $! n + 1
-
-        let name = Existential.toVariable (numUnsolved - n)
-
-        let domain = Domain.Type
-
-        let type_ = Type.solveType a (Monotype.VariableType name) t
-
-        let location = Type.location t
-
-        let nameLocation = location
-
-        return Type.Forall{..}
-    snoc t (UnsolvedFields p) | p `Type.fieldsFreeIn` t = do
-        n <- State.get
-
-        State.put $! n + 1
-
-        let name = Existential.toVariable (numUnsolved - n)
-
-        let domain = Domain.Fields
-
-        let type_ = Type.solveFields p (Monotype.Fields [] (Monotype.VariableFields name)) t
-
-        let location = Type.location t
-
-        let nameLocation = location
-
-        return Type.Forall{..}
-    snoc t (UnsolvedAlternatives p) | p `Type.alternativesFreeIn` t = do
-        n <- State.get
-
-        State.put $! n + 1
-
-        let name = Existential.toVariable (numUnsolved - n)
-
-        let domain = Domain.Alternatives
-
-        let type_ = Type.solveAlternatives p (Monotype.Alternatives [] (Monotype.VariableAlternatives name)) t
-
-        let location = Type.location t
-
-        let nameLocation = location
-
-        return Type.Forall{..}
-    snoc t _ = do
-        return t
-
-{-| Split a `Context` into two `Context`s before and after the given
-    `UnsolvedType` variable.  Neither `Context` contains the variable
+    applyUpdates :: [Type s -> Type s] -> Type s -> Type s
+    applyUpdates = flip $ foldr ($)
+
+    updateFor :: Entry s -> State (Map.Map Text Int, Int) (Type s -> Type s)
+    updateFor (SolvedType         a τ) = return (Type.solveType         a τ)
+    updateFor (SolvedFields       a r) = return (Type.solveFields       a r)
+    updateFor (SolvedAlternatives a r) = return (Type.solveAlternatives a r)
+    updateFor (UnsolvedType a) =
+        newVariable (Type.typeFreeIn a) Domain.Type (Type.solveType a . Monotype.VariableType)
+    updateFor (UnsolvedFields a) =
+        newVariable (Type.fieldsFreeIn a) Domain.Fields (Type.solveFields a . Monotype.Fields [] . Monotype.VariableFields)
+    updateFor (UnsolvedAlternatives a) =
+        newVariable (Type.alternativesFreeIn a) Domain.Alternatives (Type.solveAlternatives a . Monotype.Alternatives [] . Monotype.VariableAlternatives)
+    updateFor _ = return id
+
+    newVariable check domain solve = do
+        n <- zoom _2 (do
+            n <- State.get
+            State.put $! n + 1
+            return n)
+
+        let (internalName, _) = Existential.internalName n
+
+        name <- zoom _1 $ uniqueVariableId internalName 0
+
+        return (\t ->
+            if check t
+                then
+                    let
+                        location = Type.location t
+                        nameLocation = location
+                        type_ = solve name t
+                    in Type.Forall {..}
+                else t)
+
+{-| Split a `[Entry s]` into two `[Entry s]`s before and after the given
+    `UnsolvedType` variable.  Neither `[Entry s]` contains the variable
 
     Returns `Nothing` if no such `UnsolvedType` variable is present within the
-    `Context`
+    `[Entry s]`
 
     >>> splitOnUnsolvedType 1 [ UnsolvedType 1, SolvedType 0 (Monotype.Scalar Monotype.Bool) ]
     Just ([],[SolvedType 0 (Scalar Bool)])
@@ -394,8 +384,8 @@ complete context type0 = do
 splitOnUnsolvedType
     :: Existential Monotype
     -- ^ `UnsolvedType` variable to split on
-    -> Context s
-    -> Maybe (Context s, Context s)
+    -> [Entry s]
+    -> Maybe ([Entry s], [Entry s])
 splitOnUnsolvedType a0 (UnsolvedType a1 : entries)
     | a0 == a1 = return ([], entries)
 splitOnUnsolvedType a (entry : entries) = do
@@ -403,11 +393,10 @@ splitOnUnsolvedType a (entry : entries) = do
     return (entry : prefix, suffix)
 splitOnUnsolvedType _ [] = Nothing
 
-{-| Split a `Context` into two `Context`s before and after the given
-    `UnsolvedFields` variable.  Neither `Context` contains the variable
+{-| Split a `[Entry s]` into two `[Entry s]`s before and after the given
+    `UnsolvedFields` variable.  Neither `[Entry s]` contains the variable
 
-    Returns `Nothing` if no such `UnsolvedFields` variable is present within the
-    `Context`
+    Returns `Nothing` if no such `UnsolvedFields` variable is present within the `[Entry s]`
 
     >>> splitOnUnsolvedFields 1 [ UnsolvedFields 1, SolvedType 0 (Monotype.Scalar Monotype.Bool) ]
     Just ([],[SolvedType 0 (Scalar Bool)])
@@ -417,8 +406,8 @@ splitOnUnsolvedType _ [] = Nothing
 splitOnUnsolvedFields
     :: Existential Monotype.Record
     -- ^ `UnsolvedFields` variable to split on
-    -> Context s
-    -> Maybe (Context s, Context s)
+    -> [Entry s]
+    -> Maybe ([Entry s], [Entry s])
 splitOnUnsolvedFields p0 (UnsolvedFields p1 : entries)
     | p0 == p1 = return ([], entries)
 splitOnUnsolvedFields p (entry : entries) = do
@@ -426,11 +415,11 @@ splitOnUnsolvedFields p (entry : entries) = do
     return (entry : prefix, suffix)
 splitOnUnsolvedFields _ [] = Nothing
 
-{-| Split a `Context` into two `Context`s before and after the given
-    `UnsolvedAlternatives` variable.  Neither `Context` contains the variable
+{-| Split a `[Entry s]` into two `[Entry s]`s before and after the given
+    `UnsolvedAlternatives` variable.  Neither `[Entry s]` contains the variable
 
     Returns `Nothing` if no such `UnsolvedAlternatives` variable is present
-    within the `Context`
+    within the `[Entry s]`
 
     >>> splitOnUnsolvedAlternatives 1 [ UnsolvedAlternatives 1, SolvedType 0 (Monotype.Scalar Monotype.Bool) ]
     Just ([],[SolvedType 0 (Scalar Bool)])
@@ -440,8 +429,8 @@ splitOnUnsolvedFields _ [] = Nothing
 splitOnUnsolvedAlternatives
     :: Existential Monotype.Union
     -- ^ `UnsolvedAlternatives` variable to split on
-    -> Context s
-    -> Maybe (Context s, Context s)
+    -> [Entry s]
+    -> Maybe ([Entry s], [Entry s])
 splitOnUnsolvedAlternatives p0 (UnsolvedAlternatives p1 : entries)
     | p0 == p1 = return ([], entries)
 splitOnUnsolvedAlternatives p (entry : entries) = do
@@ -449,7 +438,7 @@ splitOnUnsolvedAlternatives p (entry : entries) = do
     return (entry : prefix, suffix)
 splitOnUnsolvedAlternatives _ [] = Nothing
 
-{-| Retrieve a variable's annotated type from a `Context`, given the variable's
+{-| Retrieve a variable's annotated type from a `[Entry s]`, given the variable's
     label and index
 
     >>> lookup "x" 0 [ Annotation "x" (Type.Scalar () Monotype.Bool), Annotation "y" (Type.Scalar () Monotype.Natural) ]
@@ -460,7 +449,7 @@ lookup
     -- ^ Variable label
     -> Int
     -- ^ Variable index (See the documentation of `Value.Variable`)
-    -> Context s
+    -> [Entry s]
     -> Maybe (Type s)
 lookup _ _ [] =
     Nothing
@@ -474,12 +463,12 @@ lookup x0 n (Annotation x1 _A : _Γ) =
 lookup x n (_ : _Γ) =
     lookup x n _Γ
 
-{-| Discard all entries from a `Context` up to and including the given `Entry`
+{-| Discard all entries from a `[Entry s]` up to and including the given `Entry`
 
     >>> discardUpTo (MarkerType 1) [ UnsolvedType 1, MarkerType 1, UnsolvedType 0 ]
     [UnsolvedType 0]
 -}
-discardUpTo :: Eq s => Entry s -> Context s -> Context s
+discardUpTo :: Eq s => Entry s -> [Entry s] -> [Entry s]
 discardUpTo entry0 (entry1 : _Γ)
     | entry0 == entry1 = _Γ
     | otherwise = discardUpTo entry0 _Γ
diff --git a/src/Grace/Existential.hs b/src/Grace/Existential.hs
index f55e1c0..9cf802d 100644
--- a/src/Grace/Existential.hs
+++ b/src/Grace/Existential.hs
@@ -13,7 +13,7 @@ module Grace.Existential
     ( -- * Types
       Existential
       -- * Utilities
-    , toVariable
+    , internalName
     ) where
 
 import Data.Text (Text)
@@ -38,23 +38,14 @@ newtype Existential a = UnsafeExistential Int
     deriving newtype (Eq, Num, Show)
 
 instance Pretty (Existential a) where
-    pretty x = label (pretty (toVariable x))
+    pretty (UnsafeExistential n) = label $ pretty $ prefix <> suffix
+      where
+        (prefix, q) = internalName n
+        suffix = if q == 0 then "" else Text.pack (show (q - 1))
 
-{-| Convert an existential variable to a user-friendly `Text`
-    representation
-
-    >>> toVariable 0
-    "a"
-    >>> toVariable 1
-    "b"
-    >>> toVariable 26
-    "a0"
--}
-toVariable :: Existential a -> Text
-toVariable (UnsafeExistential n) = Text.cons prefix suffix
+internalName :: Int -> (Text, Int)
+internalName n = (prefix, q)
   where
     (q, r) = n `quotRem` 26
 
-    prefix = Char.chr (Char.ord 'a' + r)
-
-    suffix = if q == 0 then "" else Text.pack (show (q - 1))
+    prefix = Text.singleton $ Char.chr (Char.ord 'a' + r)
diff --git a/src/Grace/Infer.hs b/src/Grace/Infer.hs
index bc98037..e727423 100644
--- a/src/Grace/Infer.hs
+++ b/src/Grace/Infer.hs
@@ -30,6 +30,8 @@ module Grace.Infer
 
 import Control.Applicative ((<|>))
 import Control.Exception.Safe (Exception(..))
+import Control.Lens (view, (%~), (.~))
+import Control.Lens.Lens (Lens', lens)
 import Control.Monad (when)
 import Control.Monad.Except (MonadError(..))
 import Control.Monad.State.Strict (MonadState)
@@ -37,17 +39,17 @@ import Data.Foldable (traverse_)
 import Data.Sequence (ViewL(..))
 import Data.Text (Text)
 import Data.Void (Void)
-import Grace.Context (Context, Entry)
+import Grace.Context (Context(..), Entry)
 import Grace.Existential (Existential)
 import Grace.Location (Location(..))
-import Grace.Monotype (Monotype)
+import Grace.Monotype (Monotype, VariableId(..))
 import Grace.Pretty (Pretty(..))
 import Grace.Syntax (Syntax)
 import Grace.Type (Type(..))
 import Grace.Value (Value)
 
 import qualified Control.Monad as Monad
-import qualified Control.Monad.State as State
+import qualified Control.Monad.State.Strict as State
 import qualified Data.Map as Map
 import qualified Data.Sequence as Seq
 import qualified Data.Text as Text
@@ -83,22 +85,28 @@ fresh = do
 
     return (fromIntegral n)
 
+_Context :: Lens' Status (Context Location)
+_Context = lens context (\s context -> s { context })
+
+_Entries :: Lens' Status [Entry Location]
+_Entries = _Context . Context._Entries
+
 -- Unlike the original paper, we don't explicitly thread the `Context` around.
 -- Instead, we modify the ambient state using the following utility functions:
 
 -- | Push a new `Context` `Entry` onto the stack
 push :: MonadState Status m => Entry Location -> m ()
-push entry = State.modify (\s -> s { context = entry : context s })
+push entry = State.modify (_Entries %~ (entry:))
 
--- | Retrieve the current `Context`
-get :: MonadState Status m => m (Context Location)
-get = State.gets context
+-- | Retrieve the current `Context` `Entry`s
+get :: MonadState Status m => m [Entry Location]
+get = State.gets (view _Entries)
 
--- | Set the `Context` to a new value
-set :: MonadState Status m => Context Location -> m ()
-set context = State.modify (\s -> s{ context })
+-- | Set the `Context` `Entry`s to a new value
+set :: MonadState Status m => [Entry Location] -> m ()
+set entries = State.modify (_Entries .~ entries)
 
-{-| This is used to temporarily add a `Context` entry that is discarded at the
+{-| This is used to temporarily add a `Context` `Entry` that is discarded at the
     end of the entry's scope, along with any downstream entries that were
     created within that same scope
 -}
@@ -108,7 +116,27 @@ scoped entry k = do
 
     r <- k
 
-    State.modify (\s -> s{ context = Context.discardUpTo entry (context s) })
+    State.modify (_Entries %~ Context.discardUpTo entry)
+
+    return r
+
+{-| Scoped `VariableType`, which possible requires substitutions to preserve uniqueness -}
+scopedVariableType :: MonadState Status m => s -> Domain.Domain -> VariableId -> ((Type.Type s -> Type.Type s) -> m a) -> m a
+scopedVariableType location domain oldId@(VariableId name ind) k = do
+    (newId, oldVariables) <- do
+        Context entries oldVariables <- State.gets (view _Context)
+        let (newInd, variables) = State.runState (Context.uniqueVariableId name ind) oldVariables
+        State.modify (_Context .~ Context entries variables)
+        return (newInd, oldVariables)
+
+    r <- scoped (Context.Variable domain newId) $ k $ if newId == oldId
+        then id
+        else case domain of
+            Domain.Type -> Type.substituteType oldId (Type.VariableType { name = newId, ..})
+            Domain.Fields -> Type.substituteFields oldId (Type.Fields [] $ Monotype.VariableFields newId)
+            Domain.Alternatives -> Type.substituteAlternatives oldId (Type.Alternatives [] $ Monotype.VariableAlternatives newId)  
+    State.modify (_Context %~ (\(Context entries _) ->
+        Context entries oldVariables))
 
     return r
 
@@ -148,7 +176,7 @@ scopedUnsolvedAlternatives k = do
 -}
 wellFormedType
     :: MonadError TypeInferenceError m
-    => Context Location -> Type Location -> m ()
+    => [Entry Location] -> Type Location -> m ()
 wellFormedType _Γ type0 =
     case type0 of
         -- UvarWF
@@ -315,13 +343,13 @@ subtype _A0 _B0 = do
 
         -- <:∃L
         (Type.Exists{..}, _) -> do
-            scoped (Context.Variable domain name) do
-                subtype type_ _B0
+            scopedVariableType nameLocation domain name \substitute ->
+                subtype (substitute type_) _B0
 
         -- <:∀R
         (_, Type.Forall{..}) -> do
-            scoped (Context.Variable domain name) do
-                subtype _A0 type_
+            scopedVariableType nameLocation domain name \substitute->
+                subtype _A0 (substitute type_)
 
         -- <:∃R
         (_, Type.Exists{ domain = Domain.Type, .. }) -> do
@@ -814,8 +842,8 @@ instantiateTypeL a _A0 = do
 
         -- InstLAllR
         Type.Forall{..} -> do
-            scoped (Context.Variable domain name) do
-                instantiateTypeL a type_
+            scopedVariableType nameLocation domain name \substitute ->
+                instantiateTypeL a (substitute type_)
 
         -- This case is the first example of a general pattern we have to
         -- follow when solving unsolved variables.
@@ -957,8 +985,8 @@ instantiateTypeR _A0 a = do
 
         -- InstRExtL
         Type.Exists{..} -> do
-            scoped (Context.Variable domain name) do
-                instantiateTypeL a type_
+            scopedVariableType nameLocation domain name \substitute ->
+                instantiateTypeL a (substitute type_)
 
         -- InstRAllL
         Type.Forall{ domain = Domain.Type, .. } -> do
@@ -1897,8 +1925,8 @@ check e Type.Exists{ domain = Domain.Alternatives, .. } = do
 
 -- ∀I
 check e Type.Forall{..} = do
-    scoped (Context.Variable domain name) do
-        check e type_
+    scopedVariableType nameLocation domain name \substitute ->
+        check e (substitute type_)
 
 check Syntax.Operator{ operator = Syntax.Times, .. } _B@Type.Scalar{ scalar }
     | scalar `elem` ([ Monotype.Natural, Monotype.Integer, Monotype.Real ] :: [Monotype.Scalar])= do
@@ -2029,8 +2057,8 @@ inferApplication Type.Forall{ domain = Domain.Alternatives, .. } e = do
 
 -- ∃App
 inferApplication Type.Exists{..} e = do
-    scoped (Context.Variable domain name) do
-        inferApplication type_ e
+    scopedVariableType nameLocation domain name \substitute ->
+        inferApplication (substitute type_) e
 
 -- αApp
 inferApplication Type.UnsolvedType{ existential = a, .. } e = do
@@ -2059,9 +2087,9 @@ inferApplication _A _ = do
 typeOf
     :: Syntax Location (Type Location, Value)
     -> Either TypeInferenceError (Type Location)
-typeOf = typeWith []
+typeOf = typeWith (Context [] Map.empty)
 
--- | Like `typeOf`, but accepts a custom type-checking `Context`
+-- | Like `typeOf`, but accepts a custom type-checking `[Entry Location]`
 typeWith
     :: Context Location
     -> Syntax Location (Type Location, Value)
@@ -2075,9 +2103,9 @@ typeWith context syntax = do
 
 -- | A data type holding all errors related to type inference
 data TypeInferenceError
-    = IllFormedAlternatives Location (Existential Monotype.Union) (Context Location)
-    | IllFormedFields Location (Existential Monotype.Record) (Context Location)
-    | IllFormedType Location (Type Location) (Context Location)
+    = IllFormedAlternatives Location (Existential Monotype.Union) ([Entry Location])
+    | IllFormedFields Location (Existential Monotype.Record) ([Entry Location])
+    | IllFormedType Location (Type Location) ([Entry Location])
     --
     | InvalidOperands Location (Type Location)
     --
@@ -2085,14 +2113,14 @@ data TypeInferenceError
     | MergeInvalidHandler Location (Type Location)
     | MergeRecord Location (Type Location)
     --
-    | MissingAllAlternatives (Existential Monotype.Union) (Context Location)
-    | MissingAllFields (Existential Monotype.Record) (Context Location)
-    | MissingOneOfAlternatives [Location] (Existential Monotype.Union) (Existential Monotype.Union) (Context Location)
-    | MissingOneOfFields [Location] (Existential Monotype.Record) (Existential Monotype.Record) (Context Location)
-    | MissingVariable (Existential Monotype) (Context Location)
+    | MissingAllAlternatives (Existential Monotype.Union) ([Entry Location])
+    | MissingAllFields (Existential Monotype.Record) ([Entry Location])
+    | MissingOneOfAlternatives [Location] (Existential Monotype.Union) (Existential Monotype.Union) ([Entry Location])
+    | MissingOneOfFields [Location] (Existential Monotype.Record) (Existential Monotype.Record) ([Entry Location])
+    | MissingVariable (Existential Monotype) ([Entry Location])
     --
     | NotFunctionType Location (Type Location)
-    | NotNecessarilyFunctionType Location Text
+    | NotNecessarilyFunctionType Location VariableId
     --
     | NotAlternativesSubtype Location (Existential Monotype.Union) (Type.Union Location)
     | NotFieldsSubtype Location (Existential Monotype.Record) (Type.Record Location)
@@ -2100,14 +2128,14 @@ data TypeInferenceError
     | NotUnionSubtype Location (Type Location) Location (Type Location)
     | NotSubtype Location (Type Location) Location (Type Location)
     --
-    | UnboundAlternatives Location Text
-    | UnboundFields Location Text
-    | UnboundTypeVariable Location Text
+    | UnboundAlternatives Location VariableId
+    | UnboundFields Location VariableId
+    | UnboundTypeVariable Location VariableId
     | UnboundVariable Location Text Int
     --
     | RecordTypeMismatch (Type Location) (Type Location) (Map.Map Text (Type Location)) (Map.Map Text (Type Location))
     | UnionTypeMismatch (Type Location) (Type Location) (Map.Map Text (Type Location)) (Map.Map Text (Type Location))
-    deriving (Eq, Show)
+    deriving Show
 
 instance Exception TypeInferenceError where
     displayException (IllFormedAlternatives location a0 _Γ) =
@@ -2360,17 +2388,17 @@ instance Exception TypeInferenceError where
         \" <> Text.unpack (Location.renderError "" locB0)
 
     displayException (UnboundAlternatives location a) =
-        "Unbound alternatives variable: " <> Text.unpack a <> "\n\
+        "Unbound alternatives variable: " <> Text.unpack (prettyToText a) <> "\n\
         \\n\
         \" <> Text.unpack (Location.renderError "" location)
 
     displayException (UnboundFields location a) =
-        "Unbound fields variable: " <> Text.unpack a <> "\n\
+        "Unbound fields variable: " <> Text.unpack (prettyToText a) <> "\n\
         \\n\
         \" <> Text.unpack (Location.renderError "" location)
 
     displayException (UnboundTypeVariable location a) =
-        "Unbound type variable: " <> Text.unpack a <> "\n\
+        "Unbound type variable: " <> Text.unpack (prettyToText a) <> "\n\
         \\n\
         \" <> Text.unpack (Location.renderError "" location)
 
diff --git a/src/Grace/Interpret.hs b/src/Grace/Interpret.hs
index 8c90125..fc7fece 100644
--- a/src/Grace/Interpret.hs
+++ b/src/Grace/Interpret.hs
@@ -30,6 +30,7 @@ import Grace.Value (Value)
 import qualified Control.Exception.Safe as Exception
 import qualified Control.Lens as Lens
 import qualified Control.Monad.Except as Except
+import qualified Data.Map as Map
 import qualified Grace.Context as Context
 import qualified Grace.HTTP as HTTP
 import qualified Grace.Import as Import
@@ -98,7 +99,7 @@ interpretWith bindings maybeAnnotation manager input = do
 
             return (Context.Annotation variable type_)
 
-    case Infer.typeWith typeContext annotatedExpression of
+    case Infer.typeWith (Context.Context typeContext Map.empty) annotatedExpression of
         Left message -> do
             Except.throwError (TypeInferenceError message)
 
diff --git a/src/Grace/Monotype.hs b/src/Grace/Monotype.hs
index ca8a743..232c15b 100644
--- a/src/Grace/Monotype.hs
+++ b/src/Grace/Monotype.hs
@@ -9,28 +9,54 @@
 -}
 module Grace.Monotype
     ( -- * Types
-      Monotype(..)
+      VariableId(..)
+    , Monotype(..)
     , Scalar(..)
     , Record(..)
     , RemainingFields(..)
     , Union(..)
     , RemainingAlternatives(..)
+      -- * Utilities
+    , variableId
     ) where
 
+import Data.List (elemIndex)
 import Data.String (IsString(..))
-import Data.Text (Text)
+import Data.Text (Text, pack, unsnoc)
 import GHC.Generics (Generic)
 import Grace.Existential (Existential)
-import Grace.Pretty (Pretty(..), builtin)
+import Grace.Pretty (Pretty(..), builtin, label)
 import Language.Haskell.TH.Syntax (Lift)
 
+data VariableId = VariableId Text Int
+    deriving (Eq, Show, Lift)
+
+{-| Construct non-unique VariableId out of raw Text. -}
+variableId :: Text -> VariableId
+variableId = \text ->
+  let (name, ind) = takeIntFromEnd 0 1 text
+  in VariableId name ind
+  where
+    takeIntFromEnd :: Int -> Int -> Text -> (Text, Int)
+    takeIntFromEnd curr mult text
+      | Just (xs, x) <- unsnoc text
+      , Just ind <- x `elemIndex` "0123456789"
+        = takeIntFromEnd (curr + ind*mult) (10*mult) xs
+    takeIntFromEnd curr _ xs = (xs, curr)
+
+instance IsString VariableId where
+  fromString = variableId . pack
+
+instance Pretty VariableId where
+  pretty (VariableId text ind) = label $ pretty (text <> if ind == 0 then "" else fromString $ show (ind - 1))
+
 {-| A monomorphic type
 
     This is same type as `Grace.Type.Type`, except without the
     `Grace.Type.Forall` and `Grace.Type.Exists` constructors
 -}
 data Monotype
-    = VariableType Text
+    = VariableType VariableId
     | UnsolvedType (Existential Monotype)
     | Function Monotype Monotype
     | Optional Monotype
@@ -41,7 +67,7 @@ data Monotype
     deriving stock (Eq, Generic, Show)
 
 instance IsString Monotype where
-    fromString string = VariableType (fromString string)
+    fromString = VariableType . fromString
 
 -- | A scalar type
 data Scalar
@@ -97,7 +123,7 @@ data RemainingFields
     -- ^ The record type is open, meaning that some fields are known and there
     --   is an unsolved fields variable that is a placeholder for other fields
     --   that may or may not be present
-    | VariableFields Text
+    | VariableFields VariableId
     -- ^ Same as `UnsolvedFields`, except that the user has given the fields
     --   variable an explicit name in the source code
     deriving stock (Eq, Generic, Lift, Show)
@@ -114,7 +140,7 @@ data RemainingAlternatives
     -- ^ The union type is open, meaning that some alternatives are known and
     --   there is an unsolved alternatives variable that is a placeholder for
     --   other alternatives that may or may not be present
-    | VariableAlternatives Text
+    | VariableAlternatives VariableId
     -- ^ Same as `UnsolvedAlternatives`, except that the user has given the
     --   alternatives variable an explicit name in the source code
     deriving stock (Eq, Generic, Lift, Show)
diff --git a/src/Grace/Parser.hs b/src/Grace/Parser.hs
index 5089b0b..85357df 100644
--- a/src/Grace/Parser.hs
+++ b/src/Grace/Parser.hs
@@ -510,7 +510,7 @@ grammar = mdo
 
     quantifiedType <- rule do
         let quantify (forallOrExists, location, (typeVariableOffset, typeVariable), domain_) type_ =
-                forallOrExists location typeVariableOffset typeVariable domain_ type_
+                forallOrExists location typeVariableOffset (Monotype.variableId typeVariable) domain_ type_
 
         fss <- many
             (   do  location <- locatedToken Lexer.Forall
@@ -573,7 +573,7 @@ grammar = mdo
         <|> do  location <- locatedToken Lexer.Text
                 return Type.Scalar{ scalar = Monotype.Text, .. }
         <|> do  ~(location, name) <- locatedLabel
-                return Type.VariableType{..}
+                return Type.VariableType{ name = Monotype.variableId name, ..}
         <|> do  let record location fields = Type.Record{..}
 
                 locatedOpenBrace <- locatedToken Lexer.OpenBrace
@@ -584,7 +584,7 @@ grammar = mdo
 
                 toFields <-
                     (   do  text_ <- recordLabel
-                            pure (\fs -> Type.Fields fs (Monotype.VariableFields text_))
+                            pure (\fs -> Type.Fields fs (Monotype.VariableFields $ Monotype.variableId text_))
                     <|> do  pure (\fs -> Type.Fields fs Monotype.EmptyFields)
                     <|> do  f <- fieldType
                             pure (\fs -> Type.Fields (fs <> [ f ]) Monotype.EmptyFields)
@@ -605,7 +605,7 @@ grammar = mdo
 
                 toAlternatives <-
                     (   do  text_ <- label
-                            return (\as -> Type.Alternatives as (Monotype.VariableAlternatives text_))
+                            return (\as -> Type.Alternatives as (Monotype.VariableAlternatives $ Monotype.variableId text_))
                     <|> do  pure (\as -> Type.Alternatives as Monotype.EmptyAlternatives)
                     <|> do  a <- alternativeType
                             return (\as -> Type.Alternatives (as <> [ a ]) Monotype.EmptyAlternatives)
diff --git a/src/Grace/Type.hs b/src/Grace/Type.hs
index 43a0179..c28cd97 100644
--- a/src/Grace/Type.hs
+++ b/src/Grace/Type.hs
@@ -51,7 +51,12 @@ import Prettyprinter (Doc)
 import Prettyprinter.Render.Terminal (AnsiStyle)
 
 import Grace.Monotype
-    (Monotype, RemainingAlternatives(..), RemainingFields(..), Scalar(..))
+    ( Monotype
+    , RemainingAlternatives(..)
+    , RemainingFields(..)
+    , Scalar(..)
+    , VariableId
+    )
 
 import qualified Control.Lens as Lens
 import qualified Data.Text as Text
@@ -68,7 +73,7 @@ import qualified Prettyprinter as Pretty
 
 -- | A potentially polymorphic type
 data Type s
-    = VariableType { location :: s, name :: Text }
+    = VariableType { location :: s, name :: VariableId }
     -- ^ Type variable
     --
     -- >>> pretty @(Type ()) (VariableType () "a")
@@ -78,12 +83,12 @@ data Type s
     --
     -- >>> pretty @(Type ()) (UnsolvedType () 0)
     -- a?
-    | Exists { location :: s, nameLocation :: s, name :: Text, domain :: Domain, type_ :: Type s }
+    | Exists { location :: s, nameLocation :: s, name :: VariableId, domain :: Domain, type_ :: Type s }
     -- ^ Existentially quantified type
     --
     -- >>> pretty @(Type ()) (Exists () () "a" Domain.Type "a")
     -- exists (a : Type) . a
-    | Forall { location :: s, nameLocation :: s, name :: Text, domain :: Domain, type_ :: Type s }
+    | Forall { location :: s, nameLocation :: s, name :: VariableId, domain :: Domain, type_ :: Type s }
     -- ^ Universally quantified type
     --
     -- >>> pretty @(Type ()) (Forall () () "a" Domain.Type "a")
@@ -264,7 +269,7 @@ solveAlternatives unsolved (Monotype.Alternatives alternativeMonotypes alternati
 
 {-| Helper function for traversing the tree during `Type` substitutions.
 -}
-substitute :: Text -> Domain -> ((Type s -> Type s) -> Type s -> Type s) -> Type s -> Type s
+substitute :: VariableId -> Domain -> ((Type s -> Type s) -> Type s -> Type s) -> Type s -> Type s
 substitute a aDomain substituter = sub
     where
         sub = substituter def
@@ -304,7 +309,7 @@ substitute a aDomain substituter = sub
 {-| Replace all occurrences of a variable within one `Type` with another `Type`,
     given the variable's label
 -}
-substituteType :: Text -> Type s -> Type s -> Type s
+substituteType :: VariableId -> Type s -> Type s -> Type s
 substituteType a _A = substitute a Domain.Type substituteType'
     where
         substituteType' _ VariableType{..}
@@ -315,7 +320,7 @@ substituteType a _A = substitute a Domain.Type substituteType'
 {-| Replace all occurrences of a variable within one `Type` with another `Type`,
     given the variable's label
 -}
-substituteFields :: Text -> Record s -> Type s -> Type s
+substituteFields :: VariableId -> Record s -> Type s -> Type s
 substituteFields ρ0 (Fields kτs ρ1) = substitute ρ0 Domain.Fields substituteFields'
     where
         substituteFields' skipLevel Record{ fields = Fields kAs0 ρ, .. }
@@ -329,7 +334,7 @@ substituteFields ρ0 (Fields kτs ρ1) = substitute ρ0 Domain.Fields substitute
 {-| Replace all occurrences of a variable within one `Type` with another `Type`,
     given the variable's label and index
 -}
-substituteAlternatives :: Text -> Union s -> Type s -> Type s
+substituteAlternatives :: VariableId -> Union s -> Type s -> Type s
 substituteAlternatives ρ0 (Alternatives kτs ρ1) = substitute ρ0 Domain.Alternatives substituteAlternatives'
     where
         substituteAlternatives' skipLevel Union{ alternatives = Alternatives kAs0 ρ, .. }
diff --git a/tasty/data/error/type/conflicting-names-input.ffg b/tasty/data/error/type/conflicting-names-input.ffg
new file mode 100644
index 0000000..88d6974
--- /dev/null
+++ b/tasty/data/error/type/conflicting-names-input.ffg
@@ -0,0 +1,6 @@
+# This test checks that matching variable names do not trick the typechecker
+# into unifying two different type variables.
+let test
+    : exists (a : Type). a
+	= 3
+in test : forall (a : Type). a
diff --git a/tasty/data/error/type/conflicting-names-stderr.txt b/tasty/data/error/type/conflicting-names-stderr.txt
new file mode 100644
index 0000000..53aa896
--- /dev/null
+++ b/tasty/data/error/type/conflicting-names-stderr.txt
@@ -0,0 +1,19 @@
+Not a subtype
+
+The following type:
+
+  a0
+
+tasty/data/error/type/conflicting-names-input.ffg:4:15: 
+  │
+4 │     : exists (a : Type). a
+  │               ↑
+
+… cannot be a subtype of:
+
+  a
+
+tasty/data/error/type/conflicting-names-input.ffg:6:30: 
+  │
+6 │ in test : forall (a : Type). a
+  │                              ↑
\ No newline at end of file