diff options
| author | Alasdair Armstrong | 2019-03-01 16:38:03 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-03-01 16:39:13 +0000 |
| commit | 3e2cd8de57d4bc865f6b8299dd4e5689b5e8b875 (patch) | |
| tree | 58da240a2d4b79a262ee7d6b8b48c6cf672755e4 /src | |
| parent | d9db6da6d031effbf820de406f06c4ee973939a5 (diff) | |
Add a test case for previous commit
Also make unifying int against int('n) work as expected for
constructor applications.
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 1afd9765..de1c1ae1 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1585,6 +1585,9 @@ let rec unify_typ l env goals (Typ_aux (aux1, _) as typ1) (Typ_aux (aux2, _) as | Typ_var v, _ when KidSet.mem v goals -> KBindings.singleton v (arg_typ typ2) + (* We need special cases for unifying range(n, m), nat, and int vs atom('n) *) + | Typ_id int, Typ_app (atom, [A_aux (A_nexp n, _)]) when string_of_id int = "int" -> KBindings.empty + | Typ_id nat, Typ_app (atom, [A_aux (A_nexp n, _)]) when string_of_id nat = "nat" -> if prove __POS__ env (nc_gteq n (nint 0)) then KBindings.empty else unify_error l (string_of_typ typ2 ^ " must be a natural number") |