diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index c0cd1161..589a5cf7 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1496,11 +1496,9 @@ 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, _)]) + | Typ_app (f1, [arg1]), Typ_app (f2, [arg2a; arg2b]) 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") + unify_typ_arg_list 0 KBindings.empty [] [] [arg1; arg1] [arg2a; arg2b] | 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] |