diff options
| author | Brian Campbell | 2018-05-24 16:49:06 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-05-24 16:49:06 +0100 |
| commit | fa2169a210a0ee911d889900d4e845629330c1de (patch) | |
| tree | 26255f7bc2793fa3a146edacdc3a84320419709f /src | |
| parent | 4932765be036afe3433e13c3473f602f35034f4c (diff) | |
Check kinds of type variables while checking well-formedness of types
Stops (e.g.) an Int being used as a Type, including when no kind was
declared. The following commit will remove the test for the latter
case.
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 65d07859..d58f38d4 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -645,8 +645,14 @@ end = struct then typ_error l ("Type constructor " ^ string_of_id id ^ " expected " ^ string_of_typquant typq) else () | Typ_id id -> typ_error l ("Undefined type " ^ string_of_id id) - | Typ_var kid when KBindings.mem kid env.typ_vars -> () - | Typ_var kid -> typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ) + | Typ_var kid -> begin + match KBindings.find kid env.typ_vars with + | BK_type -> () + | k -> typ_error l ("Kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ ^ + " is " ^ string_of_base_kind_aux k ^ " rather than Type") + | exception Not_found -> + typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ) + end | Typ_fn (typ_arg, typ_ret, effs) -> wf_typ ~exs:exs env typ_arg; wf_typ ~exs:exs env typ_ret | Typ_tup typs -> List.iter (wf_typ ~exs:exs env) typs | Typ_app (id, args) when bound_typ_id env id -> |