Treat all TyCon with hole names as skolem abstract.
authorEdward Z. Yang <ezyang@cs.stanford.edu>
Fri, 24 Feb 2017 23:58:09 +0000 (15:58 -0800)
committerEdward Z. Yang <ezyang@cs.stanford.edu>
Mon, 27 Feb 2017 00:03:13 +0000 (16:03 -0800)
Summary:
Fixes #13335.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>
Test Plan: validate

Reviewers: goldfire, austin, simonpj, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D3211

18 files changed:
compiler/backpack/RnModIface.hs
compiler/iface/IfaceSyn.hs
compiler/iface/MkIface.hs
compiler/iface/TcIface.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/types/TyCon.hs
testsuite/tests/backpack/should_fail/bkpfail10.stderr
testsuite/tests/backpack/should_fail/bkpfail23.stderr
testsuite/tests/backpack/should_fail/bkpfail25.stderr
testsuite/tests/backpack/should_fail/bkpfail26.stderr
testsuite/tests/backpack/should_fail/bkpfail27.stderr
testsuite/tests/roles/should_fail/Roles12.stderr
testsuite/tests/roles/should_fail/T9204.stderr
testsuite/tests/typecheck/should_fail/T12035.stderr
testsuite/tests/typecheck/should_fail/T12035j.stderr
testsuite/tests/typecheck/should_fail/T3468.stderr

index d4af5cc..7180918 100644 (file)
@@ -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
index 5ed30c9..0a50e86 100644 (file)
@@ -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"
index 158e48f..27bb9e0 100644 (file)
@@ -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
index 5d41232..ffe29c6 100644 (file)
@@ -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
index c668208..8688c77 100644 (file)
@@ -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 }) }
 
index 107162b..dafc4b8 100644 (file)
@@ -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")
index 805120c..a45df3a 100644 (file)
@@ -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
index dadf1ba..f98da7b 100644 (file)
@@ -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.
index c521451..70b0853 100644 (file)
@@ -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]
 
index de4026a..00a19e2 100644 (file)
@@ -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]
index ef2d035..936fbb5 100644 (file)
@@ -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]
index fa192c2..01c8c32 100644 (file)
@@ -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]
index 3d1446a..dfadb40 100644 (file)
@@ -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]
index ac57e2b..d1872f3 100644 (file)
@@ -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.
index e5e9925..998f17c 100644 (file)
@@ -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.
index 9e5ff78..c6113ea 100644 (file)
@@ -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
index 9e5ff78..c6113ea 100644 (file)
@@ -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
index cae8eed..1f8bdcb 100644 (file)
@@ -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