feat: Allow explicit bindings of implicit arguments

check/src/typecheck.rs

@@ -1427,6 +1427,29 @@ impl<'a> Typecheck<'a> {
         I: IntoIterator<Item = &'e mut SpannedExpr<Symbol>>,
     {
         func_type = self.new_skolem_scope(&func_type);
+        for arg in &mut **implicit_args {
+            let f = self.type_cache
+                .function_implicit(once(self.subs.new_var()), self.subs.new_var());
+            func_type = self.instantiate_generics(&func_type);
+            let level = self.subs.var_id();
+
+            self.subsumes(span, level, &f, func_type.clone());
+
+            func_type = match f.as_function() {
+                Some((arg_ty, ret_ty)) => {
+                    let arg_ty = self.subs.real(arg_ty).clone();
+                    let actual = self.typecheck(arg, &arg_ty);
+                    let actual = self.instantiate_generics(&actual);
+
+                    let level = self.subs.var_id();
+                    self.subsumes_expr(expr_check_span(arg), level, &arg_ty, actual, arg);
+
+                    ret_ty.clone()
+                }
+                None => return Err(TypeError::NotAFunction(func_type.clone())),
+            };
+        }
+
         for arg in args {
             let f = self.type_cache
                 .function(once(self.subs.new_var()), self.subs.new_var());

check/tests/implicits.rs

@@ -36,6 +36,19 @@ f 42
     assert_eq!(result, Ok(Type::int()));
 }
 
+#[test]
+fn single_implicit_explicit_arg() {
+    let _ = ::env_logger::try_init();
+    let text = r#"
+
+let f ?x y: [Int] -> Int -> Int = x
+f ?32 42
+"#;
+    let result = support::typecheck(text);
+
+    assert_req!(result, Ok(Type::int()));
+}
+
 #[test]
 fn multiple_implicit_args() {
     let _ = ::env_logger::try_init();

parser/src/grammar.lalrpop

@@ -525,7 +525,7 @@ SpAtomicExpr: SpannedExpr<Id> = {
 };
 
 ImplicitArg: SpannedExpr<Id> = {
-    <arg: Sp<AtomicExpr>> "?" => arg
+    "?" <arg: Sp<AtomicExpr>> => arg
 };
 
 AppExpr = {