Commit 984c6097 authored by Edward Z. Yang's avatar Edward Z. Yang

Disallow non-nullary constraint synonyms on class.

Test Plan: validate

Reviewers: simonpj, bgamari, austin

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D3230
parent 4aada7a6
......@@ -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{} =
......
......@@ -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]
......@@ -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, [''])
{-# 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]
[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]
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment