diff --git a/flap/src/hopix/hopixTypechecker.ml b/flap/src/hopix/hopixTypechecker.ml
index 3a91703..373e8f0 100644
--- a/flap/src/hopix/hopixTypechecker.ml
+++ b/flap/src/hopix/hopixTypechecker.ml
@@ -2,6 +2,8 @@
 
 open HopixAST
 
+let get_aty (HopixTypes.Scheme (_, aty_value)) : HopixTypes.aty = aty_value
+
 (** Error messages *)
 
 let invalid_instantiation pos given expected =
@@ -41,13 +43,11 @@ let check_type_scheme
   -> HopixTypes.aty_scheme * HopixTypes.typing_environment
   =
   fun env pos (ForallTy (ts, ty)) ->
-    let ts = List.map Position.value ts in
-    let env = HopixTypes.bind_type_variables pos env ts in
-    (HopixTypes.Scheme (ts, HopixTypes.internalize_ty env ty), env)
+  let ts = List.map Position.value ts in
+  let env = HopixTypes.bind_type_variables pos env ts in
+  HopixTypes.Scheme (ts, HopixTypes.internalize_ty env ty), env
 ;;
 
-
-
 let rec check_pattern
   :  HopixTypes.typing_environment -> HopixAST.pattern Position.located -> HopixTypes.aty
   -> HopixTypes.typing_environment
@@ -81,7 +81,7 @@ let rec synth_expression
   | While (ecase, expr) -> synth_while env ecase expr
   | For (id, ecase, expr1, expr2) -> synth_for env id ecase expr1 expr2
 
-and  synth_literal : HopixAST.literal -> HopixTypes.aty =
+and synth_literal : HopixAST.literal -> HopixTypes.aty =
   fun l ->
   match l with
   | LInt _ -> HopixTypes.hint
@@ -111,16 +111,16 @@ and synth_apply
   :  HopixTypes.typing_environment -> expression Position.located
   -> expression Position.located -> HopixTypes.aty
   =
-  fun tenv f x -> (*failwith "Students! This is your job! (synth_apply)"*)
+  fun tenv f x ->
+  (*failwith "Students! This is your job! (synth_apply)"*)
   let f_type = synth_expression tenv f in
-  match f_type with 
-  | HopixTypes.ATyArrow (gauche,droit) -> (*  a' -> b' *)
-  (
+  match f_type with
+  | HopixTypes.ATyArrow (gauche, droit) ->
+    (*  a' -> b' *)
     let x_type = synth_expression tenv x in
-    check_equal_types x.position  gauche x_type; droit
-  )
+    check_equal_types x.position gauche x_type;
+    droit
   | _ -> failwith ""
-    
 
 and synth_record
   :  HopixTypes.typing_environment
@@ -215,7 +215,6 @@ and synth_for
   =
   fun tenv id estart eend expr -> failwith "Students! This is your job! (synth_for)"
 
-
 and check_expression
   :  HopixTypes.typing_environment -> HopixAST.expression Position.located
   -> HopixTypes.aty -> unit
@@ -223,7 +222,9 @@ and check_expression
   fun env (Position.{ value = e; position = pos } as exp) expected ->
   match e with
   | Fun df -> failwith "Students! This is your job! Fun check"
-  | _ -> failwith "Students! This is your job! check_expression wildcard"
+  | _ ->
+    let given = synth_expression env exp in
+    check_equal_types pos ~expected ~given
 
 and check_value_definition
   :  HopixTypes.typing_environment -> HopixAST.value_definition
@@ -232,10 +233,11 @@ and check_value_definition
   fun env -> function
   | SimpleValue (id, ty, ex) ->
     (match ty with
-     | None -> failwith "Type missing."
+     | None -> failwith "A type is missing."
      | Some ty' ->
        (*failwith "Students! This is your job! (check_value_definition | SimpleValue)"*)
-       let tys,_ = Position.located_pos (check_type_scheme env) ty' in
+       let tys, tenv = Position.located_pos (check_type_scheme env) ty' in
+       check_expression tenv ex (get_aty tys);
        HopixTypes.bind_value (Position.value id) tys env)
   | RecFunctions _ ->
     (* Je crois que c'est galère et donc c'est pas grave si on arrive pas