Hole/`postulate` asymmetry in `@++` checker

[lawcho]

Another surprise from #6385:

{-# OPTIONS --polarity #-}

-- Setup
open import Agda.Builtin.Nat
open import Agda.Builtin.String
-- Non-dependent, strictly-positive pairs
record _×_ (@++ A : Set) (@++ B : Set) : Set where
  field fst : A
  field snd : B
infixr 20 _×_

-- Names of syntax constructors of an ML-like language
data Head : Set where
  ʰlet ʰwhere ʰlam ʰvar ʰapp ʰlit ʰplus : Head

-- -- Passes positivity check:
-- postulate args : @++ Set → Head → Set

-- Fails positivity check:
args : @++ Set → Head → Set
args = {!   !}

-- -- Passes positivity check:
-- args : Set → Head → Set
-- args exp ʰlet    = String × exp × exp
-- args exp ʰwhere  = exp × String × exp
-- args exp ʰlam    = String × exp
-- args exp ʰvar    = String
-- args exp ʰapp    = exp × exp
-- args exp ʰlit    = Nat
-- args exp ʰplus   = exp × exp

-- Data type of Expressions
record Exp (rec : @++ Set → Set) : Set where
  inductive
  field head : Head
  field sub-exprs : args (rec (Exp rec)) head

The error message is

/home/lawrence/pre-release/east/src/burgreport3.agda:36,1-39,46
Exp is not strictly positive, because it occurs
in an argument of a bound variable at position 0 which uses its
argument with polarity ++
in an argument of a metavariable
in the definition of Exp.

Possibly related to #7188.

My Agda version is 0f55d97 of #6385.

I'm reporting via a new issue to avoid blocking the merge (no existing code is broken).