[ fix ] Support types with determinable function calls in givens

elab-util-extra/src/Language/Reflection/Expr.idr

@@ -281,7 +281,7 @@ export
 argDeps : (args : List Arg) -> ArgDeps args.length
 argDeps args = do
   let nameToIndices = SortedMap.fromList $ mapI args $ \i, arg => (argName' arg, Fin.Set.singleton i)
-  let args = Vect.fromList args <&> \arg => allVarNames arg.type |> map (fromMaybe empty . lookup' nameToIndices)
+  let args = Vect.fromList args <&> \arg => allVarNames arg.type <&> fromMaybe empty . lookup' nameToIndices
   flip upmapI args $ \i, deps => flip concatMap deps $ \candidates =>
     maybe empty singleton $ last' $ mapMaybe tryToFit $ Fin.Set.toList candidates
 

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

@@ -44,31 +44,32 @@ canonicConsBody sig name con = do
   -- Determine names of the arguments of the constructor (as a function)
   let conArgNames = fromList $ argName' <$> con.args
 
+  -- Determine which arguments are already determined by types of givens
+  let depOfGivs = dependeesOfGivens sig
+
   -- For given arguments, determine whether they are
   --   - just a free name
-  --   - repeated name of another given parameter (need of `decEq`)
+  --   - repeated name of another given parameter (need for `decEq`)
   --   - (maybe, deeply) constructor call (need to match)
-  --   - function call on a free param (need to use "inverted function" filtering trick)
+  --   - a function call to a determined arg (can be calculated, thus need for `decEq`)
+  --   - a function call on a free param (thus, need to use "inverted function" filtering trick; not supported now)
   --   - something else (cannot manage yet, unless it is fully determined by other given arguments)
-  let deepConsApps : Vect _ (DeepConsAnalysisRes True, Maybe String, TTImp) := sig.givenParams.asVect <&> \idx => do
+  deepConsApps : Vect _ $ DeepConsAnalysisRes True <- for sig.givenParams.asVect $ \idx => do
     let argExpr = conRetTypeArg idx
     let (fns, errs) = runWriter {w=List String} $ analyseDeepConsApp True conArgNames argExpr
-    let err = if null errs then Nothing else Just $
+    when (not $ null errs) $ failAt conFC $
       "Argument #\{show idx} of \{show con.name} with given type arguments [\{showGivens sig}] is not supported, " ++
       "argument expression: \{show argExpr}, reason(s): \{joinBy "; " errs}"
-    (fns, err, argExpr)
-  let allAppliedFreeNames = foldMap (SortedSet.fromList . map fst . fst . fst) deepConsApps
-  let bindAppliedFreeNames : TTImp -> TTImp
-      bindAppliedFreeNames orig@(IVar _ n) = if contains n allAppliedFreeNames then bindVar n else orig
-      --                              /---------------------------------------------^^^^^^^
-      -- `bindVar` instead of `var` here is because this expression can be earlier than the real binding, thus undeclared,
-      -- and the compiler turns unnecessary `IBindVar`s into `IVar`s by itself
-      bindAppliedFreeNames x = x
-  deepConsApps <- for deepConsApps $ \case
-    (x, Nothing, _) => pure x
-    (x, Just err, argExpr) => if null $ (allVarNames' argExpr `intersection` conArgNames) `difference` allAppliedFreeNames
-      then pure x
-      else failAt conFC err
+    -- Clean up `MustDecEqWith`s if this argument is determined by givens' types
+    pure $ if not $ contains idx depOfGivs then fns else case fns of
+      (lst ** f) => (map determineMustDecEqs <$> lst ** rewrite lengthMap {f=map determineMustDecEqs} lst in f)
+  let allAppliedFreeNames = foldMap (SortedSet.fromList . map fst . fst) deepConsApps
+  let badDecEqExpr : ConsDetermInfo -> Maybe TTImp
+      badDecEqExpr (MustDecEqWith e) = whenT (not $ null $ (allVarNames' e `intersection` conArgNames) `difference` allAppliedFreeNames) e
+      badDecEqExpr _                 = Nothing
+  for_ deepConsApps $ \(vs ** _) => whenJust (foldAlt' vs $ badDecEqExpr . snd) $ \e => failAt conFC $
+    "Unsupported constructor \{show con.name} with given type arguments [\{showGivens sig}] since it contains " ++
+    "an undetermined non-constructor expression `\{show e}` as a given"
 
   -- Acquire LHS bind expressions for the given parameters
   -- Determine pairs of names which should be `decEq`'ed

src/Deriving/DepTyCheck/Gen/Signature.idr

@@ -55,6 +55,16 @@ Eq GenSignature where (==) = (==) `on` characteristics
 public export
 Ord GenSignature where compare = comparing characteristics
 
+||| Set of type arguments for which there exists a given argument depending on it
+-- This is very similar to `dependees` function from libs, but is takes into account the difference between given and non-given arguments.
+-- Maybe, that function should be generalised and this one to be reimplemented through the generalised one.
+export
+dependeesOfGivens : (sig : GenSignature) -> FinSet sig.targetType.args.length
+dependeesOfGivens sig = do
+  let nameToIndex = SortedMap.fromList $ mapI sig.targetType.args $ \i, arg => (argName' arg, i)
+  let varsInGivens = concatMap (\idx => allVarNames' $ type $ index' sig.targetType.args idx) sig.givenParams
+  fromList $ mapMaybe (lookup' nameToIndex) $ Prelude.toList varsInGivens
+
 appFuel : (topmost : Name) -> (fuel : TTImp) -> TTImp
 appFuel = app . var
 

src/Deriving/DepTyCheck/Util/DeepConsApp.idr

@@ -34,10 +34,17 @@ Cast ConsDetermInfo Bool where
   cast NotDeterminedByType = False
   cast $ MustDecEqWith {}  = False
 
+public export
+determineMustDecEqs : ConsDetermInfo -> ConsDetermInfo
+determineMustDecEqs DeterminedByType    = DeterminedByType
+determineMustDecEqs NotDeterminedByType = NotDeterminedByType
+determineMustDecEqs $ MustDecEqWith {}  = DeterminedByType
+
 export
 Semigroup ConsDetermInfo where
-  x@(MustDecEqWith {}) <+> _ = x
-  _ <+> x@(MustDecEqWith {}) = x
+  x@(MustDecEqWith {}) <+> MustDecEqWith {} = x
+  MustDecEqWith {} <+> DeterminedByType = DeterminedByType
+  DeterminedByType <+> MustDecEqWith {} = DeterminedByType
   DeterminedByType <+> DeterminedByType = DeterminedByType
   NotDeterminedByType <+> x = x
   x <+> NotDeterminedByType = x
@@ -87,14 +94,12 @@ analyseDeepConsApp ccdi freeNames = pass . map (, nub) . isD where
       | _ => bad "not an application to a variable"
 
     -- Check if this is a free name
-    let False = contains lhsName freeNames
-      | True => if null args
-                  then pure $ if ccdi then ([(lhsName, neutral)] ** \f => f FZ) else [lhsName]
-                  else bad "applying free name to some arguments"
+    let False = contains lhsName freeNames && null args
+      | True => pure $ if ccdi then ([(lhsName, neutral)] ** \f => f FZ) else [lhsName]
 
     -- Check that this is an application to a constructor's name
     let Just (conArgs, conType) = lookupCon lhsName <&> \con => (con.args, con.type)
-      | Nothing => bad "name `\{lhsName}` is not a constructor"
+      | Nothing => pure $ if ccdi then ([(MN (show e) 0, MustDecEqWith e)] ** \f => f FZ) else []
 
     -- Acquire type-determination info, if needed
     typeDetermInfo : Vect conArgs.length $ MaybeConsDetermInfo ccdi <-

tests/derivation/core/match-on-function-local-neg/DerivedGen.idr

@@ -0,0 +1,25 @@
+module DerivedGen
+
+import RunDerivedGen
+
+import Data.Fin
+
+%default total
+
+data X : Nat -> Type where
+  MkX  : Fin rc -> X rc
+
+data Y : (f : X rc -> Fin rc) -> X rc -> X rc -> Type where
+  MkY : Y f (MkX (f x)) x
+
+checkedGen : Fuel -> (rc : Nat) -> (r1, r2 : X rc) -> Gen MaybeEmpty (f ** Y f r1 r2)
+checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}
+
+Show (f ** Y f a b) where
+  show (_ ** MkY) = "MkY"
+
+main : IO ()
+main = runGs
+  [ G $ \fl => checkedGen fl 5 (MkX 0) (MkX 3)
+  , G $ \fl => checkedGen fl 5 (MkX 3) (MkX 3)
+  ]

tests/derivation/core/match-on-function-local-neg/RunDerivedGen.idr

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

tests/derivation/core/match-on-function-local-neg/derive.ipkg

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

tests/derivation/core/match-on-function-local-neg/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: Unsupported constructor DerivedGen.MkY with given type arguments [0(rc), 2, 3] since it contains an undetermined non-constructor expression `f x` as a given
+
+    DerivedGen:1
+     09 | data X : Nat -> Type where
+     10 |   MkX  : Fin rc -> X rc
+     11 |
+     12 | data Y : (f : X rc -> Fin rc) -> X rc -> X rc -> Type where
+     13 |   MkY : Y f (MkX (f x)) x
+                  ^^^^^^^^^^^^^^^^^
+
+Possible error:
+    Error during reflection: No arguments in the generator function signature, at least a fuel argument must be present
+
+    DerivedGen:2
+     12 | data Y : (f : X rc -> Fin rc) -> X rc -> X rc -> Type where
+     13 |   MkY : Y f (MkX (f x)) x
+     14 |
+     15 | checkedGen : Fuel -> (rc : Nat) -> (r1, r2 : X rc) -> Gen MaybeEmpty (f ** Y f r1 r2)
+     16 | checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}
+                       ^^^^^^^^^
+

tests/derivation/core/match-on-function-local-neg/run

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

tests/derivation/core/match-on-function-simple-neg-allbad/DerivedGen.idr

@@ -0,0 +1,29 @@
+module DerivedGen
+
+import RunDerivedGen
+
+import Data.Fin
+
+%default total
+
+data X : Nat -> Type where
+  MkX  : Fin rc -> X rc
+
+namespace F
+  export
+  f : X rc -> Fin rc
+  f (MkX x) = x
+
+data Y : X rc -> X rc -> Type where
+  MkY : Y (MkX (f y)) x
+
+checkedGen : Fuel -> (rc : Nat) -> (r1, r2 : X rc) -> Gen MaybeEmpty (Y r1 r2)
+checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}
+
+Show (Y a b) where
+  show MkY = "MkY"
+
+main : IO ()
+main = runGs
+  [ G $ \fl => checkedGen fl 5 (MkX 0) (MkX 3)
+  ]

tests/derivation/core/match-on-function-simple-neg-allbad/RunDerivedGen.idr

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

tests/derivation/core/match-on-function-simple-neg-allbad/derive.ipkg

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

tests/derivation/core/match-on-function-simple-neg-allbad/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: Unsupported constructor DerivedGen.MkY with given type arguments [0(rc), 1, 2] since it contains an undetermined non-constructor expression `DerivedGen.F.f {rc = {rc:1}} y` as a given
+
+    DerivedGen:1
+     14 |   f : X rc -> Fin rc
+     15 |   f (MkX x) = x
+     16 |
+     17 | data Y : X rc -> X rc -> Type where
+     18 |   MkY : Y (MkX (f y)) x
+                  ^^^^^^^^^^^^^^^
+
+Possible error:
+    Error during reflection: No arguments in the generator function signature, at least a fuel argument must be present
+
+    DerivedGen:2
+     17 | data Y : X rc -> X rc -> Type where
+     18 |   MkY : Y (MkX (f y)) x
+     19 |
+     20 | checkedGen : Fuel -> (rc : Nat) -> (r1, r2 : X rc) -> Gen MaybeEmpty (Y r1 r2)
+     21 | checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}
+                       ^^^^^^^^^
+

tests/derivation/core/match-on-function-simple-neg-allbad/run

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

tests/derivation/core/match-on-function-simple-neg-somebad/DerivedGen.idr

@@ -0,0 +1,33 @@
+module DerivedGen
+
+import RunDerivedGen
+
+import Data.Fin
+
+%default total
+
+data X : Nat -> Type where
+  MkX  : Fin rc -> Fin rc -> X rc
+
+namespace F
+  export
+  f : X rc -> Fin rc
+  f (MkX x y) = x
+
+  export
+  g : X rc -> Fin rc
+  g (MkX x y) = y
+
+data Y : X rc -> X rc -> Type where
+  MkY : Y (MkX (f y) (g x)) x
+
+checkedGen : Fuel -> (rc : Nat) -> (r1, r2 : X rc) -> Gen MaybeEmpty (Y r1 r2)
+checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}
+
+Show (Y a b) where
+  show MkY = "MkY"
+
+main : IO ()
+main = runGs
+  [ G $ \fl => checkedGen fl 5 (MkX 0 3) (MkX 3 3)
+  ]

tests/derivation/core/match-on-function-simple-neg-somebad/RunDerivedGen.idr

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

tests/derivation/core/match-on-function-simple-neg-somebad/derive.ipkg

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

tests/derivation/core/match-on-function-simple-neg-somebad/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: Unsupported constructor DerivedGen.MkY with given type arguments [0(rc), 1, 2] since it contains an undetermined non-constructor expression `DerivedGen.F.f {rc = {rc:1}} y` as a given
+
+    DerivedGen:1
+     18 |   g : X rc -> Fin rc
+     19 |   g (MkX x y) = y
+     20 |
+     21 | data Y : X rc -> X rc -> Type where
+     22 |   MkY : Y (MkX (f y) (g x)) x
+                  ^^^^^^^^^^^^^^^^^^^^^
+
+Possible error:
+    Error during reflection: No arguments in the generator function signature, at least a fuel argument must be present
+
+    DerivedGen:2
+     21 | data Y : X rc -> X rc -> Type where
+     22 |   MkY : Y (MkX (f y) (g x)) x
+     23 |
+     24 | checkedGen : Fuel -> (rc : Nat) -> (r1, r2 : X rc) -> Gen MaybeEmpty (Y r1 r2)
+     25 | checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}
+                       ^^^^^^^^^
+

tests/derivation/core/match-on-function-simple-neg-somebad/run

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

tests/derivation/core/non-cons given match 001-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: Argument #0 of DerivedGen.X2 with given type arguments [0] is not supported, argument expression: DerivedGen.boolToNat x, reason(s): name `DerivedGen.boolToNat` is not a constructor
+Error: While processing right hand side of checkedGen. Error during reflection: Unsupported constructor DerivedGen.X2 with given type arguments [0] since it contains an undetermined non-constructor expression `DerivedGen.boolToNat x` as a given
 
 DerivedGen:1
  12 |

tests/derivation/least-effort/print/regression/match-on-function-local-complex/DerivedGen.idr

@@ -0,0 +1,18 @@
+module DerivedGen
+
+import Deriving.DepTyCheck.Gen
+
+import Data.Fin
+
+%default total
+
+%language ElabReflection
+
+data X : Nat -> Type where
+  MkX  : Fin rc -> X rc
+
+data Y : (f : X rc -> Fin rc) -> X rc -> X rc -> Type where
+  MkY : Y f (MkX (f x)) x
+
+%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $
+  Fuel -> (rc : Nat) -> (f : X rc -> Fin rc) -> (r1, r2 : X rc) -> Gen MaybeEmpty (Y f r1 r2)

tests/derivation/least-effort/print/regression/match-on-function-local-complex/derive.ipkg

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