diff options
| author | Alasdair Armstrong | 2017-11-15 17:28:03 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-15 17:28:03 +0000 |
| commit | ab2b7e532247e03fc6c4e2ca0ccd139e7a4aca0f (patch) | |
| tree | c01c00f3d876362fcbcccf1fbb5b6781484e8f83 | |
| parent | ff68c0250d43869f8cc62b79ebc9930f27158bee (diff) | |
Fix atom - range unification again
| -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] |