//! Bijective mapping between types with and without lifetimes.
//!
//! Types that implement [`Static`] contain no lifetimes (other than `'static`).
//! Types that implement [`WithLt`] contain zero, one, or two lifetimes.
//! The [`Raised`] and [`Lowered`] type aliases can be used to switch between the
//! type having the lifetimes and the type that doesn't.
//!
//! In type theory terms, [`Static`] types represent type constructors needing
//! the two lifetimes `'lt` and `'ctx` (where `'ctx` outlives `'lt`).
//! [`WithLt`] represents the types that have a type constructor of the [`Static`]
//! form.

/// Lowers a higher ranked type to one with specific lifetimes.
///
/// This acts to *add* the `'lt` and `'ctx` lifetime to the type.
///
/// Note the `Bound` generic exists for implied lifetime bounds to make
/// `'ctx: 'lt` work with Rust's `for<'a>` syntax.
pub trait Lower<'lt, 'ctx: 'lt, Bound>: 'static {
    /// The lowered type with lifetimes.
    type Lowered: ?Sized + Raise<'lt, 'ctx, &'lt &'ctx (), Raised = Self>;
}

/// Raises a type to one without lifetimes.
///
/// This acts to *subtract* the `'lt` and `'ctx` lifetime from the type.
///
/// Note the `Bound` generic exists for implied lifetime bounds to make
/// `'ctx: 'lt` work with Rust's `for<'a>` syntax.
pub trait Raise<'lt, 'ctx: 'lt, Bound>: 'lt {
    /// The raised type without lifetimes.
    type Raised: ?Sized + Lower<'lt, 'ctx, &'lt &'ctx (), Lowered = Self>;
}

/// A type without lifetimes (other than `'static`).
///
/// These types can be lowered to types with lifetimes using [`Lowered`].
pub trait Static: 'static + for<'lt, 'ctx> Lower<'lt, 'ctx, &'lt &'ctx ()> {}

impl<T: ?Sized> Static for T where T: 'static + for<'lt, 'ctx> Lower<'lt, 'ctx, &'lt &'ctx ()> {}

/// A type with zero, one, or two lifetimes.
///
/// These types can be raised to types without lifetimes using [`Raised`].
pub trait WithLt<'lt, 'ctx: 'lt>: Raise<'lt, 'ctx, &'lt &'ctx ()> {}

impl<'lt, 'ctx: 'lt, T: ?Sized> WithLt<'lt, 'ctx> for T where T: Raise<'lt, 'ctx, &'lt &'ctx ()> {}

/// Add lifetimes to a type without them.
pub type Lowered<'lt, 'ctx, T> = <T as Lower<'lt, 'ctx, &'lt &'ctx ()>>::Lowered;

/// Remove lifetimes from a type with them.
pub type Raised<'lt, 'ctx, T> = <T as Raise<'lt, 'ctx, &'lt &'ctx ()>>::Raised;

fn _is_bijective_raise<'lt, 'ctx: 'lt, T>(x: Lowered<'lt, 'ctx, Raised<'lt, 'ctx, T>>)
where
    T: WithLt<'lt, 'ctx>,
{
    // This assignment shows T == Lowered<Raised<T>>
    let _y: T = x;
}

fn _is_bijective_lower<'lt, 'ctx: 'lt, U>(x: Raised<'lt, 'ctx, Lowered<'lt, 'ctx, U>>)
where
    U: Static,
{
    // This assignment shows U == Raised<Lowered<U>>
    let _y: U = x;
}

// A = set of Static types
// B = set of lifetime types
//
// We only need one of the functions above to show its a bijection.
// If we go a -> b -> a (a: A, b: B) for any a in A
// then we know that there must only exist cycles of length 2.
// This doesn't not however prove by itself that the b we encountered
// is not reused. For that we must consider that we do b -> a using
// Raised which has no information about the a we came from.
// As such, no other a could exist that uses b in it's cycle.
// This proves the two sets are of equal size and that the Lowered
// and Raised form a bijective mapping both ways.
//
// Impossible:
//
// struct A;
// struct B;
// struct C;
//
// impl<'a, 'b> Lower<'a, 'b, &'a &'b ()> for A {
//     type Lowered = B;
// }
//
// impl<'a, 'b> Raise<'a, 'b, &'a &'b ()> for B {
//     type Raised = A;
// }
//
// impl<'a, 'b> Lower<'a, 'b, &'a &'b ()> for C {
//     type Lowered = B;
// }