Allow instantiation of type or order type variables without kind declaration

2 files changed, 17 insertions, 0 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index 9de6d7e7..cad7dc47 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1861,10 +1861,12 @@ let is_nat_kid kid = function
 
 let is_order_kid kid = function
   | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_order, _)], _), kid'), _) -> Kid.compare kid kid' = 0
+  | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0
   | _ -> false
 
 let is_typ_kid kid = function
   | KOpt_aux (KOpt_kind (K_aux (K_kind [BK_aux (BK_type, _)], _), kid'), _) -> Kid.compare kid kid' = 0
+  | KOpt_aux (KOpt_none kid', _) -> Kid.compare kid kid' = 0
   | _ -> false
 
 let rec instantiate_quants quants kid uvar = match quants with
diff --git a/test/typecheck/pass/anontyvar.sail b/test/typecheck/pass/anontyvar.sail
new file mode 100644
index 00000000..99c25e6c
--- /dev/null
+++ b/test/typecheck/pass/anontyvar.sail
@@ -0,0 +1,15 @@
+$include <smt.sail>
+$include <flow.sail>
+
+/* We shouldn't have to annotate 'a with Type */
+val id : forall 'a. 'a -> 'a
+function id(x) = {
+  x
+}
+
+val test : unit -> unit
+
+function test() = {
+  let x = id(5);
+  ()
+}