Fw: Re: [Agda] Unification assumes injective postulates?

[Jan Malakhovski]

Conversation with Martin Escardo.

Begin forwarded messages:

Date: Wed, 14 Nov 2012 05:15:35 +0300
From: Jan Malakhovski <oxij at oxij.org>
To: Martin Escardo <m.escardo at cs.bham.ac.uk>
Subject: Re: [Agda] Unification assumes injective postulates?

On Wed, 14 Nov 2012 00:40:59 +0000
Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:

> On 13/11/12 23:46, Jan Malakhovski wrote:
> > By the way, I'm still using 2.3.0.1, but there is no mentions about any unification changes in release notes for 2.3.2, so I assume it still works this way.
> 
> FYI: same behaviour as reported by you with 2.3.2.
> 
> Martin
> 

Thanks.

On Wed, 14 Nov 2012 00:47:38 +0000
Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:

> I guess the cause of the problem is that postulated elements of type X 
> are treated as constructors of type X.

Judging from the verbose log, yes, they are.

> (I get the same behaviour as reported by you in the new release.)
> 
> Assuming this guess is correct, this still probably doesn't explain your 
> "with" problem.

The log shows something like this:
* [It tries to unify] (X a b) ~ (X a' b') [where X is a postulate]
* => a ~ a' [a and a' are compound expressions of type Vec, Agda normalizes them, seizes first non common subexpression]
* => [and tries to unify something like] x :: xs ~ y :: ys [where x and y are generated by subexpression, not bound by me]
* => [this gives] x ~ y => surprising unification error for unknown variables.

I think the correct error message for the code I sent earlier should be something like "Cannot decide whether there should be a case for the constructor refl" (assuming non-injective postulates).

> Because this is all guessing, I am not copying this to the agda list.

Yes, but I think this conversation should be forwarded to the list anyway. Would you object? Will you forward it yourself?

Best regards,
  Jan

> On 13/11/12 23:46, Jan Malakhovski wrote:
> > Hello everyone,
> >
> > Without further ado, the following code:
> >
> > ~~~~
> > module UnificationWithPostulates where
> >
> > data _≡_ {A : Set} (x : A) : A → Set where
> >    refl : x ≡ x
> >
> > data ℕ : Set where
> >    zero : ℕ
> >    succ : ℕ → ℕ
> >
> > postulate foo : ℕ → ℕ
> >
> > bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
> > bar refl = {!!}
> > ~~~~
> >
> > fails with:
> > ~~~~
> > zero != succ zero of type ℕ
> > when checking that the pattern refl has type
> > foo zero ≡ foo (succ zero)
> > ~~~~
> >
> > Basically, it sounds like "I have to be inconsistent to allow this match".
> >
> > I bumped upon this behavior while "manually rewriting" an expression with "with" construct in a proof of a considerable size and was quite surprised to see an unification error which mentioned equality failure for the variables that I didn't bind (generated by a proof term deep inside).
> > Running Agda with --verbose=10 helped.
> >
> > It's easy to fix the code above, but I think it's not that easy in the general case.
> > It might not always be possible not to pattern match or to expand a failing postulate.
> >
> > By the way, I'm still using 2.3.0.1, but there is no mentions about any unification changes in release notes for 2.3.2, so I assume it still works this way.
> > Why does it work this way?
> >
> > Best regards,
> >    Jan
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> 
> -- 
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe

Date: Wed, 14 Nov 2012 02:19:38 +0000
From: Martin Escardo <m.escardo at cs.bham.ac.uk>
To: Jan Malakhovski <oxij at oxij.org>
Subject: Re: [Agda] Unification assumes injective postulates?


On 14/11/12 02:15, Jan Malakhovski wrote:
> Yes, but I think this conversation should be forwarded to the list anyway. Would you object? Will you forward it yourself?

Feel free to forward it, but including my reservations.

Best,
Martin