(* SETUP *)
  Definition ptr : Set := ....
  Declare Scope ptr_scope.
  Bind Scope ptr_scope with ptr.
  Delimit Scope ptr_scope with ptr.
  Notation "p .., o" := (_offset_ptr p o) : ptr_scope.

(* TEST *)
  Definition foo p o : ptr := p .., o.
  Fail Definition foo' p o : ptr :=
    let p' : ptr := (p .., o) in
    p'.
  Definition foo' p o : ptr :=
    let p' : ptr := (p .., o)%ptr in
    p'.