diff --git a/examples/features/tuples/nested_tuples.dpt b/examples/features/tuples/nested_tuples.dpt
new file mode 100644
index 00000000..21f064a3
--- /dev/null
+++ b/examples/features/tuples/nested_tuples.dpt
@@ -0,0 +1,70 @@
+// Polymorphic parsers using nested tuple arguments.
+// Eth header
+type eth_t = {
+  int<48> dst_mac;
+  int<48> src_mac;
+  int<16> etype;
+}
+const int<16> IP_ETHERTY = 0x0800;
+
+// IPv4 header type
+type ip_t = {
+  int<4> version;
+  int<4> ihl;
+  int<8> diffserv;
+  int<16> total_len;
+  int<16> id;
+  int<3> flags;
+  int<13> frag_offset;
+  int<8> ttl;
+  int<8> protocol;
+  int<16> hdr_csum;
+  int<32> src;
+  int<32> dst;
+}
+
+type udp_t = {
+  int<16> src_port;
+  int<16> dst_port;
+  int<16> length;
+  int<16> csum;
+}
+
+event passthrough(auto hdrs, Payload.t payload) {
+    generate_port(0, this);
+}
+
+parser parse_udp(auto l2_hdrs, bitstring pkt) {
+    udp_t udp = read(pkt);
+    match udp#dst_port with
+    | 2152 -> { 
+        generate passthrough((l2_hdrs, udp), Payload.parse(pkt));
+    }
+    | _ -> {    
+        generate passthrough((l2_hdrs, udp), Payload.parse(pkt));
+    }
+}
+
+parser parse_ip(auto l1_hdrs, bitstring pkt) {
+  ip_t ip = read(pkt);
+  match ip#protocol with 
+  | 0x11 -> { 
+        parse_udp((l1_hdrs, ip), pkt); 
+    }
+  | 132 -> { 
+        generate passthrough((l1_hdrs, ip), Payload.parse(pkt));
+    }
+  | _ -> {     
+       generate passthrough((l1_hdrs, ip), Payload.parse(pkt)); 
+    }
+}
+
+
+parser main(bitstring pkt) {
+    eth_t e = read(pkt);
+    match e#etype with
+    | LUCID_ETHERTY -> { do_lucid_parsing(pkt); } // call builtin parser 
+    | IP_ETHERTY -> { parse_ip(e, pkt); }    
+    | _ -> { generate passthrough(e, Payload.parse(pkt)); }
+}
+
diff --git a/examples/features/tuples/tuple_event.dpt b/examples/features/tuples/tuple_event.dpt
new file mode 100644
index 00000000..a3ac233d
--- /dev/null
+++ b/examples/features/tuples/tuple_event.dpt
@@ -0,0 +1,17 @@
+
+event tuple_foo(auto xy);
+handle tuple_foo(auto xy) {
+    printf("here in tuple_foo");
+}
+
+
+event foo(int x, int y);
+handle foo(int x, int y) {    
+    if (x == 1) {
+        tuple<<int, int>> xy = (x, y);
+        generate(tuple_foo(xy));
+    } else {
+        generate(tuple_foo(x));
+    }
+    generate(foo(1, 2));
+}
diff --git a/examples/features/tuples/tuple_event2.dpt b/examples/features/tuples/tuple_event2.dpt
new file mode 100644
index 00000000..be99fbee
--- /dev/null
+++ b/examples/features/tuples/tuple_event2.dpt
@@ -0,0 +1,16 @@
+
+event tuple_foo(auto xy);
+handle tuple_foo(auto xy) {
+    generate_port(1, tuple_foo(xy));
+}
+
+
+event foo(int x, int y);
+handle foo(int x, int y) {    
+    if (x == 1) {
+        tuple<<int, int>> xy = (x, y);
+        generate(tuple_foo(xy));
+    } else {
+        generate(tuple_foo(x));
+    }
+}
diff --git a/examples/features/tuples/tuple_event3.dpt b/examples/features/tuples/tuple_event3.dpt
new file mode 100644
index 00000000..b9a53c5a
--- /dev/null
+++ b/examples/features/tuples/tuple_event3.dpt
@@ -0,0 +1,55 @@
+// Simple IP packet function that is generic to underlay headers.
+// Uses tuples and polymorphic event parameters.
+type eth_t = {
+    int<48> dmac;
+    int<48> smac;
+    int<16> ety;
+}
+type ip_hdr_t = {
+    int<32> src;
+    int<32> dst;
+    int<16> len;
+}
+type vlan_t = {
+    int<16> vty;
+}
+
+const int<16> ETY_IP = 0x0800;
+const int<16> ETY_VLAN = 0x8080;
+
+// packet event anon(auto hdrs, Payload.t payload) {
+//     generate_port(1, anon(hdrs, payload));
+// }
+
+packet event ip_packet(auto underlay_headers, ip_hdr_t ip_hdr, Payload.t unparsed_payload) {
+    ip_hdr_t new_ip_hdr = {ip_hdr with src = ip_hdr#dst; dst = ip_hdr#src;};
+    event pkt_out = ip_packet(underlay_headers, new_ip_hdr, unparsed_payload);
+    generate_port(1, pkt_out);
+}
+
+parser main(bitstring pkt) {
+    eth_t eth_hdr = read(pkt);
+    match eth_hdr#ety with 
+    | LUCID_ETHERTY -> { do_lucid_parsing(pkt); }
+    | ETY_IP -> {
+        ip_hdr_t ip_hdr = read(pkt);
+        generate ip_packet(eth_hdr, ip_hdr, Payload.parse(pkt));
+    }
+    | ETY_VLAN -> {
+        vlan_t vlan_hdr = read(pkt);
+        match vlan_hdr#vty with 
+        | ETY_IP -> {
+            ip_hdr_t ip_hdr =read(pkt);
+            generate ip_packet((eth_hdr, vlan_hdr), ip_hdr, Payload.parse(pkt));
+        }
+        | _ -> {
+            drop;
+            // generate anon((eth_hdr, vlan_hdr), Payload.parse(pkt));
+        }
+    }
+    | _ -> { 
+        drop;
+        // generate anon(eth_hdr, Payload.parse(pkt));
+    }
+}
+
diff --git a/examples/features/tuples/tuple_event4.dpt b/examples/features/tuples/tuple_event4.dpt
new file mode 100644
index 00000000..c130aa4b
--- /dev/null
+++ b/examples/features/tuples/tuple_event4.dpt
@@ -0,0 +1,15 @@
+type my_t = {
+    int a;
+    int b;
+}
+
+event my_event(my_t my_arg);
+handle my_event(my_t my_arg) {
+    my_t new_arg = {a=my_arg#b; b=my_arg#a;};
+    generate(my_event(new_arg));
+}
+
+event foo(int x, int y, int z, int zz); 
+handle foo(int x, int y, int z, int zz){
+    generate(my_event({a=x; b=y;}));
+}
\ No newline at end of file
diff --git a/examples/features/tuples/tuple_event_wrong.dpt b/examples/features/tuples/tuple_event_wrong.dpt
new file mode 100644
index 00000000..b4795c43
--- /dev/null
+++ b/examples/features/tuples/tuple_event_wrong.dpt
@@ -0,0 +1,11 @@
+event tuple_foo(auto xy);               
+handle tuple_foo(auto xy) {             
+    if (xy ==  (1, 2, 3)) {             
+        printf("here");
+    }
+}                                      
+event foo(int x, int y);
+handle foo(int x, int y) {    
+    tuple<<int, int>> xy = (x, y);      
+    generate(tuple_foo(xy));
+}
diff --git a/examples/features/tuples/tuples.md b/examples/features/tuples/tuples.md
new file mode 100644
index 00000000..951c9e68
--- /dev/null
+++ b/examples/features/tuples/tuples.md
@@ -0,0 +1,98 @@
+## Tuples and events with polymorphic parameters
+
+
+This branch (26.4.tuples) adds tuples and events with polymorphic parameters to Lucid. 
+
+### Motivation
+
+Lucid programs typically operate at specific protocol layers, meaning they are generic to the packet headers of lower layers and the headers + payload of higher layers. Previously, it was up to the programmer to define every combination of possible underlay headers as separate record types. 
+
+For instance if the programmer wants to handle IP packets that may arrive in either ethernet or vlan packets, they must write two separate handlers for each underlay protocol stack: 
+```
+packet event eth_ip_packet(eth_t eth_hdr, ip_hdr_t ip_hdr, bytes.t unparsed_payload) {
+    ip_hdr_t new_ip_hdr = {ip_hdr with src_addr = ip_hdr#dst_addr; dst_addr = ip_hdr#src_addr;};
+    event pkt_out = eth_ip_packet(eth_hdr, new_ip_hdr, unparsed_payload);
+    generate_port(ingress_port, pkt_out);
+}
+packet event eth_vlan_ip_packet(eth_t eth_hdr, vlan_t vlan_hdr, ip_hdr_t ip_hdr, bytes.t unparsed_payload) {
+    ip_hdr_t new_ip_hdr = {ip_hdr with src_addr = ip_hdr#dst_addr; dst_addr = ip_hdr#src_addr;};
+    event pkt_out = eth_vlan_ip_packet(eth_hdr, vlan_hdr, new_ip_hdr, unparsed_payload);
+    generate(ingress_port, pkt_out);
+}
+```
+In the above example, the handler bodies are generic with respect to the underlay headers, yet there still must be separate events and handlers. This gets unweildy very quickly in programs for more realistic networks.
+
+The solution introduced here is to support: 1. tuples as event parameters; 2. polymorphic event parameters. Then we can rewrite the above example like this: 
+```
+packet event ip_packet(auto underlay_headers, ip_hdr_t ip_hdr, bytes.t unparsed_payload) {
+    ip_hdr_t new_ip_hdr = {ip_hdr with src_addr = ip_hdr#dst_addr; dst_addr = ip_hdr#src_addr;};
+    event pkt_out = ip_packet(underlay_headers, new_ip_hdr, unparsed_payload);
+    generate(pkt_out);
+}
+```
+
+
+### New language features
+
+#### Tuples
+Tuples are basically records with anonymous fields and whose type is defined dynamically when a variable is declared. Tuples are immutable, but can be constructed, used as arguments, and projected similarly to records.
+
+**Tuple type declarations and expressions**
+
+`tuple<<int, int>> my_pair = (1, 2);`
+
+**Tuple projection**
+
+`int a = my_pair.0; int b = my_pair.1;`
+
+#### Polymorphic event parameters
+Parameters in events and handlers may now be polymorphic, using the `auto` type keyword: 
+
+```
+packet event ip_packet(auto underlay_headers, ...);
+handler ip_packet(auto underlay_headers, ...); 
+```
+
+Polymorphism works almost the same as for functions, with one exception. In a function, the type system allows the body of a function to restrict a polymorphic parameter to a specific type by operating on it. For example: 
+```
+fun foo(auto x) { int y = x + 1;} // the type checker infers type int for x
+```
+
+This is not (currently) allowed for events. Any operation on a polymorphic parameter in a handler body that requires the parameter to be a specific type will cause a typing error. 
+
+Events with polymorphic parameters may not be given user-defined tag numbers (because they are eliminated by monomorphization, which duplicates the declarations).
+
+### Implementation
+
+Tuples have dedicated AST nodes in the frontend syntax, and are eliminated before the midend. 
+
+Polymorphic event parameters are unified with the respective handler parameters by the type checker, and handlers are checked to not restrict the type of their polymorphic parameters. 
+
+Polymorphic events are eliminated by creating monomorphic duplicates based on event-typed expressions in the program (i.e., event constructors).
+
+It is currently a runtime error to send a program an event value with an argument that uses a parameter with a type not used elsewhere in the program. 
+
+For example, if the program defines: `packet event foo(auto x, ...);`
+and only ever uses `foo(int x)` events, it is a runtime error to pass in an event `foo(bool x)`.
+
+
+### Test cases
+
+`tuple_event.dpt` -- minimal example of tuples
+`tuple_event_wrong.dpt` -- a handler using a polymorphic tuple parameter incorrectly
+`tuple_event2.dpt` -- a handler using a polymorphic tuple parameter correctly
+`tuple_event3.dpt` -- event using a polymorphic parameter with different tuple types depending on parsing (this is the ip_packet example from the motivation).
+`nested_tuples.dpt` -- demonstrates support for parsers that also use tuple arguments and polymorphism.
+
+### Future considerations
+
+- The interpreter should be updated to support input of non-packet events with tuple types.
+
+- It may be useful for users to define polymorphic events with monomorphic handlers, for specific instances that they want to handle, but are not generated in the program. For example:
+```
+event foo(auto x, auto y);
+handle foo(int x, int y) { ... }
+handle foo(bool x, bool y){ ... };
+```
+
+- The polymorphic event elimination pass may fail for programs that place transitive restrictions on the types of polymorphic event parameters. See the comment in MonomorphicEventArgs.ml for more information.
\ No newline at end of file
diff --git a/src/bin/InterpMain.ml b/src/bin/InterpMain.ml
index 5bb5c55d..aaa6a771 100644
--- a/src/bin/InterpMain.ml
+++ b/src/bin/InterpMain.ml
@@ -47,6 +47,10 @@ let main () =
   in
   match spec_file with
   | None ->
+    (* run the midend pipeline for debugging *)
+    (* let _ =
+      MidendPipeline.process_prog ds
+    in *)
     Console.report "No specification file provided, so skipping simulation"
   | Some spec_file ->
     let ds =
diff --git a/src/lib/dune b/src/lib/dune
index a4260a62..8f8c18ef 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -61,7 +61,9 @@
    sizeInlining
    builtinsTupleElimination
    renaming
+   monomorphicEventArgs
    globalArgElimination
+   refreshTypes
    explicitReturns
    moduleAliasing
    recordElimination
diff --git a/src/lib/frontend/FrontendPipeline.ml b/src/lib/frontend/FrontendPipeline.ml
index 6263e5ca..7df265f9 100644
--- a/src/lib/frontend/FrontendPipeline.ml
+++ b/src/lib/frontend/FrontendPipeline.ml
@@ -42,8 +42,8 @@ let process_prog ?(opts=def_opts) builtin_tys ds =
   print_if_debug ds;
   (* TODO: Might be nice to have an additional renaming pass earlier, so we
      can run the slot analysis immediately after typing *)
+  (* TODO: fix slot analysis *)
   print_if_verbose "-------Performing parser slot analysis---------";
-  let slot_assignments = SlotAnalysis.analyze_prog ds in
   print_if_verbose "-------Eliminating modules---------";
   let ds = ModuleElimination.eliminate_prog ds in
   print_if_debug ds;
@@ -65,6 +65,8 @@ let process_prog ?(opts=def_opts) builtin_tys ds =
   print_if_verbose "---------Eliminating events with global arguments----------";
   let ds = GlobalArgElimination.eliminate_prog ds in
   print_if_debug ds;
+  (* print_if_verbose "---------Making Polymorphic Events Monomorphic----------"; *)  
+  let poly_event_renaming, ds = MonomorphicEventArgs.eliminate_prog builtin_tys ds in
   print_if_verbose "---------------typing3-------------";
   let ds = Typer.infer_prog builtin_tys ds in
   print_if_debug ds;
@@ -98,6 +100,7 @@ let process_prog ?(opts=def_opts) builtin_tys ds =
          let ds = RecordElimination.eliminate_prog ds in
          print_if_debug ds;
          print_if_verbose "---------------typing7-------------";
+         
          let ds = Typer.infer_prog builtin_tys ds in
          ds)
       else (
@@ -119,13 +122,19 @@ let process_prog ?(opts=def_opts) builtin_tys ds =
   print_if_debug ds;
   print_if_verbose "---------------typing9-------------";
   let ds = Typer.infer_prog builtin_tys ds in
+  (* Slot analysis does not handle tuples, polymorphic event args, or possibly modules, 
+     so until we get back to it, the earliest it can go is here. *)
+  let slot_assignments = SlotAnalysis.analyze_prog ds in
+
   print_if_verbose "-------Inlining Constants-------";
   let ds = ConstInlining.inline_prog ds in
   print_if_debug ds;
   (* Not sure if this is still necessary *)
   print_if_verbose "-----------re-re-renaming-----------";
   let renaming'', ds = Renaming.rename ds in
-  let renaming = Renaming.compose_envs [renaming; renaming'; renaming''] in
+  let renaming = Renaming.compose_envs [renaming; 
+  poly_event_renaming; 
+  renaming'; renaming''] in
   print_if_debug ds;
   print_if_verbose "---------------typing again-------------";
   (* Just to be safe *)
diff --git a/src/lib/frontend/Lexer.mll b/src/lib/frontend/Lexer.mll
index 00666f59..7069bd8e 100644
--- a/src/lib/frontend/Lexer.mll
+++ b/src/lib/frontend/Lexer.mll
@@ -50,6 +50,7 @@ rule token = parse
   | "else"            { ELSE (position lexbuf) }
   | "int"             { TINT (position lexbuf) }
   | "bool"            { TBOOL (position lexbuf) }
+  | "tuple"           { TUPLE (position lexbuf) }
   | "event"           { EVENT (position lexbuf) }
   | "generate"        { GENERATE (position lexbuf) }
   | "generate_switch" { SGENERATE (position lexbuf) }
diff --git a/src/lib/frontend/Parser.mly b/src/lib/frontend/Parser.mly
index 0d5bf8a1..9b36f712 100644
--- a/src/lib/frontend/Parser.mly
+++ b/src/lib/frontend/Parser.mly
@@ -120,6 +120,7 @@
 %token <Span.t> COMMA
 %token <Span.t> DOT
 %token <Span.t> TBOOL
+%token <Span.t> TUPLE
 %token <Span.t> EVENT
 %token <Span.t> GENERATE
 %token <Span.t> SGENERATE
@@ -212,6 +213,11 @@ ty:
     | QID                               { ty_sp (TQVar (QVar (snd $1))) (fst $1) }
     | AUTO                              { ty_sp (TQVar (QVar (fresh_auto ()))) $1 }
     | cid    				            { ty_sp (TName (snd $1, [], true)) (fst $1) }
+    | TUPLE ty_poly                     { 
+                                            let raw_tys = List.map (fun ty -> ty.raw_ty) (snd $2) in
+                                            ty_sp (TTuple (raw_tys)) (Span.extend $1 (fst $2)) }
+
+
     | cid poly				            { ty_sp (TName (snd $1, snd $2, true)) (fst $1) }
     | cid ty_poly                       {
                                             let raw_tys = List.map (fun ty -> ty.raw_ty) (snd $2) in
@@ -257,9 +263,18 @@ poly:
 single_poly:
     | LESS size MORE                    { Span.extend $1 $3, snd $2 }
 
-ty_or_empty_tuple: 
+ty_or_empty_tuple:
     | ty                                      { $1 }
     | LPAREN RPAREN                           { ty_sp (TTuple([])) (Span.extend $1 $2) }
+    /* Parenthesized comma-form tuple type, e.g. `(int<48>, int<32>)`. Only
+       legal inside `<<...>>` slots (Table.t key/data/arg/ret) because that's
+       the only place `ty_or_empty_tuple` is used. Requires at least two
+       element types so `(t)` continues to mean a parenthesized single ty,
+       not a 1-tuple. Avoids the lexer-greedy `>>` issue that `tuple<<...>>`
+       runs into when the inner type ends in `>`. */
+    | LPAREN ty COMMA tys RPAREN              {
+        let raw_tys = List.map (fun ty -> ty.raw_ty) ($2 :: (snd $4)) in
+        ty_sp (TTuple raw_tys) (Span.extend $1 $5) }
 
 ty_polys:
     | ty_or_empty_tuple                       { [$1] }
@@ -332,6 +347,9 @@ exp:
         op_sp PatExact [$3] (Span.extend $1 $4)}
 
     | LPAREN TINT single_poly RPAREN exp  { op_sp (Cast(snd $3))[$5] (Span.extend $1 $5.espan) }
+
+    | exp PROJ NUM                        { get_sp $1 (IConst (Z.to_int (snd $3))) (Span.extend $1.espan (fst $3)) }
+
     | exp PROJ ID                         { proj_sp $1 (Id.name (snd $3)) (Span.extend $1.espan (fst $3)) }
     // | LPAREN exp RPAREN		             	  { $2 }
     | exp LBRACKET size COLON size RBRACKET { op_sp (Slice (snd $3, snd $5)) [$1] (Span.extend ($1).espan (fst $5)) }
@@ -360,6 +378,8 @@ exp:
 // an expression with a parenthesis is a tuple, unless its a single-element tuple, in which case its just the element.
 // note that user-written tuples may not appear in the AST, so any parsed tuple must be unpacked with 
 // SyntaxUtils.unpack_tuple before calling a AST node constructor
+// Update 4/2026 -- the above comment is for table matches, 
+// where tuples were initially used. They are now also may be declared by users.
 paren_exp:
     | LPAREN args RPAREN                  { match $2 with 
                                             | [] -> tuple_sp [] (Span.extend $1 $3)
diff --git a/src/lib/frontend/Printing.ml b/src/lib/frontend/Printing.ml
index 1210f0e4..ca7c98f8 100644
--- a/src/lib/frontend/Printing.ml
+++ b/src/lib/frontend/Printing.ml
@@ -319,6 +319,7 @@ and e_to_string e =
     Printf.sprintf "hash<<%s>>(%s)" (size_to_string size) (es_to_string es)
   | EFlood e -> Printf.sprintf "flood %s" (exp_to_string e)
   | EProj (e, l) -> exp_to_string e ^ "#" ^ l
+  | EGet (e, l) -> exp_to_string e ^ "#" ^ size_to_string l
   | ERecord lst ->
     Printf.sprintf
       "{%s}"
diff --git a/src/lib/frontend/Syntax.ml b/src/lib/frontend/Syntax.ml
index 8a522bba..941950eb 100644
--- a/src/lib/frontend/Syntax.ml
+++ b/src/lib/frontend/Syntax.ml
@@ -174,6 +174,7 @@ and e =
   | ERecord of (string * exp) list
   | EWith of exp * (string * exp) list (* { e with ...} syntax *)
   | EProj of exp * string
+  | EGet  of exp * size (* tuple get *)
   | EVector of exp list
   | EComp of exp * id * size (* Vector comprehension *)
   | EIndex of exp * size
@@ -471,6 +472,7 @@ let op_sp op args span = exp_sp (EOp (op, args)) span
 let call_sp cid args span = exp_sp (ECall (cid, args, false)) span
 let ucall_sp cid args span = exp_sp (ECall (cid, args, true)) span
 let hash_sp size args span = exp_sp (EHash (size, args)) span
+let get_sp e l span = exp_sp (EGet (e, l)) span
 let proj_sp e l span = exp_sp (EProj (e, l)) span
 let record_sp lst span = exp_sp (ERecord lst) span
 let with_sp base lst span = exp_sp (EWith (base, lst)) span
diff --git a/src/lib/frontend/SyntaxUtils.ml b/src/lib/frontend/SyntaxUtils.ml
index 67cf3743..d4d991e1 100644
--- a/src/lib/frontend/SyntaxUtils.ml
+++ b/src/lib/frontend/SyntaxUtils.ml
@@ -153,8 +153,8 @@ let rec equiv_lists f lst1 lst2 =
   | _ -> false
 ;;
 
-let rec equiv_size ?(qvars_wild = false) s1 s2 =
-  let equiv_size = equiv_size ~qvars_wild in
+let rec equiv_size ?(qvars_wild = false) ?(ignore_qvar_ids = false) s1 s2 =
+  let equiv_size = equiv_size ~qvars_wild ~ignore_qvar_ids in
   match normalize_size s1, normalize_size s2 with
   | IConst n1, IConst n2 -> n1 = n2
   | IUser id1, IUser id2 -> Cid.equal id1 id2
@@ -168,7 +168,7 @@ let rec equiv_size ?(qvars_wild = false) s1 s2 =
           | IVar (QVar _) -> true
           | _ -> false)
          vs
-  | IVar tqv, s | s, IVar tqv -> STQVar.equiv_tqvar ~qvars_wild equiv_size tqv s
+  | IVar tqv, s | s, IVar tqv -> STQVar.equiv_tqvar ~qvars_wild ~ignore_qvar_ids equiv_size tqv s
   | ITup(vs1), ITup(vs2) -> equiv_lists equiv_size vs1 vs2
   | IConst _, _
   | IUser _, _ 
@@ -203,15 +203,15 @@ let try_subtract_sizes s1 s2 =
   | _ -> None
 ;;
 
-let rec equiv_effect ?(qvars_wild = false) e1 e2 =
-  let equiv_effect = equiv_effect ~qvars_wild in
+let rec equiv_effect ?(qvars_wild = false) ?(ignore_qvar_ids = false) e1 e2 =
+  let equiv_effect = equiv_effect ~qvars_wild ~ignore_qvar_ids in
   match e1, e2 with
   | FZero, FZero -> true
   | FSucc e1', FSucc e2' | FProj e1', FProj e2' -> equiv_effect e1' e2'
   | FIndex (id1, e1'), FIndex (id2, e2') ->
     Id.equal id1 id2 && equiv_effect e1' e2'
   | FVar tqv, e | e, FVar tqv ->
-    FTQVar.equiv_tqvar ~qvars_wild equiv_effect tqv e
+    FTQVar.equiv_tqvar ~qvars_wild ~ignore_qvar_ids equiv_effect tqv e
   | (FZero | FSucc _ | FProj _ | FIndex _), _ -> false
 ;;
 
@@ -263,11 +263,49 @@ let normalizer () =
 let normalize_tfun func_ty = (normalizer ())#visit_func_ty () func_ty
 let normalize_ty ty = (normalizer ())#visit_ty () ty
 
-let rec equiv_raw_ty ?(ignore_effects = false) ?(qvars_wild = false) ty1 ty2 =
-  let equiv_size = equiv_size ~qvars_wild in
-  let equiv_effect = equiv_effect ~qvars_wild in
-  let equiv_raw_ty = equiv_raw_ty ~ignore_effects ~qvars_wild in
-  let equiv_ty = equiv_ty ~ignore_effects ~qvars_wild in
+(* check if a type is polymorphic, i.e., it has a TQVar in it *)
+let rec is_polymorphic_raw_ty rty =
+  match TyTQVar.strip_links rty with
+  | TQVar _ -> true
+  | TBool | TVoid | TGroup | TEvent | TBitstring -> false
+  | TInt sz | TPat sz -> is_polymorphic_size sz
+  | TMemop (_, sz) -> is_polymorphic_size sz
+  | TFun func ->
+    is_polymorphic_ty func.ret_ty || List.exists is_polymorphic_ty func.arg_tys
+  | TName (_, sizes, _) | TAbstract (_, sizes, _, _) ->
+    List.exists is_polymorphic_size sizes
+  | TRecord fields -> List.exists (fun (_, rty) -> is_polymorphic_raw_ty rty) fields
+  | TVector (rty, sz) -> is_polymorphic_raw_ty rty || is_polymorphic_size sz
+  | TTuple rtys -> List.exists is_polymorphic_raw_ty rtys
+  | TTable tbl ->
+    List.exists is_polymorphic_ty tbl.tkey_sizes
+    || List.exists is_polymorphic_ty tbl.tparam_tys
+    || List.exists is_polymorphic_ty tbl.tret_tys
+  | TBuiltin (_, rtys, _) -> List.exists is_polymorphic_raw_ty rtys
+  | TAction acn ->
+    List.exists is_polymorphic_ty acn.aarg_tys
+    || List.exists is_polymorphic_ty acn.aret_tys
+  | TActionConstr acn_ctor ->
+    List.exists is_polymorphic_ty acn_ctor.aconst_param_tys
+    || is_polymorphic_raw_ty (TAction acn_ctor.aacn_ty)
+
+and is_polymorphic_size sz =
+  match STQVar.strip_links sz with
+  | IVar (QVar _) -> true
+  | IVar _ -> false
+  | IConst _ | IUser _ -> false
+  | ISum (sizes, _) | ITup sizes -> List.exists is_polymorphic_size sizes
+
+and is_polymorphic_ty ty =
+  is_polymorphic_raw_ty ty.raw_ty
+;;
+
+
+let rec equiv_raw_ty ?(ignore_effects = false) ?(qvars_wild = false) ?(ignore_qvar_ids = false) ty1 ty2 =
+  let equiv_size = equiv_size ~qvars_wild ~ignore_qvar_ids in
+  let equiv_effect = equiv_effect ~qvars_wild ~ignore_qvar_ids in
+  let equiv_raw_ty = equiv_raw_ty ~ignore_effects ~qvars_wild ~ignore_qvar_ids in
+  let equiv_ty = equiv_ty ~ignore_effects ~qvars_wild ~ignore_qvar_ids in
   match ty1, ty2 with
   | TBool, TBool | TVoid, TVoid | TGroup, TGroup | TEvent, TEvent -> true
   | TInt size1, TInt size2 -> equiv_size size1 size2
@@ -290,7 +328,7 @@ let rec equiv_raw_ty ?(ignore_effects = false) ?(qvars_wild = false) ty1 ty2 =
   | TAction{aarg_tys=args1; aret_tys=aret1;}, TAction{aarg_tys=args2; aret_tys=aret2;} ->
     equiv_lists equiv_ty args1 args2 && equiv_lists equiv_ty aret1 aret2
   | TQVar tqv, ty | ty, TQVar tqv ->
-    TyTQVar.equiv_tqvar ~qvars_wild equiv_raw_ty tqv ty
+    TyTQVar.equiv_tqvar ~qvars_wild ~ignore_qvar_ids equiv_raw_ty tqv ty
   | TRecord lst1, TRecord lst2 ->
     if List.length lst1 <> List.length lst2
     then false
@@ -331,11 +369,11 @@ let rec equiv_raw_ty ?(ignore_effects = false) ?(qvars_wild = false) ty1 ty2 =
       | TBuiltin _)
     , _ ) -> false
 
-and equiv_ty ?(ignore_effects = false) ?(qvars_wild = false) ty1 ty2 =
+and equiv_ty ?(ignore_effects = false) ?(qvars_wild = false) ?(ignore_qvar_ids = false) ty1 ty2 =
   (ignore_effects
   || is_not_global ty1
-  || equiv_effect ~qvars_wild ty1.teffect ty2.teffect)
-  && equiv_raw_ty ~ignore_effects ~qvars_wild ty1.raw_ty ty2.raw_ty
+  || equiv_effect ~qvars_wild ~ignore_qvar_ids ty1.teffect ty2.teffect)
+  && equiv_raw_ty ~ignore_effects ~qvars_wild ~ignore_qvar_ids ty1.raw_ty ty2.raw_ty
 ;;
 
 let max_effect e1 e2 =
@@ -358,7 +396,8 @@ let default_expression ty =
     end
     | TRecord lst ->
       record_sp (List.map (fun (s, raw_ty) -> s, aux raw_ty) lst) Span.default
-    | TTuple _ -> failwith "Cannot create default expression for tuple"
+    | TTuple(raw_tys) -> 
+      tuple_sp (List.map (fun (raw_ty) -> aux raw_ty) raw_tys) Span.default
     | TName(cid, _, _) -> failwith ("Cannot create default expression for user type "^(Cid.to_string cid))
     | TBuiltin(cid, _, _) -> failwith ("Cannot create default expression for builtin type "^(Cid.to_string cid))
     | TMemop _ -> failwith "Cannot create default expression for memop"
@@ -391,7 +430,7 @@ let rec is_compound e =
   | EHash _ | EOp _ | ECall _ | EStmt _ -> true
   | ETableCreate _ -> true
   | ETableMatch _ -> true
-  | EComp (e, _, _) | EIndex (e, _) | EProj (e, _) | EFlood e -> is_compound e
+  | EComp (e, _, _) | EIndex (e, _) | EProj (e, _) | EGet (e, _) | EFlood e -> is_compound e
   | EVector entries | ETuple entries -> List.exists is_compound entries
   | ERecord entries -> List.exists (is_compound % snd) entries
   | EWith (base, entries) ->
@@ -689,6 +728,7 @@ let e_to_constr_str e = match e with
 | ERecord (_) -> "record"
 | EWith (_) -> "with"
 | EProj (_) -> "proj"
+| EGet (_) -> "eget"
 | EVector (_) -> "vector"
 | EComp (_) -> "comp"
 | EIndex (_) -> "index"
diff --git a/src/lib/frontend/TQVar.ml b/src/lib/frontend/TQVar.ml
index b5016677..73a9d194 100644
--- a/src/lib/frontend/TQVar.ml
+++ b/src/lib/frontend/TQVar.ml
@@ -9,6 +9,14 @@ module TQVar_tys = struct
     | Unbound of id * level
     | Link of 'a
 
+    (* Note/reminder on TVar and QVar meaning: 
+        TVar represents a type that is not yet resolved (t)
+        QVar represents _any_ type, independent at each use (forall t.t)
+        - Generalization replaces TVars with QVars, it is meant to be used 
+          when we are done inferring a function body, on its polymorphic arguments.
+        - Instantiation replaces QVars with TVars, when you want to unify a 
+          polymorphic type with another type, primarily in a call. *)
+
   and 'a tqvar =
     | TVar of 'a tyvar ref
     | QVar of id
@@ -50,9 +58,10 @@ module Make (A : TQVarArg) = struct
     | _ -> a
   ;;
 
-  let equiv_tqvar ?(qvars_wild = false) equiv_a t a =
+  let equiv_tqvar ?(qvars_wild = false) ?(ignore_qvar_ids = false) equiv_a t a =
     match t, A.proj (strip_links a) with
     | QVar _, _ when qvars_wild -> true
+    | QVar _, Some (QVar _) when ignore_qvar_ids -> true
     | QVar id1, Some (QVar id2) -> Id.equal id1 id2
     | ( TVar { contents = Unbound (id1, l1) }
       , Some (TVar { contents = Unbound (id2, l2) }) ) ->
diff --git a/src/lib/frontend/analysis/EventFormat.ml b/src/lib/frontend/analysis/EventFormat.ml
index 47d5c548..a07e6c1f 100644
--- a/src/lib/frontend/analysis/EventFormat.ml
+++ b/src/lib/frontend/analysis/EventFormat.ml
@@ -37,7 +37,10 @@ let set_event_nums ds =
           let rv = DEvent(id, Some !num, sort, specs, args) in
           num := !num + 1;
           rv
-        | Some _ -> DEvent(id, num_opt, sort, specs, args)
+        | Some _ -> 
+          (* TODO: check if the event has any polymorphic arguments. 
+              If so, we cannot currently support user-defined event numbers *)
+          DEvent(id, num_opt, sort, specs, args)
     end
   in
   v#visit_decls () ds
diff --git a/src/lib/frontend/analysis/Wellformed.ml b/src/lib/frontend/analysis/Wellformed.ml
index 3404859c..266e969d 100644
--- a/src/lib/frontend/analysis/Wellformed.ml
+++ b/src/lib/frontend/analysis/Wellformed.ml
@@ -15,6 +15,7 @@ open Printing
    - All events have either one or two handlers declared: one in ingress and one in egress, 
      which must be in the same scope as them.
    - All sizes in symbolic declarations are either concrete or symbolic themselves
+   - Events with user-defined tag numbers cannot have polymorphic parameters, since they need to be monomorphized (duplicated) during compilation.
 
    Checks we do during typechecking:
    - No dynamic global creation
@@ -120,6 +121,36 @@ let check_symbolics ds =
   checker#visit_decls (ref IdSet.empty) ds
 ;;
 
+
+(* Make sure that events with user-defined tag numbers
+   do not have polymorphic events. *)
+let rec check_numbered_events ds = 
+  let checker =
+    object
+      inherit [_] s_iter
+
+      method! visit_decl _ decl =
+        match decl.d with
+        | DEvent (id, num_opt, _, _, params) ->
+          (match num_opt with
+           | None -> ()
+           | Some num ->
+             if List.exists (fun (_, ty) -> is_polymorphic_ty ty) params
+             then
+               Console.error_position decl.dspan
+               @@ Printf.sprintf
+                    "Event %s has assigned number %d, but also has polymorphic \
+                     parameters. Events with assigned numbers cannot have \
+                     polymorphic parameters, since they need to be monomorphized \
+                     (duplicated) during compilation."
+                    (id_to_string id)
+                    num)
+        | _ -> ()
+    end
+  in
+  checker#visit_decls () ds
+;;
+
 (* Next up: make sure each event has exactly one handler defined, which must be
    in the same scope. Also ensure that we don't have two events with the same
    name in a given scope.
@@ -417,7 +448,8 @@ let pre_typing_checks ?(handlers=true) ds =
   if handlers then match_handlers ds;
   check_symbolics ds;
   check_payloads ds;
-  check_match_returns ds
+  check_match_returns ds;
+  check_numbered_events ds
 ;;
 
 (*** QVar checking. This is run on each decl after its type is inferred, and makes
@@ -550,8 +582,9 @@ let rec check_qvars d =
   | DAction _ -> ()
   | DGlobal _ ->
     (* None allowed at all *) basic_qvar_checker#visit_decl (true, true) d
-  | DSize _ | DSymbolic _ | DConst _ | DExtern _ | DParser _ ->
+  | DSize _ | DSymbolic _ | DConst _ | DExtern _ ->
     (* Only allowed in effect *) basic_qvar_checker#visit_decl (false, true) d
+  | DParser _ ->  () (* no restrictions, like functions. Previously was only allowed in effects. *)
   | DConstr _ ->
     (* Allowed in both sizes and effects *)
     basic_qvar_checker#visit_decl (false, false) d
diff --git a/src/lib/frontend/transformations/BuiltinsTupleElimination.ml b/src/lib/frontend/transformations/BuiltinsTupleElimination.ml
index 24dde73f..0690e487 100644
--- a/src/lib/frontend/transformations/BuiltinsTupleElimination.ml
+++ b/src/lib/frontend/transformations/BuiltinsTupleElimination.ml
@@ -85,6 +85,10 @@ let rec eliminate_exp e =
   | EProj (e1, str) ->
     let stmt, e1' = eliminate_exp e1 in
     stmt, { e with e = EProj (e1', str) }
+  | EGet (e1, idx) -> 
+    let stmt, e1' = eliminate_exp e1 in
+    stmt, { e with e = EGet (e1', idx) }
+
   | EVector es ->
     let stmt, es' = eliminate_exps es in
     stmt, { e with e = EVector es' }
@@ -188,4 +192,29 @@ let eliminator =
   end
 ;;
 
-let eliminate_prog (ds : decl list) = eliminator#visit_decls () ds
+(* convert EGet expressions into TGet operations *)
+let eget_eliminator = 
+  object (self)
+  inherit [_] s_map as super
+  method! visit_exp acc exp = 
+    match exp.e with 
+    | EGet(etup, idx) -> 
+      let etup = {etup with e=self#visit_e acc etup.e} in
+      let i =
+        match idx with
+        | IConst i -> i
+        | _ -> failwith "Tuple elimination: encountered invalid tuple get arg"
+      in
+      let tup_len = match (Option.get etup.ety).raw_ty with 
+      | TTuple(raw_tys) -> List.length raw_tys
+      | _ -> failwith "Tuple elimination error: encountered tuple expression with non-tuple type"
+      in
+      let e_new = EOp(TGet(tup_len, i), [etup]) in
+      {exp with e=e_new}
+    | _ -> {exp with e=self#visit_e acc exp.e}
+    end
+;;
+
+let eliminate_prog (ds : decl list) =   
+  eliminator#visit_decls () (eget_eliminator#visit_decls () ds)
+;;
\ No newline at end of file
diff --git a/src/lib/frontend/transformations/ConcreteUserTypes.ml b/src/lib/frontend/transformations/ConcreteUserTypes.ml
index 648fb236..37aa473e 100644
--- a/src/lib/frontend/transformations/ConcreteUserTypes.ml
+++ b/src/lib/frontend/transformations/ConcreteUserTypes.ml
@@ -44,7 +44,7 @@ let is_tydecl_concrete (id, sizes, ty, _) =
 
 module TypeHash = struct
   type t = raw_ty
-  let equal = SyntaxUtils.equiv_raw_ty ~ignore_effects:false ~qvars_wild:false
+  let equal = SyntaxUtils.equiv_raw_ty ~ignore_effects:false ~qvars_wild:false ~ignore_qvar_ids:false
   let hash = (fun _ -> 1)
 end
 module TypeHashTbl = Hashtbl.Make(TypeHash)
diff --git a/src/lib/frontend/transformations/EStmtElimination.ml b/src/lib/frontend/transformations/EStmtElimination.ml
index c00dc05b..2c9bed30 100644
--- a/src/lib/frontend/transformations/EStmtElimination.ml
+++ b/src/lib/frontend/transformations/EStmtElimination.ml
@@ -34,6 +34,9 @@ let rec inline_exp e =
   | EProj (e1, str) ->
     let stmt, e1' = inline_exp e1 in
     stmt, { e with e = EProj (e1', str) }
+  | EGet (e1, str) ->
+    let stmt, e1' = inline_exp e1 in
+    stmt, { e with e = EGet (e1', str) }
   | EVector es ->
     let stmt, es' = inline_exps es in
     stmt, { e with e = EVector es' }
diff --git a/src/lib/frontend/transformations/MonomorphicEventArgs.ml b/src/lib/frontend/transformations/MonomorphicEventArgs.ml
new file mode 100644
index 00000000..75d6541f
--- /dev/null
+++ b/src/lib/frontend/transformations/MonomorphicEventArgs.ml
@@ -0,0 +1,528 @@
+open Batteries
+open Syntax
+open SyntaxUtils
+open Collections
+
+(* This pass converts events/handlers with polymorphic parameters into 
+   multiple monomorphic events/handlers, one for each unique type signature
+   of parameters used in the program. *)
+
+
+(* event id -> event arg types *)
+module IdMap = Collections.IdMap
+
+(* The template for a concrete instance of a poly event *)
+type concrete_sig = {id : id; concrete_tys : ty list;}
+
+let concrete_sig_equal (sig1 : concrete_sig) (sig2 : concrete_sig) = 
+  (* print_endline ("[concrete_sig_equal] comparing concrete sigs: " ^ (Id.name sig1.id) ^ " vs " ^ (Id.name sig2.id)); *)
+  let equiv_ids = Id.equal sig1.id sig2.id in
+  let equiv_tys = equiv_lists (equiv_ty ~ignore_effects:true ~qvars_wild:true) sig1.concrete_tys sig2.concrete_tys in
+  (* if not equiv_ids then
+    print_endline ("\t[concrete_sig_equal] concrete_sig_equal: ids not equal: " ^ (Id.name sig1.id) ^ " vs " ^ (Id.name sig2.id));
+  if not equiv_tys then
+    print_endline ("\t[concrete_sig_equal] concrete_sig_equal: tys not equal: " ^ (Printing.list_to_string Printing.ty_to_string sig1.concrete_tys) ^ " vs " ^ (Printing.list_to_string Printing.ty_to_string sig2.concrete_tys));
+  if equiv_ids && equiv_tys then
+    print_endline ("\t[concrete_sig_equal] concrete_sig_equal: sigs are equal!"); *)
+  equiv_ids && equiv_tys
+  (* Id.equal sig1.id sig2.id &&
+  equiv_lists (equiv_ty ~ignore_effects:true ~qvars_wild:true) sig1.concrete_tys sig2.concrete_tys *)
+;;
+(* everything about an event and handler declaration *)
+type event_decl = {
+  id:id; 
+  params : params;
+  ecalls : concrete_sig list; (* calls seen so far *)
+}
+type event_map = event_decl IdMap.t
+
+
+let event_decl_equal (edecl1 : event_decl) (edecl2 : event_decl) = 
+  (* print_endline ("[event_decl_equal] comparing event decls: " ^ (Id.name edecl1.id) ^ " vs " ^ (Id.name edecl2.id)); *)
+  let equiv_ids = Id.equal edecl1.id edecl2.id in
+  let equiv_params = equiv_lists 
+    (fun (id1, ty1) (id2, ty2) -> Id.equal id1 id2 && equiv_ty ~ignore_effects:true ~qvars_wild:true ty1 ty2) 
+    edecl1.params 
+    edecl2.params in
+  (* let ecalls_len1 = List.length edecl1.ecalls in
+  let ecalls_len2 = List.length edecl2.ecalls in *)
+  (* print_endline ("\t[even_decl_equal] edecl1 has "^ (string_of_int ecalls_len1) ^ " calls, edecl2 has "^ (string_of_int ecalls_len2) ^ " calls"); *)
+  let equiv_ecalls = equiv_lists concrete_sig_equal edecl1.ecalls edecl2.ecalls in
+  (* if not equiv_ids then
+    print_endline ("[event_decl_equal] event_decl_equal: ids not equal: " ^ (Id.name edecl1.id) ^ " vs " ^ (Id.name edecl2.id));
+  if not equiv_params then
+    print_endline ("[event_decl_equal] event_decl_equal: params not equal: " ^ (Printing.list_to_string (fun (id, ty) -> "(" ^ (Id.name id) ^ ", " ^ (Printing.ty_to_string ty) ^ ")") edecl1.params) ^ " vs " ^ (Printing.list_to_string (fun (id, ty) -> "(" ^ (Id.name id) ^ ", " ^ (Printing.ty_to_string ty) ^ ")") edecl2.params));
+  if not equiv_ecalls then
+    print_endline ("[event_decl_equal] event_decl_equal: ecalls not equal"); *)
+  equiv_ids && equiv_params && equiv_ecalls
+  (* Id.equal edecl1.id edecl2.id &&
+  equiv_lists 
+    (fun (id1, ty1) (id2, ty2) -> Id.equal id1 id2 && equiv_ty ~ignore_effects:true ~qvars_wild:true ty1 ty2) 
+    edecl1.params 
+    edecl2.params 
+  && equiv_lists concrete_sig_equal edecl1.ecalls edecl2.ecalls *)
+;;
+
+(* Add an event call to the event declaration, if one with that 
+    type signature doesn't already exist.  *)
+let add_concrete_sig event_decl call_args : (id * event_decl) = 
+  (* first, check to see if a call with the type signature exists *)
+  let arg_tys = List.map (fun exp -> Option.get exp.ety) call_args in
+  let fst_matching_call_opt = List.find_opt 
+    (fun (call : concrete_sig) -> equiv_lists 
+      (equiv_ty ~ignore_effects:true) 
+      arg_tys 
+      call.concrete_tys)
+    event_decl.ecalls
+  in
+  match fst_matching_call_opt with
+  | Some call -> (call.id, event_decl) (* if it does, return the existing monomorphic id *)
+  | None -> (* if it doesn't, create a new monomorphic id and add the call to the event declaration *)
+    (* print_endline ("[event_ctor_replacer] adding new concrete instance for event "^ (Id.name event_decl.id) ^ " with arg types: " ^ (Printing.list_to_string Printing.ty_to_string arg_tys)); *)
+    let id' = Id.create ((Id.name (event_decl.id)) ^ "_" ^ string_of_int (List.length event_decl.ecalls)) in
+    let exp_to_rawty exp = (Option.get exp.ety) in
+    let concrete_tys = List.map exp_to_rawty call_args in 
+    let ecalls' = event_decl.ecalls@[{id=id'; concrete_tys}] in
+    id', {event_decl with ecalls = ecalls'}
+;;
+
+(* New main function *)
+let update_calls emap ds : event_decl IdMap.t * decls = 
+  (* use an object to visit DEvents and find all event decls *)
+  let obj = object (self)
+    inherit [_] s_map as super
+    val mutable event_map = IdMap.empty
+    method event_map = event_map
+    (* entry point *)
+    method process emap ds = 
+      event_map <- emap; (* reset context before running *)
+      self#visit_decls () ds;
+      
+    method! visit_DEvent () id x y z params = 
+      (* if the event has a polymorphic type 
+         in any of its arguments, add it to the list *)
+      (* only add if its not already there *)
+      if List.exists (fun (_, ty) -> is_polymorphic_ty ty) params then (
+        if IdMap.mem id event_map then(
+          (* print_endline ("[event_ctor_replacer] warning: duplicate event declaration for "^ (Id.name id) ^ " with polymorphic parameters. This may cause issues with monomorphization."); *)
+          ())
+        else
+        event_map <- IdMap.add id {id; params; ecalls=[]} event_map
+      );
+      super#visit_DEvent () id x y z params
+
+    method! visit_PCall _ pcall_arg = 
+      PCall(pcall_arg) (* need to skip manually because the arg is type event *)
+
+    method! visit_PGen _ pgen_arg = 
+      (* print_endline ("[event_ctor_replacer] visiting PGen with args: "^(Printing.exp_to_string pgen_arg)); *)
+      (* print_endline ("[event_ctor_replacer] pgen_arg type: "^(Option.get pgen_arg.ety |> Printing.ty_to_string));
+      (match pgen_arg.e, (Option.get pgen_arg.ety).raw_ty with 
+        | ECall(_), TEvent -> print_endline ("[event_ctor_replacer] pgen_arg is an ecall with type TEvent, so we should visit it...");
+        | _, TEvent -> print_endline ("[event_ctor_replacer] pgen_arg has type TEvent, but is not an ecall...");
+        | ECall(_), _ -> print_endline ("[event_ctor_replacer] pgen_arg is an ECall, but does not have type TEvent... ("^(Option.get pgen_arg.ety |> Printing.ty_to_string)^")");
+        | _, _ -> print_endline ("[event_ctor_replacer] pgen_arg is not an ECall and does not have type TEvent... ");
+      ); *)
+      let pgen_arg' = self#visit_exp () pgen_arg in
+      PGen(pgen_arg')
+
+
+    method! visit_exp _ exp =
+      (* transform event constructor calls to events in the list *)
+      let _ = match exp.ety with 
+        | Some ty -> ty
+        | None -> failwith ("[event_ctor_replacer] found expression without type annotation: "^(Printing.exp_to_string exp))
+      in
+      match exp.e, ((Option.get exp.ety) |> normalize_ty).raw_ty with 
+      (* event combinator *)
+      | ECall(event_cid, _, _), TEvent when Cid.equal_names event_cid (Cid.create ["Event"; "delay"]) -> 
+        super#visit_exp () exp (* continue to inner event *)
+      | ECall(event_cid, args, flag), TEvent -> 
+        (* check if it is a builtin event combinator, for which we recurse *)
+          (* print_endline ("[event_ctor_replacer] ECall event_cid = "^(Printing.cid_to_string event_cid));
+          print_endline ("[event_ctor_replacer] visiting ECall with args: "^(Printing.list_to_string Printing.exp_to_string args)); *)
+        let event_id = Cid.to_id event_cid in
+        (match IdMap.find_opt event_id event_map with
+          | Some edecl -> (* this is an event with a polymorphic argument. We need a monomorphic id *)
+            (* if the arguments themselves are polymorphic, it doesn't define a monomorphic call
+              and we will need to replace it with the appropriate monomorphic instance later *)
+            let args_are_polymorphic = List.exists (fun arg -> is_polymorphic_ty (Option.get arg.ety)) args in
+            if args_are_polymorphic then (
+              print_endline ("[event_ctor_replacer] arguments are polymorphic, so we will not replace this call with a monomorphic one...");
+              super#visit_exp () exp 
+            )
+            else (
+            (* print_endline ("[event_ctor_replacer] Found event constructor call for event "^ (Id.name event_id) ^ " with polymorphic params, replacing with monomorphic event constructor call..."); *)
+            let monomorphic_id, updated_edecl = add_concrete_sig edecl args in
+            let event_cid' = Cid.id monomorphic_id in
+            event_map <- IdMap.add event_id updated_edecl event_map; (* update the event declaration with the new call *)
+            let exp' = {exp with e=ECall(event_cid', args, flag)} in
+            (* print_endline ("[event_ctor_replacer] new ECall exp: "^(Printing.exp_to_string exp')); *)
+            super#visit_exp () exp' (* visit the new expression to find nested event constructor calls *)
+          )
+          | None -> (* this is not an event with a polymorphic argument, only need to recurse *)
+            super#visit_exp () exp
+        )
+      | _ -> super#visit_exp () exp (* super to skip / prevent infinite recursion *)    
+        
+  end in
+  let ds = obj#process emap ds in
+  obj#event_map, ds
+;;
+
+
+(* make a concrete version of an event decl, based on concrete_sig *)
+(* all arguments besides the last are data of the base polymorphic instance *)
+let concrete_event_decl decl _ num_opt esort specs params concrete_sig =
+  let params' = List.mapi (fun i (param_id, _) -> (param_id, List.nth concrete_sig.concrete_tys i)) params in
+  { decl with d = DEvent(concrete_sig.id, num_opt, esort, specs, params') }
+;;
+
+let concrete_event_decls decl id num_opt esort specs params concrete_sigs =
+  List.map (fun concrete_sig -> concrete_event_decl decl id num_opt esort specs params concrete_sig) concrete_sigs
+;;
+
+let concrete_handler_decl decl _ hsort (params, stmt) concrete_sig =
+  let params' = List.mapi (fun i (param_id, _) -> (param_id, List.nth concrete_sig.concrete_tys i)) params in
+  { decl with d = DHandler(concrete_sig.id, hsort, (params', stmt)) }
+;;
+let concrete_handler_decls decl id hsort (params, stmt) concrete_sigs =
+  List.map (fun concrete_sig -> concrete_handler_decl decl id hsort (params, stmt) concrete_sig) concrete_sigs
+;;
+
+let update_decls event_map ds = 
+  (* use an object to visit DEvents and DHandlers and replace with monomorphic ones according to the event map *)
+  let obj = object (self)
+    inherit [_] s_map as super
+    method process event_map ds = self#visit_decls event_map ds
+    method! visit_decls event_map decls = 
+      match decls with 
+      | [] -> []
+      | decl::decls -> (
+        (* visit rest (decl may be a module, and need to visit the rest) *)
+        let decl = self#visit_decl event_map decl in
+        let decls' = self#visit_decls event_map decls in
+        match decl.d with 
+        | DEvent(id, _,  esort, specs, params) -> (
+          match IdMap.find_opt id event_map with
+          | Some edecl -> (
+            let new_decls = concrete_event_decls decl id None esort specs params edecl.ecalls in
+            decl::new_decls@decls' (* leave the event here for now, for type inference *)
+          )
+          | None -> decl::decls'
+        )
+        | DHandler(id, hsort, (params, stmt)) -> (
+          match IdMap.find_opt id event_map with
+          | Some edecl -> ( (* edecls is all the info about this event *)
+            let new_decls = concrete_handler_decls decl id hsort (params, stmt) edecl.ecalls in
+            new_decls@decls'
+          )
+          | None -> decl::decls'
+        )
+        | _ -> decl::decls'
+      )
+  end in
+  obj#process event_map ds
+;;
+
+let delete_polymorphic_event_decls ds = 
+  (* use an object to visit DEvents and delete those with polymorphic parameters *)
+  let obj = object (self)
+    inherit [_] s_map as super
+    method process ds = self#visit_decls () ds
+    method! visit_decls _ decls = 
+      match decls with 
+      | [] -> []
+      | decl::decls -> (
+        let decls' = self#visit_decls () decls in
+        match decl.d with 
+        | DEvent(_, _,  _, _, params) -> 
+          if List.exists (fun (_, ty) -> is_polymorphic_ty ty) params 
+          then decls'       (* delete this declaration *)
+          else decl::decls' (* keep this declaration *)
+        | _ -> decl::decls'
+      )
+  end in
+  obj#process ds
+
+(* ============================================================ *)
+(*  Parser monomorphization                                      *)
+(*                                                               *)
+(*  Parsers can declare polymorphic parameters (e.g., `auto`)    *)
+(*  the same way events can, and they can be invoked from        *)
+(*  other parsers via `PCall`. Because parsers are non-recursive *)
+(*  and every control-flow path ends in `generate` or `drop`,    *)
+(*  we can monomorphize them by the same scheme used for events: *)
+(*  for each PCall to a polymorphic parser, materialize a        *)
+(*  concrete copy keyed by the arg-type signature.               *)
+(*                                                               *)
+(*  This must run *before* event monomorphization, so that by    *)
+(*  the time the event pass scans `generate` statements inside   *)
+(*  duplicated parser bodies, those statements have concrete     *)
+(*  argument types.                                              *)
+(* ============================================================ *)
+
+type parser_decl = {
+  pid : id;
+  pparams : params;
+  pcalls : concrete_sig list;
+  (* prefix length of pcalls that has already been materialized as DParser
+     decls in the program. Each fixpoint iteration emits only the suffix
+     past this index, then bumps it. *)
+  nemitted : int;
+}
+type parser_map = parser_decl IdMap.t
+
+(* Convergence check: ignores nemitted, since that's bookkeeping. *)
+let parser_pcalls_equal (p1 : parser_decl) (p2 : parser_decl) =
+  Id.equal p1.pid p2.pid
+  && equiv_lists concrete_sig_equal p1.pcalls p2.pcalls
+;;
+
+(* Look up or create a concrete instance of a polymorphic parser for the
+   given call's arg types. *)
+let add_concrete_parser_sig parser_decl call_args : id * parser_decl =
+  let arg_tys = List.map (fun exp -> Option.get exp.ety) call_args in
+  let fst_matching_call_opt =
+    List.find_opt
+      (fun (call : concrete_sig) ->
+        equiv_lists (equiv_ty ~ignore_effects:true) arg_tys call.concrete_tys)
+      parser_decl.pcalls
+  in
+  match fst_matching_call_opt with
+  | Some call -> call.id, parser_decl
+  | None ->
+    let id' =
+      Id.create
+        (Id.name parser_decl.pid
+         ^ "_"
+         ^ string_of_int (List.length parser_decl.pcalls))
+    in
+    let concrete_tys = List.map (fun exp -> Option.get exp.ety) call_args in
+    let pcalls' = parser_decl.pcalls @ [{ id = id'; concrete_tys }] in
+    id', { parser_decl with pcalls = pcalls' }
+;;
+
+(* Walk the program; for each PCall to a polymorphic parser whose call-site
+   args are concrete, rewrite the call's parser id to a (possibly new)
+   monomorphic instance and record that instance in the parser_map. *)
+let update_parser_calls pmap ds : parser_map * decls =
+  let obj =
+    object (self)
+      inherit [_] s_map as super
+      val mutable parser_map = IdMap.empty
+      method parser_map = parser_map
+
+      method process pmap ds =
+        parser_map <- pmap;
+        self#visit_decls () ds
+
+      method! visit_DParser () id params block =
+        if List.exists (fun (_, ty) -> is_polymorphic_ty ty) params then begin
+          if not (IdMap.mem id parser_map) then
+            parser_map
+              <- IdMap.add id { pid = id; pparams = params; pcalls = []; nemitted = 0 } parser_map
+        end;
+        super#visit_DParser () id params block
+
+      method! visit_PCall () pcall_arg =
+        match pcall_arg.e with
+        | ECall (parser_cid, args, flag) ->
+          let parser_id = Cid.to_id parser_cid in
+          (match IdMap.find_opt parser_id parser_map with
+           | Some pdecl ->
+             let args_are_polymorphic =
+               List.exists
+                 (fun arg -> is_polymorphic_ty (Option.get arg.ety))
+                 args
+             in
+             if args_are_polymorphic
+             then super#visit_PCall () pcall_arg
+             else begin
+               let monomorphic_id, updated_pdecl =
+                 add_concrete_parser_sig pdecl args
+               in
+               parser_map <- IdMap.add parser_id updated_pdecl parser_map;
+               let pcall_arg' =
+                 { pcall_arg with e = ECall (Cid.id monomorphic_id, args, flag) }
+               in
+               super#visit_PCall () pcall_arg'
+             end
+           | None -> super#visit_PCall () pcall_arg)
+        | _ -> super#visit_PCall () pcall_arg
+    end
+  in
+  let ds = obj#process pmap ds in
+  obj#parser_map, ds
+;;
+
+(* Build a concrete copy of a polymorphic parser decl. Param identifiers are
+   preserved; only their types are replaced with the concrete sig types. The
+   body is left untouched and will be re-typed against the new params. *)
+let concrete_parser_decl decl params block (cs : concrete_sig) =
+  let params' =
+    List.mapi
+      (fun i (param_id, _) -> param_id, List.nth cs.concrete_tys i)
+      params
+  in
+  { decl with d = DParser (cs.id, params', block) }
+;;
+
+let concrete_parser_decls decl params block concrete_sigs =
+  List.map (fun cs -> concrete_parser_decl decl params block cs) concrete_sigs
+;;
+
+(* Emit one DParser per concrete sig collected so far, but skip any sig that
+   was already emitted in a prior fixpoint iteration (tracked via nemitted).
+   The original polymorphic decl is left in place until after re-typing so
+   the typer can still find it. *)
+let update_parser_decls parser_map ds =
+  let obj =
+    object (self)
+      inherit [_] s_map as super
+      method process pmap ds = self#visit_decls pmap ds
+
+      method! visit_decls pmap decls =
+        match decls with
+        | [] -> []
+        | decl :: rest ->
+          let decl = self#visit_decl pmap decl in
+          let rest' = self#visit_decls pmap rest in
+          (match decl.d with
+           | DParser (id, params, block) ->
+             (match IdMap.find_opt id pmap with
+              | Some pdecl ->
+                let pending = BatList.drop pdecl.nemitted pdecl.pcalls in
+                let new_decls =
+                  concrete_parser_decls decl params block pending
+                in
+                (decl :: new_decls) @ rest'
+              | None -> decl :: rest')
+           | _ -> decl :: rest')
+    end
+  in
+  obj#process parser_map ds
+;;
+
+(* Mark every pcall in the map as emitted. Called after update_parser_decls
+   so the next fixpoint iteration won't re-emit the same decls. *)
+let mark_emitted (pmap : parser_map) : parser_map =
+  IdMap.map
+    (fun pdecl -> { pdecl with nemitted = List.length pdecl.pcalls })
+    pmap
+;;
+
+let delete_polymorphic_parser_decls ds =
+  let obj =
+    object (self)
+      inherit [_] s_map as super
+      method process ds = self#visit_decls () ds
+
+      method! visit_decls _ decls =
+        match decls with
+        | [] -> []
+        | decl :: rest ->
+          let rest' = self#visit_decls () rest in
+          (match decl.d with
+           | DParser (_, params, _) ->
+             if List.exists (fun (_, ty) -> is_polymorphic_ty ty) params
+             then rest'
+             else decl :: rest'
+           | _ -> decl :: rest')
+    end
+  in
+  obj#process ds
+;;
+
+(* Run parser monomorphization to a fixpoint. Each iteration:
+     1. update_parser_calls: walk the program, rewrite PCalls to polymorphic
+        parsers whose call-site args are now concrete, recording the new
+        concrete sigs in pmap.
+     2. If pcalls didn't grow, we've converged.
+     3. Otherwise emit DParsers for the new sigs (update_parser_decls skips
+        sigs already emitted in prior iterations), retype, and loop.
+   Termination is bounded by the parser call-chain depth, since parsers are
+   non-recursive. The max_iters cap is a safety net. *)
+let monomorphize_parsers builtin_tys ds =
+  let max_iters = 100 in
+  let rec loop pmap ds iter =
+    if iter > max_iters
+    then
+      failwith
+        (Printf.sprintf
+           "[MonomorphicEventArgs] parser monomorphization did not converge in \
+            %d iterations"
+           max_iters);
+    let pmap', ds = update_parser_calls pmap ds in
+    if IdMap.equal parser_pcalls_equal pmap pmap'
+    then ds
+    else begin
+      let ds = update_parser_decls pmap' ds in
+      let pmap' = mark_emitted pmap' in
+      let ds = RefreshTypes.refresh_prog ds in
+      let ds = Typer.infer_prog builtin_tys ds in
+      loop pmap' ds (iter + 1)
+    end
+  in
+  let ds = loop IdMap.empty ds 1 in
+  let ds = delete_polymorphic_parser_decls ds in
+  let ds = RefreshTypes.refresh_prog ds in
+  let ds = Typer.infer_prog builtin_tys ds in
+  ds
+;;
+
+let eliminate_prog builtin_tys ds =
+  let ds = RefreshTypes.refresh_prog ds in
+  let ds = Typer.infer_prog builtin_tys ds in
+
+  (* monomorphize parsers first, so that any polymorphic events referenced by
+     parser bodies get concrete arg types in the duplicated parser copies *)
+  let ds = monomorphize_parsers builtin_tys ds in
+
+  (* collect monomorphic calls (and replace their event names) *)
+  let emap, ds = update_calls IdMap.empty ds in
+  (* replace polymorphic declarations with monomorphic copies *)
+  let ds = update_decls emap ds in
+
+  (* type check to infer all the polymorphic args inside of event calls  *)
+  let ds = RefreshTypes.refresh_prog ds in
+  let ds = Typer.infer_prog builtin_tys ds in
+
+  (* run the call collector / updator again, for all the calls in the monomorphic
+     generated handlers, which are no longer polymorphic *)
+  (* print_endline "------ Monomorphization second pass -------"; *)
+  let emap', ds = update_calls emap ds in
+  (* For now, only support cases where the second pass does not identify new 
+     monomorphic instances. TODO: find and think through edge case where that may happen. *)
+  (* print_endline "---------- current prog -----------"; *)
+  (* Printing.decls_to_string ds |> print_endline; *)
+  (* print_endline "---------- current prog -----------"; *)
+  let no_changes = IdMap.equal event_decl_equal emap emap' in
+  if not no_changes then
+    failwith "[MonomorphicEventArgs] elimination of polymorphic event encountered\
+    transitive polymorphism that requires more than 2 passes. This is not yet supported.";
+  ignore emap';
+
+    (* print_endline "-------- program at debug point --------"; *)
+  (* Printing.decls_to_string ds |> print_endline; *)
+  (* print_endline "-------- program at debug point --------"; *)
+
+  (* delete the polymorphic event declarationss, which were left for type checking *)
+  let ds = delete_polymorphic_event_decls ds in
+
+  (* reset event numbers *)
+  let ds = EventFormat.set_event_nums ds in 
+
+  (* ensure all names are unique (TODO: should be taken care of inside the event / handler copying function) *)
+  let renaming, ds = Renaming.rename ds in
+  let ds = RefreshTypes.refresh_prog ds in
+  let ds = Typer.infer_prog builtin_tys ds in
+  let ds = RefreshTypes.refresh_prog ds in
+
+  (* print_endline "---------- Output decls -----------";
+  Printing.decls_to_string ds |> print_endline;
+  print_endline "---------- Output decls -----------"; *)
+  (* exit 1; *)
+  renaming, ds
+;;
+
diff --git a/src/lib/frontend/transformations/RefreshTypes.ml b/src/lib/frontend/transformations/RefreshTypes.ml
new file mode 100644
index 00000000..b3018383
--- /dev/null
+++ b/src/lib/frontend/transformations/RefreshTypes.ml
@@ -0,0 +1,37 @@
+(* Reset effect annotations on types inside handler and function bodies.
+   This is a temporary patch / hack for type checking to work in 
+   certain phases of the frontend (from TableInlining to MonomorphicEventArgs),
+   After a typing pass, types in handler bodies carry resolved effects with
+   specific index variable IDs. These conflict with fresh variables created
+   by a subsequent typing pass. This pass replaces those teffect fields with
+   fresh effect variables, allowing a subsequent type checker to re-derive
+   effects from program structure.
+
+   Top-level declarations (globals, events, user types) are left untouched
+   since their effects carry meaningful semantic information (e.g., global
+   ordering). *)
+open Syntax
+open TyperUtil
+
+let effect_refresher =
+  object
+    inherit [_] s_map as super
+
+    method! visit_ty () ty =
+      { (super#visit_ty () ty) with teffect = fresh_effect () }
+  end
+;;
+
+let refresh_prog ds =
+  List.map
+    (fun d ->
+      match d.d with
+      | DHandler (id, sort, body) ->
+        let body' = effect_refresher#visit_body () body in
+        { d with d = DHandler (id, sort, body') }
+      | DFun (id, rty, cs, body) ->
+        let body' = effect_refresher#visit_body () body in
+        { d with d = DFun (id, rty, cs, body') }
+      | _ -> d)
+    ds
+;;
\ No newline at end of file
diff --git a/src/lib/frontend/transformations/TableInlining.ml b/src/lib/frontend/transformations/TableInlining.ml
index 0b84dcc4..3b7a66db 100644
--- a/src/lib/frontend/transformations/TableInlining.ml
+++ b/src/lib/frontend/transformations/TableInlining.ml
@@ -55,6 +55,9 @@ let rec eliminate_exp e =
   | EProj (e1, str) ->
     let stmt, e1' = eliminate_exp e1 in
     stmt, { e with e = EProj (e1', str) }
+  | EGet (e1, str) ->
+    let stmt, e1' = eliminate_exp e1 in
+    stmt, { e with e = EGet (e1', str) }
   | EVector es ->
     let stmt, es' = eliminate_exps es in
     stmt, { e with e = EVector es' }
diff --git a/src/lib/frontend/typing/Typer.ml b/src/lib/frontend/typing/Typer.ml
index b78f7c15..bb17eea7 100644
--- a/src/lib/frontend/typing/Typer.ml
+++ b/src/lib/frontend/typing/Typer.ml
@@ -261,18 +261,25 @@ let rec infer_exp (env : env) (e : exp) : env * exp =
           (* This commented out code was a workaround to get unification to work 
              for tuple expressions that contained elements from other tuples. 
              The problem was that: tup foo = (bar.1, bar.2)  failed to unify, 
-             because it tried to unify the effect of foo.0 with bar.1, and there 
-             so it ended up trying to unify FSucc(FProj()) with FProj()
-            The solution was to add a case in TyperUnify.try_unify_effect: 
+             because it tried to unify the effect of foo.0 with bar.1, causing 
+             it to attempt unification of FSucc(FProj()) with FProj(). 
+             The workaround is to use the effect of the gotten index, rather 
+             than the index written to. That is acceptable because 
+             it is illegal to dynamically construct tuples of global types, 
+             which are the only tuples with effects that matter. 
+               
+            An attempted alternative solution was to add a case in TyperUnify.try_unify_effect: 
                 | FProj(FVar(tqv)), eff | eff, FProj(FVar(tqv)) -> ...
-            This solves the problem because in such a case, one of the sides 
+            I thought this solved the problem because in such a case, one of the sides 
             is going to be a variable. And it is safe because projecting 
-            does not have an effect itself. *)
-          (* let expected = match (e'.e) with 
+            does not have an effect itself. 
+            However, that change did not solve the problem, so the workaround remains. 
+            *)
+          let expected = match (e'.e) with 
             | EOp(TGet(_, idx), _) -> wrap_effect tuple_eff [None, 0; None, idx]
             | _ -> wrap_effect tuple_eff [None, 0; None, i] 
-          in *)
-          let expected = wrap_effect tuple_eff [None, 0; None, i] in
+          in
+          (* let expected = wrap_effect tuple_eff [None, 0; None, i] in *)
           let derived = (Option.get e'.ety).teffect in           
           unify_effect e.espan expected derived
         )
@@ -377,6 +384,39 @@ let rec infer_exp (env : env) (e : exp) : env * exp =
         }
     in
     env, { e with e = EIndex (inf_e1, idx); ety }
+  | EGet(e1, idx) -> (
+    (* 4/2026 -- preliminary rule based on TGet and EIndex *)
+    let i =
+      match idx with
+      | IConst i -> i
+      | _ ->
+        error_sp e.espan
+        @@ "Index "
+        ^ size_to_string idx
+        ^ " is neither a variable nor a constant."
+    in
+    (* infer tuple type from expression *)
+    let env, inf_e1, inf_ety = infer_exp env e1 |> textract in
+    (* there is no expected type for a tuple *)
+    let size = match inf_ety.raw_ty with 
+      | TTuple(inf_rtys) -> List.length inf_rtys
+      | _ -> failwith "Type error: could not resolve tuple type length"
+    in
+    let expected_rtys = List.init size (fun _ -> (fresh_type ()).raw_ty) in
+    let expected_ty = mk_ty @@ TTuple expected_rtys in
+    unify_ty e.espan inf_ety expected_ty; (* expected type of the tuple *)
+    if i >= size
+      then (
+        let err_str = "Tuple index "^(string_of_int i)^" is out of bounds ("^(string_of_int size)^")" in
+        error_sp e.espan err_str
+      );
+    let ety = Some(
+      ty_eff
+        (List.nth expected_rtys i)
+        (wrap_effect inf_ety.teffect [None, 0; None, i])
+    ) in
+    env, {e with e = EGet(inf_e1, idx); ety}
+  )    
   | EComp (e1, idx, sz) ->
     validate_size e.espan env sz;
     let renamed_idx = Id.freshen idx in
@@ -1263,7 +1303,7 @@ let retrieve_constraints env span id params =
             }
       } ->
     let maps = fresh_maps () in
-    let params2 = List.map (instantiator#visit_ty maps) arg_tys in
+    let params2 = List.map (instantiator#visit_ty maps) arg_tys in (* instantiated event types *)
     let constraints = List.map (instantiator#visit_constr maps) constraints in
     let _ =
       (* FIXME: This isn't quite sufficient -- it won't catch e.g.
@@ -1338,6 +1378,7 @@ let rec infer_parser_step env (step, span) =
     (match exp.e with
      | ECall (cid, args, _) ->
        let params = lookup_parser span env cid in
+       let params = instantiator#visit_params (fresh_maps ()) params in
        let _, inf_args = infer_exps env args in
        List.iter2
          (fun (_, pty) arg ->
@@ -1347,7 +1388,8 @@ let rec infer_parser_step env (step, span) =
        let exp' = call_sp cid inf_args span in
        let exp' = { exp' with ety = Some (mk_ty TEvent) } in
        PCall exp', span
-     | _ ->
+
+      | _ ->
        error_sp
          span
          "Parser bodies can only read, skip, generate, match, or call another \
@@ -1446,24 +1488,23 @@ let rec infer_declaration
         (Id.name id)
         (ty_to_string (lookup_var d.dspan env (Cid.id id))); *)
       env, effect_count, DEvent (id, annot, sort, constr_specs, params)
+
     | DHandler (id, s, body) ->
+      (* Handlers with polymorphic arguments should not constrain those
+         arguments in the body. To check this, we make a generalized
+         copy of the params at the start. *)
+      let generalized_params_start = generalizer#visit_params () (fst body) in
+      (* Re-generalize the entire body to clean up any shared TVar refs
+         that were mutated by the params generalization above, then
+         re-instantiate with a single fresh_maps so params and body
+         get consistent fresh TVars. *)
+      let generalized_body = generalizer#visit_body () body in
+      let body = instantiator#visit_body (fresh_maps ()) generalized_body in
+
       enter_level ();
       let constraints = retrieve_constraints env d.dspan id (fst body) in
-      (* LEFT OFF HERE. Unify handler and event types. *)
-      (* 1. look the type of the event's constructor (follow pattern from EVar inference) *)
-      (* let inst t = instantiator#visit_ty (fresh_maps ()) t in *)
-      (* let inf_ev_ctor_ty = lookup_var d.dspan env (Cid.id id) |> inst in *)
-      (* 2. unify the event's parameters with the handler's parameters *)
-      (* let _ =   match inf_ev_ctor_ty.raw_ty with 
-        | TFun fty -> (
-          match ret_ty.raw_ty with
-        )
-        | _ -> error_sp d.dspan "Error: found a variable with the same name as this handler"
-      in  *)
-      (* match inf_ev_ctor_ty with  *)
 
-
-      (* unify_ty d.dspan ty inf_ety; *)
+      (* type the handler body *)
       let _, inf_body =
         let starting_env =
           { env with current_effect = FZero; constraints }
@@ -1473,11 +1514,50 @@ let rec infer_declaration
         infer_body starting_env body
       in
       leave_level ();
-      let inf_body = generalizer#visit_body () inf_body in
 
+      (* generalize the body *)
+      let inf_body = generalizer#visit_body () inf_body in
 
+      (* check that no polymorphic param types have been constrained by inference *)
+      let polymorphic_ty_preserved old_rty new_rty = 
+        equiv_ty ~ignore_effects:true ~qvars_wild:false ~ignore_qvar_ids:true old_rty new_rty 
+      in
+      List.iter2 
+        (fun (old_id, old_ty) (_, new_ty) -> 
+          if not (polymorphic_ty_preserved old_ty new_ty)
+          then 
+            (
+              let err_str = Printf.sprintf 
+                "Parameter %s of handler %s was declared as polymorphic (%s), but was \n\
+                used as a type %s in the handler body. \n\
+                Please declare %s parameter with a concrete type instead."
+                (Id.name old_id) (Id.name id) (ty_to_string old_ty) (ty_to_string new_ty) (Id.name old_id)
+              in
+            error_sp old_ty.tspan @@ err_str)
+        )
+        generalized_params_start
+        (fst inf_body);
 
+      (* return the handler with the typed body *)
       env, effect_count, DHandler (id, s, inf_body)
+    | DParser (id, params, parser) ->
+      enter_level ();
+      (* a parser may branch on the ingress port *)
+      let ingress_port_param = (Builtins.ingr_port_id, builtin_tys.ingr_port_ty) in
+      let parser_env =
+        add_locals env (ingress_port_param::params) 
+        |> define_parser Builtins.lucid_parse_id [(Id.create "pkt", ty TBitstring)]
+      in
+      
+      let inf_parser = infer_parser_block parser_env parser in
+      leave_level ();
+
+      let inf_params = generalizer#visit_params () params in
+      let inf_parser = generalizer#visit_parser_block () inf_parser in
+
+      let env = define_parser id params env in
+      env, effect_count, DParser (id, inf_params, inf_parser)
+
     | DFun (id, ret_ty, constr_specs, body) ->
       (* a function declaration needs to have all the 
          local builtins available to it as well. *)
@@ -1531,6 +1611,7 @@ let rec infer_declaration
         @@ "Function "
         ^ Id.name id
         ^ " violates ordering constraints";
+      (* add the function's type to the environment for later use. *)
       let fty : func_ty =
         { arg_tys = List.map (fun (_, ty) -> ty) (fst inf_body)
         ; ret_ty
@@ -1540,10 +1621,11 @@ let rec infer_declaration
         }
         |> generalizer#visit_func_ty ()
       in
-      let inf_body = generalizer#visit_body () inf_body in
-      (* add the function's type to the environment for later use. *)
       let env = define_const id (mk_ty @@ TFun fty) env in
+      (* generalize the function's body *)
+      let inf_body = generalizer#visit_body () inf_body in
       env, effect_count, DFun (id, ret_ty, constr_specs, inf_body)
+
     | DMemop (id, params, memop_body) ->
       enter_level ();
       let inf_body = infer_memop env params memop_body in
@@ -1723,20 +1805,7 @@ let rec infer_declaration
       ( env
       , effect_count
       , DActionConstr (id, ret_ty, const_params, (params, inf_action_body)) )
-    | DParser (id, params, parser) ->
-      enter_level ();
-      (* a parser may branch on the ingress port *)
-      let ingress_port_param = (Builtins.ingr_port_id, builtin_tys.ingr_port_ty) in
-      let parser_env =
-        add_locals env (ingress_port_param::params) 
-        |> define_parser Builtins.lucid_parse_id [(Id.create "pkt", ty TBitstring)]
-      in
-      
-      let inf_parser = infer_parser_block parser_env parser in
-      leave_level (); (* bug fix: parser never left level *)
-       
-      let env = define_parser id params env in
-      env, effect_count, DParser (id, params, inf_parser)
+
   in
   let new_d = { d with d = new_d } in
   Wellformed.check_qvars new_d;
diff --git a/src/lib/frontend/typing/TyperInstGen.ml b/src/lib/frontend/typing/TyperInstGen.ml
index f87fbfb9..68011e3f 100644
--- a/src/lib/frontend/typing/TyperInstGen.ml
+++ b/src/lib/frontend/typing/TyperInstGen.ml
@@ -102,7 +102,7 @@ let rec instantiate_prog ds =
         match d.d with
         (* No point instantiating if there aren't any things to unify
            the sub-parts with. *)
-        | DUserTy _ | DExtern _ | DSymbolic _ | DSize _ | DEvent _ -> d
+        | DUserTy _ | DExtern _ | DSymbolic _ | DSize _  -> d | DEvent _ -> d
         (* For modules, don't instantiate the inferface, for the same reason *)
         | DModule (id, intf, ds) ->
           leave_level ();
diff --git a/src/lib/midend/transformations/SyntaxToCore.ml b/src/lib/midend/transformations/SyntaxToCore.ml
index f4e2da5a..47901ef8 100644
--- a/src/lib/midend/transformations/SyntaxToCore.ml
+++ b/src/lib/midend/transformations/SyntaxToCore.ml
@@ -196,6 +196,7 @@ and translate_exp (e : S.exp) : C.exp =
     | S.EFlood e -> C.EFlood (translate_exp e)
     | S.ERecord(fields) -> C.ERecord (List.map (fun (id, e) -> (Id.create id), translate_exp e) fields)
     | S.EProj(e, id) -> C.EProj (translate_exp e, Id.create id)
+    | S.EGet(_, _) -> S.error "[translate_exp] tuples should be eliminated in frontend"
     | ETuple exps -> C.ETuple(List.map translate_exp exps)
     | ESizeCast _
     | EStmt _