UnificationUndecidedForNonStronglyRigidOccurrence.agda

-- Andreas, 2011-04-14
module UnificationUndecidedForNonStronglyRigidOccurrence where

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

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

i : (f : Nat -> Nat)(n : Nat) -> n ≡ f n -> Nat
i f n ()
-- this should fail, since n ≡ f n is not always empty, only in case of f=suc
-- thus, an occurrence does not always mean no match, only strict occurrences
-- mean that.