more cancellation tests

and fix a FIXME that was making some tests fail

src/type_system/lien_chains.rs

@@ -46,13 +46,28 @@ pub enum Lien {
 
 cast_impl!(Lien);
 
+impl Lien {
+    fn covers(&self, other: &Self) -> bool {
+        match (self, other) {
+            (Lien::Shared(p), Lien::Shared(q)) => p.is_prefix_of(q),
+            (Lien::Shared(_), _) | (_, Lien::Shared(_)) => false,
+            (Lien::Leased(p), Lien::Leased(q)) => p.is_prefix_of(q),
+            (Lien::Leased(_), _) | (_, Lien::Leased(_)) => false,
+            (Lien::Var(v), Lien::Var(w)) => v == w,
+            (Lien::Var(_), _) | (_, Lien::Var(_)) => false,
+            (Lien::Our, Lien::Our) => true,
+        }
+    }
+}
+
 #[derive(Copy, Clone, PartialOrd, Ord, PartialEq, Eq, Debug, Hash)]
 pub struct My();
 
 #[derive(Copy, Clone, PartialOrd, Ord, PartialEq, Eq, Debug, Hash)]
 pub struct Our();
 
 impl LienChain {
+    /// Return a new chain with all members of `liens` applied to `self` via [`Self::apply`][].
     fn apply_all(&self, env: &Env, liens: LienChain) -> Self {
         let mut this = self.clone();
         for lien in liens.vec {
@@ -61,6 +76,8 @@ impl LienChain {
         this
     }
 
+    /// Returns a new chain equal to `self` with `lien` appended;
+    /// if `lien` is shared, this will disregard existing members in `self`.
     fn apply(&self, env: &Env, lien: Lien) -> Self {
         let lien_is_shared = match &lien {
             Lien::Our => true,
@@ -78,13 +95,14 @@ impl LienChain {
         }
     }
 
+    /// Adds `lien` to the chain, but first applies all liens in `pending`
+    /// that are not covered by `lien`.
     fn apply_lien(&self, env: &Env, lien: Lien, pending: &LienChain) -> (Self, LienChain) {
         let mut this = self.clone();
         let mut pending = pending.vec.iter();
 
         while let Some(p) = pending.next() {
-            if *p == lien {
-                // FIXME: should be "p covers lien" (or the reverse?) something.
+            if lien.covers(p) {
                 break;
             }
             this = this.apply(env, p.clone());
@@ -98,6 +116,7 @@ impl LienChain {
         )
     }
 
+    /// Shortcut for [`Self::apply_lien`][] with [`Lien::Var`][].
     fn apply_var(
         &self,
         env: &Env,
@@ -107,6 +126,7 @@ impl LienChain {
         self.apply_lien(env, Lien::Var(var.upcast()), pending)
     }
 
+    /// Shortcut for [`Self::apply_lien`][] with [`Lien::Leased`][].
     fn apply_leased(
         &self,
         env: &Env,
@@ -116,16 +136,19 @@ impl LienChain {
         self.apply_lien(env, Lien::Leased(place.upcast()), pending)
     }
 
+    /// True if this chain is non-empty (and thus does not necessarily represent unique ownership).
     pub fn is_not_my(&self) -> bool {
         !self.vec.is_empty()
     }
 }
 
 impl Lien {
+    /// Creates a new [`Lien::Shared`][].
     pub fn shared(place: impl Upcast<Place>) -> Self {
         Self::Shared(place.upcast())
     }
 
+    /// Creates a new [`Lien::Leased`][].
     pub fn leased(place: impl Upcast<Place>) -> Self {
         Self::Leased(place.upcast())
     }
@@ -211,6 +234,7 @@ pub fn collapse(env: &Env, pairs: Set<(LienChain, LienChain)>) -> Set<LienChain>
 }
 
 judgment_fn! {
+    /// Computes the set of [`TyChain`][]es for a given type.
     pub fn ty_chains(
         env: Env,
         cx: LienChain,
@@ -227,6 +251,7 @@ judgment_fn! {
 }
 
 judgment_fn! {
+    /// Computes the set of [`TyChain`][]es for a given type appearing in the context of `chain` and `pending`.
     fn ty_chains_cx(
         env: Env,
         chain: LienChain,

src/type_system/subtypes.rs

@@ -274,13 +274,17 @@ judgment_fn! {
             (sub_lien_chains(env, _live_after, Our(), Cons(Lien::Shared(_), _)) => env)
         )
 
+        //
+
         (
             (lien_covered_by(lien_a, lien_b) => ())
             (sub_lien_chain_exts(&env, &chain_a, &chain_b) => env)
             --------------------------- ("matched starts")
             (sub_lien_chains(env, _live_after, Cons(lien_a, chain_a), Cons(lien_b, chain_b)) => &env)
         )
 
+        //
+
         (
             (lien_chain_is_leased(&env, &chain_a) => ())
             (if !live_after.is_live(place))

src/type_system/tests/subtyping.rs

@@ -1,6 +1,20 @@
+//! Tests for subtyping. These tests can be grouped into various categories.
+//!
+//! ## Liskov Substitution Principle (LSP)
+//!
+//! The "Liskov Substitution Principle" is that if T1 <: T2, then a value of type T1 can be
+//! substituted for a value of type T2 and nothing can go wrong. The "liskov" directory
+//! aims to systematically explore this area.
+//!
+//! ## Other stuff
+//!
+//! The other tests here need to be categorized. =)
+
 use crate::{dada_lang::term, type_system::check_program};
 use formality_core::{test, test_util::ResultTestExt};
 
+mod liskov;
+
 #[test]
 #[allow(non_snake_case)]
 fn forall_P_give_from_my_d1_P_d2_to_shared_d2() {

src/type_system/tests/subtyping/liskov.rs

@@ -0,0 +1,23 @@
+//! ## Liskov Substitution Principle (LSP)
+//!
+//! The "Liskov Substitution Principle" is that if T1 <: T2, then a value of type T1 can be
+//! substituted for a value of type T2 and nothing can go wrong. This module aims to systematically
+//! explore the various substitution considerations relevant to Dada:
+//!
+//! * [Compatible layout](`compatible_layout`): the most basic is that the layout of the data structure in memory must be compatible.
+//!   This is affected by the permisssion since `leased` structures are represented by pointers but everything
+//!   else is by-value.
+//! * [Permission](`subpermission`): All operations permitted by supertype must be permitted by the subtype (relevant when a value with
+//!   this type is live)
+//!   * This begins with edits on the data structure itself, so `our Foo` cannot be a subtype of `my Foo`
+//!     since the latter permits field mutation.
+//!   * This also includes restrictions on what can be done in the environment. So `shared{d1} Foo` cannot
+//!     be a subtype of `shared{d2} Foo` since the latter permits `d1` to be modified but the subtype does not.
+//!     (The latter also restricts edits to `d2`, but that's ok in the supertype, it can be more restrictive.)
+//! * [Liveness and cancellation](`cancellation`)
+//!   * When variables are dead, subtyping allows for *cancellation*, so e.g. if `d1` is dead,
+//!     then `shared{d1} leased{d2} Foo` is a subtype of `leased{d2} Foo`.
+
+mod cancellation;
+mod compatible_layout;
+mod subpermission;