Fix misleading error message in pattern constructor type-checking (#6126)

CONTRIBUTORS.markdown

@@ -101,3 +101,4 @@ The format for this list: name, GitHub handle
 * Taylor Fausak (@tfausak)
 * Gabriel Anderson (@andgate)
 * Alistair Roche (@aroche-p)
+* Muhammet Mustafa Senoglu (@mmustafasenoglu)

parser-typechecker/src/Unison/PrintError.hs

@@ -441,13 +441,16 @@ renderTypeError e env src = case e of
         fteFreeVars = Set.map TypeVar.underlying $ ABT.freeVars fte
         showVar (v, _t) = Set.member v fteFreeVars
         solvedVars' = filter showVar solvedVars
+        fname = case patternCtor of
+          Just ref -> showConstructor env ref
+          Nothing -> renderTerm env f
      in mconcat
           [ Pr.lines
               [ Pr.wrap $
                   "The "
                     <> ordinal argNum
                     <> " argument to "
-                    <> Pr.backticked (style ErrorSite (renderTerm env f)),
+                    <> Pr.backticked (style ErrorSite fname),
                 "",
                 "          has type:  " <> style Type2 (renderType' env foundType),
                 "    but I expected:  " <> style Type1 (renderType' env expectedType),

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

@@ -347,6 +347,7 @@ data PathElement v loc
   | InMatchGuard
   | InMatchBody
   | InActionRestriction
+  | InPatternApply ConstructorReference
   deriving (Show)
 
 type ExpectedArgCount = Int
@@ -1917,7 +1918,7 @@ checkPattern scrutineeType p =
             -- refinement then fails on its own (the branches disagree), which is
             -- the signal that the scrutinee needs a type annotation.
             overallGen <- generalizeIndex overall0
-            subtype st0 overallGen
+            scope (InPatternApply ref) $ subtype st0 overallGen
           else
             if gadtConstructorPinsIndex dct
               then do
@@ -1936,12 +1937,12 @@ checkPattern scrutineeType p =
                     appendContext refs
                     st <- applyM scrutineeType
                     ov <- applyM overall
-                    subtype st ov
+                    scope (InPatternApply ref) $ subtype st ov
               else do
                 -- Ordinary (non-pinning) ADT constructor: no index to refine, so
                 -- behavior is unchanged.
                 st <- applyM scrutineeType
-                subtype st overall
+                scope (InPatternApply ref) $ subtype st overall
       pure vs
     Pattern.As loc p' -> do
       v <- getAdvance p

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

@@ -228,6 +228,11 @@ inMatchBody = asPathExtractor $ \case
   C.InMatchBody -> Just ()
   _ -> Nothing
 
+inPatternApply :: SubseqExtractor v loc ConstructorReference
+inPatternApply = asPathExtractor $ \case
+  C.InPatternApply ref -> Just ref
+  _ -> Nothing
+
 inMatch, inVector, inIfBody :: SubseqExtractor v loc loc
 inMatch = asPathExtractor $ \case
   C.InMatch loc -> Just loc

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

@@ -4,6 +4,7 @@ module Unison.Typechecker.TypeError where
 
 import Data.List.NonEmpty (NonEmpty)
 import Unison.ABT qualified as ABT
+import Unison.ConstructorReference (ConstructorReference)
 import Unison.KindInference (KindError)
 import Unison.Pattern (Pattern)
 import Unison.Prelude hiding (whenM)
@@ -67,7 +68,8 @@ data TypeError v loc
         expectedType :: C.Type v loc,
         leafs :: Maybe (C.Type v loc, C.Type v loc), -- found, expected
         solvedVars :: [(v, C.Type v loc)],
-        note :: C.ErrorNote v loc
+        note :: C.ErrorNote v loc,
+        patternCtor :: Maybe ConstructorReference
       }
   | NotFunctionApplication
       { f :: C.Term v loc,
@@ -181,6 +183,7 @@ allErrors =
       ifBody,
       listBody,
       matchBody,
+      applyingPatternConstructor,
       applyingFunction,
       applyingNonFunction,
       generalMismatch,
@@ -500,6 +503,7 @@ applyingFunction = do
         ((\(a, b) -> (cleanup a, cleanup b)) <$> leafs)
         (second cleanup <$> solvedVars)
         n
+        Nothing
 
 inSubtypes ::
   Ex.SubseqExtractor
@@ -516,3 +520,42 @@ inSubtypes = do
         [(found, expected)] -> ((found, expected), Nothing)
         _ -> (last subtypes, Just $ head subtypes)
   pure (found, expected, leaves)
+
+-- | Like 'applyingFunction', but for type mismatches in pattern constructor
+-- arguments. The error path contains 'InPatternApply' between 'InSubtype' and
+-- 'InCheck', which breaks the adjacency chain of 'applyingFunction'.
+--
+-- Path: InSubtype → InPatternApply → InCheck → InSynthesizeApp → InFunctionCall
+applyingPatternConstructor :: forall v loc. (Var v) => Ex.ErrorExtractor v loc (TypeError v loc)
+applyingPatternConstructor = do
+  n <- Ex.errorNote
+  ctx <- Ex.typeMismatch
+  Ex.unique $ do
+    Ex.pathStart
+    (found, expected, leafs) <- inSubtypes
+    ref <- Ex.inPatternApply
+    arg <- fst . head <$> Ex.some Ex.inCheck
+    (_, _, argIndex) <- Ex.inSynthesizeApp
+    (typeVars, f, ft, _args) <- Ex.inFunctionCall
+    let go :: v -> Maybe (v, C.Type v loc)
+        go v = (v,) . Type.getPolytype <$> C.lookupSolved ctx v
+        solvedVars = catMaybes (go <$> typeVars)
+    let vm =
+          Type.cleanupVarsMap $
+            [ft, found, expected]
+              <> (fst <$> toList leafs)
+              <> (snd <$> toList leafs)
+              <> (snd <$> solvedVars)
+        cleanup = Type.cleanupVars1' vm . Type.cleanupAbilityLists
+    pure $
+      FunctionApplication
+        f
+        (cleanup ft)
+        arg
+        argIndex
+        (cleanup found)
+        (cleanup expected)
+        ((\(a, b) -> (cleanup a, cleanup b)) <$> leafs)
+        (second cleanup <$> solvedVars)
+        n
+        (Just ref)

unison-src/transcripts/idempotent/fix-6126-pattern-constructor-error.md

@@ -0,0 +1,55 @@
+Test for https://github.com/unisonweb/unison/issues/6126
+When a pattern constructor receives a wrong argument type, the error message
+should say "The Nth argument to `Constructor`" instead of "The Nth argument to `function`".
+
+``` ucm :hide
+> builtins.merge
+```
+
+``` unison
+type X = X
+type Y k = Y X
+```
+
+``` ucm :added-by-ucm
+  Loading changes detected in scratch.u.
+
+  + type X
+  + type Y k
+
+  Run `update` to apply these changes to your codebase.
+```
+
+``` ucm
+> add
+
+  Okay, I'm searching the branch for code that needs to be
+  updated...
+
+  Done.
+```
+
+This should show "The 1st argument to `Y`" not "The 1st argument to `b`":
+
+``` unison :error
+type X = X
+type Y k = Y X
+
+a =
+  b cases
+    Y (3,4) -> "c"
+
+b : (a -> b) -> c
+b = todo "whatever"
+```
+
+``` ucm :added-by-ucm
+  Loading changes detected in scratch.u.
+
+  The 1st argument to `Y`
+
+            has type:  Tuple
+      but I expected:  X
+
+      8 |     Y (3,4) -> "c"
+```