Add function def clauses

book/src/clauses/well_known_traits.md

@@ -36,6 +36,7 @@ Some common examples of auto traits are `Send` and `Sync`.
 | str             | 📚    | 📚    | ⚬     | ⚬     | ⚬   |  ⚬  |  ⚬     |  ⚬       |    ❌        |
 | never type      | 📚   |  📚   |  ✅   |  ⚬    |  ⚬    | ⚬   |   ⚬    |  ⚬       |   ❌       |
 | trait objects   | ⚬    | ⚬    | ⚬     |  ✅    | ⚬    | ⚬   | ⚬      |  ⚬       |    ⚬        |
+| functions defs  | ✅    | ✅    | ✅     | ⚬     | ⚬    |  ❌  | ⚬      |  ⚬       |    ❌         |
 | functions ptrs  | ✅    | ✅    | ✅     | ⚬     | ⚬    | ❌   | ⚬      |  ⚬       |    ❌         |
 | raw ptrs        | 📚   |  📚  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |      ❌      |
 | immutable refs  | 📚   |  📚  |   ✅   |  ⚬    |   ⚬   |  ⚬  |   ⚬    |   ⚬      |      ❌      |

chalk-solve/src/clauses/builtin_traits/copy.rs

@@ -51,6 +51,9 @@ pub fn add_copy_program_clauses<I: Interner>(
                     iter::once(substitution.at(interner, 0).assert_ty_ref(interner).clone()),
                 );
             }
+            TypeName::FnDef(_) => {
+                builder.push_fact(trait_ref.clone());
+            }
             _ => return,
         },
         TyData::Function(_) => builder.push_fact(trait_ref.clone()),

chalk-solve/src/clauses/builtin_traits/sized.rs

@@ -76,6 +76,7 @@ pub fn add_sized_program_clauses<I: Interner>(
             }
             TypeName::Array
             | TypeName::Never
+            | TypeName::FnDef(_)
             | TypeName::Scalar(_)
             | TypeName::Raw(_)
             | TypeName::Ref(_) => builder.push_fact(trait_ref.clone()),

tests/test/fn_def.rs

@@ -0,0 +1,66 @@
+use super::*;
+
+#[test]
+fn fn_def_is_well_formed() {
+    test! {
+        program {
+            fn foo() {}
+        }
+        goal {
+            WellFormed(foo)
+        } yields {
+            "Unique"
+        }
+    }
+}
+
+#[test]
+fn fn_def_is_sized() {
+    test! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+
+            fn foo() {}
+        }
+        goal {
+            foo: Sized
+        } yields {
+            "Unique"
+        }
+    }
+}
+
+#[test]
+fn fn_def_is_copy() {
+    test! {
+        program {
+            #[lang(sized)]
+            trait Copy { }
+
+            fn foo() {}
+        }
+        goal {
+            foo: Copy
+        } yields {
+            "Unique"
+        }
+    }
+}
+
+#[test]
+fn fn_def_is_clone() {
+    test! {
+        program {
+            #[lang(sized)]
+            trait Clone { }
+
+            fn foo() {}
+        }
+        goal {
+            foo: Clone
+        } yields {
+            "Unique"
+        }
+    }
+}

tests/test/never.rs

@@ -11,3 +11,18 @@ fn never_is_well_formed() {
         }
     }
 }
+
+#[test]
+fn never_is_sized() {
+    test! {
+        program {
+            #[lang(sized)]
+            trait Sized { }
+        }
+        goal {
+            !: Sized
+        } yields {
+            "Unique"
+        }
+    }
+}