Export a tiny bit more info with AbstractTyCon (fixes #5424)
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 2 Sep 2011 16:43:53 +0000 (17:43 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 2 Sep 2011 16:43:53 +0000 (17:43 +0100)
When we compile -O0 we put type constructors in the interface file
without their data constructors -- an AbstractTyCon.  But in a
client module, to give good pattern-match exhaustiveness warnings,
we need to know the difference between a data type and a newtype.
(The latter can be coerced to another type, but a data type can't.)
See Note [Pruning dead case alternatives] in Unify.

Because we weren't conveying this info, we were getting bogus
warnings about inexhaustive patterm matches with GADTs, and
(confusingly) these warnings woudl come and go depending on
whether you were compiling with -O.

This patch makes AbstractTyCon carry a flag indicating whether
the type constructor is "distinct"; two distinct TyCons cannot
be coerced into eachother (except by unsafeCoerce, in which case
all bets are off).

HEADS UP: interface file format changes slightly, so you need
to make clean.

compiler/iface/BinIface.hs
compiler/iface/BuildTyCl.lhs
compiler/iface/IfaceSyn.lhs
compiler/iface/MkIface.lhs
compiler/iface/TcIface.lhs
compiler/typecheck/TcDeriv.lhs
compiler/typecheck/TcRnDriver.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/types/TyCon.lhs
compiler/types/Unify.lhs

index 94860f9..26b3d9c 100644 (file)
@@ -1416,7 +1416,7 @@ instance Binary OverlapFlag where
                  _ -> panic ("get OverlapFlag " ++ show h)
 
 instance Binary IfaceConDecls where
-    put_ bh IfAbstractTyCon = putByte bh 0
+    put_ bh (IfAbstractTyCon d) = do { putByte bh 0; put_ bh d }
     put_ bh IfOpenDataTyCon = putByte bh 1
     put_ bh (IfDataTyCon cs) = do { putByte bh 2
                                  ; put_ bh cs }
@@ -1425,7 +1425,7 @@ instance Binary IfaceConDecls where
     get bh = do
            h <- getByte bh
            case h of
-             0 -> return IfAbstractTyCon
+             0 -> do { d <- get bh; return (IfAbstractTyCon d) }
              1 -> return IfOpenDataTyCon
              2 -> do cs <- get bh
                      return (IfDataTyCon cs)
index b9a6ab9..7f2ade2 100644 (file)
@@ -9,7 +9,7 @@ module BuildTyCl (
         buildAlgTyCon, 
         buildDataCon,
        TcMethInfo, buildClass,
-       mkAbstractTyConRhs, 
+       distinctAbstractTyConRhs, totallyAbstractTyConRhs, 
        mkNewTyConRhs, mkDataTyConRhs, 
         newImplicitBinder
     ) where
@@ -105,8 +105,9 @@ mkFamInstParentInfo tc_name tvs (family, instTys) rep_tycon
        ; return $ FamInstTyCon family instTys co_tycon }
     
 ------------------------------------------------------
-mkAbstractTyConRhs :: AlgTyConRhs
-mkAbstractTyConRhs = AbstractTyCon
+distinctAbstractTyConRhs, totallyAbstractTyConRhs :: AlgTyConRhs
+distinctAbstractTyConRhs = AbstractTyCon True
+totallyAbstractTyConRhs  = AbstractTyCon False
 
 mkDataTyConRhs :: [DataCon] -> AlgTyConRhs
 mkDataTyConRhs cons
index b5da626..eb09c2f 100644 (file)
@@ -103,16 +103,16 @@ data IfaceClassOp = IfaceClassOp OccName DefMethSpec IfaceType
         -- Just True  => generic default method
 
 data IfaceConDecls
-  = IfAbstractTyCon             -- No info
+  = IfAbstractTyCon Bool        -- c.f TyCon.AbstractTyCon
   | IfOpenDataTyCon             -- Open data family
   | IfDataTyCon [IfaceConDecl]  -- data type decls
   | IfNewTyCon  IfaceConDecl    -- newtype decls
 
 visibleIfConDecls :: IfaceConDecls -> [IfaceConDecl]
-visibleIfConDecls IfAbstractTyCon  = []
-visibleIfConDecls IfOpenDataTyCon  = []
-visibleIfConDecls (IfDataTyCon cs) = cs
-visibleIfConDecls (IfNewTyCon c)   = [c]
+visibleIfConDecls (IfAbstractTyCon {}) = []
+visibleIfConDecls IfOpenDataTyCon      = []
+visibleIfConDecls (IfDataTyCon cs)     = cs
+visibleIfConDecls (IfNewTyCon c)       = [c]
 
 data IfaceConDecl
   = IfCon {
@@ -338,7 +338,7 @@ ifaceDeclSubBndrs :: IfaceDecl -> [OccName]
 -- TyThing.getOccName should define a bijection between the two lists.
 -- This invariant is used in LoadIface.loadDecl (see note [Tricky iface loop])
 -- The order of the list does not matter.
-ifaceDeclSubBndrs IfaceData {ifCons = IfAbstractTyCon}  = []
+ifaceDeclSubBndrs IfaceData {ifCons = IfAbstractTyCon {}}  = []
 
 -- Newtype
 ifaceDeclSubBndrs (IfaceData {ifName = tc_occ,
@@ -443,10 +443,10 @@ pprIfaceDecl (IfaceData {ifName = tycon, ifCtxt = context,
                 pprFamily mbFamInst])
   where
     pp_nd = case condecls of
-                IfAbstractTyCon -> ptext (sLit "data")
-                IfOpenDataTyCon -> ptext (sLit "data family")
-                IfDataTyCon _   -> ptext (sLit "data")
-                IfNewTyCon _    -> ptext (sLit "newtype")
+                IfAbstractTyCon dis -> ptext (sLit "abstract") <> parens (ppr dis)
+                IfOpenDataTyCon     -> ptext (sLit "data family")
+                IfDataTyCon _       -> ptext (sLit "data")
+                IfNewTyCon _        -> ptext (sLit "newtype")
 
 pprIfaceDecl (IfaceClass {ifCtxt = context, ifName = clas, ifTyVars = tyvars,
                           ifFDs = fds, ifATs = ats, ifSigs = sigs,
@@ -472,9 +472,9 @@ pprIfaceDeclHead context thing tyvars
           pprIfaceTvBndrs tyvars]
 
 pp_condecls :: OccName -> IfaceConDecls -> SDoc
-pp_condecls _  IfAbstractTyCon  = ptext (sLit "{- abstract -}")
+pp_condecls _  (IfAbstractTyCon {}) = empty
+pp_condecls _  IfOpenDataTyCon      = empty
 pp_condecls tc (IfNewTyCon c)   = equals <+> pprIfaceConDecl tc c
-pp_condecls _  IfOpenDataTyCon  = empty
 pp_condecls tc (IfDataTyCon cs) = equals <+> sep (punctuate (ptext (sLit " |"))
                                                             (map (pprIfaceConDecl tc) cs))
 
index d17fe6a..b73e00a 100644 (file)
@@ -1391,7 +1391,7 @@ tyThingToIfaceDecl (ATyCon tycon)
     ifaceConDecls (DataTyCon { data_cons = cons })  = 
       IfDataTyCon (map ifaceConDecl cons)
     ifaceConDecls DataFamilyTyCon {}                = IfOpenDataTyCon
-    ifaceConDecls AbstractTyCon                            = IfAbstractTyCon
+    ifaceConDecls (AbstractTyCon distinct)         = IfAbstractTyCon distinct
        -- The last case happens when a TyCon has been trimmed during tidying
        -- Furthermore, tyThingToIfaceDecl is also used
        -- in TcRnDriver for GHCi, when browsing a module, in which case the
index dde969f..d0ce1b7 100644 (file)
@@ -511,7 +511,7 @@ tcFamInst (Just (fam, tys)) = do { famTyCon <- tcIfaceTyCon fam
 tcIfaceDataCons :: Name -> TyCon -> [TyVar] -> IfaceConDecls -> IfL AlgTyConRhs
 tcIfaceDataCons tycon_name tycon _ if_cons
   = case if_cons of
-       IfAbstractTyCon  -> return mkAbstractTyConRhs
+       IfAbstractTyCon dis -> return (AbstractTyCon dis)
        IfOpenDataTyCon  -> return DataFamilyTyCon
        IfDataTyCon cons -> do  { data_cons <- mapM tc_con_decl cons
                                ; return (mkDataTyConRhs data_cons) }
index 7bc5d8c..4a6c524 100644 (file)
@@ -1591,7 +1591,7 @@ genGenericRepExtras tc =
                         | (u,n) <- zip us [0..] ] | (us,m) <- zip uniqsS [0..] ]
         
         mkTyCon name = ASSERT( isExternalName name )
-                         buildAlgTyCon name [] [] mkAbstractTyConRhs
+                       buildAlgTyCon name [] [] distinctAbstractTyConRhs
                            NonRecursive False NoParentTyCon Nothing
 
       metaDTyCon  <- mkTyCon d_name
index 3978fc3..f5d99b4 100644 (file)
@@ -771,7 +771,9 @@ checkBootTyCon tc1 tc2
   where 
         env0 = mkRnEnv2 emptyInScopeSet
 
-        eqAlgRhs AbstractTyCon _ = True
+        eqAlgRhs (AbstractTyCon dis1) rhs2 
+          | dis1      = isDistinctAlgRhs rhs2  --Check compatibility
+          | otherwise = True
         eqAlgRhs DataFamilyTyCon{} DataFamilyTyCon{} = True
         eqAlgRhs tc1@DataTyCon{} tc2@DataTyCon{} =
             eqListBy eqCon (data_cons tc1) (data_cons tc2)
index eb950f1..93d0f5d 100644 (file)
@@ -491,8 +491,8 @@ tcTyClDecl1 _parent calc_isrec
        { let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
        ; data_cons <- tcConDecls ex_ok tycon (final_tvs, res_ty) cons
        ; tc_rhs <-
-           if null cons && is_boot     -- In a hs-boot file, empty cons means
-           then return AbstractTyCon   -- "don't know"; hence Abstract
+           if null cons && is_boot           -- In a hs-boot file, empty cons means
+           then return totallyAbstractTyConRhs  -- "don't know"; hence totally Abstract
            else case new_or_data of
                   DataType -> return (mkDataTyConRhs data_cons)
                   NewType  -> ASSERT( not (null data_cons) )
index 3cfe5fb..e7e068c 100644 (file)
@@ -45,7 +45,7 @@ module TyCon(
         isNewTyCon, isAbstractTyCon,
         isFamilyTyCon, isSynFamilyTyCon, isDataFamilyTyCon,
         isUnLiftedTyCon,
-       isGadtSyntaxTyCon,
+       isGadtSyntaxTyCon, isDistinctTyCon, isDistinctAlgRhs,
        isTyConAssoc, tyConAssoc_maybe,
        isRecursiveTyCon,
        isHiBootTyCon,
@@ -330,7 +330,7 @@ data TyCon
   | AlgTyCon {         
        tyConUnique :: Unique,
        tyConName   :: Name,
-       tc_kind   :: Kind,
+       tc_kind     :: Kind,
        tyConArity  :: Arity,
 
        tyConTyVars :: [TyVar],   -- ^ The type variables used in the type constructor.
@@ -455,6 +455,10 @@ data AlgTyConRhs
     -- it's represented by a pointer.  Used when we export a data type
     -- abstractly into an .hi file.
   = AbstractTyCon
+      Bool     -- True  <=> It's definitely a distinct data type, 
+               --           equal only to itself; ie not a newtype
+               -- False <=> Not sure
+               -- See Note [AbstractTyCon and type equality]
 
     -- | Represents an open type family without a fixed right hand
     -- side.  Additional instances can appear at any time.
@@ -512,13 +516,20 @@ data AlgTyConRhs
                              -- Watch out!  If any newtypes become transparent
                              -- again check Trac #1072.
     }
+\end{code}
+
+Note [AbstractTyCon and type equality]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+TODO
+
+\begin{code}
 
 -- | Extract those 'DataCon's that we are able to learn about.  Note
 -- that visibility in this sense does not correspond to visibility in
 -- the context of any particular user program!
 visibleDataCons :: AlgTyConRhs -> [DataCon]
-visibleDataCons AbstractTyCon                = []
-visibleDataCons DataFamilyTyCon {}                   = []
+visibleDataCons (AbstractTyCon {})           = []
+visibleDataCons DataFamilyTyCon {}           = []
 visibleDataCons (DataTyCon{ data_cons = cs }) = cs
 visibleDataCons (NewTyCon{ data_con = c })    = [c]
 
@@ -919,12 +930,13 @@ 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
 
 -- | Make an algebraic 'TyCon' abstract. Panics if the supplied 'TyCon' is not algebraic
 makeTyConAbstract :: TyCon -> TyCon
-makeTyConAbstract tc@(AlgTyCon {}) = tc { algTcRhs = AbstractTyCon }
+makeTyConAbstract tc@(AlgTyCon { algTcRhs = rhs }) 
+  = tc { algTcRhs = AbstractTyCon (isDistinctAlgRhs rhs) }
 makeTyConAbstract tc = pprPanic "makeTyConAbstract" (ppr tc)
 
 -- | Does this 'TyCon' represent something that cannot be defined in Haskell?
@@ -953,19 +965,40 @@ isDataTyCon :: TyCon -> Bool
 -- 
 -- Generally, the function will be true for all @data@ types and false
 -- for @newtype@s, unboxed tuples and type family 'TyCon's. But it is
--- not guarenteed to return @True@ in all cases that it could.
+-- not guaranteed to return @True@ in all cases that it could.
 -- 
 -- NB: for a data type family, only the /instance/ 'TyCon's
 --     get an info table.  The family declaration 'TyCon' does not
 isDataTyCon (AlgTyCon {algTcRhs = rhs})
   = case rhs of
         DataFamilyTyCon {}  -> False
-       DataTyCon {}  -> True
-       NewTyCon {}   -> False
-       AbstractTyCon -> False   -- We don't know, so return False
+       DataTyCon {}     -> True
+       NewTyCon {}      -> False
+       AbstractTyCon {} -> False        -- We don't know, so return False
 isDataTyCon (TupleTyCon {tyConBoxed = boxity}) = isBoxed boxity
 isDataTyCon _ = False
 
+-- | 'isDistinctTyCon' is true of 'TyCon's that are equal only to 
+-- themselves, even via coercions (except for unsafeCoerce).
+-- This excludes newtypes, type functions, type synonyms.
+-- It relates directly to the FC consistency story: 
+--     If the axioms are consistent, 
+--     and  co : S tys ~ T tys, and S,T are "distinct" TyCons,
+--     then S=T.
+-- Cf Note [Pruning dead case alternatives] in Unify
+isDistinctTyCon :: TyCon -> Bool
+isDistinctTyCon (AlgTyCon {algTcRhs = rhs}) = isDistinctAlgRhs rhs
+isDistinctTyCon (FunTyCon {})               = True
+isDistinctTyCon (TupleTyCon {})             = True
+isDistinctTyCon (PrimTyCon {})              = True
+isDistinctTyCon _                           = False
+
+isDistinctAlgRhs :: AlgTyConRhs -> Bool
+isDistinctAlgRhs (DataTyCon {})          = True
+isDistinctAlgRhs (DataFamilyTyCon {})     = True
+isDistinctAlgRhs (AbstractTyCon distinct) = distinct
+isDistinctAlgRhs (NewTyCon {})            = False
+
 -- | Is this 'TyCon' that for a @newtype@
 isNewTyCon :: TyCon -> Bool
 isNewTyCon (AlgTyCon {algTcRhs = NewTyCon {}}) = True
@@ -1108,8 +1141,8 @@ isRecursiveTyCon _                                 = False
 -- | Did this 'TyCon' originate from type-checking a .h*-boot file?
 isHiBootTyCon :: TyCon -> Bool
 -- Used for knot-tying in hi-boot files
-isHiBootTyCon (AlgTyCon {algTcRhs = AbstractTyCon}) = True
-isHiBootTyCon _                                     = False
+isHiBootTyCon (AlgTyCon {algTcRhs = AbstractTyCon False}) = True
+isHiBootTyCon _                                           = False
 
 -- | Is this the 'TyCon' of a foreign-imported type constructor?
 isForeignTyCon :: TyCon -> Bool
index 9c448ce..559682e 100644 (file)
@@ -268,7 +268,7 @@ The question before the house is this: if I know something about the type
 of x, can I prune away the T1 alternative?
 
 Suppose x::T Char.  It's impossible to construct a (T Char) using T1, 
-       Answer = YES (clearly)
+       Answer = YES we can prune the T1 branch (clearly)
 
 Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
 to 'Bool', in which case x::T Int, so
@@ -280,7 +280,7 @@ gives a coercion
        CoX :: X ~ Int
 So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
 of type (T X) constructed with T1.  Hence
-       ANSWER = NO (surprisingly)
+       ANSWER = NO we can't prune the T1 branch (surprisingly)
 
 Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
 mechanism uses a cast, just as above, to move from one dictionary to another,
@@ -328,11 +328,11 @@ typesCantMatch prs = any (\(s,t) -> cant_match s t) prs
        = cant_match a1 a2 || cant_match r1 r2
 
     cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
-       | isDataTyCon tc1 && isDataTyCon tc2
+       | isDistinctTyCon tc1 && isDistinctTyCon tc2
        = tc1 /= tc2 || typesCantMatch (zipEqual "typesCantMatch" tys1 tys2)
 
-    cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
-    cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
+    cant_match (FunTy {}) (TyConApp tc _) = isDistinctTyCon tc
+    cant_match (TyConApp tc _) (FunTy {}) = isDistinctTyCon tc
        -- tc can't be FunTyCon by invariant
 
     cant_match (AppTy f1 a1) ty2