Separate matching from subtyping like in F-ing modules to allow RDS

elab.ml

@@ -267,11 +267,11 @@ Trace.debug (lazy ("[AndT] ti = " ^ string_of_norm_typ ti));
  let aksi = List.filter (fun (a, k) -> VarSet.mem a vi) aks1 in
 Trace.debug (lazy ("[AndT] aksi = " ^ string_of_norm_extyp (ExT(aksi, StrT []))));
  let aks = aks1 @ aks2 in
- let ts, zs3, _ =
+ let su, zs3, _ =
  try sub_typ (add_typs aks env) t2 ti (varTs aksi) with Sub e ->
  error typ.at ("type refinement does not match: " ^ Sub.string_of_error e) in
-Trace.debug (lazy ("[AndT] ts = " ^ String.concat ", " (List.map string_of_norm_typ ts)));
- let t = merge_typs (subst_typ (subst (Lib.List.take (List.length ts) aksi) ts) t1) t2 in
+Trace.debug (lazy ("[AndT] su = " ^ string_of_match su));
+ let t = merge_typs (subst_typ (subst_of_match su) t1) t2 in
 Trace.debug (lazy ("[AndT] t = " ^ string_of_norm_typ t));
  let vt = vars_typ t in
  let s = ExT(List.filter (fun (a, k) -> VarSet.mem a vt) aks, t) in
@@ -493,16 +493,17 @@ Trace.debug (lazy ("[AppE] tf = " ^ string_of_norm_typ tf));
  let t2 = lookup_var env var2 in
 Trace.debug (lazy ("[AppE] s1 = " ^ string_of_norm_extyp (ExT(aks1, t1))));
 Trace.debug (lazy ("[AppE] t2 = " ^ string_of_norm_typ t2));
- let ts, zs3, f =
+ let su, zs3, f =
  try sub_typ env t2 t1 (varTs aks1) with Sub e -> error var2.at
  ("argument type does not match function: " ^ Sub.string_of_error e)
  in
-Trace.debug (lazy ("[AppE] ts = " ^ String.concat ", " (List.map string_of_norm_typ ts)));
+Trace.debug (lazy ("[AppE] su = " ^ string_of_match su));
  let ExT(aks2, t2) = s in
  let aks2' = freshen_vars env (rename_vars (prepend_path l) aks2) in
  let s' = ExT(aks2', subst_typ (subst aks2 (varTs aks2')) t2) in
- subst_extyp (subst aks1 ts) s', p, zs1 @ zs @ zs3,
- IL.AppE(IL.instE(ex1, List.map erase_typ ts), IL.AppE(f, IL.VarE(var2.it)))
+ subst_extyp (subst_of_match su) s', p, zs1 @ zs @ zs3,
+ IL.AppE(IL.instE(ex1, List.map (fun (_, t) -> erase_typ t) su),
+ IL.AppE(f, IL.VarE(var2.it)))
 
  | EL.UnwrapE(var, typ) ->
  let aks, t, s2, zs2 =
@@ -565,16 +566,16 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
  let t2, zs2 = elab_pathexp env1 exp1 l in
 Trace.debug (lazy ("[RecT] s1 = " ^ string_of_norm_extyp s1));
 Trace.debug (lazy ("[RecT] t2 = " ^ string_of_norm_typ t2));
- let ts, zs3, e =
+ let su, zs3, e =
  try sub_typ env1 t2 t1 (varTs aks1) with Sub e -> error typ.at
  ("recursive type does not match annotation: " ^ Sub.string_of_error e)
  in
-Trace.debug (lazy ("[RecT] ts = " ^ String.concat ", " (List.map string_of_norm_typ ts)));
+Trace.debug (lazy ("[RecT] su = " ^ string_of_match su));
  let t3, k3 = try make_rec_typ t1 with Recursive ->
  error typ.at "illegal type for recursive expression" in
  let a = freshen_var env var.it in
  let tas1 = paths_typ (VarT(a, k3)) (varTs aks1) t1 in
- let t3' = subst_typ (subst aks1 tas1) (subst_typ (subst aks1 ts) t3) in
+ let t3' = subst_typ (subst aks1 tas1) (subst_typ (subst_of_match su) t3) in
  let t4 = RecT((a, k3), t3') in
 Trace.debug (lazy ("[RecT] t4 = " ^ string_of_norm_typ t4));
  let t = subst_typ (subst aks1 (List.map (subst_typ [a, t4]) tas1)) t1 in

regression.1ml

@@ -182,6 +182,9 @@ And = {
  type RDS = {A: {type t}, B: {type t}}
  & {A: {type t}, B: {v: A.t}}
  & {B: {type t}, A: {v: B.t}}
+
+ do {A = {t = bool, v = 1}, B = {t = int, v = true}} :> RDS
+ do {A = {t = bool, v = 1}, B = {t = int, v = true}} : RDS
 }
 
 ;;

sub.ml

@@ -167,33 +167,59 @@ let unify_typ t1 t2 =
  Trace.sub (lazy ("[unify_typ] t2 = " ^ string_of_norm_typ t2));
  unify_typ t1 t2
 
-let rec psubst p t =
+let rec psubst (p, t) =
  match p with
  | VarT(a, k) -> a, t
- | AppT(p', ts) -> psubst p' (LamT(List.map unvarT ts, t))
+ | AppT(p', ts) -> psubst (p', LamT(List.map unvarT ts, t))
  | _ -> assert false
 
+let rec var_of = function
+ | VarT(a, _) -> a
+ | AppT(p', _) -> var_of p'
+ | _ -> assert false
+
+let subst_of_match su = List.map (fun (p, t) -> var_of p, t) su
+
+let string_of_match su =
+ su
+ |> List.map (fun (p, t) ->
+ string_of_norm_typ t ^ " / " ^ string_of_norm_typ p)
+ |> String.concat ", "
+
 let rec sub_typ infer_binds env t1 t2 ps =
  let lift = lift (level ()) t1 in
  Trace.sub (lazy ("[sub_typ] t1 = " ^ string_of_norm_typ t1));
  Trace.sub (lazy ("[sub_typ] t2 = " ^ string_of_norm_typ t2));
  Trace.sub (lazy ("[sub_typ] ps = " ^
  String.concat ", " (List.map string_of_norm_typ ps)));
+ let su', zs', t2, ps =
+ if ps <> [] then
+ let su, zs' = match_typ infer_binds env t1 t2 ps in
+ Trace.sub (lazy ("[sub_typ] su = " ^ string_of_match su));
+ let t2 = subst_typ (List.map psubst su) t2 in
+ let ps = List.filter (fun p -> not (List.mem_assoc p su)) ps in
+ if ps <> [] then
+ Trace.sub (lazy ("[sub_typ] unmatched ps = " ^
+ String.concat ", " (List.map string_of_norm_typ ps)));
+ su, zs', t2, ps
+ else
+ [], [], t2, ps
+ in
  let e1 = IL.VarE("x") in
- let ts, zs, e =
+ let su, zs, e =
  match norm_typ t1, freshen_typ env (norm_typ t2) with
  | t1, FunT(aks21, t21, ExT(aks22, t22), Implicit) ->
  assert (aks22 = []);
- let ts, zs, f = sub_typ infer_binds (add_typs aks21 env) t1 t22 ps in
- List.map (fun t -> LamT(aks21, t)) ts, lift env zs,
+ let su, zs, f = sub_typ infer_binds (add_typs aks21 env) t1 t22 ps in
+ List.map (fun (p, t) -> (p, LamT(aks21, t))) su, lift env zs,
  IL.genE(erase_bind aks21, (IL.LamE("y", erase_typ t21, IL.AppE(f, e1))))
 
  | FunT(aks11, t11, ExT(aks12, t12), Implicit), t2 ->
  assert (aks12 = []);
  let ts1, zs1 = guess_typs (Env.domain_typ env) aks11 in
  let t1' = subst_typ (subst aks11 ts1) t12 in
- let ts2, zs2, f = sub_typ infer_binds env t1' t2 ps in
- ts2, zs1 @ zs2,
+ let su, zs2, f = sub_typ infer_binds env t1' t2 ps in
+ su, zs1 @ zs2,
  IL.AppE(f, IL.AppE(IL.instE(e1, List.map erase_typ ts1),
  materialize_typ (subst_typ (subst aks11 ts1) t11)))
 
@@ -202,15 +228,15 @@ let rec sub_typ infer_binds env t1 t2 ps =
  | ExT(aks1, t), ExT([], p1), p2::ps' when p1 = p2 ->
  if aks1 <> [] || not (!undecidable_flag || is_small_typ t) then
  raise (Sub (Mismatch (t1, t2)));
- [t], [], e1
+ [(p1, t)], [], e1
  | _ ->
  let zs = try equal_extyp env s1 s2 with Sub e -> raise (Sub (Type e)) in
  [], zs, e1
  )
 
  | StrT(tr1), StrT(tr2) ->
- let ts, zs, fs = sub_row infer_binds env tr1 tr2 ps in
- ts, zs,
+ let su, zs, fs = sub_row infer_binds env tr1 tr2 ps in
+ su, zs,
  IL.TupE(List.map2 (fun (l, _) f -> l, f l e1) tr2 fs)
 
  | TupT(tr1), TupT(tr2) ->
@@ -220,17 +246,18 @@ let rec sub_typ infer_binds env t1 t2 ps =
  | FunT(aks1, t11, s1, Explicit p1), FunT(aks2, t21, s2, Explicit p2) ->
  if p1 = Impure && p2 = Pure then raise (Sub (FunEffect(p1, p2)));
  let env' = add_typs aks2 env in
- let ts1, zs1, f1 =
+ let su1, zs1, f1 =
  try sub_typ infer_binds env' t21 t11 (varTs aks1) with Sub e ->
  raise (Sub (FunParam e)) in
  let ps' = List.map (fun p -> AppT(p, varTs aks2)) ps in
- let ts2, zs2, f2 =
- try sub_extyp infer_binds env' (subst_extyp (subst aks1 ts1) s1) s2 ps'
+ let su2, zs2, f2 =
+ try sub_extyp infer_binds env' (subst_extyp (subst_of_match su1) s1) s2 ps'
  with Sub e -> raise (Sub (FunResult e)) in
- List.map (fun t -> LamT(aks2, t)) ts2, lift env (zs1 @ zs2),
+ List.map (fun (p, t) -> (p, LamT(aks2, t))) su2, lift env (zs1 @ zs2),
  IL.genE(erase_bind aks2, (IL.LamE("y", erase_typ t21,
- IL.AppE(f2, IL.AppE(IL.instE(e1, List.map erase_typ ts1),
- IL.AppE(f1, IL.VarE("y")))))))
+ IL.AppE(f2,
+ IL.AppE(IL.instE(e1, List.map (fun (_, t) -> erase_typ t) su1),
+ IL.AppE(f1, IL.VarE("y")))))))
 
  | WrapT(s1), WrapT(s2) ->
  let _, zs, f =
@@ -277,26 +304,26 @@ let rec sub_typ infer_binds env t1 t2 ps =
  | InferT(z) as t1, (TypT(_) as t2) ->
  let t11, zs1 = guess_typ (Env.domain_typ env) BaseK in
  let t1' = TypT(ExT([], t11)) in
- let ts, zs2, f = sub_typ infer_binds env t1' t2 ps in
+ let su, zs2, f = sub_typ infer_binds env t1' t2 ps in
  if not (resolve_typ z t1') then raise (Sub (Mismatch(t1, t2)));
- ts, zs1 @ zs2, IL.AppE(f, e1)
+ su, zs1 @ zs2, IL.AppE(f, e1)
 
  | InferT(z) as t1, (StrT(tr2) as t2) ->
  (* TODO: row polymorphism *)
  let tzsr = map_row (fun _ -> guess_typ (Env.domain_typ env) BaseK) tr2 in
  let t1' = StrT(map_row fst tzsr) in
  let zs1 = List.concat (List.map snd (List.map snd tzsr)) in
- let ts, zs2, f = sub_typ infer_binds env t1' t2 ps in
+ let su, zs2, f = sub_typ infer_binds env t1' t2 ps in
  if not (resolve_typ z t1') then raise (Sub (Mismatch(t1, t2)));
- ts, zs1 @ zs2, IL.AppE(f, e1)
+ su, zs1 @ zs2, IL.AppE(f, e1)
 
  | InferT(z) as t1, (FunT([], t21, ExT([], t22), Explicit Impure) as t2) ->
  let t11, zs1 = guess_typ (Env.domain_typ env) BaseK in
  let t12, zs2 = guess_typ (Env.domain_typ env) BaseK in
  let t1' = FunT([], t11, ExT([], t12), Explicit Impure) in
- let ts, zs3, f = sub_typ infer_binds env t1' t2 ps in
+ let su, zs3, f = sub_typ infer_binds env t1' t2 ps in
  if not (resolve_typ z t1') then raise (Sub (Mismatch(t1, t2)));
- ts, zs1 @ zs2 @ zs3, IL.AppE(f, e1)
+ su, zs1 @ zs2 @ zs3, IL.AppE(f, e1)
 
  | InferT(z) as t1, t2 ->
  if not (resolve_typ z t2) then raise (Sub (Mismatch(t1, t2)));
@@ -305,26 +332,26 @@ let rec sub_typ infer_binds env t1 t2 ps =
  | TypT(_) as t1, (InferT(z) as t2) ->
  let t21, zs1 = guess_typ (Env.domain_typ env) BaseK in
  let t2' = TypT(ExT([], t21)) in
- let ts, zs2, f = sub_typ infer_binds env t1 t2' ps in
+ let su, zs2, f = sub_typ infer_binds env t1 t2' ps in
  if not (resolve_typ z t2') then raise (Sub (Mismatch(t1, t2)));
- ts, zs1 @ zs2, IL.AppE(f, e1)
+ su, zs1 @ zs2, IL.AppE(f, e1)
 
  | StrT(tr1) as t1, (InferT(z) as t2) ->
  (* TODO: row polymorphism *)
  let tzsr = map_row (fun _ -> guess_typ (Env.domain_typ env) BaseK) tr1 in
  let t2' = StrT(map_row fst tzsr) in
  let zs1 = List.concat (List.map snd (List.map snd tzsr)) in
- let ts, zs2, f = sub_typ infer_binds env t1 t2' ps in
+ let su, zs2, f = sub_typ infer_binds env t1 t2' ps in
  if not (resolve_typ z t2') then raise (Sub (Mismatch(t1, t2)));
- ts, zs1 @ zs2, IL.AppE(f, e1)
+ su, zs1 @ zs2, IL.AppE(f, e1)
 
  | FunT([], t11, ExT([], t12), Explicit p) as t1, (InferT(z) as t2) ->
  let t21, zs1 = guess_typ (Env.domain_typ env) BaseK in
  let t22, zs2 = guess_typ (Env.domain_typ env) BaseK in
  let t2' = FunT([], t21, ExT([], t22), Explicit Impure) in
- let ts, zs3, f = sub_typ infer_binds env t1 t2' ps in
+ let su, zs3, f = sub_typ infer_binds env t1 t2' ps in
  if not (resolve_typ z t2') then raise (Sub (Mismatch(t1, t2)));
- ts, zs1 @ zs2 @ zs3, IL.AppE(f, e1)
+ su, zs1 @ zs2 @ zs3, IL.AppE(f, e1)
 
  | t1, (InferT(z) as t2) ->
  if not (resolve_typ z t1) then raise (Sub (Mismatch(t1, t2)));
@@ -335,12 +362,12 @@ let rec sub_typ infer_binds env t1 t2 ps =
 
  | _ -> raise (Sub (Mismatch(t1, t2)))
  in
+ let su = su' @ su in
  Trace.sub (lazy ("[sub_typ] done t1 = " ^ string_of_norm_typ t1));
  Trace.sub (lazy ("[sub_typ] done t2 = " ^ string_of_norm_typ t2));
- Trace.sub (lazy ("[sub_typ] done ts = " ^
- String.concat ", " (List.map string_of_norm_typ ts)));
+ Trace.sub (lazy ("[sub_typ] done su = " ^ string_of_match su));
  Trace.sub (lazy ("[sub_typ] done x -> " ^ IL.string_of_exp e));
- ts, zs, IL.LamE("x", erase_typ t1, e)
+ su, zs' @ zs, IL.LamE("x", erase_typ t1, e)
 
 and sub_extyp infer_binds env s1 s2 ps =
  Trace.sub (lazy ("[sub_extyp] s1 = " ^ string_of_norm_extyp s1));
@@ -352,12 +379,12 @@ and sub_extyp infer_binds env s1 s2 ps =
  sub_typ infer_binds env t1 t2 ps
  | _ ->
  let lift = lift (level ()) t1 in
- let ts, zs, f =
+ let su, zs, f =
  sub_typ infer_binds (add_typs aks1 env) t1 t2 (varTs aks2) in
  [], lift env zs,
  IL.LamE("x", erase_extyp s1,
  IL.openE(IL.VarE("x"), List.map fst aks1, "y",
- IL.packE(List.map erase_typ ts,
+ IL.packE(List.map (fun (_, t) -> erase_typ t) su,
  IL.AppE(f, IL.VarE("y")), erase_extyp s2)))
 
 and sub_row infer_binds env tr1 tr2 ps =
@@ -367,13 +394,13 @@ and sub_row infer_binds env tr1 tr2 ps =
  | (l, t2)::tr2' ->
  Trace.sub (lazy ("[sub_row] l = " ^ l));
  let t1, zs, app = extract_bind infer_binds env tr1 l t2 in
- let ts1, zs1, f =
+ let su1, zs1, f =
  try sub_typ infer_binds env t1 t2 ps with
  | Sub e -> raise (Sub (Struct(l, e))) in
- let su = List.map2 psubst (Lib.List.take (List.length ts1) ps) ts1 in
- let ps' = Lib.List.drop (List.length ts1) ps in
- let ts2, zs2, fs = sub_row infer_binds env tr1 (subst_row su tr2') ps' in
- ts1 @ ts2, zs @ zs1 @ zs2, app f::fs
+ let ps = List.filter (fun p -> List.mem_assoc p su1) ps in
+ let su2, zs2, fs =
+  sub_row infer_binds env tr1 (subst_row (subst_of_match su1) tr2') ps in
+ su1 @ su2, zs @ zs1 @ zs2, app f::fs
 
 and equal_typ env t1 t2 =
  Trace.sub (lazy ("[equal_typ] t1 = " ^ string_of_norm_typ t1));
@@ -400,5 +427,81 @@ and equal_row env tr1 tr2 ps =
  try sub_row false env tr2 tr1 ps with Sub e -> raise (Sub (Right e)) in
  zs1 @ zs2
 
+and match_typ infer_binds env t1 t2 ps =
+ let lift = lift (level ()) t1 in
+ let t2 = norm_typ t2 in
+ Trace.sub (lazy ("[match_typ] t1 = " ^ string_of_norm_typ t1));
+ Trace.sub (lazy ("[match_typ] t2 = " ^ string_of_typ t2));
+ Trace.sub (lazy ("[match_typ] ps = " ^
+ String.concat ", " (List.map string_of_norm_typ ps)));
+ if not (has_typs t2) then [], [] else
+ match norm_typ t1, freshen_typ env t2 with
+ | t1, FunT(aks21, t21, ExT(aks22, t22), Implicit) ->
+ assert (aks22 = []);
+ let su, zs = match_typ infer_binds (add_typs aks21 env) t1 t22 ps in
+ List.map (fun (p, t) -> (p, LamT(aks21, t))) su, lift env zs
+
+ | FunT(aks11, t11, ExT(aks12, t12), Implicit), t2 ->
+ assert (aks12 = []);
+ let ts1, zs1 = guess_typs (Env.domain_typ env) aks11 in
+ let t1' = subst_typ (subst aks11 ts1) t12 in
+ let su, zs2 = match_typ infer_binds env t1' t2 ps in
+ su, zs1 @ zs2
+
+ | TypT(s1), TypT(s2) ->
+ (match s1, s2 with
+ | ExT(aks1, t), ExT([], p) when List.mem p ps ->
+ if aks1 <> [] || not (!undecidable_flag || is_small_typ t) then
+ raise (Sub (Mismatch (t1, t2)));
+ [(p, t)], []
+ | _ ->
+ [], [])
+
+ | StrT(tr1), StrT(tr2) ->
+ match_row infer_binds env tr1 tr2 ps
+
+ | FunT(aks1, t11, s1, Explicit p1), FunT(aks2, t21, s2, Explicit p2) ->
+ if p1 = Impure && p2 = Pure then raise (Sub (FunEffect(p1, p2)));
+ if p1 <> Pure || p2 <> Pure then
+ [], []
+ else
+ let env' = add_typs aks2 env in
+ let su1, zs1, f1 =
+ try sub_typ infer_binds env' t21 t11 (varTs aks1) with Sub e ->
+ raise (Sub (FunParam e)) in
+ let ps' = List.map (fun p -> AppT(p, varTs aks2)) ps in
+ let su, zs2 =
+ try match_extyp
+ infer_binds env' (subst_extyp (subst_of_match su1) s1) s2 ps'
+ with Sub e -> raise (Sub (FunResult e)) in
+ List.map (function (AppT(p, _), t) -> (p, LamT(aks2, t))
+ | _ -> assert false) su, lift env (zs1 @ zs2)
+
+ | _ ->
+ [], []
+
+and match_extyp infer_binds env s1 s2 ps =
+ let ExT(aks2, t2) = freshen_extyp env s2 in
+ let ExT(aks1, t1) = freshen_extyp (add_typs aks2 env) s1 in
+ match aks1, aks2 with
+ | [], [] ->
+ match_typ infer_binds env t1 t2 ps
+ | _ ->
+ [], []
+
+and match_row infer_binds env tr1 tr2 ps =
+ match tr2 with
+ | [] ->
+ [], []
+ | (l, t2)::tr2' ->
+ let t1, zs, app = extract_bind infer_binds env tr1 l t2 in
+ let su1, zs1 =
+ try match_typ infer_binds env t1 t2 ps with
+ | Sub e -> raise (Sub (Struct(l, e)))
+ in
+ let su2, zs2 =
+ match_row infer_binds env tr1 (subst_row (List.map psubst su1) tr2') ps in
+ su1 @ su2, zs @ zs1 @ zs2
+
 let sub_typ = sub_typ true
 let sub_extyp = sub_extyp true

sub.mli

@@ -25,12 +25,18 @@ val string_of_error : error -> string
 
 val sub_typ :
  Env.env -> Types.typ -> Types.typ -> Types.typ list ->
- Types.typ list * Types.infer ref list * Fomega.exp (* raise Sub *)
+ (Types.typ * Types.typ) list * Types.infer ref list * Fomega.exp (* raise Sub *)
 val sub_extyp :
  Env.env -> Types.extyp -> Types.extyp -> Types.typ list ->
- Types.typ list * Types.infer ref list * Fomega.exp (* raise Sub *)
+ (Types.typ * Types.typ) list * Types.infer ref list * Fomega.exp (* raise Sub *)
 
 val equal_typ :
  Env.env -> Types.typ -> Types.typ -> Types.infer ref list (* raise Sub *)
 val equal_extyp :
  Env.env -> Types.extyp -> Types.extyp -> Types.infer ref list (* raise Sub *)
+
+val subst_of_match: (Types.typ * Types.typ) list -> (Types.var * Types.typ) list
+
+(* String conversion *)
+
+val string_of_match: (Types.typ * Types.typ) list -> string