Merge pull request #5837 from unisonweb/topic/type-errors

Attempt a couple type error improvements

Author: aryairani

parser-typechecker/src/Unison/PrintError.hs

@@ -339,6 +339,26 @@ renderTypeError e env src = case e of
         annotatedAsStyle Type1 src f,
         debugSummary note
       ]
+  ActionRestrictionFailure {..} ->
+    mconcat
+      [ Pr.lines
+          [ "I found an action in a block with a type of:",
+            "",
+            Pr.indentN 4 . style Type1 $ renderType' env foundType,
+            "",
+            showSourceMaybes src
+              [(,Type1) <$> rangeForAnnotated mismatchSite],
+            Pr.wrap . mconcat $
+            [ "All actions are expected to have a type of",
+              style Type2 "Unit",
+              "to catch accidental delayed values. To explicitly",
+              "ignore a result, use:"
+            ],
+            "",
+            Pr.indentN 4 $ style Type1 "_ = <expr>"
+          ],
+        debugSummary note
+      ]
   FunctionApplication {..} ->
     let fte = Type.removePureEffects False ft
         fteFreeVars = Set.map TypeVar.underlying $ ABT.freeVars fte

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

@@ -334,6 +334,7 @@ data PathElement v loc
   | InMatch loc -- location of 1st case body
   | InMatchGuard
   | InMatchBody
+  | InActionRestriction
   deriving (Show)
 
 type ExpectedArgCount = Int
@@ -1275,7 +1276,7 @@ synthesizeWanted tm@(Term.Request' r) =
 synthesizeWanted (Term.Let1Top' top binding boundVarAnn e) = do
   (tbinding, wb) <- synthesizeBinding top binding
   v' <- ABT.freshen e freshenVar
-  when (Var.isAction (ABT.variable e)) $
+  when (Var.isAction (ABT.variable e)) . scope InActionRestriction $
     -- enforce that actions in a block have type ()
     subtype tbinding (DDB.unitType (ABT.annotation binding))
   appendContext [Ann v' boundVarAnn tbinding]
@@ -1428,7 +1429,9 @@ synthesizeWanted e
       outputTypev <- freshenVar (Var.named "match-output")
       let outputType = existential' l B.Blank outputTypev
       appendContext [existential outputTypev]
-      cwant <- checkCases scrutineeType outputType cases
+      cwant <-
+        scope (InMatch (ABT.annotation outputType)) $
+          checkCases scrutineeType outputType cases
       want <- coalesceWanted cwant swant
       ctx <- getContext
       let matchType = apply ctx outputType
@@ -1625,13 +1628,12 @@ checkCases ::
   [Term.MatchCase loc (Term v loc)] ->
   M v loc (Wanted v loc)
 checkCases _ _ [] = pure []
-checkCases scrutType outType cases@(Term.MatchCase _ _ t : _) =
-  scope (InMatch (ABT.annotation t)) $ do
-    mes <- requestType (cases <&> \(Term.MatchCase p _ _) -> p)
-    for_ mes $ \es ->
-      applyM scrutType >>= \sty -> ensureReqEffects sty es
-    scrutType' <- applyM =<< ungeneralize scrutType
-    coalesceWanteds =<< traverse (checkCase scrutType' outType) cases
+checkCases scrutType outType cases = do
+  mes <- requestType (cases <&> \(Term.MatchCase p _ _) -> p)
+  for_ mes $ \es ->
+    applyM scrutType >>= \sty -> ensureReqEffects sty es
+  scrutType' <- applyM =<< ungeneralize scrutType
+  coalesceWanteds =<< traverse (checkCase scrutType' outType) cases
 
 -- Checks a scrutinee type against a list of effects from e.g. a list of cases
 -- from a handler.
@@ -1970,8 +1972,10 @@ annotateLetRecBindings isTop letrec =
         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) $ subtype t (DDB.unitType (ABT.annotation b))
+          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)
@@ -2569,7 +2573,7 @@ checkWanted exact want (Term.Let1Top' top binding boundVarAnn m) t = do
   want <- coalesceWanted wbinding want
   v <- ABT.freshen m freshenVar
   markThenRetractWanted v $ do
-    when (Var.isAction (ABT.variable m)) $
+    when (Var.isAction (ABT.variable m)) . scope InActionRestriction $
       -- enforce that actions in a block have type ()
       subtype tbinding (DDB.unitType (ABT.annotation binding))
     extendContext (Ann v boundVarAnn tbinding)

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

@@ -189,6 +189,11 @@ inCheck = asPathExtractor $ \case
 -- inInstantiateL
 -- inInstantiateR
 
+inActionRestriction :: SubseqExtractor v loc ()
+inActionRestriction = asPathExtractor $ \case
+  C.InActionRestriction -> Just ()
+  _ -> Nothing
+
 inSynthesizeApp :: SubseqExtractor v loc (C.Type v loc, C.Term v loc, Int)
 inSynthesizeApp = asPathExtractor $ \case
   C.InSynthesizeApp t e n -> Just (t, e, n)

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

@@ -44,6 +44,11 @@ data TypeError v loc
         mismatchSite :: C.Term v loc,
         note :: C.ErrorNote v loc
       }
+  | ActionRestrictionFailure
+      { foundType :: C.Type v loc,
+        mismatchSite :: C.Term v loc,
+        note :: C.ErrorNote v loc
+      }
   | FunctionApplication
       { f :: C.Term v loc,
         ft :: C.Type v loc,
@@ -143,6 +148,7 @@ allErrors =
     [ and,
       or,
       cond,
+      actionRestriction,
       matchGuard,
       ifBody,
       listBody,
@@ -347,6 +353,19 @@ existentialMismatch0 em getExpectedLoc = do
       -- todo : save type leaves too
       n
 
+actionRestriction ::
+  (Var v, Ord loc) =>
+  Ex.ErrorExtractor v loc (TypeError v loc)
+actionRestriction = do
+  Ex.unique Ex.inActionRestriction
+  note <- Ex.errorNote
+  mismatchSite <- Ex.innermostTerm
+  path <- Ex.path
+  let subtypes = [ t1 | C.InSubtype t1 _ <- path ]
+  guard . not $ null subtypes
+  let foundType = Type.cleanup $ last subtypes
+  pure $ ActionRestrictionFailure foundType mismatchSite note
+
 ifBody,
   listBody,
   matchBody ::

unison-cli/src/Unison/LSP/FileAnalysis.hs

@@ -286,6 +286,8 @@ analyseNotes fileUri ppe src notes = do
               TypeError.NotFunctionApplication {f} -> singleRange $ ABT.annotation f
               TypeError.AbilityCheckFailure {abilityCheckFailureSite} -> singleRange abilityCheckFailureSite
               TypeError.AbilityEqFailure {abilityCheckFailureSite} -> singleRange abilityCheckFailureSite
+              TypeError.ActionRestrictionFailure {mismatchSite} ->
+                singleRange $ ABT.annotation mismatchSite
               TypeError.AbilityEqFailureFromAp {expectedSite, mismatchSite} -> do
                 let locs = [ABT.annotation expectedSite, ABT.annotation mismatchSite]
                 (r, rs) <- withNeighbours (locs >>= aToR)

unison-src/transcripts/idempotent/fix614.md

@@ -40,14 +40,17 @@ ex2 = do
 ``` ucm :added-by-ucm
   Loading changes detected in scratch.u.
 
-  I found a value  of type:  a1 ->{Stream a1} Unit
-  where I expected to find:  Unit
+  I found an action in a block with a type of:
+
+      a ->{Stream a} Unit
 
       2 |   Stream.emit
       3 |   42
 
-  Hint: Actions within a block must have type Unit.
-        Use _ = <expr> to ignore a result.
+  All actions are expected to have a type of Unit to catch
+  accidental delayed values. To explicitly ignore a result, use:
+
+      _ = <expr>
 ```
 
 We can explicitly ignore an unused result like so:
@@ -96,16 +99,15 @@ ex4 =
 ``` ucm :added-by-ucm
   Loading changes detected in scratch.u.
 
-  I found a value  of type:  [Nat]
-  where I expected to find:  Unit
+  I found an action in a block with a type of:
+
+      [Nat]
 
       2 |   [1,2,3] -- no good
       3 |   ()
 
-    from right here:
-
-      2 |   [1,2,3] -- no good
+  All actions are expected to have a type of Unit to catch
+  accidental delayed values. To explicitly ignore a result, use:
 
-  Hint: Actions within a block must have type Unit.
-        Use _ = <expr> to ignore a result.
+      _ = <expr>
 ```

unison-src/transcripts/idempotent/fix693.md

@@ -43,18 +43,12 @@ h0 req = match req with
 ``` ucm :added-by-ucm
   Loading changes detected in scratch.u.
 
-  Each case of a match / with expression need to have the same
-  type.
-
-  Here, one   is:  Optional b
-  and another is:  Optional a
-
-
-      3 |   { X.x _ c -> _ } -> handle c with h0
-
-    from these spots, respectively:
+  I found a value  of type:  a
+  where I expected to find:  b
 
       1 | h0 : Request {X t} b -> Optional b
+      2 | h0 req = match req with
+      3 |   { X.x _ c -> _ } -> handle c with h0
 ```
 
 This code should not check because `t` does not match `b`.
@@ -69,16 +63,14 @@ h1 req = match req with
 ``` ucm :added-by-ucm
   Loading changes detected in scratch.u.
 
-  Each case of a match / with expression need to have the same
-  type.
-
-  Here, one   is:  Optional b
-  and another is:  Optional t
-
+  I found a value  of type:  t
+  where I expected to find:  b
 
+      1 | h1 : Request {X t} b -> Optional b
+      2 | h1 req = match req with
       3 |   { X.x t _ -> _ } -> handle t with h1
 
-    from these spots, respectively:
+    from right here:
 
       1 | h1 : Request {X t} b -> Optional b
 ```