`ghost` annotation is not always required in declaration of variables of ghost type

[jcp19]

Gobra correctly rejects the following program with a type error:

func f() {
    var y dict[int]int = dict[int]int{}
}

Error

ghost error: expected an actual type but found dict[int]int
[info]     var y dict[int]int = dict[int]int{}

Surprisingly, Gobra does not report a type error if we omit the type in the variable declaration:

func f() {
    var y = dict[int]int{}
}

[ArquintL]

Huh! Is y considered to be a ghost variable in the case of var y = dict[int]int{}?

I was under the impression that for var variable declarations, ghost is always required to make a variable ghost, which contrasts short variable declarations (using :=) where we infer not only the type but also ghostness.

[jcp19]

Huh! Is y considered to be a ghost variable in the case of var y = dict[int]int{}?

Yes, it may be assigned to in ghost code.

I was under the impression that for var variable declarations, ghost is always required to make a variable ghost, which contrasts short variable declarations (using :=) where we infer not only the type but also ghostness.

That was also my expectation, that's why I opened this issue.