[ fix, ux ] Fix error message when type of con's param is not accessible

buzden · Aug 28, 2024 · 76b7407 · 76b7407
1 parent f4a0b0d
commit 76b7407
Show file tree

Hide file tree

Showing 9 changed files with 17 additions and 10 deletions.
diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
@@ -64,9 +64,12 @@ namespace NonObligatoryExts
           analyseTypeApp expr = do
             let (lhs, args) = unAppAny expr
             ty <- case lhs of
-              IVar _ lhsName     => do let e = failAt (getFC lhs) $ "Only applications to non-polymorphic type constructors are supported"
-                                                                 ++ " at the moment, we found `\{lhsName}`"
-                                       maybe e pure $ lookupType lhsName -- TODO to support `lhsName` to be a type parameter of type `Type`
+              IVar _ lhsName     => do let Nothing = lookupType lhsName -- TODO to support `lhsName` to be a type parameter of type `Type`
+                                         | Just found => pure found
+                                       -- 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}`"
               IPrimVal _ (PrT t) => pure $ typeInfoForPrimType t
               IType _            => pure typeInfoForTypeOfTypes
               lhs@(IPi {})       => failAt (getFC lhs) "Fields with function types are not supported in constructors"

diff --git a/src/Deriving/DepTyCheck/Util/Reflection.idr b/src/Deriving/DepTyCheck/Util/Reflection.idr
@@ -261,6 +261,10 @@ allNameSuffixes nm = do
     [] => n
     ns => NS (MkNS $ reverse ns) n
 
+export
+isNamespaced : Name -> Bool
+isNamespaced = not . null . fst . unNS
+
 ---------------------------------------------------
 --- Working around primitive and special values ---
 ---------------------------------------------------

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: Only applications to non-polymorphic type constructors are supported at the moment, we found `ty`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `ty`
 
 DerivedGen:16:14--16:23
  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: Only applications to non-polymorphic type constructors are supported at the moment, we found `a`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
 
 DerivedGen:17:14--17:23
  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: Only applications to non-polymorphic type constructors are supported at the moment, we found `a`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
 
 DerivedGen:17:14--17:23
  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: Only applications to non-polymorphic type constructors are supported at the moment, we found `ty`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `ty`
 
 DerivedGen:17:14--17:23
  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: Only applications to non-polymorphic type constructors are supported at the moment, we found `a`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
 
 DerivedGen:17:14--17:23
  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: Only applications to non-polymorphic type constructors are supported at the moment, we found `a`
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
 
 DerivedGen:17:14--17:23
  13 | XShow = %runElab derive

diff --git a/tests/derivation/core/typealias con 003-neg/expected b/tests/derivation/core/typealias con 003-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: Only applications to non-polymorphic type constructors are supported at the moment, we found `DerivedGen.NonReducibleUseTypeAlias`
+Error: While processing right hand side of checkedGen. Error during reflection: Data type `DerivedGen.NonReducibleUseTypeAlias` is unavailable at the site of derivation (forgotten import?)
 
 DerivedGen:16:22--16:46
  12 |