"Set π != Set" when compiling

[JoeyEremondi]

I'm very excited to use this, and I'm slowly making progress, but I'm hitting roadblocks again:

Minimal Example:

import Generic.Lib.Prelude as Generic
open import Generic.Main using (deriveEqTo)
open import Data.Vec as Vec
open import Data.Nat

data BaseKind : Set where
  TypeKind : BaseKind

instance
    EqBaseKind : Generic.Eq (BaseKind)
    unquoteDef EqBaseKind = deriveEqTo EqBaseKind (quote BaseKind)

data Kind : Set where
  ArrowKind : {n : ℕ } -> Vec Kind n -> BaseKind -> Kind

instance
    EqKind : Generic.Eq (Kind)
    unquoteDef EqKind = deriveEqTo EqKind (quote Kind)

gives the error:

Set π != Set
when checking that the expression P has type Set Generic.lzero

It's also entirely possible that I'm misusing something, I'm still pretty new to Agda.

[JoeyEremondi]

I forgot to mention, I get this on 2.5.2 and 2.6.0 (master)

[effectfully]

In the first place this library is an investigation of how practical descriptions (as seen in The Gentle Art of Levitation and elsewhere) are. For your example to type check an internal representation of data types must incorporate the notion of strict positivity. This is because in

data Kind : Set where
  ArrowKind : {n : ℕ} -> Vec Kind n -> BaseKind -> Kind

Kind occurs inductively inside Vec. Agda is able to see that this is strictly positive, because Agda keeps track of polarity of parameters of data types (but she doesn't do so for indices, so if Vec has this declaration: data Vec : Set -> ℕ -> Set, Kind wouldn't even type check). Descriptions are not capable of that. There are certain encodings (see e.g. Generic Programming with Indexed Functors) that allow to find a representation of a type like your Kind, but those encodings have their own problems.

Besides, even Agda has problems with data types like Kind. If you try to define a function like

mapBaseKind : (BaseKind -> BaseKind) -> Kind -> Kind

which transforms each BaseKind into another BaseKind (assuming you have one) in a Kind, a straightforward attempt won't succeed due to termination issues. I'm deriving generic folds somewhere in the library, so it would be a problem too.

Finally, there is no Eq instance for Vec in scope (which unlike the problems above can be easily fixed, though).

Theoretically, it's possible to transform Kind into two mutually defined data types (which is roughly what you would do to define provably terminating mapBaseKind -- only with functions), i.e. inline Vec Kind into a separate data definition, so then you can derive equality for these two data types, but I didn't try to implement deriving for mutually defined data types.

But why do you want to define Kind like this? I don't remember seeing types or kinds being defined in spine form. Is the usual definition

data Kind : Set where
  BaseKind : Kind
  Arrow    : Kind -> Kind -> Kind

not appropriate in your case?

Thank you for the report. In any case the showed error is silly.