diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index 0b0154d8d..9a2b712ea 100644 --- 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 index f2329f4a1..30fbb9eb0 100644 --- 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 index efb21c56e..71c7da0f9 100644 --- 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 index 8f35a0ac4..bb472c03b 100644 --- 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 index 8f35a0ac4..bb472c03b 100644 --- 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 index 72ccc77a2..299b55a66 100644 --- 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 index 8f7835b38..ce57cd5c7 100644 --- 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 index 8f7835b38..ce57cd5c7 100644 --- 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 index 98eba5a17..643a680c3 100644 --- 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 |