[Agda] Unification assumes injective postulates?

[Nils Anders Danielsson]

On 2012-11-16 22:30, Jan Malakhovski wrote:
> "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?

AFAIK unsolved meta-variables can, in some cases, lead to a type error.

-- 
/NAD