Commit 9603de6a authored by Edward Z. Yang's avatar Edward Z. Yang

Treat all TyCon with hole names as skolem abstract.

Summary:
Fixes #13335.
Signed-off-by: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: goldfire, austin, simonpj, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D3211
parent 5c95e6b7
......@@ -512,7 +512,7 @@ rnIfaceConDecls :: Rename IfaceConDecls
rnIfaceConDecls (IfDataTyCon ds)
= IfDataTyCon <$> mapM rnIfaceConDecl ds
rnIfaceConDecls (IfNewTyCon d) = IfNewTyCon <$> rnIfaceConDecl d
rnIfaceConDecls (IfAbstractTyCon b) = pure (IfAbstractTyCon b)
rnIfaceConDecls IfAbstractTyCon = pure IfAbstractTyCon
rnIfaceConDecl :: Rename IfaceConDecl
rnIfaceConDecl d = do
......
......@@ -62,7 +62,7 @@ import Fingerprint
import Binary
import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue )
import Var( TyVarBndr(..) )
import TyCon ( Role (..), Injectivity(..), HowAbstract(..) )
import TyCon ( Role (..), Injectivity(..) )
import Util( filterOut, filterByList )
import DataCon (SrcStrictness(..), SrcUnpackedness(..))
import Lexeme (isLexSym)
......@@ -207,7 +207,7 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr]
-- See Note [Storing compatibility] in CoAxiom
data IfaceConDecls
= IfAbstractTyCon HowAbstract -- c.f TyCon.AbstractTyCon
= IfAbstractTyCon -- c.f TyCon.AbstractTyCon
| IfDataTyCon [IfaceConDecl] -- Data type decls
| IfNewTyCon IfaceConDecl -- Newtype decls
......@@ -367,9 +367,9 @@ See [http://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/RecompilationAvoid
-}
visibleIfConDecls :: IfaceConDecls -> [IfaceConDecl]
visibleIfConDecls (IfAbstractTyCon {}) = []
visibleIfConDecls IfAbstractTyCon = []
visibleIfConDecls (IfDataTyCon cs) = cs
visibleIfConDecls (IfNewTyCon c) = [c]
visibleIfConDecls (IfNewTyCon c) = [c]
ifaceDeclImplicitBndrs :: IfaceDecl -> [OccName]
-- *Excludes* the 'main' name, but *includes* the implicitly-bound names
......@@ -385,7 +385,7 @@ ifaceDeclImplicitBndrs :: IfaceDecl -> [OccName]
ifaceDeclImplicitBndrs (IfaceData {ifName = tc_name, ifCons = cons })
= case cons of
IfAbstractTyCon {} -> []
IfAbstractTyCon -> []
IfNewTyCon cd -> mkNewTyCoOcc (occName tc_name) : ifaceConDeclImplicitBndrs cd
IfDataTyCon cds -> concatMap ifaceConDeclImplicitBndrs cds
......@@ -712,10 +712,7 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
| otherwise = Nothing
pp_nd = case condecls of
IfAbstractTyCon how ->
case how of
DistinctNominalAbstract -> text "{- abstract -} data"
SkolemAbstract -> text "{- skolem -} data"
IfAbstractTyCon{} -> text "data"
IfDataTyCon{} -> text "data"
IfNewTyCon{} -> text "newtype"
......@@ -1717,13 +1714,13 @@ instance Binary IfaceAxBranch where
return (IfaceAxBranch a1 a2 a3 a4 a5 a6)
instance Binary IfaceConDecls where
put_ bh (IfAbstractTyCon d) = putByte bh 0 >> put_ bh d
put_ bh IfAbstractTyCon = putByte bh 0
put_ bh (IfDataTyCon cs) = putByte bh 1 >> put_ bh cs
put_ bh (IfNewTyCon c) = putByte bh 2 >> put_ bh c
get bh = do
h <- getByte bh
case h of
0 -> liftM IfAbstractTyCon $ get bh
0 -> return IfAbstractTyCon
1 -> liftM IfDataTyCon (get bh)
2 -> liftM IfNewTyCon (get bh)
_ -> error "Binary(IfaceConDecls).get: Invalid IfaceConDecls"
......
......@@ -1626,7 +1626,7 @@ tyConToIfaceDecl env tycon
ifaceConDecls (DataTyCon { data_cons = cons }) = IfDataTyCon (map ifaceConDecl cons)
ifaceConDecls (TupleTyCon { data_con = con }) = IfDataTyCon [ifaceConDecl con]
ifaceConDecls (SumTyCon { data_cons = cons }) = IfDataTyCon (map ifaceConDecl cons)
ifaceConDecls (AbstractTyCon distinct) = IfAbstractTyCon distinct
ifaceConDecls AbstractTyCon = IfAbstractTyCon
-- The AbstractTyCon case happens when a TyCon has been trimmed
-- during tidying.
-- Furthermore, tyThingToIfaceDecl is also used in TcRnDriver
......
......@@ -207,7 +207,7 @@ typecheckIface iface
-- | Returns true if an 'IfaceDecl' is for @data T@ (an abstract data type)
isAbstractIfaceDecl :: IfaceDecl -> Bool
isAbstractIfaceDecl IfaceData{ ifCons = IfAbstractTyCon _ } = True
isAbstractIfaceDecl IfaceData{ ifCons = IfAbstractTyCon } = True
isAbstractIfaceDecl IfaceClass{ ifCtxt = [], ifSigs = [], ifATs = [] } = True
isAbstractIfaceDecl IfaceFamily{ ifFamFlav = IfaceAbstractClosedSynFamilyTyCon } = True
isAbstractIfaceDecl _ = False
......@@ -804,7 +804,7 @@ tc_ax_branch prev_branches
tcIfaceDataCons :: Name -> TyCon -> [TyConBinder] -> IfaceConDecls -> IfL AlgTyConRhs
tcIfaceDataCons tycon_name tycon tc_tybinders if_cons
= case if_cons of
IfAbstractTyCon dis -> return (AbstractTyCon dis)
IfAbstractTyCon -> return AbstractTyCon
IfDataTyCon cons -> do { data_cons <- mapM tc_con_decl cons
; return (mkDataTyConRhs data_cons) }
IfNewTyCon con -> do { data_con <- tc_con_decl con
......
......@@ -979,8 +979,8 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
; stopWith ev "Decomposed TyConApp" }
else canEqFailure ev eq_rel ty1 ty2 }
-- See Note [Skolem abstract data] (at SkolemAbstract)
| isSkolemAbstractTyCon tc1 || isSkolemAbstractTyCon tc2
-- See Note [Skolem abstract data] (at tyConSkolem)
| tyConSkolem tc1 || tyConSkolem tc2
= do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
; continueWith (CIrredEvCan { cc_ev = ev }) }
......
......@@ -999,7 +999,7 @@ checkBootTyCon is_boot tc1 tc2
check (roles1 == roles2) roles_msg `andThenCheck`
check (eqTypeX env syn_rhs1 syn_rhs2) empty -- nothing interesting to say
-- A skolem abstract TyCon can be implemented using a type synonym, but ONLY
-- 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:
--
......@@ -1011,7 +1011,8 @@ checkBootTyCon is_boot tc1 tc2
--
-- See also 'HowAbstract' and Note [Skolem abstract data].
--
| isSkolemAbstractTyCon tc1
| isAbstractTyCon tc1
, not is_boot -- don't support for hs-boot yet
, Just (tvs, ty) <- synTyConDefn_maybe tc2
, Just (tc2', args) <- tcSplitTyConApp_maybe ty
= check (null (tcTyFamInsts ty))
......@@ -1117,7 +1118,7 @@ checkBootTyCon is_boot tc1 tc2
(text "Roles on abstract types default to" <+>
quotes (text "representational") <+> text "in boot files.")
eqAlgRhs _ (AbstractTyCon _) _rhs2
eqAlgRhs _ AbstractTyCon _rhs2
= checkSuccess -- rhs2 is guaranteed to be injective, since it's an AlgTyCon
eqAlgRhs _ tc1@DataTyCon{} tc2@DataTyCon{} =
checkListBy eqCon (data_cons tc1) (data_cons tc2) (text "constructors")
......
......@@ -965,13 +965,10 @@ tcDataDefn roles_info
-- In hs-boot, a 'data' declaration with no constructors
-- indicates an nominally distinct abstract data type.
mk_tc_rhs HsBootFile _ []
= return (AbstractTyCon DistinctNominalAbstract)
= return AbstractTyCon
-- In hsig, a 'data' declaration indicates a skolem
-- abstract data type. See 'HowAbstract' and Note
-- [Skolem abstract data] for more commentary.
mk_tc_rhs HsigFile _ []
= return (AbstractTyCon SkolemAbstract)
mk_tc_rhs HsigFile _ [] -- ditto
= return AbstractTyCon
mk_tc_rhs _ tycon data_cons
= case new_or_data of
......
......@@ -10,7 +10,7 @@ The @TyCon@ datatype
module TyCon(
-- * Main TyCon data types
TyCon, AlgTyConRhs(..), HowAbstract(..), visibleDataCons,
TyCon, AlgTyConRhs(..), visibleDataCons,
AlgTyConFlav(..), isNoParent,
FamTyConFlav(..), Role(..), Injectivity(..),
RuntimeRepInfo(..),
......@@ -56,7 +56,6 @@ module TyCon(
isDataSumTyCon_maybe,
isEnumerationTyCon,
isNewTyCon, isAbstractTyCon,
isSkolemAbstractTyCon,
isFamilyTyCon, isOpenFamilyTyCon,
isTypeFamilyTyCon, isDataFamilyTyCon,
isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
......@@ -71,6 +70,7 @@ module TyCon(
-- ** Extracting information out of TyCons
tyConName,
tyConSkolem,
tyConKind,
tyConUnique,
tyConTyVars,
......@@ -739,7 +739,6 @@ data AlgTyConRhs
-- it's represented by a pointer. Used when we export a data type
-- abstractly into an .hi file.
= AbstractTyCon
HowAbstract
-- | Information about those 'TyCon's derived from a @data@
-- declaration. This includes data types with no constructors at
......@@ -797,72 +796,6 @@ data AlgTyConRhs
-- again check Trac #1072.
}
-- | An 'AbstractTyCon' represents some matchable type constructor (i.e., valid
-- in instance heads), for which we do not know the implementation. We refer to
-- these as "abstract data".
--
-- At the moment, there are two flavors of abstract data, corresponding
-- to whether or not the abstract data declaration occurred in an hs-boot
-- file or an hsig file.
--
data HowAbstract
-- | Nominally distinct abstract data arises from abstract data
-- declarations in an hs-boot file.
--
-- Abstract data of this form is guaranteed to be nominally distinct
-- from all other declarations in the system; e.g., if I have
-- a @data T@ and @data S@ in an hs-boot file, it is safe to
-- assume that they will never equal each other. This is something
-- of an implementation accident: it is a lot easier to assume that
-- @data T@ in @A.hs-boot@ indicates there will be @data T = ...@
-- in @A.hs@, than to permit the possibility that @A.hs@ reexports
-- it from somewhere else.
= DistinctNominalAbstract
-- Note [Skolem abstract data]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Skolem abstract data arises from abstract data declarations
-- in an hsig file.
--
-- The best analogy is to interpret the abstract types in Backpack
-- unit as elaborating to universally quantified type variables;
-- e.g.,
--
-- unit p where
-- signature H where
-- data T
-- data S
-- module M where
-- import H
-- f :: (T ~ S) => a -> b
-- f x = x
--
-- elaborates as (with some fake structural types):
--
-- p :: forall t s. { f :: forall a b. t ~ s => a -> b }
-- p = { f = \x -> x } -- ill-typed
--
-- It is clear that inside p, t ~ s is not provable (and
-- if we tried to write a function to cast t to s, that
-- would not work), but if we call p @Int @Int, clearly Int ~ Int
-- is provable. The skolem variables are all distinct from
-- one another, but we can't make assumptions like "f is
-- inaccessible", because the skolem variables will get
-- instantiated eventually!
--
-- Skolem abstract data still has the constraint that there
-- are no type family applications, to keep this data matchable.
| SkolemAbstract
instance Binary HowAbstract where
put_ bh DistinctNominalAbstract = putByte bh 0
put_ bh SkolemAbstract = putByte bh 1
get bh = do { h <- getByte bh
; case h of
0 -> return DistinctNominalAbstract
_ -> return SkolemAbstract }
-- | Some promoted datacons signify extra info relevant to GHC. For example,
-- the @IntRep@ constructor of @RuntimeRep@ corresponds to the 'IntRep'
-- constructor of 'PrimRep'. This data structure allows us to store this
......@@ -1642,15 +1575,9 @@ isFunTyCon _ = False
-- | Test if the 'TyCon' is algebraic but abstract (invisible data constructors)
isAbstractTyCon :: TyCon -> Bool
isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon {} }) = True
isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon }) = True
isAbstractTyCon _ = False
-- | Test if the 'TyCon' is totally abstract; i.e., it is not even certain
-- to be nominally distinct.
isSkolemAbstractTyCon :: TyCon -> Bool
isSkolemAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon SkolemAbstract }) = True
isSkolemAbstractTyCon _ = False
-- | Make an fake, recovery 'TyCon' from an existing one.
-- Used when recovering from errors
makeRecoveryTyCon :: TyCon -> TyCon
......@@ -2454,3 +2381,53 @@ checkRecTc (RC bound rec_nts) tc
Nothing -> Just (RC bound (extendNameEnv rec_nts tc_name 1))
where
tc_name = tyConName tc
-- | Returns whether or not this 'TyCon' is definite, or a hole
-- that may be filled in at some later point. See Note [Skolem abstract data]
tyConSkolem :: TyCon -> Bool
tyConSkolem = isHoleName . tyConName
-- Note [Skolem abstract data]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Skolem abstract data arises from data declarations in an hsig file.
--
-- The best analogy is to interpret the types declared in signature files as
-- elaborating to universally quantified type variables; e.g.,
--
-- unit p where
-- signature H where
-- data T
-- data S
-- module M where
-- import H
-- f :: (T ~ S) => a -> b
-- f x = x
--
-- elaborates as (with some fake structural types):
--
-- p :: forall t s. { f :: forall a b. t ~ s => a -> b }
-- p = { f = \x -> x } -- ill-typed
--
-- It is clear that inside p, t ~ s is not provable (and
-- if we tried to write a function to cast t to s, that
-- would not work), but if we call p @Int @Int, clearly Int ~ Int
-- is provable. The skolem variables are all distinct from
-- one another, but we can't make assumptions like "f is
-- inaccessible", because the skolem variables will get
-- instantiated eventually!
--
-- Skolem abstractness can apply to "non-abstract" data as well):
--
-- unit p where
-- signature H1 where
-- data T = MkT
-- signature H2 where
-- data T = MkT
-- module M where
-- import qualified H1
-- import qualified H2
-- f :: (H1.T ~ H2.T) => a -> b
-- f x = x
--
-- This is why the test is on the original name of the TyCon,
-- not whether it is abstract or not.
......@@ -13,7 +13,7 @@ bkpfail10.bkp:8:9: error:
• Type constructor ‘H’ has conflicting definitions in the module
and its hsig file
Main module: data H a = H a
Hsig file: {- skolem -} data H
Hsig file: data H
The types have different kinds
• while checking that q:H implements signature H in p[H=q:H]
......
......@@ -15,7 +15,7 @@ bkpfail23.bkp:14:9: error:
and its hsig file
Main module: type F a = ()
Hsig file: type role F phantom
{- skolem -} data F a
data F a
Illegal parameterized type synonym in implementation of abstract data.
(Try eta reducing your type synonym so that it is nullary.)
• while checking that h:H implements signature H in p[H=h:H]
......@@ -19,5 +19,5 @@ bkpfail25.bkp:12:9: error:
• Type constructor ‘T’ has conflicting definitions in the module
and its hsig file
Main module: type T a = a
Hsig file: {- skolem -} data T a
Hsig file: data T a
• while checking that q:H implements signature H in p[H=q:H]
......@@ -14,7 +14,7 @@ bkpfail26.bkp:15:9: error:
• Type constructor ‘T’ has conflicting definitions in the module
and its hsig file
Main module: type T a = [a]
Hsig file: {- skolem -} data T a
Hsig file: data T 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:H implements signature H in p[H=q:H]
......@@ -14,6 +14,6 @@ bkpfail27.bkp:15:9: error:
• Type constructor ‘T’ has conflicting definitions in the module
and its hsig file
Main module: type T = F
Hsig file: {- skolem -} data T
Hsig file: data T
Illegal type family application in implementation of abstract data.
• while checking that q:H implements signature H in p[H=q:H]
......@@ -4,6 +4,6 @@ Roles12.hs:5:1: error:
and its hs-boot file
Main module: type role T phantom
data T a
Boot file: {- abstract -} data T a
Boot file: data T a
The roles do not match.
Roles on abstract types default to ‘representational’ in boot files.
......@@ -4,6 +4,6 @@ T9204.hs:6:1: error:
and its hs-boot file
Main module: type role D phantom
data D a
Boot file: {- abstract -} data D a
Boot file: data D a
The roles do not match.
Roles on abstract types default to ‘representational’ in boot files.
......@@ -3,4 +3,4 @@ T12035.hs-boot:2:1: error:
Type constructor ‘T’ has conflicting definitions in the module
and its hs-boot file
Main module: type T = Bool
Boot file: {- abstract -} data T
Boot file: data T
......@@ -3,4 +3,4 @@ T12035.hs-boot:2:1: error:
Type constructor ‘T’ has conflicting definitions in the module
and its hs-boot file
Main module: type T = Bool
Boot file: {- abstract -} data T
Boot file: data T
......@@ -5,5 +5,5 @@ T3468.hs-boot:3:1: error:
Main module: type role Tool phantom
data Tool d where
F :: a -> Tool d
Boot file: {- abstract -} data Tool
Boot file: data Tool
The types have different kinds
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