Agda-2.3.2.2: test/fail/MatchOnIrrelevantData1.agda

-- Andreas, 2011-10-03
{-# OPTIONS --experimental-irrelevance #-}
module MatchOnIrrelevantData1 where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

-- the index does not determine the constructor

data Fin : Nat -> Set where
  zero : (n : Nat) -> Fin (suc n)
  suc  : (n : Nat) -> Fin n -> Fin (suc n)

-- should fail:
toNat : (n : Nat) → .(Fin n) -> Nat
toNat (suc n) (zero .n) = zero
toNat (suc n) (suc .n i) = suc (toNat n i)

-- Cannot split on argument of irrelevant datatype Fin (suc @0)
-- when checking the definition of toNat