diff --git a/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl b/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
index fbf0e9a6..3eecadeb 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
+++ b/pkgs/typed-racket-pkgs/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
@@ -10,7 +10,7 @@
 @(the-eval '(require (except-in typed/racket #%top-interaction #%module-begin)))
 @(define the-top-eval (make-base-eval))
 @(the-top-eval '(require (except-in typed/racket #%module-begin)
-                         racket/flonum racket/fixnum))
+                         racket/flonum racket/extflonum racket/fixnum))
 
 @(define-syntax-rule (ex . args)
    (examples #:eval the-top-eval . args))
@@ -190,6 +190,21 @@ needed to check the desired bounds at runtime.
 -12
 3+4i]
 
+@defnums[(
+ExtFlonum
+Positive-ExtFlonum
+Nonnegative-ExtFlonum
+Negative-ExtFlonum
+Nonpositive-ExtFlonum
+ExtFlonum-Negative-Zero
+ExtFlonum-Positive-Zero
+ExtFlonum-Zero
+ExtFlonum-Nan
+)]
+80-bit @rtech{extflonum} types, for the values operated on by
+@racketmodname[racket/extflonum] exports.
+These are not part of the numeric tower.
+
 @subsection{Other Base Types}
 
 @deftogether[(
@@ -352,6 +367,8 @@ corresponding to @racket[trest], where @racket[bound]
 
 @defidform[FlVector]{An @rtech{flvector}.
   @ex[(flvector 1.0 2.0 3.0)]}
+@defidform[ExtFlVector]{An @rtech{extflvector}.
+  @ex[(extflvector 1.0t0 2.0t0 3.0t0)]}
 @defidform[FxVector]{An @rtech{fxvector}.
   @ex[(fxvector 1 2 3)]}
 
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env-indexing-abs.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env-indexing-abs.rkt
index 1bcce456..ea26d13f 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env-indexing-abs.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env-indexing-abs.rkt
@@ -2,7 +2,7 @@
 
 (require
  "../utils/utils.rkt"
- (for-template racket/base racket/list racket/unsafe/ops racket/flonum racket/fixnum)
+ (for-template racket/base racket/list racket/unsafe/ops racket/flonum racket/extflonum racket/fixnum)
  (utils tc-utils) 
  (rename-in (types union abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym]))
 
@@ -267,6 +267,10 @@
    [flvector (->* (list) -Flonum -FlVector)]
    [make-flvector (cl->* (-> index-type -FlVector)
                          (-> index-type -Flonum -FlVector))]
+   
+   [shared-flvector (->* (list) -Flonum -FlVector)]
+   [make-shared-flvector (cl->* (-> index-type -FlVector)
+                                (-> index-type -Flonum -FlVector))]
 
    [flvector-length (-> -FlVector -Index)]
    [flvector-ref (-> -FlVector index-type -Flonum)]
@@ -278,12 +282,37 @@
    [unsafe-flvector-length (-> -FlVector -Index)]
    [unsafe-flvector-ref (-> -FlVector index-type -Flonum)]
    [unsafe-flvector-set! (-> -FlVector index-type -Flonum -Void)]
+   
+   ;; Section 4.2.5.2 (ExtFlonum Vectors)
+   [extflvector? (make-pred-ty -ExtFlVector)]
+   [extflvector (->* (list) -ExtFlonum -ExtFlVector)]
+   [make-extflvector (cl->* (-> index-type -ExtFlVector)
+                            (-> index-type -ExtFlonum -ExtFlVector))]
+   
+   [shared-extflvector (->* (list) -ExtFlonum -ExtFlVector)]
+   [make-shared-extflvector (cl->* (-> index-type -ExtFlVector)
+                                   (-> index-type -ExtFlonum -ExtFlVector))]
 
+   [extflvector-length (-> -ExtFlVector -Index)]
+   [extflvector-ref (-> -ExtFlVector index-type -ExtFlonum)]
+   [extflvector-set! (-> -ExtFlVector index-type -ExtFlonum -Void)]
+   [extflvector-copy (cl->* (-> -ExtFlVector -ExtFlVector)
+                            (-> -ExtFlVector index-type -ExtFlVector)
+                            (-> -ExtFlVector index-type index-type -ExtFlVector))]
+
+   [unsafe-extflvector-length (-> -ExtFlVector -Index)]
+   [unsafe-extflvector-ref (-> -ExtFlVector index-type -ExtFlonum)]
+   [unsafe-extflvector-set! (-> -ExtFlVector index-type -ExtFlonum -Void)]
+   
    ;; Section 4.2.4.2 (Fixnum vectors)
    [fxvector? (make-pred-ty -FxVector)]
    [fxvector (->* (list) -Fixnum -FxVector)]
    [make-fxvector (cl->* (-> index-type -FxVector)
                          (-> index-type -Fixnum -FxVector))]
+   
+   [shared-fxvector (->* (list) -Fixnum -FxVector)]
+   [make-shared-fxvector (cl->* (-> index-type -FxVector)
+                                (-> index-type -Fixnum -FxVector))]
 
    [fxvector-length (-> -FxVector -Index)]
    [fxvector-ref (-> -FxVector index-type -Fixnum)]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt
index 6ee88126..7861659c 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt
@@ -2,8 +2,8 @@
 
 (begin
   (require
-   racket/list racket/math racket/flonum racket/unsafe/ops unstable/sequence racket/match
-   (for-template racket/flonum racket/fixnum racket/math racket/unsafe/ops racket/base
+   racket/list racket/math racket/flonum racket/extflonum racket/unsafe/ops unstable/sequence racket/match
+   (for-template racket/flonum racket/extflonum racket/fixnum racket/math racket/unsafe/ops racket/base
                  (only-in "../types/numeric-predicates.rkt" index?))
    (only-in (types abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R] [-PosInt -Pos]))
 
@@ -683,6 +683,171 @@
      ((Un -PosReal -NegReal) . -> . -PosReal)
      (-Real . -> . -NonNegReal)))
 
+  (define extfl-unop (lambda () (unop -ExtFlonum)))
+  
+  (define extflabs-type
+    (lambda ()
+      (cl->* (-> -ExtFlonumZero -ExtFlonumZero)
+             (-> (Un -PosExtFlonum -NegExtFlonum) -PosExtFlonum)
+             (-> -ExtFlonum -NonNegExtFlonum))))
+  (define extfl+-type
+    (lambda ()
+      (from-cases (map (lambda (t) (commutative-binop t -ExtFlonumZero t))
+                       ;; not all float types. singleton types are ruled out, since NaN can arise
+                       (list -ExtFlonumZero -ExtFlonumNan -PosExtFlonum -NonNegExtFlonum
+                             -NegExtFlonum -NonPosExtFlonum -ExtFlonum))
+                  (commutative-binop -NonNegExtFlonum -PosExtFlonum -PosExtFlonum)
+                  (map binop (list -NonNegExtFlonum -NegExtFlonum -NonPosExtFlonum -ExtFlonum))
+                  (-ExtFlonum -ExtFlonum . -> . -ExtFlonum))))
+  (define extfl--type
+    (lambda ()
+      (from-cases (binop -ExtFlonumZero)
+                  (-NegExtFlonum (Un -NonNegExtFlonum -ExtFlonumZero) . -> . -NegExtFlonum)
+                  ((Un -NonPosExtFlonum -ExtFlonumZero) -PosExtFlonum . -> . -NegExtFlonum)
+                  (-NonPosExtFlonum -NonNegExtFlonum . -> . -NonPosExtFlonum)
+                  (binop -ExtFlonum))))
+  (define extfl*-type
+    (lambda ()
+      (from-cases (binop -ExtFlonumZero)
+                  ;; we don't have Pos Pos -> Pos, possible underflow
+                  (binop -PosExtFlonum -NonNegExtFlonum)
+                  (binop -NonNegExtFlonum)
+                  (commutative-binop -NegExtFlonum -PosExtFlonum -NonPosExtFlonum)
+                  (binop -NegExtFlonum -NonNegExtFlonum)
+                  (binop -ExtFlonum))))
+  (define extfl/-type
+    (lambda ()
+      (from-cases (-ExtFlonumZero -ExtFlonum . -> . -ExtFlonumZero)
+                  (-PosExtFlonum -PosExtFlonum . -> . -NonNegExtFlonum) ; possible underflow
+                  (commutative-binop -PosExtFlonum -NegExtFlonum -NonPosExtFlonum)
+                  (-NegExtFlonum -NegExtFlonum . -> . -NonNegExtFlonum)
+                  (binop -ExtFlonum))))
+  (define extfl=-type
+    (lambda ()
+      (from-cases (map (lambda (l) (exclude-zero (car l) (cadr l) -ExtFlonumZero))
+                       (list (list -NonNegExtFlonum -PosExtFlonum)
+                             (list -NonPosExtFlonum -NegExtFlonum)))
+                  (map (lambda (t) (commutative-equality/filter -ExtFlonum t))
+                       (list -ExtFlonumZero -PosExtFlonum -NonNegExtFlonum
+                             -NegExtFlonum -NonPosExtFlonum))
+                  (comp -ExtFlonum))))
+  (define extfl<-type
+    (lambda ()
+      (from-cases
+       ;; false case, we know nothing, lhs may be NaN. same for all comparison that can involve floats
+       (-> -ExtFlonumZero -ExtFlonum B : (-FS (-filter -PosExtFlonum 1) -top))
+       (-> -ExtFlonum -ExtFlonumZero B : (-FS (-filter -NegExtFlonum 0) -top))
+       (-> -PosExtFlonum -ExtFlonum B : (-FS (-filter -PosExtFlonum 1) -top))
+       (-> -ExtFlonum -PosExtFlonum B)
+       (-> -NonNegExtFlonum -ExtFlonum B : (-FS (-filter -PosExtFlonum 1) -top))
+       (-> -ExtFlonum -NonNegExtFlonum B)
+       (-> -NegExtFlonum -ExtFlonum B)
+       (-> -ExtFlonum -NegExtFlonum B : (-FS (-filter -NegExtFlonum 0) -top))
+       (-> -NonPosExtFlonum -ExtFlonum B)
+       (-> -ExtFlonum -NonPosExtFlonum B : (-FS (-filter -NegExtFlonum 0) -top))
+       (comp -ExtFlonum))))
+  (define extfl>-type
+    (lambda ()
+      (from-cases
+       (-> -ExtFlonumZero -ExtFlonum B : (-FS (-filter -NegExtFlonum 1) -top))
+       (-> -ExtFlonum -ExtFlonumZero B : (-FS (-filter -PosExtFlonum 0) -top))
+       (-> -PosExtFlonum -ExtFlonum B)
+       (-> -ExtFlonum -PosExtFlonum B : (-FS (-filter -PosExtFlonum 0) -top))
+       (-> -NonNegExtFlonum -ExtFlonum B)
+       (-> -ExtFlonum -NonNegExtFlonum B : (-FS (-filter -PosExtFlonum 0) -top))
+       (-> -NegExtFlonum -ExtFlonum B : (-FS (-filter -NegExtFlonum 1) -top))
+       (-> -ExtFlonum -NegExtFlonum B)
+       (-> -NonPosExtFlonum -ExtFlonum B : (-FS (-filter -NegExtFlonum 1) -top))
+       (-> -ExtFlonum -NonPosExtFlonum B)
+       (comp -ExtFlonum))))
+  (define extfl<=-type
+    (lambda ()
+      (from-cases
+       (-> -ExtFlonumZero -ExtFlonum B : (-FS (-filter -NonNegExtFlonum 1) -top))
+       (-> -ExtFlonum -ExtFlonumZero B : (-FS (-filter -NonPosExtFlonum 0) -top))
+       (-> -PosExtFlonum -ExtFlonum B : (-FS (-filter -PosExtFlonum 1) -top))
+       (-> -ExtFlonum -PosExtFlonum B)
+       (-> -NonNegExtFlonum -ExtFlonum B : (-FS (-filter -NonNegExtFlonum 1) -top))
+       (-> -ExtFlonum -NonNegExtFlonum B)
+       (-> -NegExtFlonum -ExtFlonum B)
+       (-> -ExtFlonum -NegExtFlonum B : (-FS (-filter -NegExtFlonum 0) -top))
+       (-> -NonPosExtFlonum -ExtFlonum B)
+       (-> -ExtFlonum -NonPosExtFlonum B : (-FS (-filter -NonPosExtFlonum 0) -top))
+       (comp -ExtFlonum))))
+  (define extfl>=-type
+    (lambda ()
+      (from-cases
+       (-> -ExtFlonumZero -ExtFlonum B : (-FS (-filter -NonPosExtFlonum 1) -top))
+       (-> -ExtFlonum -ExtFlonumZero B : (-FS (-filter -NonNegExtFlonum 0) -top))
+       (-> -PosExtFlonum -ExtFlonum B)
+       (-> -ExtFlonum -PosExtFlonum B : (-FS (-filter -PosExtFlonum 0) -top))
+       (-> -NonNegExtFlonum -ExtFlonum B)
+       (-> -ExtFlonum -NonNegExtFlonum B : (-FS (-filter -NonNegExtFlonum 0) -top))
+       (-> -NegExtFlonum -ExtFlonum B : (-FS (-filter -NegExtFlonum 1) -top))
+       (-> -ExtFlonum -NegExtFlonum B)
+       (-> -NonPosExtFlonum -ExtFlonum B)
+       (-> -ExtFlonum -NonPosExtFlonum B : (-FS (-filter -NonPosExtFlonum 0) -top))
+       (comp -ExtFlonum))))
+  (define extflmin-type
+    (lambda ()
+      (from-cases (commutative-case -NegExtFlonum -ExtFlonum)
+                  (commutative-case -NonPosExtFlonum -ExtFlonum)
+                  (map binop (list -PosExtFlonum -NonNegExtFlonum -ExtFlonum)))))
+  (define extflmax-type
+    (lambda ()
+      (from-cases (commutative-case -PosExtFlonum -ExtFlonum)
+                  (commutative-case -NonNegExtFlonum -ExtFlonum)
+                  (map binop (list -NegExtFlonum -NonPosExtFlonum -ExtFlonum)))))
+  (define extflround-type ; truncate too
+    (lambda ()
+      (from-cases (map unop (list -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumZero
+                                  -NonNegExtFlonum -NonPosExtFlonum -ExtFlonum)))))
+  (define extflfloor-type
+    (lambda ()
+      (from-cases (map unop (list -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumZero
+                                  -NonNegExtFlonum -NegExtFlonum -NonPosExtFlonum -ExtFlonum)))))
+  (define extflceiling-type
+    (lambda ()
+      (from-cases (map unop (list -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumZero
+                                  -PosExtFlonum -NonNegExtFlonum -NonPosExtFlonum -ExtFlonum)))))
+  (define extfllog-type
+    (lambda ()
+      (from-cases (-> -ExtFlonumZero -NegExtFlonum) ; -inf
+                  (unop -ExtFlonum))))
+  (define extflexp-type
+    (lambda ()
+      (from-cases (-NonNegExtFlonum . -> . -PosExtFlonum)
+                  (-NegExtFlonum . -> . -NonNegExtFlonum)
+                  (-ExtFlonum . -> . -ExtFlonum)))) ; nan is the only non nonnegative case (returns nan)
+  (define extflsqrt-type
+    (lambda ()
+      (from-cases (map unop (list -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumZero
+                                  -NonNegExtFlonum ; we don't have positive case, possible underflow
+                                  -ExtFlonum))))) ; anything negative returns nan
+  (define extflexpt-type
+    (lambda ()
+      (from-cases (-ExtFlonumZero -PosExtFlonum . -> . -ExtFlonumZero) ; (extflexpt -0.0t0 0.1t0) -> 0.0t0 ; not sign preserving
+                  ((Un -PosExtFlonum -NegExtFlonum) -ExtFlonumZero . -> . -PosExtFlonum) ; always returns 1.0t0
+                  (-NonNegExtFlonum -ExtFlonum . -> . -NonNegExtFlonum) ; can underflow
+                  (-ExtFlonum -ExtFlonum . -> . -ExtFlonum))))
+
+  (define fx->extfl-type
+    (lambda ()
+      (fx-from-cases
+       (-PosInt . -> . -PosExtFlonum)
+       (-Nat . -> . -NonNegExtFlonum)
+       (-NegInt . -> . -NegExtFlonum)
+       (-NonPosInt . -> . -NonPosExtFlonum)
+       (-Int . -> . -ExtFlonum))))
+  (define extfl->fx-type
+    (lambda ()
+      (from-cases
+       (-ExtFlonumZero . -> . -Zero)
+       (-PosExtFlonum . -> . -PosFixnum)
+       (-NegExtFlonum . -> . -NegFixnum)
+       (-NonNegExtFlonum . -> . -NonNegFixnum)
+       (-NonPosExtFlonum . -> . -NonPosFixnum)
+       (-ExtFlonum . -> . -Fixnum))))
 
   ;Check to ensure we fail fast if the flonum bindings change
   (define-namespace-anchor anchor)
@@ -698,7 +863,20 @@
                        [unsafe-flacos     flacos]
                        [unsafe-fllog      fllog]
                        [unsafe-flexp      flexp]
-                       [unsafe-flexpt     flexpt])))
+                       [unsafe-flexpt     flexpt]
+                       [unsafe-extflround    extflround]
+                       [unsafe-extflfloor    extflfloor]
+                       [unsafe-extflceiling  extflceiling]
+                       [unsafe-extfltruncate extfltruncate]
+                       [unsafe-extflsin      extflsin]
+                       [unsafe-extflcos      extflcos]
+                       [unsafe-extfltan      extfltan]
+                       [unsafe-extflatan     extflatan]
+                       [unsafe-extflasin     extflasin]
+                       [unsafe-extflacos     extflacos]
+                       [unsafe-extfllog      extfllog]
+                       [unsafe-extflexp      extflexp]
+                       [unsafe-extflexpt     extflexpt])))
     (define phase (namespace-base-phase (namespace-anchor->namespace anchor)))
 
     (for ([op-pair (in-syntax flonum-ops)])
@@ -2107,3 +2285,95 @@
 [unsafe-flreal-part (flreal-part-type)]
 [unsafe-flimag-part (flimag-part-type)]
 [unsafe-flrandom (flrandom-type)]
+
+; racket/extflonum
+[extflonum? (make-pred-ty -ExtFlonum)]
+[extflonum-available? (-> B)]
+[pi.t -PosExtFlonum]
+
+[extflabs (extflabs-type)]
+[extfl+ (extfl+-type)]
+[extfl- (extfl--type)]
+[extfl* (extfl*-type)]
+[extfl/ (extfl/-type)]
+[extfl= (extfl=-type)]
+[extfl<= (extfl<=-type)]
+[extfl>= (extfl>=-type)]
+[extfl> (extfl>-type)]
+[extfl< (extfl<-type)]
+[extflmin (extflmin-type)]
+[extflmax (extflmax-type)]
+[extflround (extflround-type)]
+[extflfloor (extflfloor-type)]
+[extflceiling (extflceiling-type)]
+[extfltruncate (extflround-type)]
+[extflsin (extfl-unop)] ; special cases (0s) not worth special-casing
+[extflcos (extfl-unop)]
+[extfltan (extfl-unop)]
+[extflatan (extfl-unop)]
+[extflasin (extfl-unop)]
+[extflacos (extfl-unop)]
+[extfllog (extfllog-type)]
+[extflexp (extflexp-type)]
+[extflexpt (extflexpt-type)]
+[extflsqrt (extflsqrt-type)]
+[->extfl (fx->extfl-type)]
+[extfl->exact-integer (cl->* (-ExtFlonumZero . -> . -Zero)
+                             (-PosExtFlonum . -> . -PosInt)
+                             (-NonNegExtFlonum . -> . -Nat)
+                             (-NegExtFlonum . -> . -NegInt)
+                             (-NonPosExtFlonum . -> . -NonPosInt)
+                             (-ExtFlonum . -> . -Int))]
+[real->extfl (cl->* (-PosReal . -> . -PosExtFlonum)
+                    (-NegReal . -> . -NegExtFlonum)
+                    (-RealZero . -> . -ExtFlonumZero)
+                    (-NonNegReal . -> . -NonNegExtFlonum)
+                    (-NonPosReal . -> . -NonPosExtFlonum)
+                    (-Real . -> . -ExtFlonum))]
+[extfl->exact (cl->* (-ExtFlonumZero . -> . -Zero)
+                     (-PosExtFlonum . -> . -PosRat)
+                     (-NonNegExtFlonum . -> . -NonNegRat)
+                     (-NegExtFlonum . -> . -NegRat)
+                     (-NonPosExtFlonum . -> . -NonPosRat)
+                     (-ExtFlonum . -> . -Rat))]
+[extfl->inexact (cl->* (-ExtFlonumZero . -> . -FlonumZero)
+                       (-PosExtFlonum . -> . -PosFlonum)
+                       (-NonNegExtFlonum . -> . -NonNegFlonum)
+                       (-NegExtFlonum . -> . -NegFlonum)
+                       (-NonPosExtFlonum . -> . -NonPosFlonum)
+                       (-ExtFlonum . -> . -Flonum))]
+[unsafe-extflabs (extflabs-type)]
+[unsafe-extfl+ (extfl+-type)]
+[unsafe-extfl- (extfl--type)]
+[unsafe-extfl* (extfl*-type)]
+[unsafe-extfl/ (extfl/-type)]
+[unsafe-extfl= (extfl=-type)]
+[unsafe-extfl<= (extfl<=-type)]
+[unsafe-extfl>= (extfl>=-type)]
+[unsafe-extfl> (extfl>-type)]
+[unsafe-extfl< (extfl<-type)]
+[unsafe-extflmin (extflmin-type)]
+[unsafe-extflmax (extflmax-type)]
+
+;These are currently the same binding as the safe versions
+;and so are not needed. If this changes they should be
+;uncommented. There is a check in the definitions part of
+;the file that makes sure that they are the same binding.
+;
+;[unsafe-extflround (extflround-type)]
+;[unsafe-extflfloor (extflfloor-type)]
+;[unsafe-extflceiling (extflceiling-type)]
+;[unsafe-extfltruncate (extflround-type)]
+;[unsafe-extflsin (extfl-unop)]
+;[unsafe-extflcos (extfl-unop)]
+;[unsafe-extfltan (extfl-unop)]
+;[unsafe-extflatan (extfl-unop)]
+;[unsafe-extflasin (extfl-unop)]
+;[unsafe-extflacos (extfl-unop)]
+;[unsafe-extfllog (extfllog-type)]
+;[unsafe-extflexp (extflexp-type)]
+;[unsafe-extflexpt (extflexpt-type)]
+;
+[unsafe-extflsqrt (extflsqrt-type)]
+[unsafe-fx->extfl (fx->extfl-type)]
+[unsafe-extfl->fx (extfl->fx-type)]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt
index 054227a8..0ff68623 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-env.rkt
@@ -7,6 +7,7 @@
   (except-in racket -> ->* one-of/c class)
   racket/unsafe/ops
   racket/unsafe/undefined
+  (only-in racket/extflonum floating-point-bytes->extfl extfl->floating-point-bytes)
   ;(only-in rnrs/lists-6 fold-left)
   '#%paramz
   "extra-procs.rkt"
@@ -88,6 +89,10 @@
 
 [order-of-magnitude (-> -PosReal -Int)]
 
+;; Section 4.2.5.3 (ExtFlonum-Bytes Conversions)
+[floating-point-bytes->extfl (->opt -Bytes [Univ -Nat -Nat] -ExtFlonum)]
+[extfl->floating-point-bytes (->opt -ExtFlonum [Univ -Bytes -Nat] -Bytes)]
+
 ;; Section 4.3 (Strings)
 [string? (make-pred-ty -String)]
 ;make-string (in Index)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-special-env.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-special-env.rkt
index cd0e93a2..088ff19d 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-special-env.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-special-env.rkt
@@ -218,9 +218,11 @@
   ;; for `define-runtime-module-path`
   [(make-template-identifier 'combine-module-path 'racket/runtime-path)
    (-> -Variable-Reference -Module-Path -Resolved-Module-Path)]
-  ;; in-fxvector, in-flvector
+  ;; in-fxvector, in-flvector, in-extflvector
   [(make-template-identifier 'in-fxvector* 'racket/fixnum)
    (-> -FxVector (-seq -Fixnum))]
   [(make-template-identifier 'in-flvector* 'racket/flonum)
    (-> -FlVector (-seq -Flonum))]
+  [(make-template-identifier 'in-extflvector* 'racket/extflonum)
+   (-> -ExtFlVector (-seq -ExtFlonum))]
   )
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt
index c5be1e01..615ae617 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/base-types.rkt
@@ -75,7 +75,15 @@
 [Positive-Byte -PosByte]
 [Zero (-val 0)]
 [One  (-val 1)]
-
+[ExtFlonum -ExtFlonum]
+[Nonpositive-ExtFlonum -NonPosExtFlonum]
+[Negative-ExtFlonum -NegExtFlonum]
+[Nonnegative-ExtFlonum -NonNegExtFlonum]
+[Positive-ExtFlonum -PosExtFlonum]
+[ExtFlonum-Nan -ExtFlonumNan]
+[ExtFlonum-Zero -ExtFlonumZero]
+[ExtFlonum-Negative-Zero -ExtFlonumNegZero]
+[ExtFlonum-Positive-Zero -ExtFlonumPosZero]
 
 [Void -Void]
 [Undefined -Undefined] ; initial value of letrec bindings
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt
index 77f71082..12dd634a 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/base-env/prims.rkt
@@ -106,6 +106,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
          "case-lambda.rkt"
          'struct-extraction
          racket/flonum ; for for/flvector and for*/flvector
+         racket/extflonum ; for for/extflvector and for*/extflvector
          (for-syntax
           racket/lazy-require
           syntax/parse
@@ -1368,7 +1369,8 @@ This file defines two sorts of primitives. All of them are provided into any mod
 
 (define-syntax (base-for/flvector: stx)
   (syntax-parse stx
-    [(_ for: #:length n-expr:expr (clauses ...) body ...+)
+    [(_ for: Float flvector make-flvector unsafe-flvector-ref unsafe-flvector-set! flvector-copy
+        #:length n-expr:expr (clauses ...) body ...+)
      (syntax/loc stx
        (-let ([n : Integer  n-expr])
          (cond [(n . > . 0)
@@ -1381,7 +1383,8 @@ This file defines two sorts of primitives. All of them are provided into any mod
                     (when (i . unsafe-fx>= . n) (break (void)))))
                 xs]
                [else  (flvector)])))]
-    [(_ for: (clauses ...) body ...+)
+    [(_ for: Float flvector make-flvector unsafe-flvector-ref unsafe-flvector-set! flvector-copy
+        (clauses ...) body ...+)
      (syntax/loc stx
        (let ()
          (define n 4)
@@ -1402,7 +1405,13 @@ This file defines two sorts of primitives. All of them are provided into any mod
          (flvector-copy xs 0 i)))]))
 
 (define-syntax-rule (for/flvector: e ...)
-  (base-for/flvector: for: e ...))
+  (base-for/flvector: for: Flonum flvector make-flvector unsafe-flvector-ref unsafe-flvector-set! flvector-copy e ...))
 
 (define-syntax-rule (for*/flvector: e ...)
-  (base-for/flvector: for*: e ...))
+  (base-for/flvector: for*: Flonum flvector make-flvector unsafe-flvector-ref unsafe-flvector-set! flvector-copy e ...))
+
+(define-syntax-rule (for/extflvector: e ...)
+  (base-for/flvector: for: ExtFlonum extflvector make-extflvector unsafe-extflvector-ref unsafe-extflvector-set! extflvector-copy e ...))
+
+(define-syntax-rule (for*/extflvector: e ...)
+  (base-for/flvector: for*: ExtFlonum extflvector make-extflvector unsafe-extflvector-ref unsafe-extflvector-set! extflvector-copy e ...))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt
index 9655a298..f0c30fc9 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -539,9 +539,14 @@
     [_ (int-err "not a function" f)]))
 
 (module predicates racket/base
-  (provide nonnegative? nonpositive?)
+  (require racket/extflonum)
+  (provide nonnegative? nonpositive?
+           extflonum? extflzero? extflnonnegative? extflnonpositive?)
   (define nonnegative? (lambda (x) (>= x 0)))
-  (define nonpositive? (lambda (x) (<= x 0))))
+  (define nonpositive? (lambda (x) (<= x 0)))
+  (define extflzero? (lambda (x) (extfl= x 0.0t0)))
+  (define extflnonnegative? (lambda (x) (extfl>= x 0.0t0)))
+  (define extflnonpositive? (lambda (x) (extfl<= x 0.0t0))))
 
 (module numeric-contracts racket/base
   (require
@@ -603,6 +608,11 @@
                      (and (inexact-real? (imag-part x))
                           (inexact-real? (real-part x)))))))
   (define number/sc (numeric/sc Number number?))
+  
+  (define extflonum-zero/sc (numeric/sc ExtFlonum-Zero (and/c extflonum? extflzero?)))
+  (define nonnegative-extflonum/sc (numeric/sc Nonnegative-ExtFlonum (and/c extflonum? extflnonnegative?)))
+  (define nonpositive-extflonum/sc (numeric/sc Nonpositive-ExtFlonum (and/c extflonum? extflnonpositive?)))
+  (define extflonum/sc (numeric/sc ExtFlonum extflonum?))
 
   )
 (require 'numeric-contracts)
@@ -654,6 +664,10 @@
     [(== t:-ExactNumber type-equal?) exact-number/sc]
     [(== t:-InexactComplex type-equal?) inexact-complex/sc]
     [(== t:-Number type-equal?) number/sc]
+    [(== t:-ExtFlonumZero type-equal?) extflonum-zero/sc]
+    [(== t:-NonNegExtFlonum type-equal?) nonnegative-extflonum/sc]
+    [(== t:-NonPosExtFlonum type-equal?) nonpositive-extflonum/sc]
+    [(== t:-ExtFlonum type-equal?) extflonum/sc]
     [else #f]))
 
 
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
index ccf175d3..455b2c01 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
@@ -9,7 +9,8 @@
          (utils stxclass-util)
          syntax/parse
          unstable/function
-         unstable/sequence)
+         unstable/sequence
+         racket/extflonum)
 
 (import)
 (export tc-literal^)
@@ -67,6 +68,16 @@
     ;; can't have real and imaginary parts that are both inexact, but not the same precision
     [(~var i (3d number?)) -Number] ; otherwise, Number
     
+    ;; 80-bit flonums
+    [(~var i (3d (lambda (x) (eqv? x 0.0t0)))) -ExtFlonumPosZero]
+    [(~var i (3d (lambda (x) (eqv? x -0.0t0)))) -ExtFlonumNegZero]
+    [(~var i (3d (lambda (x) (eqv? x +nan.t)))) -ExtFlonumNan]
+    [(~var i (3d (lambda (x) (eqv? x +inf.t)))) (-val +inf.t)]
+    [(~var i (3d (lambda (x) (eqv? x -inf.t)))) (-val -inf.t)]
+    [(~var i (3d (conjoin extflonum? (λ (x) (extfl> x 0.0t0))))) -PosExtFlonum]
+    [(~var i (3d (conjoin extflonum? (λ (x) (extfl< x 0.0t0))))) -NegExtFlonum]
+    [(~var i (3d extflonum?)) -ExtFlonum] ; for nan
+    
     [i:str -String]
     [i:char -Char]
     [i:keyword (-val (syntax-e #'i))]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt
index 2f5c8e59..5dd6d382 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/abbrev.rkt
@@ -30,12 +30,14 @@
            (only-in racket/udp udp?)
            (only-in racket/tcp tcp-listener?)
            (only-in racket/flonum flvector?)
+           (only-in racket/extflonum extflvector?)
            (only-in racket/fixnum fxvector?)
            (only-in '#%place place? place-channel?))
          (only-in racket/pretty pretty-print-style-table?)
          (only-in racket/udp udp?)
          (only-in racket/tcp tcp-listener?)
          (only-in racket/flonum flvector?)
+         (only-in racket/extflonum extflvector?)
          (only-in racket/fixnum fxvector?)
          (only-in '#%place place? place-channel?))
 
@@ -148,6 +150,7 @@
 (define/decl -TCP-Listener (make-Base 'TCP-Listener #'tcp-listener? tcp-listener?))
 (define/decl -UDP-Socket (make-Base 'UDP-Socket #'udp? udp?))
 (define/decl -FlVector (make-Base 'FlVector #'flvector? flvector?))
+(define/decl -ExtFlVector (make-Base 'ExtFlVector #'extflvector? extflvector?))
 (define/decl -FxVector (make-Base 'FxVector #'fxvector? fxvector?))
 (define -Syntax make-Syntax)
 (define/decl In-Syntax
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/generalize.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/generalize.rkt
index 332c3cb2..eefa91d0 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/generalize.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/generalize.rkt
@@ -28,6 +28,7 @@
         [(? (lambda (t) (subtype t -FloatComplex))) -FloatComplex]
         [(? (lambda (t) (subtype t -SingleFlonumComplex))) -SingleFlonumComplex]
         [(? (lambda (t) (subtype t -Number))) -Number]
+        [(? (lambda (t) (subtype t -ExtFlonum))) -ExtFlonum]
         [(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*]
         [(Pair: t1 (Value: '())) (-lst t1)]
         [(MPair: t1 (Value: '())) (-mlst t1)]
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/numeric-tower.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/numeric-tower.rkt
index 4072657e..e666cda0 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/numeric-tower.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/numeric-tower.rkt
@@ -5,8 +5,9 @@
                     [simple-Un *Un])
          (rename-in (rep type-rep) [make-Base make-Base*])
          unstable/function
+         racket/extflonum
          ;; For base type contracts
-         (for-template racket/base racket/contract/base (types numeric-predicates)))
+         (for-template racket/base racket/contract/base racket/extflonum (types numeric-predicates)))
 
 (provide portable-fixnum? portable-index?
          -Zero -One -PosByte -Byte -PosIndex -Index
@@ -19,9 +20,11 @@
          -RealZero -PosReal -NonNegReal -NegReal -NonPosReal -Real
          -ExactImaginary -FloatImaginary -SingleFlonumImaginary -InexactImaginary -Imaginary
          -ExactNumber -ExactComplex -FloatComplex -SingleFlonumComplex -InexactComplex -Number
-         (rename-out (-Int -Integer)))
+         (rename-out (-Int -Integer))
+         -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumZero -ExtFlonumNan
+         -PosExtFlonum -NonNegExtFlonum -NegExtFlonum -NonPosExtFlonum -ExtFlonum)
 
-;; all the types defined here are numeric
+;; all the types defined here are numeric (except 80-bit flonums)
 (define (make-Base name contract predicate)
   (make-Base* name contract predicate #t))
 
@@ -287,3 +290,42 @@
 (define/decl -InexactComplex (*Un -FloatComplex -SingleFlonumComplex))
 (define/decl -Complex (*Un -Real -Imaginary -ExactComplex -InexactComplex))
 (define/decl -Number -Complex)
+
+;; 80-bit floating-point numbers
+;; +nan.t is included in all 80-bit floating-point types
+(define/decl -ExtFlonumNan
+  (make-Base* 'ExtFlonum-Nan
+              #'(and/c extflonum? (lambda (x) (eqv? x +nan.t)))
+              (lambda (x) (and (extflonum? x) (eqv? x +nan.t)))
+              #f))
+
+(define/decl -ExtFlonumPosZero
+  (make-Base* 'ExtFlonum-Positive-Zero
+              #'(lambda (x) (eqv? x 0.0t0))
+              (lambda (x) (eqv? x 0.0t0))
+              #f))
+
+(define/decl -ExtFlonumNegZero
+  (make-Base* 'ExtFlonum-Negative-Zero
+              #'(lambda (x) (eqv? x -0.0t0))
+              (lambda (x) (eqv? x -0.0t0))
+              #f))
+
+(define/decl -NegExtFlonumNoNan
+  (make-Base* 'Negative-ExtFlonum-No-NaN
+              #'(and/c extflonum? (λ (x) (extfl<= x 0.0t0)))
+              (lambda (x) (and (extflonum? x) (extfl<= x 0.0t0)))
+              #f))
+
+(define/decl -PosExtFlonumNoNan
+  (make-Base* 'Positive-ExtFlonum-No-NaN
+              #'(and/c extflonum? (λ (x) (extfl>= x 0.0t0)))
+              (lambda (x) (and (extflonum? x) (extfl>= x 0.0t0)))
+              #f))
+
+(define/decl -ExtFlonumZero (*Un -ExtFlonumPosZero -ExtFlonumNegZero -ExtFlonumNan))
+(define/decl -PosExtFlonum (*Un -PosExtFlonumNoNan -ExtFlonumNan))
+(define/decl -NonNegExtFlonum (*Un -PosExtFlonum -ExtFlonumZero))
+(define/decl -NegExtFlonum (*Un -NegExtFlonumNoNan -ExtFlonumNan))
+(define/decl -NonPosExtFlonum (*Un -NegExtFlonum -ExtFlonumZero))
+(define/decl -ExtFlonum (*Un -NegExtFlonumNoNan -ExtFlonumNegZero -ExtFlonumPosZero -PosExtFlonumNoNan -ExtFlonumNan))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
index 7c2f6d1c..581cc9dc 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -330,6 +330,8 @@
           (subtype* A0 t t*)]
          [((Base: 'FlVector _ _ _) (Sequence: (list t*)))
           (subtype* A0 -Flonum t*)]
+         [((Base: 'ExtFlVector _ _ _) (Sequence: (list t*)))
+          (subtype* A0 -ExtFlonum t*)]
          [((Base: 'FxVector _ _ _) (Sequence: (list t*)))
           (subtype* A0 -Fixnum t*)]
          [((Base: 'String _ _ _) (Sequence: (list t*)))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/any-wrap.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/any-wrap.rkt
index 887bfb11..8c60bc5a 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/any-wrap.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/any-wrap.rkt
@@ -1,7 +1,7 @@
 #lang racket/base
 
 (require racket/match racket/contract/combinator
-         racket/fixnum racket/flonum
+         racket/fixnum racket/flonum racket/extflonum
          racket/set
          racket/undefined
          (only-in (combine-in racket/private/promise)
@@ -15,7 +15,7 @@
       ;; Base values because you can only store flonums/fixnums in these
       ;; and not any higher-order values. This isn't sound if we ever
       ;; introduce bounded polymorphism for Flvector/Fxvector.
-      (flvector? e) (fxvector? e)))
+      (flvector? e) (fxvector? e) (extflvector? e)))
 
 (define (val-first-projection b)
   (define (fail neg-party v)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/flonum.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/flonum.rkt
index b1489932..e09fe2bf 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/flonum.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/flonum.rkt
@@ -1,8 +1,9 @@
-#lang typed/scheme
+#lang typed/racket
 
 (require
- scheme/flonum
- scheme/unsafe/ops)
+ racket/flonum
+ racket/extflonum
+ racket/unsafe/ops)
 
 (: check (All (a) ((a a -> Boolean) a a -> Boolean)))
 ;; Simple check function as RackUnit doesn't work in Typed Scheme (yet)
@@ -55,3 +56,36 @@
 (check = (flsqrt 1.45) (unsafe-flsqrt 1.45))
 (check = (->fl 1) 1.0)
 (check = (unsafe-fx->fl 1) 1.0)
+
+(check extfl= (extflabs 1.45t0) (unsafe-extflabs 1.45t0))
+(check extfl= (extfl+ 1.45t0 2.36t0) (unsafe-extfl+ 1.45t0 2.36t0))
+(check extfl= (extfl- 1.45t0 2.36t0) (unsafe-extfl- 1.45t0 2.36t0))
+(check extfl= (extfl* 1.45t0 2.36t0) (unsafe-extfl* 1.45t0 2.36t0))
+(check extfl= (extfl/ 1.45t0 2.36t0) (unsafe-extfl/ 1.45t0 2.36t0))
+(check-pred true? (extfl= 1.45t0 1.45t0))
+(check-pred true? (extfl<= 1.45t0 1.45t0))
+(check-pred true? (extfl>= 1.45t0 1.45t0))
+(check-pred true? (extfl> 1.45t0 1.36t0))
+(check-pred true? (extfl< 1.36t0 1.45t0))
+(check-pred true? (unsafe-extfl= 1.45t0 1.45t0))
+(check-pred true? (unsafe-extfl<= 1.45t0 1.45t0))
+(check-pred true? (unsafe-extfl>= 1.45t0 1.45t0))
+(check-pred true? (unsafe-extfl> 1.45t0 1.36t0))
+(check-pred true? (unsafe-extfl< 1.36t0 1.45t0))
+(check extfl= (extflmin 1.45t0 2.36t0) (unsafe-extflmin 1.45t0 2.36t0))
+(check extfl= (extflmax 1.45t0 2.36t0) (unsafe-extflmax 1.45t0 2.36t0))
+(check extfl= (extflround 1.45t0) (unsafe-extflround 1.45t0))
+(check extfl= (extflfloor 1.45t0) (unsafe-extflfloor 1.45t0))
+(check extfl= (extflceiling 1.45t0) (unsafe-extflceiling 1.45t0))
+(check extfl= (extfltruncate 1.45t0) (unsafe-extfltruncate 1.45t0))
+(check extfl= (extflsin 1.45t0) (unsafe-extflsin 1.45t0))
+(check extfl= (extflcos 1.45t0) (unsafe-extflcos 1.45t0))
+(check extfl= (extfltan 1.45t0) (unsafe-extfltan 1.45t0))
+(check extfl= (extflatan 1.45t0) (unsafe-extflatan 1.45t0))
+(check extfl= (extflasin .45t0) (unsafe-extflasin .45t0))
+(check extfl= (extflacos .45t0) (unsafe-extflacos .45t0))
+(check extfl= (extfllog 1.45t0) (unsafe-extfllog 1.45t0))
+(check extfl= (extflexp 1.45t0) (unsafe-extflexp 1.45t0))
+(check extfl= (extflsqrt 1.45t0) (unsafe-extflsqrt 1.45t0))
+(check extfl= (->extfl 1) 1.0t0)
+(check extfl= (unsafe-fx->extfl 1) 1.0t0)
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/for-vector.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/for-vector.rkt
index 5a1741aa..61663f86 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/for-vector.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/for-vector.rkt
@@ -3,7 +3,8 @@
 (require (for-syntax syntax/parse)
          racket/unsafe/ops
          typed/rackunit
-         racket/flonum)
+         racket/flonum
+         racket/extflonum)
 
 (check-equal? (for/vector: #:length 4 ([i  (in-range 4)]) : Float
                 (real->double-flonum i))
@@ -154,156 +155,305 @@
 ;; ===================================================================================================
 ;; for/flvector:
 
-(define-syntax-rule (test-flvector a b) ; for some reason, check-equal? doesn't work below
-  (unless (equal? a b)
-    (error "bad")))
-
-(test-flvector (for/flvector: #:length 4 ([i  (in-range 4)])
+(check-equal? (for/flvector: #:length 4 ([i  (in-range 4)])
                 (real->double-flonum i))
               (flvector 0.0 1.0 2.0 3.0))
 
-(test-flvector (for/flvector: #:length 4 ([i  (in-range 0)])
+(check-equal? (for/flvector: #:length 4 ([i  (in-range 0)])
                 (real->double-flonum i))
               (flvector 0.0 0.0 0.0 0.0))
 
-(test-flvector (for/flvector: #:length 4 ()
+(check-equal? (for/flvector: #:length 4 ()
                 1.2)
               (flvector 1.2 0.0 0.0 0.0))
 
-(test-flvector (for/flvector: #:length 4 ([i  (in-range 2)])
+(check-equal? (for/flvector: #:length 4 ([i  (in-range 2)])
                 (real->double-flonum i))
               (flvector 0.0 1.0 0.0 0.0))
 
-(test-flvector (for/flvector: #:length 4 ([i  (in-range 5)])
+(check-equal? (for/flvector: #:length 4 ([i  (in-range 5)])
                 (real->double-flonum i))
               (flvector 0.0 1.0 2.0 3.0))
 
-(test-flvector (for/flvector: #:length 0 ([i  (in-range 5)])
+(check-equal? (for/flvector: #:length 0 ([i  (in-range 5)])
                 (real->double-flonum i))
               (flvector))
 
-(test-flvector (for/flvector: ([i  (in-range 4)])
+(check-equal? (for/flvector: ([i  (in-range 4)])
                 (real->double-flonum i))
               (flvector 0.0 1.0 2.0 3.0))
 
-(test-flvector (for/flvector: () 1.2)
+(check-equal? (for/flvector: () 1.2)
               (flvector 1.2))
 
-(test-flvector (for/flvector: ([i  (in-range 0)])
+(check-equal? (for/flvector: ([i  (in-range 0)])
                 (real->double-flonum i))
               (flvector))
 
-(test-flvector (for/flvector: #:length 4 ([x  (in-range 2)]
-                                          #:when #t
-                                          [y  (in-range 2)])
+(check-equal? (for/flvector: #:length 4 ([x  (in-range 2)]
+                                         #:when #t
+                                         [y  (in-range 2)])
                 (real->double-flonum (+ x y)))
               (flvector 0.0 1.0 1.0 2.0))
 
-(test-flvector (for/flvector: #:length 4 ([x  (in-range 0)]
-                                          #:when #t
-                                          [y  (in-range 2)])
+(check-equal? (for/flvector: #:length 4 ([x  (in-range 0)]
+                                         #:when #t
+                                         [y  (in-range 2)])
                 (real->double-flonum (+ x y)))
               (flvector 0.0 0.0 0.0 0.0))
 
-(test-flvector (for/flvector: #:length 4 ([x  (in-range 2)]
-                                          #:when #t
-                                          [y  (in-range 1)])
+(check-equal? (for/flvector: #:length 4 ([x  (in-range 2)]
+                                         #:when #t
+                                         [y  (in-range 1)])
                 (real->double-flonum (+ x y)))
               (flvector 0.0 1.0 0.0 0.0))
 
-(test-flvector (for/flvector: #:length 4 ([x  (in-range 2)]
-                                          #:when #t
-                                          [y  (in-range 3)])
+(check-equal? (for/flvector: #:length 4 ([x  (in-range 2)]
+                                         #:when #t
+                                         [y  (in-range 3)])
                 (real->double-flonum (+ x y)))
               (flvector 0.0 1.0 2.0 1.0))
 
-(test-flvector (for/flvector: #:length 0 ([x  (in-range 2)]
-                                          #:when #t
-                                          [y  (in-range 3)])
+(check-equal? (for/flvector: #:length 0 ([x  (in-range 2)]
+                                         #:when #t
+                                         [y  (in-range 3)])
                 (real->double-flonum (+ x y)))
               (flvector))
 
-(test-flvector (for/flvector: ([x  (in-range 2)]
-                               #:when #t
-                               [y  (in-range 2)])
+(check-equal? (for/flvector: ([x  (in-range 2)]
+                              #:when #t
+                              [y  (in-range 2)])
                 (real->double-flonum (+ x y)))
               (flvector 0.0 1.0 1.0 2.0))
 
-(test-flvector (for/flvector: ([x  (in-range 0)]
-                               #:when #t
-                               [y  (in-range 2)])
+(check-equal? (for/flvector: ([x  (in-range 0)]
+                              #:when #t
+                              [y  (in-range 2)])
                 (real->double-flonum (+ x y)))
               (flvector))
 
 ;; ===================================================================================================
 ;; for*/flvector:
 
-(test-flvector (for*/flvector: #:length 4 ([i  (in-range 4)])
+(check-equal? (for*/flvector: #:length 4 ([i  (in-range 4)])
                 (real->double-flonum i))
               (flvector 0.0 1.0 2.0 3.0))
 
-(test-flvector (for*/flvector: #:length 4 ([i  (in-range 0)])
+(check-equal? (for*/flvector: #:length 4 ([i  (in-range 0)])
                 (real->double-flonum i))
               (flvector 0.0 0.0 0.0 0.0))
 
-(test-flvector (for*/flvector: #:length 4 ()
+(check-equal? (for*/flvector: #:length 4 ()
                 1.2)
               (flvector 1.2 0.0 0.0 0.0))
 
-(test-flvector (for*/flvector: #:length 4 ([i  (in-range 2)])
+(check-equal? (for*/flvector: #:length 4 ([i  (in-range 2)])
                 (real->double-flonum i))
               (flvector 0.0 1.0 0.0 0.0))
 
-(test-flvector (for*/flvector: #:length 4 ([i  (in-range 5)])
+(check-equal? (for*/flvector: #:length 4 ([i  (in-range 5)])
                 (real->double-flonum i))
               (flvector 0.0 1.0 2.0 3.0))
 
-(test-flvector (for*/flvector: #:length 0 ([i  (in-range 5)])
+(check-equal? (for*/flvector: #:length 0 ([i  (in-range 5)])
                 (real->double-flonum i))
               (flvector))
 
-(test-flvector (for*/flvector: ([i  (in-range 4)])
+(check-equal? (for*/flvector: ([i  (in-range 4)])
                 (real->double-flonum i))
               (flvector 0.0 1.0 2.0 3.0))
 
-(test-flvector (for*/flvector: () 1.2)
+(check-equal? (for*/flvector: () 1.2)
               (flvector 1.2))
 
-(test-flvector (for*/flvector: ([i  (in-range 0)])
+(check-equal? (for*/flvector: ([i  (in-range 0)])
                 (real->double-flonum i))
               (flvector))
 
-(test-flvector (for*/flvector: #:length 4 ([x  (in-range 2)]
-                                           [y  (in-range 2)])
+(check-equal? (for*/flvector: #:length 4 ([x  (in-range 2)]
+                                          [y  (in-range 2)])
                 (real->double-flonum (+ x y)))
               (flvector 0.0 1.0 1.0 2.0))
 
-(test-flvector (for*/flvector: #:length 4 ([x  (in-range 0)]
-                                           [y  (in-range 2)])
+(check-equal? (for*/flvector: #:length 4 ([x  (in-range 0)]
+                                          [y  (in-range 2)])
                 (real->double-flonum (+ x y)))
               (flvector 0.0 0.0 0.0 0.0))
 
-(test-flvector (for*/flvector: #:length 4 ([x  (in-range 2)]
-                                           [y  (in-range 1)])
+(check-equal? (for*/flvector: #:length 4 ([x  (in-range 2)]
+                                          [y  (in-range 1)])
                 (real->double-flonum (+ x y)))
               (flvector 0.0 1.0 0.0 0.0))
 
-(test-flvector (for*/flvector: #:length 4 ([x  (in-range 2)]
-                                           [y  (in-range 3)])
+(check-equal? (for*/flvector: #:length 4 ([x  (in-range 2)]
+                                          [y  (in-range 3)])
                 (real->double-flonum (+ x y)))
               (flvector 0.0 1.0 2.0 1.0))
 
-(test-flvector (for*/flvector: #:length 0 ([x  (in-range 2)]
-                                           [y  (in-range 3)])
+(check-equal? (for*/flvector: #:length 0 ([x  (in-range 2)]
+                                          [y  (in-range 3)])
                 (real->double-flonum (+ x y)))
               (flvector))
 
-(test-flvector (for*/flvector: ([x  (in-range 2)]
-                                [y  (in-range 2)])
+(check-equal? (for*/flvector: ([x  (in-range 2)]
+                               [y  (in-range 2)])
                 (real->double-flonum (+ x y)))
               (flvector 0.0 1.0 1.0 2.0))
 
-(test-flvector (for*/flvector: ([x  (in-range 0)]
-                                [y  (in-range 2)])
+(check-equal? (for*/flvector: ([x  (in-range 0)]
+                               [y  (in-range 2)])
                 (real->double-flonum (+ x y)))
               (flvector))
+
+;; ===================================================================================================
+;; for/extflvector:
+
+(check-equal? (for/extflvector: #:length 4 ([i  (in-range 4)])
+                (real->extfl i))
+              (extflvector 0.0t0 1.0t0 2.0t0 3.0t0))
+
+(check-equal? (for/extflvector: #:length 4 ([i  (in-range 0)])
+                (real->extfl i))
+              (extflvector 0.0t0 0.0t0 0.0t0 0.0t0))
+
+(check-equal? (for/extflvector: #:length 4 ()
+                1.2t0)
+              (extflvector 1.2t0 0.0t0 0.0t0 0.0t0))
+
+(check-equal? (for/extflvector: #:length 4 ([i  (in-range 2)])
+                (real->extfl i))
+              (extflvector 0.0t0 1.0t0 0.0t0 0.0t0))
+
+(check-equal? (for/extflvector: #:length 4 ([i  (in-range 5)])
+                (real->extfl i))
+              (extflvector 0.0t0 1.0t0 2.0t0 3.0t0))
+
+(check-equal? (for/extflvector: #:length 0 ([i  (in-range 5)])
+                (real->extfl i))
+              (extflvector))
+
+(check-equal? (for/extflvector: ([i  (in-range 4)])
+                (real->extfl i))
+              (extflvector 0.0t0 1.0t0 2.0t0 3.0t0))
+
+(check-equal? (for/extflvector: () 1.2t0)
+              (extflvector 1.2t0))
+
+(check-equal? (for/extflvector: ([i  (in-range 0)])
+                (real->extfl i))
+              (extflvector))
+
+(check-equal? (for/extflvector: #:length 4 ([x  (in-range 2)]
+                                            #:when #t
+                                            [y  (in-range 2)])
+                (real->extfl (+ x y)))
+              (extflvector 0.0t0 1.0t0 1.0t0 2.0t0))
+
+(check-equal? (for/extflvector: #:length 4 ([x  (in-range 0)]
+                                            #:when #t
+                                            [y  (in-range 2)])
+                (real->extfl (+ x y)))
+              (extflvector 0.0t0 0.0t0 0.0t0 0.0t0))
+
+(check-equal? (for/extflvector: #:length 4 ([x  (in-range 2)]
+                                            #:when #t
+                                            [y  (in-range 1)])
+                (real->extfl (+ x y)))
+              (extflvector 0.0t0 1.0t0 0.0t0 0.0t0))
+
+(check-equal? (for/extflvector: #:length 4 ([x  (in-range 2)]
+                                            #:when #t
+                                            [y  (in-range 3)])
+                (real->extfl (+ x y)))
+              (extflvector 0.0t0 1.0t0 2.0t0 1.0t0))
+
+(check-equal? (for/extflvector: #:length 0 ([x  (in-range 2)]
+                                            #:when #t
+                                            [y  (in-range 3)])
+                (real->extfl (+ x y)))
+              (extflvector))
+
+(check-equal? (for/extflvector: ([x  (in-range 2)]
+                                 #:when #t
+                                 [y  (in-range 2)])
+                (real->extfl (+ x y)))
+              (extflvector 0.0t0 1.0t0 1.0t0 2.0t0))
+
+(check-equal? (for/extflvector: ([x  (in-range 0)]
+                                 #:when #t
+                                 [y  (in-range 2)])
+                (real->extfl (+ x y)))
+              (extflvector))
+
+;; ===================================================================================================
+;; for*/extflvector:
+
+(check-equal? (for*/extflvector: #:length 4 ([i  (in-range 4)])
+                (real->extfl i))
+              (extflvector 0.0t0 1.0t0 2.0t0 3.0t0))
+
+(check-equal? (for*/extflvector: #:length 4 ([i  (in-range 0)])
+                (real->extfl i))
+              (extflvector 0.0t0 0.0t0 0.0t0 0.0t0))
+
+(check-equal? (for*/extflvector: #:length 4 ()
+                1.2t0)
+              (extflvector 1.2t0 0.0t0 0.0t0 0.0t0))
+
+(check-equal? (for*/extflvector: #:length 4 ([i  (in-range 2)])
+                (real->extfl i))
+              (extflvector 0.0t0 1.0t0 0.0t0 0.0t0))
+
+(check-equal? (for*/extflvector: #:length 4 ([i  (in-range 5)])
+                (real->extfl i))
+              (extflvector 0.0t0 1.0t0 2.0t0 3.0t0))
+
+(check-equal? (for*/extflvector: #:length 0 ([i  (in-range 5)])
+                (real->extfl i))
+              (extflvector))
+
+(check-equal? (for*/extflvector: ([i  (in-range 4)])
+                (real->extfl i))
+              (extflvector 0.0t0 1.0t0 2.0t0 3.0t0))
+
+(check-equal? (for*/extflvector: () 1.2t0)
+              (extflvector 1.2t0))
+
+(check-equal? (for*/extflvector: ([i  (in-range 0)])
+                (real->extfl i))
+              (extflvector))
+
+(check-equal? (for*/extflvector: #:length 4 ([x  (in-range 2)]
+                                             [y  (in-range 2)])
+                (real->extfl (+ x y)))
+              (extflvector 0.0t0 1.0t0 1.0t0 2.0t0))
+
+(check-equal? (for*/extflvector: #:length 4 ([x  (in-range 0)]
+                                             [y  (in-range 2)])
+                (real->extfl (+ x y)))
+              (extflvector 0.0t0 0.0t0 0.0t0 0.0t0))
+
+(check-equal? (for*/extflvector: #:length 4 ([x  (in-range 2)]
+                                             [y  (in-range 1)])
+                (real->extfl (+ x y)))
+              (extflvector 0.0t0 1.0t0 0.0t0 0.0t0))
+
+(check-equal? (for*/extflvector: #:length 4 ([x  (in-range 2)]
+                                             [y  (in-range 3)])
+                (real->extfl (+ x y)))
+              (extflvector 0.0t0 1.0t0 2.0t0 1.0t0))
+
+(check-equal? (for*/extflvector: #:length 0 ([x  (in-range 2)]
+                                             [y  (in-range 3)])
+                (real->extfl (+ x y)))
+              (extflvector))
+
+(check-equal? (for*/extflvector: ([x  (in-range 2)]
+                                  [y  (in-range 2)])
+                (real->extfl (+ x y)))
+              (extflvector 0.0t0 1.0t0 1.0t0 2.0t0))
+
+(check-equal? (for*/extflvector: ([x  (in-range 0)]
+                                  [y  (in-range 2)])
+                (real->extfl (+ x y)))
+              (extflvector))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/pr13464.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/pr13464.rkt
index d29fe7a2..d9a6b0bd 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/pr13464.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/pr13464.rkt
@@ -22,6 +22,11 @@
   (: pos-real     Positive-Real)
   (: non-neg-real Nonnegative-Real)
   (: non-pos-real Nonpositive-Real)
+  
+  (: neg-extflonum     Negative-ExtFlonum)
+  (: pos-extflonum     Positive-ExtFlonum)
+  (: non-neg-extflonum Nonnegative-ExtFlonum)
+  (: non-pos-extflonum Nonpositive-ExtFlonum)
 
 
   (define neg-flonum     +nan.0)
@@ -44,7 +49,12 @@
   (define non-neg-real +nan.0)
   (define non-pos-real +nan.0)
 
+  (define neg-extflonum     +nan.t)
+  (define pos-extflonum     +nan.t)
+  (define non-neg-extflonum +nan.t)
+  (define non-pos-extflonum +nan.t)
 
+  
   ;; extra tests for zeroes
   (: non-neg-flonum+0 Nonnegative-Flonum)
   (: non-pos-flonum+0 Nonpositive-Flonum)
@@ -66,6 +76,11 @@
   (: non-neg-real-0 Nonnegative-Real)
   (: non-pos-real-0 Nonpositive-Real)
 
+  (: non-neg-extflonum+0 Nonnegative-ExtFlonum)
+  (: non-pos-extflonum+0 Nonpositive-ExtFlonum)
+  (: non-neg-extflonum-0 Nonnegative-ExtFlonum)
+  (: non-pos-extflonum-0 Nonpositive-ExtFlonum)
+
   (define non-neg-flonum+0 0.0)
   (define non-pos-flonum+0 0.0)
   (define non-neg-flonum-0 -0.0)
@@ -85,6 +100,11 @@
   (define non-pos-real+0 0.0)
   (define non-neg-real-0 -0.0)
   (define non-pos-real-0 -0.0)
+
+  (define non-neg-extflonum+0 0.0t0)
+  (define non-pos-extflonum+0 0.0t0)
+  (define non-neg-extflonum-0 -0.0t0)
+  (define non-pos-extflonum-0 -0.0t0)
   )
 
 
@@ -106,6 +126,10 @@ neg-real
 pos-real
 non-neg-real
 non-pos-real
+neg-extflonum
+pos-extflonum
+non-neg-extflonum
+non-pos-extflonum
 
 non-neg-flonum+0
 non-pos-flonum+0
@@ -126,3 +150,8 @@ non-neg-real+0
 non-pos-real+0
 non-neg-real-0
 non-pos-real-0
+
+non-neg-extflonum+0
+non-pos-extflonum+0
+non-neg-extflonum-0
+non-pos-extflonum-0
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
index 4632771b..bfb7e485 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
@@ -268,6 +268,7 @@
   racket/file
   racket/fixnum
   racket/flonum
+  racket/extflonum
   racket/function
   racket/future
   racket/list
@@ -399,6 +400,9 @@
         (tc-e (flexpt 0.5 0.3) -NonNegFlonum)
         (tc-e (flexpt 0.00000000001 100000000000.0) -NonNegFlonum)
         (tc-e (flexpt -2.0 -0.5) -Flonum) ; NaN
+        (tc-e (extflexpt 0.5t0 0.3t0) -NonNegExtFlonum)
+        (tc-e (extflexpt 0.00000000001t0 100000000000.0t0) -NonNegExtFlonum)
+        (tc-e (extflexpt -2.0t0 -0.5t0) -ExtFlonum) ; NaN
         (tc-e (tanh (ann 0 Nonnegative-Integer)) -NonNegReal)
         (tc-e (sinh (ann 0 Nonpositive-Integer)) -NonPosReal)
         (tc-e (angle -1) (t:Un -InexactReal -Zero))
@@ -2163,8 +2167,10 @@
                (define f1 (sequence-ref s1 0))
                (define s2 (in-fxvector (fxvector 1 2 3)))
                (define f2 (sequence-ref s2 2))
-               (list f1 f2))
-             (-lst* -Flonum -Fixnum)]
+               (define s3 (in-extflvector (extflvector 1.0t0 2.0t0 3.0t0)))
+               (define f3 (sequence-ref s3 1))
+               (list f1 f2 f3))
+             (-lst* -Flonum -Fixnum -ExtFlonum)]
 
        ;; for/hash, for*/hash - PR 14306
        [tc-e (for/hash: : (HashTable Symbol String)
@@ -2807,6 +2813,14 @@
    (tc-l -5# -NegFlonum)
    (tc-l -5.0 -NegFlonum)
    (tc-l -5.1 -NegFlonum)
+   (tc-l 0.0t0 -ExtFlonumPosZero)
+   (tc-l -0.0t0 -ExtFlonumNegZero)
+   (tc-l 5#t0 -PosExtFlonum)
+   (tc-l 5.0t0 -PosExtFlonum)
+   (tc-l 5.1t0 -PosExtFlonum)
+   (tc-l -5#t0 -NegExtFlonum)
+   (tc-l -5.0t0 -NegExtFlonum)
+   (tc-l -5.1t0 -NegExtFlonum)
    (tc-l 1+1i -ExactNumber)
    (tc-l 1+1.0i -FloatComplex)
    (tc-l 1.0+1i -FloatComplex)