From 3e2cd8de57d4bc865f6b8299dd4e5689b5e8b875 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 1 Mar 2019 16:38:03 +0000
Subject: Add a test case for previous commit

Also make unifying int against int('n) work as expected for
constructor applications.
---
 src/type_check.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src')

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")
-- 
cgit v1.2.3