diff --git a/CHANGELOG.d/internal_type-traversals.md b/CHANGELOG.d/internal_type-traversals.md
new file mode 100644
index 0000000000..2bba7424a5
--- /dev/null
+++ b/CHANGELOG.d/internal_type-traversals.md
@@ -0,0 +1,4 @@
+* Fix incomplete type traversals
+
+  This corrects oversights in some compiler internals that are not known to be
+  the cause of any user-facing issues.
diff --git a/purescript.cabal b/purescript.cabal
index fdad946654..cfbfd78500 100644
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -144,6 +144,7 @@ common defaults
     Glob >=0.10.1 && <0.11,
     haskeline >=0.8.2 && <0.9,
     language-javascript ==0.7.0.0,
+    lens >=4.19.2 && <4.20,
     lifted-async >=0.10.2.2 && <0.11,
     lifted-base >=0.2.3.12 && <0.3,
     memory >=0.15.0 && <0.16,
@@ -401,8 +402,10 @@ test-suite tests
   main-is: Main.hs
   build-depends:
       purescript
+    , generic-random
     , hspec
     , HUnit
+    , newtype
     , QuickCheck
     , regex-base
   build-tool-depends:
@@ -421,6 +424,7 @@ test-suite tests
     Language.PureScript.Ide.Test
     Language.PureScript.Ide.UsageSpec
     PscIdeSpec
+    TestAst
     TestCompiler
     TestCoreFn
     TestCst
diff --git a/src/Language/PureScript/Errors.hs b/src/Language/PureScript/Errors.hs
index 2d89b49b81..ec030cc6b0 100644
--- a/src/Language/PureScript/Errors.hs
+++ b/src/Language/PureScript/Errors.hs
@@ -429,7 +429,7 @@ unwrapErrorMessage :: ErrorMessage -> SimpleErrorMessage
 unwrapErrorMessage (ErrorMessage _ se) = se
 
 replaceUnknowns :: SourceType -> State TypeMap SourceType
-replaceUnknowns = everywhereOnTypesM replaceTypes where
+replaceUnknowns = everywhereOnTypesTopDownM replaceTypes where
   replaceTypes :: SourceType -> State TypeMap SourceType
   replaceTypes (TUnknown ann u) = do
     m <- get
@@ -439,14 +439,17 @@ replaceUnknowns = everywhereOnTypesM replaceTypes where
         put $ m { umUnknownMap = M.insert u u' (umUnknownMap m), umNextIndex = u' + 1 }
         return (TUnknown ann u')
       Just u' -> return (TUnknown ann u')
-  replaceTypes (Skolem ann name mbK s sko) = do
+  -- We intentionally remove the kinds from skolems, because they are never
+  -- presented when pretty-printing. Any unknowns in those kinds shouldn't
+  -- appear in the list of unknowns unless used somewhere else.
+  replaceTypes (Skolem ann name _ s sko) = do
     m <- get
     case M.lookup s (umSkolemMap m) of
       Nothing -> do
         let s' = umNextIndex m
         put $ m { umSkolemMap = M.insert s (T.unpack name, s', Just (fst ann)) (umSkolemMap m), umNextIndex = s' + 1 }
-        return (Skolem ann name mbK s' sko)
-      Just (_, s', _) -> return (Skolem ann name mbK s' sko)
+        return (Skolem ann name Nothing s' sko)
+      Just (_, s', _) -> return (Skolem ann name Nothing s' sko)
   replaceTypes other = return other
 
 onTypesInErrorMessage :: (SourceType -> SourceType) -> ErrorMessage -> ErrorMessage
diff --git a/src/Language/PureScript/TypeChecker/Entailment/Coercible.hs b/src/Language/PureScript/TypeChecker/Entailment/Coercible.hs
index bb16e25b62..ba06ea55c7 100644
--- a/src/Language/PureScript/TypeChecker/Entailment/Coercible.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment/Coercible.hs
@@ -527,6 +527,10 @@ insoluble
   -> SourceType
   -> MultipleErrors
 insoluble k a b =
+  -- We can erase kind applications when determining whether to show the
+  -- "Consider adding a type annotation" hint, because annotating kinds to
+  -- instantiate unknowns in Coercible constraints should never resolve
+  -- NoInstanceFound errors.
   errorMessage $ NoInstanceFound (srcConstraint Prim.Coercible [k] [a, b] Nothing) [] (any containsUnknowns [a, b])
 
 -- | Constraints of the form @Coercible a b@ can be solved if the two arguments
diff --git a/src/Language/PureScript/Types.hs b/src/Language/PureScript/Types.hs
index 1be0077735..ca942e543b 100644
--- a/src/Language/PureScript/Types.hs
+++ b/src/Language/PureScript/Types.hs
@@ -559,8 +559,10 @@ unknowns = everythingOnTypes (<>) go where
   go (TUnknown _ u) = IS.singleton u
   go _ = mempty
 
+-- | Check if a type contains unknowns in a position that is relevant to
+-- constraint solving. (Kinds are not.)
 containsUnknowns :: Type a -> Bool
-containsUnknowns = everythingOnTypes (||) go where
+containsUnknowns = everythingOnTypes (||) go . eraseKindApps where
   go :: Type a -> Bool
   go TUnknown{} = True
   go _ = False
@@ -570,6 +572,8 @@ eraseKindApps = everywhereOnTypes $ \case
   KindApp _ ty _ -> ty
   ConstrainedType ann con ty ->
     ConstrainedType ann (con { constraintKindArgs = [] }) ty
+  Skolem ann name _ i sc ->
+    Skolem ann name Nothing i sc
   other -> other
 
 eraseForAllKindAnnotations :: Type a -> Type a
@@ -621,6 +625,7 @@ everywhereOnTypes f = go where
   go (KindApp ann t1 t2) = f (KindApp ann (go t1) (go t2))
   go (ForAll ann arg mbK ty sco) = f (ForAll ann arg (go <$> mbK) (go ty) sco)
   go (ConstrainedType ann c ty) = f (ConstrainedType ann (mapConstraintArgsAll (map go) c) (go ty))
+  go (Skolem ann name mbK i sc) = f (Skolem ann name (go <$> mbK) i sc)
   go (RCons ann name ty rest) = f (RCons ann name (go ty) (go rest))
   go (KindedType ann ty k) = f (KindedType ann (go ty) (go k))
   go (BinaryNoParensType ann t1 t2 t3) = f (BinaryNoParensType ann (go t1) (go t2) (go t3))
@@ -633,6 +638,7 @@ everywhereOnTypesM f = go where
   go (KindApp ann t1 t2) = (KindApp ann <$> go t1 <*> go t2) >>= f
   go (ForAll ann arg mbK ty sco) = (ForAll ann arg <$> traverse go mbK <*> go ty <*> pure sco) >>= f
   go (ConstrainedType ann c ty) = (ConstrainedType ann <$> overConstraintArgsAll (mapM go) c <*> go ty) >>= f
+  go (Skolem ann name mbK i sc) = (Skolem ann name <$> traverse go mbK <*> pure i <*> pure sc) >>= f
   go (RCons ann name ty rest) = (RCons ann name <$> go ty <*> go rest) >>= f
   go (KindedType ann ty k) = (KindedType ann <$> go ty <*> go k) >>= f
   go (BinaryNoParensType ann t1 t2 t3) = (BinaryNoParensType ann <$> go t1 <*> go t2 <*> go t3) >>= f
@@ -645,11 +651,12 @@ everywhereOnTypesTopDownM f = go <=< f where
   go (KindApp ann t1 t2) = KindApp ann <$> (f t1 >>= go) <*> (f t2 >>= go)
   go (ForAll ann arg mbK ty sco) = ForAll ann arg <$> traverse (f >=> go) mbK <*> (f ty >>= go) <*> pure sco
   go (ConstrainedType ann c ty) = ConstrainedType ann <$> overConstraintArgsAll (mapM (go <=< f)) c <*> (f ty >>= go)
+  go (Skolem ann name mbK i sc) = Skolem ann name <$> traverse (f >=> go) mbK <*> pure i <*> pure sc
   go (RCons ann name ty rest) = RCons ann name <$> (f ty >>= go) <*> (f rest >>= go)
   go (KindedType ann ty k) = KindedType ann <$> (f ty >>= go) <*> (f k >>= go)
   go (BinaryNoParensType ann t1 t2 t3) = BinaryNoParensType ann <$> (f t1 >>= go) <*> (f t2 >>= go) <*> (f t3 >>= go)
   go (ParensInType ann t) = ParensInType ann <$> (f t >>= go)
-  go other = f other
+  go other = pure other
 
 everythingOnTypes :: (r -> r -> r) -> (Type a -> r) -> Type a -> r
 everythingOnTypes (<+>) f = go where
@@ -658,6 +665,7 @@ everythingOnTypes (<+>) f = go where
   go t@(ForAll _ _ (Just k) ty _) = f t <+> go k <+> go ty
   go t@(ForAll _ _ _ ty _) = f t <+> go ty
   go t@(ConstrainedType _ c ty) = foldl (<+>) (f t) (map go (constraintKindArgs c) ++ map go (constraintArgs c)) <+> go ty
+  go t@(Skolem _ _ (Just k) _ _) = f t <+> go k
   go t@(RCons _ _ ty rest) = f t <+> go ty <+> go rest
   go t@(KindedType _ ty k) = f t <+> go ty <+> go k
   go t@(BinaryNoParensType _ t1 t2 t3) = f t <+> go t1 <+> go t2 <+> go t3
@@ -672,6 +680,7 @@ everythingWithContextOnTypes s0 r0 (<+>) f = go' s0 where
   go s (ForAll _ _ (Just k) ty _) = go' s k <+> go' s ty
   go s (ForAll _ _ _ ty _) = go' s ty
   go s (ConstrainedType _ c ty) = foldl (<+>) r0 (map (go' s) (constraintKindArgs c) ++ map (go' s) (constraintArgs c)) <+> go' s ty
+  go s (Skolem _ _ (Just k) _ _) = go' s k
   go s (RCons _ _ ty rest) = go' s ty <+> go' s rest
   go s (KindedType _ ty k) = go' s ty <+> go' s k
   go s (BinaryNoParensType _ t1 t2 t3) = go' s t1 <+> go' s t2 <+> go' s t3
diff --git a/tests/Main.hs b/tests/Main.hs
index c61dd473d5..5d202bae64 100644
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -7,6 +7,7 @@ import Prelude.Compat
 
 import Test.Hspec
 
+import qualified TestAst
 import qualified TestCompiler
 import qualified TestCoreFn
 import qualified TestCst
@@ -32,6 +33,7 @@ main = do
 
   hspec $ do
     describe "cst" TestCst.spec
+    describe "ast" TestAst.spec
     describe "ide" TestIde.spec
     beforeAll TestUtils.setupSupportModules $ do
       describe "compiler" TestCompiler.spec
diff --git a/tests/TestAst.hs b/tests/TestAst.hs
new file mode 100644
index 0000000000..a7d0439d2e
--- /dev/null
+++ b/tests/TestAst.hs
@@ -0,0 +1,94 @@
+{-# LANGUAGE TypeApplications #-}
+module TestAst where
+
+import Protolude hiding (Constraint, Type, (:+))
+
+import Control.Lens ((+~))
+import Control.Newtype (ala')
+import Generic.Random
+import Test.Hspec
+import Test.QuickCheck
+
+import Language.PureScript.Label
+import Language.PureScript.Names
+import Language.PureScript.PSString
+import Language.PureScript.Types
+
+spec :: Spec
+spec = do
+  describe "Language.PureScript.Types" $ do
+    describe "everywhereOnTypes" $ do
+      everywhereOnTypesSpec everywhereOnTypes
+    describe "everywhereOnTypesM" $ do
+      everywhereOnTypesSpec $ ala' Identity everywhereOnTypesM
+    describe "everywhereOnTypesTopDownM" $ do
+      everywhereOnTypesSpec $ ala' Identity everywhereOnTypesTopDownM
+    describe "everythingOnTypes" $ do
+      everythingOnTypesSpec everythingOnTypes
+    describe "everythingWithContextOnTypes" $ do
+      everythingOnTypesSpec $ \f g -> everythingWithContextOnTypes () [] f $ \s -> (s, ) . g
+
+everywhereOnTypesSpec :: ((Type Int -> Type Int) -> Type Int -> Type Int) -> Spec
+everywhereOnTypesSpec everywhereOnTypesUnderTest = do
+  it "should visit each type once" $
+    forAllShrink (genTypeAnnotatedWith (pure 0) (pure 1)) subterms $ \t ->
+      all (== 1) `isSatisfiedBy` everywhereOnTypesUnderTest (annForType +~ 1) t
+
+everythingOnTypesSpec :: (([Int] -> [Int] -> [Int]) -> (Type Int -> [Int]) -> Type Int -> [Int]) -> Spec
+everythingOnTypesSpec everythingOnTypesUnderTest = do
+  it "should visit each type once" $
+    forAllShrink (genTypeAnnotatedWith (pure 1) (pure 0)) subterms $ \t ->
+      everythingOnTypesUnderTest (++) (pure . getAnnForType) t ===
+        filter (== 1) (toList t)
+
+
+infixr 0 `isSatisfiedBy`
+isSatisfiedBy :: forall a p. Show a => Testable p => (a -> p) -> a -> Property
+isSatisfiedBy = liftA2 counterexample show
+
+genTypeAnnotatedWith :: forall a. Gen a -> Gen a -> Gen (Type a)
+genTypeAnnotatedWith genTypeAnn genConstraintAnn = genType where
+  generatorEnvironment
+    =  genConstraint
+    :+ maybeOf genConstraintData
+    :+ Label <$> genPSString
+    :+ genPSString
+    :+ genQualified (OpName @'TypeOpName)
+    :+ genQualified (ProperName @'ClassName)
+    :+ genQualified (ProperName @'TypeName)
+    :+ genSkolemScope
+    :+ maybeOf genSkolemScope
+    :+ genText
+    :+ listOf' (listOf' genText)
+    :+ maybeOf genText
+    :+ genType
+    :+ listOf' genType
+    :+ maybeOf genType
+    :+ genWildcardData
+
+  genConstraint :: Gen (Constraint a)
+  genConstraint = genericArbitraryUG (genConstraintAnn :+ generatorEnvironment)
+
+  genConstraintData :: Gen ConstraintData
+  genConstraintData = genericArbitraryUG generatorEnvironment
+
+  genQualified :: forall b. (Text -> b) -> Gen (Qualified b)
+  genQualified ctor = Qualified Nothing . ctor <$> genText
+
+  genSkolemScope :: Gen SkolemScope
+  genSkolemScope = SkolemScope <$> arbitrary
+
+  genType :: Gen (Type a)
+  genType = genericArbitraryRecG (genTypeAnn :+ generatorEnvironment) uniform `withBaseCase` (TypeVar <$> genTypeAnn <*> genText)
+
+  genWildcardData :: Gen WildcardData
+  genWildcardData = genericArbitraryUG genText
+
+  maybeOf :: forall b. Gen b -> Gen (Maybe b)
+  maybeOf = genericArbitraryUG
+
+  genText :: Gen Text
+  genText = pure "x" -- Feel free to make this random if it matters at some point.
+
+  genPSString :: Gen PSString
+  genPSString = pure "x" -- Ditto.