Improve handling of newtypes (fixes Trac 1495)
authorsimonpj@microsoft.com <unknown>
Fri, 21 Dec 2007 09:04:06 +0000 (09:04 +0000)
committersimonpj@microsoft.com <unknown>
Fri, 21 Dec 2007 09:04:06 +0000 (09:04 +0000)
In a few places we want to "look through" newtypes to get to the
representation type.  But we need to be careful that  we don't fall
into an ininite loop with e.g.
newtype T = MkT T

The old mechansim for doing this was to have a field nt_rep, inside
a newtype TyCon, that gave the "ultimate representation" of the type.
But that failed for Trac 1495, which looked like this:
   newtype Fix a = Fix (a (Fix a))
   data I a = I a
Then, expanding the type (Fix I) went on for ever.

The right thing to do seems to be to check for loops when epxanding
the *type*, rather than in the *tycon*.  This patch does that,
- Removes nt_rep from TyCon
- Make Type.repType check for loops
See Note [Expanding newtypes] in Type.lhs.

At the same time I also fixed a bug for Roman, where newtypes were not
being expanded properly in FamInstEnv.topNormaliseType.  This function
and Type.repType share a common structure.

Ian, see if this merges easily to the branch
If not, I don't think it's essential to fix 6.8

compiler/coreSyn/MkExternalCore.lhs
compiler/iface/BuildTyCl.lhs
compiler/main/TidyPgm.lhs
compiler/typecheck/TcDeriv.lhs
compiler/types/FamInstEnv.lhs
compiler/types/TyCon.lhs
compiler/types/Type.lhs

index a0bccda..e5f81d0 100644 (file)
@@ -69,13 +69,11 @@ collect_tdefs tcon tdefs
   where
     tdef | isNewTyCon tcon = 
                 C.Newtype (make_con_qid (tyConName tcon)) (map make_tbind tyvars) repclause 
--- 20060420 GHC handles empty data types just fine. ExtCore should too! jds
---         | null (tyConDataCons tcon) = error "MkExternalCore died: can't handle datatype declarations with no data constructors"
          | otherwise = 
                 C.Data (make_con_qid (tyConName tcon)) (map make_tbind tyvars) (map make_cdef (tyConDataCons tcon)) 
          where repclause | isRecursiveTyCon tcon || isOpenTyCon tcon= Nothing
-                        | otherwise = Just (make_ty rep)
-                                           where (_, rep) = newTyConRep tcon
+                        | otherwise = Just (make_ty (repType rhs))
+                                           where (_, rhs) = newTyConRhs tcon
     tyvars = tyConTyVars tcon
 
 collect_tdefs _ tdefs = tdefs
index 80428a7..534bc5f 100644 (file)
@@ -146,10 +146,9 @@ mkNewTyConRhs tycon_name tycon con
        ; return (NewTyCon { data_con    = con, 
                             nt_rhs      = rhs_ty,
                             nt_etad_rhs = (etad_tvs, etad_rhs),
-                            nt_co       = cocon_maybe, 
+                            nt_co       = cocon_maybe } ) }
                              -- Coreview looks through newtypes with a Nothing
                              -- for nt_co, or uses explicit coercions otherwise
-                            nt_rep = mkNewTyConRep tycon rhs_ty }) }
   where
         -- If all_coercions is True then we use coercions for all newtypes
         -- otherwise we use coercions for recursive newtypes and look through
@@ -180,42 +179,6 @@ mkNewTyConRhs tycon_name tycon con
     eta_reduce tvs ty = (reverse tvs, ty)
                                
 
-mkNewTyConRep :: TyCon         -- The original type constructor
-             -> Type           -- The arg type of its constructor
-             -> Type           -- Chosen representation type
--- The "representation type" is guaranteed not to be another newtype
--- at the outermost level; but it might have newtypes in type arguments
-
--- Find the representation type for this newtype TyCon
--- Remember that the representation type is the *ultimate* representation
--- type, looking through other newtypes.
--- 
--- splitTyConApp_maybe no longer looks through newtypes, so we must
--- deal explicitly with this case
--- 
--- The trick is to to deal correctly with recursive newtypes
--- such as     newtype T = MkT T
-
-mkNewTyConRep tc rhs_ty
-  | null (tyConDataCons tc) = unitTy
-       -- External Core programs can have newtypes with no data constructors
-  | otherwise              = go [tc] rhs_ty
-  where
-       -- Invariant: tcs have been seen before
-    go tcs rep_ty 
-       = case splitTyConApp_maybe rep_ty of
-           Just (tc, tys)
-               | tc `elem` tcs -> unitTy       -- Recursive loop
-               | isNewTyCon tc -> 
-                    if isRecursiveTyCon tc then
-                       go (tc:tcs) (substTyWith tvs tys rhs_ty)
-                    else
-                        substTyWith tvs tys rhs_ty
-               where
-                 (tvs, rhs_ty) = newTyConRhs tc
-
-           other -> rep_ty 
-
 ------------------------------------------------------
 buildDataCon :: Name -> Bool
            -> [StrictnessMark] 
index 131b617..fc951cc 100644 (file)
@@ -403,13 +403,14 @@ mustExposeTyCon exports tc
   | isEnumerationTyCon tc      -- For an enumeration, exposing the constructors
   = True                       -- won't lead to the need for further exposure
                                -- (This includes data types with no constructors.)
-  | isOpenTyCon tc             -- open type family
+  | isOpenTyCon tc             -- Open type family
   = True
+
   | otherwise                  -- Newtype, datatype
   = any exported_con (tyConDataCons tc)
        -- Expose rep if any datacon or field is exported
 
-  || (isNewTyCon tc && isFFITy (snd (newTyConRep tc)))
+  || (isNewTyCon tc && isFFITy (snd (newTyConRhs tc)))
        -- Expose the rep for newtypes if the rep is an FFI type.  
        -- For a very annoying reason.  'Foreign import' is meant to
        -- be able to look through newtypes transparently, but it
index e79318b..f3224c8 100644 (file)
@@ -798,10 +798,10 @@ mkNewTypeEqn orig mayDeriveDataTypeable newtype_deriving tvs
                -- Want to drop 1 arg from (T s a) and (ST s a)
                -- to get       instance Monad (ST s) => Monad (T s)
 
-       -- Note [newtype representation]
-       -- Need newTyConRhs *not* newTyConRep to get the representation 
-       -- type, because the latter looks through all intermediate newtypes
-       -- For example
+       -- Note [Newtype representation]
+       -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+       -- Need newTyConRhs (*not* a recursive representation finder) 
+       -- to get the representation type. For example
        --      newtype B = MkB Int
        --      newtype A = MkA B deriving( Num )
        -- We want the Num instance of B, *not* the Num instance of Int,
index 4f83aba..a9e1548 100644 (file)
@@ -342,42 +342,63 @@ bind_fn tv | isTcTyVar tv && isExistentialTyVar tv = Skolem
 
 \begin{code}
 topNormaliseType :: FamInstEnvs
-                     -> Type
-                     -> Maybe (Coercion, Type)
+                -> Type
+                -> Maybe (Coercion, Type)
 
--- Get rid of *outermost* (or toplevel) type functions by rewriting them
+-- Get rid of *outermost* (or toplevel) 
+--     * type functions 
+--     * newtypes
+-- using appropriate coercions.
 -- By "outer" we mean that toplevelNormaliseType guarantees to return
 -- a type that does not have a reducible redex (F ty1 .. tyn) as its
 -- outermost form.  It *can* return something like (Maybe (F ty)), where
 -- (F ty) is a redex.
 
-topNormaliseType env ty
-  | Just ty' <- tcView ty = topNormaliseType env ty'
-
-topNormaliseType env ty@(TyConApp tc tys)
-  | isOpenTyCon tc
-  , (ACo co, ty) <- normaliseType env ty
-  = Just (co, ty)
+-- Its a bit like Type.repType, but handles type families too
 
 topNormaliseType env ty
-  = Nothing
+  = go [] ty
+  where
+    go :: [TyCon] -> Type -> Maybe (Coercion, Type)
+    go rec_nts ty | Just ty' <- coreView ty    -- Expand synonyms
+       = go rec_nts ty'        
+
+    go rec_nts (TyConApp tc tys)               -- Expand newtypes
+       | Just co_con <- newTyConCo_maybe tc    -- See Note [Expanding newtypes]
+       = if tc `elem` rec_nts                  --  in Type.lhs
+         then Nothing
+         else let nt_co = mkTyConApp co_con tys
+              in add_co nt_co rec_nts' nt_rhs
+       where
+         nt_rhs = newTyConInstRhs tc tys
+         rec_nts' | isRecursiveTyCon tc = tc:rec_nts
+                  | otherwise           = rec_nts
+
+    go rec_nts (TyConApp tc tys)               -- Expand open tycons
+       | isOpenTyCon tc
+       , (ACo co, ty) <- normaliseTcApp env tc tys
+       =       -- The ACo says "something happened"
+               -- Note that normaliseType fully normalises, but it has do to so
+               -- to be sure that 
+          add_co co rec_nts ty
+
+    go rec_nts ty = Nothing
+
+    add_co co rec_nts ty 
+       = case go rec_nts ty of
+               Nothing         -> Just (co, ty)
+               Just (co', ty') -> Just (mkTransCoercion co co', ty')
         
 
-normaliseType :: FamInstEnvs           -- environment with family instances
-             -> Type                   -- old type
-             -> (CoercionI,Type)       -- (coercion,new type), where
-                                       -- co :: old-type ~ new_type
--- Normalise the input type, by eliminating all type-function redexes
-
-normaliseType env ty 
-  | Just ty' <- coreView ty = normaliseType env ty' 
-
-normaliseType env ty@(TyConApp tyCon tys)
-  = let        -- First normalise the arg types
+---------------
+normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
+normaliseTcApp env tc tys
+  = let        -- First normalise the arg types so that they'll match 
+       -- when we lookup in in the instance envt
        (cois, ntys) = mapAndUnzip (normaliseType env) tys
-       tycon_coi    = mkTyConAppCoI tyCon ntys cois
+       tycon_coi    = mkTyConAppCoI tc ntys cois
     in         -- Now try the top-level redex
-    case lookupFamInstEnv env tyCon ntys of
+    case lookupFamInstEnv env tc ntys of
                -- A matching family instance exists
        [(fam_inst, tys)] -> (fix_coi, nty)
            where
@@ -390,29 +411,39 @@ normaliseType env ty@(TyConApp tyCon tys)
 
                -- No unique matching family instance exists;
                -- we do not do anything
-       other -> (tycon_coi, TyConApp tyCon ntys)
-
-  where
+       other -> (tycon_coi, TyConApp tc ntys)
+---------------
+normaliseType :: FamInstEnvs           -- environment with family instances
+             -> Type                   -- old type
+             -> (CoercionI, Type)      -- (coercion,new type), where
+                                       -- co :: old-type ~ new_type
+-- Normalise the input type, by eliminating *all* type-function redexes
+-- Returns with IdCo if nothing happens
 
+normaliseType env ty 
+  | Just ty' <- coreView ty = normaliseType env ty' 
+normaliseType env ty@(TyConApp tc tys)
+  = normaliseTcApp env tc tys
 normaliseType env ty@(AppTy ty1 ty2)
-  =    let (coi1,nty1) = normaliseType env ty1
-           (coi2,nty2) = normaliseType env ty2
-       in  (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
+  = let (coi1,nty1) = normaliseType env ty1
+        (coi2,nty2) = normaliseType env ty2
+    in  (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
 normaliseType env ty@(FunTy ty1 ty2)
-  =    let (coi1,nty1) = normaliseType env ty1
-           (coi2,nty2) = normaliseType env ty2
-       in  (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
+  = let (coi1,nty1) = normaliseType env ty1
+        (coi2,nty2) = normaliseType env ty2
+    in  (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
 normaliseType env ty@(ForAllTy tyvar ty1)
-  =    let (coi,nty1) = normaliseType env ty1
-       in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+  = let (coi,nty1) = normaliseType env ty1
+    in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
 normaliseType env ty@(NoteTy note ty1)
-  =    let (coi,nty1) = normaliseType env ty1
-       in  (mkNoteTyCoI note coi,NoteTy note nty1)
+  = let (coi,nty1) = normaliseType env ty1
+    in  (mkNoteTyCoI note coi,NoteTy note nty1)
 normaliseType env ty@(TyVarTy _)
-  =    (IdCo,ty)
+  = (IdCo,ty)
 normaliseType env (PredTy predty)
-  =    normalisePred env predty        
+  = normalisePred env predty   
 
+---------------
 normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
 normalisePred env (ClassP cls tys)
   =    let (cois,tys') = mapAndUnzip (normaliseType env) tys
index 7d11482..c495ebb 100644 (file)
@@ -33,7 +33,7 @@ module TyCon(
        isEnumerationTyCon, isGadtSyntaxTyCon, isOpenTyCon,
        assocTyConArgPoss_maybe, isTyConAssoc, setTyConArgPoss,
        isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon, tupleTyConBoxity,
-       isRecursiveTyCon, newTyConRep, newTyConRhs, newTyConEtadRhs, newTyConCo_maybe,
+       isRecursiveTyCon, newTyConRhs, newTyConEtadRhs, newTyConCo_maybe,
        isHiBootTyCon, isSuperKindTyCon,
         isCoercionTyCon_maybe, isCoercionTyCon,
         isImplicitTyCon,
@@ -259,26 +259,11 @@ data AlgTyConRhs
                                -- Watch out!  If any newtypes become transparent
                                -- again check Trac #1072.
 
-       nt_etad_rhs :: ([TyVar], Type) ,
+       nt_etad_rhs :: ([TyVar], Type)
                        -- The same again, but this time eta-reduced
                        -- hence the [TyVar] which may be shorter than the declared 
                        -- arity of the TyCon.  See Note [Newtype eta]
-
-       nt_rep :: Type  -- Cached: the *ultimate* representation type
-                       -- By 'ultimate' I mean that the top-level constructor
-                       -- of the rep type is not itself a newtype or type synonym.
-                       -- The rep type isn't entirely simple:
-                       --  for a recursive newtype we pick () as the rep type
-                       --      newtype T = MkT T
-                       -- 
-                       -- This one does not need to be eta reduced; hence its
-                       -- free type variables are conveniently tyConTyVars
-                       -- Thus:
-                       --      newtype T a = MkT [(a,Int)]
-                       -- The rep type is [(a,Int)]
-                       -- NB: the rep type isn't necessarily the original RHS of the
-                       --     newtype decl, because the rep type looks through other
-    }                  --     newtypes.
+    }
 
 visibleDataCons :: AlgTyConRhs -> [DataCon]
 visibleDataCons AbstractTyCon                = []
@@ -871,9 +856,7 @@ tyConFamilySize (AlgTyCon   {algTcRhs = DataTyCon {data_cons = cons}}) =
 tyConFamilySize (AlgTyCon   {algTcRhs = NewTyCon {}})                  = 1
 tyConFamilySize (AlgTyCon   {algTcRhs = OpenTyCon {}})                 = 0
 tyConFamilySize (TupleTyCon {})                                               = 1
-#ifdef DEBUG
 tyConFamilySize other = pprPanic "tyConFamilySize:" (ppr other)
-#endif
 
 tyConSelIds :: TyCon -> [Id]
 tyConSelIds (AlgTyCon {algTcSelIds = fs}) = fs
@@ -894,10 +877,6 @@ newTyConEtadRhs :: TyCon -> ([TyVar], Type)
 newTyConEtadRhs (AlgTyCon {algTcRhs = NewTyCon { nt_etad_rhs = tvs_rhs }}) = tvs_rhs
 newTyConEtadRhs tycon = pprPanic "newTyConEtadRhs" (ppr tycon)
 
-newTyConRep :: TyCon -> ([TyVar], Type)
-newTyConRep (AlgTyCon {tyConTyVars = tvs, algTcRhs = NewTyCon { nt_rep = rep }}) = (tvs, rep)
-newTyConRep tycon = pprPanic "newTyConRep" (ppr tycon)
-
 newTyConCo_maybe :: TyCon -> Maybe TyCon
 newTyConCo_maybe (AlgTyCon {algTcRhs = NewTyCon { nt_co = co }}) = co
 newTyConCo_maybe _                                              = Nothing
index 662dd6f..c36893b 100644 (file)
@@ -468,6 +468,31 @@ The reason is that we then get better (shorter) type signatures in
 interfaces.  Notably this plays a role in tcTySigs in TcBinds.lhs.
 
 
+Note [Expanding newtypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+When expanding a type to expose a data-type constructor, we need to be
+careful about newtypes, lest we fall into an infinite loop. Here are
+the key examples:
+
+  newtype Id  x = MkId x
+  newtype Fix f = MkFix (f (Fix f))
+  newtype T     = MkT (T -> T) 
+  
+  Type          Expansion
+ --------------------------
+  T             T -> T
+  Fix Maybe      Maybe (Fix Maybe)
+  Id (Id Int)    Int
+  Fix Id         NO NO NO
+
+Notice that we can expand T, even though it's recursive.
+And we can expand Id (Id Int), even though the Id shows up
+twice at the outer level.  
+
+So, when expanding, we keep track of when we've seen a recursive
+newtype at outermost level; and bale out if we see it again.
+
+
                Representation types
                ~~~~~~~~~~~~~~~~~~~~
 repType looks through 
@@ -481,19 +506,28 @@ It's useful in the back end.
 \begin{code}
 repType :: Type -> Type
 -- Only applied to types of kind *; hence tycons are saturated
-repType ty | Just ty' <- coreView ty = repType ty'
-repType (ForAllTy _ ty)  = repType ty
-repType (TyConApp tc tys)
-  | isNewTyCon tc
-  , (tvs, rep_ty) <- newTyConRep tc
-  = -- Recursive newtypes are opaque to coreView
-    -- but we must expand them here.  Sure to
-    -- be saturated because repType is only applied
-    -- to types of kind *
-    ASSERT( tys `lengthIs` tyConArity tc )
-    repType (substTyWith tvs tys rep_ty)
-
-repType ty = ty
+repType ty
+  = go [] ty
+  where
+    go :: [TyCon] -> Type -> Type
+    go rec_nts ty | Just ty' <- coreView ty    -- Expand synonyms
+       = go rec_nts ty'        
+
+    go rec_nts (ForAllTy _ ty)                 -- Look through foralls
+       = go rec_nts ty
+
+    go rec_nts ty@(TyConApp tc tys)            -- Expand newtypes
+       | Just co_con <- newTyConCo_maybe tc    -- See Note [Expanding newtypes]
+       = if tc `elem` rec_nts                  --  in Type.lhs
+         then ty
+         else go rec_nts' nt_rhs
+       where
+         nt_rhs = newTyConInstRhs tc tys
+         rec_nts' | isRecursiveTyCon tc = tc:rec_nts
+                  | otherwise           = rec_nts
+
+    go rec_nts ty = ty
+
 
 -- ToDo: this could be moved to the code generator, using splitTyConApp instead
 -- of inspecting the type directly.