diff --git a/src/TypeInference/Error.ml b/src/TypeInference/Error.ml
index 849a140c..8ffc4128 100644
--- a/src/TypeInference/Error.ml
+++ b/src/TypeInference/Error.ml
@@ -107,6 +107,13 @@ let unbound_method ~pos ~env x name =
     name
   in (pos, msg ^ Pretty.additional_info pp_ctx, [])
 
+let unbound_adt ~pos ~env x =
+  let pp_ctx = Pretty.empty_context () in
+  let msg = Printf.sprintf
+    "There is no ADT assigned to this type var %s"
+    (Pretty.tvar_to_string pp_ctx env x)
+  in (pos, msg ^ Pretty.additional_info pp_ctx, [])
+
 let method_fn_without_arg ~pos x name =
   (pos, Printf.sprintf
     "Variable %s is registered as method %s and cannot be used without argument"
@@ -461,3 +468,10 @@ let redundant_named_pattern ~pos name =
     "Providing %s to a constructor that do not expect it"
     (string_of_name name),
     [])
+
+let invalid_whnf_form ~pos ~env tp =
+  let pp_ctx = Pretty.empty_context () in
+  let msg = Printf.sprintf
+    "Got invalid whnf form when converting type %s"
+    (Pretty.type_to_string pp_ctx env tp)
+  in (pos, msg ^ Pretty.additional_info pp_ctx, [])
diff --git a/src/TypeInference/Error.mli b/src/TypeInference/Error.mli
index 30c0004d..ded7bf8b 100644
--- a/src/TypeInference/Error.mli
+++ b/src/TypeInference/Error.mli
@@ -35,6 +35,7 @@ val unbound_module : pos:Position.t -> S.module_name S.path -> t
 val unbound_the_effect : pos:Position.t -> t
 val unbound_named_param : pos:Position.t -> S.var -> t
 val unbound_the_label : pos:Position.t -> t
+val unbound_adt : pos:Position.t -> env:Env.t -> T.tvar -> t
 
 val unbound_method :
   pos:Position.t -> env:Env.t -> T.tvar -> S.method_name -> t
@@ -140,3 +141,4 @@ val ctor_arity_mismatch :
 val redundant_named_type : pos:Position.t -> T.tname -> t
 val redundant_named_parameter : pos:Position.t -> T.name -> t
 val redundant_named_pattern : pos:Position.t -> T.name -> t
+val invalid_whnf_form : pos:Position.t -> env:Env.t -> T.typ -> t
diff --git a/src/TypeInference/PreludeTypes.ml b/src/TypeInference/PreludeTypes.ml
index 89a440d4..51b6aed1 100644
--- a/src/TypeInference/PreludeTypes.ml
+++ b/src/TypeInference/PreludeTypes.ml
@@ -10,20 +10,24 @@ let mk_Option ~env ~pos tp_arg =
   match Env.lookup_tvar env (S.NPName "Option") with
   | None -> Error.fatal (Error.unbound_type_var ~pos (S.NPName "Option"))
   | Some tp ->
-    if
-      not
-        (Unification.unify_kind (T.Type.kind tp)
-           (T.Kind.k_arrow T.Kind.k_type T.Kind.k_type))
-    then
-      Error.fatal
-        (Error.kind_mismatch ~pos (T.Type.kind tp)
-           (T.Kind.k_arrow T.Kind.k_type T.Kind.k_type))
-    else T.Type.t_app tp tp_arg
+      if
+        not
+          (Unification.unify_kind (T.Type.kind tp)
+             (T.Kind.k_arrow T.Kind.k_type T.Kind.k_type))
+      then
+        Error.fatal
+          (Error.kind_mismatch ~pos (T.Type.kind tp)
+             (T.Kind.k_arrow T.Kind.k_type T.Kind.k_type))
+      else T.Type.t_app tp tp_arg
 
 let option_to_whnf ~env ~pos option_tp =
   match T.Type.whnf option_tp with
   | Whnf_Neutral (NH_Var x, tp :: []) -> (tp, x)
-  | _ -> Error.fatal (Error.empty_match_on_non_adt ~pos ~env option_tp)
+  | _ -> Error.fatal (Error.invalid_whnf_form ~pos ~env option_tp)
+
+let extr_arg_tp ~env ~pos option_tp =
+  let tp, _ = option_to_whnf ~env ~pos option_tp in
+  tp
 
 let mk_Some ~env ~pos tp_arg expr_arg : T.expr =
   let make data pos = { T.data; T.pos } in
@@ -31,43 +35,38 @@ let mk_Some ~env ~pos tp_arg expr_arg : T.expr =
   let _, x = option_to_whnf ~env ~pos tp' in
   match Env.lookup_adt env x with
   | Some adt_info -> (
-    let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in
-    match
-      List.find_index
-        (fun (ctor_decl : T.ctor_decl) -> ctor_decl.ctor_name == "Some")
-        adt_ctors
-    with
-    | Some idx ->
-      make
-        (T.ECtor
-           ( make (T.ETApp (adt_proof, tp_arg)) Position.nowhere,
-             idx,
-             [],
-             [ expr_arg ] ))
-        Position.nowhere
-    | None -> failwith "")
-  | None -> Error.fatal (Error.ctor_not_in_type ~pos ~env "Some" tp')
-
-(* match Env.lookup_ctor env (S.NPName "Some") with
-   | Some (idx, adt_info) ->
-     let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in
-     make
-       (T.ECtor
-          ( make (T.ETApp (adt_proof, tp_arg)) Position.nowhere,
-            idx,
-            [],
-            [ expr_arg ] ))
-       Position.nowhere
-   | None -> Error.fatal (Error.ctor_not_in_type ~pos ~env "Some" tp') *)
+      let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in
+      match
+        List.find_index
+          (fun (ctor_decl : T.ctor_decl) -> String.compare ctor_decl.ctor_name "Some" == 0)
+          adt_ctors
+      with
+      | Some idx ->
+          make
+            (T.ECtor
+               ( make (T.ETApp (adt_proof, tp_arg)) Position.nowhere,
+                 idx,
+                 [],
+                 [ expr_arg ] ))
+            Position.nowhere
+      | None -> Error.fatal (Error.ctor_not_in_type ~pos ~env "Some" tp'))
+  | None -> Error.fatal (Error.unbound_adt ~pos ~env x)
 
 let mk_None ~env ~pos option_tp : T.expr =
   let make data pos = { T.data; T.pos } in
   let tp_arg, x = option_to_whnf ~env ~pos option_tp in
-  match Env.lookup_ctor env (S.NPName "None") with
-  | Some (idx, adt_info) ->
-    let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in
-    make
-      (T.ECtor
-         (make (T.ETApp (adt_proof, tp_arg)) Position.nowhere, idx, [], []))
-      Position.nowhere
-  | None -> Error.fatal (Error.ctor_not_in_type ~pos ~env "None" option_tp)
+  match Env.lookup_adt env x with
+  | Some adt_info -> (
+      let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in
+      match
+        List.find_index
+          (fun (ctor_decl : T.ctor_decl) -> String.compare ctor_decl.ctor_name "None" == 0)
+          adt_ctors
+      with
+      | Some idx ->
+          make
+            (T.ECtor
+               (make (T.ETApp (adt_proof, tp_arg)) Position.nowhere, idx, [], []))
+            Position.nowhere
+      | None -> Error.fatal (Error.ctor_not_in_type ~pos ~env "None" option_tp))
+  | None -> Error.fatal (Error.unbound_adt ~pos ~env x)
diff --git a/test/err/tc_0007_missingOptionTypeDef.fram b/test/err/tc_0007_missingOptionTypeDef.fram
new file mode 100644
index 00000000..84f741e9
--- /dev/null
+++ b/test/err/tc_0007_missingOptionTypeDef.fram
@@ -0,0 +1,2 @@
+let f {?x} = x
+let a = f
\ No newline at end of file
diff --git a/test/err/tc_0007_invalidOptionDef.fram b/test/err/tc_0008_invalidOptionTypeConstructors.fram
similarity index 51%
rename from test/err/tc_0007_invalidOptionDef.fram
rename to test/err/tc_0008_invalidOptionTypeConstructors.fram
index 680784ca..9e30ca17 100644
--- a/test/err/tc_0007_invalidOptionDef.fram
+++ b/test/err/tc_0008_invalidOptionTypeConstructors.fram
@@ -1,6 +1,4 @@
-data Option A = None | Some of A
 data Option A = Non | Som of A
 
 let f {?x} = x
-let a = f
-
+let a = f
\ No newline at end of file