[base] Unable to make a functor derivation for some Ctors

[GulinSS]

A sample of issue:

module TestWithDataFunctor

import Deriving.Functor

%language ElabReflection

data D : Type -> Type -> Type where
  D' : a -> b -> D a b

Functor (D Int) where
    map f (D' a b) = D' a (f b)

data C : Type -> Type where
  C' : a -> C a

Functor C where
    map f (C' a) = C' (f a)

data A2 : Type -> Type where
    A2' : (C a) -> (A2 a)

aa2 : Functor A2
aa2 = %runElab derive

data A : Type -> Type where
    A' : (D Int) (C a) -> (A a)

aa : Functor A
aa = %runElab derive

Here aa2 is OK, but aa raises a error:

% rlwrap idris2 -p idris2 --source-dir ./src --check ./src/TestWithDataFunctor.idr --log derive.functor:50
3/3: Building TestWithDataFunctor (./src/TestWithDataFunctor.idr)
LOG derive.functor:1: Deriving Functor for A2
LOG derive.functor.constructors:1:
  A2' : {0 a : Type} -> ({arg:3756} : C a) -> A2 a
LOG derive.functor.clauses:10: A2' (Type, C a)
LOG derive.functor.clauses:10: Exec typeView: []
LOG derive.functor.clauses:10: Exec typeView: []
LOG derive.functor.parameters:20: Functors: []
Bifunctors: []
Parameters: []

LOG derive.functor.clauses:1:
  mapA2 : {0 a, b : Type} -> (a -> b) -> A2 a -> A2 b
  mapA2 f (A2' x1) = A2' (map f x1)
LOG derive.functor:1: Deriving Functor for A
LOG derive.functor.constructors:1:
  A' : {0 a : Type} -> ({arg:3819} : D Int (C a)) -> A a
LOG derive.functor.clauses:10: A' (Type, D Int (C a))
Error: While processing right hand side of aa. Error during reflection: When checking constructor TestWithDataFunctor.A'
When checking argument of type D Int (C a)
Couldn't find a `Functor' instance for the type constructor TestWithDataFunctor.D Int

TestWithDataFunctor:41:6--41:21
 37 | data A : Type -> Type where
 38 |     A' : (D Int) (C a) -> (A a)
 39 |
 40 | aa : Functor A
 41 | aa = %runElab derive

Thanks @spcfox for a more precise minimal sample ❤️ .

[GulinSS]

The case with a presaturated type:

module TestWithDataFunctor

import Deriving.Functor

%language ElabReflection

data D a b = MkD b

Functor (D Int) where
    map f (MkD b) = MkD (f b)

data C a = MkC a

Functor C where
    map f (MkC a) = MkC (f a)

data A2 : Type -> Type where
    A2' : (C a) -> (A2 a)

aa2 : Functor A2
aa2 = %runElab derive

data A : Type -> Type where
    A' : (D Int) (C a) -> (A a)

aa : Functor A
aa = %runElab derive

WithD : Type -> Type
WithD = D Int

data A3 : Type -> Type where
    A3' : WithD (C a) -> (A3 a)

aa3 : Functor A3
aa3 = %runElab derive

WithD introduces a case which might not be covered by resolution the case with (D Int).

[gallais]

It's due to isType only accepting a type constructor applied to a bunch of variables.

This could be relaxed to allow more complex parameters.

[GulinSS]

Going to provide a fix for this

[GulinSS]

@gallais could you take a look here for the review: #3737 ?