[ fix ] Fix the support for generated function type arguments

Author: buzden

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

@@ -45,6 +45,11 @@ lookupLengthChecked intSig m = lookup intSig m >>= \(extSig, name) => (name,) <$
                                     Yes prf => Just $ Element extSig prf
                                     No _    => Nothing
 
+considerNewType : Elaboration m => ClosuringContext m => TypeInfo -> m ()
+considerNewType ty = do
+  _ : (NamesInfoInTypes, ConsRecs) <- get
+  when .| not (isTypeKnown ty) .| updateNamesAndConsRecs ty >>= put
+
 DeriveBodyForType => ClosuringContext m => Elaboration m => DerivationClosure m where
 
   needWeightFun ty = when (not !(gets $ contains ty.name)) $ do
@@ -64,7 +69,7 @@ DeriveBodyForType => ClosuringContext m => Elaboration m => DerivationClosure m
     startLoop <- get <* put False
 
     -- update names info in types and cons recs if the asked type is not there
-    _ <- considerNewType sig.targetType
+    considerNewType sig.targetType
 
     -- get the expression of calling the internal gen, derive if necessary
     internalGenCall <- do
@@ -98,12 +103,6 @@ DeriveBodyForType => ClosuringContext m => Elaboration m => DerivationClosure m
 
     where
 
-      considerNewType : TypeInfo -> m (NamesInfoInTypes, ConsRecs)
-      considerNewType ty = do
-        nc : (NamesInfoInTypes, ConsRecs) <- get
-        let False = isTypeKnown ty | True => pure nc
-        updateNamesAndConsRecs sig.targetType >>= \x => put x $> x
-
       deriveOne : (GenSignature, Name) -> m ()
       deriveOne (sig, name) = do
 

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

@@ -48,39 +48,40 @@ record TypeApp (0 con : Con) where
   argHeadType : TypeInfo
   {auto 0 argHeadTypeGood : AllTyArgsNamed argHeadType}
   argApps : Vect argHeadType.args.length .| Either (Fin con.args.length) TTImp
-  determ  : Determination con
 
-getTypeApps : Elaboration m => NamesInfoInTypes => (con : Con) -> m $ Vect con.args.length $ TypeApp con
+getTypeApps : Elaboration m => NamesInfoInTypes => (con : Con) -> m $ Vect con.args.length (Either (FC, String) $ TypeApp con, Determination con)
 getTypeApps con = do
   let conArgIdxs = SortedMap.fromList $ mapI con.args $ \idx, arg => (argName' arg, idx)
 
   -- Analyse that we can do subgeneration for each constructor argument
   -- Fails using `Elaboration` if the given expression is not an application to a type constructor
-  let analyseTypeApp : TTImp -> m $ TypeApp con
+  let analyseTypeApp : TTImp -> m (Either (FC, String) $ TypeApp con, Determination con)
       analyseTypeApp expr = do
         let (lhs, args) = unAppAny expr
+        let as = args.asVect <&> \arg => case getExpr arg of
+                   expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs
+                   expr            => Right expr
         ty <- case lhs of
           IVar _ lhsName     => do let Nothing = lookupType lhsName -- TODO to support `lhsName` to be a type parameter of type `Type`
-                                     | Just found => pure found
+                                     | Just found => pure $ pure found
                                    -- we haven'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 "Unsupported 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, 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
-        let as = rewrite lengthCorrect in args.asVect <&> \arg => case getExpr arg of
-                   expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs
-                   expr            => Right expr
+                                   if isNamespaced lhsName
+                                     then failAt (getFC lhs) "Data type `\{lhsName}` is unavailable at the site of derivation (forgotten import?)"
+                                     else pure $ Left (getFC lhs, "Unsupported applications to a non-concrete type `\{lhsName}` in \{show con.name}")
+          IPrimVal _ (PrT t) => pure $ pure $ typeInfoForPrimType t
+          IType _            => pure $ pure typeInfoForTypeOfTypes
+          lhs@(IPi {})       => pure $ Left (getFC lhs, "Fields with function types are not supported in constructors, like in \{show con.name}")
+          lhs                => pure $ Left (getFC lhs, "Unsupported type of a constructor's \{show con.name} field: \{show lhs}")
+        ta <- Prelude.for ty $ \ty : TypeInfo => do
+          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
+          pure $ MkTypeApp ty $ rewrite lengthCorrect in as
         let strongDetermination = rights as.asList <&> mapMaybe (lookup' conArgIdxs) . allVarNames
         let strongDeterminationWeight = concatMap @{Additive} (max 1 . length) strongDetermination -- we add 1 for constant givens
         let stronglyDeterminedBy = fromList $ join strongDetermination
         let argsDependsOn = fromList (lefts as.asList) `difference` stronglyDeterminedBy
-        pure $ MkTypeApp ty as $ MkDetermination stronglyDeterminedBy argsDependsOn $ argsDependsOn.size + strongDeterminationWeight
+        pure (ta, MkDetermination stronglyDeterminedBy argsDependsOn $ argsDependsOn.size + strongDeterminationWeight)
 
   for con.args.asVect $ analyseTypeApp . type
 
@@ -229,7 +230,7 @@ export
     -------------------------------------------------------------
 
     -- Compute left-to-right need of generation when there are non-trivial types at the left
-    argsTypeApps <- getTypeApps con
+    (argsTypeApps, argsDeterms) <- unzip <$> getTypeApps con
 
     -- Decide how constructor arguments would be named during generation
     let bindNames = argName' <$> fromList con.args
@@ -252,7 +253,8 @@ export
         genForOrder order = map (foldr apply callCons) $ evalStateT givs $ for order $ \genedArg => do
 
           -- Get info for the `genedArg`
-          let MkTypeApp typeOfGened argsOfTypeOfGened _ = index genedArg $ the (Vect _ $ TypeApp con) argsTypeApps
+          let Right $ MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ $ Either _ $ TypeApp con) argsTypeApps
+            | Left (fc, str) => failAt fc str
 
           -- Acquire the set of arguments that are already present
           presentArguments <- get
@@ -308,7 +310,7 @@ export
     --------------------------------------------
 
     -- Compute determination map without weak determination information
-    let determ = insertFrom' empty $ mapI (\i, ta => (i, ta.determ)) argsTypeApps
+    let determ = insertFrom' empty $ withIndex argsDeterms
 
     logPoint Debug "deptycheck.derive.least-effort" [sig, con] "- determ: \{determ}"
     logPoint Debug "deptycheck.derive.least-effort" [sig, con] "- givs: \{givs}"

tests/derivation/core/norec t-pi--.. noext 003/expected

@@ -1,12 +1,7 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Unsupported applications to a non-concrete type `a` in Builtin.Refl
+Error: While processing right hand side of checkedGen. Error during reflection: While processing right hand side of $resolved1,<Builtin.Equal>[0, 1, 2, 3]. While processing right hand side of $resolved1,<Builtin.Equal>[0, 1, 2, 3],<<Builtin.Refl>>. Can't find an implementation for DecEq Type.
 
-DerivedGen:1
- 13 | Show (X b1 b2) where
- 14 |   show (MkX b1 b2 _) = "MkX \{show b1} \{show b2} Refl"
- 15 |
- 16 | checkedGen : Fuel -> (b1 : Bool) -> (b2 : Bool) -> Gen MaybeEmpty (X b1 b2)
- 17 | checkedGen = deriveGen
-                   ^^^^^^^^^
+Deriving.DepTyCheck.Gen.ForOneTypeCon.Impl:1
+                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 

tests/derivation/core/norec t-pi--.. noext 004/expected

@@ -1,12 +1,7 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Unsupported applications to a non-concrete type `a` in Builtin.Refl
+Error: While processing right hand side of checkedGen. Error during reflection: While processing right hand side of $resolved1,<Builtin.Equal>[0, 1, 2, 3]. While processing right hand side of $resolved1,<Builtin.Equal>[0, 1, 2, 3],<<Builtin.Refl>>. Can't find an implementation for DecEq Type.
 
-DerivedGen:1
- 15 |   show (X0 b1 b2 _) = "X0 \{show b1} \{show b2} Refl"
- 16 |   show X1           = "X1"
- 17 |
- 18 | checkedGen : Fuel -> (b1 : Bool) -> (b2 : Bool) -> Gen MaybeEmpty (X b1 b2)
- 19 | checkedGen = deriveGen
-                   ^^^^^^^^^
+Deriving.DepTyCheck.Gen.ForOneTypeCon.Impl:1
+                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 

tests/derivation/least-effort/print/adt/025 given-list-gen/DerivedGen.idr

@@ -0,0 +1,12 @@
+module DerivedGen
+
+import Deriving.DepTyCheck.Gen
+
+%default total
+
+%language ElabReflection
+
+data X : Type -> Type where
+  MkX : Nat -> List a -> X a
+
+%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $ Fuel -> (Fuel -> Gen MaybeEmpty (t ** List t)) => Gen MaybeEmpty (t ** X t)

tests/derivation/least-effort/print/adt/025 given-list-gen/derive.ipkg

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