introduce variance predicates and req in classes

src/grammar.rs

@@ -471,4 +471,26 @@ pub enum PredicateKind {
 
     /// `leased(p)` is true for leased types that are always passed by reference.
     Leased,
+
+    /// `relative(p)` is used to express variance.
+    /// Whenever a type `P T` appears in a struct
+    /// and `P != my`, `Relative(T)` must hold.
+    /// This indicates that `T`
+    /// appears in a position that is relative to some
+    /// permission.
+    Relative,
+
+    /// `atomic(p)` is used to express variance.
+    /// It has to hold for all types appearing
+    /// an atomic field.
+    Atomic,
+}
+
+impl PredicateKind {
+    pub fn apply(self, parameter: impl Upcast<Parameter>) -> Predicate {
+        Predicate {
+            kind: self,
+            parameter: parameter.upcast(),
+        }
+    }
 }

src/type_system/classes.rs

@@ -3,9 +3,16 @@ use std::sync::Arc;
 use fn_error_context::context;
 use formality_core::Fallible;
 
-use crate::grammar::{Atomic, ClassDecl, ClassDeclBoundData, FieldDecl, NamedTy, Program, Var};
+use crate::grammar::{
+    Atomic, ClassDecl, ClassDeclBoundData, FieldDecl, NamedTy, PredicateKind, Program, Var,
+};
 
-use super::{env::Env, methods::check_method, predicates::check_predicate, types::check_type};
+use super::{
+    env::Env,
+    methods::check_method,
+    predicates::{check_predicate, prove_predicate},
+    types::check_type,
+};
 
 #[context("check class named `{:?}`", decl.name)]
 pub fn check_class(program: &Arc<Program>, decl: &ClassDecl) -> Fallible<()> {
@@ -23,6 +30,8 @@ pub fn check_class(program: &Arc<Program>, decl: &ClassDecl) -> Fallible<()> {
 
     let class_ty = NamedTy::new(name, &substitution);
 
+    env.add_assumptions(&predicates);
+
     for predicate in predicates {
         check_predicate(&env, &predicate)?;
     }
@@ -50,14 +59,13 @@ fn check_field(class_ty: &NamedTy, env: &Env, decl: &FieldDecl) -> Fallible<()>
 
     env.push_local_variable(Var::This, class_ty)?;
 
-    check_type(env, ty)?;
+    check_type(&*env, ty)?;
 
     match atomic {
         Atomic::No => {}
 
         Atomic::Yes => {
-            // FIXME: Check that any perm/type variables used in this field's type
-            // are declared atomic.
+            prove_predicate(&*env, PredicateKind::Atomic.apply(ty)).check_proven()?;
         }
     }
 

src/type_system/methods.rs

@@ -2,7 +2,8 @@ use fn_error_context::context;
 use formality_core::{Fallible, Upcast};
 
 use crate::grammar::{
-    Block, LocalVariableDecl, MethodDecl, MethodDeclBoundData, NamedTy, ThisDecl, Ty, Var::This,
+    Block, LocalVariableDecl, MethodDecl, MethodDeclBoundData, NamedTy, Predicate, PredicateKind,
+    ThisDecl, Ty, Var::This,
 };
 
 use super::{
@@ -16,7 +17,7 @@ pub fn check_method(class_ty: &NamedTy, env: impl Upcast<Env>, decl: &MethodDecl
 
     let MethodDecl { name: _, binder } = decl;
     let (
-        _,
+        vars,
         MethodDeclBoundData {
             this,
             inputs,
@@ -26,6 +27,19 @@ pub fn check_method(class_ty: &NamedTy, env: impl Upcast<Env>, decl: &MethodDecl
         },
     ) = &env.open_universally(binder);
 
+    // Methods don't really care about variance, so they can assume all their
+    // parameters are relative/atomic for purposes of WF checking.
+    env.add_assumptions(
+        vars.iter()
+            .flat_map(|v| {
+                vec![
+                    Predicate::new(PredicateKind::Relative, &v),
+                    Predicate::new(PredicateKind::Atomic, &v),
+                ]
+            })
+            .collect::<Vec<_>>(),
+    );
+
     check_predicates(&env, predicates)?;
 
     env.add_assumptions(predicates);

src/type_system/predicates.rs

@@ -1,9 +1,10 @@
 use super::{env::Env, types::check_parameter};
 use crate::{
     dada_lang::grammar::UniversalVar,
-    grammar::{Parameter, Predicate, PredicateKind},
+    grammar::{NamedTy, Parameter, Perm, Place, Predicate, PredicateKind, Ty},
     type_system::{
         is_::{is_leased, is_shared},
+        places::place_ty,
         quantifiers::for_all,
     },
 };
@@ -76,5 +77,109 @@ judgment_fn! {
             ---------------------------- ("leased")
             (prove_predicate(env, Predicate { kind: PredicateKind::Leased, parameter: p }) => ())
         )
+
+        (
+            (variance_predicate(env, PredicateKind::Relative, parameter) => ())
+            ---------------------------- ("relative")
+            (prove_predicate(env, Predicate { kind: PredicateKind::Relative, parameter }) => ())
+        )
+
+        (
+            (variance_predicate(env, PredicateKind::Atomic, parameter) => ())
+            ---------------------------- ("atomic")
+            (prove_predicate(env, Predicate { kind: PredicateKind::Atomic, parameter }) => ())
+        )
+    }
+}
+
+judgment_fn! {
+    fn variance_predicate(
+        env: Env,
+        kind: PredicateKind,
+        parameter: Parameter,
+    ) => () {
+        debug(kind, parameter, env)
+
+        (
+            (for_all(parameters, &|parameter| prove_predicate(&env, Predicate::new(kind, parameter))) => ())
+            ----------------------------- ("ty-named")
+            (variance_predicate(env, kind, NamedTy { name: _, parameters }) => ())
+        )
+
+        (
+            (prove_predicate(&env, Predicate::new(kind, &*ty1)) => ())
+            (prove_predicate(&env, Predicate::new(kind, &*ty2)) => ())
+            ----------------------------- ("ty-or")
+            (variance_predicate(env, kind, Ty::Or(ty1, ty2)) => ())
+        )
+
+        (
+            (prove_predicate(&env, Predicate::new(kind, perm)) => ())
+            (prove_predicate(&env, Predicate::new(kind, &*ty)) => ())
+            ----------------------------- ("ty")
+            (variance_predicate(env, kind, Ty::ApplyPerm(perm, ty)) => ())
+        )
+
+        (
+            ----------------------------- ("my")
+            (variance_predicate(_env, _kind, Perm::My) => ())
+        )
+
+        (
+            ----------------------------- ("our")
+            (variance_predicate(_env, _kind, Perm::Our) => ())
+        )
+
+        // FIXME: Is this right? What about e.g. `struct Foo[perm P, ty T] { x: T, y: P shared{x} String }`
+        // or other such things? and what about `given{x}`?
+
+        (
+            ----------------------------- ("shared")
+            (variance_predicate(_env, _kind, Perm::Shared(_)) => ())
+        )
+
+        (
+            (for_all(places, &|place| variance_predicate_place(&env, kind, place)) => ())
+            ----------------------------- ("leased")
+            (variance_predicate(env, kind, Perm::Leased(places)) => ())
+        )
+
+        (
+            (for_all(places, &|place| variance_predicate_place(&env, kind, place)) => ())
+            ----------------------------- ("given")
+            (variance_predicate(env, kind, Perm::Given(places)) => ())
+        )
+
+        (
+            (prove_predicate(&env, Predicate::new(kind, &*perm1)) => ())
+            (prove_predicate(&env, Predicate::new(kind, &*perm2)) => ())
+            ----------------------------- ("perm-or")
+            (variance_predicate(env, kind, Perm::Or(perm1, perm2)) => ())
+        )
+
+        (
+            (prove_predicate(&env, Predicate::new(kind, &*perm1)) => ())
+            (prove_predicate(&env, Predicate::new(kind, &*perm2)) => ())
+            ----------------------------- ("perm-apply")
+            (variance_predicate(env, kind, Perm::Apply(perm1, perm2)) => ())
+        )
+
+    }
+}
+
+judgment_fn! {
+    fn variance_predicate_place(
+        env: Env,
+        kind: PredicateKind,
+        place: Place,
+    ) => () {
+        debug(kind, place, env)
+
+        (
+            (place_ty(&env, place) => ty)
+            (prove_predicate(&env, Predicate::new(kind, ty)) => ())
+            ----------------------------- ("perm")
+            (variance_predicate_place(env, kind, place) => ())
+        )
     }
 }