[ ux, derive ] Improve an error message of a function in a constructor

buzden · Aug 15, 2024 · 11bb223 · 11bb223
1 parent 7c0168b
commit 11bb223
Show file tree

Hide file tree

Showing 6 changed files with 51 additions and 1 deletion.
diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
@@ -65,7 +65,8 @@ namespace NonObligatoryExts
                                        maybe e pure $ lookupType lhsName -- TODO to support `lhsName` to be a type parameter of type `Type`
               IPrimVal _ (PrT t) => pure $ typeInfoForPrimType t
               IType _            => pure typeInfoForTypeOfTypes
-              lhs                => failAt (getFC lhs) "Only applications to a name is supported, given \{show lhs}"
+              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}"
             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/tests/derivation/least-effort/run/regression/function-in-cons/DerivedGen.idr b/tests/derivation/least-effort/run/regression/function-in-cons/DerivedGen.idr
@@ -0,0 +1,21 @@
+module DerivedGen
+
+import RunDerivedGen
+
+%default total
+
+data X : Type where
+  MkX : (Unit -> Unit) -> X
+
+Show X where
+  show (MkX f) = "MkX f"
+
+%language ElabReflection
+
+checkedGen : Fuel -> Gen MaybeEmpty X
+checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}
+
+main : IO ()
+main = runGs
+  [ G $ \fl => checkedGen fl
+  ]
diff --git a/tests/derivation/least-effort/run/regression/function-in-cons/RunDerivedGen.idr b/tests/derivation/least-effort/run/regression/function-in-cons/RunDerivedGen.idr
@@ -0,0 +1 @@
+../_common/RunDerivedGen.idr
diff --git a/tests/derivation/least-effort/run/regression/function-in-cons/derive.ipkg b/tests/derivation/least-effort/run/regression/function-in-cons/derive.ipkg
@@ -0,0 +1 @@
+../_common/derive.ipkg
diff --git a/tests/derivation/least-effort/run/regression/function-in-cons/expected b/tests/derivation/least-effort/run/regression/function-in-cons/expected
@@ -0,0 +1,25 @@
+1/2: Building RunDerivedGen (RunDerivedGen.idr)
+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
+
+    DerivedGen:8:10--8:22
+     4 | 
+     5 | %default total
+     6 | 
+     7 | data X : Type where
+     8 |   MkX : (Unit -> Unit) -> X
+                  ^^^^^^^^^^^^
+
+Possible error:
+    Error during reflection: No arguments in the generator function signature, at least a fuel argument must be present
+
+    DerivedGen:16:14--16:23
+     12 | 
+     13 | %language ElabReflection
+     14 | 
+     15 | checkedGen : Fuel -> Gen MaybeEmpty X
+     16 | checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}
+                       ^^^^^^^^^
+
diff --git a/tests/derivation/least-effort/run/regression/function-in-cons/run b/tests/derivation/least-effort/run/regression/function-in-cons/run
@@ -0,0 +1 @@
+../_common/run