[Agda] Unification assumes injective postulates?

[Jan Malakhovski]

On Fri, 16 Nov 2012 19:53:48 +0100
Nils Anders Danielsson <nad at chalmers.se> wrote:

> On 2012-11-16 16:53, Jan Malakhovski wrote:
> > It looks that
> > ~~~~
> > postulate foo : ℕ → ℕ
> >
> > bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
> > bar refl = {!!}
> > ~~~~
> >
> > and
> >
> > ~~~~
> > module Postulate (foo : ℕ → ℕ) where
> >    bar : foo zero ≡ foo (succ zero) → foo zero ≡ foo (succ zero)
> >    bar refl = {!!}
> > ~~~~
> > work the same way.
> 
> Postulates and parameters are not always treated in the same way (unless
> things have changed):
> 
>    http://code.google.com/p/agda/issues/detail?id=170.
> 

Ouch, sorry, I've missed this one even it was mentioned before. It complicates everything another bit more. The only thing I don't understand there is

"Besides even if we treated postulates like parameters things might break once you start replacing them with actual definitions, since the metavariable solver will behave differently."

What might brake? It's fine if it's only a bunch of unsolved implicit arguments. Might it stop type-checking completely?

Best regards,
  Jan