Internal error with postfix projection

[barrettj12]

I ran the code

open import Relation.Binary.PropositionalEquality using (_≡_)

record Magma : Set₁ where
  field
    A : Set
    _+_ : A → A → A

record CommMagmaFam (I : Set) : Set₁ where
  field
    M : I → Magma
    comm : (i : I) → let open Magma (M i) in
      (a b : M i .A) →
      a + b ≡ b + a

and Agda told me

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full\Agda\TypeChecking\Rules\Application.hs:968:23 in Agda-2.6.3-8qnHSysNZe1HBYMluPboCb:Agda.TypeChecking.Rules.Application

I am running 6cb77e1, using VSCode's agda-mode on Windows 10.

[andreasabel]

Here is a version without the standard-library:

open import Agda.Builtin.Equality using (_≡_)

record Magma : Set₁ where
  field
    A : Set
    _+_ : A → A → A

record CommMagmaFam (I : Set) : Set₁ where
  field
    M : I → Magma
    comm : (i : I) → let open Magma (M i) in
      (a b : M i .A) →
      a + b ≡ b + a

The error given by Agda 2.5.2 - 2.6.1 is:

Set should be a function type, but it isn't
when checking that (M i) is a valid argument to a function of type Set

This is the correct error.
The crash happens starting in 2.6.2.

agda/src/full/Agda/TypeChecking/Rules/Application.hs

Line 968 in 058e350

pr <- fromMaybe __IMPOSSIBLE__ <$> isProjection x

Seems I introduced this regression in 535da23 when fixing #3289.

[andreasabel]

This seems to be the MWE:

record R : Set₁ where
  field A : Set

postulate r : R
open R r

fail : Set
fail = r .A

The scope checker recognizes .A as projection, but then isProjection fails because the open statement brought A : Set into scope, which is clearly not a projection.
Seems like the solution is simply to not throw __IMPOSSIBLE__ at loc.cit., since it is possible if the user made a mistake.