diff --git a/lib/purescript-ast/src/Language/PureScript/AST/Declarations.hs b/lib/purescript-ast/src/Language/PureScript/AST/Declarations.hs
index 5b451e904c..84ebd129e5 100644
--- a/lib/purescript-ast/src/Language/PureScript/AST/Declarations.hs
+++ b/lib/purescript-ast/src/Language/PureScript/AST/Declarations.hs
@@ -382,6 +382,9 @@ data DataConstructorDeclaration = DataConstructorDeclaration
   , dataCtorFields :: ![(Ident, SourceType)]
   } deriving (Show, Eq)
 
+mapDataCtorFields :: ([(Ident, SourceType)] -> [(Ident, SourceType)]) -> DataConstructorDeclaration -> DataConstructorDeclaration
+mapDataCtorFields f DataConstructorDeclaration{..} = DataConstructorDeclaration { dataCtorFields = f dataCtorFields, .. }
+
 traverseDataCtorFields :: Monad m => ([(Ident, SourceType)] -> m [(Ident, SourceType)]) -> DataConstructorDeclaration -> m DataConstructorDeclaration
 traverseDataCtorFields f DataConstructorDeclaration{..} = DataConstructorDeclaration dataCtorAnn dataCtorName <$> f dataCtorFields
 
diff --git a/lib/purescript-ast/src/Language/PureScript/Environment.hs b/lib/purescript-ast/src/Language/PureScript/Environment.hs
index f2324e413e..229cebb4b5 100644
--- a/lib/purescript-ast/src/Language/PureScript/Environment.hs
+++ b/lib/purescript-ast/src/Language/PureScript/Environment.hs
@@ -408,7 +408,7 @@ primBooleanTypes =
 primCoerceTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
 primCoerceTypes =
   M.fromList $ mconcat
-    [ primClass (primSubName C.moduleCoerce "Coercible") (\kind -> kindType -:> kindType -:> kind)
+    [ primClass (primSubName C.moduleCoerce "Coercible") (\kind -> tyForall "k" kindType $ tyVar "k" -:> tyVar "k" -:> kind)
     ]
 
 primOrderingTypes :: M.Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
@@ -485,9 +485,10 @@ allPrimClasses = M.unions
 primCoerceClasses :: M.Map (Qualified (ProperName 'ClassName)) TypeClassData
 primCoerceClasses =
   M.fromList
+    -- class Coercible (a :: k) (b :: k)
     [ (primSubName C.moduleCoerce "Coercible", makeTypeClassData
-        [ ("a", Just kindType)
-        , ("b", Just kindType)
+        [ ("a", Just (tyVar "k"))
+        , ("b", Just (tyVar "k"))
         ] [] [] [] True)
     ]
 
@@ -635,8 +636,11 @@ nominalRolesForKind :: Type a -> [Role]
 nominalRolesForKind k = replicate (kindArity k) Nominal
 
 kindArity :: Type a -> Int
-kindArity = go 0 where
-  go n (TypeApp _ (TypeApp _ fn _) k)
-    | eqType fn tyFunction = go (n + 1) k
-  go n (ForAll _ _ _ k _) = go n k
-  go n _ = n
+kindArity = length . fst . unapplyKinds
+
+unapplyKinds :: Type a -> ([Type a], Type a)
+unapplyKinds = go [] where
+  go kinds (TypeApp _ (TypeApp _ fn k1) k2)
+    | eqType fn tyFunction = go (k1 : kinds) k2
+  go kinds (ForAll _ _ _ k _) = go kinds k
+  go kinds k = (reverse kinds, k)
diff --git a/src/Language/PureScript/Docs/Prim.hs b/src/Language/PureScript/Docs/Prim.hs
index f06a5dce74..e99854a414 100644
--- a/src/Language/PureScript/Docs/Prim.hs
+++ b/src/Language/PureScript/Docs/Prim.hs
@@ -393,7 +393,7 @@ coercible = primClassOf (P.primSubName "Coerce") "Coercible" $ T.unlines
   , ""
   , "there is an instance:"
   , ""
-  , "    coercibleConstructor :: Coercible a a' => Coercible (D a b) (D a' b')"
+  , "    instance coercibleConstructor :: Coercible a a' => Coercible (D a b) (D a' b')"
   , ""
   , "Note that, since the type variable `a` plays a role in `D`'s representation,"
   , "we require that the types `a` and `a'` are themselves `Coercible`. However,"
@@ -408,7 +408,22 @@ coercible = primClassOf (P.primSubName "Coerce") "Coercible" $ T.unlines
   , "    instance coercibleNewtypeRight :: Coercible T b => Coercible NT b"
   , ""
   , "To prevent breaking abstractions, these instances are only usable if the"
-  , "constructor `MkNT` is in scope."
+  , "constructor `MkNT` is exported."
+  , ""
+  , "Fourth, every pair of unsaturated type constructors can be coerced if"
+  , "there is an instance for the fully saturated types. For example,"
+  , "given the definitions:"
+  , ""
+  , "newtype NT1 a = MkNT1 a"
+  , "newtype NT2 a b = MkNT2 b"
+  , ""
+  , "there is an instance:"
+  , ""
+  , "    instance coercibleUnsaturedTypes :: Coercible (NT1 b) (NT2 a b) => Coercible NT1 (NT2 a)"
+  , ""
+  , "This rule may seem puzzling since it is impossible to apply `coerce` to a term"
+  , "of type `NT1` but it is necessary to coerce types with higher kinded parameters."
+  , ""
   ]
 
 kindOrdering :: Declaration
diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index 7ef955e790..02fb947cf7 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -14,17 +14,18 @@ module Language.PureScript.TypeChecker.Entailment
 import Prelude.Compat
 import Protolude (ordNub)
 
-import Control.Applicative ((<|>))
+import Control.Applicative ((<|>), empty)
 import Control.Arrow (second, (&&&))
 import Control.Monad.Error.Class (MonadError(..))
 import Control.Monad.State
 import Control.Monad.Supply.Class (MonadSupply(..))
+import Control.Monad.Trans.Maybe (MaybeT(..))
 import Control.Monad.Writer
 
-import Data.Foldable (for_, fold, toList)
+import Data.Foldable (for_, fold, foldl', toList)
 import Data.Function (on)
 import Data.Functor (($>))
-import Data.List (minimumBy, groupBy, nubBy, sortBy)
+import Data.List (minimumBy, groupBy, nubBy, sortBy, zipWith4)
 import Data.Maybe (fromMaybe, mapMaybe)
 import qualified Data.Map as M
 import qualified Data.Set as S
@@ -168,12 +169,18 @@ entails
 entails SolverOptions{..} constraint context hints =
     solve constraint
   where
+    forClassNameM :: Environment -> InstanceContext -> Qualified (ProperName 'ClassName) -> [SourceType] -> [SourceType] -> m [TypeClassDict]
+    forClassNameM env ctx cn@C.Coercible kinds args =
+      solveCoercible env kinds args >>=
+        pure . fromMaybe (forClassName env ctx cn kinds args)
+    forClassNameM env ctx cn kinds args =
+      pure $ forClassName env ctx cn kinds args
+
     forClassName :: Environment -> InstanceContext -> Qualified (ProperName 'ClassName) -> [SourceType] -> [SourceType] -> [TypeClassDict]
     forClassName _ ctx cn@C.Warn _ [msg] =
       -- Prefer a warning dictionary in scope if there is one available.
       -- This allows us to defer a warning by propagating the constraint.
       findDicts ctx cn Nothing ++ [TypeClassDictionaryInScope [] 0 (WarnInstance msg) [] C.Warn [] [] [msg] Nothing]
-    forClassName env _ C.Coercible _ args | Just dicts <- solveCoercible env args = dicts
     forClassName _ _ C.IsSymbol _ args | Just dicts <- solveIsSymbol args = dicts
     forClassName _ _ C.SymbolCompare _ args | Just dicts <- solveSymbolCompare args = dicts
     forClassName _ _ C.SymbolAppend _ args | Just dicts <- solveSymbolAppend args = dicts
@@ -225,10 +232,12 @@ entails SolverOptions{..} constraint context hints =
                 Nothing -> throwError . errorMessage $ UnknownClass className'
                 Just tcd -> pure tcd
 
+            dicts <- lift . lift $ forClassNameM env (combineContexts context inferred) className' kinds'' tys''
+
             let instances = do
                   chain <- groupBy ((==) `on` tcdChain) $
                            sortBy (compare `on` (tcdChain &&& tcdIndex)) $
-                           forClassName env (combineContexts context inferred) className' kinds'' tys''
+                           dicts
                   -- process instances in a chain in index order
                   let found = for chain $ \tcd ->
                                 -- Make sure the type unifies with the type in the type instance definition
@@ -381,80 +390,88 @@ entails SolverOptions{..} constraint context hints =
         subclassDictionaryValue dict className index =
           App (Accessor (mkString (superclassName className index)) dict) valUndefined
 
-    solveCoercible :: Environment -> [SourceType] -> Maybe [TypeClassDict]
-    solveCoercible env [a, b] = do
-      let tySynMap = typeSynonyms env
-          kindMap = types env
-          replaceTySyns = either (const Nothing) Just . replaceAllTypeSynonymsM tySynMap kindMap
-      a' <- replaceTySyns a
-      b' <- replaceTySyns b
+    solveCoercible :: Environment -> [SourceType] -> [SourceType] -> m (Maybe [TypeClassDict])
+    solveCoercible env kinds [a, b] = runMaybeT $ do
+      let kindOf = lift . (sequence . (id &&& elaborateKind)) <=< replaceAllTypeSynonyms
+      (a', kind) <- kindOf a
+      (b', kind') <- kindOf b
+      lift $ unifyKinds kind kind'
       -- Solving terminates when the two arguments are the same. Since we
       -- currently don't support higher-rank arguments in instance heads, term
       -- equality is a sufficient notion of "the same".
       if a' == b'
-        then pure [TypeClassDictionaryInScope [] 0 EmptyClassInstance [] C.Coercible [] [] [a, b] Nothing]
+        then pure [TypeClassDictionaryInScope [] 0 EmptyClassInstance [] C.Coercible [] kinds [a, b] Nothing]
         else do
           -- When solving must reduce and recurse, it doesn't matter whether we
           -- reduce the first or second argument -- if the constraint is
           -- solvable, either path will yield the same outcome. Consequently we
           -- just try the first argument first and the second argument second.
-          ws <- coercibleWanteds env a' b' <|> coercibleWanteds env b' a'
-          pure [TypeClassDictionaryInScope [] 0 EmptyClassInstance [] C.Coercible [] [] [a, b] (Just ws)]
-    solveCoercible _ _ = Nothing
+          ws <- (MaybeT $ coercibleWanteds env a' b') <|> (MaybeT $ coercibleWanteds env b' a')
+          pure [TypeClassDictionaryInScope [] 0 EmptyClassInstance [] C.Coercible [] kinds [a, b] (Just ws)]
+    solveCoercible _ _ _ = pure Nothing
 
     -- | Take two types, @a@ and @b@ representing a desired constraint
     -- @Coercible a b@ and reduce them to a set of simpler wanted constraints
     -- whose satisfaction will yield the goal.
-    coercibleWanteds :: Environment -> SourceType -> SourceType -> Maybe [SourceConstraint]
-    coercibleWanteds env a b = case a of
-      TypeConstructor _ tyName -> do
-        -- If the first argument is a plain newtype (e.g. @newtype T = T U@ and
-        -- the constraint @Coercible T b@), look up the type of its wrapped
-        -- field and yield a new wanted constraint in terms of that type
-        -- (@Coercible U b@ in the example).
-        (_, wrappedTy, _) <- lookupNewtypeConstructor env tyName
-        pure [Constraint nullSourceAnn C.Coercible [] [wrappedTy, b] Nothing]
-      t
-        | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
-        , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
-        , not (null axs) && not (null bxs) && aTyName == bTyName -> do
-            -- If both arguments are applications of the same type constructor
-            -- (e.g. @data D a b = D a@ in the constraint
-            -- @Coercible (D a b) (D a' b')@), infer the roles of the type
-            -- constructor's arguments and generate wanted constraints
-            -- appropriately (e.g. here @a@ is representational and @b@ is
-            -- phantom, yielding @Coercible a a'@).
-            let tyRoles = lookupRoles env aTyName
-                k role ax bx = case role of
-                  Nominal
-                    -- If we had first-class equality constraints, we'd just
-                    -- emit one of the form @(a ~ b)@ here and let the solver
-                    -- recurse. Since we don't we must compare the types at
-                    -- this point and fail if they don't match. This likely
-                    -- means there are cases we should be able to handle that
-                    -- we currently can't, but is at least sound.
-                    | ax == bx ->
-                        Just []
-                    | otherwise ->
-                        Nothing
-                  Representational ->
-                    Just [Constraint nullSourceAnn C.Coercible [] [ax, bx] Nothing]
-                  Phantom ->
-                    Just []
-            fmap concat $ sequence $ zipWith3 k tyRoles axs bxs
-        | (TypeConstructor _ tyName, _, xs) <- unapplyTypes t
-        , not $ null xs
-        , Just (tvs, wrappedTy, _) <- lookupNewtypeConstructor env tyName -> do
-            -- If the first argument is a newtype applied to some other types
-            -- (e.g. @newtype T a = T a@ in @Coercible (T X) b@), look up the
-            -- type of its wrapped field and yield a new wanted constraint in
-            -- terms of that type with the type arguments substituted in (e.g.
-            -- @Coercible (T[X/a]) b = Coercible X b@ in the example).
-            let wrappedTySub = replaceAllTypeVars (zip tvs xs) wrappedTy
-            pure [Constraint nullSourceAnn C.Coercible [] [wrappedTySub, b] Nothing]
-      _ ->
+    coercibleWanteds :: Environment -> SourceType -> SourceType -> m (Maybe [SourceConstraint])
+    coercibleWanteds env a b
+      | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
+      , (aTyKind, _) <- fromMaybe (internalError "coercibleWanteds: type lookup failed") $ M.lookup aTyName (types env)
+      , (aks, kind) <- unapplyKinds aTyKind
+      , length axs < length aks = do
+          -- If both arguments have kind @k1 -> k2@ (e.g. @data D a b = D a@
+          -- in the constraint @Coercible (D a) (D a')@), yield a new wanted
+          -- constraint in terms of the types saturated with the same variables
+          -- (e.g. @Coercible (D a t0) (D a' t0)@ in the exemple).
+          tys <- traverse freshTypeWithKind $ drop (length axs) aks
+          let a' = foldl' srcTypeApp a tys
+              b' = foldl' srcTypeApp b tys
+          pure $ Just [srcCoercibleConstraint kind a' b']
+      | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
+      , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
+      , not (null axs) && aTyName == bTyName
+      , (aTyKind, _) <- fromMaybe (internalError "coercibleWanteds: type lookup failed") $ M.lookup aTyName (types env)
+      = runMaybeT $ do
+          -- If both arguments are applications of the same type constructor
+          -- (e.g. @data D a b = D a@ in the constraint
+          -- @Coercible (D a b) (D a' b')@), infer the roles of the type
+          -- constructor's arguments and generate wanted constraints
+          -- appropriately (e.g. here @a@ is representational and @b@ is
+          -- phantom, yielding @Coercible a a'@).
+          let roles = lookupRoles env aTyName
+              kinds = fst $ unapplyKinds aTyKind
+              f role kx ax bx = case role of
+                Nominal
+                  -- If we had first-class equality constraints, we'd just
+                  -- emit one of the form @(a ~ b)@ here and let the solver
+                  -- recurse. Since we don't we must compare the types at
+                  -- this point and fail if they don't match. This likely
+                  -- means there are cases we should be able to handle that
+                  -- we currently can't, but is at least sound.
+                  | ax == bx ->
+                      pure []
+                  | otherwise ->
+                      empty
+                Representational ->
+                  pure [srcCoercibleConstraint kx ax bx]
+                Phantom ->
+                  pure []
+          fmap concat $ sequence $ zipWith4 f roles kinds axs bxs
+      | (TypeConstructor _ tyName, _, xs) <- unapplyTypes a
+      , Just (tvs, wrappedTy, _) <- lookupNewtypeConstructor env tyName = do
+          -- If the first argument is a newtype applied to some other types
+          -- (e.g. @newtype T a = T a@ in @Coercible (T X) b@), look up the
+          -- type of its wrapped field and yield a new wanted constraint in
+          -- terms of that type with the type arguments substituted in (e.g.
+          -- @Coercible (T[X/a]) b = Coercible X b@ in the example).
+          let wrappedTySub = replaceAllTypeVars (zip tvs xs) wrappedTy
+          pure $ Just [srcCoercibleConstraint kindType wrappedTySub b]
+      | otherwise =
         -- In all other cases we can't solve the constraint.
-        Nothing
+        pure Nothing
+
+    srcCoercibleConstraint :: SourceType -> SourceType -> SourceType -> SourceConstraint
+    srcCoercibleConstraint k a b = srcConstraint C.Coercible [k] [a, b] Nothing
 
     solveIsSymbol :: [SourceType] -> Maybe [TypeClassDict]
     solveIsSymbol [TypeLevelString ann sym] = Just [TypeClassDictionaryInScope [] 0 (IsSymbolInstance sym) [] C.IsSymbol [] [] [TypeLevelString ann sym] Nothing]
diff --git a/src/Language/PureScript/TypeChecker/Kinds.hs b/src/Language/PureScript/TypeChecker/Kinds.hs
index e3306fb488..7bd01f5e4c 100644
--- a/src/Language/PureScript/TypeChecker/Kinds.hs
+++ b/src/Language/PureScript/TypeChecker/Kinds.hs
@@ -24,6 +24,7 @@ module Language.PureScript.TypeChecker.Kinds
 
 import Prelude.Compat
 
+import Control.Arrow ((***))
 import Control.Monad
 import Control.Monad.Error.Class (MonadError(..))
 import Control.Monad.State
@@ -602,15 +603,17 @@ inferDataDeclaration moduleName (ann, tyName, tyArgs, ctors) = do
           tyCtor' = foldl (\ty -> srcTypeApp ty . srcTypeVar . fst) tyCtor tyArgs'
           ctorBinders = fmap (fmap (fmap Just)) $ sigBinders <> fmap (nullSourceAnn,) tyArgs'
       for ctors $ \ctor ->
-        fmap ((ctor,) . mkForAll ctorBinders) $ inferDataConstructor tyCtor' ctor
+        fmap (mkForAll ctorBinders) <$> inferDataConstructor tyCtor' ctor
 
 inferDataConstructor
   :: forall m. (MonadError MultipleErrors m, MonadState CheckState m)
   => SourceType
   -> DataConstructorDeclaration
-  -> m SourceType
-inferDataConstructor tyCtor =
-  flip checkKind E.kindType . foldr ((E.-:>) . snd) tyCtor . dataCtorFields
+  -> m (DataConstructorDeclaration, SourceType)
+inferDataConstructor tyCtor DataConstructorDeclaration{..} = do
+  dataCtorFields' <- traverse (traverse (flip checkKind E.kindType)) dataCtorFields
+  dataCtor <- flip (foldr ((E.-:>) . snd)) dataCtorFields' <$> checkKind tyCtor E.kindType
+  pure ( DataConstructorDeclaration { dataCtorFields = dataCtorFields', .. }, dataCtor )
 
 type TypeDeclarationArgs =
   ( SourceAnn
@@ -914,7 +917,7 @@ kindsOfAll moduleName syns dats clss = withFreshSubstitution $ do
       pure (((synName, synKind'), synBody'), unknowns synKind')
     datResultsWithUnks <- for (zip datDict datResults) $ \((datName, datKind), ctors) -> do
       datKind' <- apply datKind
-      ctors' <- traverse (traverse apply) ctors
+      ctors' <- traverse (bitraverse (traverseDataCtorFields (traverse (traverse apply))) apply) ctors
       pure (((datName, datKind'), ctors'), unknowns datKind')
     clsResultsWithUnks <- for (zip clsDict clsResults) $ \((clsName, clsKind), (args, supers, decls)) -> do
       clsKind' <- apply clsKind
@@ -951,7 +954,8 @@ kindsOfAll moduleName syns dats clss = withFreshSubstitution $ do
           (args', supers', decls', generalizeUnknownsWithVars unkBinders clsKind)
     datResultsWithKinds <- for datResultsWithUnks $ \(((datName, datKind), ctors), _) -> do
       let tyUnks = snd . fromJust $ lookup (mkQualified datName moduleName) tySubs
-          ctors' = fmap (fmap (generalizeUnknowns tyUnks . replaceTypeCtors)) ctors
+          replaceDataCtorField ty = replaceUnknownsWithVars (unknownVarNames (usedTypeVariables ty) tyUnks) $ replaceTypeCtors ty
+          ctors' = fmap (mapDataCtorFields (fmap (fmap replaceDataCtorField)) *** generalizeUnknowns tyUnks . replaceTypeCtors) ctors
       traverse_ (traverse_ checkTypeQuantification) ctors'
       pure (ctors', generalizeUnknowns tyUnks datKind)
     synResultsWithKinds <- for synResultsWithUnks $ \(((synName, synKind), synBody), _) -> do
diff --git a/tests/purs/failing/3275-DataBindingGroupErrorPos.out b/tests/purs/failing/3275-DataBindingGroupErrorPos.out
index f20c51e038..1039d74617 100644
--- a/tests/purs/failing/3275-DataBindingGroupErrorPos.out
+++ b/tests/purs/failing/3275-DataBindingGroupErrorPos.out
@@ -14,7 +14,6 @@ at tests/purs/failing/3275-DataBindingGroupErrorPos.purs:7:19 - 7:22 (line 7, co
 while checking that type Bar a
   has kind t0 -> t1
 while inferring the kind of Bar a a
-while inferring the kind of Bar a a -> Foo a
 in data binding group Bar, Foo
 
 where t0 is an unknown type
diff --git a/tests/purs/failing/CoercibleForeign.out b/tests/purs/failing/CoercibleForeign.out
index 78b9536a51..39d5f61d71 100644
--- a/tests/purs/failing/CoercibleForeign.out
+++ b/tests/purs/failing/CoercibleForeign.out
@@ -8,7 +8,7 @@ at tests/purs/failing/CoercibleForeign.purs:11:20 - 11:26 (line 11, column 20 -
                           (Foreign (Id a0) (Id b1))
                                                    
 
-while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
   is at least as general as type Foreign a0 b1 -> Foreign (Id a0) (Id b1)
 while checking that expression coerce
   has type Foreign a0 b1 -> Foreign (Id a0) (Id b1)
diff --git a/tests/purs/failing/CoercibleForeign2.out b/tests/purs/failing/CoercibleForeign2.out
index 083afcb7bf..781eb1ed9f 100644
--- a/tests/purs/failing/CoercibleForeign2.out
+++ b/tests/purs/failing/CoercibleForeign2.out
@@ -8,7 +8,7 @@ at tests/purs/failing/CoercibleForeign2.purs:9:20 - 9:26 (line 9, column 20 - li
                           (Foreign a0 b1 d3)
                                             
 
-while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
   is at least as general as type Foreign a0 b1 c2 -> Foreign a0 b1 d3
 while checking that expression coerce
   has type Foreign a0 b1 c2 -> Foreign a0 b1 d3
diff --git a/tests/purs/failing/CoercibleForeign3.out b/tests/purs/failing/CoercibleForeign3.out
index 9bf213691d..12f68bff9a 100644
--- a/tests/purs/failing/CoercibleForeign3.out
+++ b/tests/purs/failing/CoercibleForeign3.out
@@ -8,7 +8,7 @@ at tests/purs/failing/CoercibleForeign3.purs:9:20 - 9:26 (line 9, column 20 - li
                           (Foreign @k0 a1 c3)
                                              
 
-while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
   is at least as general as type Foreign @k0 a1 b2 -> Foreign @k0 a1 c3
 while checking that expression coerce
   has type Foreign @k0 a1 b2 -> Foreign @k0 a1 c3
diff --git a/tests/purs/failing/CoercibleHigherKindedData.out b/tests/purs/failing/CoercibleHigherKindedData.out
new file mode 100644
index 0000000000..7800515797
--- /dev/null
+++ b/tests/purs/failing/CoercibleHigherKindedData.out
@@ -0,0 +1,28 @@
+Error found:
+in module Main
+at tests/purs/failing/CoercibleHigherKindedData.purs:13:17 - 13:23 (line 13, column 17 - line 13, column 23)
+
+  No type class instance was found for
+                                                
+    Prim.Coerce.Coercible (Unary @t4 t5)        
+                          (Binary @t2 @t4 a3 t5)
+                                                
+  The instance head contains unknown type variables. Consider adding a type annotation.
+
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
+  is at least as general as type Proxy @(t0 -> Type) (Unary @t0) -> Proxy @(t1 -> Type) (... @t1 a3)
+while checking that expression coerce
+  has type Proxy @(t0 -> Type) (Unary @t0) -> Proxy @(t1 -> Type) (... @t1 a3)
+in value declaration unaryToBinary
+
+where a3 is a rigid type variable
+        bound at (line 13, column 17 - line 13, column 23)
+      t0 is an unknown type
+      t2 is an unknown type
+      t1 is an unknown type
+      t4 is an unknown type
+      t5 is an unknown type
+
+See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
+or to contribute content related to this error.
+
diff --git a/tests/purs/failing/CoercibleHigherKindedData.purs b/tests/purs/failing/CoercibleHigherKindedData.purs
new file mode 100644
index 0000000000..bb0f718010
--- /dev/null
+++ b/tests/purs/failing/CoercibleHigherKindedData.purs
@@ -0,0 +1,13 @@
+-- @shouldFailWith NoInstanceFound
+module Main where
+
+import Safe.Coerce (coerce)
+
+data Unary a
+data Binary a b
+
+data Proxy a = Proxy
+type role Proxy representational
+
+unaryToBinary :: forall a. Proxy Unary -> Proxy (Binary a)
+unaryToBinary = coerce
diff --git a/tests/purs/failing/CoercibleHigherKindedNewtypes.out b/tests/purs/failing/CoercibleHigherKindedNewtypes.out
new file mode 100644
index 0000000000..de1064d6c5
--- /dev/null
+++ b/tests/purs/failing/CoercibleHigherKindedNewtypes.out
@@ -0,0 +1,23 @@
+Error found:
+in module Main
+at tests/purs/failing/CoercibleHigherKindedNewtypes.purs:13:8 - 13:14 (line 13, column 8 - line 13, column 14)
+
+  No type class instance was found for
+                            
+    Prim.Coerce.Coercible t0
+                          t1
+                            
+  The instance head contains unknown type variables. Consider adding a type annotation.
+
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
+  is at least as general as type Ap @Type @Type N1 Int String -> Ap @Type @Type N2 Int String
+while checking that expression coerce
+  has type Ap @Type @Type N1 Int String -> Ap @Type @Type N2 Int String
+in value declaration swap
+
+where t1 is an unknown type
+      t0 is an unknown type
+
+See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
+or to contribute content related to this error.
+
diff --git a/tests/purs/failing/CoercibleHigherKindedNewtypes.purs b/tests/purs/failing/CoercibleHigherKindedNewtypes.purs
new file mode 100644
index 0000000000..39dc2563f1
--- /dev/null
+++ b/tests/purs/failing/CoercibleHigherKindedNewtypes.purs
@@ -0,0 +1,13 @@
+-- @shouldFailWith NoInstanceFound
+module Main where
+
+import Safe.Coerce (coerce)
+
+newtype Ap f a b = Ap (f a b)
+
+data Tuple a b = Tuple a b
+newtype N1 a b = N1 (Tuple a b)
+newtype N2 b a = N2 (Tuple a b)
+
+swap :: Ap N1 Int String -> Ap N2 Int String
+swap = coerce
diff --git a/tests/purs/failing/CoercibleKindMismatch.out b/tests/purs/failing/CoercibleKindMismatch.out
new file mode 100644
index 0000000000..c6f3b0027b
--- /dev/null
+++ b/tests/purs/failing/CoercibleKindMismatch.out
@@ -0,0 +1,31 @@
+Error found:
+in module Main
+at tests/purs/failing/CoercibleKindMismatch.purs:14:39 - 14:45 (line 14, column 39 - line 14, column 45)
+
+  Could not match kind
+        
+    Type
+        
+  with kind
+               
+    t29 -> Type
+               
+
+while solving type class constraint
+                                        
+  Prim.Coerce.Coercible (Unary @t0)     
+                        (Binary @t1 @t2)
+                                        
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
+  is at least as general as type Proxy @(t0 -> Type) (Unary @t0) -> Proxy @(t1 -> ...) (Binary @t1 @t2)
+while checking that expression coerce
+  has type Proxy @(t0 -> Type) (Unary @t0) -> Proxy @(t1 -> ...) (Binary @t1 @t2)
+in value declaration unaryToBinary
+
+where t0 is an unknown type
+      t1 is an unknown type
+      t2 is an unknown type
+
+See https://github.com/purescript/documentation/blob/master/errors/KindsDoNotUnify.md for more information,
+or to contribute content related to this error.
+
diff --git a/tests/purs/failing/CoercibleKindMismatch.purs b/tests/purs/failing/CoercibleKindMismatch.purs
new file mode 100644
index 0000000000..32a91f633a
--- /dev/null
+++ b/tests/purs/failing/CoercibleKindMismatch.purs
@@ -0,0 +1,15 @@
+-- @shouldFailWith KindsDoNotUnify
+module Main where
+
+import Safe.Coerce (coerce)
+
+data Unary a
+data Binary a b
+
+data Proxy :: forall k. k -> Type
+data Proxy a = Proxy
+
+type role Proxy representational
+
+unaryToBinary :: Proxy Unary -> Proxy Binary
+unaryToBinary = coerce
diff --git a/tests/purs/failing/CoercibleNominal.out b/tests/purs/failing/CoercibleNominal.out
index e84c6ee6a6..9f850dc4bd 100644
--- a/tests/purs/failing/CoercibleNominal.out
+++ b/tests/purs/failing/CoercibleNominal.out
@@ -8,7 +8,7 @@ at tests/purs/failing/CoercibleNominal.purs:11:20 - 11:26 (line 11, column 20 -
                           (Nominal b2 c1)
                                          
 
-while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
   is at least as general as type Nominal a0 c1 -> Nominal b2 c1
 while checking that expression coerce
   has type Nominal a0 c1 -> Nominal b2 c1
diff --git a/tests/purs/failing/CoercibleNominalTypeApp.out b/tests/purs/failing/CoercibleNominalTypeApp.out
index d99972caef..2232a1983f 100644
--- a/tests/purs/failing/CoercibleNominalTypeApp.out
+++ b/tests/purs/failing/CoercibleNominalTypeApp.out
@@ -8,7 +8,7 @@ at tests/purs/failing/CoercibleNominalTypeApp.purs:13:8 - 13:14 (line 13, column
                           (G @Type Maybe String)
                                                 
 
-while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
   is at least as general as type G @Type Maybe Int -> G @Type Maybe String
 while checking that expression coerce
   has type G @Type Maybe Int -> G @Type Maybe String
diff --git a/tests/purs/failing/CoercibleNominalWrapped.out b/tests/purs/failing/CoercibleNominalWrapped.out
index 781959f8a0..a60528d314 100644
--- a/tests/purs/failing/CoercibleNominalWrapped.out
+++ b/tests/purs/failing/CoercibleNominalWrapped.out
@@ -8,7 +8,7 @@ at tests/purs/failing/CoercibleNominalWrapped.purs:15:14 - 15:20 (line 15, colum
                           (Wrap (Id a0) b1)
                                            
 
-while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
   is at least as general as type Wrap a0 b1 -> Wrap (Id a0) b1
 while checking that expression coerce
   has type Wrap a0 b1 -> Wrap (Id a0) b1
diff --git a/tests/purs/failing/CoercibleRepresentational.out b/tests/purs/failing/CoercibleRepresentational.out
index 90ef1ae9b6..2d3eb6eb16 100644
--- a/tests/purs/failing/CoercibleRepresentational.out
+++ b/tests/purs/failing/CoercibleRepresentational.out
@@ -8,7 +8,7 @@ at tests/purs/failing/CoercibleRepresentational.purs:11:20 - 11:26 (line 11, col
                           b3
                             
 
-while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
   is at least as general as type Phantom @t0 a1 -> Phantom @t2 b3
 while checking that expression coerce
   has type Phantom @t0 a1 -> Phantom @t2 b3
diff --git a/tests/purs/failing/CoercibleRepresentational2.out b/tests/purs/failing/CoercibleRepresentational2.out
index b2b1d38004..5e82bf8851 100644
--- a/tests/purs/failing/CoercibleRepresentational2.out
+++ b/tests/purs/failing/CoercibleRepresentational2.out
@@ -8,7 +8,7 @@ at tests/purs/failing/CoercibleRepresentational2.purs:9:14 - 9:20 (line 9, colum
                           String
                                 
 
-while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
   is at least as general as type Arr1 Int -> Arr1 String
 while checking that expression coerce
   has type Arr1 Int -> Arr1 String
diff --git a/tests/purs/failing/CoercibleRepresentational3.out b/tests/purs/failing/CoercibleRepresentational3.out
index 529edab386..416387b287 100644
--- a/tests/purs/failing/CoercibleRepresentational3.out
+++ b/tests/purs/failing/CoercibleRepresentational3.out
@@ -8,7 +8,7 @@ at tests/purs/failing/CoercibleRepresentational3.purs:9:14 - 9:20 (line 9, colum
                           String
                                 
 
-while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
   is at least as general as type Rec1 Int -> Rec1 String
 while checking that expression coerce
   has type Rec1 Int -> Rec1 String
diff --git a/tests/purs/failing/InfiniteKind.out b/tests/purs/failing/InfiniteKind.out
index 69e5eb4b9a..3bb4745c23 100644
--- a/tests/purs/failing/InfiniteKind.out
+++ b/tests/purs/failing/InfiniteKind.out
@@ -10,7 +10,6 @@ at tests/purs/failing/InfiniteKind.purs:5:17 - 5:18 (line 5, column 17 - line 5,
 while checking that type a
   has kind t0
 while inferring the kind of a a
-while inferring the kind of a a -> F a
 in type constructor F
 
 where t0 is an unknown type
diff --git a/tests/purs/failing/InfiniteKind2.out b/tests/purs/failing/InfiniteKind2.out
index 0153bcc434..1be74af830 100644
--- a/tests/purs/failing/InfiniteKind2.out
+++ b/tests/purs/failing/InfiniteKind2.out
@@ -10,7 +10,6 @@ at tests/purs/failing/InfiniteKind2.purs:5:23 - 5:27 (line 5, column 23 - line 5
 while checking that type Tree
   has kind t0
 while inferring the kind of m Tree
-while inferring the kind of m Tree -> Tree m
 in type constructor Tree
 
 where t0 is an unknown type
diff --git a/tests/purs/failing/KindError.out b/tests/purs/failing/KindError.out
index 1339a8890d..fe56bd3e06 100644
--- a/tests/purs/failing/KindError.out
+++ b/tests/purs/failing/KindError.out
@@ -14,7 +14,6 @@ at tests/purs/failing/KindError.purs:6:35 - 6:36 (line 6, column 35 - line 6, co
 while checking that type f
   has kind t0 -> t1
 while inferring the kind of f a
-while inferring the kind of f a -> KindError f a
 in type constructor KindError
 
 where t0 is an unknown type
diff --git a/tests/purs/failing/StandaloneKindSignatures2.out b/tests/purs/failing/StandaloneKindSignatures2.out
index 9e9df4a898..0835b79c5b 100644
--- a/tests/purs/failing/StandaloneKindSignatures2.out
+++ b/tests/purs/failing/StandaloneKindSignatures2.out
@@ -14,7 +14,6 @@ at tests/purs/failing/StandaloneKindSignatures2.purs:8:35 - 8:36 (line 8, column
 while checking that type b
   has kind k1
 while inferring the kind of Pair a b
-while inferring the kind of Pair a b -> Pair' @k1 @k2 a b
 in type constructor Pair'
 
 See https://github.com/purescript/documentation/blob/master/errors/KindsDoNotUnify.md for more information,
diff --git a/tests/purs/passing/Coercible.purs b/tests/purs/passing/Coercible.purs
index 684b0e10cd..1a5f5b08fe 100644
--- a/tests/purs/passing/Coercible.purs
+++ b/tests/purs/passing/Coercible.purs
@@ -18,7 +18,7 @@ nt2ToNT1 :: NTString2 -> NTString1
 nt2ToNT1 = coerce
 
 newtype Id1 a = Id1 a
-newtype Id2 a = Id2 a
+newtype Id2 b = Id2 b
 
 id1ToId2 :: forall a. Id1 a -> Id2 a
 id1ToId2 = coerce
@@ -26,6 +26,11 @@ id1ToId2 = coerce
 id12ToId21 :: forall b. Id1 (Id2 b) -> Id2 (Id1 b)
 id12ToId21 = coerce
 
+newtype Ap f a = Ap (f a)
+
+apId1ToApId2 :: forall a. Ap Id1 a -> Ap Id2 a
+apId1ToApId2 = coerce
+
 newtype Phantom1 a b = Phantom1 a
 
 phantom1TypeToPhantom1Symbol :: forall x (y :: Type) (z :: Symbol). Phantom1 x y -> Phantom1 x z
@@ -115,6 +120,16 @@ data Rec3 a = Rec3 {}
 rec3ToRec3 :: forall m n. Rec3 m -> Rec3 n
 rec3ToRec3 = coerce
 
+newtype Rec4 f = Rec4 (f {})
+
+unwrapRec4 :: forall f. Rec4 f -> f {}
+unwrapRec4 = coerce
+
+newtype Rec5 a f = Rec5 (f {})
+
+apRec4ToApRec5 :: forall a. Ap Rec4 Id1 -> Ap (Rec5 a) Id1
+apRec4ToApRec5 = coerce
+
 data Arr1 a b = Arr1 (Array a) (Array b)
 
 arr1ToArr1 :: Arr1 Int String -> Arr1 (Id1 Int) (Id2 String)