From 5daa03cb1aae4852d39b2f77e7f504095e78bdd1 Mon Sep 17 00:00:00 2001 From: Mylloon Date: Tue, 30 Apr 2024 12:02:14 +0200 Subject: [PATCH] fix arg inference --- lib/inference.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/lib/inference.ml b/lib/inference.ml index 905c94d..6f38001 100644 --- a/lib/inference.ml +++ b/lib/inference.ml @@ -30,7 +30,7 @@ let typeof t = | _ -> None, env) | Term.Fun (id, body) -> let arg = TypeSubstitution.singleton id (Type.Var id) in - (match infer (TypeSubstitution.compose env arg) body with + (match infer (TypeSubstitution.compose arg env) body with | Some ty_body, env' -> (match infer env' (Term.Var id) with | Some ty, _ -> Some (Type.Arrow (ty, ty_body)), env' @@ -39,10 +39,14 @@ let typeof t = | Term.App (t1, t2) -> (* Infer the type of t1 and t2 *) (match infer env t1, infer env t2 with - | (Some (Type.Arrow (ty_param, ty_fn)), _), (Some ty_args, _) -> + | (Some (Type.Arrow (ty_param, _)), _), (Some ty_args, _) -> (* Check if the argument type matches the parameter type *) (match Unification.unify ty_param ty_args with - | Some env' -> Some ty_fn, env' + | Some env' -> + (* Infer again now that we have some extra typing infos *) + (match infer env' t1 with + | Some (Type.Arrow (_, ty_fn)), env'' -> Some ty_fn, env'' + | _ -> None, env) | None -> None, env) (* | (Some (Type.Var _ as ty1), _), _ -> (* On this case we may have a function represented as a variable *)