⅄ trunk → 25-11-05-difftool

Author: mitchellwrosen

.github/workflows/bundle-ucm.yaml

@@ -24,8 +24,8 @@ jobs:
         os: 
           - ubuntu-24.04
           - ubuntu-24.04-arm
-          - macos-13 # intel
-          - macos-14 # apple silicon
+          - macos-15-intel
+          - macos-latest
           - windows-2025
           # - windows-11-arm # 2025-06-17 apparently there's no stack or ghc builds for arm64 windows
     runs-on: ${{matrix.os}}
@@ -105,8 +105,8 @@ jobs:
         os: 
           - ubuntu-24.04
           - ubuntu-24.04-arm
-          - macos-13
-          - macos-14
+          - macos-15-intel
+          - macos-latest
           - windows-2025
           # - windows-11-arm
     steps:

.github/workflows/ci.yaml

@@ -39,8 +39,8 @@ jobs:
           # While iterating on this file, you can disable one or more of these to speed things up
           - ubuntu-24.04
           - ubuntu-24.04-arm
-          - macos-13
-          - macos-14
+          - macos-15-intel
+          - macos-latest
           - windows-2025
           # - windows-11-arm
     steps:
@@ -210,8 +210,8 @@ jobs:
           # While iterating on this file, you can disable one or more of these to speed things up
           - ubuntu-24.04
           - ubuntu-24.04-arm
-          - macos-13
-          - macos-14
+          - macos-15-intel
+          - macos-latest
           - windows-2025
           # - windows-11-arm
     steps:
@@ -297,8 +297,8 @@ jobs:
           # While iterating on this file, you can disable one or more of these to speed things up
           - ubuntu-24.04
           - ubuntu-24.04-arm
-          - macos-13
-          - macos-14
+          - macos-15-intel
+          - macos-latest
           # - windows-2025 fails! :-\ https://github.com/unisonweb/unison/actions/runs/15706568824/job/44253742036?pr=5765
           # - windows-11-arm
     steps:

.github/workflows/nix-dev-cache.yaml

@@ -23,8 +23,8 @@ jobs:
         os:
           # - ubuntu-24.04 disabling this because it's been failing for a while
           # - ubuntu-24.04-arm https://github.com/unisonweb/unison/issues/5789
-          - macos-13
-          - macos-15
+          - macos-15-intel
+          - macos-latest
     steps:
     - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4
     - name: mount Nix store on larger partition

.github/workflows/tmate.yaml

@@ -9,8 +9,8 @@ on:
         options:
         - ubuntu-24.04
         - ubuntu-24.04-arm
-        - macos-13
-        - macos-14
+        - macos-15-intel
+        - macos-latest
         - windows-2022
         - windows-2025
         - windows-11-arm

.github/workflows/update-transcripts.yaml

@@ -12,7 +12,7 @@ jobs:
     strategy:
       matrix:
         os:
-          - macos-13
+          - macos-15-intel
     steps:
       - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4
       - uses: unisonweb/actions/stack/cache/restore@main

parser-typechecker/src/Unison/PrintError.hs

@@ -75,6 +75,7 @@ import Unison.Util.AnnotatedText qualified as AT
 import Unison.Util.ColorText (Color)
 import Unison.Util.ColorText qualified as Color
 import Unison.Util.Monoid (intercalateMap)
+import Unison.Util.Monoid qualified as Monoid
 import Unison.Util.Pretty (ColorText, Pretty)
 import Unison.Util.Pretty qualified as Pr
 import Unison.Util.Range (Range (..), startingLine)
@@ -332,14 +333,6 @@ renderTypeError e env src = case e of
               " expression ",
               "need to have the same type."
             ]
-  NotFunctionApplication {..} ->
-    mconcat
-      [ "This looks like a function call, but with a ",
-        style Type1 (renderType' env ft),
-        " where the function should be.  Are you missing an operator?\n\n",
-        annotatedAsStyle Type1 src f,
-        debugSummary note
-      ]
   ActionRestrictionFailure {..} ->
     mconcat
       [ Pr.lines
@@ -361,6 +354,87 @@ renderTypeError e env src = case e of
           ],
         debugSummary note
       ]
+  FunctionUnderApplied {..} ->
+    let expectedTypeStr = style Type2 (renderType' env expectedLeaf)
+        actualTypeStr = style ErrorSite (renderType' env foundLeaf)
+     in mconcat
+          [ "This call-site has type " <> actualTypeStr <> ":\n",
+            showSourceMaybes src [styleAnnotated ErrorSite foundLeaf],
+            "\n\n",
+            "But I expected the type " <> expectedTypeStr <> " because of:\n",
+            showSourceMaybes
+              src
+              [ (,Type1) . startingLine <$> (rangeForAnnotated mismatchSite),
+                (,Type2) <$> rangeForAnnotated expectedLeaf
+              ],
+            "\n\n",
+            Pr.lines
+              [ "It looks like the function application is missing these arguments:\n",
+                Pr.indentN 2 $ Monoid.intercalateMap ", " (style Type2 . renderType' env) needArgs
+              ],
+            unitHint,
+            intLiteralSyntaxTip mismatchSite expectedType,
+            debugNoteLoc
+              . mconcat
+              $ [ "\nloc debug:",
+                  "\n  mismatchSite: ",
+                  annotatedToEnglish mismatchSite,
+                  "\n     foundType: ",
+                  annotatedToEnglish foundType,
+                  "\n     foundLeaf: ",
+                  annotatedToEnglish foundLeaf,
+                  "\n  expectedType: ",
+                  annotatedToEnglish expectedType,
+                  "\n  expectedLeaf: ",
+                  annotatedToEnglish expectedLeaf,
+                  "\n"
+                ],
+            debugSummary note
+          ]
+    where
+      unitHintMsg =
+        "\nHint: Actions within a block must have type "
+          <> style Type2 (renderType' env expectedLeaf)
+          <> ".\n"
+          <> "      Use "
+          <> style Type1 "_ = <expr>"
+          <> " to ignore a result."
+      unitHint = if giveUnitHint then unitHintMsg else ""
+      giveUnitHint = case expectedType of
+        Type.Ref' u | u == unitRef -> case mismatchSite of
+          Term.Let1Named' v _ _ -> Var.isAction v
+          _ -> False
+        _ -> False
+  NotFunctionApplication {..} ->
+    case Type.arityIgnoringEffects ft of
+      0 ->
+        mconcat
+          [ "It looks like" <> style ErrorSite " this " <> "expression is being called like a function:\n\n",
+            annotatedAsStyle ErrorSite src f,
+            "\n\nbut the thing being applied has the type:\n\n",
+            style Type2 (renderType' env ft),
+            "\n\nWhich doesn't expect any arguments.",
+            "\n\n",
+            debugSummary note
+          ]
+      arity ->
+        mconcat
+          [ "It looks like" <> style ErrorSite " this " <> "function call:\n\n",
+            annotatedAsStyle ErrorSite src f,
+            "\n\nis being applied to ",
+            Pr.blue $ Pr.shown (length args),
+            " arguments, but it has the type\n\n",
+            Pr.indentN 2 $ style Type2 (renderType' env ft),
+            "\n\nwhich only accepts ",
+            Pr.blue $ Pr.shown arity,
+            maybePlural " argument" arity <> ".\n\n",
+            "Maybe you applied the function to too many arguments?\n\n",
+            debugSummary note
+          ]
+    where
+      maybePlural word n
+        | n == 1 = word
+        | otherwise = word <> "s"
   FunctionApplication {..} ->
     let fte = Type.removePureEffects False ft
         fteFreeVars = Set.map TypeVar.underlying $ ABT.freeVars fte
@@ -454,18 +528,14 @@ renderTypeError e env src = case e of
         "\n\n",
         showSourceMaybes
           src
-          [ -- these are overwriting the colored ranges for some reason?
-            --   (,Color.ForceShow) <$> rangeForAnnotated mismatchSite
-            -- , (,Color.ForceShow) <$> rangeForType foundType
-            -- , (,Color.ForceShow) <$> rangeForType expectedType
-            -- ,
-            (,Type1) . startingLine <$> (rangeForAnnotated mismatchSite),
+          [ (,Type1) . startingLine <$> (rangeForAnnotated mismatchSite),
             (,Type2) <$> rangeForAnnotated expectedLeaf
           ],
         fromOverHere'
           src
           [styleAnnotated Type1 foundLeaf]
           [styleAnnotated Type2 expectedLeaf],
+        missingDelayHint,
         unitHint,
         intLiteralSyntaxTip mismatchSite expectedType,
         debugNoteLoc
@@ -486,6 +556,20 @@ renderTypeError e env src = case e of
         debugSummary note
       ]
     where
+      missingDelayHint = case additionalInfo of
+        Nothing -> ""
+        Just MissingDelay ->
+          Pr.lines
+            [ "I expected the expression to be delayed, but it was not.",
+              "Are you missing a `do`?"
+            ]
+        Just SuperfluousDelay ->
+          Pr.lines
+            [ "",
+              "I didn't expect this expression to be delayed, but it was.",
+              "Are you using a `do` where you don't need one,",
+              "or are you missing a `()` to force an expression?"
+            ]
       unitHintMsg =
         "\nHint: Actions within a block must have type "
           <> style Type2 (renderType' env expectedLeaf)

parser-typechecker/src/Unison/Typechecker.hs

@@ -10,6 +10,7 @@ module Unison.Typechecker
     isEqual,
     isSubtype,
     fitsScheme,
+    isMismatchMissingDelay,
     Env (..),
     Notes (..),
     Resolution (..),
@@ -32,6 +33,7 @@ import Data.Text qualified as Text
 import Data.Tuple qualified as Tuple
 import Unison.ABT qualified as ABT
 import Unison.Blank qualified as B
+import Unison.Builtin.Decls qualified as BuiltinDecls
 import Unison.Codebase.BuiltinAnnotation (BuiltinAnnotation)
 import Unison.Name qualified as Name
 import Unison.Prelude
@@ -43,6 +45,7 @@ import Unison.Syntax.Name qualified as Name (unsafeParseText, unsafeParseVar)
 import Unison.Term (Term)
 import Unison.Term qualified as Term
 import Unison.Type (Type)
+import Unison.Type qualified as Type
 import Unison.Typechecker.Context qualified as Context
 import Unison.Typechecker.TypeLookup qualified as TL
 import Unison.Typechecker.TypeVar qualified as TypeVar
@@ -126,6 +129,33 @@ synthesize ppe pmccSwitch env t =
             (TypeVar.liftTerm t)
    in Result.hoist (pure . runIdentity) $ fmap TypeVar.lowerType result
 
+-- | @subtype a b@ is @Right b@ iff @f x@ is well-typed given
+-- @x : a@ and @f : b -> t@. That is, if a value of type `a`
+-- can be passed to a function expecting a `b`, then `subtype a b`
+-- returns `Right b`. This function returns @Left note@ with information
+-- about the reason for subtyping failure otherwise.
+--
+-- Example: @subtype (forall a. a -> a) (Int -> Int)@ returns @Right (Int -> Int)@.
+-- subtype :: Var v => Type v -> Type v -> Either Note (Type v)
+-- subtype t1 t2 = error "todo"
+-- let (t1', t2') = (ABT.vmap TypeVar.Universal t1, ABT.vmap TypeVar.Universal t2)
+-- in case Context.runM (Context.subtype t1' t2')
+--                      (Context.MEnv Context.env0 [] Map.empty True) of
+--   Left e -> Left e
+--   Right _ -> Right t2
+
+-- | Returns true if @subtype t1 t2@ returns @Right@, false otherwise
+-- isSubtype :: Var v => Type v -> Type v -> Bool
+-- isSubtype t1 t2 = case subtype t1 t2 of
+--   Left _ -> False
+--   Right _ -> True
+
+-- | Returns true if the two type are equal, up to alpha equivalence and
+-- order of quantifier introduction. Note that alpha equivalence considers:
+-- `forall b a . a -> b -> a` and
+-- `forall a b . a -> b -> a` to be different types
+-- equals :: Var v => Type v -> Type v -> Bool
+-- equals t1 t2 = isSubtype t1 t2 && isSubtype t2 t1
 isSubtype :: (Var v) => Type v loc -> Type v loc -> Bool
 isSubtype t1 t2 =
   handleCompilerBug (Context.isSubtype (tvar $ void t1) (tvar $ void t2))
@@ -450,30 +480,12 @@ wellTyped ppe env term =
     enable =
       Context.PatternMatchCoverageCheckAndKindInferenceSwitch'Enabled
 
--- | @subtype a b@ is @Right b@ iff @f x@ is well-typed given
--- @x : a@ and @f : b -> t@. That is, if a value of type `a`
--- can be passed to a function expecting a `b`, then `subtype a b`
--- returns `Right b`. This function returns @Left note@ with information
--- about the reason for subtyping failure otherwise.
---
--- Example: @subtype (forall a. a -> a) (Int -> Int)@ returns @Right (Int -> Int)@.
--- subtype :: Var v => Type v -> Type v -> Either Note (Type v)
--- subtype t1 t2 = error "todo"
--- let (t1', t2') = (ABT.vmap TypeVar.Universal t1, ABT.vmap TypeVar.Universal t2)
--- in case Context.runM (Context.subtype t1' t2')
---                      (Context.MEnv Context.env0 [] Map.empty True) of
---   Left e -> Left e
---   Right _ -> Right t2
-
--- | Returns true if @subtype t1 t2@ returns @Right@, false otherwise
--- isSubtype :: Var v => Type v -> Type v -> Bool
--- isSubtype t1 t2 = case subtype t1 t2 of
---   Left _ -> False
---   Right _ -> True
-
--- | Returns true if the two type are equal, up to alpha equivalence and
--- order of quantifier introduction. Note that alpha equivalence considers:
--- `forall b a . a -> b -> a` and
--- `forall a b . a -> b -> a` to be different types
--- equals :: Var v => Type v -> Type v -> Bool
--- equals t1 t2 = isSubtype t1 t2 && isSubtype t2 t1
+-- | Checks if the mismatch between two types is due to a missing delay, if so returns a tag for which type is
+-- missing the delay
+isMismatchMissingDelay :: (Var v) => Type v loc -> Type v loc -> Maybe (Either (Type v loc) (Type v loc))
+isMismatchMissingDelay typeA typeB
+  | isSubtype (Type.arrow () (Type.ref () BuiltinDecls.unitRef) (typeA $> ())) (typeB $> ()) =
+      Just (Left typeA)
+  | isSubtype (ABT.tm (ABT.tm (Type.Ref BuiltinDecls.unitRef) `Type.Arrow` (typeB $> ()))) (typeA $> ()) =
+      Just (Right typeB)
+  | otherwise = Nothing

parser-typechecker/src/Unison/Typechecker/Context.hs

@@ -2638,13 +2638,16 @@ checkWanted exact want (Term.Lam' boundVarAnn body) (Type.Arrow'' i es o) = do
 checkWanted exact want tm@(Term.Var' _) ty@(Type.Arrow'' i es o) =
   synthesize tm >>= \case
     -- special case to detect quadratic abilities
-    (Type.Arrow'' j fs p, wnew) -> do
+    (ts@(Type.Arrow'' j fs p), wnew) -> do
       ctx <- getContext
-      subtype (apply ctx i) (apply ctx j)
-      ctx <- getContext
-      sub <- subAbilities ((Nothing,) . apply ctx <$> fs) (apply ctx <$> es)
-      ctx <- getContext
-      subtype (apply ctx p) (apply ctx o)
+      sub <- scope (InSubtype ts ty) do
+        -- morally this is a subtype call, but we've expanded it to
+        -- get some better information.
+        subtype (apply ctx i) (apply ctx j)
+        ctx <- getContext
+        sub <- subAbilities ((Nothing,) . apply ctx <$> fs) (apply ctx <$> es)
+        ctx <- getContext
+        sub <$ subtype (apply ctx p) (apply ctx o)
       exactAbilitiesWarning fs es exact sub
       coalesceWanted wnew want
     (u, wnew) -> do
@@ -2681,6 +2684,31 @@ checkWanted _ want e@(Term.Match' scrut cases) t = do
     PatternMatchCoverageCheckAndKindInferenceSwitch'Disabled ->
       pure ()
   pure want
+checkWanted exact want (Term.If' cond t f) ty = do
+  want <-
+    scope InIfCond
+      . checkWanted exact want cond
+      . Type.boolean
+      $ loc cond
+  ty <- applyM ty
+  want <- scope (InIfBody $ loc t) $ checkWantedScoped bexact want t ty
+  ty <- applyM ty
+  scope (InIfBody $ loc f) $ checkWantedScoped bexact want f ty
+  where
+    bexact = isJust exact
+checkWanted exact want (Term.List' es) lty
+  | Type.App' (Type.Ref' r) te <- lty,
+    r == Type.listRef =
+      let f want e = checkWantedScoped bexact want e =<< applyM te
+       in Foldable.foldlM f want es
+  | Type.Var' (TypeVar.Existential _ v) <- lty = do
+      ev <- extendExistential v
+      let te = existentialp (loc lty) ev
+      subtype (Type.app' (Type.ref (loc lty) Type.listRef) te) lty
+      let f want e = checkWantedScoped bexact want e =<< applyM te
+      Foldable.foldlM f want es
+  where
+    bexact = isJust exact
 checkWanted _ want e t = do
   (u, wnew) <- synthesize e
   ctx <- getContext