module Generic.Macro.NegativeTests where

open import Generic.Core
open import Generic.Macro

import Agda.Builtin.Reflection as R
open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Nat using (Nat; zero; suc)
open import Agda.Builtin.Unit using (⊤; tt)

expectNonIndexedRejectionTC : R.Name → R.Term → R.TC ⊤
expectNonIndexedRejectionTC ty hole =
  R.catchTC
    (ensureNonIndexedType ty >>= λ _ → R.returnTC false)
    (R.returnTC true)
  >>= λ where
    true → R.unify hole (R.con (quote tt) [])
    false → R.typeError
      (R.strErr "expected the generic macro to reject a parameterized or indexed datatype" ∷ [])

macro
  expectNonIndexedRejection : R.Name → R.Term → R.TC ⊤
  expectNonIndexedRejection = expectNonIndexedRejectionTC

data Indexed : Nat → Type₀ where
  indexed-zero : Indexed zero
  indexed-suc  : ∀ {n} → Indexed n → Indexed (suc n)

data Parameterized (A : Type₀) : Type₀ where
  parameterized : A → Parameterized A

indexed-is-rejected : ⊤
indexed-is-rejected = expectNonIndexedRejection Indexed

parameterized-is-rejected : ⊤
parameterized-is-rejected = expectNonIndexedRejection Parameterized