Adjust option contrusctors to properly handle invalid option types

Co-authored-by: Zieliński Patryk <[email protected]>

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, [])

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

src/TypeInference/PreludeTypes.ml

@@ -10,64 +10,63 @@ 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
   let tp' = mk_Option ~env ~pos tp_arg in
   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)

test/err/tc_0007_missingOptionTypeDef.fram

@@ -0,0 +1,2 @@
+let f {?x} = x
+let a = f

test/err/tc_0007_invalidOptionDef.fram → 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