[ derive ] Don't discard types with implciits

src/Deriving/DepTyCheck/Gen/Core/ConsEntry.idr

@@ -28,11 +28,7 @@ canonicConsBody sig name con = do
 
   -- Acquire constructor's return type arguments
   let (conRetTy, conRetTypeArgs) = unAppAny con.type
-  conRetTypeArgs <- for conRetTypeArgs $ \case -- resembles similar management from `Entry` module; they must be consistent
-    PosApp e     => pure e
-    NamedApp _ _ => failAt conFC "Named implicit applications (like to `\{show conRetTy}`) are not supported yet"
-    AutoApp _    => failAt conFC "Auto-implicit applications (like to `\{show conRetTy}`) are not supported yet"
-    WithApp _    => failAt conFC "Unexpected `with` application to `\{show conRetTy}` in a constructor's argument"
+  let conRetTypeArgs = conRetTypeArgs <&> getExpr
 
   -- Match lengths of `conRetTypeArgs` and `sig.targetType.args`
   let Yes conRetTypeArgsLengthCorrect = conRetTypeArgs.length `decEq` sig.targetType.args.length

src/Deriving/DepTyCheck/Gen/Entry.idr

@@ -108,11 +108,7 @@ checkTypeIsGen checkSide sig = do
   let (targetType, targetTypeArgs) = unAppAny targetType
 
   -- check out applications types
-  targetTypeArgs <- for targetTypeArgs $ \case
-    PosApp     arg => pure arg
-    NamedApp n arg => failAt targetTypeFC "Target types with implicit type parameters are not supported yet"
-    AutoApp    arg => failAt targetTypeFC "Target types with `auto` implicit type parameters are not supported yet"
-    WithApp    arg => failAt targetTypeFC "Unexpected `with`-application in the target type"
+  let targetTypeArgs = targetTypeArgs <&> getExpr
 
   ------------------------------------------
   -- Working with the target type familly --

tests/derivation/core/norec t-pi->.. noext 001/expected

@@ -1,12 +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: Target types with implicit type parameters are not supported yet
+Error: While processing right hand side of checkedGen. Error during reflection: Target type `Builtin.(===)` is not a top-level data definition
 
-DerivedGen:9:55--9:60
+DerivedGen:9:39--9:42
  5 | %default total
  6 | 
  7 | %language ElabReflection
  8 | 
  9 | checkedGen : Fuel -> (a, b : Bool) -> Gen MaybeEmpty (a = b)
-                                                           ^^^^^
+                                           ^^^
 

tests/derivation/core/norec t-pi->.. noext 002/expected

@@ -1,12 +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: Target types with implicit type parameters are not supported yet
+Error: While processing right hand side of checkedGen. Error during reflection: Target type `Builtin.(===)` is not a top-level data definition
 
-DerivedGen:10:54--10:59
+DerivedGen:10:38--10:41
  06 | 
  07 | %language ElabReflection
  08 | 
  09 | export
  10 | checkedGen : Fuel -> (a, b : Nat) -> Gen MaybeEmpty (a = b)
-                                                           ^^^^^
+                                           ^^^
 

tests/derivation/core/norec t-pi->.. 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: Named implicit applications (like to `Builtin.Equal`) are not supported yet
+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 | Show (X b1 b2) where

tests/derivation/core/norec t-pi->.. 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: Named implicit applications (like to `Builtin.Equal`) are not supported yet
+Error: While processing right hand side of checkedGen. Error during reflection: Usupported applications to a non-concrete type `a`
 
 DerivedGen:19:14--19:23
  15 |   show (X0 b1 b2 _) = "X0 \{show b1} \{show b2} Refl"

tests/derivation/core/norec t-pi->.. noext 005/DerivedGen.idr

@@ -12,7 +12,7 @@ import RunDerivedGen
 
 data FinEq : Fin n -> Fin n -> Type where
   Here  : FinEq FZ FZ
-  These : FinEq n m -> FinEq (FS n) (FS m)
+  These : {n : Nat} -> {0 i, j : Fin n} -> FinEq i j -> FinEq (FS i) (FS j)
 
 data X : (n : Nat) -> Fin n -> Fin n -> Type where
   MkX : (i1, i2 : Fin n) -> (i1 `FinEq` i2) -> X n i1 i2

tests/derivation/core/norec t-pi->.. noext 005/expected

@@ -1,12 +1,47 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Named implicit applications (like to `DerivedGen.FinEq`) are not supported yet
-
-DerivedGen:14:11--14:22
- 10 | 
- 11 | %language ElabReflection
- 12 | 
- 13 | data FinEq : Fin n -> Fin n -> Type where
- 14 |   Here  : FinEq FZ FZ
-                ^^^^^^^^^^^
-
+Generated values:
+-----
+-----
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+-----
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)

tests/derivation/core/norec t-pi->.. w_ext 002/expected

@@ -1,12 +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: Target types with implicit type parameters are not supported yet
+Error: While processing right hand side of checkedGen. Error during reflection: Target type `Builtin.(===)` is not a top-level data definition
 
-DerivedGen:9:63--9:68
+DerivedGen:9:47--9:50
  5 | %default total
  6 | 
  7 | %language ElabReflection
  8 | 
  9 | checkedGen : DecEq a => Fuel -> (x, y : a) -> Gen MaybeEmpty (x = y)
-                                                                   ^^^^^
+                                                   ^^^
 

tests/derivation/core/norec t-pi->.. w_ext 003/expected

@@ -1,12 +1,47 @@
 1/2: Building RunDerivedGen (RunDerivedGen.idr)
 2/2: Building DerivedGen (DerivedGen.idr)
-Error: While processing right hand side of checkedGen. Error during reflection: Target types with implicit type parameters are not supported yet
-
-DerivedGen:25:81--25:92
- 21 | 
- 22 | Show (X n i1 i2) where
- 23 |   show $ MkX i1 i2 prf = "MkX \{show i1} \{show i2} \{show prf}"
- 24 | 
- 25 | checkedGen : Fuel -> (Fuel -> {n : Nat} -> (i1, i2 : Fin n) -> Gen MaybeEmpty $ FinEq i1 i2) =>
-                                                                                      ^^^^^^^^^^^
-
+Generated values:
+-----
+-----
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+MkX 1 1 These Here
+-----
+-----
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)
+-----
+MkX 2 2 These (These Here)

tests/derivation/least-effort/print/regression/dependent-givens-impl-big/DerivedGen.idr

@@ -0,0 +1,68 @@
+module DerivedGen
+
+import Data.Fin
+
+import Deriving.DepTyCheck.Gen
+
+%default total
+
+data AnyType = PrimTy | RefTy
+
+DecEq AnyType where
+  decEq PrimTy PrimTy = Yes Refl
+  decEq PrimTy RefTy  = No $ \case Refl impossible
+  decEq RefTy  PrimTy = No $ \case Refl impossible
+  decEq RefTy  RefTy  = Yes Refl
+
+namespace MaybeAnyType
+
+  -- specialisation since we don't support polymorphism over types yet
+  public export
+  data MaybeAnyType
+    = Nothing
+    | Just AnyType
+
+  export
+  Injective MaybeAnyType.Just where
+    injective Refl = Refl
+
+  export
+  DecEq MaybeAnyType where
+    decEq Nothing  Nothing  = Yes Refl
+    decEq Nothing  (Just _) = No $ \case Refl impossible
+    decEq (Just _) Nothing  = No $ \case Refl impossible
+    decEq (Just x) (Just y) = decEqCong $ decEq x y
+
+namespace VectMaybeAnyType
+
+  -- specialisation since we don't support polymorphism over types yet
+  public export
+  data VectMaybeAnyType : Nat -> Type where
+    Nil  : VectMaybeAnyType Z
+    (::) : MaybeAnyType -> VectMaybeAnyType n -> VectMaybeAnyType (S n)
+
+  public export
+  index : Fin n -> VectMaybeAnyType n -> MaybeAnyType
+  index FZ     (x::_ ) = x
+  index (FS i) (_::xs) = index i xs
+
+  export
+  Biinjective VectMaybeAnyType.(::) where
+    biinjective Refl = (Refl, Refl)
+
+  export
+  DecEq (VectMaybeAnyType n) where
+    decEq []      []      = Yes Refl
+    decEq (x::xs) (y::ys) = decEqCong2 (decEq x y) (decEq xs ys)
+
+  public export
+  data AtIndex : Fin n -> MaybeAnyType -> VectMaybeAnyType n -> Type where
+    Here  : AtIndex FZ x (x::xs)
+    There : {n : Nat} -> {0 i : Fin n} -> {0 zs : VectMaybeAnyType n} ->
+            AtIndex i x zs -> AtIndex (FS i) x (z::zs)
+
+%language ElabReflection
+
+%logging "deptycheck.derive.print" 5
+%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $
+  Fuel -> {n : Nat} -> (v : VectMaybeAnyType n) -> Gen MaybeEmpty (i ** t ** AtIndex i t v)