fix some compiler not-matched warnings about Typ_bidir and Typ_internal_unknown

10 files changed, 134 insertions, 18 deletions

diff --git a/src/extra_pervasives.ml b/src/extra_pervasives.ml
new file mode 100644
index 00000000..a7808a95
--- /dev/null
+++ b/src/extra_pervasives.ml
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+let unreachable l pos msg =
+  raise (Reporting_basic.err_unreachable l pos msg)
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 55031ff9..2723d143 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -59,6 +59,7 @@ open Ast
 open Ast_util
 module Big_int = Nat_big_num
 open Type_check
+open Extra_pervasives
 
 let size_set_limit = 64
 
@@ -135,11 +136,13 @@ let subst_src_typ substs t =
     | Typ_var _
       -> ty
     | Typ_fn (t1,t2,e) -> re (Typ_fn (s_styp substs t1, s_styp substs t2,e))
+    | Typ_bidir (t1, t2) -> re (Typ_bidir (s_styp substs t1, s_styp substs t2))
     | Typ_tup ts -> re (Typ_tup (List.map (s_styp substs) ts))
     | Typ_app (id,tas) -> re (Typ_app (id,List.map (s_starg substs) tas))
     | Typ_exist (kids,nc,t) ->
        let substs = List.fold_left (fun sub v -> KBindings.remove v sub) substs kids in
        re (Typ_exist (kids,nc,s_styp substs t))
+    | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
   and s_starg substs (Typ_arg_aux (ta,l) as targ) =
     match ta with
     | Typ_arg_nexp ne -> Typ_arg_aux (Typ_arg_nexp (subst_nexp substs ne),l)
@@ -313,6 +316,8 @@ let rec inst_src_type insts (Typ_aux (ty,l) as typ) =
     -> insts,typ
   | Typ_fn _ ->
      raise (Reporting_basic.err_general l "Function type in constructor")
+  | Typ_bidir _ ->
+     raise (Reporting_basic.err_general l "Mapping type in constructor")
   | Typ_tup ts ->
      let insts,ts = 
        List.fold_right
@@ -325,13 +330,15 @@ let rec inst_src_type insts (Typ_aux (ty,l) as typ) =
          (fun arg (insts,args) -> let insts,arg = inst_src_typ_arg insts arg in insts,arg::args)
          args (insts,[])
      in insts, Typ_aux (Typ_app (id,ts),l)
-  | Typ_exist (kids, nc, t) ->
+  | Typ_exist (kids, nc, t) -> begin
      let kid_insts, insts' = peel (kids,insts) in
      let kids', t' = apply_kid_insts kid_insts t in
      (* TODO: subst in nc *)
      match kids' with
      | [] -> insts', t'
      | _ -> insts', Typ_aux (Typ_exist (kids', nc, t'), l)
+    end
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and inst_src_typ_arg insts (Typ_arg_aux (ta,l) as tyarg) =
   match ta with
   | Typ_arg_nexp _
@@ -341,15 +348,17 @@ and inst_src_typ_arg insts (Typ_arg_aux (ta,l) as tyarg) =
      let insts', typ' = inst_src_type insts typ in
      insts', Typ_arg_aux (Typ_arg_typ typ',l)
 
-let rec contains_exist (Typ_aux (ty,_)) =
+let rec contains_exist (Typ_aux (ty,l)) =
   match ty with
   | Typ_id _
   | Typ_var _
     -> false
   | Typ_fn (t1,t2,_) -> contains_exist t1 || contains_exist t2
+  | Typ_bidir (t1, t2) -> contains_exist t1 || contains_exist t2
   | Typ_tup ts -> List.exists contains_exist ts
   | Typ_app (_,args) -> List.exists contains_exist_arg args
   | Typ_exist _ -> true
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and contains_exist_arg (Typ_arg_aux (arg,_)) =
   match arg with
   | Typ_arg_nexp _
@@ -385,6 +394,8 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
       -> (KidSet.empty,[[],typ])
     | Typ_fn _ ->
        raise (Reporting_basic.err_general l ("Function type in constructor " ^ i))
+    | Typ_bidir _ ->
+       raise (Reporting_basic.err_general l ("Mapping type in constructor " ^ i))
     | Typ_tup ts ->
        let (vars,tys) = List.split (List.map size_nvars_ty ts) in
        let insttys = List.map (fun x -> let (insts,tys) = List.split x in
@@ -421,6 +432,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
        let tys = List.concat (List.map (fun instty -> List.map (ty_and_inst instty) insts) tys) in
        let free = List.fold_left (fun vars k -> KidSet.remove k vars) vars kids in
        (free,tys)
+    | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
   in
   (* Only single-variable prenex-form for now *)
   let size_nvars_ty (Typ_aux (ty,l) as typ) =
@@ -2164,7 +2176,8 @@ let rec sizes_of_typ (Typ_aux (t,l)) =
   | Typ_var _
     -> KidSet.empty
   | Typ_fn _ -> raise (Reporting_basic.err_general l
-                         "Function type on expressinon")
+                         "Function type on expression")
+  | Typ_bidir _ -> raise (Reporting_basic.err_general l "Mapping type on expression")
   | Typ_tup typs -> kidset_bigunion (List.map sizes_of_typ typs)
   | Typ_exist (kids,_,typ) ->
      List.fold_left (fun s k -> KidSet.remove k s) (sizes_of_typ typ) kids
@@ -2174,6 +2187,7 @@ let rec sizes_of_typ (Typ_aux (t,l)) =
      KidSet.of_list (size_nvars_nexp size)
   | Typ_app (_,tas) ->
      kidset_bigunion (List.map sizes_of_typarg tas)
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and sizes_of_typarg (Typ_arg_aux (ta,_)) =
   match ta with
     Typ_arg_nexp _
@@ -4148,6 +4162,10 @@ let replace_nexp_in_typ env typ orig new_nexp =
        let f1, arg = aux arg in
        let f2, res = aux res in
        f1 || f2, Typ_aux (Typ_fn (arg, res, eff),l)
+    | Typ_bidir (t1, t2) ->
+       let f1, t1 = aux t1 in
+       let f2, t2 = aux t2 in
+       f1 || f2, Typ_aux (Typ_bidir (t1, t2), l)
     | Typ_tup typs ->
        let fs, typs = List.split (List.map aux typs) in
        List.exists (fun x -> x) fs, Typ_aux (Typ_tup typs,l)
@@ -4157,6 +4175,7 @@ let replace_nexp_in_typ env typ orig new_nexp =
     | Typ_app (id, targs) ->
        let fs, targs = List.split (List.map aux_targ targs) in
        List.exists (fun x -> x) fs, Typ_aux (Typ_app (id, targs),l)
+    | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
   and aux_targ (Typ_arg_aux (ta,l) as typ_arg) =
     match ta with
     | Typ_arg_nexp nexp ->
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 9757ec32..6e5eb774 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -98,7 +98,7 @@ let ocaml_string_parens inside = string "\"(\" ^ " ^^ inside ^^ string " ^ \")\"
 
 let ocaml_string_comma = string " ^ \", \" ^ "
 
-let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg =
+let rec ocaml_string_typ (Typ_aux (typ_aux, l)) arg =
   match typ_aux with
   | Typ_id id when string_of_id id = "exception" -> string "Printexc.to_string" ^^ space ^^ arg
   | Typ_id id -> ocaml_string_of id ^^ space ^^ arg
@@ -118,8 +118,10 @@ let rec ocaml_string_typ (Typ_aux (typ_aux, _)) arg =
      parens (separate space [string "fun"; parens (separate (comma ^^ space) args); string "->"; body])
      ^^ space ^^ arg
   | Typ_fn (typ1, typ2, _) -> string "\"FN\""
+  | Typ_bidir (t1, t2) -> string "\"BIDIR\""
   | Typ_var kid -> string "\"VAR\""
   | Typ_exist _ -> assert false
+  | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
 
 let ocaml_typ_id ctx = function
   | id when Id.compare id (mk_id "string") = 0 -> string "string"
@@ -134,15 +136,17 @@ let ocaml_typ_id ctx = function
   | id when Id.compare id (mk_id "register") = 0 -> string "ref"
   | id -> zencode ctx id
 
-let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) =
+let rec ocaml_typ ctx (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> ocaml_typ_id ctx id
   | Typ_app (id, []) -> ocaml_typ_id ctx id
   | Typ_app (id, typs) -> parens (separate_map (string " * ") (ocaml_typ_arg ctx) typs) ^^ space ^^ ocaml_typ_id ctx id
   | Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs)
   | Typ_fn (typ1, typ2, _) -> separate space [ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2]
+  | Typ_bidir (t1, t2) -> raise (Reporting_basic.err_general l "Ocaml doesn't support bidir types")
   | Typ_var kid -> zencode_kid kid
   | Typ_exist _ -> assert false
+  | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
 and ocaml_typ_arg ctx (Typ_arg_aux (typ_arg_aux, _) as typ_arg) =
   match typ_arg_aux with
   | Typ_arg_typ typ -> ocaml_typ ctx typ
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index b449c72a..2c6c1381 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -54,6 +54,7 @@ open PPrint
 
 let pipe = string "|"
 let arrow = string "->"
+let bidir = string "<->"
 let dotdot = string ".."
 let coloncolon = string "::"
 let coloneq = string ":="
@@ -128,7 +129,9 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
   let rec typ ty = fn_typ ty
   and fn_typ ((Typ_aux (t, _)) as ty) = match t with
   | Typ_fn(arg,ret,efct) ->
-      separate space [tup_typ arg; arrow; fn_typ ret; string "effect"; doc_effects efct]
+     separate space [tup_typ arg; arrow; fn_typ ret; string "effect"; doc_effects efct]
+  | Typ_bidir (t1, t2) ->
+     separate space [tup_typ t1; bidir; tup_typ t2]
   | _ -> tup_typ ty
   and tup_typ ((Typ_aux (t, _)) as ty) = match t with
   | Typ_exist (kids, nc, ty) ->
@@ -149,10 +152,12 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
   and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
   | Typ_id id  -> doc_id id
   | Typ_var v  -> doc_var v
-  | Typ_app _ | Typ_tup _ | Typ_fn _ | Typ_exist _ ->
+  | Typ_app _ | Typ_tup _ | Typ_fn _ | Typ_bidir _ | Typ_exist _ ->
       (* exhaustiveness matters here to avoid infinite loops
        * if we add a new Typ constructor *)
-      group (parens (typ ty))
+     group (parens (typ ty))
+  | Typ_internal_unknown -> string "UNKNOWN"
+
   and doc_typ_arg (Typ_arg_aux(t,_)) = match t with
   (* Be careful here because typ_arg is implemented as nexp in the
    * parser - in practice falling through app_typ after all the proper nexp
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index b47ac21c..adfb378a 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -54,6 +54,7 @@ open Ast_util
 open Rewriter
 open PPrint
 open Pretty_print_common
+open Extra_pervasives
 
 module StringSet = Set.Make(String)
 
@@ -255,7 +256,7 @@ let rec orig_nexp (Nexp_aux (nexp, l)) =
 (* Returns the set of type variables that will appear in the Lem output,
    which may be smaller than those in the Sail type.  May need to be
    updated with doc_typ_lem *)
-let rec lem_nexps_of_typ (Typ_aux (t,_)) =
+let rec lem_nexps_of_typ (Typ_aux (t,l)) =
   let trec = lem_nexps_of_typ in
   match t with
   | Typ_id _ -> NexpSet.empty
@@ -281,6 +282,8 @@ let rec lem_nexps_of_typ (Typ_aux (t,_)) =
      List.fold_left (fun s ta -> NexpSet.union s (lem_nexps_of_typ_arg ta))
        NexpSet.empty tas
   | Typ_exist (kids,_,t) -> trec t
+  | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types"
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and lem_nexps_of_typ_arg (Typ_arg_aux (ta,_)) =
   match ta with
   | Typ_arg_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp))
@@ -312,6 +315,8 @@ let drop_duplicate_atoms kids ty =
     (* Don't recurse into type arguments, removing stuff there
        would be weird (and difficult) *)
     | Typ_app _ -> Some full_typ
+    | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types"
+    | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
   in aux_typ ty
 
 (* Follows Coq precedence levels *)
@@ -478,7 +483,9 @@ let doc_typ, doc_atomic_typ =
            match nc with
 (*           | NC_aux (NC_true,_) -> List.fold_left add_tyvar (string "Z") (List.tl kids)*)
            | _ -> List.fold_left add_tyvar (doc_arithfact ctx nc) kids
-      end
+        end
+      | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types"
+      | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
     and doc_typ_arg (Typ_arg_aux(t,_)) = match t with
       | Typ_arg_typ t -> app_typ true t
       | Typ_arg_nexp n -> doc_nexp ctx n
@@ -603,7 +610,7 @@ let doc_typquant ctx (TypQ_aux(tq,_)) typ = match tq with
    machine words.  Often these will be unnecessary, but this simple
    approach will do for now. *)
 
-let rec typeclass_nexps (Typ_aux(t,_)) =
+let rec typeclass_nexps (Typ_aux(t,l)) =
   match t with
   | Typ_id _
   | Typ_var _
@@ -620,6 +627,8 @@ let rec typeclass_nexps (Typ_aux(t,_)) =
        NexpSet.singleton (orig_nexp size_nexp)
   | Typ_app _ -> NexpSet.empty
   | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *)
+  | Typ_bidir _ -> unreachable l __POS__ "Coq doesn't support bidir types"
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 
 let doc_typschm ctx quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
   let pt = doc_typ ctx t in
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index c20fe5f4..70db46b8 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -54,6 +54,7 @@ open Ast_util
 open Rewriter
 open PPrint
 open Pretty_print_common
+open Extra_pervasives
 
 (****************************************************************************
  * PPrint-based sail-to-lem pprinter
@@ -213,7 +214,7 @@ let rec orig_nexp (Nexp_aux (nexp, l)) =
 (* Returns the set of type variables that will appear in the Lem output,
    which may be smaller than those in the Sail type.  May need to be
    updated with doc_typ_lem *)
-let rec lem_nexps_of_typ (Typ_aux (t,_)) =
+let rec lem_nexps_of_typ (Typ_aux (t,l)) =
   let trec = lem_nexps_of_typ in
   match t with
   | Typ_id _ -> NexpSet.empty
@@ -239,6 +240,8 @@ let rec lem_nexps_of_typ (Typ_aux (t,_)) =
      List.fold_left (fun s ta -> NexpSet.union s (lem_nexps_of_typ_arg ta))
        NexpSet.empty tas
   | Typ_exist (kids,_,t) -> trec t
+  | Typ_bidir _ -> raise (Reporting_basic.err_unreachable l __POS__ "Lem doesn't support bidir types")
+  | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
 and lem_nexps_of_typ_arg (Typ_arg_aux (ta,_)) =
   match ta with
   | Typ_arg_nexp nexp -> NexpSet.singleton (nexp_simp (orig_nexp nexp))
@@ -322,7 +325,9 @@ let doc_typ_lem, doc_atomic_typ_lem =
                            ("Existential type variable(s) " ^
                                String.concat ", " (List.map string_of_kid bad) ^
                                " escape into Lem"))
-      end
+        end
+      | Typ_bidir _ -> unreachable l __POS__ "Lem doesn't support bidir types"
+      | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
     and doc_typ_arg_lem (Typ_arg_aux(t,_)) = match t with
       | Typ_arg_typ t -> app_typ true t
       | Typ_arg_nexp n -> doc_nexp_lem (nexp_simp n)
@@ -433,7 +438,7 @@ let doc_typquant_lem (TypQ_aux(tq,_)) vars_included typ = match tq with
    machine words.  Often these will be unnecessary, but this simple
    approach will do for now. *)
 
-let rec typeclass_nexps (Typ_aux(t,_)) =
+let rec typeclass_nexps (Typ_aux(t,l)) =
   if !opt_mwords then
     match t with
     | Typ_id _
@@ -457,6 +462,8 @@ let rec typeclass_nexps (Typ_aux(t,_)) =
        in
        List.fold_left add_arg_nexps NexpSet.empty args
     | Typ_exist (kids,_,t) -> NexpSet.empty (* todo *)
+    | Typ_bidir _ -> unreachable l __POS__ "Lem doesn't support bidir types"
+    | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
   else NexpSet.empty
 
 let doc_typclasses_lem t =
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 06f1d768..b84bc3be 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -135,7 +135,7 @@ let doc_nc =
   in
   nc0
 
-let rec doc_typ (Typ_aux (typ_aux, _)) =
+let rec doc_typ (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
   | Typ_app (id, []) -> doc_id id
@@ -161,6 +161,7 @@ let rec doc_typ (Typ_aux (typ_aux, _)) =
      separate space [doc_typ typ1; string "->"; doc_typ typ2; string "effect"; ocaml_eff]
   | Typ_bidir (typ1, typ2) ->
      separate space [doc_typ typ1; string "<->"; doc_typ typ2]
+  | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
 and doc_typ_arg (Typ_arg_aux (ta_aux, _)) =
   match ta_aux with
   | Typ_arg_typ typ -> doc_typ typ
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index f6da074c..44440ecf 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -51,6 +51,7 @@
 open Ast
 open Util
 open Ast_util
+open Extra_pervasives
 
 module Nameset = Set.Make(String)
 
@@ -84,7 +85,7 @@ let conditional_add_exp = conditional_add false
 let nameset_bigunion = List.fold_left Nameset.union mt
 
 
-let rec free_type_names_t consider_var (Typ_aux (t, _)) = match t with
+let rec free_type_names_t consider_var (Typ_aux (t, l)) = match t with
   | Typ_var name -> if consider_var then Nameset.add (string_of_kid name) mt else mt
   | Typ_id name -> Nameset.add (string_of_id name) mt
   | Typ_fn (t1,t2,_) -> Nameset.union (free_type_names_t consider_var t1)
@@ -94,6 +95,7 @@ let rec free_type_names_t consider_var (Typ_aux (t, _)) = match t with
   | Typ_tup ts -> free_type_names_ts consider_var ts
   | Typ_app (name,targs) -> Nameset.add (string_of_id name) (free_type_names_t_args consider_var targs)
   | Typ_exist (kids,_,t') -> List.fold_left (fun s kid -> Nameset.remove (string_of_kid kid) s) (free_type_names_t consider_var t') kids
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and free_type_names_ts consider_var ts = nameset_bigunion (List.map (free_type_names_t consider_var) ts)
 and free_type_names_maybe_t consider_var = function
   | Some t -> free_type_names_t consider_var t
@@ -111,7 +113,7 @@ let rec free_type_names_tannot consider_var tannot =
   | Some (_, t, _) -> free_type_names_t consider_var t
 
 
-let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t =
+let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t =
   match t with
   | Typ_var (Kid_aux (Var v,l)) ->
     if consider_var
@@ -124,6 +126,7 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t =
   | Typ_app(id,targs) ->
      List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id)
   | Typ_exist (kids,_,t') -> fv_of_typ consider_var (List.fold_left (fun b (Kid_aux (Var v,_)) -> Nameset.add v b) bound kids) used t'
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 
 and fv_of_targ consider_var bound used (Ast.Typ_arg_aux(targ,_)) : Nameset.t = match targ with
   | Typ_arg_typ t -> fv_of_typ consider_var bound used t
diff --git a/src/specialize.ml b/src/specialize.ml
index 9723689f..81c8b0b0 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -51,6 +51,7 @@
 open Ast
 open Ast_util
 open Rewriter
+open Extra_pervasives
 
 let is_typ_ord_uvar = function
   | Type_check.U_typ _ -> true
@@ -65,6 +66,8 @@ let rec nexp_simp_typ (Typ_aux (typ_aux, l)) =
     | Typ_app (f, args) -> Typ_app (f, List.map nexp_simp_typ_arg args)
     | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, nexp_simp_typ typ)
     | Typ_fn (typ1, typ2, effect) -> Typ_fn (nexp_simp_typ typ1, nexp_simp_typ typ2, effect)
+    | Typ_bidir (t1, t2) -> Typ_bidir (nexp_simp_typ t1, nexp_simp_typ t2)
+    | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
   in
   Typ_aux (typ_aux, l)
 and nexp_simp_typ_arg (Typ_arg_aux (typ_arg_aux, l)) =
@@ -136,8 +139,11 @@ let string_of_instantiation instantiation =
     | Typ_app (id, args) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_typ_arg args ^ ")"
     | Typ_fn (typ_arg, typ_ret, eff) ->
        string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
+    | Typ_bidir (t1, t2) ->
+       string_of_typ t1 ^ " <-> " ^ string_of_typ t2
     | Typ_exist (kids, nc, typ) ->
        "exist " ^ Util.string_of_list " " kid_name kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ
+    | Typ_internal_unknown -> "UNKNOWN"
   and string_of_typ_arg = function
     | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg
   and string_of_typ_arg_aux = function
@@ -252,6 +258,8 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_frees ~exs:exs) args)
   | Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ
   | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2)
+  | Typ_bidir (t1, t2) -> KidSet.union (typ_frees ~exs:exs t1) (typ_frees ~exs:exs t2)
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
   match typ_arg_aux with
   | Typ_arg_nexp n -> KidSet.empty
@@ -266,6 +274,8 @@ let rec typ_int_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_int_frees ~exs:exs) args)
   | Typ_exist (kids, nc, typ) -> typ_int_frees ~exs:(KidSet.of_list kids) typ
   | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_int_frees ~exs:exs typ1) (typ_int_frees ~exs:exs typ2)
+  | Typ_bidir (t1, t2) -> KidSet.union (typ_int_frees ~exs:exs t1) (typ_int_frees ~exs:exs t2)
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and typ_arg_int_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
   match typ_arg_aux with
   | Typ_arg_nexp n -> KidSet.diff (tyvars_of_nexp n) exs
diff --git a/src/type_check.ml b/src/type_check.ml
index a731130a..dbbc704c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -52,6 +52,8 @@ open Ast
 open Util
 open Ast_util
 open Lazy
+open Extra_pervasives
+
 module Big_int = Nat_big_num
 
 (* opt_tc_debug controls the verbosity of the type checker. 0 is
@@ -707,6 +709,7 @@ end = struct
            | Typ_tup _ | Typ_app _ -> Typ_exist (existentials, List.fold_left nc_and (List.hd constrs) (List.tl constrs), typ)
            | Typ_exist (kids, nc, typ) -> Typ_exist (kids @ existentials, List.fold_left nc_and nc constrs, typ)
            | Typ_fn _ | Typ_bidir _ | Typ_id _ | Typ_var _ -> assert false (* These must be simple *)
+           | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
          in
          Typ_aux (typ_aux, l)
 
@@ -744,6 +747,7 @@ end = struct
        wf_constraint ~exs:(KidSet.of_list kids) env nc;
        wf_typ ~exs:(KidSet.of_list kids) { env with constraints = nc :: env.constraints } typ
     | Typ_exist (_, _, _) -> typ_error l ("Nested existentials are not allowed")
+    | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
   and wf_typ_arg ?exs:(exs=KidSet.empty) env (Typ_arg_aux (typ_arg_aux, _)) =
     match typ_arg_aux with
     | Typ_arg_nexp nexp -> wf_nexp ~exs:exs env nexp
@@ -1277,7 +1281,7 @@ let destruct_vector env typ =
   in
   destruct_vector' (Env.expand_synonyms env typ)
 
-let rec is_typ_monomorphic (Typ_aux (typ, _)) =
+let rec is_typ_monomorphic (Typ_aux (typ, l)) =
   match typ with
   | Typ_id _ -> true
   | Typ_tup typs -> List.for_all is_typ_monomorphic typs
@@ -1285,6 +1289,7 @@ let rec is_typ_monomorphic (Typ_aux (typ, _)) =
   | Typ_fn (typ1, typ2, _) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2
   | Typ_bidir (typ1, typ2) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2
   | Typ_exist _ | Typ_var _ -> false
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and is_typ_arg_monomorphic (Typ_arg_aux (arg, _)) =
   match arg with
   | Typ_arg_nexp _ -> true
@@ -1827,6 +1832,7 @@ let rec kid_order kids (Typ_aux (aux, l) as typ) =
   | Typ_app (_, args) ->
      List.fold_left (fun (ord, kids) arg -> let (ord', kids) = kid_order_arg kids arg in (ord @ ord', kids)) ([], kids) args
   | Typ_fn _ | Typ_bidir _ | Typ_exist _ -> typ_error l ("Existential or function type cannot appear within existential type: " ^ string_of_typ typ)
+  | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and kid_order_arg kids (Typ_arg_aux (aux, l) as arg) =
   match aux with
   | Typ_arg_typ typ -> kid_order kids typ