diff options
| author | Alasdair Armstrong | 2017-11-15 17:25:58 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-15 17:25:58 +0000 |
| commit | ff68c0250d43869f8cc62b79ebc9930f27158bee (patch) | |
| tree | 88ef2e95d29cc50456c7a4110cc6eee179d3c87d /src | |
| parent | 599930a7256340c9ecb6d872c82a487149ee551e (diff) | |
Fix rule for allowing atom to unify with range
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index f71e52c1..c0cd1161 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1496,6 +1496,11 @@ let rec unify l env typ1 typ2 = | Invalid_argument _ -> unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2 ^ " tuple type is of different length") end + | Typ_app (f1, [arg1]), Typ_app (f2, [Typ_arg_aux (Typ_arg_nexp n1, _) as arg2a; Typ_arg_aux (Typ_arg_nexp n2, _)]) + when Id.compare (mk_id "atom") f1 = 0 && Id.compare (mk_id "range") f2 = 0 -> + if prove env (nc_eq n1 n2) + then unify_typ_arg_list 0 KBindings.empty [] [] [arg1] [arg2a] + else typ_error l ("Cannot unify atom with range when range indices " ^ string_of_nexp n1 ^ " and " ^ string_of_nexp n2 ^ " are not equal") | Typ_app (f1, [arg1a; arg1b]), Typ_app (f2, [arg2]) when Id.compare (mk_id "range") f1 = 0 && Id.compare (mk_id "atom") f2 = 0 -> unify_typ_arg_list 0 KBindings.empty [] [] [arg1a; arg1b] [arg2; arg2] |