OccursCheck1.agda

-- Andreas, 2012-05-04
-- Occurs check when unifying indices in patterns
{-# OPTIONS --allow-unsolved-metas #-}
-- The option is supplied to force a real error to pass the regression test.
module OccursCheck1 where

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

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

test :
  let X : Nat
      X = _
  in  X == suc X
test = refl
-- should fail with error message indicating no solution possible