Walk under constrained types during role inference

src/Language/PureScript/TypeChecker/Roles.hs

@@ -187,6 +187,10 @@ inferDataDeclarationRoles moduleName (tyName, tyArgs, ctors) roleEnv =
     -- doesn't appear as a spurious parameter to @D@ when we complete
     -- inference.
     walk (S.insert tv btvs) t
+  walk btvs (ConstrainedType _ Constraint{..} t) =
+    -- For constrained types, mark all free variables in the constraint
+    -- arguments as nominal and recurse on the type beneath the constraint.
+    walk btvs t <> foldMap (freeNominals btvs) constraintArgs
   walk btvs (RCons _ _ thead ttail) = do
     -- For row types, we just walk along them and collect the results.
     walk btvs thead <> walk btvs ttail
@@ -214,7 +218,7 @@ inferDataDeclarationRoles moduleName (tyName, tyArgs, ctors) roleEnv =
               t1Roles = fromMaybe (repeat Phantom) $ M.lookup t1Name roleEnv
               k role ti = case role of
                 Nominal ->
-                  freeNominals ti
+                  freeNominals btvs ti
                 Representational ->
                   go ti
                 Phantom ->
@@ -224,14 +228,16 @@ inferDataDeclarationRoles moduleName (tyName, tyArgs, ctors) roleEnv =
           -- that term to collect its roles and mark all free variables in
           -- its argument as nominal.
           _ -> do
-            go t1 <> foldMap freeNominals t2s
+            go t1 <> foldMap (freeNominals btvs) t2s
     | otherwise =
         mempty
     where
       go = walk btvs
-      -- Given a type, computes the list of free variables in that type
-      -- (taking into account those bound in @walk@) and returns a @RoleMap@
-      -- ascribing a nominal role to each of those variables.
-      freeNominals x =
-        let ftvs = filter (flip S.notMember btvs) (freeTypeVariables x)
-        in  RoleMap (M.fromList $ map (, Nominal) ftvs)
+
+-- Given a type, computes the list of free variables in that type
+-- (taking into account those bound in @walk@) and returns a @RoleMap@
+-- ascribing a nominal role to each of those variables.
+freeNominals :: S.Set Text -> SourceType -> RoleMap
+freeNominals btvs x =
+  let ftvs = filter (flip S.notMember btvs) (freeTypeVariables x)
+  in  RoleMap (M.fromList $ map (, Nominal) ftvs)

tests/purs/failing/CoercibleConstrained1.out

@@ -0,0 +1,24 @@
+Error found:
+in module Main
+at tests/purs/failing/CoercibleConstrained1.purs:11:28 - 11:34 (line 11, column 28 - line 11, column 34)
+
+  No type class instance was found for
+                            
+    Prim.Coerce.Coercible a0
+                          b1
+                            
+
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
+  is at least as general as type Constrained a0 -> Constrained b1
+while checking that expression coerce
+  has type Constrained a0 -> Constrained b1
+in value declaration constrainedToConstrained
+
+where a0 is a rigid type variable
+        bound at (line 11, column 28 - line 11, column 34)
+      b1 is a rigid type variable
+        bound at (line 11, column 28 - line 11, column 34)
+
+See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
+or to contribute content related to this error.
+

tests/purs/failing/CoercibleConstrained1.purs

@@ -0,0 +1,11 @@
+-- @shouldFailWith NoInstanceFound
+module Main where
+
+import Safe.Coerce (coerce)
+
+class Nullary
+
+data Constrained a = Constrained (Nullary => a)
+
+constrainedToConstrained :: forall a b. Constrained a -> Constrained b
+constrainedToConstrained = coerce

tests/purs/failing/CoercibleConstrained2.out

@@ -0,0 +1,24 @@
+Error found:
+in module Main
+at tests/purs/failing/CoercibleConstrained2.purs:11:28 - 11:34 (line 11, column 28 - line 11, column 34)
+
+  No type class instance was found for
+                                          
+    Prim.Coerce.Coercible (Constrained a0)
+                          (Constrained b1)
+                                          
+
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
+  is at least as general as type Constrained a0 -> Constrained b1
+while checking that expression coerce
+  has type Constrained a0 -> Constrained b1
+in value declaration constrainedToConstrained
+
+where a0 is a rigid type variable
+        bound at (line 11, column 28 - line 11, column 34)
+      b1 is a rigid type variable
+        bound at (line 11, column 28 - line 11, column 34)
+
+See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
+or to contribute content related to this error.
+

tests/purs/failing/CoercibleConstrained2.purs

@@ -0,0 +1,11 @@
+-- @shouldFailWith NoInstanceFound
+module Main where
+
+import Safe.Coerce (coerce)
+
+class Unary a
+
+data Constrained a = Constrained (Unary a => a)
+
+constrainedToConstrained :: forall a b. Constrained a -> Constrained b
+constrainedToConstrained = coerce

tests/purs/failing/CoercibleConstrained3.out

@@ -0,0 +1,22 @@
+Error found:
+in module Main
+at tests/purs/failing/CoercibleConstrained3.purs:13:28 - 13:34 (line 13, column 28 - line 13, column 34)
+
+  No type class instance was found for
+                                              
+    Prim.Coerce.Coercible (Constrained a0)    
+                          (Constrained (N a0))
+                                              
+
+while checking that type forall (a :: Type) (b :: Type). Coercible @Type a b => a -> b
+  is at least as general as type Constrained a0 -> Constrained (N a0)
+while checking that expression coerce
+  has type Constrained a0 -> Constrained (N a0)
+in value declaration constrainedToConstrained
+
+where a0 is a rigid type variable
+        bound at (line 13, column 28 - line 13, column 34)
+
+See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
+or to contribute content related to this error.
+

tests/purs/failing/CoercibleConstrained3.purs

@@ -0,0 +1,13 @@
+-- @shouldFailWith NoInstanceFound
+module Main where
+
+import Safe.Coerce (coerce)
+
+class Unary a
+
+data Constrained a = Constrained (Unary a => a)
+
+newtype N a = N a
+
+constrainedToConstrained :: forall a. Constrained a -> Constrained (N a)
+constrainedToConstrained = coerce

tests/purs/passing/Coercible.purs

@@ -159,6 +159,17 @@ type role MyMap nominal representational
 mapToMap :: MyMap String String -> MyMap String NTString1
 mapToMap = coerce
 
+class Unary a
+
+data Constrained1 a b = Constrained1 (Unary a => b)
+
+constrained1ToConstrained1 :: forall a b. Constrained1 a b -> Constrained1 a (Id1 b)
+constrained1ToConstrained1 = coerce
+
+data Constrained2 a = Constrained2 a (forall a. Unary a => a)
+
+type role Constrained2 representational
+
 -- "role" should only be a reserved word after "type"
 testRoleNotReserved :: String -> String
 testRoleNotReserved role = role