From 60de827cc399be6a0fa2de520c632a498eee84bd Mon Sep 17 00:00:00 2001 From: Cyril Sobierajewicz Date: Wed, 3 Jun 2020 22:15:13 +0200 Subject: [PATCH 1/3] Recurse on the right of arrows when inferring nominal roles from kinds --- src/Language/PureScript/TypeChecker/Roles.hs | 6 ++--- tests/purs/failing/CoercibleForeign2.out | 28 ++++++++++++++++++++ tests/purs/failing/CoercibleForeign2.purs | 9 +++++++ 3 files changed, 40 insertions(+), 3 deletions(-) create mode 100644 tests/purs/failing/CoercibleForeign2.out create mode 100644 tests/purs/failing/CoercibleForeign2.purs diff --git a/src/Language/PureScript/TypeChecker/Roles.hs b/src/Language/PureScript/TypeChecker/Roles.hs index 5edbad4b80..7e8da42278 100644 --- a/src/Language/PureScript/TypeChecker/Roles.hs +++ b/src/Language/PureScript/TypeChecker/Roles.hs @@ -143,7 +143,7 @@ rolesFromForeignTypeKind = go [] where go acc = \case - TypeApp _ (TypeApp _ fn k1) _k2 | eqType fn tyFunction -> - go (Nominal : acc) k1 + TypeApp _ (TypeApp _ fn _k1) k2 | eqType fn tyFunction -> + go (Nominal : acc) k2 _k -> - Nominal : acc + acc diff --git a/tests/purs/failing/CoercibleForeign2.out b/tests/purs/failing/CoercibleForeign2.out new file mode 100644 index 0000000000..083afcb7bf --- /dev/null +++ b/tests/purs/failing/CoercibleForeign2.out @@ -0,0 +1,28 @@ +Error found: +in module Main +at tests/purs/failing/CoercibleForeign2.purs:9:20 - 9:26 (line 9, column 20 - line 9, column 26) + + No type class instance was found for +   +  Prim.Coerce.Coercible (Foreign a0 b1 c2) +  (Foreign a0 b1 d3) +   + +while checking that type forall (a :: Type) (b :: Type). Coercible 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 +in value declaration foreignToForeign + +where a0 is a rigid type variable + bound at (line 9, column 20 - line 9, column 26) + b1 is a rigid type variable + bound at (line 9, column 20 - line 9, column 26) + c2 is a rigid type variable + bound at (line 9, column 20 - line 9, column 26) + d3 is a rigid type variable + bound at (line 9, column 20 - line 9, column 26) + +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/CoercibleForeign2.purs b/tests/purs/failing/CoercibleForeign2.purs new file mode 100644 index 0000000000..bc94a389d1 --- /dev/null +++ b/tests/purs/failing/CoercibleForeign2.purs @@ -0,0 +1,9 @@ +-- @shouldFailWith NoInstanceFound +module Main where + +import Safe.Coerce (coerce) + +foreign import data Foreign :: Type -> Type -> Type -> Type + +foreignToForeign :: forall a b c d. Foreign a b c -> Foreign a b d +foreignToForeign = coerce From 483fcc23aeb5fb51aed5e50ffca6a20bebd2c762 Mon Sep 17 00:00:00 2001 From: Cyril Sobierajewicz Date: Wed, 3 Jun 2020 22:26:33 +0200 Subject: [PATCH 2/3] Recurse under foralls when inferring nominal roles from kinds --- src/Language/PureScript/TypeChecker/Roles.hs | 2 ++ tests/purs/failing/CoercibleForeign3.out | 28 ++++++++++++++++++++ tests/purs/failing/CoercibleForeign3.purs | 9 +++++++ 3 files changed, 39 insertions(+) create mode 100644 tests/purs/failing/CoercibleForeign3.out create mode 100644 tests/purs/failing/CoercibleForeign3.purs diff --git a/src/Language/PureScript/TypeChecker/Roles.hs b/src/Language/PureScript/TypeChecker/Roles.hs index 7e8da42278..eac4934285 100644 --- a/src/Language/PureScript/TypeChecker/Roles.hs +++ b/src/Language/PureScript/TypeChecker/Roles.hs @@ -145,5 +145,7 @@ rolesFromForeignTypeKind go acc = \case TypeApp _ (TypeApp _ fn _k1) k2 | eqType fn tyFunction -> go (Nominal : acc) k2 + ForAll _ _ _ k _ -> + go acc k _k -> acc diff --git a/tests/purs/failing/CoercibleForeign3.out b/tests/purs/failing/CoercibleForeign3.out new file mode 100644 index 0000000000..9bf213691d --- /dev/null +++ b/tests/purs/failing/CoercibleForeign3.out @@ -0,0 +1,28 @@ +Error found: +in module Main +at tests/purs/failing/CoercibleForeign3.purs:9:20 - 9:26 (line 9, column 20 - line 9, column 26) + + No type class instance was found for +   +  Prim.Coerce.Coercible (Foreign @k0 a1 b2) +  (Foreign @k0 a1 c3) +   + +while checking that type forall (a :: Type) (b :: Type). Coercible 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 +in value declaration foreignToForeign + +where k0 is a rigid type variable + bound at (line 9, column 20 - line 9, column 26) + a1 is a rigid type variable + bound at (line 9, column 20 - line 9, column 26) + b2 is a rigid type variable + bound at (line 9, column 20 - line 9, column 26) + c3 is a rigid type variable + bound at (line 9, column 20 - line 9, column 26) + +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/CoercibleForeign3.purs b/tests/purs/failing/CoercibleForeign3.purs new file mode 100644 index 0000000000..2abd379b12 --- /dev/null +++ b/tests/purs/failing/CoercibleForeign3.purs @@ -0,0 +1,9 @@ +-- @shouldFailWith NoInstanceFound +module Main where + +import Safe.Coerce (coerce) + +foreign import data Foreign :: ∀ k. k -> k -> Type + +foreignToForeign :: ∀ k (a :: k) (b :: k) (c :: k). Foreign a b -> Foreign a c +foreignToForeign = coerce From 308b44b0c6f98ddd8df068a14f86da9989c2264a Mon Sep 17 00:00:00 2001 From: Cyril Sobierajewicz Date: Wed, 3 Jun 2020 23:49:41 +0200 Subject: [PATCH 3/3] Infer nominal roles from kinds arity --- src/Language/PureScript/TypeChecker/Roles.hs | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/src/Language/PureScript/TypeChecker/Roles.hs b/src/Language/PureScript/TypeChecker/Roles.hs index eac4934285..bc0f0c7b5d 100644 --- a/src/Language/PureScript/TypeChecker/Roles.hs +++ b/src/Language/PureScript/TypeChecker/Roles.hs @@ -139,13 +139,11 @@ inferRoles env tyName -- the absence of a role signature, provides the safest default for a type whose -- constructors are opaque to us. rolesFromForeignTypeKind :: SourceType -> [Role] -rolesFromForeignTypeKind - = go [] - where - go acc = \case - TypeApp _ (TypeApp _ fn _k1) k2 | eqType fn tyFunction -> - go (Nominal : acc) k2 - ForAll _ _ _ k _ -> - go acc k - _k -> - acc +rolesFromForeignTypeKind k = replicate (kindArity k) Nominal + +kindArity :: SourceType -> Int +kindArity = go 0 where + go n (TypeApp _ (TypeApp _ fn _) k) + | fn == tyFunction = go (n + 1) k + go n (ForAll _ _ _ k _) = go n k + go n _ = n