Surface

trait-decl  ::= attribute* 'pub'? 'trait' Ident generic-params?
                   (':' TypeExpr ('+' TypeExpr)*)?            -- supertraits (requires-constraints)
                   ('{' trait-item* '}')? | ';'               -- empty body = marker trait
trait-item  ::= fn-signature ';'                              -- invocation-plane member ('self' leads)
             |  'mutate' Ident '(' 'self' (',' member-params)? ')' ';'   -- invocation-plane member
             |  'derive' Ident '(' member-params ')' ';'                    -- rule-plane member
             |  'check' Ident '(' member-params ')'
                   ('=>' 'Severity' '::' Ident)? ';'          -- rule-plane member; optional
                                                              -- severity pin (issue #230)
             |  'query' Ident '(' member-params ')' '->' TypeExpr ';'       -- rule-plane member
             -- 'type' Ident ';' / 'const' Ident ':' TypeExpr ';' remain reserved

impl-block      ::= 'impl' generic-params? TypeExpr ('for' TypeExpr)? ('{' … '}')? | ';'
trait-impl-item ::= fn-decl | mutate-decl                     -- full bodies
                 |  derive-decl | check-decl | query-decl     -- full bodies (rule body; select
                                                              -- body for query), Self admitted

When 'for' TypeExpr is present the construct is a trait impl (impl Renewable for Lease) and its items are trait-impl-items; when absent it is a bare impl (impl Lease { … }), whose items parse per impl Type { … } — grouping but are gated at elaboration (OE1326) until inherent members execute. Conformance (Conformance) governs trait impls only. Impls of either form are standpoint-global: declaring one inside a standpoint { … } block is refused at elaboration (per-standpoint impls are an open design question RFD 0026 deliberately does not decide).

• Self resolves only inside trait and impl bodies: in a trait item it is the obligation’s type parameter; in an impl item it denotes the impl’s target type. Misuse is OE0675. A trait member signature must mention Self in at least one parameter position (a member that is not about the implementing type belongs at module level — OE0675 says so). Multiple Self positions are legal.
• Supertraits use : (pub trait Repaintable: Drawable), Rust’s spelling, because they are Rust’s semantics — requires-constraints, not subsumption (Resolution). <: is reserved for the concept lattice.
• Generic parameters remain unbounded-only (Generic parameters); generic members, bounded generics, and trait-side default bodies refuse loudly, never dropped.