[Agda] acyclicity of constructors

[Dan Licata]

Conor, thanks for the story.  Makes sense.

Thorsten,

On Jun28, Thorsten Altenkirch wrote:
> I am not sure what precisely you mean by (2)? Certainly yoo shouldn't  
> be allowed to assume that you can solve an acyclic equation either,  
> because this would force the type to be coinductive. I.e. the coverage  
> checking and unification should be agnostic wrt the question whether  
> cyclic equations can be solved.

An example of what I meant is:

  acyclic : (n : Nat) -> Id n (S n) -> False
  acyclic n Refl = ?

to which agda responds:

  /Users/drl/work/cmu/rsh/progind/code/agda/misc/occurs.agda:21,15-23
  n != S n of type Nat
  when checking that the pattern Refl has type Id n (S n)

[What exactly does != mean here?  I'm assuming it's (the failure of)
 unification-modulo-definitional-equality.]

All I was saying is that unification fails, but Agda doesn't use the
unification failure to conclude anything (besides the fact that I can't
write down this case this way).  I'd be happy for it to conclude that
the case is impossible---which is correct in this case because we have a
constructor-path cycle.  

Actually, the corresponding situation for CoNat is puzzling to me.  As
far as I can tell, in Agda right now, you can neither prove nor refute 
(Id n (S n)) for CoNat.

    codata CoNat : Set where
      Z : CoNat
      S : CoNat -> CoNat
  
    data Id : CoNat -> CoNat -> Set where
      Refl : {n : CoNat} -> Id n n 

    omega : CoNat
    omega ~ S omega

    eq : Id omega (S omega)
    eq = Refl -- unification error

    acyclic : (n : CoNat) -> Id n (S n) -> False
    acyclic n Refl = ? -- unification error

Assuming definitional equality is not extended to include things like
'eq', it seems ok to me to allow 'acyclic' to be proved with no cases
(there are no constructors I can write!).  But if you can't prove it
without such an extension to pattern matching, then I guess this is
saying that adding decidability of definitional equality as an axiom
changes provability.

-Dan