diff --git a/document/core/util/macros.def b/document/core/util/macros.def
index 35413fb95..8676c91fe 100644
--- a/document/core/util/macros.def
+++ b/document/core/util/macros.def
@@ -239,6 +239,7 @@
 .. |NULL| mathdef:: \xref{syntax/types}{syntax-reftype}{\K{null}}
 
 .. |EXACT| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{exact}}
+.. |INEXACT| mathdef:: {}
 .. |ANY| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{any}}
 .. |EQT| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{eq}}
 .. |I31| mathdef:: \xref{syntax/types}{syntax-heaptype}{\K{i\scriptstyle31}}
@@ -309,6 +310,7 @@
 .. |subtype| mathdef:: \xref{syntax/types}{syntax-subtype}{\X{subtype}}
 .. |rectype| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{rectype}}
 .. |deftype| mathdef:: \xref{valid/conventions}{syntax-deftype}{\X{deftype}}
+.. |exact| mathdef:: \X{exact}
 
 .. |globaltype| mathdef:: \xref{syntax/types}{syntax-globaltype}{\X{globaltype}}
 .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}}
@@ -349,6 +351,7 @@
 .. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}}
 
 .. |unpack| mathdef:: \xref{syntax/types}{aux-unpack}{\F{unpack}}
+.. |exactheaptype| mathdef:: \F{exactheaptype}
 
 .. |funcsxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}}
 .. |tablesxt| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}}
diff --git a/specification/wasm-latest/1.2-syntax.types.spectec b/specification/wasm-latest/1.2-syntax.types.spectec
index 25990998e..0502851e4 100644
--- a/specification/wasm-latest/1.2-syntax.types.spectec
+++ b/specification/wasm-latest/1.2-syntax.types.spectec
@@ -7,6 +7,9 @@
 ;; TODO(3, rossberg): add ability to do this inline
 syntax null hint(show NULL) hint(macro "%" "%") = NULL
 
+syntax exact hint(desc "exactness") =
+  | EXACT | INEXACT
+
 syntax addrtype hint(desc "address type") =
   | I32 | I64
 
@@ -32,6 +35,8 @@ syntax rectype hint(desc "recursive type")  ;; forward decl
 syntax deftype hint(desc "defined type") =
   | _DEF rectype n hint(show %.%)
 
+syntax exactdeftype hint(show (exact deftype)) = exact deftype
+
 syntax typeuse/syn hint(desc "type use") =
   | _IDX typeidx | ...
 syntax typeuse/sem =
@@ -85,6 +90,12 @@ def $NULLEXNREF  = (REF NULL NOEXN)
 def $NULLEXTERNREF = (REF NULL NOEXTERN)
 
 
+def $exactheaptype(exact, typeuse) : heaptype
+
+def $exactheaptype(EXACT, typeuse) = EXACT typeuse
+def $exactheaptype(INEXACT, typeuse) = typeuse
+
+
 ;; Packed types
 
 syntax packtype hint(desc "packed type") = I8 | I16
@@ -141,7 +152,7 @@ syntax datatype hint(desc "data type") = OK hint(macro "%data")
 syntax elemtype hint(desc "element type") = reftype
 
 syntax externtype hint(desc "external type") hint(macro "%" "XT%") =
-  | TAG tagtype | GLOBAL globaltype | MEM memtype | TABLE tabletype | FUNC typeuse
+  | TAG tagtype | GLOBAL globaltype | MEM memtype | TABLE tabletype | FUNC exact typeuse
 
 syntax moduletype hint(desc "module type") =
   externtype* -> externtype* hint(macro "toM")
@@ -156,6 +167,7 @@ var at : addrtype
 ;; var bt : blocktype  ;; defined below
 var ct : comptype
 var dt : deftype
+var edt : exactdeftype
 var et : elemtype
 var ft : fieldtype
 var gt : globaltype
@@ -315,7 +327,7 @@ def $tagsxt(externtype*) : tagtype*        hint(show $tags(%))    hint(macro "ta
 def $globalsxt(externtype*) : globaltype*  hint(show $globals(%)) hint(macro "globalsxt")
 def $memsxt(externtype*) : memtype*        hint(show $mems(%))    hint(macro "memsxt")
 def $tablesxt(externtype*) : tabletype*    hint(show $tables(%))  hint(macro "tablesxt")
-def $funcsxt(externtype*) : deftype*       hint(show $funcs(%))   hint(macro "funcsxt")
+def $funcsxt(externtype*) : exactdeftype*  hint(show $funcs(%))   hint(macro "funcsxt")
 
 def $tagsxt(eps) = eps
 def $tagsxt((TAG jt) xt*) = jt $tagsxt(xt*)
@@ -334,7 +346,7 @@ def $tablesxt((TABLE tt) xt*) = tt $tablesxt(xt*)
 def $tablesxt(externtype xt*) = $tablesxt(xt*)  -- otherwise
 
 def $funcsxt(eps) = eps
-def $funcsxt((FUNC dt) xt*) = dt $funcsxt(xt*)
+def $funcsxt((FUNC exact dt) xt*) = (exact dt) $funcsxt(xt*)
 def $funcsxt(externtype xt*) = $funcsxt(xt*)  -- otherwise
 
 
@@ -436,7 +448,7 @@ def $subst_externtype((TAG jt), tv*, tu*) = TAG $subst_tagtype(jt, tv*, tu*)
 def $subst_externtype((GLOBAL gt), tv*, tu*) = GLOBAL $subst_globaltype(gt, tv*, tu*)
 def $subst_externtype((TABLE tt), tv*, tu*) = TABLE $subst_tabletype(tt, tv*, tu*)
 def $subst_externtype((MEM mt), tv*, tu*) = MEM $subst_memtype(mt, tv*, tu*)
-def $subst_externtype((FUNC dt), tv*, tu*) = FUNC $subst_deftype(dt, tv*, tu*)
+def $subst_externtype((FUNC exact dt), tv*, tu*) = FUNC exact $subst_deftype(dt, tv*, tu*)
 
 def $subst_moduletype(xt_1* -> xt_2*, tv*, tu*) = $subst_externtype(xt_1, tv*, tu*)* -> $subst_externtype(xt_2, tv*, tu*)*
 
@@ -598,7 +610,7 @@ def $free_externtype(TAG tagtype) = $free_tagtype(tagtype)
 def $free_externtype(GLOBAL globaltype) = $free_globaltype(globaltype)
 def $free_externtype(MEM memtype) = $free_memtype(memtype)
 def $free_externtype(TABLE tabletype) = $free_tabletype(tabletype)
-def $free_externtype(FUNC typeuse) = $free_typeuse(typeuse)
+def $free_externtype(FUNC exact typeuse) = $free_typeuse(typeuse)
 
 def $free_moduletype(externtype_1* -> externtype_2*) =
   $free_list($free_externtype(externtype_1)*) ++
diff --git a/specification/wasm-latest/2.0-validation.contexts.spectec b/specification/wasm-latest/2.0-validation.contexts.spectec
index e9205fa2b..a48d50338 100644
--- a/specification/wasm-latest/2.0-validation.contexts.spectec
+++ b/specification/wasm-latest/2.0-validation.contexts.spectec
@@ -28,7 +28,7 @@ syntax context hint(desc "context") hint(macro "%" "C%") =
     GLOBALS globaltype*     hint(desc "global"),
     MEMS memtype*           hint(desc "memory"),
     TABLES tabletype*       hint(desc "table"),
-    FUNCS deftype*          hint(desc "function"),
+    FUNCS exactdeftype*     hint(desc "function"),
     DATAS datatype*         hint(desc "data segment"),
     ELEMS elemtype*         hint(desc "element segment"),
     LOCALS localtype*       hint(desc "local"),
diff --git a/specification/wasm-latest/2.1-validation.types.spectec b/specification/wasm-latest/2.1-validation.types.spectec
index ddb81eb2f..c1089a135 100644
--- a/specification/wasm-latest/2.1-validation.types.spectec
+++ b/specification/wasm-latest/2.1-validation.types.spectec
@@ -265,6 +265,6 @@ rule Externtype_ok/table:
   -- Tabletype_ok: C |- tabletype : OK
 
 rule Externtype_ok/func:
-  C |- FUNC typeuse : OK
+  C |- FUNC exact typeuse : OK
   -- Typeuse_ok: C |- typeuse : OK
   -- Expand_use: typeuse ~~_C $($(FUNC t_1* -> t_2*))
diff --git a/specification/wasm-latest/2.2-validation.subtyping.spectec b/specification/wasm-latest/2.2-validation.subtyping.spectec
index 9bd60602f..3c7fd4bf2 100644
--- a/specification/wasm-latest/2.2-validation.subtyping.spectec
+++ b/specification/wasm-latest/2.2-validation.subtyping.spectec
@@ -260,5 +260,5 @@ rule Externtype_sub/table:
   -- Tabletype_sub: C |- tabletype_1 <: tabletype_2
 
 rule Externtype_sub/func:
-  C |- FUNC deftype_1 <: FUNC deftype_2
-  -- Deftype_sub: C |- deftype_1 <: deftype_2
+  C |- FUNC exact_1 deftype_1 <: FUNC exact_2 deftype_2
+  -- Heaptype_sub: C |- $exactheaptype(exact_1, deftype_1) <: $exactheaptype(exact_2, deftype_2)
diff --git a/specification/wasm-latest/2.3-validation.instructions.spectec b/specification/wasm-latest/2.3-validation.instructions.spectec
index 2e042e76f..a41160bf6 100644
--- a/specification/wasm-latest/2.3-validation.instructions.spectec
+++ b/specification/wasm-latest/2.3-validation.instructions.spectec
@@ -120,7 +120,8 @@ rule Instr_ok/br_on_cast_fail:
 
 rule Instr_ok/call:
   C |- CALL x : t_1* -> t_2*
-  -- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2*
+  -- if C.FUNCS[x] = exact dt
+  -- Expand: dt ~~ FUNC t_1* -> t_2*
 
 rule Instr_ok/call_ref:
   C |- CALL_REF (_IDX x) : t_1* (REF NULL (_IDX x)) -> t_2*
@@ -140,7 +141,8 @@ rule Instr_ok/return:
 ;; TODO(3, rossberg): enable t_2* <: C.RETURN
 rule Instr_ok/return_call:
   C |- RETURN_CALL x : t_3* t_1* -> t_4*
-  -- Expand: C.FUNCS[x] ~~ FUNC t_1* -> t_2*
+  -- if C.FUNCS[x] = exact dt
+  -- Expand: dt ~~ FUNC t_1* -> t_2*
   -- if C.RETURN = (t'_2*)
   -- Resulttype_sub: C |- t_2* <: t'_2*
   -- Instrtype_ok: C |- t_3* -> t_4* : OK
@@ -210,8 +212,9 @@ rule Instr_ok/ref.null:
   -- Heaptype_ok: C |- ht : OK
 
 rule Instr_ok/ref.func:
-  C |- REF.FUNC x : eps -> (REF dt)
-  -- if C.FUNCS[x] = dt
+  C |- REF.FUNC x : eps -> (REF ht)
+  -- if C.FUNCS[x] = exact dt
+  -- if ht = $exactheaptype(exact, dt)
   -- if x <- C.REFS
 
 rule Instr_ok/ref.i31:
diff --git a/specification/wasm-latest/2.4-validation.modules.spectec b/specification/wasm-latest/2.4-validation.modules.spectec
index a78814662..2d021afe2 100644
--- a/specification/wasm-latest/2.4-validation.modules.spectec
+++ b/specification/wasm-latest/2.4-validation.modules.spectec
@@ -90,7 +90,8 @@ rule Elemmode_ok/active:
 
 rule Start_ok:
   C |- START x : OK
-  -- Expand: C.FUNCS[x] ~~ FUNC eps -> eps
+  -- if C.FUNCS[x] = exact dt
+  -- Expand: dt ~~ FUNC eps -> eps
 
 
 ;; Im/exports
@@ -125,8 +126,8 @@ rule Externidx_ok/table:
   -- if C.TABLES[x] = tt
 
 rule Externidx_ok/func:
-  C |- FUNC x : FUNC dt
-  -- if C.FUNCS[x] = dt
+  C |- FUNC x : FUNC exact dt
+  -- if C.FUNCS[x] = exact dt
 
 
 ;; Modules
@@ -159,14 +160,15 @@ rule Module_ok:
   ----
   -- if C = C' ++ {TAGS jt_I* jt*, GLOBALS gt*, MEMS mt_I* mt*, TABLES tt_I* tt*, DATAS ok*, ELEMS rt*}
   ----
-  -- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS dt_I* dt*, REFS x*}
+  -- if C' = {TYPES dt'*, GLOBALS gt_I*, FUNCS edt_I* edt*, REFS x*}
+  -- if edt* = (EXACT dt)*
   -- if x* = $funcidx_nonfuncs(global* mem* table* elem*)
   ----
   -- if jt_I* = $tagsxt(xt_I*)
   -- if gt_I* = $globalsxt(xt_I*)
   -- if mt_I* = $memsxt(xt_I*)
   -- if tt_I* = $tablesxt(xt_I*)
-  -- if dt_I* = $funcsxt(xt_I*)
+  -- if edt_I* = $funcsxt(xt_I*)
 
 
 rule Types_ok/empty:
diff --git a/specification/wasm-latest/4.1-execution.values.spectec b/specification/wasm-latest/4.1-execution.values.spectec
index 1b38a0623..03cef8d5a 100644
--- a/specification/wasm-latest/4.1-execution.values.spectec
+++ b/specification/wasm-latest/4.1-execution.values.spectec
@@ -102,7 +102,7 @@ rule Externaddr_ok/table:
   -- if s.TABLES[a] = tableinst
 
 rule Externaddr_ok/func:
-  s |- FUNC a : FUNC funcinst.TYPE
+  s |- FUNC a : FUNC EXACT funcinst.TYPE
   -- if s.FUNCS[a] = funcinst
 
 rule Externaddr_ok/sub:
diff --git a/specification/wasm-latest/5.2-binary.types.spectec b/specification/wasm-latest/5.2-binary.types.spectec
index 743ff8785..c44cdb5b6 100644
--- a/specification/wasm-latest/5.2-binary.types.spectec
+++ b/specification/wasm-latest/5.2-binary.types.spectec
@@ -100,7 +100,8 @@ grammar Btabletype : tabletype =
 
 
 grammar Bexterntype : externtype =
-  | 0x00 x:Btypeidx => FUNC (_IDX x)
+  | 0x00 x:Btypeidx => FUNC INEXACT (_IDX x)
+  | 0x20 x:Btypeidx => FUNC EXACT (_IDX x)
   | 0x01 tt:Btabletype => TABLE tt
   | 0x02 mt:Bmemtype => MEM mt
   | 0x03 gt:Bglobaltype => GLOBAL gt
diff --git a/specification/wasm-latest/6.2-text.types.spectec b/specification/wasm-latest/6.2-text.types.spectec
index 2afedafc9..ee285b8fa 100644
--- a/specification/wasm-latest/6.2-text.types.spectec
+++ b/specification/wasm-latest/6.2-text.types.spectec
@@ -152,7 +152,8 @@ grammar Texterntype_(I) : (externtype, idctxt) =
   | "(" "global" id?:Tid? gt:Tglobaltype_(I) ")" => (GLOBAL gt, {GLOBALS (id?)})
   | "(" "memory" id?:Tid? mt:Tmemtype_(I) ")" => (MEM mt, {MEMS (id?)})
   | "(" "table" id?:Tid? tt:Ttabletype_(I) ")" => (TABLE tt, {TABLES (id?)})
-  | "(" "func" id?:Tid? (x,I'):Ttypeuse_(I) ")" => (FUNC $($(_IDX x)), {FUNCS (id?)})
+  | "(" "func" id?:Tid? (x,I'):Ttypeuse_(I) ")" => (FUNC INEXACT $($(_IDX x)), {FUNCS (id?)})
+  | "(" "func" id?:Tid? "(" "exact" (x,I'):Ttypeuse_(I) ")" ")" => (FUNC EXACT $($(_IDX x)), {FUNCS (id?)})
 
 
 ;; Type uses