introduce self into the environment

src/type_system/classes.rs

@@ -3,29 +3,32 @@ use std::sync::Arc;
 use fn_error_context::context;
 use formality_core::Fallible;
 
-use crate::grammar::{Atomic, ClassDecl, ClassDeclBoundData, FieldDecl, Program};
+use crate::grammar::{Atomic, ClassDecl, ClassDeclBoundData, ClassTy, FieldDecl, Program};
 
 use super::{env::Env, methods::check_method, types::check_type};
 
 #[context("check class named `{:?}`", decl.name)]
 pub fn check_class(program: &Arc<Program>, decl: &ClassDecl) -> Fallible<()> {
     let mut env = Env::new(program);
 
-    let ClassDeclBoundData { fields, methods } = env.open_universally(&decl.binder);
+    let ClassDecl { name, binder } = decl;
+    let (substitution, ClassDeclBoundData { fields, methods }) = env.open_universally(binder);
+
+    let class_ty = ClassTy::new(name, &substitution);
 
     for field in fields {
-        check_field(&env, &field)?;
+        check_field(&class_ty, &env, &field)?;
     }
 
     for method in methods {
-        check_method(&env, &method)?;
+        check_method(&class_ty, &env, &method)?;
     }
 
     Ok(())
 }
 
 #[context("check field named `{:?}`", decl.name)]
-fn check_field(env: &Env, decl: &FieldDecl) -> Fallible<()> {
+fn check_field(_class_ty: &ClassTy, env: &Env, decl: &FieldDecl) -> Fallible<()> {
     let FieldDecl {
         atomic,
         name: _,

src/type_system/env.rs

@@ -159,14 +159,16 @@ impl Env {
 
     /// Replace all the bound variables in `b` with fresh universal variables
     /// and return the contents.
-    pub fn open_universally<T: Term>(&mut self, b: &Binder<T>) -> T {
+    pub fn open_universally<T: Term>(&mut self, b: &Binder<T>) -> (Vec<UniversalVar>, T) {
         let universal_vars: Vec<_> = b
             .kinds()
             .iter()
             .map(|&k| self.push_next_universal_var(k))
             .collect();
 
-        b.instantiate_with(&universal_vars).unwrap()
+        let result = b.instantiate_with(&universal_vars).unwrap();
+
+        (universal_vars, result)
     }
 
     /// Introduces a program variable into scope, failing if this would introduce shadowing

src/type_system/methods.rs

@@ -1,23 +1,35 @@
-use std::sync::Arc;
-
 use anyhow::bail;
 use fn_error_context::context;
 use formality_core::{Fallible, Upcast};
 
-use crate::grammar::{Block, LocalVariableDecl, MethodDecl, MethodDeclBoundData, Program, Ty};
+use crate::grammar::{
+    Block, ClassTy, LocalVariableDecl, MethodDecl, MethodDeclBoundData, ThisDecl, Ty, Var::This,
+};
 
 use super::{env::Env, flow::Flow, type_expr::can_type_expr_as, types::check_type};
 
 #[context("check method named `{:?}`", decl.name)]
-pub fn check_method(env: impl Upcast<Env>, decl: &MethodDecl) -> Fallible<()> {
+pub fn check_method(class_ty: &ClassTy, env: impl Upcast<Env>, decl: &MethodDecl) -> Fallible<()> {
     let mut env = env.upcast();
 
-    let MethodDeclBoundData {
-        this,
-        inputs,
-        output,
-        body,
-    } = &env.open_universally(&decl.binder);
+    let MethodDecl { name: _, binder } = decl;
+    let (
+        _,
+        MethodDeclBoundData {
+            this,
+            inputs,
+            output,
+            body,
+        },
+    ) = &env.open_universally(binder);
+
+    if let Some(ThisDecl { perm }) = this {
+        let this_ty = Ty::apply_perm(perm, class_ty);
+        env.push_local_variable_decl(LocalVariableDecl {
+            name: This,
+            ty: this_ty,
+        })?;
+    }
 
     for input in inputs {
         env.push_local_variable_decl(input)?;