diff options
| -rw-r--r-- | src/type_check.ml | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/plus_one_unify.sail | 6 |
2 files changed, 11 insertions, 1 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 603052b5..48a64226 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1851,7 +1851,7 @@ let instantiate_quants quants unifier = they'll be unambigiously unified with the argument types so it's better to just not bother with the return type. *) -let rec ambiguous_vars (Typ_aux (aux, _)) = +let rec ambiguous_vars' (Typ_aux (aux, _)) = match aux with | Typ_app (_, args) -> List.fold_left KidSet.union KidSet.empty (List.map ambiguous_arg_vars args) | _ -> KidSet.empty @@ -1876,6 +1876,10 @@ and ambiguous_nexp_vars (Nexp_aux (aux, _)) = | Nexp_sum (nexp1, nexp2) -> KidSet.union (tyvars_of_nexp nexp1) (tyvars_of_nexp nexp2) | _ -> KidSet.empty +let ambiguous_vars typ = + let vars = ambiguous_vars' typ in + if KidSet.cardinal vars > 1 then vars else KidSet.empty + (**************************************************************************) (* 3.5. Subtyping with existentials *) (**************************************************************************) diff --git a/test/typecheck/pass/plus_one_unify.sail b/test/typecheck/pass/plus_one_unify.sail new file mode 100644 index 00000000..0dceaa4c --- /dev/null +++ b/test/typecheck/pass/plus_one_unify.sail @@ -0,0 +1,6 @@ + +val f2 : forall 'm, 'm in {0,1}. (int('m+1)) -> int + +function f2(_) = 3 + +let x = f2(1)
\ No newline at end of file |