diff options
| author | Alasdair Armstrong | 2019-03-01 16:29:28 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-03-01 16:30:12 +0000 |
| commit | d9db6da6d031effbf820de406f06c4ee973939a5 (patch) | |
| tree | c820a5b555cc0594b1bc0c08c917fa9749b4344e /src | |
| parent | a8da14a23cd8dfdd5fcc527b930ed553d376d18f (diff) | |
Fix bug with naturals in quantified constructors
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index a2612794..1afd9765 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1585,6 +1585,10 @@ 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) + | 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") + | Typ_app (range, [A_aux (A_nexp n1, _); A_aux (A_nexp n2, _)]), Typ_app (atom, [A_aux (A_nexp m, _)]) when string_of_id range = "range" && string_of_id atom = "atom" -> |