Generic icon indicating copy to clipboard operation
Generic copied to clipboard

"Set π != Set" when compiling

Open JoeyEremondi opened this issue 7 years ago • 2 comments

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 avatar Apr 13 '17 02:04 JoeyEremondi