[Agda] Can rigid variables be treated as constructors/postulates?

[Arseniy Alekseyev]

I have the following example, which does not work:

    module test (A B : Set) where

    data U : Set where
      a b : U

    [_] : U → Set
    [_] a = A
    [_] b = B

    f : ∀ u → [ u ] → U
    f u _ = u

    postulate x : A

    zzz = f _ x

Here we have unresolved meta on the last line.
When we change A and B to be constructors with a data keyword (or
postulates), the meta gets resolved. It gets resolved because the
function [_] becomes constructor-headed (A and B become different
constructors).

Does it make sense to treat rigid variables, such as A and B in the
example the same way constructors are treated? Why not?

A related, but separate issue:
http://code.google.com/p/agda/issues/detail?id=796

Cheers!
Arseniy