diff --git a/src/bin/sail.ml b/src/bin/sail.ml
index f29cd1e7c..42af7ad80 100644
--- a/src/bin/sail.ml
+++ b/src/bin/sail.ml
@@ -68,14 +68,14 @@
 open Libsail
 
 let opt_new_cli = ref false
-let opt_file_arguments : string list ref = ref []
+let opt_free_arguments : string list ref = ref []
 let opt_file_out : string option ref = ref None
 let opt_just_check : bool ref = ref false
 let opt_auto_interpreter_rewrites : bool ref = ref false
 let opt_interactive_script : string option ref = ref None
 let opt_splice : string list ref = ref []
 let opt_print_version = ref false
-let opt_memo_z3 = ref false
+let opt_memo_z3 = ref true
 let opt_have_feature = ref None
 let opt_show_sail_dir = ref false
 let opt_project_file : string option ref = ref None
@@ -356,13 +356,33 @@ let file_to_string filename =
 
 let run_sail (config : Yojson.Basic.t option) tgt =
   Target.run_pre_parse_hook tgt ();
+
+  let rigging_files, frees = List.partition (fun free -> Filename.check_suffix free ".rigging") !opt_free_arguments in
+
   let ast, env, effect_info =
-    match !opt_project_file with
-    | Some file ->
+    match rigging_files with
+    | [] ->
+        (* If there are no provided rigging files, we concatenate all
+           the free file arguments into one big blob like before *)
+        Frontend.load_files ~target:tgt Manifest.dir !options Type_check.initial_env frees
+    | _ ->
         let t = Profile.start () in
-        let root_directory = Filename.dirname file in
-        let defs = Initial_check.parse_project ~filename:file ~contents:(file_to_string file) in
-        let proj = Project.initialize_project_structure ~root_directory defs in
+        let defs =
+          List.map
+            (fun rigging_file ->
+              let root_directory = Filename.dirname rigging_file in
+              let contents = file_to_string rigging_file in
+              Project.mk_root root_directory :: Initial_check.parse_project ~filename:rigging_file ~contents ()
+            )
+            rigging_files
+          |> List.concat
+        in
+        let proj = Project.initialize_project_structure defs in
+        if !opt_list_files then (
+          let files = Project.all_files proj in
+          print_endline (Util.string_of_list " " fst files);
+          exit 0
+        );
         let mod_ids =
           List.map
             (fun mod_name ->
@@ -370,11 +390,11 @@ let run_sail (config : Yojson.Basic.t option) tgt =
               | Some id -> id
               | None -> raise (Reporting.err_general Parse_ast.Unknown ("Unknown module " ^ mod_name))
             )
-            !opt_file_arguments
+            frees
         in
         Profile.finish "parsing project" t;
-        Frontend.load_modules ~target:tgt Manifest.dir !options Type_check.initial_env proj mod_ids
-    | None -> Frontend.load_files ~target:tgt Manifest.dir !options Type_check.initial_env !opt_file_arguments
+        let env = Type_check.initial_env_with_modules proj in
+        Frontend.load_modules ~target:tgt Manifest.dir !options env proj mod_ids
   in
   let ast, env = Frontend.initial_rewrite effect_info env ast in
   let ast, env = List.fold_right (fun file (ast, _) -> Splice.splice ast file) !opt_splice (ast, env) in
@@ -402,7 +422,7 @@ let run_sail_format (config : Yojson.Basic.t option) =
       | None -> Format_sail.default_config
   end in
   let module Formatter = Format_sail.Make (Config) in
-  let parsed_files = List.map (fun f -> (f, Initial_check.parse_file f)) !opt_file_arguments in
+  let parsed_files = List.map (fun f -> (f, Initial_check.parse_file f)) !opt_free_arguments in
   List.iter
     (fun (f, (comments, parse_ast)) ->
       let source = file_to_string f in
@@ -485,7 +505,7 @@ let main () =
       )
   end;
 
-  Arg.parse_dynamic options (fun s -> opt_file_arguments := !opt_file_arguments @ [s]) usage_msg;
+  Arg.parse_dynamic options (fun s -> opt_free_arguments := !opt_free_arguments @ [s]) usage_msg;
 
   let config = Option.bind (get_config_file ()) parse_config_file in
 
diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml
index b6f77022f..84280fe13 100644
--- a/src/lib/chunk_ast.ml
+++ b/src/lib/chunk_ast.ml
@@ -1277,7 +1277,7 @@ let chunk_def source last_line_span comments chunks (DEF_aux (def, l)) =
   begin
     match def with
     | DEF_fundef fdef -> chunk_fundef comments chunks fdef
-    | DEF_pragma (pragma, arg) ->
+    | DEF_pragma (pragma, arg, _) ->
         Queue.add (Pragma (pragma, arg)) chunks;
         pragma_span := true
     | DEF_default dts -> chunk_default_typing_spec comments chunks dts
diff --git a/src/lib/frontend.ml b/src/lib/frontend.ml
index bc61d1667..efb3074f4 100644
--- a/src/lib/frontend.ml
+++ b/src/lib/frontend.ml
@@ -93,17 +93,10 @@ let wrap_module proj parsed_module =
   let module P = Parse_ast in
   let open Project in
   let name, l = module_name proj parsed_module.id in
-  let bracket_pragma p = P.DEF_aux (P.DEF_pragma (p, Printf.sprintf "%d %s" parsed_module.id name), to_loc l) in
-  let require_pragma =
-    let reqs = module_requires proj parsed_module.id in
-    if Util.list_empty reqs then []
-    else [P.DEF_aux (P.DEF_pragma ("require#", Util.string_of_list " " string_of_int reqs), to_loc l)]
-  in
+  let bracket_pragma p = P.DEF_aux (P.DEF_pragma (p, name, 1), to_loc l) in
   parsed_module.files
-  |> Util.update_first (fun (f, (comments, defs)) ->
-         (f, (comments, (bracket_pragma "module_start#" :: require_pragma) @ defs))
-     )
-  |> Util.update_last (fun (f, (comments, defs)) -> (f, (comments, defs @ [bracket_pragma "module_end#"])))
+  |> Util.update_first (fun (f, (comments, defs)) -> (f, (comments, bracket_pragma "start_module#" :: defs)))
+  |> Util.update_last (fun (f, (comments, defs)) -> (f, (comments, defs @ [bracket_pragma "end_module#"])))
 
 let process_ast target type_envs ast =
   if !opt_ddump_initial_ast then Pretty_print_sail.pp_ast stdout ast;
diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml
index 21da88fc8..29c7a48c2 100644
--- a/src/lib/initial_check.ml
+++ b/src/lib/initial_check.ml
@@ -1248,6 +1248,17 @@ let check_annotation (DEF_aux (aux, def_annot)) =
     | _ -> ()
   )
 
+let pragma_arg_loc pragma arg_left_trim l =
+  let open Lexing in
+  Reporting.map_loc_range
+    (fun p1 p2 ->
+      let left_trim = String.length pragma + arg_left_trim + 1 in
+      let p1 = { p1 with pos_cnum = p1.pos_cnum + left_trim } in
+      let p2 = { p2 with pos_cnum = p2.pos_cnum - 1; pos_bol = p1.pos_bol; pos_lnum = p1.pos_lnum } in
+      (p1, p2)
+    )
+    l
+
 let rec to_ast_def doc attrs ctx (P.DEF_aux (def, l)) : uannot def list ctx_out =
   let annot = mk_def_annot ?doc ~attrs l in
   match def with
@@ -1305,25 +1316,30 @@ let rec to_ast_def doc attrs ctx (P.DEF_aux (def, l)) : uannot def list ctx_out
   | P.DEF_register dec ->
       let d = to_ast_dec ctx dec in
       ([DEF_aux (DEF_register d, annot)], ctx)
-  | P.DEF_pragma ("sail_internal", arg) -> begin
-      match Reporting.loc_file l with
-      | Some file ->
-          ( [DEF_aux (DEF_pragma ("sail_internal", arg, l), annot)],
-            { ctx with internal_files = StringSet.add file ctx.internal_files }
-          )
-      | None -> ([DEF_aux (DEF_pragma ("sail_internal", arg, l), annot)], ctx)
-    end
-  | P.DEF_pragma ("target_set", arg) ->
-      let args = String.split_on_char ' ' arg |> List.filter (fun s -> String.length s > 0) in
+  | P.DEF_pragma (pragma, arg, ltrim) ->
+      let l = pragma_arg_loc pragma ltrim l in
       begin
-        match args with
-        | set :: targets ->
-            ( [DEF_aux (DEF_pragma ("target_set", arg, l), annot)],
-              { ctx with target_sets = StringMap.add set targets ctx.target_sets }
-            )
-        | [] -> raise (Reporting.err_general l "No arguments provided to target set directive")
+        match pragma with
+        | "sail_internal" -> begin
+            match Reporting.loc_file l with
+            | Some file ->
+                ( [DEF_aux (DEF_pragma ("sail_internal", arg, l), annot)],
+                  { ctx with internal_files = StringSet.add file ctx.internal_files }
+                )
+            | None -> ([DEF_aux (DEF_pragma ("sail_internal", arg, l), annot)], ctx)
+          end
+        | "target_set" ->
+            let args = String.split_on_char ' ' arg |> List.filter (fun s -> String.length s > 0) in
+            begin
+              match args with
+              | set :: targets ->
+                  ( [DEF_aux (DEF_pragma ("target_set", arg, l), annot)],
+                    { ctx with target_sets = StringMap.add set targets ctx.target_sets }
+                  )
+              | [] -> raise (Reporting.err_general l "No arguments provided to target set directive")
+            end
+        | _ -> ([DEF_aux (DEF_pragma (pragma, arg, l), annot)], ctx)
       end
-  | P.DEF_pragma (pragma, arg) -> ([DEF_aux (DEF_pragma (pragma, arg, l), annot)], ctx)
   | P.DEF_internal_mutrec _ ->
       (* Should never occur because of remove_mutrec *)
       raise (Reporting.err_unreachable l __POS__ "Internal mutual block found when processing scattered defs")
@@ -1773,11 +1789,20 @@ let parse_file_from_string ~filename:f ~contents:s =
     let tok = Lexing.lexeme lexbuf in
     raise (Reporting.err_syntax pos ("current token: " ^ tok))
 
-let parse_project ~filename:f ~contents:s =
+let parse_project ?inline ?filename:f ~contents:s () =
   let open Project in
   let open Lexing in
   let lexbuf = from_string s in
-  lexbuf.lex_curr_p <- { pos_fname = f; pos_lnum = 1; pos_bol = 0; pos_cnum = 0 };
+
+  (* Note that OCaml >= 4.11 has a much less hacky way of doing this *)
+  begin
+    match inline with
+    | Some p ->
+        lexbuf.lex_curr_p <- p;
+        lexbuf.lex_abs_pos <- p.pos_cnum
+    | None -> lexbuf.lex_curr_p <- { pos_fname = Option.get f; pos_lnum = 1; pos_bol = 0; pos_cnum = 0 }
+  end;
+
   try Project_parser.file Project_lexer.token lexbuf
   with Project_parser.Error ->
     let pos = Lexing.lexeme_start_p lexbuf in
diff --git a/src/lib/initial_check.mli b/src/lib/initial_check.mli
index 9dafc892b..cbb7c92c1 100644
--- a/src/lib/initial_check.mli
+++ b/src/lib/initial_check.mli
@@ -139,4 +139,5 @@ val parse_file : ?loc:Parse_ast.l -> string -> Lexer.comment list * Parse_ast.de
 
 val parse_file_from_string : filename:string -> contents:string -> Lexer.comment list * Parse_ast.def list
 
-val parse_project : filename:string -> contents:string -> Project.def Project.spanned list
+val parse_project :
+  ?inline:Lexing.position -> ?filename:string -> contents:string -> unit -> Project.def Project.spanned list
diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll
index 6d50d89d7..09956aa3a 100644
--- a/src/lib/lexer.mll
+++ b/src/lib/lexer.mll
@@ -224,7 +224,10 @@ rule token = parse
   | "$[" (ident+ as i)
     { let attr = attribute 0 (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf in Attribute(i, String.trim attr) }
   | "$" (ident+ as i)
-    { let p = pragma (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) false lexbuf in Pragma(i, String.trim p) }
+    { let startpos = Lexing.lexeme_start_p lexbuf in
+      let arg = pragma (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) false lexbuf in
+      lexbuf.lex_start_p <- startpos;
+      Pragma (i, arg) }
   | "infix" ws (digit as p) ws (operator as op)
     { Fixity (Infix, Big_int.of_string (Char.escaped p), op) }
   | "infixl" ws (digit as p) ws (operator as op)
diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml
index 5a6d73841..d53bb5037 100644
--- a/src/lib/parse_ast.ml
+++ b/src/lib/parse_ast.ml
@@ -439,7 +439,7 @@ type def_aux =
   | DEF_measure of id * pat * exp (* separate termination measure declaration *)
   | DEF_loop_measures of id * loop_measure list (* separate termination measure declaration *)
   | DEF_register of dec_spec (* register declaration *)
-  | DEF_pragma of string * string
+  | DEF_pragma of string * string * int
   | DEF_attribute of string * string * def
   | DEF_doc of string * def
   | DEF_internal_mutrec of fundef list
diff --git a/src/lib/parser.mly b/src/lib/parser.mly
index a43ed8fe0..d95864af2 100644
--- a/src/lib/parser.mly
+++ b/src/lib/parser.mly
@@ -233,6 +233,20 @@ let fix_extern typschm = function
 let funcl_annot fs fcl =
   List.fold_right (fun f fcl -> f fcl) fs fcl
 
+let pragma_left_spaces pragma p s =
+  let n = ref 0 in
+  while !n < String.length s && (s.[!n] = ' ' || s.[!n] = '\t') do
+    if s.[!n] = '\t' then (
+      (* If find a tab we won't be able to correctly format errors
+         found in the directive argument. It would be very weird for a
+         tab to show up here, so just bail. *)
+      let p = { p with Lexing.pos_cnum = p.Lexing.pos_cnum + String.length pragma + 1 + !n } in
+      raise (Reporting.err_lex p "Tab character (\\t) found between directive and argument. Please use spaces.")
+    );
+    incr n
+  done;
+  !n
+
 let effect_deprecated l =
   Reporting.warn ~once_from:__POS__ "Deprecated" l "Explicit effect annotations are deprecated. They are no longer used and can be removed."
 
@@ -1319,7 +1333,9 @@ def_aux:
   | Mutual Lcurly fun_def_list Rcurly
     { DEF_internal_mutrec $3 }
   | Pragma
-    { DEF_pragma (fst $1, snd $1) }
+    { let (pragma, arg) = $1 in
+      let ltrim = pragma_left_spaces pragma $startpos arg in
+      DEF_pragma (pragma, String.trim arg, ltrim) }
   | TerminationMeasure id pat Eq exp
     { DEF_measure ($2, $3, $5) }
   | TerminationMeasure id loop_measures
diff --git a/src/lib/preprocess.ml b/src/lib/preprocess.ml
index ad5107f5f..86cc006f7 100644
--- a/src/lib/preprocess.ml
+++ b/src/lib/preprocess.ml
@@ -70,6 +70,19 @@ open Parse_ast
 (* Simple preprocessor features for conditional file loading *)
 module StringSet = Set.Make (String)
 
+(* Adjust a pragma location so it doesn't end after the newline. *)
+let pragma_loc l =
+  let open Lexing in
+  Reporting.map_loc_range
+    (fun p1 p2 ->
+      if p1.pos_lnum + 1 = p2.pos_lnum then (
+        let p2 = { p2 with pos_cnum = p2.pos_cnum - 1; pos_bol = p1.pos_bol; pos_lnum = p1.pos_lnum } in
+        (p1, p2)
+      )
+      else (p1, p2)
+    )
+    l
+
 let default_symbols =
   List.fold_left
     (fun set str -> StringSet.add str set)
@@ -110,22 +123,22 @@ let cond_pragma l defs =
   let push_def def = if !in_then then then_defs := def :: !then_defs else else_defs := def :: !else_defs in
 
   let rec scan = function
-    | DEF_aux (DEF_pragma ("endif", _), _) :: defs when !depth = 0 -> (List.rev !then_defs, List.rev !else_defs, defs)
-    | DEF_aux (DEF_pragma ("else", _), _) :: defs when !depth = 0 ->
+    | DEF_aux (DEF_pragma ("endif", _, _), _) :: defs when !depth = 0 -> (List.rev !then_defs, List.rev !else_defs, defs)
+    | DEF_aux (DEF_pragma ("else", _, _), _) :: defs when !depth = 0 ->
         in_then := false;
         scan defs
-    | (DEF_aux (DEF_pragma (p, _), _) as def) :: defs when p = "ifdef" || p = "ifndef" || p = "iftarget" ->
+    | (DEF_aux (DEF_pragma (p, _, _), _) as def) :: defs when p = "ifdef" || p = "ifndef" || p = "iftarget" ->
         incr depth;
         push_def def;
         scan defs
-    | (DEF_aux (DEF_pragma ("endif", _), _) as def) :: defs ->
+    | (DEF_aux (DEF_pragma ("endif", _, _), _) as def) :: defs ->
         decr depth;
         push_def def;
         scan defs
     | def :: defs ->
         push_def def;
         scan defs
-    | [] -> raise (Reporting.err_general l "$ifdef, $ifndef, or $iftarget never ended by $endif")
+    | [] -> raise (Reporting.err_general (pragma_loc l) "$ifdef, $ifndef, or $iftarget never ended by $endif")
   in
   scan defs
 
@@ -161,16 +174,18 @@ let all_pragmas =
 
 let wrap_include l file = function
   | [] -> []
-  | defs -> [DEF_aux (DEF_pragma ("include_start", file), l)] @ defs @ [DEF_aux (DEF_pragma ("include_end", file), l)]
+  | defs ->
+      [DEF_aux (DEF_pragma ("include_start", file, 1), l)] @ defs @ [DEF_aux (DEF_pragma ("include_end", file, 1), l)]
 
 let preprocess dir target opts =
   let module P = Parse_ast in
   let rec aux acc = function
     | [] -> List.rev acc
-    | DEF_aux (DEF_pragma ("define", symbol), _) :: defs ->
+    | DEF_aux (DEF_pragma ("define", symbol, _), _) :: defs ->
         symbols := StringSet.add symbol !symbols;
         aux acc defs
-    | (DEF_aux (DEF_pragma ("option", command), l) as opt_pragma) :: defs ->
+    | (DEF_aux (DEF_pragma ("option", command, _), l) as opt_pragma) :: defs ->
+        let l = pragma_loc l in
         begin
           let first_line err_msg =
             match String.split_on_char '\n' err_msg with line :: _ -> "\n" ^ line | [] -> ("" [@coverage off])
@@ -188,28 +203,30 @@ let preprocess dir target opts =
           | Arg.Bad msg -> raise (Reporting.err_general l ("Invalid flag passed to $option directive" ^ first_line msg))
         end;
         aux (opt_pragma :: acc) defs
-    | DEF_aux (DEF_pragma ("ifndef", symbol), l) :: defs ->
+    | DEF_aux (DEF_pragma ("ifndef", symbol, _), l) :: defs ->
         let then_defs, else_defs, defs = cond_pragma l defs in
         if not (StringSet.mem symbol !symbols) then aux acc (then_defs @ defs) else aux acc (else_defs @ defs)
-    | DEF_aux (DEF_pragma ("ifdef", symbol), l) :: defs ->
+    | DEF_aux (DEF_pragma ("ifdef", symbol, _), l) :: defs ->
         let then_defs, else_defs, defs = cond_pragma l defs in
         if StringSet.mem symbol !symbols then aux acc (then_defs @ defs) else aux acc (else_defs @ defs)
-    | DEF_aux (DEF_pragma ("iftarget", t), l) :: defs ->
+    | DEF_aux (DEF_pragma ("iftarget", t, _), l) :: defs ->
         let then_defs, else_defs, defs = cond_pragma l defs in
         begin
           match target with Some t' when t = t' -> aux acc (then_defs @ defs) | _ -> aux acc (else_defs @ defs)
         end
-    | DEF_aux (DEF_pragma ("include", file), l) :: defs ->
+    | DEF_aux (DEF_pragma ("include", file, _), l) :: defs ->
         let len = String.length file in
         if len = 0 then (
-          Reporting.warn "" l "Skipping bad $include. No file argument.";
+          Reporting.warn "" (pragma_loc l) "Skipping bad $include. No file argument.";
           aux acc defs
         )
         else if file.[0] = '"' && file.[len - 1] = '"' then (
           let relative =
             match l with
             | Parse_ast.Range (pos, _) -> Filename.dirname Lexing.(pos.pos_fname)
-            | _ -> failwith "Couldn't figure out relative path for $include. This really shouldn't ever happen."
+            | _ ->
+                Reporting.unreachable (pragma_loc l) __POS__
+                  "Couldn't figure out relative path for $include. This really shouldn't ever happen."
           in
           let file = String.sub file 1 (len - 2) in
           let include_file = Filename.concat relative file in
@@ -225,10 +242,10 @@ let preprocess dir target opts =
         )
         else (
           let help = "Make sure the filename is surrounded by quotes or angle brackets" in
-          Reporting.warn "" l ("Skipping bad $include " ^ file ^ ". " ^ help);
+          Reporting.warn "" (pragma_loc l) ("Skipping bad $include " ^ file ^ ". " ^ help);
           aux acc defs
         )
-    | DEF_aux (DEF_pragma ("suppress_warnings", _), l) :: defs ->
+    | DEF_aux (DEF_pragma ("suppress_warnings", _, _), l) :: defs ->
         begin
           match Reporting.simp_loc l with
           | None -> () (* This shouldn't happen, but if it does just continue *)
@@ -238,11 +255,12 @@ let preprocess dir target opts =
     (* Filter file_start and file_end out of the AST so when we
        round-trip files through the compiler we don't end up with
        incorrect start/end annotations *)
-    | (DEF_aux (DEF_pragma ("file_start", _), _) | DEF_aux (DEF_pragma ("file_end", _), _)) :: defs -> aux acc defs
-    | DEF_aux (DEF_pragma (p, arg), l) :: defs ->
+    | (DEF_aux (DEF_pragma ("file_start", _, _), _) | DEF_aux (DEF_pragma ("file_end", _, _), _)) :: defs ->
+        aux acc defs
+    | (DEF_aux (DEF_pragma (p, _, _), l) as pragma_def) :: defs ->
         if not (StringSet.mem p all_pragmas || String.contains p '#') then
-          Reporting.warn "" l ("Unrecognised directive: " ^ p);
-        aux (DEF_aux (DEF_pragma (p, arg), l) :: acc) defs
+          Reporting.warn "" (pragma_loc l) ("Unrecognised directive: " ^ p);
+        aux (pragma_def :: acc) defs
     | DEF_aux (DEF_outcome (outcome_spec, inner_defs), l) :: defs ->
         aux (DEF_aux (DEF_outcome (outcome_spec, aux [] inner_defs), l) :: acc) defs
     | (DEF_aux (DEF_default (DT_aux (DT_order (_, ATyp_aux (atyp, _)), _)), l) as def) :: defs -> begin
diff --git a/src/lib/project.ml b/src/lib/project.ml
index 5b12662b9..b8a817592 100644
--- a/src/lib/project.ml
+++ b/src/lib/project.ml
@@ -114,7 +114,9 @@ type mdl_def = M_dep of dependency | M_directory of exp spanned | M_module of md
 
 and mdl = { name : string spanned; defs : mdl_def spanned list; span : l }
 
-type def = Def_var of string spanned * exp spanned | Def_module of mdl | Def_test of string list
+type def = Def_root of string | Def_var of string spanned * exp spanned | Def_module of mdl | Def_test of string list
+
+let mk_root root = (Def_root root, (Lexing.dummy_pos, Lexing.dummy_pos))
 
 class type project_visitor = object
   method vexp : exp spanned -> exp spanned visit_action
@@ -122,6 +124,8 @@ class type project_visitor = object
   method vmodule : mdl -> mdl visit_action
   method vdef : def spanned -> def spanned visit_action
 
+  method on_root_change : string -> unit
+
   method short_circuit_if : bool
 end
 
@@ -197,13 +201,16 @@ let rec visit_module vis (outer_module : mdl) =
 let visit_def vis outer_def =
   let aux vis no_change =
     match no_change with
+    | Def_test _, _ -> no_change
     | Def_var (v, exp), l ->
         let exp' = visit_exp vis exp in
         if exp == exp' then no_change else (Def_var (v, exp'), l)
     | Def_module m, l ->
         let m' = visit_module vis m in
         if m == m' then no_change else (Def_module m', l)
-    | Def_test _, _ -> no_change
+    | Def_root root, _ ->
+        vis#on_root_change root;
+        no_change
   in
   do_visit vis (vis#vdef outer_def) aux outer_def
 
@@ -227,6 +234,8 @@ class empty_project_visitor : project_visitor =
     method vmodule _ = DoChildren
     method vdef _ = DoChildren
 
+    method on_root_change _ = ()
+
     method short_circuit_if = false
   end
 
@@ -328,7 +337,6 @@ class eval_visitor (vars : value StringMap.t ref) =
 type project_structure = {
   names : string spanned array;
   ids : int StringMap.t;
-  root_directory : string;
   mutable parents : int ModMap.t;
   mutable children : ModGraph.graph;
   mutable files : string spanned list ModMap.t;
@@ -386,12 +394,17 @@ let rec collect_files = function
   | _ :: mdefs -> collect_files mdefs
   | [] -> []
 
+let add_root root_opt (file, l) =
+  match root_opt with Some root -> (root ^ Filename.dir_sep ^ file, l) | None -> (file, l)
+
 class structure_visitor (proj : project_structure) =
   object
     inherit empty_project_visitor
 
     val mutable parents : int list = []
 
+    val mutable last_root : string option = None
+
     method vexp _ = SkipChildren
     method vdependency _ _ = SkipChildren
 
@@ -399,7 +412,7 @@ class structure_visitor (proj : project_structure) =
       let name = fst m.name in
       let id = StringMap.find name proj.ids in
       let files = collect_files m.defs in
-      proj.files <- ModMap.add id files proj.files;
+      proj.files <- ModMap.add id (List.map (add_root last_root) files) proj.files;
       link_parent id parents proj;
       parents <- id :: parents;
       ChangeDoChildrenPost
@@ -408,6 +421,8 @@ class structure_visitor (proj : project_structure) =
             parents <- List.tl parents;
             m
         )
+
+    method on_root_change new_root = last_root <- Some new_root
   end
 
 (**************************************************************************)
@@ -441,7 +456,7 @@ let get_from_frame f stack proj =
                | S_only, Some id -> ModSet.add id acc
                | S_tree, Some id ->
                    ModSet.union acc (ModGraph.reachable (ModSet.singleton id) ModSet.empty proj.children)
-               | _, None -> raise (Reporting.err_general (to_loc l) (name ^ " does not exist"))
+               | _, None -> raise (Reporting.err_general (to_loc l) ("Module " ^ name ^ " does not exist"))
              )
              acc (f frame)
           )
@@ -541,7 +556,7 @@ let run_tests defs (proj : project_structure) =
   in
   List.iter (function Def_test (cmd :: args), l -> run_test_cmd l cmd args | _ -> ()) defs
 
-let initialize_project_structure ~root_directory defs =
+let initialize_project_structure defs =
   (* Visit all the declared modules and assign them module ids *)
   let xs = ref [] in
   let _ = visit_defs (new order_visitor xs) defs in
@@ -556,7 +571,6 @@ let initialize_project_structure ~root_directory defs =
     {
       names;
       ids;
-      root_directory;
       parents = ModMap.empty;
       children = ModMap.empty;
       files = ModMap.empty;
@@ -590,6 +604,8 @@ let required_modules ~roots (proj : project_structure) =
   let reqs = ModGraph.prune roots ModSet.empty proj.requires in
   fun id -> ModMap.mem id reqs
 
+let valid_module_id proj id = 0 <= id && id < Array.length proj.names
+
 let module_name proj id = proj.names.(id)
 
 let module_order proj =
@@ -610,9 +626,8 @@ let module_order proj =
   in
   flatten sccs
 
-let module_files proj id =
-  List.map (fun (f, l) -> (proj.root_directory ^ Filename.dir_sep ^ f, l)) (ModMap.find id proj.files)
+let module_files proj id = ModMap.find id proj.files
 
 let module_requires (proj : project_structure) id = ModMap.find id proj.requires |> ModSet.elements
 
-let file_list modules proj = List.map (fun id -> ModMap.find id proj.files) modules |> List.concat
+let all_files proj = List.map (fun id -> ModMap.find id proj.files) (module_order proj) |> List.concat
diff --git a/src/lib/project.mli b/src/lib/project.mli
index 0876edd5f..b975aaddc 100644
--- a/src/lib/project.mli
+++ b/src/lib/project.mli
@@ -103,27 +103,31 @@ type mdl_def = M_dep of dependency | M_directory of exp spanned | M_module of md
 
 and mdl = { name : string spanned; defs : mdl_def spanned list; span : l }
 
-type def = Def_var of string spanned * exp spanned | Def_module of mdl | Def_test of string list
+type def = Def_root of string | Def_var of string spanned * exp spanned | Def_module of mdl | Def_test of string list
+
+val mk_root : string -> def spanned
 
 type project_structure
 
-val initialize_project_structure : root_directory:string -> def spanned list -> project_structure
+val initialize_project_structure : def spanned list -> project_structure
 
 val get_module_id : project_structure -> string -> mod_id option
 
 val get_children : mod_id -> project_structure -> ModSet.t
 
 (** Create a predicate that returns true for any module that is
-    (transitively) required by any module in the root set of
+    (transitively) required by any module in the roots set of
     modules. *)
 val required_modules : roots:ModSet.t -> project_structure -> mod_id -> bool
 
 val module_name : project_structure -> mod_id -> string spanned
 
+val valid_module_id : project_structure -> mod_id -> bool
+
 val module_order : project_structure -> mod_id list
 
 val module_files : project_structure -> mod_id -> string spanned list
 
 val module_requires : project_structure -> mod_id -> mod_id list
 
-val file_list : mod_id list -> project_structure -> string spanned list
+val all_files : project_structure -> string spanned list
diff --git a/src/lib/reporting.ml b/src/lib/reporting.ml
index 0537fc27a..22dbb3673 100644
--- a/src/lib/reporting.ml
+++ b/src/lib/reporting.ml
@@ -140,6 +140,15 @@ let rec simp_loc = function
   | Parse_ast.Hint (_, l1, l2) -> begin match simp_loc l1 with None -> simp_loc l2 | pos -> pos end
   | Parse_ast.Range (p1, p2) -> Some (p1, p2)
 
+let rec map_loc_range f = function
+  | Parse_ast.Unknown -> Parse_ast.Unknown
+  | Parse_ast.Unique (n, l) -> Parse_ast.Unique (n, map_loc_range f l)
+  | Parse_ast.Generated l -> Parse_ast.Generated (map_loc_range f l)
+  | Parse_ast.Hint (hint, l1, l2) -> Parse_ast.Hint (hint, l1, map_loc_range f l2)
+  | Parse_ast.Range (p1, p2) ->
+      let p1, p2 = f p1 p2 in
+      Parse_ast.Range (p1, p2)
+
 let rec loc_file = function
   | Parse_ast.Unknown -> None
   | Parse_ast.Unique (_, l) -> loc_file l
diff --git a/src/lib/reporting.mli b/src/lib/reporting.mli
index f020dec49..bf68d2990 100644
--- a/src/lib/reporting.mli
+++ b/src/lib/reporting.mli
@@ -94,6 +94,11 @@ val loc_file : Parse_ast.l -> string option
 (** Reduce a location to a pair of positions if possible *)
 val simp_loc : Ast.l -> (Lexing.position * Lexing.position) option
 
+(** Adjust the range of a location. Note that only the primary
+    location is adjusted. Hint locations are unaffected. *)
+val map_loc_range :
+  (Lexing.position -> Lexing.position -> Lexing.position * Lexing.position) -> Parse_ast.l -> Parse_ast.l
+
 (** [short_loc_to_string] prints the location as a single line in a simple format *)
 val short_loc_to_string : Parse_ast.l -> string
 
diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml
index 77f84bd78..6d0bc5a42 100644
--- a/src/lib/type_check.ml
+++ b/src/lib/type_check.ml
@@ -215,7 +215,7 @@ let expand_bind_synonyms l env (typq, typ) = (typq, Env.expand_synonyms (Env.add
 
 let wf_binding l env (typq, typ) =
   let env = Env.add_typquant l typq env in
-  Env.wf_typ env typ
+  Env.wf_typ ~at:l env typ
 
 let wf_typschm env (TypSchm_aux (TypSchm_ts (typq, typ), l)) = wf_binding l env (typq, typ)
 
@@ -1656,7 +1656,7 @@ let crule r env exp typ =
   typ_print (lazy (Util.("Check " |> cyan |> clear) ^ string_of_exp exp ^ " <= " ^ string_of_typ typ));
   try
     let checked_exp = r env exp typ in
-    Env.wf_typ env (typ_of checked_exp);
+    Env.wf_typ ~at:(exp_loc exp) env (typ_of checked_exp);
     decr depth;
     checked_exp
   with Type_error (l, err) ->
@@ -1669,7 +1669,7 @@ let irule r env exp =
     let inferred_exp = r env exp in
     typ_print
       (lazy (Util.("Infer " |> blue |> clear) ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp)));
-    Env.wf_typ env (typ_of inferred_exp);
+    Env.wf_typ ~at:(exp_loc exp) env (typ_of inferred_exp);
     decr depth;
     inferred_exp
   with Type_error (l, err) ->
@@ -1899,7 +1899,7 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
   | E_let (LB_aux (letbind, (let_loc, _)), exp), _ -> begin
       match letbind with
       | LB_val ((P_aux (P_typ (ptyp, _), _) as pat), bind) ->
-          Env.wf_typ env ptyp;
+          Env.wf_typ ~at:l env ptyp;
           let checked_bind = crule check_exp env bind ptyp in
           ignore (check_pattern_duplicates env pat);
           let env = bind_pattern_vector_subranges pat env in
@@ -1925,11 +1925,11 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
       if prove __POS__ env nc then typ_error l ("Can prove " ^ string_of_n_constraint nc)
       else annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
   | E_app (f, [E_aux (E_typ (typ, exp), _)]), _ when string_of_id f = "_check" ->
-      Env.wf_typ env typ;
+      Env.wf_typ ~at:l env typ;
       let _ = crule check_exp env exp typ in
       annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
   | E_app (f, [E_aux (E_typ (typ, exp), _)]), _ when string_of_id f = "_not_check" ->
-      Env.wf_typ env typ;
+      Env.wf_typ ~at:l env typ;
       if
         try
           ignore (crule check_exp env exp typ);
@@ -2061,7 +2061,7 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
       let bind_exp, ptyp =
         match pat with
         | P_aux (P_typ (ptyp, _), _) ->
-            Env.wf_typ env ptyp;
+            Env.wf_typ ~at:l env ptyp;
             let checked_bind = crule check_exp env bind ptyp in
             (checked_bind, ptyp)
         | _ ->
@@ -2545,7 +2545,7 @@ and infer_pat env (P_aux (pat_aux, (l, uannot)) as pat) =
       | _ -> typ_error l ("Malformed mapping type " ^ string_of_id f)
     end
   | P_typ (typ_annot, pat) ->
-      Env.wf_typ env typ_annot;
+      Env.wf_typ ~at:l env typ_annot;
       let typed_pat, env, guards = bind_pat env pat typ_annot in
       (annot_pat (P_typ (typ_annot, typed_pat)) typ_annot, env, guards)
   | P_lit (L_aux (L_string _, _) as lit) ->
@@ -3305,7 +3305,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) =
       let bind_exp, ptyp =
         match pat with
         | P_aux (P_typ (ptyp, _), _) ->
-            Env.wf_typ env ptyp;
+            Env.wf_typ ~at:l env ptyp;
             let checked_bind = crule check_exp env bind ptyp in
             (checked_bind, ptyp)
         | _ ->
@@ -3331,7 +3331,7 @@ and infer_exp env (E_aux (exp_aux, (l, uannot)) as exp) =
       let bind_exp, pat, ptyp =
         match letbind with
         | LB_val ((P_aux (P_typ (ptyp, _), _) as pat), bind) ->
-            Env.wf_typ env ptyp;
+            Env.wf_typ ~at:l env ptyp;
             let checked_bind = crule check_exp env bind ptyp in
             (checked_bind, pat, ptyp)
         | LB_val (pat, bind) ->
@@ -3833,7 +3833,7 @@ and infer_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, uannot)) as mp
   | MP_lit (L_aux (L_string _, _) as lit) -> (annot_mpat (MP_lit lit) string_typ, env, [])
   | MP_lit lit -> (annot_mpat (MP_lit lit) (infer_lit env lit), env, [])
   | MP_typ (mpat, typ_annot) ->
-      Env.wf_typ env typ_annot;
+      Env.wf_typ ~at:l env typ_annot;
       let typed_mpat, env, guards = bind_mpat allow_unknown other_env env mpat typ_annot in
       (annot_mpat (MP_typ (typed_mpat, typ_annot)) typ_annot, env, guards)
   | MP_vector (mpat :: mpats) ->
@@ -3890,7 +3890,7 @@ let check_letdef orig_env def_annot (LB_aux (letbind, (l, _))) =
   match letbind with
   | LB_val ((P_aux (P_typ (typ_annot, _), _) as pat), bind) ->
       check_duplicate_letbinding l pat orig_env;
-      Env.wf_typ orig_env typ_annot;
+      Env.wf_typ ~at:l orig_env typ_annot;
       let checked_bind = crule check_exp orig_env bind typ_annot in
       let tpat, env = bind_pat_no_guard orig_env pat typ_annot in
       ( [DEF_aux (DEF_let (LB_aux (LB_val (tpat, checked_bind), (l, empty_tannot))), def_annot)],
@@ -4073,11 +4073,13 @@ let check_fundef env def_annot (FD_aux (FD_function (recopt, tannotopt, funcls),
   typ_print (lazy ("\n" ^ Util.("Check function " |> cyan |> clear) ^ string_of_id id));
   let have_val_spec, (quant, typ), env =
     try (true, Env.get_val_spec id env, env) with
-    | Type_error (l, Err_not_in_scope (_, scope_l)) ->
+    | Type_error (l, Err_not_in_scope (_, scope_l, item_scope, into_scope)) ->
         typ_raise l
           (Err_not_in_scope
              ( Some "Cannot infer type of function as it has a defined type already. However, this type is not in scope.",
-               scope_l
+               scope_l,
+               item_scope,
+               into_scope
              )
           )
     | Type_error (l, _) ->
@@ -4204,12 +4206,16 @@ let forbid_recursive_types type_l f =
     let msg = "Types are not well-formed within this type definition. Note that recursive types are forbidden." in
     raise (Type_error (type_l, err_because (Err_other msg, l, err)))
 
+let extension_def_attribute env def_annot =
+  match get_def_attribute "extension" def_annot with Some (l, name) -> Env.get_module_id_opt env name | None -> None
+
 let check_type_union u_l non_rec_env env variant typq (Tu_aux (Tu_ty_id (arg_typ, v), def_annot)) =
   let ret_typ = app_typ variant (List.fold_left fold_union_quant [] (quant_items typq)) in
   let typ = mk_typ (Typ_fn ([arg_typ], ret_typ)) in
   forbid_recursive_types u_l (fun () -> wf_binding def_annot.loc non_rec_env (typq, arg_typ));
   wf_binding def_annot.loc env (typq, typ);
-  env |> Env.add_union_id v (typq, typ) |> Env.add_val_spec v (typq, typ)
+  let in_module = extension_def_attribute env def_annot in
+  env |> Env.add_union_id ?in_module v (typq, typ) |> Env.add_val_spec ?in_module v (typq, typ)
 
 let check_record l env def_annot id typq fields =
   forbid_recursive_types l (fun () ->
@@ -4421,7 +4427,7 @@ and check_outcome_instantiation :
                 in
                 typ_raise decl_l (err_because (Err_other msg, prev_l, Err_other "Previously instantiated here"))
             | None ->
-                Env.wf_typ env subst_typ;
+                Env.wf_typ ~at:decl_l env subst_typ;
                 ( typ_subst kid (mk_typ_arg (A_typ subst_typ)) typ,
                   (kid, subst_typ) :: new_instantiated,
                   fns,
@@ -4515,27 +4521,17 @@ and check_def : Env.t -> uannot def -> tannot def list * Env.t =
         ],
         env
       )
-  | DEF_pragma ("unscope#", arg, l) when !Initial_check.opt_magic_hash ->
-      let env =
-        match String.split_on_char ' ' arg with
-        | [id_category; id] -> Type_env.unscope_pragma id_category (mk_id id) env
-        | _ -> env
-      in
-      ([DEF_aux (DEF_pragma ("unscope#", arg, l), def_annot)], env)
-  | DEF_pragma ("module_start#", arg, l) ->
-      let sep = String.index_from arg 0 ' ' in
-      let m = int_of_string (String.sub arg 0 sep) in
-      typ_print
-        ( lazy
-          (let name = String.sub arg (sep + 1) (String.length arg - (sep + 1)) in
-           Printf.sprintf "module start %s %d" name m
-          )
-          );
-      ([], Env.start_module m env)
-  | DEF_pragma ("require#", arg, l) ->
-      let ms = List.map int_of_string (String.split_on_char ' ' arg) in
-      ([], Env.open_modules ms env)
-  | DEF_pragma ("module_end#", arg, l) -> ([], Env.end_module env)
+  | DEF_pragma ("rigging#", arg, l) ->
+      let start_p = match Reporting.simp_loc l with Some (p, _) -> Some p | None -> None in
+      let proj_defs = Initial_check.parse_project ?inline:start_p ~contents:arg () in
+      let proj = Project.initialize_project_structure proj_defs in
+      typ_print (lazy "set modules");
+      ([], Env.set_modules proj env)
+  | DEF_pragma ("start_module#", arg, l) ->
+      let mod_id = Env.get_module_id ~at:l env arg in
+      typ_print (lazy (Printf.sprintf "module start %d '%s'" mod_id arg));
+      ([], Env.start_module ~at:l mod_id env)
+  | DEF_pragma ("end_module#", _, _) -> ([], Env.end_module env)
   | DEF_pragma (pragma, arg, l) -> ([DEF_aux (DEF_pragma (pragma, arg, l), def_annot)], env)
   | DEF_scattered sdef -> check_scattered env def_annot sdef
   | DEF_measure (id, pat, exp) -> ([check_termination_measure_decl env def_annot (id, pat, exp)], env)
@@ -4597,3 +4593,5 @@ let initial_env =
      but which don't affect flow-typing. *)
   |> Env.add_val_spec (mk_id "sail_assume")
        (TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), function_typ [bool_typ] unit_typ)
+
+let initial_env_with_modules proj = Env.set_modules proj initial_env
diff --git a/src/lib/type_check.mli b/src/lib/type_check.mli
index bd6eee8c4..bc82dd303 100644
--- a/src/lib/type_check.mli
+++ b/src/lib/type_check.mli
@@ -118,7 +118,7 @@ module Env : sig
       Useful when processing the body of the function. *)
   val get_val_spec_orig : id -> t -> typquant * typ
 
-  val update_val_spec : id -> typquant * typ -> t -> t
+  val update_val_spec : ?in_module:Project.mod_id -> id -> typquant * typ -> t -> t
 
   val get_register : id -> t -> typ
   val get_registers : t -> typ Bindings.t
@@ -507,4 +507,7 @@ val check_with_envs : Env.t -> uannot def list -> (tannot def list * Env.t) list
 (** The initial type checking environment *)
 val initial_env : Env.t
 
+(** The initial type checking environment, with a specific set of available modules. *)
+val initial_env_with_modules : Project.project_structure -> Env.t
+
 val prove_smt : assumptions:n_constraint list -> n_constraint -> bool
diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml
index d896af1ad..01cfbb774 100644
--- a/src/lib/type_env.ml
+++ b/src/lib/type_env.ml
@@ -79,6 +79,8 @@ let opt_smt_linearize = ref false
 
 let opt_string_literal_type = ref false
 
+module StringMap = Map.Make (String)
+
 module IdPair = struct
   type t = id * id
   let compare (a, b) (c, d) =
@@ -98,6 +100,7 @@ let item_loc item = item.loc
 
 type global_env = {
   default_order : order option;
+  modules : Project.project_structure option;
   val_specs : (typquant * typ) env_item Bindings.t;
   defined_val_specs : IdSet.t;
   externs : extern Bindings.t;
@@ -120,6 +123,7 @@ type global_env = {
 let empty_global_env =
   {
     default_order = None;
+    modules = None;
     val_specs = Bindings.empty;
     defined_val_specs = IdSet.empty;
     externs = Bindings.empty;
@@ -157,9 +161,14 @@ type env = {
   outcome_typschm : (typquant * typ) option;
 }
 
+let update_global f env = { env with global = f env.global }
+
 let mk_item ~loc:l env item = { item; loc = l; mod_id = env.current_module }
 let mk_item_in ~loc:l scope item = { item; loc = l; mod_id = scope }
 
+let mk_item_in2 ~loc scope_opt env item =
+  match scope_opt with Some scope -> mk_item_in ~loc scope item | None -> mk_item ~loc env item
+
 let item_in_scope env item = item.mod_id = env.current_module || IntSet.mem item.mod_id env.opened || env.open_all
 
 let filter_items_with f env bindings =
@@ -167,8 +176,22 @@ let filter_items_with f env bindings =
 
 let filter_items env bindings = filter_items_with (fun x -> x) env bindings
 
+let err_not_in_scope env msg l item =
+  match env.global.modules with
+  | None -> Err_not_in_scope (msg, l, None, None)
+  | Some proj ->
+      let module_name_opt mod_id =
+        if Project.valid_module_id proj mod_id then Some (Project.module_name proj mod_id) else None
+      in
+      Err_not_in_scope (msg, l, module_name_opt item.mod_id, module_name_opt env.current_module)
+
 let get_item_with_loc get_loc l env item =
-  if item_in_scope env item then item.item else typ_raise l (Err_not_in_scope (None, get_loc item.loc))
+  if item_in_scope env item then item.item
+  else (
+    match env.global.modules with
+    | None -> typ_raise l (err_not_in_scope env None (get_loc item.loc) item)
+    | Some proj -> typ_raise l (err_not_in_scope env None (get_loc item.loc) item)
+  )
 
 let get_item env item = get_item_with_loc (fun l -> Some l) env item
 
@@ -180,35 +203,25 @@ type t = env
 
 let global_scope = -1
 
-let start_module id env = { env with current_module = id; opened = IntSet.singleton global_scope }
+let set_modules proj env = update_global (fun global -> { global with modules = Some proj }) env
 
-let end_module env = { env with current_module = global_scope; opened = IntSet.empty }
+let get_module_id_opt env name = Option.bind env.global.modules (fun proj -> Project.get_module_id proj name)
 
-let open_modules ids env = { env with opened = IntSet.of_list (global_scope :: ids) }
+let get_module_id ~at:l env name =
+  match get_module_id_opt env name with Some mod_id -> mod_id | None -> typ_error l ("Failed to find module " ^ name)
 
-let open_all_modules env = { env with open_all = true }
+let start_module ~at:l mod_id env =
+  match env.global.modules with
+  | None -> Reporting.unreachable l __POS__ "start_module called in environment with no modules"
+  | Some proj ->
+      if not (Project.valid_module_id proj mod_id) then
+        Reporting.unreachable l __POS__ "start_module got an invalid module id";
+      let requires = Project.module_requires proj mod_id in
+      { env with current_module = mod_id; opened = IntSet.of_list (global_scope :: requires) }
 
-let update_global f env = { env with global = f env.global }
+let end_module env = { env with current_module = global_scope; opened = IntSet.empty }
 
-let unscope_pragma id_category id env =
-  typ_debug (lazy ("Unscope " ^ id_category ^ " " ^ string_of_id id));
-  let update_id id m =
-    Bindings.update id (function Some item -> Some { item with mod_id = Int.max_int } | None -> None) m
-  in
-  match id_category with
-  | "bitfield" -> update_global (fun global -> { global with bitfields = update_id id global.bitfields }) env
-  | "enum" -> update_global (fun global -> { global with enums = update_id id global.enums }) env
-  | "let" -> update_global (fun global -> { global with letbinds = update_id id global.letbinds }) env
-  | "mapping" -> update_global (fun global -> { global with mappings = update_id id global.mappings }) env
-  | "overload" -> update_global (fun global -> { global with overloads = update_id id global.overloads }) env
-  | "register" -> update_global (fun global -> { global with registers = update_id id global.registers }) env
-  | "struct" -> update_global (fun global -> { global with records = update_id id global.records }) env
-  | "type" -> update_global (fun global -> { global with synonyms = update_id id global.synonyms }) env
-  | "union" -> update_global (fun global -> { global with unions = update_id id global.unions }) env
-  | "val" -> update_global (fun global -> { global with val_specs = update_id id global.val_specs }) env
-  | _ ->
-      typ_debug (lazy "Unrecognized unscope category");
-      env
+let open_all_modules env = { env with open_all = true }
 
 let empty =
   {
@@ -831,7 +844,7 @@ let add_typquant l quant env =
   | TypQ_aux (TypQ_no_forall, _) -> env
   | TypQ_aux (TypQ_tq quants, _) -> List.fold_left add_quant_item env quants
 
-let wf_typ env (Typ_aux (_, l) as typ) =
+let wf_typ ~at:at_l env (Typ_aux (_, l) as typ) =
   let typ = expand_synonyms env typ in
   wf_debug "typ" string_of_typ typ KidSet.empty;
   incr depth;
@@ -840,7 +853,8 @@ let wf_typ env (Typ_aux (_, l) as typ) =
     decr depth
   with Type_error (err_l, err) ->
     decr depth;
-    typ_raise l (err_because (Err_other "Well-formedness check failed for type", err_l, err))
+    let extra, l = match l with Parse_ast.Unknown -> (" here", at_l) | _ -> ("", l) in
+    typ_raise l (err_because (Err_other ("Well-formedness check failed for type" ^ extra), err_l, err))
 
 let add_typ_synonym id typq arg env =
   if bound_typ_id env id then
@@ -894,12 +908,14 @@ let get_val_spec id env =
 
 let get_val_specs env = filter_items env env.global.val_specs
 
-let add_union_id id bind env =
+let add_union_id ?in_module id bind env =
   if bound_ctor_fn env id then already_bound_ctor_fn "union constructor" id env
   else (
     typ_print (lazy (adding ^ "union identifier " ^ string_of_id id ^ " : " ^ string_of_bind bind));
     update_global
-      (fun global -> { global with union_ids = Bindings.add id (mk_item env ~loc:(id_loc id) bind) global.union_ids })
+      (fun global ->
+        { global with union_ids = Bindings.add id (mk_item_in2 in_module env ~loc:(id_loc id) bind) global.union_ids }
+      )
       env
   )
 
@@ -917,7 +933,7 @@ let rec valid_implicits env start = function
   | _ :: rest -> valid_implicits env false rest
   | [] -> ()
 
-let rec update_val_spec id (typq, typ) env =
+let rec update_val_spec ?in_module id (typq, typ) env =
   let typq_env = add_typquant (id_loc id) typq env in
   begin
     match expand_synonyms typq_env typ with
@@ -942,7 +958,10 @@ let rec update_val_spec id (typq, typ) env =
         typ_print (lazy (adding ^ "val " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
         update_global
           (fun global ->
-            { global with val_specs = Bindings.add id (mk_item env ~loc:(id_loc id) (typq, typ)) global.val_specs }
+            {
+              global with
+              val_specs = Bindings.add id (mk_item_in2 in_module env ~loc:(id_loc id) (typq, typ)) global.val_specs;
+            }
           )
           env
     | Typ_aux (Typ_bidir (typ1, typ2), _) ->
@@ -956,8 +975,9 @@ let rec update_val_spec id (typq, typ) env =
     | _ -> typ_error (id_loc id) "val definition must have a mapping or function type"
   end
 
-and add_val_spec ?(ignore_duplicate = false) id (bind_typq, bind_typ) env =
-  if (not (Bindings.mem id env.global.val_specs)) || ignore_duplicate then update_val_spec id (bind_typq, bind_typ) env
+and add_val_spec ?in_module ?(ignore_duplicate = false) id (bind_typq, bind_typ) env =
+  if (not (Bindings.mem id env.global.val_specs)) || ignore_duplicate then
+    update_val_spec ?in_module id (bind_typq, bind_typ) env
   else if ignore_duplicate then env
   else (
     let previous_loc =
@@ -1189,7 +1209,7 @@ let string_of_mtyp (mut, typ) =
 
 let add_local id mtyp env =
   if not env.allow_bindings then typ_error (id_loc id) "Bindings are not allowed in this context";
-  wf_typ env (snd mtyp);
+  wf_typ ~at:(id_loc id) env (snd mtyp);
   if Bindings.mem id env.global.val_specs then
     typ_error (id_loc id) ("Local variable " ^ string_of_id id ^ " is already bound as a function name")
   else ();
@@ -1295,7 +1315,7 @@ let get_extern id env backend =
   with Not_found -> typ_error (id_loc id) ("No extern binding found for " ^ string_of_id id)
 
 let add_register id typ env =
-  wf_typ env typ;
+  wf_typ ~at:(id_loc id) env typ;
   if Bindings.mem id env.global.registers then
     typ_error (id_loc id) ("Register " ^ string_of_id id ^ " is already bound")
   else (
@@ -1330,10 +1350,9 @@ let lookup_id id env =
                   else (
                     let enum_name = string_of_id enum_id in
                     typ_raise (id_loc id)
-                      (Err_not_in_scope
-                         ( Some ("Enumeration " ^ enum_name ^ " containing " ^ string_of_id id ^ " is not in scope"),
-                           Some item.loc
-                         )
+                      (err_not_in_scope env
+                         (Some ("Enumeration " ^ enum_name ^ " containing " ^ string_of_id id ^ " is not in scope"))
+                         (Some item.loc) item
                       )
                   )
               | None -> Unbound id
diff --git a/src/lib/type_env.mli b/src/lib/type_env.mli
index c38b93481..c2377aa4c 100644
--- a/src/lib/type_env.mli
+++ b/src/lib/type_env.mli
@@ -81,27 +81,34 @@ type env
 
 type t = env
 
-val start_module : Project.mod_id -> t -> t
+(** Set the modules in the environment. Note that calling this twice
+    on an environment with different arguments will invalidate all
+    module identifiers! *)
+val set_modules : Project.project_structure -> t -> t
+
+val get_module_id_opt : t -> string -> Project.mod_id option
+val get_module_id : at:l -> t -> string -> Project.mod_id
+
+(** Start typechecking within a module context. The module id must be
+    a valid module created via the set_modules call, otherwise we will
+    fail with an internal error. *)
+val start_module : at:l -> Project.mod_id -> t -> t
+
+(** End the current module context, returning us to type-checking in
+    the global scope. *)
 val end_module : t -> t
-val open_modules : Project.mod_id list -> t -> t
 
 (** This effectively disables all module related access control *)
 val open_all_modules : t -> t
 
-(** This implements the unscope# pragma, which removes an identifier
-    from scope by setting its module id to -1 (which is never a valid
-    module id). This is used only to test the typechecker, and should
-    not be used for any other reason! *)
-val unscope_pragma : string -> id -> t -> t
-
 val freshen_bind : t -> typquant * typ -> typquant * typ
 
 val get_default_order : t -> order
 val get_default_order_opt : t -> order option
 val set_default_order : order -> t -> t
 
-val add_val_spec : ?ignore_duplicate:bool -> id -> typquant * typ -> t -> t
-val update_val_spec : id -> typquant * typ -> t -> t
+val add_val_spec : ?in_module:Project.mod_id -> ?ignore_duplicate:bool -> id -> typquant * typ -> t -> t
+val update_val_spec : ?in_module:Project.mod_id -> id -> typquant * typ -> t -> t
 val define_val_spec : id -> t -> t
 val get_defined_val_specs : t -> IdSet.t
 val get_val_spec : id -> t -> typquant * typ
@@ -126,7 +133,7 @@ val set_scattered_variant_env : variant_env:t -> id -> t -> t
 val union_constructor_info : id -> t -> (int * int * id * type_union) option
 val is_union_constructor : id -> t -> bool
 val is_singleton_union_constructor : id -> t -> bool
-val add_union_id : id -> typquant * typ -> t -> t
+val add_union_id : ?in_module:Project.mod_id -> id -> typquant * typ -> t -> t
 val get_union_id : id -> t -> typquant * typ
 
 val is_mapping : id -> t -> bool
@@ -217,7 +224,7 @@ val no_bindings : t -> t
 val is_toplevel : t -> l option
 
 (* Well formedness-checks *)
-val wf_typ : t -> typ -> unit
+val wf_typ : at:l -> t -> typ -> unit
 val wf_constraint : ?exs:KidSet.t -> t -> n_constraint -> unit
 
 (** Some of the code in the environment needs to use the smt solver,
diff --git a/src/lib/type_error.ml b/src/lib/type_error.ml
index 6361f4b9f..cfcb06355 100644
--- a/src/lib/type_error.ml
+++ b/src/lib/type_error.ml
@@ -352,14 +352,40 @@ let message_of_type_error =
           ([coercion; Line "Coercion failed because:"; msg trigger]
           @ if not (reasons = []) then Line "Possible reasons:" :: List.map msg reasons else []
           )
-    | Err_not_in_scope (explanation, Some l) ->
+    | Err_not_in_scope (explanation, Some l, item_scope, into_scope) ->
+        let suggest, in_mod, add_requires_here =
+          match (item_scope, into_scope) with
+          | None, None -> ("Try bringing the following into scope:", "", [])
+          | Some (item, _), None ->
+              (Printf.sprintf "Try requiring module %s to bring the following into scope:" item, " in " ^ item, [])
+          | None, Some (into, into_l) ->
+              ( Printf.sprintf "Try bringing the following into scope for module %s:" into,
+                "",
+                [Location ("", Some "add requires here", Project.to_loc into_l, Seq [])]
+              )
+          | Some (item, _), Some (into, into_l) ->
+              ( Printf.sprintf "Try requiring module %s to bring the following into scope for module %s:" item into,
+                " in " ^ item,
+                [
+                  Location
+                    ( "",
+                      Some (Printf.sprintf "add 'requires %s' within %s here" item into),
+                      Project.to_loc into_l,
+                      Seq []
+                    );
+                ]
+              )
+        in
         Seq
-          [
-            Line (Option.value ~default:"Not in scope" explanation);
-            Line "Try bringing the following definition into scope:";
-            Location ("", Some "definition here", l, Seq []);
-          ]
-    | Err_not_in_scope (explanation, None) -> Line (Option.value ~default:"Not in scope" explanation)
+          ([
+             Line (Option.value ~default:"Not in scope" explanation);
+             Line "";
+             Line suggest;
+             Location ("", Some ("definition here" ^ in_mod), l, Seq []);
+           ]
+          @ add_requires_here
+          )
+    | Err_not_in_scope (explanation, None, _, _) -> Line (Option.value ~default:"Not in scope" explanation)
   in
   msg
 
diff --git a/src/lib/type_error.mli b/src/lib/type_error.mli
index 7795a7481..c35112adc 100644
--- a/src/lib/type_error.mli
+++ b/src/lib/type_error.mli
@@ -94,7 +94,8 @@ type type_error =
   | Err_no_num_ident of id
   | Err_other of string
   | Err_inner of type_error * Parse_ast.l * string * string option * type_error
-  | Err_not_in_scope of string option * Parse_ast.l option
+  | Err_not_in_scope of
+      string option * Parse_ast.l option * string Project.spanned option * string Project.spanned option
 
 exception Type_error of Parse_ast.l * type_error
 
diff --git a/src/lib/type_internal.ml b/src/lib/type_internal.ml
index 70546a1a8..9cd7ebd65 100644
--- a/src/lib/type_internal.ml
+++ b/src/lib/type_internal.ml
@@ -109,7 +109,8 @@ type type_error =
   | Err_no_num_ident of id
   | Err_other of string
   | Err_inner of type_error * Parse_ast.l * string * string option * type_error
-  | Err_not_in_scope of string option * Parse_ast.l option
+  | Err_not_in_scope of
+      string option * Parse_ast.l option * string Project.spanned option * string Project.spanned option
 
 let err_because (error1, l, error2) = Err_inner (error1, l, "Caused by", None, error2)
 
diff --git a/test/lexing/bad_option_pragma.expect b/test/lexing/bad_option_pragma.expect
index 494f051e4..f571da463 100644
--- a/test/lexing/bad_option_pragma.expect
+++ b/test/lexing/bad_option_pragma.expect
@@ -1,3 +1,5 @@
 Error:
-bad_option_pragma.sail:2.17-3.0:
+bad_option_pragma.sail:2.0-17:
+2 |$option file.sail
+  |^---------------^
   | Anonymous argument 'file.sail' cannot be passed via $option directive
diff --git a/test/lexing/bad_option_pragma2.expect b/test/lexing/bad_option_pragma2.expect
index 59508d615..0a3fc7887 100644
--- a/test/lexing/bad_option_pragma2.expect
+++ b/test/lexing/bad_option_pragma2.expect
@@ -1,4 +1,6 @@
 Error:
-bad_option_pragma2.sail:2.24-3.0:
+bad_option_pragma2.sail:2.0-24:
+2 |$option -not_a_sail_flag
+  |^----------------------^
   | Invalid flag passed to $option directive
   | sail: unknown option '-not_a_sail_flag'.
diff --git a/test/lexing/help_option_pragma.expect b/test/lexing/help_option_pragma.expect
index f5e478b4a..65d86dd22 100644
--- a/test/lexing/help_option_pragma.expect
+++ b/test/lexing/help_option_pragma.expect
@@ -1,3 +1,5 @@
 Error:
-help_option_pragma.sail:2.13-3.0:
+help_option_pragma.sail:2.0-13:
+2 |$option -help
+  |^-----------^
   | -help flag passed to $option directive
diff --git a/test/lexing/unterminated_ifdef.expect b/test/lexing/unterminated_ifdef.expect
index 8ce6a9945..883d550bb 100644
--- a/test/lexing/unterminated_ifdef.expect
+++ b/test/lexing/unterminated_ifdef.expect
@@ -1,3 +1,5 @@
 Error:
-unterminated_ifdef.sail:2.6-3.0:
+unterminated_ifdef.sail:2.0-6:
+2 |$ifdef
+  |^----^
   | $ifdef, $ifndef, or $iftarget never ended by $endif
diff --git a/test/typecheck/fail/overload_member_scope.expect b/test/typecheck/fail/overload_member_scope.expect
new file mode 100644
index 000000000..5300f5b68
--- /dev/null
+++ b/test/typecheck/fail/overload_member_scope.expect
@@ -0,0 +1,8 @@
+Type error:
+fail/overload_member_scope.sail:21.0-20:
+21 |overload bar = {foo}
+   |^------------------^ Overload defined here
+fail/overload_member_scope.sail:29.17-22:
+29 |function baz() = bar()
+   |                 ^---^
+   | Overload bar is defined, but nothing it overloads is in scope
diff --git a/test/typecheck/fail/overload_member_scope.sail b/test/typecheck/fail/overload_member_scope.sail
new file mode 100644
index 000000000..a617bcfb1
--- /dev/null
+++ b/test/typecheck/fail/overload_member_scope.sail
@@ -0,0 +1,31 @@
+$option -dmagic_hash
+
+// This test demonstrates that even though bar overloads foo, we
+// cannot use bar to access foo in a module where it is not available
+
+// While it might make some sense to permit this (essentially using an
+// overload to re-export a function), it would break the property we want
+// that allows us to cleanly remove optional modules if they overload
+// identifiers.
+
+$rigging# A { } B { requires A } C { requires B }
+
+$start_module# A
+
+val foo : unit -> unit
+
+$end_module# A
+
+$start_module# B
+
+overload bar = {foo}
+
+$end_module# B
+
+$start_module# C
+
+val baz : unit -> unit
+
+function baz() = bar()
+
+$end_module# C
diff --git a/test/typecheck/fail/unbound_tyvar.expect b/test/typecheck/fail/unbound_tyvar.expect
index 69442a3ce..6bd49bae1 100644
--- a/test/typecheck/fail/unbound_tyvar.expect
+++ b/test/typecheck/fail/unbound_tyvar.expect
@@ -1,7 +1,10 @@
 Type error:
-Well-formedness check failed for type
-
-Caused by fail/unbound_tyvar.sail:5.23-44:
+fail/unbound_tyvar.sail:5.9-12:
 5 |function foo() -> bits(definitelydoesntexist) = {
-  |                       ^-------------------^
-  | Undefined type synonym definitelydoesntexist
+  |         ^-^
+  | Well-formedness check failed for type here
+  | 
+  | Caused by fail/unbound_tyvar.sail:5.23-44:
+  | 5 |function foo() -> bits(definitelydoesntexist) = {
+  |   |                       ^-------------------^
+  |   | Undefined type synonym definitelydoesntexist
diff --git a/test/typecheck/fail/unscope_enum.expect b/test/typecheck/fail/unscope_enum.expect
index 65b61dc37..4c9df83b7 100644
--- a/test/typecheck/fail/unscope_enum.expect
+++ b/test/typecheck/fail/unscope_enum.expect
@@ -1,9 +1,10 @@
 Type error:
-fail/unscope_enum.sail:14.10-11:
-14 |  let _ = A;
+fail/unscope_enum.sail:18.10-11:
+18 |  let _ = A;
    |          ^
    | Enumeration E containing A is not in scope
-   | Try bringing the following definition into scope:
-   | fail/unscope_enum.sail:7.5-6:
-   | 7 |enum E = A | B | C
-   |   |     ^ definition here
+   | 
+   | Try requiring module A to bring the following into scope:
+   | fail/unscope_enum.sail:11.5-6:
+   | 11 |enum E = A | B | C
+   |    |     ^ definition here in A
diff --git a/test/typecheck/fail/unscope_enum.sail b/test/typecheck/fail/unscope_enum.sail
index 3962777c8..3ece26a93 100644
--- a/test/typecheck/fail/unscope_enum.sail
+++ b/test/typecheck/fail/unscope_enum.sail
@@ -1,12 +1,16 @@
 $option -dmagic_hash
 
+$rigging# A {}
+
 default Order dec
 
 $include <prelude.sail>
 
+$start_module# A
+
 enum E = A | B | C
 
-$unscope# enum E
+$end_module# A
 
 val bar : unit -> unit
 
diff --git a/test/typecheck/fail/unscope_let.expect b/test/typecheck/fail/unscope_let.expect
index f4927bf4f..5015f5592 100644
--- a/test/typecheck/fail/unscope_let.expect
+++ b/test/typecheck/fail/unscope_let.expect
@@ -1,9 +1,10 @@
 Type error:
-fail/unscope_let.sail:14.10-13:
-14 |  let _ = foo;
+fail/unscope_let.sail:18.10-13:
+18 |  let _ = foo;
    |          ^-^
    | Not in scope
-   | Try bringing the following definition into scope:
-   | fail/unscope_let.sail:7.4-7:
-   | 7 |let foo : bits(32) = 0xFFFF_FFFF
-   |   |    ^-^ definition here
+   | 
+   | Try requiring module A to bring the following into scope:
+   | fail/unscope_let.sail:11.4-7:
+   | 11 |let foo : bits(32) = 0xFFFF_FFFF
+   |    |    ^-^ definition here in A
diff --git a/test/typecheck/fail/unscope_let.sail b/test/typecheck/fail/unscope_let.sail
index 836b585f2..cc4dde625 100644
--- a/test/typecheck/fail/unscope_let.sail
+++ b/test/typecheck/fail/unscope_let.sail
@@ -1,12 +1,16 @@
 $option -dmagic_hash
 
+$rigging# A {}
+
 default Order dec
 
 $include <prelude.sail>
 
+$start_module# A
+
 let foo : bits(32) = 0xFFFF_FFFF
 
-$unscope# let foo
+$end_module# A
 
 val bar : unit -> unit
 
diff --git a/test/typecheck/fail/unscope_register.expect b/test/typecheck/fail/unscope_register.expect
index afc2745d3..78a76e5f2 100644
--- a/test/typecheck/fail/unscope_register.expect
+++ b/test/typecheck/fail/unscope_register.expect
@@ -1,9 +1,10 @@
 Type error:
-fail/unscope_register.sail:14.10-13:
-14 |  let _ = foo;
+fail/unscope_register.sail:18.10-13:
+18 |  let _ = foo;
    |          ^-^
    | Not in scope
-   | Try bringing the following definition into scope:
-   | fail/unscope_register.sail:7.9-12:
-   | 7 |register foo : bits(32)
-   |   |         ^-^ definition here
+   | 
+   | Try requiring module A to bring the following into scope:
+   | fail/unscope_register.sail:11.9-12:
+   | 11 |register foo : bits(32)
+   |    |         ^-^ definition here in A
diff --git a/test/typecheck/fail/unscope_register.sail b/test/typecheck/fail/unscope_register.sail
index a746dbf7b..02647c537 100644
--- a/test/typecheck/fail/unscope_register.sail
+++ b/test/typecheck/fail/unscope_register.sail
@@ -1,12 +1,16 @@
 $option -dmagic_hash
 
+$rigging# A {}
+
 default Order dec
 
 $include <prelude.sail>
 
+$start_module# A
+
 register foo : bits(32)
 
-$unscope# register foo
+$end_module# A
 
 val bar : unit -> unit
 
diff --git a/test/typecheck/fail/unscope_type.expect b/test/typecheck/fail/unscope_type.expect
index 03264fb8f..573a29123 100644
--- a/test/typecheck/fail/unscope_type.expect
+++ b/test/typecheck/fail/unscope_type.expect
@@ -1,9 +1,10 @@
 Type error:
-fail/unscope_type.sail:14.10-13:
-14 |  let _ : foo = 0xFFFF_FFFF;
+fail/unscope_type.sail:18.10-13:
+18 |  let _ : foo = 0xFFFF_FFFF;
    |          ^-^
    | Not in scope
-   | Try bringing the following definition into scope:
-   | fail/unscope_type.sail:7.5-8:
-   | 7 |type foo = bits(32)
-   |   |     ^-^ definition here
+   | 
+   | Try requiring module A to bring the following into scope:
+   | fail/unscope_type.sail:11.5-8:
+   | 11 |type foo = bits(32)
+   |    |     ^-^ definition here in A
diff --git a/test/typecheck/fail/unscope_type.sail b/test/typecheck/fail/unscope_type.sail
index 01b4397a1..603090458 100644
--- a/test/typecheck/fail/unscope_type.sail
+++ b/test/typecheck/fail/unscope_type.sail
@@ -1,12 +1,16 @@
 $option -dmagic_hash
 
+$rigging# A {}
+
 default Order dec
 
 $include <prelude.sail>
 
+$start_module# A
+
 type foo = bits(32)
 
-$unscope# type foo
+$end_module# A
 
 val bar : unit -> unit
 
diff --git a/test/typecheck/fail/unscope_val.expect b/test/typecheck/fail/unscope_val.expect
index 3e54d0f70..9bf0b81fc 100644
--- a/test/typecheck/fail/unscope_val.expect
+++ b/test/typecheck/fail/unscope_val.expect
@@ -1,9 +1,10 @@
 Type error:
-fail/unscope_val.sail:11.9-12:
-11 |function foo() = ()
+fail/unscope_val.sail:15.9-12:
+15 |function foo() = ()
    |         ^-^
    | Cannot infer type of function as it has a defined type already. However, this type is not in scope.
-   | Try bringing the following definition into scope:
-   | fail/unscope_val.sail:7.4-7:
-   | 7 |val foo : unit -> unit
-   |   |    ^-^ definition here
+   | 
+   | Try requiring module A to bring the following into scope:
+   | fail/unscope_val.sail:11.4-7:
+   | 11 |val foo : unit -> unit
+   |    |    ^-^ definition here in A
diff --git a/test/typecheck/fail/unscope_val.sail b/test/typecheck/fail/unscope_val.sail
index 538667a79..da9ea3d20 100644
--- a/test/typecheck/fail/unscope_val.sail
+++ b/test/typecheck/fail/unscope_val.sail
@@ -1,11 +1,15 @@
 $option -dmagic_hash
 
+$rigging# A {}
+
 default Order dec
 
 $include <prelude.sail>
 
+$start_module# A
+
 val foo : unit -> unit
 
-$unscope# val foo
+$end_module# A
 
 function foo() = ()
diff --git a/test/typecheck/pass/constraint_ctor/v4.expect b/test/typecheck/pass/constraint_ctor/v4.expect
index bf507dd0a..348a91da1 100644
--- a/test/typecheck/pass/constraint_ctor/v4.expect
+++ b/test/typecheck/pass/constraint_ctor/v4.expect
@@ -1,7 +1,10 @@
 Type error:
-Well-formedness check failed for type
-
-Caused by pass/constraint_ctor/v4.sail:17.33-36:
+pass/constraint_ctor/v4.sail:17.9-12:
 17 |function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
-   |                                 ^-^
-   | Could not prove 23 <= 22 for type constructor Bar
+   |         ^-^
+   | Well-formedness check failed for type here
+   | 
+   | Caused by pass/constraint_ctor/v4.sail:17.33-36:
+   | 17 |function bar(Bar(x as int('x)) : Bar(23)) -> unit = {
+   |    |                                 ^-^
+   |    | Could not prove 23 <= 22 for type constructor Bar
diff --git a/test/typecheck/pass/extension_constructor.sail b/test/typecheck/pass/extension_constructor.sail
new file mode 100644
index 000000000..f8776962d
--- /dev/null
+++ b/test/typecheck/pass/extension_constructor.sail
@@ -0,0 +1,38 @@
+$option -dmagic_hash
+
+$rigging# A { } B { requires A } C { requires A }
+
+// Module A
+$start_module# A
+
+union Foo = {
+  Bar : unit,
+  $[extension B] Baz : unit,
+}
+
+$end_module# A
+
+// Module B
+$start_module# B
+
+val bravo : unit -> unit
+
+function bravo() = {
+  let _ = Baz();
+}
+
+$end_module# B
+
+// Module C
+$start_module# C
+
+val charlie : Foo -> unit
+
+function charlie(x) = {
+  match x {
+    Bar() => (),
+    _ => (),
+  }
+}
+
+$end_module# C
diff --git a/test/typecheck/pass/extension_constructor/v1.expect b/test/typecheck/pass/extension_constructor/v1.expect
new file mode 100644
index 000000000..823bee999
--- /dev/null
+++ b/test/typecheck/pass/extension_constructor/v1.expect
@@ -0,0 +1,13 @@
+Type error:
+pass/extension_constructor/v1.sail:34.4-7:
+34 |    Baz() => (),
+   |    ^-^
+   | Not in scope
+   | 
+   | Try requiring module B to bring the following into scope for module C:
+   | pass/extension_constructor/v1.sail:10.17-20:
+   | 10 |  $[extension B] Baz : unit,
+   |    |                 ^-^ definition here in B
+   | pass/extension_constructor/v1.sail:3.33-34:
+   | 3 |$rigging# A { } B { requires A } C { requires A }
+   |   |                                 ^ add 'requires B' within C here
diff --git a/test/typecheck/pass/extension_constructor/v1.sail b/test/typecheck/pass/extension_constructor/v1.sail
new file mode 100644
index 000000000..14b32368c
--- /dev/null
+++ b/test/typecheck/pass/extension_constructor/v1.sail
@@ -0,0 +1,38 @@
+$option -dmagic_hash
+
+$rigging# A { } B { requires A } C { requires A }
+
+// Module A
+$start_module# A
+
+union Foo = {
+  Bar : unit,
+  $[extension B] Baz : unit,
+}
+
+$end_module# A
+
+// Module B
+$start_module# B
+
+val bravo : unit -> unit
+
+function bravo() = {
+  let _ = Baz();
+}
+
+$end_module# B
+
+// Module C
+$start_module# C
+
+val charlie : Foo -> unit
+
+function charlie(x) = {
+  match x {
+    Bar() => (),
+    Baz() => (),
+  }
+}
+
+$end_module# C
diff --git a/test/typecheck/pass/extension_constructor/v2.expect b/test/typecheck/pass/extension_constructor/v2.expect
new file mode 100644
index 000000000..b4e02a745
--- /dev/null
+++ b/test/typecheck/pass/extension_constructor/v2.expect
@@ -0,0 +1,18 @@
+Type error:
+pass/extension_constructor/v2.sail:29.14-25:
+29 |val charlie : Foo -> unit
+   |              ^---------^
+   | Well-formedness check failed for type
+   | 
+   | Caused by pass/extension_constructor/v2.sail:29.14-17:
+   | 29 |val charlie : Foo -> unit
+   |    |              ^-^
+   |    | Not in scope
+   |    | 
+   |    | Try requiring module A to bring the following into scope for module C:
+   |    | pass/extension_constructor/v2.sail:8.6-9:
+   |    | 8 |union Foo = {
+   |    |   |      ^-^ definition here in A
+   |    | pass/extension_constructor/v2.sail:3.33-34:
+   |    | 3 |$rigging# A { } B { requires A } C { }
+   |    |   |                                 ^ add 'requires A' within C here
diff --git a/test/typecheck/pass/extension_constructor/v2.sail b/test/typecheck/pass/extension_constructor/v2.sail
new file mode 100644
index 000000000..6c5ee07eb
--- /dev/null
+++ b/test/typecheck/pass/extension_constructor/v2.sail
@@ -0,0 +1,38 @@
+$option -dmagic_hash
+
+$rigging# A { } B { requires A } C { }
+
+// Module A
+$start_module# A
+
+union Foo = {
+  Bar : unit,
+  $[extension B] Baz : unit,
+}
+
+$end_module# A
+
+// Module B
+$start_module# B
+
+val bravo : unit -> unit
+
+function bravo() = {
+  let _ = Baz();
+}
+
+$end_module# B
+
+// Module C
+$start_module# C
+
+val charlie : Foo -> unit
+
+function charlie(x) = {
+  match x {
+    Bar() => (),
+    _ => (),
+  }
+}
+
+$end_module# C