[Agda] acyclicity of constructors

[Dan Licata]

Hi everyone,  

This morning here at LICS, we were trying a cute little example in
various proof assistants:

Define (a) raw (untyped) syntax for lambda terms, and (b) inference
rules for type assignment, where the type of a lambda-bound variable is
non-deterministically guessed.  Now show that omega (i.e. \ x . x x) is
not well-typed.

In Twelf and Delphin, there's not much to do because (1) the bound
variable has a unique type, which means the typing rule for application
can only be applied by unifying \tau and (\tau arrow \sigma) for some
\tau,\sigma and (2) the coverage checker notices this cyclic equality,
and therefore leaves you with 0 cases to consider.

When James Chapman and I tried the problem in Agda, we couldn't get the
coverage checker to rule out cases automatically based on a cyclic
equation.  The best we came up with was to do the proof of acyclicity
ourselves (see an abstracted version below).

So, two questions:
(1) Is there a better way of handling this right now?

(2) Is this behavior intentional, or just an implementation issue? It
seems that Agda already commits to constructors being acyclic: when we
pattern-matched deep enough to force the cyclic equality, Agda told us
that we couldn't do that because \tau != (\tau arrow \sigma) --- exactly
the unification failure that should rule out the case!

Thanks!
-Dan

module Occurs where

  data Nat : Set where
    Z : Nat
    S : Nat -> Nat

  data Id : Nat -> Nat -> Set where
    Refl : forall {m} -> Id m m 

  data False : Set where

  invert : forall {m n} -> Id (S n) (S m) -> Id n m
  invert Refl = Refl

  -- is there a way to write this without doing the induction?
  acyclic : (n : Nat) -> Id n (S n) -> False
  acyclic Z ()
  acyclic (S n) p = acyclic n (invert p)