Type-level use

src/boot/lib/ast.ml

@@ -383,6 +383,8 @@ and ty =
   | TyVar of info * ustring
   (* Type application *)
   | TyApp of info * ty * ty
+  (* Type-level use *)
+  | TyUse of info * ustring * ty
 
 (* Kind of identifier *)
 and ident =
@@ -523,6 +525,9 @@ let smap_accum_left_ty_ty (f : 'a -> ty -> 'a * ty) (acc : 'a) : ty -> 'a * ty =
      let acc, l = f acc l in
      let acc, r = f acc r in
      (acc, TyApp (fi, l, r))
+  | TyUse (fi, lang, ty) ->
+     let acc, ty = f acc ty in
+     (acc, TyUse (fi, lang, ty))
   | (TyUnknown _ | TyBool _ | TyInt _ | TyFloat _ | TyChar _ | TyVariant _ | TyCon _ | TyVar _) as ty -> (acc, ty)
 
 let smap_accum_left_tm_pat (f : 'a -> pat -> 'a * pat) (acc : 'a) : tm -> 'a * tm = function
@@ -660,6 +665,7 @@ let ty_info = function
   | TyVariant (fi, _)
   | TyCon (fi, _)
   | TyVar (fi, _)
+  | TyUse (fi, _, _)
   | TyApp (fi, _, _) ->
       fi
 

src/boot/lib/mlang.ml

@@ -386,6 +386,12 @@ let rec translate_ty (env : mlang_env) : ty -> ty = function
      | Some id -> TyCon (fi, id)
      | None -> TyCon (fi, empty_mangle id)
      end
+  | TyUse (fi, lang, ty) ->
+     begin match Record.find_opt lang env.language_envs with
+     | Some new_env -> translate_ty (merge_env_prefer_right env new_env) ty
+     | None -> raise_error fi
+                 ( "Unbound language fragment '" ^ Ustring.to_utf8 lang ^ "'" )
+     end
   | ty ->
      let ty = smap_ty_ty (translate_ty env) ty in
      ty

src/boot/lib/parser.mly

@@ -555,6 +555,9 @@ ty:
   | ALL var_ident DOT ty
       { let fi = mkinfo $1.i (ty_info $4) in
         TyAll(fi, $2.v, $4) }
+  | USE ident IN ty
+      { let fi = mkinfo $1.i $3.i in
+        TyUse(fi, $2.v, $4) }
 
 ty_left:
   | ty_atom

src/boot/lib/pprint.ml

@@ -208,6 +208,8 @@ let rec ustring_of_ty = function
       pprint_type_str x
   | TyVar (_, x) ->
       pprint_var_str x
+  | TyUse (_, lang, ty) ->
+     us"use " ^. lang ^. us" in " ^. ustring_of_ty ty
   | TyApp (_, ty1, ty2) ->
       us "(" ^. ustring_of_ty ty1 ^. us " " ^. ustring_of_ty ty2 ^. us ")"