diff --git a/typed-racket-lib/typed-racket/types/abbrev.rkt b/typed-racket-lib/typed-racket/types/abbrev.rkt
index f507a697..23a22e02 100644
--- a/typed-racket-lib/typed-racket/types/abbrev.rkt
+++ b/typed-racket-lib/typed-racket/types/abbrev.rkt
@@ -121,20 +121,23 @@
 (define/decl -Thread (make-Base 'Thread #'thread? thread?))
 (define/decl -Path (make-Base 'Path #'path? path?))
 (define/decl -Module-Path
-  (Un -Symbol -String -Path
-      (-lst* (-val 'quote) -Symbol)
-      (-lst* (-val 'lib) -String)
-      (-lst* (-val 'file) -String)
-      (-pair (-val 'planet)
-	     (Un (-lst* -Symbol)
-		 (-lst* -String)
-		 (-lst* -String
-			(-lst*
-			 -String -String
-			 #:tail (make-Listof
-				 (Un -Nat
-				     (-lst* (Un -Nat (one-of/c '= '+ '-))
-					    -Nat)))))))))
+  (-mu X
+       (Un -Symbol -String -Path
+           (-lst* (-val 'quote) -Symbol)
+           (-lst* (-val 'lib) -String)
+           (-lst* (-val 'file) -String)
+           (-pair (-val 'planet)
+                  (Un (-lst* -Symbol)
+                      (-lst* -String)
+                      (-lst* -String
+                             (-lst*
+                              -String -String
+                              #:tail (make-Listof
+                                      (Un -Nat
+                                          (-lst* (Un -Nat (one-of/c '= '+ '-))
+                                                 -Nat)))))))
+           (-lst* (-val 'submod) X
+                  #:tail (-lst (Un -Symbol (-val "..")))))))
 (define/decl -Resolved-Module-Path (make-Base 'Resolved-Module-Path #'resolved-module-path? resolved-module-path?))
 (define/decl -Module-Path-Index (make-Base 'Module-Path-Index #'module-path-index? module-path-index?))
 (define/decl -Compiled-Module-Expression (make-Base 'Compiled-Module-Expression #'compiled-module-expression? compiled-module-expression?))
diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt
index 75e86dd1..9ebbe5a7 100644
--- a/typed-racket-test/unit-tests/typecheck-tests.rkt
+++ b/typed-racket-test/unit-tests/typecheck-tests.rkt
@@ -3740,6 +3740,24 @@
                               (-result -Boolean (-FS (-filter -NonPosFlonum 0) -top))
                               (-result -Boolean)
                               (-result -Boolean))))]
+
+       ;; Tests for Module-Path
+       [tc-e/t (ann "x" Module-Path) -Module-Path]
+       [tc-e/t (ann 'x Module-Path) -Module-Path]
+       [tc-e/t (ann '(planet x) Module-Path) -Module-Path]
+       [tc-e/t (ann '(planet "foo") Module-Path) -Module-Path]
+       [tc-e/t (ann '(planet "foo" ("x" "y" 1 2)) Module-Path) -Module-Path]
+       [tc-e/t (ann '(submod "foo" foo) Module-Path) -Module-Path]
+       [tc-e/t (ann '(submod "." bar) Module-Path) -Module-Path]
+       [tc-e/t (ann '(submod ".." bar) Module-Path) -Module-Path]
+       ;; Need an `ann` here because TR doesn't typecheck the literal ".."
+       ;; with a precise enough type to satisfy Module-Path
+       [tc-e (ann `(submod ".." bar ,(ann ".." "..")) Module-Path)
+             #:ret (ret -Module-Path)
+             #:expected (ret -Module-Path)]
+       [tc-e/t (ann '(lib "foo") Module-Path) -Module-Path]
+       [tc-err (begin (ann '(submod ".." bar ".") Module-Path)
+                      (error "foo"))]
        )
 
   (test-suite