Fix strange resulting type for functions with val spec, favouring the declared return type when consistent instead of using the derived one.

3 files changed, 17 insertions, 12 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 06eccbaf..47810801 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -14,12 +14,14 @@ let id_to_string (Id_aux(id,l)) =
 let var_to_string (Kid_aux(Var v,l)) = v
 
 (*placeholder, write in type_internal*)
-let kind_to_string kind = match kind.k with
+let rec kind_to_string kind = match kind.k with
   | K_Nat -> "Nat"
   | K_Typ -> "Type"
   | K_Ord -> "Order"
   | K_Efct -> "Effect"
-  | _ -> " kind pp place holder "
+  | K_infer -> "Infer"
+  | K_Lam (kinds,kind) -> "Lam ... -> " ^ (kind_to_string kind)
+
 
 let typquant_to_quantkinds k_env typquant = 
   match typquant with
@@ -159,14 +161,14 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
     ), l)
 
 and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
-(*  let _ = Printf.eprintf "to_ast_nexp\n" in*)
+  (*let _ = Printf.eprintf "to_ast_nexp\n" in*)
   match n with
   | Parse_ast.ATyp_aux(t,l) ->
     (match t with
     | Parse_ast.ATyp_var(v) ->                 
                 let v = to_ast_var v in
                 let mk = Envmap.apply k_env (var_to_string v) in
-(*		let _ = Envmap.iter (fun v' k -> Printf.eprintf "%s -> %s, %s =? %b\n" v' (kind_to_string k) (var_to_string v) ((var_to_string v) = v') ) k_env in *)
+		(*let _ = Envmap.iter (fun v' k -> Printf.eprintf "%s -> %s, %s =? %b\n" v' (kind_to_string k) (var_to_string v) ((var_to_string v) = v') ) k_env in *)
                 (match mk with
                 | Some(k) -> Nexp_aux((match k.k with
                                       | K_Nat -> Nexp_var v
@@ -545,6 +547,7 @@ let to_ast_spec (names,k_env,default_order) (val_:Parse_ast.val_spec) : (tannot
   | Parse_ast.VS_aux(vs,l) ->
     (match vs with
     | Parse_ast.VS_val_spec(ts,id) ->
+      (*let _ = Printf.eprintf "to_ast_spec called for internal spec: for %s\n" (id_to_string (to_ast_id id)) in*)
       let typsch,_,_ = to_ast_typschm k_env default_order ts in
       VS_aux(VS_val_spec(typsch,to_ast_id id),(l,NoTyp)),(names,k_env,default_order)
     | Parse_ast.VS_extern_spec(ts,id,s) ->
@@ -654,6 +657,7 @@ let to_ast_funcl (names,k_env,def_ord) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.fun
 let to_ast_fundef  (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (tannot fundef) envs_out = 
   match fd with
   | Parse_ast.FD_function(rec_opt,tannot_opt,effects_opt,funcls) -> 
+    (*let _ = Printf.eprintf "to_ast_fundef\n" in*)
     let tannot_opt, k_env,_ = to_ast_tannot_opt k_env def_ord tannot_opt in
     FD_aux(FD_function(to_ast_rec rec_opt, tannot_opt, to_ast_effects_opt k_env effects_opt, List.map (to_ast_funcl (names, k_env, def_ord)) funcls), (l,NoTyp)), (names,k_env,def_ord)
     
diff --git a/src/type_check.ml b/src/type_check.ml
index 85064e42..6c332e0b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1717,7 +1717,7 @@ let check_default envs (DT_aux(ds,l)) =
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot)),b_env,tp_env))
 
 let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,annot))) =
-  (*let _ = Printf.printf "checking fundef\n" in*)
+  (*let _ = Printf.eprintf "checking fundef\n" in*)
   let Env(d_env,t_env,b_env,tp_env) = envs in
   let _ = reset_fresh () in
   let is_rec = match recopt with
@@ -1733,12 +1733,13 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
   let in_env = Envmap.apply t_env id in 
   let typ_params = match in_env with
     | Some(Base( (params,u),Spec,constraints,eft,_)) -> params
-    | _ -> [] in
+    | None -> [] in
   let ret_t,param_t,tannot,t_param_env = match tannotopt with
     | Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),l') ->
       let (ids,_,constraints) = typq_to_params envs typq in
       let t = typ_to_t false false typ in
-      let t,constraints,_,t_param_env = subst (if ids=[] then typ_params else ids) true t constraints pure_e in
+      (*TODO add check that ids == typ_params*)
+      let t,constraints,_,t_param_env = subst typ_params true t constraints pure_e in
       let p_t = new_t () in
       let ef = new_e () in
       t,p_t,Base((ids,{t=Tfn(p_t,t,IP_none,ef)}),Emp_global,constraints,ef,nob),t_param_env in
@@ -1772,7 +1773,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       let imp_param = match u.t with 
 	| Tfn(_,_,IP_user n,_) -> Some n
 	| _ -> None in
-      let t_env = if is_rec then t_env else Envmap.remove t_env id in
+      let (t_env,orig_env) = if is_rec then (t_env,t_env) else (Envmap.remove t_env id,t_env) in
       let funcls,cs_ef = check t_env t_param_env_spec imp_param in
       let cs,ef = ((fun (cses,efses) -> 
 	(List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in
@@ -1786,7 +1787,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       in
       (*let _ = Printf.eprintf "done funcheck case 1\n" in*)
       (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
-      Env(d_env,Envmap.insert t_env (id,tannot),b_env,tp_env)
+      Env(d_env,orig_env (*Envmap.insert t_env (id,tannot)*),b_env,tp_env)
     | _ , _-> 
       let t_env = if is_rec then Envmap.insert t_env (id,tannot) else t_env in
       let funcls,cs_ef = check t_env t_param_env None in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index a860c719..19c3e288 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1137,9 +1137,9 @@ let initial_typ_env =
       Base(((mk_typ_params ["a";"b";"c"]),
             (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),External (Some "add"),[],pure_e,nob),
       true,
-      [Base(((mk_nat_params ["n";"m";"o";"p"]),
-             (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")])
-		          (mk_range (mk_add (mk_nv "n") (mk_nv "o")) (mk_add (mk_nv "m") (mk_nv "p"))))),
+      [Base(((mk_nat_params ["n";"m"]),
+             (mk_pure_fun (mk_tup [mk_atom (mk_nv "n"); mk_atom (mk_nv "m")])
+		          (mk_atom (mk_add (mk_nv "n") (mk_nv "m"))))),
 	    External (Some "add"),[],pure_e,nob);
        Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]),
              (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n");