From 560a1b71be68326665c858a2e56007dfafc5e586 Mon Sep 17 00:00:00 2001
From: Cyril Sobierajewicz <sobierajewicz.cyril@gmail.com>
Date: Thu, 28 May 2020 23:17:17 +0200
Subject: [PATCH 01/10] Saturate higher kinded types in `Coercible` constraints

---
 .../src/Language/PureScript/Environment.hs    |   7 +-
 .../src/Language/PureScript/Types.hs          |  17 ++-
 src/Language/PureScript/Docs/Prim.hs          |  19 +++-
 .../PureScript/TypeChecker/Entailment.hs      | 103 ++++++++++--------
 tests/purs/failing/CoercibleForeign.out       |   2 +-
 tests/purs/failing/CoercibleForeign2.out      |   2 +-
 tests/purs/failing/CoercibleForeign3.out      |   2 +-
 .../failing/CoercibleHigherKindedNewtypes.out |  19 ++++
 .../CoercibleHigherKindedNewtypes.purs        |  13 +++
 tests/purs/failing/CoercibleNominal.out       |   2 +-
 .../purs/failing/CoercibleNominalTypeApp.out  |   2 +-
 .../purs/failing/CoercibleNominalWrapped.out  |   2 +-
 .../failing/CoercibleRepresentational.out     |   2 +-
 .../failing/CoercibleRepresentational2.out    |   2 +-
 .../failing/CoercibleRepresentational3.out    |   2 +-
 tests/purs/passing/Coercible.purs             |   7 +-
 16 files changed, 139 insertions(+), 64 deletions(-)
 create mode 100644 tests/purs/failing/CoercibleHigherKindedNewtypes.out
 create mode 100644 tests/purs/failing/CoercibleHigherKindedNewtypes.purs

diff --git a/lib/purescript-ast/src/Language/PureScript/Environment.hs b/lib/purescript-ast/src/Language/PureScript/Environment.hs
index f2324e413e..541fd803bf 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)
     ]
 
diff --git a/lib/purescript-ast/src/Language/PureScript/Types.hs b/lib/purescript-ast/src/Language/PureScript/Types.hs
index f221d3619d..6b1b91dc40 100644
--- a/lib/purescript-ast/src/Language/PureScript/Types.hs
+++ b/lib/purescript-ast/src/Language/PureScript/Types.hs
@@ -10,11 +10,13 @@ import Codec.Serialise (Serialise)
 import Control.Applicative ((<|>))
 import Control.Arrow (first, second)
 import Control.DeepSeq (NFData)
-import Control.Monad ((<=<), (>=>))
+import Control.Monad ((<=<), (>=>), replicateM)
+import Control.Monad.Supply (runSupply)
+import Control.Monad.Supply.Class (fresh)
 import Data.Aeson ((.:), (.:?), (.!=), (.=))
 import qualified Data.Aeson as A
 import qualified Data.Aeson.Types as A
-import Data.Foldable (fold)
+import Data.Foldable (fold, foldl')
 import qualified Data.IntSet as IS
 import Data.List (sort, sortBy)
 import Data.Ord (comparing)
@@ -585,6 +587,17 @@ unapplyConstraints = go []
   go acc (ConstrainedType _ con ty) = go (con : acc) ty
   go acc ty = (reverse acc, ty)
 
+saturate :: S.Set Text -> SourceType -> Int -> SourceType
+saturate bound ty n = fst . runSupply 0 $ do
+  tvs <- replicateM n freshTyVar
+  return $ foldl' srcTypeApp ty (srcTypeVar <$> tvs)
+  where
+  freshTyVar = do
+    tv <- ("t" <>) . T.pack . show <$> fresh
+    if tv `elem` bound
+      then freshTyVar
+      else return tv
+
 everywhereOnTypes :: (Type a -> Type a) -> Type a -> Type a
 everywhereOnTypes f = go where
   go (TypeApp ann t1 t2) = f (TypeApp ann (go t1) (go t2))
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..035099795d 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -406,56 +406,65 @@ entails SolverOptions{..} constraint context hints =
     -- @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 env a b
+      | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
+      , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
+      , Just (aTyKind, _) <- M.lookup aTyName $ types env
+      , Just (bTyKind, _) <- M.lookup bTyName $ types env
+      , i <- kindArity aTyKind - length axs
+      , j <- kindArity bTyKind - length bxs
+      , i > 0 && j > 0 = 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).
+          let aTyVars = S.fromList $ usedTypeVariables a
+              bTyVars = S.fromList $ usedTypeVariables b
+              saturate' = saturate $ aTyVars `S.union` bTyVars
+          pure [srcCoercibleConstraint (saturate' a i) (saturate' b j)]
+      | (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 [srcCoercibleConstraint ax bx]
+                Phantom ->
+                  Just []
+          fmap concat $ sequence $ zipWith3 k tyRoles 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 [srcCoercibleConstraint wrappedTySub b]
+      | otherwise =
         -- In all other cases we can't solve the constraint.
         Nothing
 
+    srcCoercibleConstraint :: SourceType -> SourceType -> SourceConstraint
+    srcCoercibleConstraint a b = srcConstraint C.Coercible [] [a, b] Nothing
+
     solveIsSymbol :: [SourceType] -> Maybe [TypeClassDict]
     solveIsSymbol [TypeLevelString ann sym] = Just [TypeClassDictionaryInScope [] 0 (IsSymbolInstance sym) [] C.IsSymbol [] [] [TypeLevelString ann sym] Nothing]
     solveIsSymbol _ = Nothing
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/CoercibleHigherKindedNewtypes.out b/tests/purs/failing/CoercibleHigherKindedNewtypes.out
new file mode 100644
index 0000000000..dd5a9b44ad
--- /dev/null
+++ b/tests/purs/failing/CoercibleHigherKindedNewtypes.out
@@ -0,0 +1,19 @@
+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 t1
+                          t0
+                            
+
+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
+
+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/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/passing/Coercible.purs b/tests/purs/passing/Coercible.purs
index 684b0e10cd..28a53d13d6 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

From e4c53046964aa32d62ac46a2ec1161821982db4d Mon Sep 17 00:00:00 2001
From: Cyril Sobierajewicz <sobierajewicz.cyril@gmail.com>
Date: Sat, 4 Jul 2020 15:55:12 +0200
Subject: [PATCH 02/10] Apply the polymorphic kind of `Coercible` constraints
 when solving them

---
 .../src/Language/PureScript/Environment.hs    | 13 +++---
 .../PureScript/TypeChecker/Entailment.hs      | 40 ++++++++++---------
 2 files changed, 30 insertions(+), 23 deletions(-)

diff --git a/lib/purescript-ast/src/Language/PureScript/Environment.hs b/lib/purescript-ast/src/Language/PureScript/Environment.hs
index 541fd803bf..229cebb4b5 100644
--- a/lib/purescript-ast/src/Language/PureScript/Environment.hs
+++ b/lib/purescript-ast/src/Language/PureScript/Environment.hs
@@ -636,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/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index 035099795d..9ec64ae460 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -24,7 +24,7 @@ import Control.Monad.Writer
 import Data.Foldable (for_, fold, 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
@@ -173,7 +173,7 @@ entails SolverOptions{..} constraint context hints =
       -- 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 env _ C.Coercible kinds args | Just dicts <- solveCoercible env kinds 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
@@ -381,8 +381,8 @@ 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
+    solveCoercible :: Environment -> [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
+    solveCoercible env kinds [a, b] = do
       let tySynMap = typeSynonyms env
           kindMap = types env
           replaceTySyns = either (const Nothing) Just . replaceAllTypeSynonymsM tySynMap kindMap
@@ -392,15 +392,15 @@ entails SolverOptions{..} constraint context hints =
       -- 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
+          pure [TypeClassDictionaryInScope [] 0 EmptyClassInstance [] C.Coercible [] kinds [a, b] (Just ws)]
+    solveCoercible _ _ _ = Nothing
 
     -- | Take two types, @a@ and @b@ representing a desired constraint
     -- @Coercible a b@ and reduce them to a set of simpler wanted constraints
@@ -411,8 +411,10 @@ entails SolverOptions{..} constraint context hints =
       , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
       , Just (aTyKind, _) <- M.lookup aTyName $ types env
       , Just (bTyKind, _) <- M.lookup bTyName $ types env
-      , i <- kindArity aTyKind - length axs
-      , j <- kindArity bTyKind - length bxs
+      , (aks, kind) <- unapplyKinds aTyKind
+      , (bks, _) <- unapplyKinds bTyKind
+      , i <- length aks - length axs
+      , j <- length bks - length bxs
       , i > 0 && j > 0 = 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
@@ -421,18 +423,20 @@ entails SolverOptions{..} constraint context hints =
           let aTyVars = S.fromList $ usedTypeVariables a
               bTyVars = S.fromList $ usedTypeVariables b
               saturate' = saturate $ aTyVars `S.union` bTyVars
-          pure [srcCoercibleConstraint (saturate' a i) (saturate' b j)]
+          pure [srcCoercibleConstraint kind (saturate' a i) (saturate' b j)]
       | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
       , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
-      , not (null axs) && not (null bxs) && aTyName == bTyName = do
+      , not (null axs) && not (null bxs) && aTyName == bTyName
+      , Just (aTyKind, _) <- M.lookup aTyName (types env) = 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
+          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
@@ -445,10 +449,10 @@ entails SolverOptions{..} constraint context hints =
                   | otherwise ->
                       Nothing
                 Representational ->
-                  Just [srcCoercibleConstraint ax bx]
+                  Just [srcCoercibleConstraint kx ax bx]
                 Phantom ->
                   Just []
-          fmap concat $ sequence $ zipWith3 k tyRoles axs bxs
+          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
@@ -457,13 +461,13 @@ entails SolverOptions{..} constraint context hints =
           -- 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 [srcCoercibleConstraint wrappedTySub b]
+          pure [srcCoercibleConstraint kindType wrappedTySub b]
       | otherwise =
         -- In all other cases we can't solve the constraint.
         Nothing
 
-    srcCoercibleConstraint :: SourceType -> SourceType -> SourceConstraint
-    srcCoercibleConstraint a b = srcConstraint C.Coercible [] [a, b] 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]

From a46578484d6d230cdc030d8fa6577253d1298b6b Mon Sep 17 00:00:00 2001
From: Cyril Sobierajewicz <sobierajewicz.cyril@gmail.com>
Date: Sun, 5 Jul 2020 16:55:32 +0200
Subject: [PATCH 03/10] Forbid heterogenously kinded `Coercible` constraints
 arguments

---
 .../src/Language/PureScript/Types.hs          | 17 +----
 .../PureScript/TypeChecker/Entailment.hs      | 62 +++++++++++--------
 .../failing/CoercibleHigherKindedNewtypes.out |  8 ++-
 tests/purs/failing/CoercibleKindMismatch.out  | 27 ++++++++
 tests/purs/failing/CoercibleKindMismatch.purs | 18 ++++++
 5 files changed, 90 insertions(+), 42 deletions(-)
 create mode 100644 tests/purs/failing/CoercibleKindMismatch.out
 create mode 100644 tests/purs/failing/CoercibleKindMismatch.purs

diff --git a/lib/purescript-ast/src/Language/PureScript/Types.hs b/lib/purescript-ast/src/Language/PureScript/Types.hs
index 6b1b91dc40..f221d3619d 100644
--- a/lib/purescript-ast/src/Language/PureScript/Types.hs
+++ b/lib/purescript-ast/src/Language/PureScript/Types.hs
@@ -10,13 +10,11 @@ import Codec.Serialise (Serialise)
 import Control.Applicative ((<|>))
 import Control.Arrow (first, second)
 import Control.DeepSeq (NFData)
-import Control.Monad ((<=<), (>=>), replicateM)
-import Control.Monad.Supply (runSupply)
-import Control.Monad.Supply.Class (fresh)
+import Control.Monad ((<=<), (>=>))
 import Data.Aeson ((.:), (.:?), (.!=), (.=))
 import qualified Data.Aeson as A
 import qualified Data.Aeson.Types as A
-import Data.Foldable (fold, foldl')
+import Data.Foldable (fold)
 import qualified Data.IntSet as IS
 import Data.List (sort, sortBy)
 import Data.Ord (comparing)
@@ -587,17 +585,6 @@ unapplyConstraints = go []
   go acc (ConstrainedType _ con ty) = go (con : acc) ty
   go acc ty = (reverse acc, ty)
 
-saturate :: S.Set Text -> SourceType -> Int -> SourceType
-saturate bound ty n = fst . runSupply 0 $ do
-  tvs <- replicateM n freshTyVar
-  return $ foldl' srcTypeApp ty (srcTypeVar <$> tvs)
-  where
-  freshTyVar = do
-    tv <- ("t" <>) . T.pack . show <$> fresh
-    if tv `elem` bound
-      then freshTyVar
-      else return tv
-
 everywhereOnTypes :: (Type a -> Type a) -> Type a -> Type a
 everywhereOnTypes f = go where
   go (TypeApp ann t1 t2) = f (TypeApp ann (go t1) (go t2))
diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index 9ec64ae460..1c40954094 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -14,14 +14,15 @@ 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, zipWith4)
@@ -39,7 +40,7 @@ import Language.PureScript.Environment
 import Language.PureScript.Errors
 import Language.PureScript.Names
 import Language.PureScript.Roles
-import Language.PureScript.TypeChecker.Kinds (elaborateKind, unifyKinds)
+import Language.PureScript.TypeChecker.Kinds (elaborateKind, kindOf, unifyKinds)
 import Language.PureScript.TypeChecker.Monad
 import Language.PureScript.TypeChecker.Roles
 import Language.PureScript.TypeChecker.Synonyms
@@ -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 kinds args | Just dicts <- solveCoercible env kinds 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,11 +390,11 @@ entails SolverOptions{..} constraint context hints =
         subclassDictionaryValue dict className index =
           App (Accessor (mkString (superclassName className index)) dict) valUndefined
 
-    solveCoercible :: Environment -> [SourceType] -> [SourceType] -> Maybe [TypeClassDict]
-    solveCoercible env kinds [a, b] = do
+    solveCoercible :: Environment -> [SourceType] -> [SourceType] -> m (Maybe [TypeClassDict])
+    solveCoercible env kinds [a, b] = runMaybeT $ do
       let tySynMap = typeSynonyms env
           kindMap = types env
-          replaceTySyns = either (const Nothing) Just . replaceAllTypeSynonymsM tySynMap kindMap
+          replaceTySyns = lift . replaceAllTypeSynonymsM tySynMap kindMap
       a' <- replaceTySyns a
       b' <- replaceTySyns b
       -- Solving terminates when the two arguments are the same. Since we
@@ -394,18 +403,22 @@ entails SolverOptions{..} constraint context hints =
       if a' == b'
         then pure [TypeClassDictionaryInScope [] 0 EmptyClassInstance [] C.Coercible [] kinds [a, b] Nothing]
         else do
+          lift $ do
+            (_, kind) <- kindOf a'
+            (_, kind') <- kindOf b'
+            unifyKinds kind kind'
           -- 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'
+          ws <- (MaybeT $ coercibleWanteds env a' b') <|> (MaybeT $ coercibleWanteds env b' a')
           pure [TypeClassDictionaryInScope [] 0 EmptyClassInstance [] C.Coercible [] kinds [a, b] (Just ws)]
-    solveCoercible _ _ _ = Nothing
+    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 :: Environment -> SourceType -> SourceType -> m (Maybe [SourceConstraint])
     coercibleWanteds env a b
       | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
       , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
@@ -413,21 +426,20 @@ entails SolverOptions{..} constraint context hints =
       , Just (bTyKind, _) <- M.lookup bTyName $ types env
       , (aks, kind) <- unapplyKinds aTyKind
       , (bks, _) <- unapplyKinds bTyKind
-      , i <- length aks - length axs
-      , j <- length bks - length bxs
-      , i > 0 && j > 0 = do
+      , length axs < length aks
+      , length bxs < length bks = 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).
-          let aTyVars = S.fromList $ usedTypeVariables a
-              bTyVars = S.fromList $ usedTypeVariables b
-              saturate' = saturate $ aTyVars `S.union` bTyVars
-          pure [srcCoercibleConstraint kind (saturate' a i) (saturate' b j)]
+          tys <- traverse freshTypeWithKind aks
+          let a' = foldl' srcTypeApp a $ drop (length axs) tys
+              b' = foldl' srcTypeApp b $ drop (length bxs) tys
+          pure $ Just [srcCoercibleConstraint kind a' b']
       | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
       , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
       , not (null axs) && not (null bxs) && aTyName == bTyName
-      , Just (aTyKind, _) <- M.lookup aTyName (types env) = do
+      , Just (aTyKind, _) <- 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
@@ -445,13 +457,13 @@ entails SolverOptions{..} constraint context hints =
                   -- means there are cases we should be able to handle that
                   -- we currently can't, but is at least sound.
                   | ax == bx ->
-                      Just []
+                      pure []
                   | otherwise ->
-                      Nothing
+                      empty
                 Representational ->
-                  Just [srcCoercibleConstraint kx ax bx]
+                  pure [srcCoercibleConstraint kx ax bx]
                 Phantom ->
-                  Just []
+                  pure []
           fmap concat $ sequence $ zipWith4 f roles kinds axs bxs
       | (TypeConstructor _ tyName, _, xs) <- unapplyTypes a
       , Just (tvs, wrappedTy, _) <- lookupNewtypeConstructor env tyName = do
@@ -461,10 +473,10 @@ entails SolverOptions{..} constraint context hints =
           -- 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 [srcCoercibleConstraint kindType wrappedTySub b]
+          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
diff --git a/tests/purs/failing/CoercibleHigherKindedNewtypes.out b/tests/purs/failing/CoercibleHigherKindedNewtypes.out
index dd5a9b44ad..de1064d6c5 100644
--- a/tests/purs/failing/CoercibleHigherKindedNewtypes.out
+++ b/tests/purs/failing/CoercibleHigherKindedNewtypes.out
@@ -4,9 +4,10 @@ at tests/purs/failing/CoercibleHigherKindedNewtypes.purs:13:8 - 13:14 (line 13,
 
   No type class instance was found for
                             
-    Prim.Coerce.Coercible t1
-                          t0
+    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
@@ -14,6 +15,9 @@ 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/CoercibleKindMismatch.out b/tests/purs/failing/CoercibleKindMismatch.out
new file mode 100644
index 0000000000..31ca3fa401
--- /dev/null
+++ b/tests/purs/failing/CoercibleKindMismatch.out
@@ -0,0 +1,27 @@
+Error found:
+in module Main
+at tests/purs/failing/CoercibleKindMismatch.purs:17:39 - 17:45 (line 17, column 39 - line 17, column 45)
+
+  Could not match kind
+        
+    Type
+        
+  with kind
+                
+    Type -> Type
+                
+
+while solving type class constraint
+                              
+  Prim.Coerce.Coercible Unary 
+                        Binary
+                              
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
+  is at least as general as type Proxy @(Type -> Type) Unary -> Proxy @(Type -> ...) Binary
+while checking that expression coerce
+  has type Proxy @(Type -> Type) Unary -> Proxy @(Type -> ...) Binary
+in value declaration unaryToBinary
+
+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..9ffb2db6ac
--- /dev/null
+++ b/tests/purs/failing/CoercibleKindMismatch.purs
@@ -0,0 +1,18 @@
+-- @shouldFailWith KindsDoNotUnify
+module Main where
+
+import Safe.Coerce (coerce)
+
+data Unary :: Type -> Type
+data Unary a
+
+data Binary :: Type -> Type -> Type
+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

From d2405fe44bfe4a05069b9c1043a7d82459ac2d8a Mon Sep 17 00:00:00 2001
From: Cyril Sobierajewicz <sobierajewicz.cyril@gmail.com>
Date: Sun, 12 Jul 2020 13:17:07 +0200
Subject: [PATCH 04/10] =?UTF-8?q?Don=E2=80=99t=20rewrite=20thrown=20away?=
 =?UTF-8?q?=20types=20when=20unifying=20`Coercible`=20arguments=20kinds?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Language/PureScript/TypeChecker/Entailment.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index 1c40954094..e205d70ee4 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -40,7 +40,7 @@ import Language.PureScript.Environment
 import Language.PureScript.Errors
 import Language.PureScript.Names
 import Language.PureScript.Roles
-import Language.PureScript.TypeChecker.Kinds (elaborateKind, kindOf, unifyKinds)
+import Language.PureScript.TypeChecker.Kinds (elaborateKind, unifyKinds)
 import Language.PureScript.TypeChecker.Monad
 import Language.PureScript.TypeChecker.Roles
 import Language.PureScript.TypeChecker.Synonyms
@@ -404,8 +404,8 @@ entails SolverOptions{..} constraint context hints =
         then pure [TypeClassDictionaryInScope [] 0 EmptyClassInstance [] C.Coercible [] kinds [a, b] Nothing]
         else do
           lift $ do
-            (_, kind) <- kindOf a'
-            (_, kind') <- kindOf b'
+            kind <- elaborateKind a'
+            kind' <- elaborateKind b'
             unifyKinds kind kind'
           -- When solving must reduce and recurse, it doesn't matter whether we
           -- reduce the first or second argument -- if the constraint is

From 8552334f8deca65cd997a2349d8f37266cc796a4 Mon Sep 17 00:00:00 2001
From: Cyril Sobierajewicz <sobierajewicz.cyril@gmail.com>
Date: Sun, 12 Jul 2020 21:58:34 +0200
Subject: [PATCH 05/10] Compare `Coercible` arguments rewritten with their
 inferred kinds

---
 src/Language/PureScript/TypeChecker/Entailment.hs | 13 +++++--------
 tests/purs/passing/Coercible.purs                 |  5 +++++
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index e205d70ee4..a363b4c1c4 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -40,7 +40,7 @@ import Language.PureScript.Environment
 import Language.PureScript.Errors
 import Language.PureScript.Names
 import Language.PureScript.Roles
-import Language.PureScript.TypeChecker.Kinds (elaborateKind, unifyKinds)
+import Language.PureScript.TypeChecker.Kinds (elaborateKind, kindOf, unifyKinds)
 import Language.PureScript.TypeChecker.Monad
 import Language.PureScript.TypeChecker.Roles
 import Language.PureScript.TypeChecker.Synonyms
@@ -394,19 +394,16 @@ entails SolverOptions{..} constraint context hints =
     solveCoercible env kinds [a, b] = runMaybeT $ do
       let tySynMap = typeSynonyms env
           kindMap = types env
-          replaceTySyns = lift . replaceAllTypeSynonymsM tySynMap kindMap
-      a' <- replaceTySyns a
-      b' <- replaceTySyns b
+          replaceTySyns = replaceAllTypeSynonymsM tySynMap kindMap
+      (a', kind) <- lift $ replaceTySyns a >>= kindOf
+      (b', kind') <- lift $ replaceTySyns b >>= kindOf
+      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 [] kinds [a, b] Nothing]
         else do
-          lift $ do
-            kind <- elaborateKind a'
-            kind' <- elaborateKind b'
-            unifyKinds kind kind'
           -- 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
diff --git a/tests/purs/passing/Coercible.purs b/tests/purs/passing/Coercible.purs
index 28a53d13d6..8ba16f6fc8 100644
--- a/tests/purs/passing/Coercible.purs
+++ b/tests/purs/passing/Coercible.purs
@@ -120,6 +120,11 @@ 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
+
 data Arr1 a b = Arr1 (Array a) (Array b)
 
 arr1ToArr1 :: Arr1 Int String -> Arr1 (Id1 Int) (Id2 String)

From d9b8da88d469a6d26eb1f4f11358841fc9d3cd7d Mon Sep 17 00:00:00 2001
From: Cyril Sobierajewicz <sobierajewicz.cyril@gmail.com>
Date: Tue, 25 Aug 2020 19:38:58 +0200
Subject: [PATCH 06/10] Throw on failed type lookups when solving `Coercible`
 constraints

---
 src/Language/PureScript/TypeChecker/Entailment.hs | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index a363b4c1c4..2f0cd344e1 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -419,8 +419,8 @@ entails SolverOptions{..} constraint context hints =
     coercibleWanteds env a b
       | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
       , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
-      , Just (aTyKind, _) <- M.lookup aTyName $ types env
-      , Just (bTyKind, _) <- M.lookup bTyName $ types env
+      , (aTyKind, _) <- fromMaybe (internalError "coercibleWanteds: type lookup failed") $ M.lookup aTyName (types env)
+      , (bTyKind, _) <- fromMaybe (internalError "coercibleWanteds: type lookup failed") $ M.lookup bTyName (types env)
       , (aks, kind) <- unapplyKinds aTyKind
       , (bks, _) <- unapplyKinds bTyKind
       , length axs < length aks
@@ -436,7 +436,8 @@ entails SolverOptions{..} constraint context hints =
       | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
       , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
       , not (null axs) && not (null bxs) && aTyName == bTyName
-      , Just (aTyKind, _) <- M.lookup aTyName (types env) = runMaybeT $ do
+      , (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

From cf6d84e0d3acbaa01f0758fd693911ed19f62ff3 Mon Sep 17 00:00:00 2001
From: Cyril Sobierajewicz <sobierajewicz.cyril@gmail.com>
Date: Tue, 25 Aug 2020 19:44:26 +0200
Subject: [PATCH 07/10] Remove redundant checks from `coercibleWanteds` guards

---
 src/Language/PureScript/TypeChecker/Entailment.hs | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index 2f0cd344e1..e641d5c4ca 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -418,13 +418,10 @@ entails SolverOptions{..} constraint context hints =
     coercibleWanteds :: Environment -> SourceType -> SourceType -> m (Maybe [SourceConstraint])
     coercibleWanteds env a b
       | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
-      , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
+      , (TypeConstructor _ _, _, bxs) <- unapplyTypes b
       , (aTyKind, _) <- fromMaybe (internalError "coercibleWanteds: type lookup failed") $ M.lookup aTyName (types env)
-      , (bTyKind, _) <- fromMaybe (internalError "coercibleWanteds: type lookup failed") $ M.lookup bTyName (types env)
       , (aks, kind) <- unapplyKinds aTyKind
-      , (bks, _) <- unapplyKinds bTyKind
-      , length axs < length aks
-      , length bxs < length bks = do
+      , 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
@@ -435,7 +432,7 @@ entails SolverOptions{..} constraint context hints =
           pure $ Just [srcCoercibleConstraint kind a' b']
       | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
       , (TypeConstructor _ bTyName, _, bxs) <- unapplyTypes b
-      , not (null axs) && not (null bxs) && aTyName == bTyName
+      , 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

From eea4f60f67932eea04ebce09853812f770ccd321 Mon Sep 17 00:00:00 2001
From: Cyril Sobierajewicz <sobierajewicz.cyril@gmail.com>
Date: Tue, 25 Aug 2020 19:48:08 +0200
Subject: [PATCH 08/10] Support `Coercible` constraints on unsaturated type
 constructors with different kinds

---
 src/Language/PureScript/TypeChecker/Entailment.hs | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index e641d5c4ca..b520946c74 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -418,7 +418,6 @@ entails SolverOptions{..} constraint context hints =
     coercibleWanteds :: Environment -> SourceType -> SourceType -> m (Maybe [SourceConstraint])
     coercibleWanteds env a b
       | (TypeConstructor _ aTyName, _, axs) <- unapplyTypes a
-      , (TypeConstructor _ _, _, bxs) <- unapplyTypes b
       , (aTyKind, _) <- fromMaybe (internalError "coercibleWanteds: type lookup failed") $ M.lookup aTyName (types env)
       , (aks, kind) <- unapplyKinds aTyKind
       , length axs < length aks = do
@@ -426,9 +425,9 @@ entails SolverOptions{..} constraint context hints =
           -- 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 aks
-          let a' = foldl' srcTypeApp a $ drop (length axs) tys
-              b' = foldl' srcTypeApp b $ drop (length bxs) tys
+          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

From 7e8c171b08075703b96267b7cc350f2775d49858 Mon Sep 17 00:00:00 2001
From: Cyril Sobierajewicz <sobierajewicz.cyril@gmail.com>
Date: Sun, 6 Sep 2020 01:07:21 +0200
Subject: [PATCH 09/10] Rewrite constructor fields when checking the kind of
 their data type
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Given the following declaration

```purs
newtype N f = N (f {})
```

solving a `Coercible (N f) (f {})` constraints yields a `Coercible (f {}) (f {})` subgoal by the unwraping rule. This constraint seems trivial but if constructors fields are not elaborated the actual subgoal is `Coercible (f (Record ())) (f (Record (() @Type)))`, which isn’t solvable because of the missing kind application on the left!

Inferring kinds and comparing the rewritten terms fixes the issue at the expense of redundant work (kinds are already inferred during type checking) but then invalid coercions between unsaturated higher kinded types with polymorphic parameters fail to type check with an `UndefinedTypeVariable` error instead of the expected `NoInstanceFound`.
---
 .../Language/PureScript/AST/Declarations.hs   |  3 ++
 .../PureScript/TypeChecker/Entailment.hs      | 10 +++----
 src/Language/PureScript/TypeChecker/Kinds.hs  | 16 +++++++----
 .../failing/3275-DataBindingGroupErrorPos.out |  1 -
 .../failing/CoercibleHigherKindedData.out     | 28 +++++++++++++++++++
 .../failing/CoercibleHigherKindedData.purs    | 13 +++++++++
 tests/purs/failing/CoercibleKindMismatch.purs |  3 --
 tests/purs/failing/InfiniteKind.out           |  1 -
 tests/purs/failing/InfiniteKind2.out          |  1 -
 tests/purs/failing/KindError.out              |  1 -
 .../failing/StandaloneKindSignatures2.out     |  1 -
 tests/purs/passing/Coercible.purs             |  5 ++++
 12 files changed, 63 insertions(+), 20 deletions(-)
 create mode 100644 tests/purs/failing/CoercibleHigherKindedData.out
 create mode 100644 tests/purs/failing/CoercibleHigherKindedData.purs

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/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
index b520946c74..02fb947cf7 100644
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -40,7 +40,7 @@ import Language.PureScript.Environment
 import Language.PureScript.Errors
 import Language.PureScript.Names
 import Language.PureScript.Roles
-import Language.PureScript.TypeChecker.Kinds (elaborateKind, kindOf, unifyKinds)
+import Language.PureScript.TypeChecker.Kinds (elaborateKind, unifyKinds)
 import Language.PureScript.TypeChecker.Monad
 import Language.PureScript.TypeChecker.Roles
 import Language.PureScript.TypeChecker.Synonyms
@@ -392,11 +392,9 @@ entails SolverOptions{..} constraint context hints =
 
     solveCoercible :: Environment -> [SourceType] -> [SourceType] -> m (Maybe [TypeClassDict])
     solveCoercible env kinds [a, b] = runMaybeT $ do
-      let tySynMap = typeSynonyms env
-          kindMap = types env
-          replaceTySyns = replaceAllTypeSynonymsM tySynMap kindMap
-      (a', kind) <- lift $ replaceTySyns a >>= kindOf
-      (b', kind') <- lift $ replaceTySyns b >>= kindOf
+      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
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/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/CoercibleKindMismatch.purs b/tests/purs/failing/CoercibleKindMismatch.purs
index 9ffb2db6ac..32a91f633a 100644
--- a/tests/purs/failing/CoercibleKindMismatch.purs
+++ b/tests/purs/failing/CoercibleKindMismatch.purs
@@ -3,10 +3,7 @@ module Main where
 
 import Safe.Coerce (coerce)
 
-data Unary :: Type -> Type
 data Unary a
-
-data Binary :: Type -> Type -> Type
 data Binary a b
 
 data Proxy :: forall k. k -> Type
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 8ba16f6fc8..1a5f5b08fe 100644
--- a/tests/purs/passing/Coercible.purs
+++ b/tests/purs/passing/Coercible.purs
@@ -125,6 +125,11 @@ 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)

From e1b50bc73670f405d991845421eea2d3bd83b1e4 Mon Sep 17 00:00:00 2001
From: Cyril Sobierajewicz <sobierajewicz.cyril@gmail.com>
Date: Tue, 8 Sep 2020 19:18:20 +0200
Subject: [PATCH 10/10] Fix CoercibleKindMismatch golden test

---
 tests/purs/failing/CoercibleKindMismatch.out | 24 ++++++++++++--------
 1 file changed, 14 insertions(+), 10 deletions(-)

diff --git a/tests/purs/failing/CoercibleKindMismatch.out b/tests/purs/failing/CoercibleKindMismatch.out
index 31ca3fa401..c6f3b0027b 100644
--- a/tests/purs/failing/CoercibleKindMismatch.out
+++ b/tests/purs/failing/CoercibleKindMismatch.out
@@ -1,27 +1,31 @@
 Error found:
 in module Main
-at tests/purs/failing/CoercibleKindMismatch.purs:17:39 - 17:45 (line 17, column 39 - line 17, column 45)
+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
-                
-    Type -> Type
-                
+               
+    t29 -> Type
+               
 
 while solving type class constraint
-                              
-  Prim.Coerce.Coercible Unary 
-                        Binary
-                              
+                                        
+  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 @(Type -> Type) Unary -> Proxy @(Type -> ...) Binary
+  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 @(Type -> Type) Unary -> Proxy @(Type -> ...) Binary
+  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.