Generic
Generic copied to clipboard
"Set π != Set" when compiling
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.