pub enum ProjectionError {
SelfMessage {
role: Role,
},
EmptyChoice {
from: Role,
to: Role,
},
MergeFailed {
role: Role,
labels: (String, String),
left: Box<SessionType>,
right: Box<SessionType>,
},
UnboundVariable(String),
}Expand description
Negative verdict of the projection / safe-realizability gate.
Variants§
SelfMessage
from == to for some message or choice — protocols at the
global layer don’t model self-talk (it would have no observable
effect; the §41.a algebra has no operational rule for it).
EmptyChoice
Choice { arms: {} } — a choice with no arms has no projection
for the chooser (no internal-choice arm to select).
MergeFailed
The merge condition failed: a role r that doesn’t participate
in a choice p → q saw arms that project to non-equivalent local
types, so it cannot observe which branch p chose. The protocol
is unrealizable.
Fields
labels: (String, String)The two labels whose continuations disagree (deterministic pick: alphabetically first divergent pair).
left: Box<SessionType>The two projections that fail to merge — useful for the type-checker’s diagnostic.
right: Box<SessionType>UnboundVariable(String)
Var(x) reached outside any enclosing Rec(x, _). The global
type is open and has no closed-form projection.
Trait Implementations§
Source§impl Clone for ProjectionError
impl Clone for ProjectionError
Source§fn clone(&self) -> ProjectionError
fn clone(&self) -> ProjectionError
1.0.0 (const: unstable) · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source. Read moreSource§impl Debug for ProjectionError
impl Debug for ProjectionError
Source§impl Display for ProjectionError
impl Display for ProjectionError
impl Eq for ProjectionError
Source§impl Error for ProjectionError
impl Error for ProjectionError
1.30.0 · Source§fn source(&self) -> Option<&(dyn Error + 'static)>
fn source(&self) -> Option<&(dyn Error + 'static)>
1.0.0 · Source§fn description(&self) -> &str
fn description(&self) -> &str
use the Display impl or to_string()
Source§impl PartialEq for ProjectionError
impl PartialEq for ProjectionError
Source§fn eq(&self, other: &ProjectionError) -> bool
fn eq(&self, other: &ProjectionError) -> bool
self and other values to be equal, and is used by ==.impl StructuralPartialEq for ProjectionError
Auto Trait Implementations§
impl Freeze for ProjectionError
impl RefUnwindSafe for ProjectionError
impl Send for ProjectionError
impl Sync for ProjectionError
impl Unpin for ProjectionError
impl UnsafeUnpin for ProjectionError
impl UnwindSafe for ProjectionError
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
Source§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
Source§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
Source§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
key and return true if they are equal.Source§impl<T> Instrument for T
impl<T> Instrument for T
Source§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
Source§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more