[ ux ] Change a couple of error messages to be slightly more concrete

buzden · buzden · commit 342ce75a73b8 · 2025-04-23T11:55:57.000+03:00
diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
@@ -63,11 +63,11 @@ getTypeApps con = do
                                    -- we didn't found, failing, there are at least two reasons
                                    failAt (getFC lhs) $ if isNamespaced lhsName
                                      then "Data type `\{lhsName}` is unavailable at the site of derivation (forgotten import?)"
-                                     else "Usupported applications to a non-concrete type `\{lhsName}`"
+                                     else "Usupported applications to a non-concrete type `\{lhsName}` in \{show con.name}"
           IPrimVal _ (PrT t) => pure $ typeInfoForPrimType t
           IType _            => pure typeInfoForTypeOfTypes
-          lhs@(IPi {})       => failAt (getFC lhs) "Fields with function types are not supported in constructors"
-          lhs                => failAt (getFC lhs) "Unsupported type of a constructor field: \{show lhs}"
+          lhs@(IPi {})       => failAt (getFC lhs) "Fields with function types are not supported in constructors, like in \{show con.name}"
+          lhs                => failAt (getFC lhs) "Unsupported type of a constructor's \{show con.name} field: \{show lhs}"
         let Yes lengthCorrect = decEq ty.args.length args.length
           | No _ => failAt (getFC lhs) "INTERNAL ERROR: wrong count of unapp when analysing type application"
         _ <- ensureTyArgsNamed ty
diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsEntry.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsEntry.idr
@@ -48,7 +48,8 @@ canonicConsBody sig name con = do
   --   - something else (cannot manage yet)
   let deepConsApps = sig.givenParams.asVect <&> \idx => do
     let argExpr = conRetTypeArg idx
-    mapFst (\err => ("Argument #\{show idx} is not supported yet, argument expression: \{show argExpr}, reason: \{err}", argExpr)) $
+    mapFst (\err => ("Argument #\{show idx} of \{show con.name} with given type arguments [\{showGivens sig}] is not supported, " ++
+                     "argument expression: \{show argExpr}, reason: \{err}", argExpr)) $
       analyseDeepConsApp True conArgNames argExpr
   let allAppliedFreeNames = foldMap (either .| const empty .| SortedSet.fromList . map fst . fst) deepConsApps
   deepConsApps <- for deepConsApps $ \case
diff --git a/src/Deriving/DepTyCheck/Gen/Derive.idr b/src/Deriving/DepTyCheck/Gen/Derive.idr
@@ -32,14 +32,17 @@ public export %inline
 (.generatedParams) : (sig : GenSignature) -> SortedSet $ Fin sig.targetType.args.length
 sig.generatedParams = fromList (allFins sig.targetType.args.length) `difference` sig.givenParams
 
+export
+showGivens : GenSignature -> String
+showGivens sig = joinBy ", " $ do
+  let uName : Arg -> Maybe UserName
+      uName $ MkArg {name=Just $ UN un, _} = Just un
+      uName _ = Nothing
+  sig.givenParams.asList <&> \idx => maybe (show idx) (\n => "\{show idx}(\{show n})") $ uName $ index' sig.targetType.args idx
+
 export
 SingleLogPosition GenSignature where
-  logPosition sig = do
-    let uName : Arg -> Maybe UserName
-        uName $ MkArg {name=Just $ UN un, _} = Just un
-        uName _ = Nothing
-    let givs = sig.givenParams.asList <&> \idx => maybe (show idx) (\n => "\{show idx}(\{show n})") $ uName $ index' sig.targetType.args idx
-    "\{logPosition sig.targetType}[\{joinBy ", " givs}]"
+  logPosition sig = "\{logPosition sig.targetType}[\{showGivens sig}]"
 
 public export
 Eq GenSignature where
diff --git a/tests/derivation/core/non-cons given match 001-neg/expected b/tests/derivation/core/non-cons given match 001-neg/expected
@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Argument #0 is not supported yet, argument expression: DerivedGen.boolToNat x, reason: name `DerivedGen.boolToNat` is not a constructor
+Error: While processing right hand side of checkedGen. Error during reflection: Argument #0 of DerivedGen.X2 with given type arguments [0] is not supported, argument expression: DerivedGen.boolToNat x, reason: name `DerivedGen.boolToNat` is not a constructor
 
 DerivedGen:1
  12 | 
diff --git a/tests/derivation/core/norec part noext 003/expected b/tests/derivation/core/norec part noext 003/expected
@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `ty`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `ty` in Prelude.Types.Just
 
 DerivedGen:1
  12 | XShow : Show X
diff --git a/tests/derivation/core/norec part noext 004/expected b/tests/derivation/core/norec part noext 004/expected
@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a` in Builtin.MkPair
 
 DerivedGen:1
  13 | XShow = %runElab derive
diff --git a/tests/derivation/core/norec part noext 005/expected b/tests/derivation/core/norec part noext 005/expected
@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a` in Builtin.MkPair
 
 DerivedGen:1
  13 | XShow = %runElab derive
diff --git a/tests/derivation/core/norec part w_ext 001/expected b/tests/derivation/core/norec part w_ext 001/expected
@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `ty`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `ty` in Prelude.Types.Just
 
 DerivedGen:1
  13 | XShow = %runElab derive
diff --git a/tests/derivation/core/norec part w_ext 002/expected b/tests/derivation/core/norec part w_ext 002/expected
@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a` in Builtin.MkPair
 
 DerivedGen:1
  13 | XShow = %runElab derive
diff --git a/tests/derivation/core/norec part w_ext 003/expected b/tests/derivation/core/norec part w_ext 003/expected
@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a` in Builtin.MkPair
 
 DerivedGen:1
  13 | XShow = %runElab derive
diff --git a/tests/derivation/core/norec t-pi--.. noext 003/expected b/tests/derivation/core/norec t-pi--.. noext 003/expected
@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a` in Builtin.Refl
 
 DerivedGen:1
  13 | Show (X b1 b2) where
diff --git a/tests/derivation/core/norec t-pi--.. noext 004/expected b/tests/derivation/core/norec t-pi--.. noext 004/expected
@@ -1,6 +1,6 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a` in Builtin.Refl
 
 DerivedGen:1
  15 |   show (X0 b1 b2 _) = "X0 \{show b1} \{show b2} Refl"
diff --git a/tests/derivation/least-effort/run/regression/function-in-cons/expected b/tests/derivation/least-effort/run/regression/function-in-cons/expected
@@ -2,7 +2,7 @@
 2/2: Building DerivedGen (DerivedGen.idr)
 Error: While processing right hand side of checkedGen. Sorry, I can't find any elaboration which works. All errors:
 Possible error:
-    Error during reflection: Fields with function types are not supported in constructors
+    Error during reflection: Fields with function types are not supported in constructors, like in DerivedGen.MkX
 
     DerivedGen:1
      4 | 
