diff options
| -rw-r--r-- | src/type_check.ml | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/anontyvar.sail | 15 |
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); + () +} |