diff options
author | Edward Z. Yang <ezyang@cs.stanford.edu> | 2017-02-27 15:52:27 -0800 |
---|---|---|
committer | Edward Z. Yang <ezyang@cs.stanford.edu> | 2017-03-02 15:58:18 -0800 |
commit | 984c6097c63096d10789f6eb6da6f6656195cdaf (patch) | |
tree | 514104e1e1426db8d4f421187c5b8c2e650b938f | |
parent | 4aada7a6c13752652cfce5e04f015a8909553917 (diff) | |
download | haskell-984c6097c63096d10789f6eb6da6f6656195cdaf.tar.gz |
Disallow non-nullary constraint synonyms on class.
Test Plan: validate
Reviewers: simonpj, bgamari, austin
Subscribers: thomie
Differential Revision: https://phabricator.haskell.org/D3230
-rw-r--r-- | compiler/typecheck/TcRnDriver.hs | 143 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_compile/bkp39.bkp | 6 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_fail/all.T | 1 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_fail/bkpfail46.bkp | 17 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_fail/bkpfail46.stderr | 20 |
5 files changed, 112 insertions, 75 deletions
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index 5634891f4f..e08d2e19d4 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -1000,78 +1000,26 @@ checkBootTyCon is_boot tc1 tc2 checkRoles roles1 roles2 `andThenCheck` check (eqTypeX env syn_rhs1 syn_rhs2) empty -- nothing interesting to say - -- An abstract TyCon can be implemented using a type synonym, but ONLY - -- if the type synonym is nullary and has no type family applications. - -- This arises from two properties of skolem abstract data: - -- - -- For any T (with some number of paramaters), - -- - -- 1. T is a valid type (it is "curryable"), and - -- - -- 2. T is valid in an instance head (no type families). - -- - -- See also 'HowAbstract' and Note [Skolem abstract data]. - -- - | isAbstractTyCon tc1 - , not is_boot -- don't support for hs-boot yet + -- This allows abstract 'data T a' to be implemented using 'type T = ...' + -- See Note [Synonyms implement abstract data] + | not is_boot -- don't support for hs-boot yet + , isAbstractTyCon tc1 , Just (tvs, ty) <- synTyConDefn_maybe tc2 , Just (tc2', args) <- tcSplitTyConApp_maybe ty - = check (null (tcTyFamInsts ty)) - (text "Illegal type family application in implementation of abstract data.") - `andThenCheck` - check (null tvs) - (text "Illegal parameterized type synonym in implementation of abstract data." $$ - text "(Try eta reducing your type synonym so that it is nullary.)") - `andThenCheck` - -- Don't report roles errors unless the type synonym is nullary - checkUnless (not (null tvs)) $ - ASSERT( null roles2 ) - -- If we have something like: - -- - -- signature H where - -- data T a - -- module H where - -- data K a b = ... - -- type T = K Int - -- - -- we need to drop the first role of K when comparing! - checkRoles roles1 (drop (length args) (tyConRoles tc2')) - - -- Note [Constraint synonym implements abstract class] - -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -- This clause allows an abstract class to be implemented with a constraint - -- synonym. For instance, consider a signature requiring an abstract class, - -- - -- signature ASig where - -- class K a - -- - -- Since K has no methods (i.e. is abstract), the module implementing this - -- signature may want to implement it using a constraint synonym of another - -- class, - -- - -- module AnImpl where - -- class SomeClass a where ... - -- type K a = SomeClass a - -- - -- This was originally requested in #12679. For now, we only allow this - -- in hsig files (@not is_boot@). - - | not is_boot + = checkSynAbsData tvs ty tc2' args + + -- This allows abstract 'class C a' to be implemented using 'type C = ...' + -- This was originally requested in #12679. + -- See Note [Synonyms implement abstract data] + | not is_boot -- don't support for hs-boot yet , Just c1 <- tyConClass_maybe tc1 , let (_, _clas_fds1, sc_theta1, _, ats1, op_stuff1) = classExtraBigSig c1 -- Is it abstract? , null sc_theta1 && null op_stuff1 && null ats1 , Just (tvs, ty) <- synTyConDefn_maybe tc2 - = -- The synonym may or may not be eta-expanded, so we need to - -- massage it into the correct form before checking if roles - -- match. - if length tvs == length roles1 - then checkRoles roles1 roles2 - else case tcSplitTyConApp_maybe ty of - Just (tc2', args) -> - checkRoles roles1 (drop (length args) (tyConRoles tc2') ++ roles2) - Nothing -> Just roles_msg + , Just (tc2', args) <- tcSplitTyConApp_maybe ty + = checkSynAbsData tvs ty tc2' args -- TODO: We really should check if the fundeps are satisfied, but -- there is not an obvious way to do this for a constraint synonym. -- So for now, let it all through (it won't cause segfaults, anyway). @@ -1131,10 +1079,11 @@ checkBootTyCon is_boot tc1 tc2 -- Note [Role subtyping] -- ~~~~~~~~~~~~~~~~~~~~~ - -- In the current formulation of roles, role subtyping is only OK if - -- the "abstract" TyCon was not injective. Among the most notable - -- examples of non-injective TyCons are abstract data, which can be - -- implemented via newtypes (which are not injective). The key example is + -- In the current formulation of roles, role subtyping is only OK if the + -- "abstract" TyCon was not representationally injective. Among the most + -- notable examples of non representationally injective TyCons are abstract + -- data, which can be implemented via newtypes (which are not + -- representationally injective). The key example is -- in this example from #13140: -- -- -- In an hsig file @@ -1147,9 +1096,9 @@ checkBootTyCon is_boot tc1 tc2 -- -- We must NOT allow foo to typecheck, because if we instantiate -- T with a concrete data type with a phantom role would cause - -- Coercible (T a) (T b) to be provable. Fortunately, if T - -- is not injective, we cannot make the inference that a ~N b - -- if T a ~R T b. + -- Coercible (T a) (T b) to be provable. Fortunately, if T is not + -- representationally injective, we cannot make the inference that a ~N b if + -- T a ~R T b. -- -- Unconditional role subtyping would be possible if we setup -- an extra set of roles saying when we can project out coercions @@ -1179,10 +1128,62 @@ checkBootTyCon is_boot tc1 tc2 -- (i.e., a user could explicitly ask for one behavior or another) but -- the current role system isn't expressive enough to do this. -- Having explict proj-roles would solve this problem. + rolesSubtypeOf [] [] = True + -- NB: this relation is the OPPOSITE of the subroling relation rolesSubtypeOf (x:xs) (y:ys) = x >= y && rolesSubtypeOf xs ys rolesSubtypeOf _ _ = False + -- Note [Synonyms implement abstract data] + -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + -- An abstract data type or class can be implemented using a type synonym, + -- but ONLY if the type synonym is nullary and has no type family + -- applications. This arises from two properties of skolem abstract data: + -- + -- For any T (with some number of paramaters), + -- + -- 1. T is a valid type (it is "curryable"), and + -- + -- 2. T is valid in an instance head (no type families). + -- + -- See also 'HowAbstract' and Note [Skolem abstract data]. + + -- | Given @type T tvs = ty@, where @ty@ decomposes into @tc2' args@, + -- check that this synonym is an acceptable implementation of @tc1@. + -- See Note [Synonyms implement abstract data] + checkSynAbsData :: [TyVar] -> Type -> TyCon -> [Type] -> Maybe SDoc + checkSynAbsData tvs ty tc2' args = + check (null (tcTyFamInsts ty)) + (text "Illegal type family application in implementation of abstract data.") + `andThenCheck` + check (null tvs) + (text "Illegal parameterized type synonym in implementation of abstract data." $$ + text "(Try eta reducing your type synonym so that it is nullary.)") + `andThenCheck` + -- Don't report roles errors unless the type synonym is nullary + checkUnless (not (null tvs)) $ + ASSERT( null roles2 ) + -- If we have something like: + -- + -- signature H where + -- data T a + -- module H where + -- data K a b = ... + -- type T = K Int + -- + -- we need to drop the first role of K when comparing! + checkRoles roles1 (drop (length args) (tyConRoles tc2')) +{- + -- Hypothetically, if we were allow to non-nullary type synonyms, here + -- is how you would check the roles + if length tvs == length roles1 + then checkRoles roles1 roles2 + else case tcSplitTyConApp_maybe ty of + Just (tc2', args) -> + checkRoles roles1 (drop (length args) (tyConRoles tc2') ++ roles2) + Nothing -> Just roles_msg +-} + eqAlgRhs _ AbstractTyCon _rhs2 = checkSuccess -- rhs2 is guaranteed to be injective, since it's an AlgTyCon eqAlgRhs _ tc1@DataTyCon{} tc2@DataTyCon{} = diff --git a/testsuite/tests/backpack/should_compile/bkp39.bkp b/testsuite/tests/backpack/should_compile/bkp39.bkp index bf98b10c96..a6216edc24 100644 --- a/testsuite/tests/backpack/should_compile/bkp39.bkp +++ b/testsuite/tests/backpack/should_compile/bkp39.bkp @@ -3,7 +3,6 @@ unit p where signature A where import Prelude hiding ((==)) class K a - class K2 a infix 4 == (==) :: K a => a -> a -> Bool module M where @@ -11,8 +10,7 @@ unit p where import A f a b c = a == b && b == c unit q where - module A(K, K2, (==)) where - type K a = Eq a - type K2 = Eq + module A(K, (==)) where + type K = Eq unit r where dependency p[A=q:A] diff --git a/testsuite/tests/backpack/should_fail/all.T b/testsuite/tests/backpack/should_fail/all.T index 77b7aa23d8..82b4e6803b 100644 --- a/testsuite/tests/backpack/should_fail/all.T +++ b/testsuite/tests/backpack/should_fail/all.T @@ -41,3 +41,4 @@ test('bkpfail42', normal, backpack_compile_fail, ['']) test('bkpfail43', normal, backpack_compile_fail, ['']) test('bkpfail44', normal, backpack_compile_fail, ['']) test('bkpfail45', normal, backpack_compile_fail, ['']) +test('bkpfail46', normal, backpack_compile_fail, ['']) diff --git a/testsuite/tests/backpack/should_fail/bkpfail46.bkp b/testsuite/tests/backpack/should_fail/bkpfail46.bkp new file mode 100644 index 0000000000..0fc8b676a8 --- /dev/null +++ b/testsuite/tests/backpack/should_fail/bkpfail46.bkp @@ -0,0 +1,17 @@ +{-# LANGUAGE ConstraintKinds #-} +unit p where + signature A where + import Prelude hiding ((==)) + class K a + infix 4 == + (==) :: K a => a -> a -> Bool + module M where + import Prelude hiding ((==)) + import A + f a b c = a == b && b == c +unit q where + module A(K, (==)) where + -- This won't match because it's not nullary + type K a = Eq a +unit r where + dependency p[A=q:A] diff --git a/testsuite/tests/backpack/should_fail/bkpfail46.stderr b/testsuite/tests/backpack/should_fail/bkpfail46.stderr new file mode 100644 index 0000000000..9aeaccbb7e --- /dev/null +++ b/testsuite/tests/backpack/should_fail/bkpfail46.stderr @@ -0,0 +1,20 @@ +[1 of 3] Processing p + [1 of 2] Compiling A[sig] ( p/A.hsig, nothing ) + [2 of 2] Compiling M ( p/M.hs, nothing ) +[2 of 3] Processing q + Instantiating q + [1 of 1] Compiling A ( q/A.hs, bkpfail46.out/q/A.o ) +[3 of 3] Processing r + Instantiating r + [1 of 1] Including p[A=q:A] + Instantiating p[A=q:A] + [1 of 2] Compiling A[sig] ( p/A.hsig, bkpfail46.out/p/p-HVmFlcYSefiK5n1aDP1v7x/A.o ) + +bkpfail46.bkp:15:9: error: + ⢠Type constructor âKâ has conflicting definitions in the module + and its hsig file + Main module: type K a = GHC.Classes.Eq a :: Constraint + Hsig file: class K a + Illegal parameterized type synonym in implementation of abstract data. + (Try eta reducing your type synonym so that it is nullary.) + ⢠while checking that q:A implements signature A in p[A=q:A] |