Interface file optimisation and removal of nameParent
[ghc-hetmet.git] / compiler / basicTypes / MkId.lhs
index 8f71aab..9818eba 100644 (file)
@@ -20,12 +20,13 @@ module MkId (
        mkRecordSelId, 
        mkPrimOpId, mkFCallId,
 
        mkRecordSelId, 
        mkPrimOpId, mkFCallId,
 
-       mkReboxingAlt, mkNewTypeBody,
+       mkReboxingAlt, wrapNewTypeBody, unwrapNewTypeBody,
+        mkUnpackCase, mkProductBox,
 
        -- And some particular Ids; see below for why they are wired in
        wiredInIds, ghcPrimIds,
        unsafeCoerceId, realWorldPrimId, voidArgId, nullAddrId, seqId,
 
        -- And some particular Ids; see below for why they are wired in
        wiredInIds, ghcPrimIds,
        unsafeCoerceId, realWorldPrimId, voidArgId, nullAddrId, seqId,
-       lazyId, lazyIdUnfolding, lazyIdKey,
+       lazyId, lazyIdUnfolding, lazyIdKey, 
 
        mkRuntimeErrorApp,
        rEC_CON_ERROR_ID, iRREFUT_PAT_ERROR_ID, rUNTIME_ERROR_ID,
 
        mkRuntimeErrorApp,
        rEC_CON_ERROR_ID, iRREFUT_PAT_ERROR_ID, rUNTIME_ERROR_ID,
@@ -45,31 +46,41 @@ import TysPrim              ( openAlphaTyVars, alphaTyVar, alphaTy,
                        )
 import TysWiredIn      ( charTy, mkListTy )
 import PrelRules       ( primOpRules )
                        )
 import TysWiredIn      ( charTy, mkListTy )
 import PrelRules       ( primOpRules )
-import Type            ( TyThing(..), mkForAllTy, tyVarsOfTypes )
+import Type            ( TyThing(..), mkForAllTy, tyVarsOfTypes, 
+                         newTyConInstRhs, mkTopTvSubst, substTyVar, 
+                         substTys, zipTopTvSubst )
+import TcGadt           ( gadtRefine, refineType, emptyRefinement )
+import HsBinds          ( HsWrapper(..), isIdHsWrapper )
+import Coercion         ( mkSymCoercion, mkUnsafeCoercion, isEqPred )
 import TcType          ( Type, ThetaType, mkDictTy, mkPredTys, mkPredTy, 
 import TcType          ( Type, ThetaType, mkDictTy, mkPredTys, mkPredTy, 
-                         mkTyConApp, mkTyVarTys, mkClassPred, 
-                         mkFunTys, mkFunTy, mkSigmaTy, tcSplitSigmaTy, 
+                         mkTyConApp, mkTyVarTys, mkClassPred, isPredTy,
+                         mkFunTys, mkFunTy, mkSigmaTy, tcSplitSigmaTy, tcEqType,
                          isUnLiftedType, mkForAllTys, mkTyVarTy, tyVarsOfType,
                          tcSplitFunTys, tcSplitForAllTys, dataConsStupidTheta
                        )
                          isUnLiftedType, mkForAllTys, mkTyVarTy, tyVarsOfType,
                          tcSplitFunTys, tcSplitForAllTys, dataConsStupidTheta
                        )
-import CoreUtils       ( exprType )
+import CoreUtils       ( exprType, dataConOrigInstPat, mkCoerce )
 import CoreUnfold      ( mkTopUnfolding, mkCompulsoryUnfolding )
 import Literal         ( nullAddrLit, mkStringLit )
 import CoreUnfold      ( mkTopUnfolding, mkCompulsoryUnfolding )
 import Literal         ( nullAddrLit, mkStringLit )
-import TyCon           ( TyCon, isNewTyCon, tyConDataCons, FieldLabel,
-                          tyConStupidTheta, isProductTyCon, isDataTyCon, isRecursiveTyCon )
+import TyCon           ( TyCon, isNewTyCon, tyConTyVars, tyConDataCons,
+                         FieldLabel,
+                          tyConStupidTheta, isProductTyCon, isDataTyCon,
+                          isRecursiveTyCon, isFamInstTyCon,
+                          tyConFamInst_maybe, tyConFamilyCoercion_maybe,
+                          newTyConCo_maybe )
 import Class           ( Class, classTyCon, classSelIds )
 import Class           ( Class, classTyCon, classSelIds )
-import Var             ( Id, TyVar, Var )
+import Var             ( Id, TyVar, Var, setIdType )
 import VarSet          ( isEmptyVarSet, subVarSet, varSetElems )
 import VarSet          ( isEmptyVarSet, subVarSet, varSetElems )
-import Name            ( mkFCallName, mkWiredInName, Name, BuiltInSyntax(..) )
+import Name            ( mkFCallName, mkWiredInName, Name, BuiltInSyntax(..))
 import OccName         ( mkOccNameFS, varName )
 import PrimOp          ( PrimOp, primOpSig, primOpOcc, primOpTag )
 import ForeignCall     ( ForeignCall )
 import OccName         ( mkOccNameFS, varName )
 import PrimOp          ( PrimOp, primOpSig, primOpOcc, primOpTag )
 import ForeignCall     ( ForeignCall )
-import DataCon         ( DataCon, DataConIds(..), dataConTyVars,
+import DataCon         ( DataCon, DataConIds(..), dataConTyCon,
+                         dataConUnivTyVars, 
                          dataConFieldLabels, dataConRepArity, dataConResTys,
                          dataConFieldLabels, dataConRepArity, dataConResTys,
-                         dataConRepArgTys, dataConRepType, 
-                         dataConSig, dataConStrictMarks, dataConExStricts, 
+                         dataConRepArgTys, dataConRepType, dataConFullSig,
+                         dataConStrictMarks, dataConExStricts, 
                          splitProductType, isVanillaDataCon, dataConFieldType,
                          splitProductType, isVanillaDataCon, dataConFieldType,
-                         dataConInstOrigArgTys
+                         deepSplitProductType, 
                        )
 import Id              ( idType, mkGlobalId, mkVanillaGlobal, mkSysLocal, 
                          mkTemplateLocals, mkTemplateLocalsNum, mkExportedLocalId,
                        )
 import Id              ( idType, mkGlobalId, mkVanillaGlobal, mkSysLocal, 
                          mkTemplateLocals, mkTemplateLocalsNum, mkExportedLocalId,
@@ -91,7 +102,7 @@ import PrelNames
 import Util             ( dropList, isSingleton )
 import Outputable
 import FastString
 import Util             ( dropList, isSingleton )
 import Outputable
 import FastString
-import ListSetOps      ( assoc )
+import ListSetOps      ( assoc, minusList )
 \end{code}             
 
 %************************************************************************
 \end{code}             
 
 %************************************************************************
@@ -181,33 +192,80 @@ Notice that
   Making an explicit case expression allows the simplifier to eliminate
   it in the (common) case where the constructor arg is already evaluated.
 
   Making an explicit case expression allows the simplifier to eliminate
   it in the (common) case where the constructor arg is already evaluated.
 
+[Wrappers for data instance tycons]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+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.  For example, consider the declarations
+
+  data family Map k :: * -> *
+  data instance Map (a, b) v = MapPair (Map a (Pair b v))
+
+The tycon to which the datacon MapPair belongs gets a unique internal name of
+the form :R123Map, and we call it the representation tycon.  In contrast, Map
+is the family tycon (accessible via tyConFamInst_maybe).  The wrapper and work
+of MapPair get the types
+
+  $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
+  $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
+
+which implies that the wrapper code will have to apply the coercion moving
+between representation and family type.  It is accessible via
+tyConFamilyCoercion_maybe and has kind
+
+  Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
+
+This coercion is conditionally applied by wrapFamInstBody.
 
 \begin{code}
 mkDataConIds :: Name -> Name -> DataCon -> DataConIds
 
 \begin{code}
 mkDataConIds :: Name -> Name -> DataCon -> DataConIds
-       -- Makes the *worker* for the data constructor; that is, the function
-       -- that takes the reprsentation arguments and builds the constructor.
 mkDataConIds wrap_name wkr_name data_con
   | isNewTyCon tycon
 mkDataConIds wrap_name wkr_name data_con
   | isNewTyCon tycon
-  = NewDC nt_wrap_id
+  = DCIds Nothing nt_work_id                 -- Newtype, only has a worker
 
 
-  | any isMarkedStrict all_strict_marks                -- Algebraic, needs wrapper
-  = AlgDC (Just alg_wrap_id) wrk_id
+  | any isMarkedStrict all_strict_marks             -- Algebraic, needs wrapper
+    || not (null eq_spec)                   -- NB: LoadIface.ifaceDeclSubBndrs
+    || isFamInstTyCon tycon                 --     depends on this test
+  = DCIds (Just alg_wrap_id) wrk_id
 
 
-  | otherwise                                  -- Algebraic, no wrapper
-  = AlgDC Nothing wrk_id
+  | otherwise                               -- Algebraic, no wrapper
+  = DCIds Nothing wrk_id
   where
   where
-    (tyvars, theta, orig_arg_tys, tycon, res_tys) = dataConSig data_con
-
-    dict_tys    = mkPredTys theta
-    all_arg_tys = dict_tys ++ orig_arg_tys
-    result_ty   = mkTyConApp tycon res_tys
+    (univ_tvs, ex_tvs, eq_spec, 
+     theta, orig_arg_tys)          = dataConFullSig data_con
+    tycon                          = dataConTyCon data_con
 
 
-    wrap_ty = mkForAllTys tyvars (mkFunTys all_arg_tys result_ty)
+       ----------- Wrapper --------------
        -- We used to include the stupid theta in the wrapper's args
        -- but now we don't.  Instead the type checker just injects these
        -- extra constraints where necessary.
        -- We used to include the stupid theta in the wrapper's args
        -- but now we don't.  Instead the type checker just injects these
        -- extra constraints where necessary.
+    wrap_tvs = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs
+    subst         = mkTopTvSubst eq_spec
+    famSubst      = ASSERT( length (tyConTyVars tycon  ) ==  
+                            length (mkTyVarTys univ_tvs)   )
+                    zipTopTvSubst (tyConTyVars tycon) (mkTyVarTys univ_tvs)
+                    -- substitution mapping the type constructor's type
+                    -- arguments to the universals of the data constructor
+                    -- (crucial when type checking interfaces)
+    dict_tys       = mkPredTys theta
+    result_ty_args = map (substTyVar subst) univ_tvs
+    result_ty      = case tyConFamInst_maybe tycon of
+                        -- ordinary constructor
+                      Nothing            -> mkTyConApp tycon result_ty_args
+                        -- family instance constructor
+                      Just (familyTyCon, 
+                            instTys)     -> 
+                        mkTyConApp familyTyCon ( substTys subst 
+                                               . substTys famSubst 
+                                               $ 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 
+       --     constraints in data constructor signatures
 
        ----------- Worker (algebraic data types only) --------------
 
        ----------- Worker (algebraic data types only) --------------
+       -- The *worker* for the data constructor is the function that
+       -- takes the representation arguments and builds the constructor.
     wrk_id = mkGlobalId (DataConWorkId data_con) wkr_name
                        (dataConRepType data_con) wkr_info
 
     wrk_id = mkGlobalId (DataConWorkId data_con) wkr_name
                        (dataConRepType data_con) wkr_info
 
@@ -243,9 +301,9 @@ mkDataConIds wrap_name wkr_name data_con
        -- RetCPR is only true for products that are real data types;
        -- that is, not unboxed tuples or [non-recursive] newtypes
 
        -- RetCPR is only true for products that are real data types;
        -- that is, not unboxed tuples or [non-recursive] newtypes
 
-       ----------- Wrappers for newtypes --------------
-    nt_wrap_id   = mkGlobalId (DataConWrapId data_con) wrap_name wrap_ty nt_wrap_info
-    nt_wrap_info = noCafIdInfo         -- The NoCaf-ness is set by noCafIdInfo
+       ----------- Workers for newtypes --------------
+    nt_work_id   = mkGlobalId (DataConWrapId data_con) wkr_name wrap_ty nt_work_info
+    nt_work_info = noCafIdInfo         -- The NoCaf-ness is set by noCafIdInfo
                  `setArityInfo` 1      -- Arity 1
                  `setUnfoldingInfo`     newtype_unf
     newtype_unf  = ASSERT( isVanillaDataCon data_con &&
                  `setArityInfo` 1      -- Arity 1
                  `setUnfoldingInfo`     newtype_unf
     newtype_unf  = ASSERT( isVanillaDataCon data_con &&
@@ -253,8 +311,9 @@ mkDataConIds wrap_name wkr_name data_con
                   -- No existentials on a newtype, but it can have a context
                   -- e.g.      newtype Eq a => T a = MkT (...)
                   mkCompulsoryUnfolding $ 
                   -- No existentials on a newtype, but it can have a context
                   -- e.g.      newtype Eq a => T a = MkT (...)
                   mkCompulsoryUnfolding $ 
-                  mkLams tyvars $ Lam id_arg1 $ 
-                  mkNewTypeBody tycon result_ty (Var id_arg1)
+                  mkLams wrap_tvs $ Lam id_arg1 $ 
+                  wrapNewTypeBody tycon result_ty_args
+                       (Var id_arg1)
 
     id_arg1 = mkTemplateLocal 1 (head orig_arg_tys)
 
 
     id_arg1 = mkTemplateLocal 1 (head orig_arg_tys)
 
@@ -282,14 +341,17 @@ mkDataConIds wrap_name wkr_name data_con
        -- we want to see that w is strict in its two arguments
 
     alg_unf = mkTopUnfolding $ Note InlineMe $
        -- we want to see that w is strict in its two arguments
 
     alg_unf = mkTopUnfolding $ Note InlineMe $
-             mkLams tyvars $ 
+             mkLams wrap_tvs $ 
              mkLams dict_args $ mkLams id_args $
              foldr mk_case con_app 
                    (zip (dict_args ++ id_args) all_strict_marks)
                    i3 []
 
              mkLams dict_args $ mkLams id_args $
              foldr mk_case con_app 
                    (zip (dict_args ++ id_args) all_strict_marks)
                    i3 []
 
-    con_app i rep_ids = mkApps (Var wrk_id)
-                              (map varToCoreExpr (tyvars ++ 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
 
     (dict_args,i2) = mkLocals 1  dict_tys
     (id_args,i3)   = mkLocals i2 orig_arg_tys
@@ -310,14 +372,9 @@ mkDataConIds wrap_name wkr_name data_con
                        Case (Var arg) arg result_ty [(DEFAULT,[], body i (arg:rep_args))]
 
                MarkedUnboxed
                        Case (Var arg) arg result_ty [(DEFAULT,[], body i (arg:rep_args))]
 
                MarkedUnboxed
-                  -> case splitProductType "do_unbox" (idType arg) of
-                          (tycon, tycon_args, con, tys) ->
-                                  Case (Var arg) arg result_ty  
-                                       [(DataAlt con, 
-                                         con_args,
-                                         body i' (reverse con_args ++ rep_args))]
-                             where 
-                               (con_args, i') = mkLocals i tys
+                  -> unboxProduct i (Var arg) (idType arg) the_body 
+                      where
+                        the_body i con_args = body i (reverse con_args ++ rep_args)
 
 mAX_CPR_SIZE :: Arity
 mAX_CPR_SIZE = 10
 
 mAX_CPR_SIZE :: Arity
 mAX_CPR_SIZE = 10
@@ -333,6 +390,18 @@ mAX_CPR_SIZE = 10
 mkLocals i tys = (zipWith mkTemplateLocal [i..i+n-1] tys, i+n)
               where
                 n = length tys
 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 <- tyConFamilyCoercion_maybe tycon
+  = mkCoerce (mkSymCoercion (mkTyConApp co_con args)) result_expr
+  | otherwise
+  = result_expr
 \end{code}
 
 
 \end{code}
 
 
@@ -391,11 +460,13 @@ We obviously can't define
 Nevertheless we *do* put a RecordSelId into the type environment
 so that if the user tries to use 'x' as a selector we can bleat
 helpfully, rather than saying unhelpfully that 'x' is not in scope.
 Nevertheless we *do* put a RecordSelId into the type environment
 so that if the user tries to use 'x' as a selector we can bleat
 helpfully, rather than saying unhelpfully that 'x' is not in scope.
-Hence the sel_naughty flag, to identify record selcectors that don't really exist.
+Hence the sel_naughty flag, to identify record selectors that don't really exist.
 
 In general, a field is naughty if its type mentions a type variable that
 isn't in the result type of the constructor.
 
 
 In general, a field is naughty if its type mentions a type variable that
 isn't in the result type of the constructor.
 
+Note [GADT record selectors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 For GADTs, we require that all constructors with a common field 'f' have the same
 result type (modulo alpha conversion).  [Checked in TcTyClsDecls.checkValidTyCon]
 E.g. 
 For GADTs, we require that all constructors with a common field 'f' have the same
 result type (modulo alpha conversion).  [Checked in TcTyClsDecls.checkValidTyCon]
 E.g. 
@@ -424,7 +495,7 @@ mkRecordSelId tycon field_label
   | is_naughty = naughty_id
   | otherwise  = sel_id
   where
   | is_naughty = naughty_id
   | otherwise  = sel_id
   where
-    is_naughty = not (tyVarsOfType field_ty `subVarSet` tyvar_set)
+    is_naughty = not (tyVarsOfType field_ty `subVarSet` res_tv_set)
     sel_id_details = RecordSelId tycon field_label is_naughty
 
     -- Escapist case here for naughty construcotrs
     sel_id_details = RecordSelId tycon field_label is_naughty
 
     -- Escapist case here for naughty construcotrs
@@ -440,8 +511,8 @@ mkRecordSelId tycon field_label
 
     con1       = head data_cons_w_field
     res_tys    = dataConResTys con1
 
     con1       = head data_cons_w_field
     res_tys    = dataConResTys con1
-    tyvar_set  = tyVarsOfTypes res_tys
-    tyvars     = varSetElems tyvar_set
+    res_tv_set = tyVarsOfTypes res_tys
+    res_tvs    = varSetElems res_tv_set
     data_ty    = mkTyConApp tycon res_tys
     field_ty   = dataConFieldType con1 field_label
     
     data_ty    = mkTyConApp tycon res_tys
     field_ty   = dataConFieldType con1 field_label
     
@@ -456,7 +527,9 @@ mkRecordSelId tycon field_label
     stupid_dict_tys = mkPredTys (dataConsStupidTheta data_cons_w_field)
     n_stupid_dicts  = length stupid_dict_tys
 
     stupid_dict_tys = mkPredTys (dataConsStupidTheta data_cons_w_field)
     n_stupid_dicts  = length stupid_dict_tys
 
-    (field_tyvars,field_theta,field_tau) = tcSplitSigmaTy field_ty
+    (field_tyvars,pre_field_theta,field_tau) = tcSplitSigmaTy field_ty
+  
+    field_theta  = filter (not . isEqPred) pre_field_theta
     field_dict_tys                      = mkPredTys field_theta
     n_field_dict_tys                    = length field_dict_tys
        -- If the field has a universally quantified type we have to 
     field_dict_tys                      = mkPredTys field_theta
     n_field_dict_tys                    = length field_dict_tys
        -- If the field has a universally quantified type we have to 
@@ -475,7 +548,7 @@ mkRecordSelId tycon field_label
        --      op (R op) = op
 
     selector_ty :: Type
        --      op (R op) = op
 
     selector_ty :: Type
-    selector_ty  = mkForAllTys tyvars $ mkForAllTys field_tyvars $
+    selector_ty  = mkForAllTys res_tvs $ mkForAllTys field_tyvars $
                   mkFunTys stupid_dict_tys  $  mkFunTys field_dict_tys $
                   mkFunTy data_ty field_tau
       
                   mkFunTys stupid_dict_tys  $  mkFunTys field_dict_tys $
                   mkFunTy data_ty field_tau
       
@@ -515,12 +588,14 @@ mkRecordSelId tycon field_label
     caf_info    | no_default = NoCafRefs
                | otherwise  = MayHaveCafRefs
 
     caf_info    | no_default = NoCafRefs
                | otherwise  = MayHaveCafRefs
 
-    sel_rhs = mkLams tyvars   $ mkLams field_tyvars $ 
+    sel_rhs = mkLams res_tvs $ mkLams field_tyvars $ 
              mkLams stupid_dict_ids $ mkLams field_dict_ids $
              mkLams stupid_dict_ids $ mkLams field_dict_ids $
-             Lam data_id     $ sel_body
+             Lam data_id     $ mk_result sel_body
 
 
-    sel_body | isNewTyCon tycon = mk_result (mkNewTypeBody tycon field_ty (Var data_id))
-            | otherwise        = Case (Var data_id) data_id field_tau (default_alt ++ the_alts)
+       -- NB: A newtype always has a vanilla DataCon; no existentials etc
+       --     res_tys will simply be the dataConUnivTyVars
+    sel_body | isNewTyCon tycon = unwrapNewTypeBody tycon res_tys (Var data_id)
+            | otherwise        = Case (Var data_id) data_id field_ty (default_alt ++ the_alts)
 
     mk_result poly_result = mkVarApps (mkVarApps poly_result field_tyvars) field_dict_ids
        -- We pull the field lambdas to the top, so we need to 
 
     mk_result poly_result = mkVarApps (mkVarApps poly_result field_tyvars) field_dict_ids
        -- We pull the field lambdas to the top, so we need to 
@@ -531,30 +606,112 @@ mkRecordSelId tycon field_label
        --      foo = /\a. \t:T. case t of { MkT f -> f a }
 
     mk_alt data_con 
        --      foo = /\a. \t:T. case t of { MkT f -> f a }
 
     mk_alt data_con 
-      =        -- In the non-vanilla case, the pattern must bind type variables and
-               -- the context stuff; hence the arg_prefix binding below
-         mkReboxingAlt uniqs data_con (arg_prefix ++ arg_ids)
-                       (mk_result (Var the_arg_id))
+      =   ASSERT2( res_ty `tcEqType` field_ty, ppr data_con $$ ppr res_ty $$ ppr field_ty )
+         mkReboxingAlt rebox_uniqs data_con (ex_tvs ++ co_tvs ++ arg_vs) rhs
       where
       where
-       (arg_prefix, arg_ids)
-          | isVanillaDataCon data_con          -- Instantiate from commmon base
-          = ([], mkTemplateLocalsNum arg_base (dataConInstOrigArgTys data_con res_tys))
-          | otherwise          -- The case pattern binds type variables, which are used
-                               -- in the types of the arguments of the pattern
-          = (dc_tyvars ++ mkTemplateLocalsNum arg_base (mkPredTys dc_theta),
-             mkTemplateLocalsNum arg_base' dc_arg_tys)
+           -- get pattern binders with types appropriately instantiated
+       arg_uniqs = map mkBuiltinUnique [arg_base..]
+        (ex_tvs, co_tvs, arg_vs) = dataConOrigInstPat arg_uniqs data_con res_tys
+
+       rebox_base  = arg_base + length ex_tvs + length co_tvs + length arg_vs
+       rebox_uniqs = map mkBuiltinUnique [rebox_base..]
+
+       -- data T :: *->* where T1 { fld :: Maybe b } -> T [b]
+       --      Hence T1 :: forall a b. (a=[b]) => b -> T a
+       -- fld :: forall b. T [b] -> Maybe b
+       -- fld = /\b.\(t:T[b]). case t of 
+       --              T1 b' (c : [b]=[b']) (x:Maybe b') 
+       --                      -> x `cast` Maybe (sym (right c))
+
+        Succeeded refinement = gadtRefine emptyRefinement ex_tvs co_tvs
+        (co_fn, res_ty) = refineType refinement (idType the_arg_id)
+               -- Generate the refinement for b'=b, 
+               -- and apply to (Maybe b'), to get (Maybe b)
+
+        rhs = case co_fn of
+               WpCo co -> Cast (Var the_arg_id) co
+               id_co       -> ASSERT(isIdHsWrapper id_co) Var the_arg_id
+
+       field_vs    = filter (not . isPredTy . idType) arg_vs 
+       the_arg_id  = assoc "mkRecordSelId:mk_alt" (field_lbls `zip` field_vs) field_label
+       field_lbls  = dataConFieldLabels data_con
 
 
-       (dc_tyvars, dc_theta, dc_arg_tys, _, _) = dataConSig data_con
-       arg_base' = arg_base + length dc_theta
+    error_expr = mkRuntimeErrorApp rEC_SEL_ERROR_ID field_ty full_msg
+    full_msg   = showSDoc (sep [text "No match in record selector", ppr sel_id])
 
 
-       unpack_base = arg_base' + length dc_arg_tys
-       uniqs = map mkBuiltinUnique [unpack_base..]
+-- unbox a product type...
+-- we will recurse into newtypes, casting along the way, and unbox at the
+-- first product data constructor we find. e.g.
+--  
+--   data PairInt = PairInt Int Int
+--   newtype S = MkS PairInt
+--   newtype T = MkT S
+--
+-- If we have e = MkT (MkS (PairInt 0 1)) and some body expecting a list of
+-- ids, we get (modulo int passing)
+--
+--   case (e `cast` CoT) `cast` CoS of
+--     PairInt a b -> body [a,b]
+--
+-- The Ints passed around are just for creating fresh locals
+unboxProduct :: Int -> CoreExpr -> Type -> (Int -> [Id] -> CoreExpr) -> CoreExpr
+unboxProduct i arg arg_ty body
+  = result
+  where 
+    result = mkUnpackCase the_id arg con_args boxing_con rhs
+    (_tycon, _tycon_args, boxing_con, tys) = deepSplitProductType "unboxProduct" arg_ty
+    ([the_id], i') = mkLocals i [arg_ty]
+    (con_args, i'') = mkLocals i' tys
+    rhs = body i'' con_args
+
+mkUnpackCase ::  Id -> CoreExpr -> [Id] -> DataCon -> CoreExpr -> CoreExpr
+-- (mkUnpackCase x e args Con body)
+--     returns
+-- case (e `cast` ...) of bndr { Con args -> body }
+-- 
+-- the type of the bndr passed in is irrelevent
+mkUnpackCase bndr arg unpk_args boxing_con body
+  = Case cast_arg (setIdType bndr bndr_ty) (exprType body) [(DataAlt boxing_con, unpk_args, body)]
+  where
+  (cast_arg, bndr_ty) = go (idType bndr) arg
+  go ty arg 
+    | (tycon, tycon_args, _, _)  <- splitProductType "mkUnpackCase" ty
+    , isNewTyCon tycon && not (isRecursiveTyCon tycon)
+    = go (newTyConInstRhs tycon tycon_args) 
+         (unwrapNewTypeBody tycon tycon_args arg)
+    | otherwise = (arg, ty)
+
+-- ...and the dual
+reboxProduct :: [Unique]     -- uniques to create new local binders
+             -> Type         -- type of product to box
+             -> ([Unique],   -- remaining uniques
+                 CoreExpr,   -- boxed product
+                 [Id])       -- Ids being boxed into product
+reboxProduct us ty
+  = let 
+       (_tycon, _tycon_args, _pack_con, con_arg_tys) = deepSplitProductType "reboxProduct" ty
+        us' = dropList con_arg_tys us
+
+       arg_ids  = zipWith (mkSysLocal FSLIT("rb")) us con_arg_tys
+
+        bind_rhs = mkProductBox arg_ids ty
 
 
-       the_arg_id  = assoc "mkRecordSelId:mk_alt" (field_lbls `zip` arg_ids) field_label
-       field_lbls  = dataConFieldLabels data_con
+    in
+      (us', bind_rhs, arg_ids)
+
+mkProductBox :: [Id] -> Type -> CoreExpr
+mkProductBox arg_ids ty 
+  = result_expr
+  where 
+    (tycon, tycon_args, pack_con, _con_arg_tys) = splitProductType "mkProductBox" ty
 
 
-    error_expr = mkRuntimeErrorApp rEC_SEL_ERROR_ID field_tau full_msg
-    full_msg   = showSDoc (sep [text "No match in record selector", ppr sel_id]) 
+    result_expr
+      | isNewTyCon tycon && not (isRecursiveTyCon tycon) 
+      = wrap (mkProductBox arg_ids (newTyConInstRhs tycon tycon_args))
+      | otherwise = mkConApp pack_con (map Type tycon_args ++ map Var arg_ids)
+
+    wrap expr = wrapNewTypeBody tycon tycon_args expr
 
 
 -- (mkReboxingAlt us con xs rhs) basically constructs the case
 
 
 -- (mkReboxingAlt us con xs rhs) basically constructs the case
@@ -590,7 +747,7 @@ mkReboxingAlt us con args rhs
   where
     stricts = dataConExStricts con ++ dataConStrictMarks con
 
   where
     stricts = dataConExStricts con ++ dataConStrictMarks con
 
-    go [] stricts us = ([], [])
+    go [] _stricts _us = ([], [])
 
        -- Type variable case
     go (arg:args) stricts us 
 
        -- Type variable case
     go (arg:args) stricts us 
@@ -601,16 +758,11 @@ mkReboxingAlt us con args rhs
        -- Term variable case
     go (arg:args) (str:stricts) us
       | isMarkedUnboxed str
        -- Term variable case
     go (arg:args) (str:stricts) us
       | isMarkedUnboxed str
-      = let
-         (_, tycon_args, pack_con, con_arg_tys)
-                = splitProductType "mkReboxingAlt" (idType arg)
-
-         unpacked_args  = zipWith (mkSysLocal FSLIT("rb")) us con_arg_tys
-         (binds, args') = go args stricts (dropList con_arg_tys us)
-         con_app        = mkConApp pack_con (map Type tycon_args ++ map Var unpacked_args)
-       in
-       (NonRec arg con_app : binds, unpacked_args ++ args')
-
+      = 
+        let (binds, unpacked_args')        = go args stricts us'
+            (us', bind_rhs, unpacked_args) = reboxProduct us (idType arg)
+        in
+            (NonRec arg bind_rhs : binds, unpacked_args ++ unpacked_args')
       | otherwise
       = let (binds, args') = go args stricts us
         in  (binds, arg:args')
       | otherwise
       = let (binds, args') = go args stricts us
         in  (binds, arg:args')
@@ -672,26 +824,59 @@ mkDictSelId name clas
 
     tycon      = classTyCon clas
     [data_con] = tyConDataCons tycon
 
     tycon      = classTyCon clas
     [data_con] = tyConDataCons tycon
-    tyvars     = dataConTyVars data_con
-    arg_tys    = dataConRepArgTys data_con
+    tyvars     = dataConUnivTyVars data_con
+    arg_tys    = ASSERT( isVanillaDataCon data_con ) dataConRepArgTys data_con
     the_arg_id = assoc "MkId.mkDictSelId" (map idName (classSelIds clas) `zip` arg_ids) name
 
     pred             = mkClassPred clas (mkTyVarTys tyvars)
     (dict_id:arg_ids) = mkTemplateLocals (mkPredTy pred : arg_tys)
 
     the_arg_id = assoc "MkId.mkDictSelId" (map idName (classSelIds clas) `zip` arg_ids) name
 
     pred             = mkClassPred clas (mkTyVarTys tyvars)
     (dict_id:arg_ids) = mkTemplateLocals (mkPredTy pred : arg_tys)
 
-    rhs | isNewTyCon tycon = mkLams tyvars $ Lam dict_id $ 
-                            mkNewTypeBody tycon (head arg_tys) (Var dict_id)
-       | otherwise        = mkLams tyvars $ Lam dict_id $
-                            Case (Var dict_id) dict_id (idType the_arg_id)
-                                 [(DataAlt data_con, arg_ids, Var the_arg_id)]
-
-mkNewTypeBody tycon result_ty result_expr
-       -- Adds a coerce where necessary
-       -- Used for both wrapping and unwrapping
-  | isRecursiveTyCon tycon     -- Recursive case; use a coerce
-  = Note (Coerce result_ty (exprType result_expr)) result_expr
-  | otherwise                  -- Normal case
+    rhs = mkLams tyvars (Lam dict_id rhs_body)
+    rhs_body | isNewTyCon tycon = unwrapNewTypeBody tycon (map mkTyVarTy tyvars) (Var dict_id)
+            | otherwise        = Case (Var dict_id) dict_id (idType the_arg_id)
+                                      [(DataAlt data_con, arg_ids, Var the_arg_id)]
+
+wrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
+-- The wrapper for the data constructor for a newtype looks like this:
+--     newtype T a = MkT (a,Int)
+--     MkT :: forall a. (a,Int) -> T a
+--     MkT = /\a. \(x:(a,Int)). x `cast` sym (CoT a)
+-- where CoT is the coercion TyCon assoicated with the newtype
+--
+-- The call (wrapNewTypeBody T [a] e) returns the
+-- body of the wrapper, namely
+--     e `cast` (CoT [a])
+--
+-- If a coercion constructor is prodivided in the newtype, then we use
+-- it, otherwise the wrap/unwrap are both no-ops 
+--
+-- If the we are dealing with a newtype instance, we have a second coercion
+-- identifying the family instance with the constructor of the newtype
+-- instance.  This coercion is applied in any case (ie, composed with the
+-- coercion constructor of the newtype or applied by itself).
+--
+wrapNewTypeBody tycon args result_expr
+  = wrapFamInstBody tycon args inner
+  where
+    inner
+      | Just co_con <- newTyConCo_maybe tycon
+      = mkCoerce (mkSymCoercion (mkTyConApp co_con args)) result_expr
+      | otherwise
+      = result_expr
+
+-- When unwrapping, we do *not* apply any family coercion, because this will
+-- be done via a CoPat by the type checker.  We have to do it this way as
+-- computing the right type arguments for the coercion requires more than just
+-- a spliting operation (cf, TcPat.tcConPat).
+--
+unwrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
+unwrapNewTypeBody tycon args result_expr
+  | Just co_con <- newTyConCo_maybe tycon
+  = mkCoerce (mkTyConApp co_con args) result_expr
+  | otherwise
   = result_expr
   = result_expr
+
+
 \end{code}
 
 
 \end{code}
 
 
@@ -710,7 +895,7 @@ mkPrimOpId prim_op
     ty   = mkForAllTys tyvars (mkFunTys arg_tys res_ty)
     name = mkWiredInName gHC_PRIM (primOpOcc prim_op) 
                         (mkPrimOpIdUnique (primOpTag prim_op))
     ty   = mkForAllTys tyvars (mkFunTys arg_tys res_ty)
     name = mkWiredInName gHC_PRIM (primOpOcc prim_op) 
                         (mkPrimOpIdUnique (primOpTag prim_op))
-                        Nothing (AnId id) UserSyntax
+                        (AnId id) UserSyntax
     id   = mkGlobalId (PrimOpId prim_op) name ty info
                
     info = noCafIdInfo
     id   = mkGlobalId (PrimOpId prim_op) name ty info
                
     info = noCafIdInfo
@@ -849,7 +1034,7 @@ another gun with which to shoot yourself in the foot.
 
 \begin{code}
 mkWiredInIdName mod fs uniq id
 
 \begin{code}
 mkWiredInIdName mod fs uniq id
- = mkWiredInName mod (mkOccNameFS varName fs) uniq Nothing (AnId id) UserSyntax
+ = mkWiredInName mod (mkOccNameFS varName fs) uniq (AnId id) UserSyntax
 
 unsafeCoerceName = mkWiredInIdName gHC_PRIM FSLIT("unsafeCoerce#") unsafeCoerceIdKey  unsafeCoerceId
 nullAddrName     = mkWiredInIdName gHC_PRIM FSLIT("nullAddr#")    nullAddrIdKey      nullAddrId
 
 unsafeCoerceName = mkWiredInIdName gHC_PRIM FSLIT("unsafeCoerce#") unsafeCoerceIdKey  unsafeCoerceId
 nullAddrName     = mkWiredInIdName gHC_PRIM FSLIT("nullAddr#")    nullAddrIdKey      nullAddrId
@@ -882,7 +1067,8 @@ unsafeCoerceId
                      (mkFunTy openAlphaTy openBetaTy)
     [x] = mkTemplateLocals [openAlphaTy]
     rhs = mkLams [openAlphaTyVar,openBetaTyVar,x] $
                      (mkFunTy openAlphaTy openBetaTy)
     [x] = mkTemplateLocals [openAlphaTy]
     rhs = mkLams [openAlphaTyVar,openBetaTyVar,x] $
-         Note (Coerce openBetaTy openAlphaTy) (Var x)
+--       Note (Coerce openBetaTy openAlphaTy) (Var x)
+         Cast (Var x) (mkUnsafeCoercion openAlphaTy openBetaTy)
 
 -- nullAddr# :: Addr#
 -- The reason is is here is because we don't provide 
 
 -- nullAddr# :: Addr#
 -- The reason is is here is because we don't provide