[ fix ] Better error message on derivation of a primitive type

Author: buzden

src/Deriving/DepTyCheck/Gen/ForAllNeededTypes/Impl.idr

@@ -46,7 +46,7 @@ deriveAll weightFunTys decls {cc=(alreadyDerived, _)}= do
       else do
         (niit, cr) <- updateNamesAndConsRecs $ targetType <$> toList toDeriveUnknown
         put (toDeriveUnknown, empty)
-        assert_total $ deriveAll @{niit} @{cr} {cc=(alreadyDerived `union` toDeriveUnknown, %search)} weightFunTys decls
+        assert_total $ deriveAll @{niit} @{cr} {cc=(alreadyDerived, %search)} weightFunTys decls
   where
     deriveOne : GenSignature -> m (List TypeInfo, Decl, Decl)
     deriveOne sig = do
@@ -66,10 +66,12 @@ DeriveBodyForType => ClosuringContext m => Elaboration m => SortedMap GenSignatu
           logValue Details "deptycheck.derive.closuring.external" [sig] "is used as an external generator" $
             (callExternalGen extSig name (var outmostFuelArg) $ rewrite lenEq in values, Just (_ ** extSig.gendOrder))
 
-    -- put to derivation queue if necessary
-    when (not $ List.Set.contains sig %search) $ do
+    -- check if internal generator asked for is for a primitive type
+    when (isTypeInfoPrim sig.targetType) $
+      fail "Cannot derive generator for the primitive type \{show $ extractTargetTyExpr sig.targetType}, use external instead"
 
-      -- remember the task to derive
+    -- remember the task to derive, if necessary
+    when (not $ List.Set.contains sig %search) $ do
       modify $ if isTypeKnown sig.targetType then mapFst $ normalise . List.Set.insert sig else mapSnd $ normalise . List.Set.insert sig
 
     -- call the internal gen

src/Deriving/DepTyCheck/Util/Primitives.idr

@@ -50,3 +50,12 @@ extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Double" ) [
 extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "%World" ) [] [] = primVal $ PrT WorldType
 extractTargetTyExpr $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic "Type"   ) [] [] = type
 extractTargetTyExpr ti = var ti.name
+
+export
+isTypeInfoPrim : TypeInfo -> Bool
+isTypeInfoPrim $ MkTypeInfo (NS (MkNS ["^prim^"]) $ UN $ Basic s) [] [] = True
+isTypeInfoPrim _ = False
+--isTypeInfoPrim = not . isVar . extractTragetTyExpr
+
+0 isTypeInfoPrim_correct : (s : String) -> isTypeInfoPrim (primTypeInfo s) = True
+isTypeInfoPrim_correct s = Refl

tests/derivation/core/trivial 005-neg/DerivedGen.idr

@@ -0,0 +1,18 @@
+module DerivedGen
+
+import RunDerivedGen
+
+%default total
+
+%language ElabReflection
+
+data X = MkX String
+
+checkedGen : Fuel -> Gen MaybeEmpty X
+checkedGen = deriveGen
+
+Show X where
+  show (MkX s) = "MkX \{show s}"
+
+main : IO ()
+main = runGs [ G checkedGen ]

tests/derivation/core/trivial 005-neg/RunDerivedGen.idr

@@ -0,0 +1 @@
+../_common/RunDerivedGen.idr

tests/derivation/core/trivial 005-neg/derive.ipkg

@@ -0,0 +1 @@
+../_common/derive.ipkg

tests/derivation/core/trivial 005-neg/expected

@@ -0,0 +1,12 @@
+1/2: Building RunDerivedGen (RunDerivedGen.idr)
+2/2: Building DerivedGen (DerivedGen.idr)
+Error: While processing right hand side of checkedGen. Error during reflection: Cannot derive generator for the primitive type String, use external instead
+
+DerivedGen:1
+ 08 |
+ 09 | data X = MkX String
+ 10 |
+ 11 | checkedGen : Fuel -> Gen MaybeEmpty X
+ 12 | checkedGen = deriveGen
+                   ^^^^^^^^^
+

tests/derivation/core/trivial 005-neg/run

@@ -0,0 +1 @@
+../_common/run