purescript · hdgarrood · Sep 9, 2020 · May 28, 2020 · Jul 4, 2020 · Jul 5, 2020
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -14,7 +14,6 @@ at tests/purs/failing/3275-DataBindingGroupErrorPos.purs:7:19 - 7:22 (line 7, co
 while checking that type [33mBar a[0m
   has kind [33mt0 -> t1[0m
 while inferring the kind of [33mBar a a[0m
-while inferring the kind of [33mBar a a -> Foo a[0m
 in data binding group Bar, Foo
 
 where [33mt0[0m is an unknown type

diff --git 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 -
   [33m                        (Foreign (Id a0) (Id b1))[0m
   [33m                                                 [0m
 
-while checking that type [33mforall (a :: Type) (b :: Type). Coercible a b => a -> b[0m
+while checking that type [33mforall (a :: Type) (b :: Type). Coercible @Type a b => a -> b[0m
   is at least as general as type [33mForeign a0 b1 -> Foreign (Id a0) (Id b1)[0m
 while checking that expression [33mcoerce[0m
   has type [33mForeign a0 b1 -> Foreign (Id a0) (Id b1)[0m

diff --git 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
   [33m                        (Foreign a0 b1 d3)[0m
   [33m                                          [0m
 
-while checking that type [33mforall (a :: Type) (b :: Type). Coercible a b => a -> b[0m
+while checking that type [33mforall (a :: Type) (b :: Type). Coercible @Type a b => a -> b[0m
   is at least as general as type [33mForeign a0 b1 c2 -> Foreign a0 b1 d3[0m
 while checking that expression [33mcoerce[0m
   has type [33mForeign a0 b1 c2 -> Foreign a0 b1 d3[0m