diff --git a/src/ast.rs b/src/ast.rs
index a70a06d..354fa99 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -259,7 +259,7 @@ pub enum SelfParam {
     Inferred,
 
     /// Function signature has a `self` parameter with explicit type signature.
-    Explicit(L<Type>),
+    Explicit(Type),
 }
 
 #[derive(Debug, Clone)]
diff --git a/src/ast/printer.rs b/src/ast/printer.rs
index b9f1d31..1add27d 100644
--- a/src/ast/printer.rs
+++ b/src/ast/printer.rs
@@ -323,7 +323,7 @@ impl FunSig {
             }
             SelfParam::Explicit(ty) => {
                 buffer.push_str("self: ");
-                ty.node.print(buffer);
+                ty.print(buffer);
                 if !self.params.is_empty() {
                     buffer.push_str(", ");
                 }
diff --git a/src/parser.lalrpop b/src/parser.lalrpop
index f5a6a35..8b8a575 100644
--- a/src/parser.lalrpop
+++ b/src/parser.lalrpop
@@ -309,7 +309,7 @@ FunSig: (Option<L<Id>>, L<Id>, FunSig) = {
                 }
                 self_ = match param_ty {
                     None => SelfParam::Inferred,
-                    Some(ty) => SelfParam::Explicit(ty),
+                    Some(ty) => SelfParam::Explicit(ty.node),
                 };
             } else {
                 match param_ty {
diff --git a/src/parser.rs b/src/parser.rs
index 43840fc..59484f0 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -1,5 +1,5 @@
 // auto-generated: "lalrpop 0.22.0"
-// sha3: f29e9af2bd7cc34226fd49342a8058ae56e0299b586cb3bc3b1dca66c78319db
+// sha3: 857086d3194941087844d3d0d094985a4bac0b38fdf0ba0424dd60262fbebb4f
 #![allow(clippy::all)]
 use crate::ast::*;
 use crate::interpolation::{copy_update_escapes, parse_string_parts};
@@ -41357,7 +41357,7 @@ fn __action39<'a>(
                 }
                 self_ = match param_ty {
                     None => SelfParam::Inferred,
-                    Some(ty) => SelfParam::Explicit(ty),
+                    Some(ty) => SelfParam::Explicit(ty.node),
                 };
             } else {
                 match param_ty {
diff --git a/src/type_checker.rs b/src/type_checker.rs
index 29956ef..20066d7 100644
--- a/src/type_checker.rs
+++ b/src/type_checker.rs
@@ -407,10 +407,6 @@ fn collect_cons(module: &mut ast::Module) -> TyMap {
                                 &item.loc,
                             );
 
-                            if fun.sig.self_ {
-                                tys.insert_var(SmolStr::new_static("self"), self_ty.clone());
-                            }
-
                             let mut arg_tys: Vec<Ty> = fun
                                 .sig
                                 .params
@@ -418,8 +414,14 @@ fn collect_cons(module: &mut ast::Module) -> TyMap {
                                 .map(|(_name, ty)| convert_ast_ty(&tys, &ty.node, &ty.loc))
                                 .collect();
 
-                            if fun.sig.self_ {
-                                arg_tys.insert(0, self_ty.clone());
+                            match fun.sig.self_ {
+                                ast::SelfParam::No => {}
+                                ast::SelfParam::Inferred => {
+                                    arg_tys.insert(0, self_ty.clone());
+                                }
+                                ast::SelfParam::Explicit(_) => {
+                                    panic!("{}: `self` parameter in trait methods can't have type annotations", loc_display(&item.loc));
+                                }
                             }
 
                             let ret_ty: Ty = match &fun.sig.return_ty {
@@ -490,10 +492,7 @@ fn collect_cons(module: &mut ast::Module) -> TyMap {
             _ => continue,
         };
 
-        let trait_con_id = match &impl_decl.trait_ {
-            Some(trait_id) => &trait_id.node,
-            None => continue,
-        };
+        let trait_con_id = &impl_decl.trait_.node;
 
         // New scope for the context.
         assert_eq!(tys.len_scopes(), 1);
@@ -633,10 +632,7 @@ fn collect_cons(module: &mut ast::Module) -> TyMap {
             _ => continue,
         };
 
-        let trait_con_id = match &impl_decl.trait_ {
-            Some(trait_id) => &trait_id.node,
-            None => continue,
-        };
+        let trait_con_id = &impl_decl.trait_.node;
 
         tys.enter_scope();
 
@@ -706,7 +702,7 @@ fn collect_cons(module: &mut ast::Module) -> TyMap {
 
 // `ty_cons` is `mut` to be able to update it with associated types when checking traits.
 fn collect_schemes(
-    module: &ast::Module,
+    module: &mut ast::Module,
     tys: &mut TyMap,
 ) -> (
     Map<Id, Scheme>,
@@ -722,11 +718,57 @@ fn collect_schemes(
         assert_eq!(tys.len_scopes(), 1);
         tys.enter_scope();
 
-        match &decl.node {
+        match &mut decl.node {
             ast::TopDecl::Fun(ast::L {
-                node: ast::FunDecl { name, sig, body: _ },
+                node:
+                    ast::FunDecl {
+                        ty_name,
+                        name,
+                        sig,
+                        body: _,
+                    },
                 loc,
             }) => {
+                // If this is a method without a `self` type, add type parameters of the type to
+                // function context and annotate `self`.
+                let mut self_ty: Option<Ty> = None;
+                if let Some(ty_name) = ty_name {
+                    match &sig.self_ {
+                        ast::SelfParam::No => {
+                            // Associated function.
+                        }
+
+                        ast::SelfParam::Inferred => {
+                            // Method, but `self` doesn't have a type. Annotate it with the type
+                            // owning the function.
+                            // If the type has parameters, for now we require the user to
+                            // specify the self type.
+                            let ty_con = tys.cons().get(&ty_name.node).unwrap_or_else(|| {
+                                panic!(
+                                    "{}: Undefined type {}",
+                                    loc_display(&ty_name.loc),
+                                    ty_name.node
+                                )
+                            });
+
+                            if !ty_con.ty_params.is_empty() {
+                                panic!(
+                                    "{}: Associated type self parameter needs type annotation",
+                                    loc_display(loc)
+                                );
+                            }
+
+                            self_ty = Some(Ty::Con(ty_con.id.clone()));
+                        }
+
+                        ast::SelfParam::Explicit(ty) => {
+                            self_ty = Some(convert_ast_ty(tys, &ty, &loc));
+                        }
+                    }
+                }
+
+                // Because we require self type to be specified if the owning type has parameters,
+                // this doesn't need to consider `self` type.
                 let fun_var_kinds = fun_sig_ty_var_kinds(sig);
 
                 let fun_context: Vec<(Id, QVar)> = convert_and_bind_context(
@@ -737,12 +779,16 @@ fn collect_schemes(
                     loc,
                 );
 
-                let arg_tys: Vec<Ty> = sig
+                let mut arg_tys: Vec<Ty> = sig
                     .params
                     .iter()
                     .map(|(_name, ty)| convert_ast_ty(tys, &ty.node, &ty.loc))
                     .collect();
 
+                if let Some(self_ty) = self_ty {
+                    arg_tys.insert(0, self_ty);
+                }
+
                 let ret_ty: Ty = match &sig.return_ty {
                     Some(ret_ty) => convert_ast_ty(tys, &ret_ty.node, &ret_ty.loc),
                     None => Ty::unit(),
@@ -765,13 +811,31 @@ fn collect_schemes(
                     loc: loc.clone(),
                 };
 
-                let old = top_schemes.insert(name.node.clone(), scheme);
-                if old.is_some() {
-                    panic!(
-                        "{}: Function {} is defined multiple times",
-                        loc_display(loc),
-                        name.node
-                    );
+                match ty_name {
+                    Some(ty_name) => {
+                        let old = associated_fn_schemes
+                            .get_mut(&ty_name.node)
+                            .unwrap()
+                            .insert(name.node.clone(), scheme);
+                        if old.is_some() {
+                            panic!(
+                                "{}: Associated function {}.{} is defined multiple times",
+                                loc_display(loc),
+                                ty_name.node,
+                                name.node
+                            );
+                        }
+                    }
+                    None => {
+                        let old = top_schemes.insert(name.node.clone(), scheme);
+                        if old.is_some() {
+                            panic!(
+                                "{}: Function {} is defined multiple times",
+                                loc_display(loc),
+                                name.node
+                            );
+                        }
+                    }
                 }
             }
 
@@ -806,17 +870,6 @@ fn collect_schemes(
 
                 let (self_ty_con_id, _) = self_ty.con(tys.cons()).unwrap();
 
-                // If not in a trait impl block, make sure `self` is not a trait.
-                if impl_decl.node.trait_.is_none()
-                    && tys.cons().get(&self_ty_con_id).map(|con| con.is_trait()) == Some(true)
-                {
-                    panic!(
-                        "{}: Type constructor {} in trait `impl` block is not a trait",
-                        loc_display(&impl_decl.loc),
-                        self_ty_con_id
-                    );
-                }
-
                 bind_associated_types(impl_decl, tys);
 
                 for item in &impl_decl.node.items {
@@ -841,18 +894,23 @@ fn collect_schemes(
                         &item.loc,
                     );
 
-                    if sig.self_ {
-                        tys.insert_var(SmolStr::new_static("self"), self_ty.clone());
-                    }
-
                     let mut arg_tys: Vec<Ty> = sig
                         .params
                         .iter()
                         .map(|(_name, ty)| convert_ast_ty(tys, &ty.node, &ty.loc))
                         .collect();
 
-                    if sig.self_ {
-                        arg_tys.insert(0, self_ty.clone());
+                    match sig.self_ {
+                        ast::SelfParam::No => {}
+                        ast::SelfParam::Inferred => {
+                            arg_tys.insert(0, self_ty.clone());
+                        }
+                        ast::SelfParam::Explicit(_) => {
+                            panic!(
+                                "{}: `self` parameter in trait methods can't have type annotations",
+                                loc_display(&item.loc)
+                            );
+                        }
                     }
 
                     let ret_ty: Ty = match &sig.return_ty {
@@ -881,96 +939,75 @@ fn collect_schemes(
                         loc: item.loc.clone(),
                     };
 
-                    if sig.self_ {
-                        let old = method_schemes
-                            .entry(self_ty_con_id.clone())
-                            .or_default()
-                            .insert(fun.name.node.clone(), scheme.clone());
-
-                        // Add the type key to associated_fn_schemes to make lookups easier.
-                        associated_fn_schemes
-                            .entry(self_ty_con_id.clone())
-                            .or_default();
-
-                        if old.is_some() {
-                            panic!(
-                                "{}: Method {} for type {} is defined multiple times",
-                                loc_display(&item.loc),
-                                fun.name.node,
-                                self_ty_con_id
-                            );
-                        }
-                    } else {
-                        let old = associated_fn_schemes
-                            .entry(self_ty_con_id.clone())
-                            .or_default()
-                            .insert(fun.name.node.clone(), scheme.clone());
+                    let old = method_schemes
+                        .entry(self_ty_con_id.clone())
+                        .or_default()
+                        .insert(fun.name.node.clone(), scheme.clone());
 
-                        method_schemes.entry(self_ty_con_id.clone()).or_default();
+                    // Add the type key to associated_fn_schemes to make lookups easier.
+                    associated_fn_schemes
+                        .entry(self_ty_con_id.clone())
+                        .or_default();
 
-                        if old.is_some() {
-                            panic!(
-                                "{}: Associated function {} for type {} is defined multiple times",
-                                loc_display(&item.loc),
-                                fun.name.node,
-                                self_ty_con_id
-                            );
-                        }
+                    if old.is_some() {
+                        panic!(
+                            "{}: Method {} for type {} is defined multiple times",
+                            loc_display(&item.loc),
+                            fun.name.node,
+                            self_ty_con_id
+                        );
                     }
 
                     tys.exit_scope();
                     assert_eq!(tys.len_scopes(), 2); // top-level, impl
 
-                    // If this is a trait method, check that the type matches the method type in
-                    // the trait.
-                    if let Some(trait_id) = &impl_decl.node.trait_ {
-                        let trait_ty_con = tys.cons().get(&trait_id.node).unwrap();
-                        let trait_details = trait_ty_con.trait_details().unwrap();
+                    // Check that the type matches the method type in the trait.
+                    let trait_ty_con = tys.cons().get(&impl_decl.node.trait_.node).unwrap();
+                    let trait_details = trait_ty_con.trait_details().unwrap();
 
-                        let fun_name: &Id = &fun.name.node;
+                    let fun_name: &Id = &fun.name.node;
 
-                        let trait_fun_scheme = &trait_details
-                            .methods
-                            .get(fun_name)
-                            .unwrap_or_else(|| {
-                                panic!(
-                                    "{}: Trait {} does not have a method named {}",
-                                    loc_display(&item.loc),
-                                    trait_ty_con.id,
-                                    fun_name
-                                )
-                            })
-                            .scheme;
-
-                        let trait_ty_param = &trait_ty_con.ty_params[0].0;
-
-                        // Type of the method in the trait declaration, with `self` type substituted for the
-                        // type implementing the trait.
-                        let mut trait_fun_scheme = trait_fun_scheme
-                            .subst(trait_ty_param, &self_ty, &item.loc)
-                            .subst_self(&self_ty);
-
-                        // Also add quantified variables of `impl`.
-                        trait_fun_scheme
-                            .quantified_vars
-                            .splice(0..0, impl_context.iter().cloned());
-
-                        if !trait_fun_scheme.eq_modulo_alpha(
-                            tys.cons(),
-                            &Default::default(),
-                            &scheme,
-                            &item.loc,
-                        ) {
+                    let trait_fun_scheme = &trait_details
+                        .methods
+                        .get(fun_name)
+                        .unwrap_or_else(|| {
                             panic!(
-                                "{}: Trait method implementation of {} does not match the trait method type
-                                Trait method type:          {}
-                                Implementation method type: {}",
+                                "{}: Trait {} does not have a method named {}",
                                 loc_display(&item.loc),
-                                fun_name,
-                                trait_fun_scheme,
-                                scheme
-                            );
-                        }
+                                trait_ty_con.id,
+                                fun_name
+                            )
+                        })
+                        .scheme;
+
+                    let trait_ty_param = &trait_ty_con.ty_params[0].0;
+
+                    // Type of the method in the trait declaration, with `self` type substituted for the
+                    // type implementing the trait.
+                    let mut trait_fun_scheme = trait_fun_scheme
+                        .subst(trait_ty_param, &self_ty, &item.loc)
+                        .subst_self(&self_ty);
+
+                    // Also add quantified variables of `impl`.
+                    trait_fun_scheme
+                        .quantified_vars
+                        .splice(0..0, impl_context.iter().cloned());
+
+                    if !trait_fun_scheme.eq_modulo_alpha(
+                        tys.cons(),
+                        &Default::default(),
+                        &scheme,
+                        &item.loc,
+                    ) {
+                        panic!(
+                            "{}: Trait method implementation of {} does not match the trait method type
+                            Trait method type:          {}
+                            Implementation method type: {}",
+                            loc_display(&item.loc),
+                            fun_name,
+                            trait_fun_scheme,
+                            scheme
+                        );
                     }
                 }
             }
@@ -1227,239 +1264,157 @@ fn check_impl(impl_: &mut ast::L<ast::ImplDecl>, tys: &mut PgmTypes) {
     // Bind associated types.
     bind_associated_types(impl_, &mut tys.tys);
 
-    match &impl_.node.trait_ {
-        Some(trait_ty_con_id) => {
-            let trait_ty_con = tys.tys.get_con(&trait_ty_con_id.node).unwrap_or_else(|| {
-                panic!(
-                    "{}: Unknown trait {}",
-                    loc_display(&trait_ty_con_id.loc),
-                    trait_ty_con_id.node
-                )
-            });
-
-            let trait_details = trait_ty_con
-                .trait_details()
-                .unwrap_or_else(|| {
-                    panic!(
-                        "{}: {} in `impl` block is not a trait",
-                        loc_display(&trait_ty_con_id.loc),
-                        trait_ty_con_id.node
-                    )
-                })
-                .clone();
-
-            tys.tys.insert_con(
-                "Self".into(),
-                TyCon {
-                    id: "Self".into(),
-                    ty_params: vec![],
-                    assoc_tys: Default::default(),
-                    details: TyConDetails::Synonym(self_ty.clone()),
-                },
-            );
-
-            // Check method bodies.
-            for item in &mut impl_.node.items {
-                let fun = match &mut item.node {
-                    ast::ImplDeclItem::AssocTy(_) => continue,
-                    ast::ImplDeclItem::Fun(fun) => fun,
-                };
-
-                tys.tys.enter_scope();
-
-                // Bind function type parameters.
-                let var_kinds = fun_sig_ty_var_kinds(&fun.sig);
-                let fn_bounds = convert_and_bind_context(
-                    &mut tys.tys,
-                    &fun.sig.type_params,
-                    &var_kinds,
-                    TyVarConversion::ToOpaque,
-                    &impl_.loc,
-                );
-
-                // Schemes overridden by method bounds.
-                let old_schemes_2 = bind_type_params(&fn_bounds, tys, &item.loc);
-
-                // Check the body.
-                if let Some(body) = &mut fun.body {
-                    let ret_ty = match &fun.sig.return_ty {
-                        Some(ty) => convert_ast_ty(&tys.tys, &ty.node, &ty.loc),
-                        None => Ty::unit(),
-                    };
-
-                    let mut preds: PredSet = Default::default();
-                    let mut env: ScopeMap<Id, Ty> = ScopeMap::default();
-                    let mut var_gen = TyVarGen::default();
-
-                    env.insert(SmolStr::new_static("self"), self_ty.clone());
-
-                    for (param_name, param_ty) in &fun.sig.params {
-                        env.insert(
-                            param_name.clone(),
-                            convert_ast_ty(&tys.tys, &param_ty.node, &item.loc),
-                        );
-                    }
-
-                    let context = impl_bounds
-                        .iter()
-                        .cloned()
-                        .chain(fn_bounds.into_iter())
-                        .collect();
+    let trait_ty_con_id = &impl_.node.trait_;
 
-                    let exceptions = match &fun.sig.exceptions {
-                        Some(exc) => convert_ast_ty(&tys.tys, &exc.node, &exc.loc),
-                        None => panic!(),
-                    };
+    let trait_ty_con = tys.tys.get_con(&trait_ty_con_id.node).unwrap_or_else(|| {
+        panic!(
+            "{}: Unknown trait {}",
+            loc_display(&trait_ty_con_id.loc),
+            trait_ty_con_id.node
+        )
+    });
 
-                    let mut tc_state = TcFunState {
-                        context: &context,
-                        return_ty: ret_ty.clone(),
-                        env: &mut env,
-                        var_gen: &mut var_gen,
-                        tys,
-                        preds: &mut preds,
-                        exceptions,
-                    };
+    let trait_details = trait_ty_con
+        .trait_details()
+        .unwrap_or_else(|| {
+            panic!(
+                "{}: {} in `impl` block is not a trait",
+                loc_display(&trait_ty_con_id.loc),
+                trait_ty_con_id.node
+            )
+        })
+        .clone();
+
+    tys.tys.insert_con(
+        "Self".into(),
+        TyCon {
+            id: "Self".into(),
+            ty_params: vec![],
+            assoc_tys: Default::default(),
+            details: TyConDetails::Synonym(self_ty.clone()),
+        },
+    );
 
-                    check_stmts(&mut tc_state, body, Some(&ret_ty), 0, 0);
+    // Check method bodies.
+    for item in &mut impl_.node.items {
+        let fun = match &mut item.node {
+            ast::ImplDeclItem::AssocTy(_) => continue,
+            ast::ImplDeclItem::Fun(fun) => fun,
+        };
 
-                    for stmt in body.iter_mut() {
-                        normalize_instantiation_types(&mut stmt.node, tys.tys.cons());
-                    }
+        tys.tys.enter_scope();
 
-                    resolve_all_preds(&context, tys, preds, &mut var_gen, 0);
-                }
+        // Bind function type parameters.
+        let var_kinds = fun_sig_ty_var_kinds(&fun.sig);
+        let fn_bounds = convert_and_bind_context(
+            &mut tys.tys,
+            &fun.sig.type_params,
+            &var_kinds,
+            TyVarConversion::ToOpaque,
+            &impl_.loc,
+        );
 
-                unbind_type_params(old_schemes_2, &mut tys.method_schemes);
+        // Schemes overridden by method bounds.
+        let old_schemes_2 = bind_type_params(&fn_bounds, tys, &item.loc);
 
-                tys.tys.exit_scope();
-            }
+        // Check the body.
+        if let Some(body) = &mut fun.body {
+            let ret_ty = match &fun.sig.return_ty {
+                Some(ty) => convert_ast_ty(&tys.tys, &ty.node, &ty.loc),
+                None => Ty::unit(),
+            };
 
-            // Check that all methods without default implementations are implemented.
-            let trait_method_ids: Set<&Id> = trait_details.methods.keys().collect();
-            let mut implemented_method_ids: Set<&Id> = Default::default();
-            for item in &impl_.node.items {
-                let fun_decl = match &item.node {
-                    ast::ImplDeclItem::AssocTy(_) => continue,
-                    ast::ImplDeclItem::Fun(fun_decl) => fun_decl,
-                };
-                let fun_id = &fun_decl.name.node;
-                match (
-                    trait_method_ids.contains(fun_id),
-                    implemented_method_ids.contains(fun_id),
-                ) {
-                    (true, true) => panic!(
-                        "{}: Trait method {} implemented multiple times",
-                        loc_display(&item.loc),
-                        fun_id
-                    ),
+            let mut preds: PredSet = Default::default();
+            let mut env: ScopeMap<Id, Ty> = ScopeMap::default();
+            let mut var_gen = TyVarGen::default();
 
-                    (true, false) => {
-                        implemented_method_ids.insert(fun_id);
-                    }
+            env.insert(SmolStr::new_static("self"), self_ty.clone());
 
-                    (false, _) => {
-                        panic!(
-                            "{}: Trait {} does not have method {}",
-                            loc_display(&item.loc),
-                            trait_ty_con_id.node,
-                            fun_id
-                        )
-                    }
-                }
-            }
-            let missing_methods: Vec<&&Id> = trait_method_ids
-                .difference(&implemented_method_ids)
-                .collect();
-            if !missing_methods.is_empty() {
-                panic!(
-                    "{}: Trait methods missing: {:?}",
-                    loc_display(&impl_.loc),
-                    missing_methods
+            for (param_name, param_ty) in &fun.sig.params {
+                env.insert(
+                    param_name.clone(),
+                    convert_ast_ty(&tys.tys, &param_ty.node, &item.loc),
                 );
             }
-        }
-
-        None => {
-            for item in &mut impl_.node.items {
-                let fun = match &mut item.node {
-                    ast::ImplDeclItem::AssocTy(_) => continue,
-                    ast::ImplDeclItem::Fun(fun) => fun,
-                };
-
-                assert_eq!(tys.tys.len_scopes(), 2); // top-level, impl
-                tys.tys.enter_scope();
-
-                // Bind function type parameters.
-                let var_kinds = fun_sig_ty_var_kinds(&fun.sig);
-                let fn_bounds: Vec<(Id, QVar)> = convert_and_bind_context(
-                    &mut tys.tys,
-                    &fun.sig.type_params,
-                    &var_kinds,
-                    TyVarConversion::ToOpaque,
-                    &item.loc,
-                );
-
-                // Schemes overridden by method bounds.
-                let old_schemes_2 = bind_type_params(&fn_bounds, tys, &item.loc);
-
-                // Check the body.
-                if let Some(body) = &mut fun.body {
-                    let ret_ty = match &fun.sig.return_ty {
-                        Some(ty) => convert_ast_ty(&tys.tys, &ty.node, &ty.loc),
-                        None => Ty::unit(),
-                    };
 
-                    let mut preds: PredSet = Default::default();
-                    let mut env: ScopeMap<Id, Ty> = ScopeMap::default();
-                    let mut var_gen = TyVarGen::default();
+            let context = impl_bounds
+                .iter()
+                .cloned()
+                .chain(fn_bounds.into_iter())
+                .collect();
 
-                    env.insert(SmolStr::new_static("self"), self_ty.clone());
+            let exceptions = match &fun.sig.exceptions {
+                Some(exc) => convert_ast_ty(&tys.tys, &exc.node, &exc.loc),
+                None => panic!(),
+            };
 
-                    for (param_name, param_ty) in &fun.sig.params {
-                        env.insert(
-                            param_name.clone(),
-                            convert_ast_ty(&tys.tys, &param_ty.node, &item.loc),
-                        );
-                    }
+            let mut tc_state = TcFunState {
+                context: &context,
+                return_ty: ret_ty.clone(),
+                env: &mut env,
+                var_gen: &mut var_gen,
+                tys,
+                preds: &mut preds,
+                exceptions,
+            };
 
-                    let context = impl_bounds
-                        .iter()
-                        .map(|(qvar, details)| (qvar.clone(), details.clone()))
-                        .chain(fn_bounds.into_iter())
-                        .collect();
+            check_stmts(&mut tc_state, body, Some(&ret_ty), 0, 0);
 
-                    let exceptions = match &fun.sig.exceptions {
-                        Some(exc) => convert_ast_ty(&tys.tys, &exc.node, &exc.loc),
-                        None => panic!(),
-                    };
+            for stmt in body.iter_mut() {
+                normalize_instantiation_types(&mut stmt.node, tys.tys.cons());
+            }
 
-                    let mut tc_state = TcFunState {
-                        context: &context,
-                        return_ty: ret_ty.clone(),
-                        env: &mut env,
-                        var_gen: &mut var_gen,
-                        tys,
-                        preds: &mut preds,
-                        exceptions,
-                    };
+            resolve_all_preds(&context, tys, preds, &mut var_gen, 0);
+        }
 
-                    check_stmts(&mut tc_state, body, Some(&ret_ty), 0, 0);
+        unbind_type_params(old_schemes_2, &mut tys.method_schemes);
 
-                    for stmt in body.iter_mut() {
-                        normalize_instantiation_types(&mut stmt.node, tys.tys.cons());
-                    }
+        tys.tys.exit_scope();
+    }
 
-                    resolve_all_preds(&context, tys, preds, &mut var_gen, 0);
-                }
+    // Check that all methods without default implementations are implemented.
+    let trait_method_ids: Set<&Id> = trait_details.methods.keys().collect();
+    let mut implemented_method_ids: Set<&Id> = Default::default();
+    for item in &impl_.node.items {
+        let fun_decl = match &item.node {
+            ast::ImplDeclItem::AssocTy(_) => continue,
+            ast::ImplDeclItem::Fun(fun_decl) => fun_decl,
+        };
+        let fun_id = &fun_decl.name.node;
+        match (
+            trait_method_ids.contains(fun_id),
+            implemented_method_ids.contains(fun_id),
+        ) {
+            (true, true) => panic!(
+                "{}: Trait method {} implemented multiple times",
+                loc_display(&item.loc),
+                fun_id
+            ),
 
-                unbind_type_params(old_schemes_2, &mut tys.method_schemes);
+            (true, false) => {
+                implemented_method_ids.insert(fun_id);
+            }
 
-                tys.tys.exit_scope();
-                assert_eq!(tys.tys.len_scopes(), 2); // top-level, impl
+            (false, _) => {
+                panic!(
+                    "{}: Trait {} does not have method {}",
+                    loc_display(&item.loc),
+                    trait_ty_con_id.node,
+                    fun_id
+                )
             }
         }
     }
+    let missing_methods: Vec<&&Id> = trait_method_ids
+        .difference(&implemented_method_ids)
+        .collect();
+    if !missing_methods.is_empty() {
+        panic!(
+            "{}: Trait methods missing: {:?}",
+            loc_display(&impl_.loc),
+            missing_methods
+        );
+    }
 
     unbind_type_params(old_schemes_1, &mut tys.method_schemes);