Introduce coercions for data instance decls
authorManuel M T Chakravarty <chak@cse.unsw.edu.au>
Wed, 20 Sep 2006 18:36:46 +0000 (18:36 +0000)
committerManuel M T Chakravarty <chak@cse.unsw.edu.au>
Wed, 20 Sep 2006 18:36:46 +0000 (18:36 +0000)
Mon Sep 18 19:07:30 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
  * Introduce coercions for data instance decls
  Tue Aug 22 20:33:46 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
    * Introduce coercions for data instance decls
    - data instance declarations implicitly generate a coercion moving between the
      representation type and family instance type.
    - The coercion is *implicitly* generated when type checking both source and
      ifaces.  Ie, we don't safe it in ifaces - this is really exactly as newtype
      coercions are handled.
    - The previous addition of the instance types to DataCons has been moved to
      the representation TyCon.  This is more efficient as it is shared between all
      constructors of one representation tycon and it also gathers everything about
      data instances (family tycon, instance types, and coercion) in one place: the
      algTcParent field of TyCon.
    - The coercion is already used in the datacon wrappers, but not yet during type
      checking pattern matching of indexed data types.
    - The code has only been lightly tested, but doesn't seem to break features not
      related to indexed types.  For indexed data types only the pattern matching
      tc code (in TcPat.tcConPat) and some well-formedness checks are still
      missing.  And there will surely be some bugs to fix.  (newtypes still require
      some more work.)

        ** WARNING: Interface file format changed! **
        **          Recompile from scratch!        **

12 files changed:
compiler/basicTypes/DataCon.lhs
compiler/basicTypes/MkId.lhs
compiler/basicTypes/OccName.lhs
compiler/iface/BinIface.hs
compiler/iface/BuildTyCl.lhs
compiler/iface/IfaceSyn.lhs
compiler/iface/MkIface.lhs
compiler/iface/TcIface.lhs
compiler/prelude/TysWiredIn.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/types/Coercion.lhs
compiler/types/TyCon.lhs

index a04f28f..aa87958 100644 (file)
@@ -11,7 +11,6 @@ module DataCon (
        dataConRepType, dataConSig, dataConFullSig,
        dataConName, dataConTag, dataConTyCon, dataConUserType,
        dataConUnivTyVars, dataConExTyVars, dataConAllTyVars, dataConResTys,
-       dataConInstTys,
        dataConEqSpec, eqSpecPreds, dataConTheta, dataConStupidTheta, 
        dataConInstArgTys, dataConOrigArgTys, 
        dataConInstOrigArgTys, dataConRepArgTys, 
@@ -39,7 +38,7 @@ import Type           ( Type, ThetaType,
 import Coercion                ( isEqPred, mkEqPred )
 import TyCon           ( TyCon, FieldLabel, tyConDataCons, 
                          isProductTyCon, isTupleTyCon, isUnboxedTupleTyCon,
-                          isNewTyCon, isRecursiveTyCon, tyConFamily_maybe )
+                          isNewTyCon, isRecursiveTyCon, tyConFamInst_maybe )
 import Class           ( Class, classTyCon )
 import Name            ( Name, NamedThing(..), nameUnique, mkSysTvName, mkSystemName )
 import Var             ( TyVar, CoVar, Id, mkTyVar, tyVarKind, setVarUnique,
@@ -336,13 +335,9 @@ data DataCon
        -- An entirely separate wrapper function is built in TcTyDecls
        dcIds :: DataConIds,
 
-       dcInfix :: Bool,        -- True <=> declared infix
+       dcInfix :: Bool         -- True <=> declared infix
                                -- Used for Template Haskell and 'deriving' only
                                -- The actual fixity is stored elsewhere
-
-        dcInstTys :: Maybe [Type]  -- If this data constructor is part of a
-                                  -- data instance, then these are the type
-                                  -- patterns of the instance.
   }
 
 data DataConIds
@@ -438,7 +433,6 @@ mkDataCon :: Name
          -> [TyVar] -> [TyVar] 
          -> [(TyVar,Type)] -> ThetaType
          -> [Type] -> TyCon
-         -> Maybe [Type]
          -> ThetaType -> DataConIds
          -> DataCon
   -- Can get the tag from the TyCon
@@ -449,7 +443,6 @@ mkDataCon name declared_infix
          univ_tvs ex_tvs 
          eq_spec theta
          orig_arg_tys tycon
-         mb_typats
          stupid_theta ids
   = ASSERT( not (any isEqPred theta) )
        -- We don't currently allow any equality predicates on
@@ -469,8 +462,7 @@ mkDataCon name declared_infix
                  dcStrictMarks = arg_stricts, 
                  dcRepStrictness = rep_arg_stricts,
                  dcFields = fields, dcTag = tag, dcRepType = ty,
-                 dcIds = ids,
-                 dcInstTys = mb_typats }
+                 dcIds = ids }
 
        -- Strictness marks for source-args
        --      *after unboxing choices*, 
@@ -609,9 +601,6 @@ dataConResTys dc = [substTyVar env tv | tv <- dcUnivTyVars dc]
   where
     env = mkTopTvSubst (dcEqSpec dc)
 
-dataConInstTys :: DataCon -> Maybe [Type]
-dataConInstTys = dcInstTys
-
 dataConUserType :: DataCon -> Type
 -- The user-declared type of the data constructor
 -- in the nice-to-read form 
@@ -623,18 +612,13 @@ dataConUserType :: DataCon -> Type
 dataConUserType  (MkData { dcUnivTyVars = univ_tvs, 
                           dcExTyVars = ex_tvs, dcEqSpec = eq_spec,
                           dcTheta = theta, dcOrigArgTys = arg_tys,
-                          dcTyCon = tycon, dcInstTys = mb_insttys })
+                          dcTyCon = tycon })
   = mkForAllTys ((univ_tvs `minusList` map fst eq_spec) ++ ex_tvs) $
     mkFunTys (mkPredTys theta) $
     mkFunTys arg_tys $
-    case mb_insttys of
-      Nothing      -> mkTyConApp tycon (map (substTyVar subst) univ_tvs)
-      Just insttys -> mkTyConApp ftycon insttys            -- data instance
-        where
-         ftycon = case tyConFamily_maybe tycon of
-                    Just ftycon -> ftycon
-                    Nothing     -> panic err
-          err    = "dataConUserType: type patterns without family tycon"
+    case tyConFamInst_maybe tycon of
+      Nothing             -> mkTyConApp tycon (map (substTyVar subst) univ_tvs)
+      Just (ftc, insttys) -> mkTyConApp ftc insttys        -- data instance
   where
     subst = mkTopTvSubst eq_spec
 
index 6af89b7..d306128 100644 (file)
@@ -62,7 +62,8 @@ import CoreUnfold     ( mkTopUnfolding, mkCompulsoryUnfolding )
 import Literal         ( nullAddrLit, mkStringLit )
 import TyCon           ( TyCon, isNewTyCon, tyConDataCons, FieldLabel,
                           tyConStupidTheta, isProductTyCon, isDataTyCon,
-                          isRecursiveTyCon, tyConFamily_maybe, newTyConCo )
+                          isRecursiveTyCon, isFamInstTyCon,
+                          tyConFamInst_maybe, newTyConCo ) 
 import Class           ( Class, classTyCon, classSelIds )
 import Var             ( Id, TyVar, Var, setIdType )
 import VarSet          ( isEmptyVarSet, subVarSet, varSetElems )
@@ -71,7 +72,7 @@ import OccName                ( mkOccNameFS, varName )
 import PrimOp          ( PrimOp, primOpSig, primOpOcc, primOpTag )
 import ForeignCall     ( ForeignCall )
 import DataCon         ( DataCon, DataConIds(..), dataConTyCon,
-                         dataConUnivTyVars, dataConInstTys,
+                         dataConUnivTyVars, 
                          dataConFieldLabels, dataConRepArity, dataConResTys,
                          dataConRepArgTys, dataConRepType, dataConFullSig,
                          dataConStrictMarks, dataConExStricts, 
@@ -189,6 +190,9 @@ Notice that
   Making an explicit case expression allows the simplifier to eliminate
   it in the (common) case where the constructor arg is already evaluated.
 
+In the case of data instances, the wrapper also applies the coercion turning
+the representation type into the family instance type to cast the result of
+the wrapper.
 
 \begin{code}
 mkDataConIds :: Name -> Name -> DataCon -> DataConIds
@@ -198,7 +202,7 @@ mkDataConIds wrap_name wkr_name data_con
 
   | any isMarkedStrict all_strict_marks                -- Algebraic, needs wrapper
     || not (null eq_spec)
-    || isInst
+    || isFamInstTyCon tycon
   = DCIds (Just alg_wrap_id) wrk_id
 
   | otherwise                                  -- Algebraic, no wrapper
@@ -207,13 +211,6 @@ mkDataConIds wrap_name wkr_name data_con
     (univ_tvs, ex_tvs, eq_spec, 
      theta, orig_arg_tys)          = dataConFullSig data_con
     tycon                          = dataConTyCon data_con
-    (isInst, instTys, familyTyCon) = 
-      case dataConInstTys data_con of
-        Nothing      -> (False, []     , familyTyCon)
-       Just instTys -> (True , instTys, familyTyCon)
-         where
-           familyTyCon = fromJust $ tyConFamily_maybe tycon
-                         -- this is defined whenever `isInst'
 
        ----------- Wrapper --------------
        -- We used to include the stupid theta in the wrapper's args
@@ -223,10 +220,13 @@ mkDataConIds wrap_name wkr_name data_con
     subst         = mkTopTvSubst eq_spec
     dict_tys       = mkPredTys theta
     result_ty_args = map (substTyVar subst) univ_tvs
-    familyArgs     = map (substTy    subst) instTys
-    result_ty      = if isInst
-                    then mkTyConApp familyTyCon familyArgs  -- instance con
-                    else mkTyConApp tycon result_ty_args    -- ordinary con
+    result_ty      = case tyConFamInst_maybe tycon of
+                        -- ordinary constructor
+                      Nothing            -> mkTyConApp tycon result_ty_args
+                        -- family instance constructor
+                      Just (familyTyCon, 
+                            instTys)     -> 
+                        mkTyConApp familyTyCon (map (substTy subst) instTys)
     wrap_ty        = mkForAllTys wrap_tvs $ mkFunTys dict_tys $
                     mkFunTys orig_arg_tys $ result_ty
        -- NB: watch out here if you allow user-written equality 
@@ -316,10 +316,11 @@ mkDataConIds wrap_name wkr_name data_con
                    (zip (dict_args ++ id_args) all_strict_marks)
                    i3 []
 
-    con_app _ rep_ids = Var wrk_id `mkTyApps`  result_ty_args
-                                  `mkVarApps` ex_tvs
-                                  `mkTyApps`  map snd eq_spec
-                                  `mkVarApps` reverse rep_ids
+    con_app _ rep_ids = wrapFamInstBody tycon result_ty_args $
+                         Var wrk_id `mkTyApps`  result_ty_args
+                                    `mkVarApps` ex_tvs
+                                    `mkTyApps`  map snd eq_spec
+                                    `mkVarApps` reverse rep_ids
 
     (dict_args,i2) = mkLocals 1  dict_tys
     (id_args,i3)   = mkLocals i2 orig_arg_tys
@@ -358,6 +359,19 @@ mAX_CPR_SIZE = 10
 mkLocals i tys = (zipWith mkTemplateLocal [i..i+n-1] tys, i+n)
               where
                 n = length tys
+
+-- If the type constructor is a representation type of a data instance, wrap
+-- the expression into a cast adjusting the expression type, which is an
+-- instance of the representation type, to the corresponding instance of the
+-- family instance type.
+--
+wrapFamInstBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
+wrapFamInstBody tycon args result_expr
+  | Just (co_con, _) <- tyConFamInst_maybe tycon
+  = mkCoerce (mkSymCoercion (mkTyConApp co_con args)) result_expr
+  | otherwise
+  = result_expr
+
 \end{code}
 
 
index 48137c6..13a7f81 100644 (file)
@@ -27,12 +27,13 @@ module OccName (
        setOccNameSpace,
 
        -- ** Derived OccNames
-       mkDataConWrapperOcc, mkWorkerOcc, mkDefaultMethodOcc, mkDerivedTyConOcc,
-        mkNewTyCoOcc,
+       mkDataConWrapperOcc, mkWorkerOcc, mkDefaultMethodOcc,
+       mkDerivedTyConOcc, mkNewTyCoOcc,
        mkClassTyConOcc, mkClassDataConOcc, mkDictOcc, mkIPOcc, 
        mkSpecOcc, mkForeignExportOcc, mkGenOcc1, mkGenOcc2,
        mkDataTOcc, mkDataCOcc, mkDataConWorkerOcc,
-       mkSuperDictSelOcc, mkLocalOcc, mkMethodOcc,
+       mkSuperDictSelOcc, mkLocalOcc, mkMethodOcc, mkInstTyTcOcc,
+       mkInstTyCoOcc, 
 
        -- ** Deconstruction
        occNameFS, occNameString, occNameSpace, 
@@ -477,6 +478,26 @@ mkLocalOcc uniq occ
        -- that need encoding (e.g. 'z'!)
 \end{code}
 
+\begin{code}
+
+-- Derive a name for the representation type constructor of a data/newtype
+-- instance.
+--
+mkInstTyTcOcc :: Unique                -- Unique
+             -> OccName                -- Local name (e.g. "Map")
+             -> OccName                -- Nice unique version (":T23Map")
+mkInstTyTcOcc uniq occ
+   = mk_deriv varName (":T" ++ show uniq) (occNameString occ)
+
+-- Derive a name for the coercion of a data/newtype instance.
+--
+mkInstTyCoOcc :: Unique                -- Unique
+             -> OccName                -- Local name (e.g. "Map")
+             -> OccName                -- Nice unique version ("Co23Map")
+mkInstTyCoOcc uniq occ
+   = mk_deriv varName ("Co" ++ show uniq) (occNameString occ)
+
+\end{code}
 
 \begin{code}
 mkDFunOcc :: String            -- Typically the class and type glommed together e.g. "OrdMaybe"
index ac28ddb..e1a1aa1 100644 (file)
@@ -1006,7 +1006,7 @@ instance Binary IfaceConDecls where
                      return (IfNewTyCon aa)
 
 instance Binary IfaceConDecl where
-    put_ bh (IfCon a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) = do
+    put_ bh (IfCon a1 a2 a3 a4 a5 a6 a7 a8 a9) = do
            put_ bh a1
            put_ bh a2
            put_ bh a3
@@ -1016,7 +1016,6 @@ instance Binary IfaceConDecl where
            put_ bh a7
            put_ bh a8
            put_ bh a9
-           put_ bh a10
     get bh = do a1 <- get bh
                a2 <- get bh
                a3 <- get bh          
@@ -1026,8 +1025,7 @@ instance Binary IfaceConDecl where
                a7 <- get bh
                a8 <- get bh
                a9 <- get bh
-               a10 <- get bh
-               return (IfCon a1 a2 a3 a4 a5 a6 a7 a8 a9 a10)
+               return (IfCon a1 a2 a3 a4 a5 a6 a7 a8 a9)
 
 instance Binary IfaceClassOp where
    put_ bh (IfaceClassOp n def ty) = do        
index 05f5f4b..5f23fd5 100644 (file)
@@ -25,7 +25,8 @@ import BasicTypes     ( RecFlag, StrictnessMark(..) )
 import Name            ( Name )
 import OccName         ( mkDataConWrapperOcc, mkDataConWorkerOcc,
                          mkClassTyConOcc, mkClassDataConOcc,
-                         mkSuperDictSelOcc, mkNewTyCoOcc, mkLocalOcc ) 
+                         mkSuperDictSelOcc, mkNewTyCoOcc, mkInstTyTcOcc,
+                         mkInstTyCoOcc ) 
 import MkId            ( mkDataConIds, mkRecordSelId, mkDictSelId )
 import Class           ( mkClass, Class( classTyCon), FunDep, DefMeth(..) )
 import TyCon           ( mkSynTyCon, mkAlgTyCon, visibleDataCons,
@@ -41,7 +42,7 @@ import Type           ( mkArrowKinds, liftedTypeKind, typeKind,
                          TyThing(..), 
                          substTyWith, zipTopTvSubst, substTheta, mkForAllTys,
                           mkTyConApp, mkTyVarTy )
-import Coercion         ( mkNewTypeCoercion )
+import Coercion         ( mkNewTypeCoercion, mkDataInstCoercion )
 import Outputable
 import List            ( nub )
 
@@ -68,27 +69,55 @@ buildAlgTyCon :: Name -> [TyVar]
              -> RecFlag
              -> Bool                   -- True <=> want generics functions
              -> Bool                   -- True <=> was declared in GADT syntax
-             -> Maybe TyCon            -- Just family <=> instance of `family'
+             -> Maybe (TyCon, [Type])  -- Just (family, tys) 
+                                       -- <=> instance of `family' at `tys'
              -> TcRnIf m n TyCon
 
 buildAlgTyCon tc_name tvs stupid_theta rhs is_rec want_generics gadt_syn
              mb_family
-  = do { -- In case of a type instance, we need to invent a new name for the
-         -- instance type, as `tc_name' is the family name.
-       ; uniq <- newUnique
-       ; (final_name, parent) <- 
-           case mb_family of
-             Nothing     -> return (tc_name, NoParentTyCon)
-             Just family -> 
-               do { final_name <- newImplicitBinder tc_name (mkLocalOcc uniq)
-                  ; return (final_name, FamilyTyCon family)
-                  }
-       ; let { tycon = mkAlgTyCon final_name kind tvs stupid_theta rhs
-                                  fields parent is_rec want_generics gadt_syn
-             ; kind    = mkArrowKinds (map tyVarKind tvs) liftedTypeKind
-             ; fields  = mkTyConSelIds tycon rhs
-         }
-       ; return tycon }
+  = do { -- We need to tie a knot as the coercion of a data instance depends
+        -- on the instance representation tycon and vice versa.
+       ; tycon <- fixM (\ tycon_rec -> do 
+        { (final_name, parent) <- maybeComputeFamilyInfo mb_family tycon_rec
+        ; let { tycon = mkAlgTyCon final_name kind tvs stupid_theta rhs
+                                   fields parent is_rec want_generics gadt_syn
+              ; kind    = mkArrowKinds (map tyVarKind tvs) liftedTypeKind
+              ; fields  = mkTyConSelIds tycon rhs
+              }
+         ; return tycon
+         })
+       ; return tycon 
+       }
+  where
+    -- If a family tycon with instance types is given, the current tycon is an
+    -- instance of that family and we have to perform three extra tasks:
+    --
+    -- (1) The instance tycon (representing the family at a particular type
+    --     instance) need to get a new, derived name - we may not reuse the
+    --     family name.
+    -- (2) Create a coercion that identifies the family instance type and the
+    --     representation type from Step (1); ie, it is of the form 
+    --    `Co tvs :: F ts :=: R tvs', where `Co' is the name of the coercion,
+    --    `F' the family tycon and `R' the (derived) representation tycon.
+    -- (3) Produce a `AlgTyConParent' value containing the parent and coercion
+    --     information.
+    --
+    maybeComputeFamilyInfo Nothing                  rep_tycon = 
+      return (tc_name, NoParentTyCon)
+    maybeComputeFamilyInfo (Just (family, instTys)) rep_tycon =
+      do { -- (1) New, derived name for the instance tycon
+        ; uniq <- newUnique
+        ; final_name <- newImplicitBinder tc_name (mkInstTyTcOcc uniq)
+
+          -- (2) Create the coercion.
+        ; co_tycon_name <- newImplicitBinder tc_name (mkInstTyCoOcc uniq)
+        ; let co_tycon = mkDataInstCoercion co_tycon_name tvs
+                                            family instTys rep_tycon
+
+          -- (3) Produce parent information.
+        ; return (final_name, FamilyTyCon family instTys co_tycon)
+        }
+    
 
 ------------------------------------------------------
 mkAbstractTyConRhs :: AlgTyConRhs
@@ -190,14 +219,13 @@ buildDataCon :: Name -> Bool
            -> ThetaType                -- Does not include the "stupid theta"
                                        -- or the GADT equalities
            -> [Type] -> TyCon
-           -> Maybe [Type]             -- Just ts <=> type pats of inst type
            -> TcRnIf m n DataCon
 -- A wrapper for DataCon.mkDataCon that
 --   a) makes the worker Id
 --   b) makes the wrapper Id if necessary, including
 --     allocating its unique (hence monadic)
 buildDataCon src_name declared_infix arg_stricts field_lbls
-            univ_tvs ex_tvs eq_spec ctxt arg_tys tycon mb_typats
+            univ_tvs ex_tvs eq_spec ctxt arg_tys tycon
   = do { wrap_name <- newImplicitBinder src_name mkDataConWrapperOcc
        ; work_name <- newImplicitBinder src_name mkDataConWorkerOcc
        -- This last one takes the name of the data constructor in the source
@@ -209,7 +237,7 @@ buildDataCon src_name declared_infix arg_stricts field_lbls
                data_con = mkDataCon src_name declared_infix
                                     arg_stricts field_lbls
                                     univ_tvs ex_tvs eq_spec ctxt
-                                    arg_tys tycon mb_typats
+                                    arg_tys tycon
                                     stupid_ctxt dc_ids
                dc_ids = mkDataConIds wrap_name work_name data_con
 
@@ -286,7 +314,7 @@ buildClass class_name tvs sc_theta fds ats sig_stuff tc_isrec
                                   tvs [{- no existentials -}]
                                    [{- No equalities -}] [{-No context-}] 
                                    dict_component_tys 
-                                  rec_tycon Nothing
+                                  rec_tycon
 
        ; rhs <- case dict_component_tys of
                            [rep_ty] -> mkNewTyConRhs tycon_name rec_tycon dict_con
index 02fa5b5..bf62095 100644 (file)
@@ -85,7 +85,9 @@ data IfaceDecl
                                                -- been compiled with
                                                -- different flags to the
                                                -- current compilation unit 
-                ifFamily     :: Maybe IfaceTyCon-- Just fam <=> instance of fam
+                ifFamInst    :: Maybe           -- Just _ <=> instance of fam
+                                 (IfaceTyCon,  --   Family tycon
+                                  [IfaceType]) --   Instance types
     }
 
   | IfaceSyn  {        ifName    :: OccName,           -- Type constructor
@@ -137,9 +139,8 @@ data IfaceConDecl
        ifConCtxt    :: IfaceContext,           -- Non-stupid context
        ifConArgTys  :: [IfaceType],            -- Arg types
        ifConFields  :: [OccName],              -- ...ditto... (field labels)
-       ifConStricts :: [StrictnessMark],       -- Empty (meaning all lazy),
+       ifConStricts :: [StrictnessMark]}       -- Empty (meaning all lazy),
                                                -- or 1-1 corresp with arg tys
-        ifConInstTys :: Maybe [IfaceType] }     -- instance types
 
 data IfaceInst 
   = IfaceInst { ifInstCls  :: IfaceExtName,            -- See comments with
@@ -258,10 +259,10 @@ pprIfaceDecl (IfaceSyn {ifName = tycon, ifTyVars = tyvars,
 
 pprIfaceDecl (IfaceData {ifName = tycon, ifGeneric = gen, ifCtxt = context,
                         ifTyVars = tyvars, ifCons = condecls, 
-                        ifRec = isrec, ifFamily = mbFamily})
+                        ifRec = isrec, ifFamInst = mbFamInst})
   = hang (pp_nd <+> pprIfaceDeclHead context tycon tyvars)
-       4 (vcat [pprRec isrec, pprGen gen, pprFamily mbFamily, 
-               pp_condecls tycon condecls])
+       4 (vcat [pprRec isrec, pprGen gen, pp_condecls tycon condecls,
+               pprFamily mbFamInst])
   where
     pp_nd = case condecls of
                IfAbstractTyCon -> ptext SLIT("data")
@@ -282,15 +283,17 @@ pprRec isrec = ptext SLIT("RecFlag") <+> ppr isrec
 pprGen True  = ptext SLIT("Generics: yes")
 pprGen False = ptext SLIT("Generics: no")
 
-pprFamily Nothing    = ptext SLIT("DataFamily: none")
-pprFamily (Just fam) = ptext SLIT("DataFamily:") <+> ppr fam
+pprFamily Nothing           = ptext SLIT("FamilyInstance: none")
+pprFamily (Just (fam, tys)) = ptext SLIT("FamilyInstance:") <+> 
+                             ppr fam <+> hsep (map ppr tys)
 
 instance Outputable IfaceClassOp where
    ppr (IfaceClassOp n dm ty) = ppr n <+> ppr dm <+> dcolon <+> ppr ty
 
 pprIfaceDeclHead :: IfaceContext -> OccName -> [IfaceTvBndr] -> SDoc
-pprIfaceDeclHead context thing tyvars 
-  = hsep [pprIfaceContext context, parenSymOcc thing (ppr thing), pprIfaceTvBndrs tyvars]
+pprIfaceDeclHead context thing tyvars
+  = hsep [pprIfaceContext context, parenSymOcc thing (ppr thing), 
+         pprIfaceTvBndrs tyvars]
 
 pp_condecls tc IfAbstractTyCon  = ptext SLIT("{- abstract -}")
 pp_condecls tc IfOpenNewTyCon   = empty
@@ -542,7 +545,7 @@ eqIfDecl d1@(IfaceData {}) d2@(IfaceData {})
          ifRec d1     == ifRec   d2 && 
          ifGadtSyntax d1 == ifGadtSyntax   d2 && 
          ifGeneric d1 == ifGeneric d2) &&&
-    ifFamily d1 `eqIfTc_mb` ifFamily d2 &&&
+    ifFamInst d1 `eqIfTc_fam` ifFamInst d2 &&&
     eqWith (ifTyVars d1) (ifTyVars d2) (\ env -> 
            eq_ifContext env (ifCtxt d1) (ifCtxt d2) &&& 
            eq_hsCD env (ifCons d1) (ifCons d2) 
@@ -551,9 +554,10 @@ eqIfDecl d1@(IfaceData {}) d2@(IfaceData {})
        -- over the constructors (any more), but they do scope
        -- over the stupid context in the IfaceConDecls
   where
-    Nothing     `eqIfTc_mb` Nothing     = Equal
-    (Just fam1) `eqIfTc_mb` (Just fam2) = fam1 `eqIfTc` fam2
-    _          `eqIfTc_mb` _           = NotEqual
+    Nothing             `eqIfTc_fam` Nothing             = Equal
+    (Just (fam1, tys1)) `eqIfTc_fam` (Just (fam2, tys2)) = 
+      fam1 `eqIfTc` fam2 &&& eqListBy eqIfType tys1 tys2
+    _                  `eqIfTc_fam` _                   = NotEqual
 
 eqIfDecl d1@(IfaceSyn {}) d2@(IfaceSyn {})
   = bool (ifName d1 == ifName d2) &&&
index 4cb2b53..d399967 100644 (file)
@@ -191,11 +191,11 @@ import TyCon              ( TyCon, AlgTyConRhs(..), SynTyConRhs(..),
                          isTupleTyCon, tupleTyConBoxity, tyConStupidTheta,
                          tyConHasGenerics, synTyConRhs, isGadtSyntaxTyCon,
                          tyConArity, tyConTyVars, algTyConRhs, tyConExtName,
-                         tyConFamily_maybe )
+                         tyConFamInst_maybe )
 import DataCon         ( dataConName, dataConFieldLabels, dataConStrictMarks,
                          dataConTyCon, dataConIsInfix, dataConUnivTyVars,
                          dataConExTyVars, dataConEqSpec, dataConTheta,
-                         dataConOrigArgTys, dataConInstTys ) 
+                         dataConOrigArgTys ) 
 import Type            ( TyThing(..), splitForAllTys, funResultTy )
 import TcType          ( deNoteType )
 import TysPrim         ( alphaTyVars )
@@ -1036,7 +1036,7 @@ tyThingToIfaceDecl ext (ATyCon tycon)
                ifRec     = boolToRecFlag (isRecursiveTyCon tycon),
                ifGadtSyntax = isGadtSyntaxTyCon tycon,
                ifGeneric = tyConHasGenerics tycon,
-               ifFamily  = fmap (toIfaceTyCon ext) $ tyConFamily_maybe tycon }
+               ifFamInst = famInstToIface $ tyConFamInst_maybe tycon }
 
   | isForeignTyCon tycon
   = IfaceForeign { ifName    = getOccName tycon,
@@ -1051,7 +1051,7 @@ tyThingToIfaceDecl ext (ATyCon tycon)
                ifGadtSyntax = False,
                ifGeneric = False,
                ifRec     = NonRecursive,
-               ifFamily  = Nothing }
+               ifFamInst = Nothing }
 
   | otherwise = pprPanic "toIfaceDecl" (ppr tycon)
   where
@@ -1083,12 +1083,14 @@ tyThingToIfaceDecl ext (ATyCon tycon)
                                       (dataConOrigArgTys data_con),
                    ifConFields  = map getOccName 
                                       (dataConFieldLabels data_con),
-                   ifConStricts = dataConStrictMarks data_con,
-                   ifConInstTys = fmap (map (toIfaceType ext)) 
-                                       (dataConInstTys data_con) }
+                   ifConStricts = dataConStrictMarks data_con }
 
     to_eq_spec spec = [(getOccName tv, toIfaceType ext ty) | (tv,ty) <- spec]
 
+    famInstToIface Nothing                    = Nothing
+    famInstToIface (Just (famTyCon, instTys)) = 
+      Just (toIfaceTyCon ext famTyCon, map (toIfaceType ext) instTys)
+
 tyThingToIfaceDecl ext (ADataCon dc)
  = pprPanic "toIfaceDecl" (ppr dc)     -- Should be trimmed out earlier
 
index 388d040..2831c2d 100644 (file)
@@ -361,21 +361,23 @@ tcIfaceDecl (IfaceData {ifName = occ_name,
                        ifCons = rdr_cons, 
                        ifRec = is_rec, 
                        ifGeneric = want_generic,
-                       ifFamily = mb_family })
+                       ifFamInst = mb_family })
   = do { tc_name <- lookupIfaceTop occ_name
        ; bindIfaceTyVars tv_bndrs $ \ tyvars -> do
 
        { tycon <- fixM ( \ tycon -> do
            { stupid_theta <- tcIfaceCtxt ctxt
+           ; famInst <- 
+               case mb_family of
+                 Nothing         -> return Nothing
+                 Just (fam, tys) -> 
+                   do { famTyCon <- tcIfaceTyCon fam
+                      ; insttys <- mapM tcIfaceType tys
+                      ; return $ Just (famTyCon, insttys)
+                      }
            ; cons <- tcIfaceDataCons tc_name tycon tyvars rdr_cons
-           ; family <- case mb_family of
-                         Nothing  -> return Nothing
-                         Just fam -> 
-                           do { famTyCon <- tcIfaceTyCon fam
-                              ; return $ Just famTyCon
-                              }
            ; buildAlgTyCon tc_name tyvars stupid_theta
-                           cons is_rec want_generic gadt_syn family
+                           cons is_rec want_generic gadt_syn famInst
            })
         ; traceIf (text "tcIfaceDecl4" <+> ppr tycon)
        ; return (ATyCon tycon)
@@ -437,7 +439,7 @@ tcIfaceDataCons tycon_name tycon tc_tyvars if_cons
                         ifConUnivTvs = univ_tvs, ifConExTvs = ex_tvs,
                         ifConOcc = occ, ifConCtxt = ctxt, ifConEqSpec = spec,
                         ifConArgTys = args, ifConFields = field_lbls,
-                        ifConStricts = stricts, ifConInstTys = mb_insttys })
+                        ifConStricts = stricts})
       = bindIfaceTyVars univ_tvs $ \ univ_tyvars -> do
        bindIfaceTyVars ex_tvs   $ \ ex_tyvars -> do
        { name  <- lookupIfaceTop occ
@@ -456,17 +458,12 @@ tcIfaceDataCons tycon_name tycon tc_tyvars if_cons
        -- the component types unless they are really needed
        ; arg_tys <- forkM (mk_doc name) (mappM tcIfaceType args)
        ; lbl_names <- mappM lookupIfaceTop field_lbls
-       ; mb_insttys' <- case mb_insttys of 
-                          Nothing      -> return Nothing 
-                          Just insttys -> liftM Just $ 
-                                            mappM tcIfaceType insttys
 
        ; buildDataCon name is_infix {- Not infix -}
                       stricts lbl_names
                       univ_tyvars ex_tyvars 
                        eq_spec theta 
                       arg_tys tycon
-                      mb_insttys'
        }
     mk_doc con_name = ptext SLIT("Constructor") <+> ppr con_name
 
index db80d3c..598fa42 100644 (file)
@@ -232,7 +232,6 @@ pcDataConWithFixity declared_infix dc_name tyvars arg_tys tycon
                []      -- No equality spec
                []      -- No theta
                arg_tys tycon
-               Nothing -- not a data instance
                []      -- No stupid theta
                (mkDataConIds bogus_wrap_name wrk_name data_con)
                
index ddccb2f..7f6baf8 100644 (file)
@@ -311,7 +311,7 @@ tcIdxTyInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
 
        ; tycon <- fixM (\ tycon -> do 
             { data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data 
-                                             tycon t_tvs (Just t_typats)))
+                                             tycon t_tvs))
                                  k_cons
             ; tc_rhs <-
                 case new_or_data of
@@ -320,7 +320,7 @@ tcIdxTyInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
                            ASSERT( isSingleton data_cons )
                            mkNewTyConRhs tc_name tycon (head data_cons)
             ; buildAlgTyCon tc_name t_tvs stupid_theta tc_rhs Recursive
-                            False h98_syntax (Just family)
+                            False h98_syntax (Just (family, t_typats))
                  -- We always assume that indexed types are recursive.  Why?
                  -- (1) Due to their open nature, we can never be sure that a
                  -- further instance might not introduce a new recursive
@@ -329,7 +329,6 @@ tcIdxTyInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
             })
 
          -- construct result
-        -- !!!TODO: missing eq axiom
        ; return (Nothing, Just (ATyCon tycon))
        }}
        where
@@ -679,7 +678,7 @@ tcTyClDecl1 calc_isrec
 
   ; tycon <- fixM (\ tycon -> do 
        { data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data 
-                                                tycon final_tvs Nothing)) 
+                                                tycon final_tvs)) 
                             cons
        ; tc_rhs <-
            if null cons && is_boot     -- In a hs-boot file, empty cons means
@@ -737,11 +736,10 @@ tcTyClDecl1 calc_isrec
 tcConDecl :: Bool              -- True <=> -funbox-strict_fields
          -> NewOrData 
          -> TyCon -> [TyVar] 
-         -> Maybe [Type]       -- Just ts <=> type patterns of instance type
          -> ConDecl Name 
          -> TcM DataCon
 
-tcConDecl unbox_strict NewType tycon tc_tvs mb_typats  -- Newtypes
+tcConDecl unbox_strict NewType tycon tc_tvs    -- Newtypes
          (ConDecl name _ ex_tvs ex_ctxt details ResTyH98)
   = do { let tc_datacon field_lbls arg_ty
                = do { arg_ty' <- tcHsKindedType arg_ty -- No bang on newtype
@@ -751,8 +749,7 @@ tcConDecl unbox_strict NewType tycon tc_tvs mb_typats       -- Newtypes
                                    tc_tvs []  -- No existentials
                                    [] []      -- No equalities, predicates
                                    [arg_ty']
-                                   tycon 
-                                   mb_typats}
+                                   tycon }
 
                -- Check that a newtype has no existential stuff
        ; checkTc (null ex_tvs && null (unLoc ex_ctxt)) (newtypeExError name)
@@ -765,7 +762,7 @@ tcConDecl unbox_strict NewType tycon tc_tvs mb_typats       -- Newtypes
                        -- Check that the constructor has exactly one field
        }
 
-tcConDecl unbox_strict DataType tycon tc_tvs mb_typats -- Data types
+tcConDecl unbox_strict DataType tycon tc_tvs   -- Data types
          (ConDecl name _ tvs ctxt details res_ty)
   = tcTyVarBndrs tvs           $ \ tvs' -> do 
     { ctxt' <- tcHsKindedContext ctxt
@@ -778,8 +775,7 @@ tcConDecl unbox_strict DataType tycon tc_tvs mb_typats      -- Data types
                    (argStrictness unbox_strict tycon bangs arg_tys)
                    (map unLoc field_lbls)
                    univ_tvs ex_tvs eq_preds ctxt' arg_tys
-                   data_tc 
-                   mb_typats}
+                   data_tc }
                -- NB:  we put data_tc, the type constructor gotten from the
                --      constructor type signature into the data constructor;
                --      that way checkValidDataCon can complain if it's wrong.
index 25d04ec..d715016 100644 (file)
@@ -22,7 +22,7 @@ module Coercion (
         mkSymCoercion, mkTransCoercion,
         mkLeftCoercion, mkRightCoercion, mkInstCoercion, mkAppCoercion,
         mkForAllCoercion, mkFunCoercion, mkInstsCoercion, mkUnsafeCoercion,
-        mkNewTypeCoercion, mkAppsCoercion,
+        mkNewTypeCoercion, mkDataInstCoercion, mkAppsCoercion,
 
         splitNewTypeRepCo_maybe, decomposeCo,
 
@@ -323,7 +323,31 @@ mkNewTypeCoercion name tycon tvs rhs_ty
     rhs_eta
       | (ty, ty_args) <- splitAppTys rhs_ty
       = mkAppTys ty (reverse (drop n_eta_tys (reverse ty_args)))
+
+-- Coercion identifying a data/newtype representation type and its family
+-- instance.  It has the form `Co tvs :: F ts :=: R tvs', where `Co' is the
+-- coercion tycon built here, `F' the family tycon and `R' the (derived)
+-- representation tycon.
+--
+mkDataInstCoercion :: Name     -- unique name for the coercion tycon
+                  -> [TyVar]   -- type parameters of the coercion (`tvs')
+                  -> TyCon     -- family tycon (`F')
+                  -> [Type]    -- type instance (`ts')
+                  -> TyCon     -- representation tycon (`R')
+                  -> TyCon     -- => coercion tycon (`Co')
+mkDataInstCoercion name tvs family instTys rep_tycon
+  = mkCoercionTyCon name coArity (mkKindingFun rule)
+  where
+    coArity = length tvs
+
+    rule args = (substTyWith tvs tys $         -- with sigma = [tys/tvs],
+                  TyConApp family instTys,     --     sigma (F ts)
+                TyConApp rep_tycon instTys,    -- :=: R tys
+                rest)                          -- surplus arguments
+      where
+        tys  = take coArity args
+        rest = drop coArity args
+
 --------------------------------------
 -- Coercion Type Constructors...
 
index 7fcc52b..5ded0a8 100644 (file)
@@ -47,7 +47,7 @@ module TyCon(
        tyConStupidTheta,
        tyConArity,
        isClassTyCon, tyConClass_maybe,
-       isFamInstTyCon, tyConFamily_maybe,
+       isFamInstTyCon, tyConFamInst_maybe, tyConFamilyCoercion_maybe,
        synTyConDefn, synTyConRhs, synTyConType, synTyConResKind,
        tyConExtName,           -- External name for foreign types
 
@@ -237,9 +237,24 @@ visibleDataCons OpenNewTyCon                     = []
 visibleDataCons (DataTyCon{ data_cons = cs }) = cs
 visibleDataCons (NewTyCon{ data_con = c })    = [c]
 
-data AlgTyConParent = NoParentTyCon            -- ordinary data type
-                   | ClassTyCon    Class       -- class dictionary
-                   | FamilyTyCon   TyCon       -- instance of type family
+-- Both type classes as well as data/newtype family instances imply implicit
+-- type constructors.  These implicit type constructors refer to their parent
+-- structure (ie, the class or family from which they derive) using a type of
+-- the following form.
+--
+data AlgTyConParent = -- An ordinary type constructor has no parent.
+                     NoParentTyCon
+
+                     -- Type constructors representing a class dictionary.
+                   | ClassTyCon    Class       
+
+                     -- Type constructors representing an instances of a type
+                     -- family.
+                   | FamilyTyCon   TyCon       -- the type family
+                                   [Type]      -- instance types
+                                   TyCon       -- a *coercion* identifying
+                                               -- the representation type
+                                               -- with the type instance
 
 data SynTyConRhs
   = OpenSynTyCon Kind  -- Type family: *result* kind given
@@ -754,12 +769,20 @@ tyConClass_maybe (AlgTyCon {algTcParent = ClassTyCon clas}) = Just clas
 tyConClass_maybe ther_tycon                                = Nothing
 
 isFamInstTyCon :: TyCon -> Bool
-isFamInstTyCon (AlgTyCon {algTcParent = FamilyTyCon _}) = True
-isFamInstTyCon other_tycon                             = False
-
-tyConFamily_maybe :: TyCon -> Maybe TyCon
-tyConFamily_maybe (AlgTyCon {algTcParent = FamilyTyCon fam}) = Just fam
-tyConFamily_maybe ther_tycon                                = Nothing
+isFamInstTyCon (AlgTyCon {algTcParent = FamilyTyCon _ _ _}) = True
+isFamInstTyCon other_tycon                                 = False
+
+tyConFamInst_maybe :: TyCon -> Maybe (TyCon, [Type])
+tyConFamInst_maybe (AlgTyCon {algTcParent = FamilyTyCon fam instTys _}) = 
+  Just (fam, instTys)
+tyConFamInst_maybe ther_tycon                                          = 
+  Nothing
+
+tyConFamilyCoercion_maybe :: TyCon -> Maybe TyCon
+tyConFamilyCoercion_maybe (AlgTyCon {algTcParent = FamilyTyCon _ _ coe}) = 
+  Just coe
+tyConFamilyCoercion_maybe ther_tycon                                    = 
+  Nothing
 \end{code}