diff --git a/lib/inference.ml b/lib/inference.ml index 1023a7c..9cf1771 100644 --- a/lib/inference.ml +++ b/lib/inference.ml @@ -56,13 +56,6 @@ let typeof t = (* Nested *) nested_infer env env' ty_fn | None -> None, env) - | (Some (Type.Var _ as ty1), _), _ -> - (* On this case we may have a function represented as a variable *) - (* TODO: Nested application *) - let ty2 = Type.Arrow (ty1, ty1) in - (match Unification.unify ty1 ty2 with - | Some env' -> Some ty2, env' - | _ -> None, env) | _ -> None, env) in fst (infer TypeSubstitution.empty t) diff --git a/test/test_projet_pfa_23_24.ml b/test/test_projet_pfa_23_24.ml index d3819cd..efb8f2b 100644 --- a/test/test_projet_pfa_23_24.ml +++ b/test/test_projet_pfa_23_24.ml @@ -76,13 +76,6 @@ let tests_typeof = ( Fun (x, Proj (First, Proj (Second, Var x))) , Pair (Pair (IntConst 1, IntConst 2), Pair (IntConst 3, IntConst 2)) )) , Some Type.Int ) - (* ; (* x -> y -> (x -> y -> z) -> z *) - ( "fun x -> fun y -> fun z -> z x y" - , Term.(Fun (x, Fun (y, Fun (z, App (Var z, App (Var x, Var y)))))) - , Some - Type.( - Arrow (Var x, Arrow (Var y, Arrow (Arrow (Var x, Arrow (Var y, Var z)), Var z)))) - ) *) ] ;;