Merge pull request #137 from obeis/add-fn-ui-tests

Add ui tests for functions

crates/formality-check/src/fns.rs

@@ -3,9 +3,7 @@ use formality_rust::{
     grammar::{Fn, FnBoundData},
     prove::ToWcs,
 };
-use formality_types::{
-    grammar::{Fallible, Wcs},
-};
+use formality_types::grammar::{Fallible, Wcs};
 
 use crate::Check;
 

tests/ui/fn/lifetime.stderr

@@ -0,0 +1 @@
+Error: failed to prove {@ wf((rigid &(shared) !lt_1 !ty_2))} given {}, got {}

tests/ui/fn/lifetime.🔬

@@ -0,0 +1,7 @@
+// Test lifetimes on function
+[
+    crate Foo {
+        // fn one_lt_arg<'a, T>(_: &'a T) -> () {}
+        fn one_lt_arg<lt a, ty T>(&a T) -> () where [] { trusted }
+    }
+]

tests/ui/fn/ok.🔬

@@ -0,0 +1,20 @@
+// Test functions, function's arguments, and function's returns
+//@check-pass
+[
+    crate Foo {
+        // fn simple_fn() {}
+        fn simple_fn<>() -> () where [] { trusted }
+
+        // fn one_arg<T>(_: T) {}
+        fn one_arg<ty T>(T) -> () where [] { trusted }
+
+        // fn one_ret<T>(_: T) {}
+        fn one_ret<ty T>() -> T where [] { trusted }
+
+        // fn arg_ret<T, U>(_: T) -> U {}
+        fn arg_ret<ty T, ty U>(T) -> U where [] { trusted }
+
+        // fn multi_arg_ret<T, Y, U, I>(_: T, _: Y) -> (U, I) {}
+        fn multi_arg_ret<ty T, ty Y, ty U, ty I>(T, Y) -> (U, I) where [] { trusted }
+    }
+]