diff --git a/parser-typechecker/src/Unison/Paths.hs b/parser-typechecker/src/Unison/Paths.hs
index 3f6cc109d..9eb4d6881 100644
--- a/parser-typechecker/src/Unison/Paths.hs
+++ b/parser-typechecker/src/Unison/Paths.hs
@@ -50,11 +50,11 @@ focus1 e = ABT.Path go' where
   go Fn (Term (E.App' fn arg)) =
     Just (Term fn, \fn -> Term <$> (E.app <$> asTerm fn <*> pure (w arg)), [])
   go Fn (Type (T.App' fn arg)) =
-    Just (Type fn, \fn -> Type <$> (T.app <$> asType fn <*> pure (wt arg)), [])
+    Just (Type fn, \fn -> Type <$> (T.app() <$> asType fn <*> pure (wt arg)), [])
   go Arg (Term (E.App' fn arg)) =
     Just (Term arg, \arg -> Term <$> (E.app (w fn) <$> asTerm arg), [])
   go Arg (Type (T.App' fn arg)) =
-    Just (Type arg, \arg -> Type <$> (T.app (wt fn) <$> asType arg), [])
+    Just (Type arg, \arg -> Type <$> (T.app() (wt fn) <$> asType arg), [])
   go Body (Term (E.LamNamed' v body)) = Just (Term body, \t -> Term . set <$> asTerm t, [v]) where
     set body = ABT.tm (E.Lam (ABT.absr v body))
   go Body (Term (E.Let1Named' v b body)) = Just (Term body, \t -> Term . set <$> asTerm t, [v]) where
@@ -81,7 +81,7 @@ focus1 e = ABT.Path go' where
   go Bound (Term (E.Let1Named' v b body)) =
     Just (Var v, \v -> (\v -> Term $ E.let1 [(v,w b)] (w body)) <$> asVar v, [])
   go Bound (Type (T.ForallNamed' v body)) =
-    Just (Var v, \v -> Type <$> (T.forall <$> asVar v <*> pure (wt body)), [])
+    Just (Var v, \v -> Type <$> (T.forall() <$> asVar v <*> pure (wt body)), [])
   go (Index i) (Term (E.Vector' vs)) | i < Vector.length vs && i >= 0 =
     Just (Term (vs `Vector.unsafeIndex` i),
           \e -> (\e -> Term $ E.vector' $ fmap w vs // [(i,e)]) <$> asTerm e,
@@ -91,8 +91,8 @@ focus1 e = ABT.Path go' where
     set _ = Nothing
   go Annotation (Term (E.Ann' e t)) = Just (Type t, \t -> Term . E.ann (w e) <$> asType t, [])
   go Body (Term (E.Ann' body t)) = Just (Term body, \body -> Term . flip E.ann (wt t) <$> asTerm body, [])
-  go Input (Type (T.Arrow' i o)) = Just (Type i, \i -> Type <$> (T.arrow <$> asType i <*> pure (wt o)), [])
-  go Output (Type (T.Arrow' i o)) = Just (Type o, \o -> Type . T.arrow (wt i) <$> asType o, [])
+  go Input (Type (T.Arrow' i o)) = Just (Type i, \i -> Type <$> (T.arrow() <$> asType i <*> pure (wt o)), [])
+  go Output (Type (T.Arrow' i o)) = Just (Type o, \o -> Type . T.arrow() (wt i) <$> asType o, [])
   go _ _ = Nothing
 
 type Path = [PathElement]
diff --git a/parser-typechecker/src/Unison/TermParser.hs b/parser-typechecker/src/Unison/TermParser.hs
index 7a2ba2940..963f87c24 100644
--- a/parser-typechecker/src/Unison/TermParser.hs
+++ b/parser-typechecker/src/Unison/TermParser.hs
@@ -351,8 +351,10 @@ alias = do
   TypeParser.Aliases s <- get
   let s' = (fn, apply)
       apply args | length args <= length params = ABT.substs (params `zip` args) body
-      apply args = apply (take n args) `Type.apps` drop n args
+      apply args = apply (take n args) `Type.apps` (addUnit <$> drop n args)
+      apply args = apply (take n args) `Type.apps` (addUnit <$> drop n args)
       n = length params
+      addUnit a = ((), a)
   set (TypeParser.Aliases (s':s))
 
 -- bindings :: Var v => Parser (S v) [(v, Term v)]
diff --git a/parser-typechecker/src/Unison/Type.hs b/parser-typechecker/src/Unison/Type.hs
index 77ac00866..61cde12ab 100644
--- a/parser-typechecker/src/Unison/Type.hs
+++ b/parser-typechecker/src/Unison/Type.hs
@@ -25,6 +25,7 @@ import qualified Unison.Hashable as Hashable
 import qualified Unison.Kind as K
 import qualified Unison.Reference as Reference
 import qualified Unison.TypeVar as TypeVar
+import qualified Unison.Var as Var
 
 -- | Base functor for types in the Unison language
 data F a
@@ -117,65 +118,66 @@ isArrow _ = False
 
 -- some smart constructors
 
-infixr 7 -->
-(-->) :: Ord v => Type v -> Type v -> Type v
-(-->) = arrow
+vector :: Ord v => a -> AnnotatedType v a
+vector a = builtin a "Sequence"
 
-vector :: Ord v => Type v
-vector = builtin "Sequence"
+-- vectorOf :: Ord v => a -> AnnotatedType v a -> Type v
+-- vectorOf a t = vector `app` t
 
-vectorOf :: Ord v => Type v -> Type v
-vectorOf t = vector `app` t
+ref :: Ord v => a -> Reference -> AnnotatedType v a
+ref a = ABT.tm' a . Ref
 
-ref :: Ord v => Reference -> Type v
-ref = ABT.tm . Ref
+builtin :: Ord v => a -> Text -> AnnotatedType v a
+builtin a = ref a . Reference.Builtin
 
-builtin :: Ord v => Text -> Type v
-builtin = ref . Reference.Builtin
+int64 :: Ord v => a -> AnnotatedType v a
+int64 a = builtin a "Int64"
 
-int64 :: Ord v => Type v
-int64 = builtin "Int64"
+uint64 :: Ord v => a -> AnnotatedType v a
+uint64 a = builtin a "UInt64"
 
-uint64 :: Ord v => Type v
-uint64 = builtin "UInt64"
+float :: Ord v => a -> AnnotatedType v a
+float a = builtin a "Float"
 
-float :: Ord v => Type v
-float = builtin "Float"
+boolean :: Ord v => a -> AnnotatedType v a
+boolean a = builtin a "Boolean"
 
-boolean :: Ord v => Type v
-boolean = builtin "Boolean"
+text :: Ord v => a -> AnnotatedType v a
+text a = builtin a "Text"
 
-text :: Ord v => Type v
-text = builtin "Text"
+stream :: Ord v => a -> AnnotatedType v a
+stream a = builtin a "Stream"
 
-stream :: Ord v => Type v
-stream = builtin "Stream"
+app :: Ord v => a -> AnnotatedType v a -> AnnotatedType v a -> AnnotatedType v a
+app a f arg = ABT.tm' a (App f arg)
+
+-- `f x y z` means `((f x) y) z` and the annotation paired with `y` is the one
+-- meant for `app (f x) y`
+apps :: Ord v => AnnotatedType v a -> [(a, AnnotatedType v a)] -> AnnotatedType v a
+apps f params = foldl' go f params where
+  go f (a,t) = app a f t
+
+arrow :: Ord v => a -> AnnotatedType v a -> AnnotatedType v a -> AnnotatedType v a
+arrow a i o = ABT.tm' a (Arrow i o)
+
+ann :: Ord v => a -> AnnotatedType v a -> K.Kind -> AnnotatedType v a
+ann a e t = ABT.tm' a (Ann e t)
+
+forall :: Ord v => a -> v -> AnnotatedType v a -> AnnotatedType v a
+forall a v body = ABT.tm' a (Forall (ABT.abs' a v body))
 
 iff :: Var v => Type v
-iff = forall aa $ arrows [boolean, a, a] a
+iff = forall () aa $ arrows (f <$> [boolean(), a, a]) a
   where aa = ABT.v' "a"
-        a = var aa
+        a = var () aa
+        f x = ((), x)
 
 andor :: Ord v => Type v
-andor = arrows [boolean, boolean] boolean
+andor = arrows (f <$> [boolean(), boolean()]) $ boolean()
+  where f x = ((), x)
 
-app :: Ord v => Type v -> Type v -> Type v
-app f arg = ABT.tm (App f arg)
-
-apps :: Ord v => Type v -> [Type v] -> Type v
-apps f = foldl' app f
-
-arrow :: Ord v => Type v -> Type v -> Type v
-arrow i o = ABT.tm (Arrow i o)
-
-ann :: Ord v => Type v -> K.Kind -> Type v
-ann e t = ABT.tm (Ann e t)
-
-forall :: Ord v => v -> Type v -> Type v
-forall v body = ABT.tm (Forall (ABT.abs v body))
-
-var :: Ord v => v -> Type v
-var = ABT.var
+var :: Ord v => a -> v -> AnnotatedType v a
+var = ABT.annotatedVar
 
 existential :: Ord v => v -> Type (TypeVar v)
 existential v = ABT.var (TypeVar.Existential v)
@@ -192,24 +194,28 @@ universal' a v = ABT.annotatedVar a (TypeVar.Universal v)
 v' :: Var v => Text -> Type v
 v' s = ABT.var (ABT.v' s)
 
-forall' :: Var v => [Text] -> Type v -> Type v
-forall' vs body = foldr forall body (map ABT.v' vs)
+forall' :: Var v => a -> [Text] -> AnnotatedType v a -> AnnotatedType v a
+forall' a vs body = foldr (forall a) body (Var.named <$> vs)
 
-foralls :: Var v => [v] -> Type v -> Type v
-foralls vs body = foldr forall body vs
+foralls :: Var v => a -> [v] -> AnnotatedType v a -> AnnotatedType v a
+foralls a vs body = foldr (forall a) body vs
 
-arrows :: Ord v => [Type v] -> Type v -> Type v
-arrows ts result = foldr arrow result ts
+-- Note: `a -> b -> c` parses as `a -> (b -> c)`
+-- the annotation associated with `b` will be the annotation for the `b -> c`
+-- node
+arrows :: Ord v => [(a, AnnotatedType v a)] -> AnnotatedType v a -> AnnotatedType v a
+arrows ts result = foldr go result ts where
+  go (a,t) result = arrow a t result
 
 -- The types of effectful computations
-effect :: Ord v => [Type v] -> Type v -> Type v
-effect es (Effect' fs t) = ABT.tm (Effect (es ++ fs) t)
-effect es t = ABT.tm (Effect es t)
+effect :: Ord v => a -> [AnnotatedType v a] -> AnnotatedType v a -> AnnotatedType v a
+effect a es (Effect' fs t) = ABT.tm' a (Effect (es ++ fs) t)
+effect a es t = ABT.tm' a (Effect es t)
 
 -- The types of first-class effect values
 -- which get deconstructed in effect handlers.
-effectV :: Ord v => Type v -> Type v -> Type v
-effectV e t = apps (builtin "Effect") [e, t]
+effectV :: Ord v => a -> (a, AnnotatedType v a) -> (a, AnnotatedType v a) -> AnnotatedType v a
+effectV builtinA e t = apps (builtin builtinA "Effect") [e, t]
 
 -- Strips effects from a type. E.g. `{e} a` becomes `a`.
 stripEffect :: AnnotatedType v a -> ([AnnotatedType v a], AnnotatedType v a)
@@ -219,12 +225,12 @@ stripEffect t = ([], t)
 -- The type of the flipped function application operator:
 -- `(a -> (a -> b) -> b)`
 flipApply :: Var v => Type v -> Type v
-flipApply t = forall b $ arrow (arrow t (var b)) (var b)
+flipApply t = forall() b $ arrow() (arrow() t (var() b)) (var() b)
   where b = ABT.fresh t (ABT.v' "b")
 
 -- | Bind all free variables with an outer `forall`.
-generalize :: Ord v => Type v -> Type v
-generalize t = foldr forall t $ Set.toList (ABT.freeVars t)
+generalize :: Ord v => AnnotatedType v a -> AnnotatedType v a
+generalize t = foldr (forall (ABT.annotation t)) t $ Set.toList (ABT.freeVars t)
 
 instance Hashable1 F where
   hash1 hashCycle hash e =
diff --git a/parser-typechecker/src/Unison/TypeParser.hs b/parser-typechecker/src/Unison/TypeParser.hs
index 8765e0693..412be7bb0 100644
--- a/parser-typechecker/src/Unison/TypeParser.hs
+++ b/parser-typechecker/src/Unison/TypeParser.hs
@@ -66,15 +66,15 @@ effect = do
   es <- sepBy (token (string ",")) valueType
   token_ $ string "}"
   t <- valueTypeLeaf
-  pure (Type.effect es t)
+  pure (Type.effect() es t)
 
 tupleOrParenthesized :: Ord v => TypeP v -> TypeP v
 tupleOrParenthesized rec =
   parenthesized $ go <$> sepBy (token $ string ",") rec where
     go [t] = t
     go types = foldr pair unit types
-    pair t1 t2 = Type.builtin "Pair" `Type.app` t1 `Type.app` t2
-    unit = Type.builtin "()"
+    pair t1 t2 = Type.app() (Type.app() (Type.builtin() "Pair") t1) t2
+    unit = Type.builtin() "()"
 
 -- "TypeA TypeB TypeC"
 app :: Ord v => TypeP v -> TypeP v
@@ -82,14 +82,14 @@ app rec = get >>= \(Aliases aliases) -> do
   (hd:tl) <- some rec
   pure $ case hd of
     Type.Var' v -> case lookup v aliases of
-      Nothing -> foldl' Type.app hd tl
+      Nothing -> foldl' (Type.app()) hd tl
       Just apply -> apply tl
-    _ -> foldl' Type.app hd tl
+    _ -> foldl' (Type.app()) hd tl
 
 --  valueType ::= ... | Arrow valueType computationType
 arrow :: Var v => TypeP v -> TypeP v
 arrow rec = do
-  t <- foldr1 Type.arrow <$> sepBy1 (token (string "->")) (effect <|> rec)
+  t <- foldr1 (Type.arrow()) <$> sepBy1 (token (string "->")) (effect <|> rec)
   case t of
     Type.Arrow' (Type.Effect' _ _) _ -> fail "effect to the left of an ->"
     _ -> pure t
@@ -101,7 +101,7 @@ forall rec = do
     vars <- some $ token varName
     _ <- token (char '.')
     t <- rec
-    pure $ Type.forall' (fmap Text.pack vars) t
+    pure $ Type.forall'() (fmap Text.pack vars) t
 
 varName :: Parser s String
 varName = do
diff --git a/parser-typechecker/src/Unison/Typechecker/Context2.hs b/parser-typechecker/src/Unison/Typechecker/Context2.hs
index f525022c7..c802302fb 100644
--- a/parser-typechecker/src/Unison/Typechecker/Context2.hs
+++ b/parser-typechecker/src/Unison/Typechecker/Context2.hs
@@ -371,6 +371,21 @@ extendMarker loc v = do
 notMember :: Var v => v -> Set (TypeVar v) -> Bool
 notMember v s = Set.notMember (TypeVar.Universal v) s && Set.notMember (TypeVar.Existential v) s
 
+-- | Replace any existentials with their solution in the context
+apply :: Var v => Context v loc -> Type v loc -> Type v loc
+apply ctx t = _todo
+--case t of
+--  Type.Universal' _ -> t
+--  Type.Ref' _ -> t
+--  Type.Existential' v ->
+--    maybe t (\(Type.Monotype t') -> apply ctx t') (lookup v (solved ctx))
+--  Type.Arrow' i o -> Type.arrow (apply ctx i) (apply ctx o)
+--  Type.App' x y -> Type.app (apply ctx x) (apply ctx y)
+--  Type.Ann' v k -> Type.ann (apply ctx v) k
+--  Type.Effect' es t -> Type.effect (map (apply ctx) es) (apply ctx t)
+--  Type.ForallNamed' v t' -> Type.forall v (apply ctx t')
+--  _ -> error $ "Match error in Context.apply: " ++ show t
+--
 -- | `subtype ctx t1 t2` returns successfully if `t1` is a subtype of `t2`.
 -- This may have the effect of altering the context.
 subtype :: forall v loc . (Eq loc, Var v) => loc -> Type v loc -> Type v loc -> M v loc ()
@@ -418,8 +433,6 @@ subtype loc tx ty = withinSubtype tx ty $
          es2' = map (apply ctx) es2
      _abilityCheck' es2' es1'
   go _ _ _ = fail "not a subtype"
-  apply = _todoApply
-
 
 -- abilityCheck' :: Var v => [Type v] -> [Type v] -> M v ()
 -- abilityCheck' ambient requested = do