@@ -1 +1 @@
-81f2478b2f6ca8e038ae9182064d583dc8056a9ab6c32f37096ce11bec6f5545 ab5370655049c955d122d644eb26598258e7998bf91ebc7433f068470a966a9e pass
+6b44977fe76c555d6919a7ea4efe69ee9302c402ef3bec69aec5445076f0f731 ab5370655049c955d122d644eb26598258e7998bf91ebc7433f068470a966a9e pass
@@ -1 +1 @@
-a5f459f7c3bb4ca79684ff1c710e44704c03fb9c09e1ad01e5ef90e04086a04f 7a39b8df88ef160e852c6aac30ee2a8bfdb8074b060d5afc8c72bf5f03d1f0a7 pass
+37ec63df5a1906ffa4520b1c2993a228a8a9555e0415b81198933281b74b6a79 7a39b8df88ef160e852c6aac30ee2a8bfdb8074b060d5afc8c72bf5f03d1f0a7 pass
@@ -1 +1 @@
-8b97c8236ca3229efc479a562ad93b802bbaa8a34fdc2f30efeb5bcf9b53bae6 72c0b9bfd651515ecb3d3f4981a6bdb8c6d52eba2308cd11fea004d31941aeef pass
+11b365a07b04255c18a3acabab1bc76533a6daadff43fe6711c7fc4966a1252a 72c0b9bfd651515ecb3d3f4981a6bdb8c6d52eba2308cd11fea004d31941aeef pass
@@ -1883,28 +1883,30 @@ resetContextAfter x a = do
   setContext ctx
   pure a
 
+type LetRecInfo v loc =
+  (v -> M v loc v) -> M v loc ([((loc, v), Term v loc)], Term v loc)
+
 -- | Synthesize and generalize the type of each binding in a let rec.
 -- Updates the context so that all bindings are annotated with
 -- their type. Also returns the freshened version of `body`.
 -- See usage in `synthesize` and `check` for `LetRec'` case.
 annotateLetRecBindings ::
   (Var v, Ord loc, Semigroup loc) =>
-  Term.IsTop ->
-  ((v -> M v loc v) -> M v loc ([((loc, v), Term v loc)], Term v loc)) ->
-  M v loc (Term v loc)
+  Term.IsTop -> LetRecInfo v loc -> M v loc (Term v loc)
 annotateLetRecBindings isTop letrec =
   -- If this is a top-level letrec, then emit a TopLevelComponent note,
   -- which asks if the user-provided type annotations were needed.
   if isTop
     then do
       -- First, typecheck (using annotateLetRecBindings') the bindings with any
       -- user-provided annotations.
-      (body, vts) <- annotateLetRecBindings' True
+      (body, vts) <- annotateLetRecBindings' letrec True
       -- Then, try typechecking again, but ignoring any user-provided annotations.
       -- This will infer whatever type.  If it altogether fails to typecheck here
       -- then, ...(1)
       withoutAnnotations <-
-        resetContextAfter Nothing $ Just <$> annotateLetRecBindings' False
+        resetContextAfter Nothing $
+          Just <$> annotateLetRecBindings' letrec False
       -- convert from typechecker TypeVar back to regular `v` vars
       let unTypeVar (v, t) = (v, generalizeAndUnTypeVar t)
       case withoutAnnotations of
@@ -1918,58 +1920,147 @@ annotateLetRecBindings isTop letrec =
       pure body
     else do
       -- If this isn't a top-level letrec, then we don't have to do anything special
-      (body, _vts) <- annotateLetRecBindings' True
+      (body, _vts) <- annotateLetRecBindings' letrec True
       pure body
+
+-- A wrapper type for demuxed binding information in a let. Only used
+-- locally.
+data Bindings v loc
+  = Bindings
+  { bnds :: [Term v loc], -- actual bindings
+    bndTyps :: [Type v loc], -- types for the bindings
+    bndVars :: [v], -- variables the bindings are bound to
+    bndVarLocs :: [loc] -- locations of said variables
+  }
+
+demuxBindings :: [(Term v loc, Type v loc, v, loc)] -> Bindings v loc
+demuxBindings = uncurry4 Bindings . unzip4
+
+-- Calculates the associations between variables and their bindings in
+-- a `Bindings`, discarding some of the other information.
+namedBindings :: Bindings v loc -> [(v, Term v loc)]
+namedBindings bs = bndVars bs `zip` bnds bs
+
+-- Helper function for checking recursive let bindings. This is the
+-- part of the check that processes the type of the _bindings_, and
+-- returns information that can be used to subsequently check the
+-- body.
+--
+-- To achieve better results, this classifies the bindings into two
+-- categories
+--
+--   1. Bindings given with completely closed types, that need no
+--      parts inferred.
+--   2. Bindings that need at least some part of the type inferred.
+--
+-- The first category can be checked _last_, under the presumption
+-- that the given types are accurate, because the checking of the
+-- second category has no effect on the types in the first category.
+-- This allows us to _generalize_ the types in the second category
+-- before checking the first category. This is necessary when you have
+-- examples like:
+--
+--   f x = g x
+--   g : a -> b
+--   g x = f x
+--
+-- because otherwise the inferred type of `f` will seem too concrete
+-- for the checking of `g` to succeed.
+--
+-- Note however that "closed" can be somewhat deceptive. The type of
+-- `g` above is actually not closed, because it is shorthand for the
+-- type `a ->{e} b`, where the `e` needs to be inferred. To avoid this
+-- defeating the whole approach, it's advisable to be somewhat
+-- conservative with making up these inference variables. For instance
+--
+--   f : a -> b -> c ->{E} d
+--   f x y z = ...
+--
+-- can be immediately completed to `a ->{} b ->{} c ->{E} d` instead
+-- of making up variables for the two positions that must be pure.
+annotateLetRecBindings' ::
+  (Var v, Ord loc, Semigroup loc) =>
+  LetRecInfo v loc ->
+  Bool ->
+  M v loc (Term v loc, [(v, Type v loc)])
+annotateLetRecBindings' letrec useAnn = do
+  (binds, body) <- letrec freshenVar
+
+  ((allbnds, abnds, ubnds), ctx) <-
+    markThenRetract Var.inferOther $ do
+      binds <- traverse prepare binds
+      let (unanns, anns) = partitionEithers binds
+          ubnds = demuxBindings unanns
+          abnds = demuxBindings anns
+          allbnds = demuxBindings $ map (either id id) binds
+
+      -- check un-annotated bindings against their types
+      appendContext (varAnns allbnds)
+
+      Foldable.for_ (vbts ubnds) \(v, b, t) -> do
+        -- elements of a cycle need to be pure, otherwise order of
+        -- effects is unclear and chaos ensues.
+
+        -- ensure actions in blocks have type ()
+        when (Var.isAction v) . scope InActionRestriction $
+          subtype t (DDB.unitType (ABT.annotation b))
+        insideDef v $ checkScopedWith b t []
+
+      pure (allbnds, abnds, ubnds)
+
+  -- compute generalized types for bindings that needed inference
+  vars <- getVariances
+  let bindingArities = Term.arity <$> bnds ubnds
+      gen bty _arity =
+        generalizeExistentials ctx vars bty
+      gbndTyps = zipWith gen (bndTyps ubnds) bindingArities
+      genAnns =
+        zipWith3 Ann (bndVars ubnds) (bndVarLocs ubnds) gbndTyps
+
+      allAnns = genAnns ++ varAnns abnds
+
+  appendContext allAnns
+
+  -- check annotated bindings
+  _ <- markThenRetract Var.inferOther $ do
+    Foldable.for_ (vbts abnds) \(v, b, t) -> do
+      when (Var.isAction v) . scope InActionRestriction $
+        subtype t (DDB.unitType (ABT.annotation b))
+      insideDef v $ checkScopedWith b t []
+
+  ensureGuardedCycle (namedBindings allbnds)
+
+  let vTypes =
+        zip (bndVars ubnds) gbndTyps
+          ++ zip (bndVars abnds) (bndTyps abnds)
+
+  pure (body, vTypes)
   where
-    annotateLetRecBindings' useUserAnnotations = do
-      (bindings, body) <- letrec freshenVar
-      let vs = map (snd . fst) bindings
-      ((bindings, bindingTypes, vlocs), ctx2) <- markThenRetract Var.inferOther $ do
-        let f ((vloc, v), binding) = case binding of
-              -- If user has provided an annotation, we use that
-              Term.Ann' e t | useUserAnnotations -> do
-                -- Arrows in `t` with no ability lists get an attached fresh
-                -- existential to allow inference of required abilities
-                t2 <- existentializeArrows =<< applyM t
-                pure (Term.ann (loc binding) e t2, t2, vloc)
-              -- If we're not using an annotation, we make one up. There's 2 cases:
-
-              lam@(Term.Lam' {}) ->
-                -- If `e` is a lambda of arity K, we immediately refine the
-                -- existential to `a1 ->{e1} a2 ... ->{eK} r`. This gives better
-                -- inference of the lambda's ability variables in conjunction with
-                -- handling of lambdas in `check` judgement.
-                (lam,,vloc) <$> existentialFunctionTypeFor lam
-              e -> do
-                -- Anything else, just make up a fresh existential
-                -- which will be refined during typechecking of the binding
-                vt <- extendExistential v
-                pure $ (e, existential' (loc binding) B.Blank vt, vloc)
-        (bindings, bindingTypes, vlocs) <- unzip3 <$> traverse f bindings
-        appendContext (zipWith3 Ann vs vlocs bindingTypes)
-        -- check each `bi` against its type
-        Foldable.for_ (zip3 vs bindings bindingTypes) $ \(v, b, t) -> do
-          -- note: elements of a cycle have to be pure, otherwise order of effects
-          -- is unclear and chaos ensues
-
-          -- ensure actions in blocks have type ()
-          when (Var.isAction v) . scope InActionRestriction $
-            subtype t (DDB.unitType (ABT.annotation b))
-          insideDef v $ checkScopedWith b t []
-        ensureGuardedCycle (vs `zip` bindings)
-        pure (bindings, bindingTypes, vlocs)
-      -- compute generalized types `gt1, gt2 ...` for each binding `b1, b2...`;
-      -- add annotations `v1 : gt1, v2 : gt2 ...` to the context
-      vars <- getVariances
-      let bindingArities = Term.arity <$> bindings
-          gen bindingType _arity =
-            generalizeExistentials ctx2 vars bindingType
-          bindingTypesGeneralized = zipWith gen bindingTypes bindingArities
-          annotations = zipWith3 Ann vs vlocs bindingTypesGeneralized
-
-      appendContext annotations
-      let vTypes = vs `zip` bindingTypesGeneralized
-      pure (body, vTypes)
+    closed = Set.null . ABT.freeVars
+    indicate t = if closed t then Right else Left
+
+    varAnns bs = zipWith3 Ann (bndVars bs) (bndVarLocs bs) (bndTyps bs)
+
+    vbts bs = zip3 (bndVars bs) (bnds bs) (bndTyps bs)
+
+    prepare ((vloc, v), binding)
+      -- If a term has an annotation add any missing ability
+      -- annotations. We indicate whether the type is completely
+      -- closed, because such types can be separated out of the
+      -- binding cycle.
+      | useAnn,
+        Term.Ann' e t <- binding = do
+          t <- addAbilities (countLambdas e) =<< applyM t
+          pure $ indicate t (Term.ann (loc binding) e t, t, v, vloc)
+      -- If the term is a lambda, we immediately make a refined type
+      -- for better inference.
+      | Term.Lam' {} <- binding =
+          Left . (binding,,v,vloc)
+            <$> existentialFunctionTypeFor binding
+      -- otherwise just make up a fresh existential and proceed
+      | otherwise = do
+          vt <- extendExistential v
+          pure $ Left (binding, existential' (loc binding) B.Blank vt, v, vloc)
 
 ensureGuardedCycle :: (Var v) => [(v, Term v loc)] -> M v loc ()
 ensureGuardedCycle bindings =
@@ -1984,16 +2075,24 @@ ensureGuardedCycle bindings =
         then pure ()
         else failWith $ UnguardedLetRecCycle (fst <$> notok) bindings
 
-existentialFunctionTypeFor :: (Ord loc, Var v) => Term v loc -> M v loc (Type v loc)
-existentialFunctionTypeFor lam@(Term.LamNamed' v body) = do
-  v <- extendExistential v
+-- Create a n existential type for a lambda term.
+--
+-- Note: for lambdas like `x y z -> ...` only the abilities after z
+-- will ever be non-empty, so we can just make up empty ability lists
+-- for repeated lambdas.
+existentialFunctionTypeFor ::
+  (Ord loc, Var v) => Term v loc -> M v loc (Type v loc)
+existentialFunctionTypeFor lam@(Term.LamsNamed' vs _) = do
+  let expl = existentialp (loc lam)
+  us <- traverse extendExistential vs
   e <- extendExistential Var.inferAbility
-  o <- existentialFunctionTypeFor body
-  pure $
-    Type.arrow
-      (loc lam)
-      (existentialp (loc lam) v)
-      (Type.effect (loc lam) [existentialp (loc lam) e] o)
+  o <- extendExistential Var.inferOutput
+  let f u t =
+        Type.arrow
+          (loc lam)
+          (expl u)
+          (Type.effect (loc lam) [] t)
+  pure $ foldr f (Type.effect (loc lam) [expl e] (expl o)) us
 existentialFunctionTypeFor e = do
   v <- extendExistential Var.inferOutput
   pure $ existentialp (loc e) v
@@ -2004,6 +2103,38 @@ existentializeArrows t = do
   t <- Type.existentializeArrows newVar t
   pure t
 
+-- Adds ability lists to arrows in a type that lack them. Unlike
+-- `existentializeArrows`, this takes a count for a corresponding
+-- repeated lambda, like
+--
+--    w x y z -> ...
+--
+-- since it is impossible for abilities to be used except after `z` in
+-- such a case, this avoids making up variables for them. The `Int`
+-- argument specifies how many repeated variables there are in the
+-- corresponding term.
+addAbilities :: (Var v) => Int -> Type v loc -> M v loc (Type v loc)
+addAbilities ct ty
+  | a <- ABT.annotation ty,
+    Type.ForallsNamed' vs ty <- ty =
+      Type.foralls a vs <$> addAbilities ct ty
+  -- Note: Arrow'' matches even with no abilities, providing []
+  | ct > 1,
+    Type.Arrow'' a es b <- ty = do
+      a <- existentializeArrows a
+      b <- addAbilities (ct - 1) b
+      pure $ Type.arrow ann a (Type.effect ann es b)
+  | otherwise = existentializeArrows ty
+  where
+    ann = ABT.annotation ty
+
+-- Counts the number of iterated lambdas in a term; for use with the
+-- above `addAbilities`
+countLambdas :: Term v loc -> Int
+countLambdas tm
+  | Term.LamsNamed' vs _ <- tm = length vs
+  | otherwise = 0
+
 ungeneralize :: (Var v, Ord loc) => Type v loc -> M v loc (Type v loc)
 ungeneralize t = snd <$> ungeneralize' t
 
@@ -2213,7 +2344,7 @@ checkScoped e (Type.Forall' body) = do
   want <- substAndDefaultWanted want pop
   pure (generalizeP variableP pop ty, want)
 checkScoped e t = do
-  t <- existentializeArrows t
+  t <- addAbilities (countLambdas e) t
   (t,) <$> check e t
 
 checkScopedWith ::
 
@@ -89,15 +89,15 @@ fancyTryEval = reraise << catchAll.impl
 
   The check that
 
-      (Unit ->{IO, Exception} 𝕩88) ->{𝕖82, Exception, 𝕖89, IO} 𝕩88
+      (Unit ->{IO, Exception} 𝕩84) ->{𝕖78, Exception, 𝕖85, IO} 𝕩84
 
   is a subtype of
 
-      (Unit ->{g71, IO, Exception} a68) ->{g71, IO, Exception} a68
+      (Unit ->{g69, IO, Exception} a66) ->{g69, IO, Exception} a66
 
   failed because
 
-      {g71}
+      {g69}
 
   is not a subtype of
 
 
@@ -0,0 +1,31 @@
+``` ucm :hide
+scratch/main> builtins.merge
+```
+
+This transcript tests a type checking issue with recursive lets
+that only have some bindings annotated. In such a scenario,
+checking the whole group at once may cause problems with polymorphic
+annotations, because unification variables will fail to be general
+enough for the polymorphic types.
+
+A better strategy allows sufficiently annotated types to be checked
+separately after generalizing the un-annotated types. Unfortunately,
+omitting ability annotations throws a wrench into this. The checker
+tries to avoid this problem as much as possible, though, so the below
+example should work even though there is a missing ability annotation.
+
+``` unison
+f x = g x x
+
+g : a -> b ->{IO} a
+g x y = f x
+```
+
+``` ucm :added-by-ucm
+  Loading changes detected in scratch.u.
+
+  + f : x ->{IO} x
+  + g : a -> b ->{IO} a
+
+  Run `update` to apply these changes to your codebase.
+```
Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-81f2478b2f6ca8e038ae9182064d583dc8056a9ab6c32f37096ce11bec6f5545 ab5370655049c955d122d644eb26598258e7998bf91ebc7433f068470a966a9e pass`
	`1`	`+6b44977fe76c555d6919a7ea4efe69ee9302c402ef3bec69aec5445076f0f731 ab5370655049c955d122d644eb26598258e7998bf91ebc7433f068470a966a9e pass`
Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-a5f459f7c3bb4ca79684ff1c710e44704c03fb9c09e1ad01e5ef90e04086a04f 7a39b8df88ef160e852c6aac30ee2a8bfdb8074b060d5afc8c72bf5f03d1f0a7 pass`
	`1`	`+37ec63df5a1906ffa4520b1c2993a228a8a9555e0415b81198933281b74b6a79 7a39b8df88ef160e852c6aac30ee2a8bfdb8074b060d5afc8c72bf5f03d1f0a7 pass`
Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-8b97c8236ca3229efc479a562ad93b802bbaa8a34fdc2f30efeb5bcf9b53bae6 72c0b9bfd651515ecb3d3f4981a6bdb8c6d52eba2308cd11fea004d31941aeef pass`
	`1`	`+11b365a07b04255c18a3acabab1bc76533a6daadff43fe6711c7fc4966a1252a 72c0b9bfd651515ecb3d3f4981a6bdb8c6d52eba2308cd11fea004d31941aeef pass`