diff --git a/lib/inference.ml b/lib/inference.ml
index 6c66973..1023a7c 100644
--- a/lib/inference.ml
+++ b/lib/inference.ml
@@ -27,10 +27,8 @@ let typeof t =
          (match TypeSubstitution.find id env' with
           | Some ty -> Some ty, env'
           | None -> None, env')
-       (* Directly the type *)
-       | Some ty, _ -> Some ty, env
        (* Bad typed *)
-       | None, _ -> None, env)
+       | _ -> None, env)
     | Term.Fun (id, body) ->
       let arg = TypeSubstitution.singleton id (Type.Var id) in
       (match infer (TypeSubstitution.compose arg env) body with
diff --git a/test/test_projet_pfa_23_24.ml b/test/test_projet_pfa_23_24.ml
index e8c6aa8..204b629 100644
--- a/test/test_projet_pfa_23_24.ml
+++ b/test/test_projet_pfa_23_24.ml
@@ -55,12 +55,19 @@ let tests_typeof =
     ( "(fun x -> fst x) (1, 2)"
     , Term.(App (Fun (x, Proj (First, Var x)), Pair (IntConst 1, IntConst 2)))
     , Some Type.Int )
-  ; (* Function application with nested pair and projection *)
+  ; (* Bad Application on a function application with nested pair and projection *)
     ( "(fun x -> fst (snd x)) ((1, 2), 3)"
     , Term.(
         App
           ( Fun (x, Proj (First, Proj (Second, Var x)))
           , Pair (Pair (IntConst 1, IntConst 2), IntConst 3) ))
+    , None )
+  ; (* Function application with nested pair and projection *)
+    ( "(fun x -> fst (snd x)) ((1, 2), (3, 2))"
+    , Term.(
+        App
+          ( 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"