Add {-# OPTIONS_GHC -w #-} and some blurb to all compiler modules
[ghc-hetmet.git] / compiler / basicTypes / MkId.lhs
index 8df6aa7..76fd6e4 100644 (file)
@@ -1,7 +1,7 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The AQUA Project, Glasgow University, 1998
 %
-\section[StdIdInfo]{Standard unfoldings}
 
 This module contains definitions for the IdInfo for things that
 have a standard form, namely:
@@ -12,15 +12,23 @@ have a standard form, namely:
        * primitive operations
 
 \begin{code}
+{-# OPTIONS_GHC -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+--     http://hackage.haskell.org/trac/ghc/wiki/WorkingConventions#Warnings
+-- for details
+
 module MkId (
        mkDictFunId, mkDefaultMethodId,
        mkDictSelId, 
 
        mkDataConIds,
        mkRecordSelId, 
-       mkPrimOpId, mkFCallId,
+       mkPrimOpId, mkFCallId, mkTickBoxOpId, mkBreakPointOpId,
 
        mkReboxingAlt, wrapNewTypeBody, unwrapNewTypeBody,
+        wrapFamInstBody, unwrapFamInstScrut,
         mkUnpackCase, mkProductBox,
 
        -- And some particular Ids; see below for why they are wired in
@@ -38,70 +46,42 @@ module MkId (
 
 #include "HsVersions.h"
 
-
-import BasicTypes      ( Arity, StrictnessMark(..), isMarkedUnboxed, isMarkedStrict )
-import Rules           ( mkSpecInfo )
-import TysPrim         ( openAlphaTyVars, alphaTyVar, alphaTy, 
-                         realWorldStatePrimTy, addrPrimTy
-                       )
-import TysWiredIn      ( charTy, mkListTy )
-import PrelRules       ( primOpRules )
-import Type            ( TyThing(..), mkForAllTy, tyVarsOfTypes, newTyConInstRhs, coreEqType,
-                          PredType(..),
-                         mkTopTvSubst, substTyVar )
-import TcGadt           ( gadtRefine, refineType, emptyRefinement )
-import HsBinds          ( ExprCoFn(..), isIdCoercion )
-import Coercion         ( mkSymCoercion, mkUnsafeCoercion, 
-                          splitNewTypeRepCo_maybe, isEqPred )
-import TcType          ( Type, ThetaType, mkDictTy, mkPredTys, mkPredTy, 
-                         mkTyConApp, mkTyVarTys, mkClassPred, 
-                         mkFunTys, mkFunTy, mkSigmaTy, tcSplitSigmaTy, 
-                         isUnLiftedType, mkForAllTys, mkTyVarTy, tyVarsOfType,
-                         tcSplitFunTys, tcSplitForAllTys, dataConsStupidTheta
-                       )
-import CoreUtils       ( exprType, dataConOrigInstPat )
-import CoreUnfold      ( mkTopUnfolding, mkCompulsoryUnfolding )
-import Literal         ( nullAddrLit, mkStringLit )
-import TyCon           ( TyCon, isNewTyCon, tyConDataCons, FieldLabel,
-                          tyConStupidTheta, isProductTyCon, isDataTyCon, isRecursiveTyCon,
-                          newTyConCo, tyConArity )
-import Class           ( Class, classTyCon, classSelIds )
-import Var             ( Id, TyVar, Var, setIdType, mkCoVar, mkWildCoVar )
-import VarSet          ( isEmptyVarSet, subVarSet, varSetElems )
-import Name            ( mkFCallName, mkWiredInName, Name, BuiltInSyntax(..),
-                          mkSysTvName )
-import OccName         ( mkOccNameFS, varName )
-import PrimOp          ( PrimOp, primOpSig, primOpOcc, primOpTag )
-import ForeignCall     ( ForeignCall )
-import DataCon         ( DataCon, DataConIds(..), dataConTyCon, dataConUnivTyVars,
-                         dataConFieldLabels, dataConRepArity, dataConResTys,
-                         dataConRepArgTys, dataConRepType, dataConFullSig,
-                         dataConSig, dataConStrictMarks, dataConExStricts, 
-                         splitProductType, isVanillaDataCon, dataConFieldType,
-                         dataConInstOrigArgTys, deepSplitProductType
-                       )
-import Id              ( idType, mkGlobalId, mkVanillaGlobal, mkSysLocal, 
-                         mkTemplateLocals, mkTemplateLocalsNum, mkExportedLocalId,
-                         mkTemplateLocal, idName, mkWildId
-                       )
-import IdInfo          ( IdInfo, noCafIdInfo,  setUnfoldingInfo, 
-                         setArityInfo, setSpecInfo, setCafInfo,
-                         setAllStrictnessInfo, vanillaIdInfo,
-                         GlobalIdDetails(..), CafInfo(..)
-                       )
-import NewDemand       ( mkStrictSig, DmdResult(..),
-                         mkTopDmdType, topDmd, evalDmd, lazyDmd, retCPR,
-                         Demand(..), Demands(..) )
-import DmdAnal         ( dmdAnalTopRhs )
+import Rules
+import TysPrim
+import TysWiredIn
+import PrelRules
+import Type
+import TypeRep
+import TcGadt
+import Coercion
+import TcType
+import CoreUtils
+import CoreUnfold
+import Literal
+import TyCon
+import Class
+import VarSet
+import Name
+import OccName
+import PrimOp
+import ForeignCall
+import DataCon
+import Id
+import Var              ( Var, TyVar, mkCoVar)
+import IdInfo
+import NewDemand
+import DmdAnal
 import CoreSyn
-import Unique          ( mkBuiltinUnique, mkPrimOpIdUnique )
+import Unique
 import Maybes
 import PrelNames
-import Util             ( dropList, isSingleton )
+import BasicTypes       hiding ( SuccessFlag(..) )
+import Util
 import Outputable
 import FastString
-import ListSetOps      ( assoc, minusList )
-\end{code}             
+import ListSetOps
+import Module
+\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -190,36 +170,69 @@ Notice that
   Making an explicit case expression allows the simplifier to eliminate
   it in the (common) case where the constructor arg is already evaluated.
 
+Note [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). A coercion allows you to move between
+representation and family type.  It is accessible from :R123Map via
+tyConFamilyCoercion_maybe and has kind
+
+  Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
+
+The wrapper and worker of MapPair get the types
+
+       -- Wrapper
+  $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
+  $WMapPair a b v = MapPair a b v `cast` sym (Co123Map a b v)
+
+       -- Worker
+  MapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
+
+This coercion is conditionally applied by wrapFamInstBody.
+
+It's a bit more complicated if the data instance is a GADT as well!
+
+   data instance T [a] where
+       T1 :: forall b. b -> T [Maybe b]
+Hence
+   Co7T a :: T [a] ~ :R7T a
+
+Now we want
+
+       -- Wrapper
+  $WT1 :: forall b. b -> T [Maybe b]
+  $WT1 b v = T1 (Maybe b) b (Maybe b) v
+                       `cast` sym (Co7T (Maybe b))
+
+       -- Worker
+  T1 :: forall c b. (c ~ Maybe b) => b -> :R7T c
 
 \begin{code}
 mkDataConIds :: Name -> Name -> DataCon -> DataConIds
 mkDataConIds wrap_name wkr_name data_con
-  | isNewTyCon tycon
-  = NewDC nt_wrap_id
+  | isNewTyCon tycon                   -- Newtype, only has a worker
+  = DCIds Nothing nt_work_id                 
 
-  | any isMarkedStrict all_strict_marks                -- Algebraic, needs wrapper
-    || not (null eq_spec)
-  = 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
-    (univ_tvs, ex_tvs, eq_spec, theta, orig_arg_tys) = dataConFullSig data_con
-    tycon = dataConTyCon data_con
-
-       ----------- 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.
-    wrap_tvs = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs
-    subst         = mkTopTvSubst eq_spec
-    dict_tys       = mkPredTys theta
-    result_ty_args = map (substTyVar subst) univ_tvs
-    result_ty      = mkTyConApp tycon result_ty_args
-    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
+    (univ_tvs, ex_tvs, eq_spec, 
+     eq_theta, dict_theta, orig_arg_tys, res_ty) = dataConFullSig data_con
+    tycon = dataConTyCon data_con      -- The representation TyCon (not family)
 
        ----------- Worker (algebraic data types only) --------------
        -- The *worker* for the data constructor is the function that
@@ -235,6 +248,7 @@ mkDataConIds wrap_name wkr_name data_con
                                                        -- even if arity = 0
 
     wkr_sig = mkStrictSig (mkTopDmdType (replicate wkr_arity topDmd) cpr_info)
+       --      Note [Data-con worker strictness]
        -- Notice that we do *not* say the worker is strict
        -- even if the data constructor is declared strict
        --      e.g.    data T = MkT !(Int,Int)
@@ -259,29 +273,49 @@ 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
 
-       ----------- 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 &&
-                          isSingleton orig_arg_tys )
+    newtype_unf  = -- The assertion below is no longer correct:
+                  --   there may be a dict theta rather than a singleton orig_arg_ty
+                  -- ASSERT( isVanillaDataCon data_con &&
+                  --      isSingleton orig_arg_tys )
+                  --
                   -- No existentials on a newtype, but it can have a context
                   -- e.g.      newtype Eq a => T a = MkT (...)
                   mkCompulsoryUnfolding $ 
                   mkLams wrap_tvs $ Lam id_arg1 $ 
-                  wrapNewTypeBody tycon result_ty_args
+                  wrapNewTypeBody tycon res_ty_args
                        (Var id_arg1)
 
-    id_arg1 = mkTemplateLocal 1 (head orig_arg_tys)
+    id_arg1 = mkTemplateLocal 1 
+               (if null orig_arg_tys
+                   then ASSERT(not (null $ dataConDictTheta data_con)) mkPredTy $ head (dataConDictTheta data_con)
+                   else head orig_arg_tys
+               )
+
+       ----------- 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.
+    wrap_tvs    = (univ_tvs `minusList` map fst eq_spec) ++ ex_tvs
+    res_ty_args        = substTyVars (mkTopTvSubst eq_spec) univ_tvs
+    eq_tys   = mkPredTys eq_theta
+    dict_tys = mkPredTys dict_theta
+    wrap_ty  = mkForAllTys wrap_tvs $ mkFunTys eq_tys $ mkFunTys dict_tys $
+              mkFunTys orig_arg_tys $ res_ty
+       -- NB: watch out here if you allow user-written equality 
+       --     constraints in data constructor signatures
 
        ----------- Wrappers for algebraic data types -------------- 
     alg_wrap_id = mkGlobalId (DataConWrapId data_con) wrap_name wrap_ty alg_wrap_info
     alg_wrap_info = noCafIdInfo                -- The NoCaf-ness is set by noCafIdInfo
-                   `setArityInfo`         alg_arity
+                   `setArityInfo`         wrap_arity
                        -- It's important to specify the arity, so that partial
                        -- applications are treated as values
-                   `setUnfoldingInfo`     alg_unf
+                   `setUnfoldingInfo`     wrap_unf
                    `setAllStrictnessInfo` Just wrap_sig
 
     all_strict_marks = dataConExStricts data_con ++ dataConStrictMarks data_con
@@ -298,21 +332,30 @@ mkDataConIds wrap_name wkr_name data_con
        --      ...(let w = C x in ...(w p q)...)...
        -- we want to see that w is strict in its two arguments
 
-    alg_unf = mkTopUnfolding $ Note InlineMe $
+    wrap_unf = mkTopUnfolding $ Note InlineMe $
              mkLams wrap_tvs $ 
+             mkLams eq_args $
              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 = 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 res_ty_args $
+                         Var wrk_id `mkTyApps`  res_ty_args
+                                    `mkVarApps` ex_tvs                 
+                                    `mkTyApps`  map snd eq_spec        -- Equality evidence 
+                                    `mkVarApps` eq_args
+                                    `mkVarApps` reverse rep_ids
 
     (dict_args,i2) = mkLocals 1  dict_tys
     (id_args,i3)   = mkLocals i2 orig_arg_tys
-    alg_arity     = i3-1
+    wrap_arity    = i3-1
+    (eq_args,_)    = mkCoVarLocals i3 eq_tys
+
+    mkCoVarLocals i []     = ([],i)
+    mkCoVarLocals i (x:xs) = let (ys,j) = mkCoVarLocals (i+1) xs
+                                 y      = mkCoVar (mkSysTvName (mkBuiltinUnique i) FSLIT("dc_co")) x
+                             in (y:ys,j)
 
     mk_case 
           :: (Id, StrictnessMark)      -- Arg, strictness
@@ -326,10 +369,10 @@ mkDataConIds wrap_name wkr_name data_con
                MarkedStrict 
                   | isUnLiftedType (idType arg) -> body i (arg:rep_args)
                   | otherwise ->
-                       Case (Var arg) arg result_ty [(DEFAULT,[], body i (arg:rep_args))]
+                       Case (Var arg) arg res_ty [(DEFAULT,[], body i (arg:rep_args))]
 
                MarkedUnboxed
-                  -> unboxProduct i (Var arg) (idType arg) the_body result_ty
+                  -> unboxProduct i (Var arg) (idType arg) the_body 
                       where
                         the_body i con_args = body i (reverse con_args ++ rep_args)
 
@@ -427,23 +470,42 @@ Note the forall'd tyvars of the selector are just the free tyvars
 of the result type; there may be other tyvars in the constructor's
 type (e.g. 'b' in T2).
 
-\begin{code}
+Note [Selector running example]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's OK to combine GADTs and type families.  Here's a running example:
+
+       data instance T [a] where 
+         T1 { fld :: b } :: T [Maybe b]
+
+The representation type looks like this
+       data :R7T a where
+         T1 { fld :: b } :: :R7T (Maybe b)
+
+and there's coercion from the family type to the representation type
+       :CoR7T a :: T [a] ~ :R7T a
 
--- Steps for handling "naughty" vs "non-naughty" selectors:
---  1. Determine naughtiness by comparing field type vs result type
---  2. Install naughty ones with selector_ty of type _|_ and fill in mzero for info
---  3. If it's not naughty, do the normal plan.
+The selector we want for fld looks like this:
 
+       fld :: forall b. T [Maybe b] -> b
+       fld = /\b. \(d::T [Maybe b]).
+             case d `cast` :CoR7T (Maybe b) of 
+               T1 (x::b) -> x
+
+The scrutinee of the case has type :R7T (Maybe b), which can be
+gotten by appying the eq_spec to the univ_tvs of the data con.
+
+\begin{code}
 mkRecordSelId :: TyCon -> FieldLabel -> Id
 mkRecordSelId tycon field_label
        -- Assumes that all fields with the same field label have the same type
   | is_naughty = naughty_id
   | otherwise  = sel_id
   where
-    is_naughty = not (tyVarsOfType field_ty `subVarSet` res_tv_set)
-    sel_id_details = RecordSelId tycon field_label is_naughty
+    is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tv_set)
+    sel_id_details = RecordSelId { sel_tycon = tycon, sel_label = field_label, sel_naughty = is_naughty }
+       -- For a data type family, the tycon is the *instance* TyCon
 
-    -- Escapist case here for naughty construcotrs
+    -- Escapist case here for naughty constructors
     -- We give it no IdInfo, and a type of forall a.a (never looked at)
     naughty_id = mkGlobalId sel_id_details field_label forall_a_a noCafIdInfo
     forall_a_a = mkForAllTy alphaTyVar (mkTyVarTy alphaTyVar)
@@ -454,11 +516,12 @@ mkRecordSelId tycon field_label
     data_cons_w_field = filter has_field data_cons     -- Can't be empty!
     has_field con     = field_label `elem` dataConFieldLabels con
 
-    con1       = head data_cons_w_field
-    res_tys    = dataConResTys con1
-    res_tv_set = tyVarsOfTypes res_tys
-    res_tvs    = varSetElems res_tv_set
-    data_ty    = mkTyConApp tycon res_tys
+    con1       = ASSERT( not (null data_cons_w_field) ) head data_cons_w_field
+    (univ_tvs, _, eq_spec, _, _, _, data_ty) = dataConFullSig con1
+       -- For a data type family, the data_ty (and hence selector_ty) mentions
+       -- only the family TyCon, not the instance TyCon
+    data_tv_set        = tyVarsOfType data_ty
+    data_tvs   = varSetElems data_tv_set
     field_ty   = dataConFieldType con1 field_label
     
        -- *Very* tiresomely, the selectors are (unnecessarily!) overloaded over
@@ -473,10 +536,9 @@ mkRecordSelId tycon field_label
     n_stupid_dicts  = length stupid_dict_tys
 
     (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
+    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 
        -- be a bit careful.  Suppose we have
        --      data R = R { op :: forall a. Foo a => a -> a }
@@ -493,7 +555,7 @@ mkRecordSelId tycon field_label
        --      op (R op) = op
 
     selector_ty :: Type
-    selector_ty  = mkForAllTys res_tvs $ mkForAllTys field_tyvars $
+    selector_ty  = mkForAllTys data_tvs $ mkForAllTys field_tyvars $
                   mkFunTys stupid_dict_tys  $  mkFunTys field_dict_tys $
                   mkFunTy data_ty field_tau
       
@@ -520,7 +582,8 @@ mkRecordSelId tycon field_label
     field_dict_ids   = mkTemplateLocalsNum field_dict_base field_dict_tys
     dict_id_base     = field_dict_base + n_field_dict_tys
     data_id         = mkTemplateLocal dict_id_base data_ty
-    arg_base        = dict_id_base + 1
+    scrut_id        = mkTemplateLocal (dict_id_base+1) scrut_ty
+    arg_base        = dict_id_base + 2
 
     the_alts :: [CoreAlt]
     the_alts   = map mk_alt data_cons_w_field  -- Already sorted by data-con
@@ -533,14 +596,19 @@ mkRecordSelId tycon field_label
     caf_info    | no_default = NoCafRefs
                | otherwise  = MayHaveCafRefs
 
-    sel_rhs = mkLams res_tvs $ mkLams field_tyvars $ 
+    sel_rhs = mkLams data_tvs $ mkLams field_tyvars $ 
              mkLams stupid_dict_ids $ mkLams field_dict_ids $
-             Lam data_id     $ mk_result sel_body
+             Lam data_id $ mk_result sel_body
+
+    scrut_ty_args = substTyVars (mkTopTvSubst eq_spec) univ_tvs
+    scrut_ty     = mkTyConApp tycon scrut_ty_args
+    scrut = unwrapFamInstScrut tycon scrut_ty_args (Var data_id)
+       -- First coerce from the type family to the representation type
 
        -- 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)
+       --     data_tys will simply be the dataConUnivTyVars
+    sel_body | isNewTyCon tycon = unwrapNewTypeBody tycon scrut_ty_args scrut
+            | otherwise        = Case scrut scrut_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 
@@ -551,50 +619,37 @@ mkRecordSelId tycon field_label
        --      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) rhs
+      =   ASSERT2( data_ty `tcEqType` field_ty, ppr data_con $$ ppr data_ty $$ ppr field_ty )
+         mkReboxingAlt rebox_uniqs data_con (ex_tvs ++ co_tvs ++ arg_vs) rhs
       where
-       -- TODO: this is *not* right; Orig vs Rep tys
-       (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
-          = (ex_tvs ++ co_tvs ++ dict_vs, field_vs)
-
-        (ex_tvs, co_tvs, arg_vs) = dataConOrigInstPat uniqs' data_con res_tys
-        (dict_vs, field_vs) = splitAt (length dc_theta) arg_vs
+           -- get pattern binders with types appropriately instantiated
+       arg_uniqs = map mkBuiltinUnique [arg_base..]
+        (ex_tvs, co_tvs, arg_vs) = dataConOrigInstPat arg_uniqs data_con scrut_ty_args
 
-       (_, pre_dc_theta, dc_arg_tys) = dataConSig data_con
-        dc_theta  = filter (not . isEqPred) pre_dc_theta
+       rebox_base  = arg_base + length ex_tvs + length co_tvs + length arg_vs
+       rebox_uniqs = map mkBuiltinUnique [rebox_base..]
 
-       arg_base' = arg_base + length dc_theta
+       -- 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))
 
-       unpack_base = arg_base' + length dc_arg_tys
-
-       uniq_list = map mkBuiltinUnique [unpack_base..]
 
+               -- Generate the refinement for b'=b, 
+               -- and apply to (Maybe b'), to get (Maybe b)
         Succeeded refinement = gadtRefine emptyRefinement ex_tvs co_tvs
-        (co_fn, _)      = refineType refinement (idType the_arg_id)
-
-        rhs = perform_co co_fn (Var the_arg_id)
-
-        perform_co (ExprCoFn co) expr = Cast expr co
-        perform_co id_co expr = ASSERT(isIdCoercion id_co) expr
-
-          -- split the uniq_list into two
-        uniqs  = takeHalf uniq_list
-        uniqs' = takeHalf (drop 1 uniq_list)
+       the_arg_id_ty = idType the_arg_id
+        (rhs, data_ty) = case refineType refinement the_arg_id_ty of
+                         Just (co, data_ty) -> (Cast (Var the_arg_id) co, data_ty)
+                         Nothing            -> (Var the_arg_id, the_arg_id_ty)
 
-        takeHalf [] = []
-        takeHalf (h:_:t) = h:(takeHalf t)  
-        takeHalf (h:t) = [h]
-
-       the_arg_id  = assoc "mkRecordSelId:mk_alt" (field_lbls `zip` arg_ids) field_label
+       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
 
-    error_expr = mkRuntimeErrorApp rEC_SEL_ERROR_ID field_tau full_msg
+    error_expr = mkRuntimeErrorApp rEC_SEL_ERROR_ID field_ty full_msg
     full_msg   = showSDoc (sep [text "No match in record selector", ppr sel_id])
 
 -- unbox a product type...
@@ -608,32 +663,32 @@ mkRecordSelId tycon field_label
 -- 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` (sym CoT)) `cast` (sym CoS) of
+--   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) -> Type -> CoreExpr
-unboxProduct i arg arg_ty body res_ty
+unboxProduct :: Int -> CoreExpr -> Type -> (Int -> [Id] -> CoreExpr) -> CoreExpr
+unboxProduct i arg arg_ty body
   = result
   where 
-    result = mkUnpackCase the_id arg arg_ty con_args boxing_con rhs
-    (tycon, tycon_args, boxing_con, tys) = deepSplitProductType "unboxProduct" arg_ty
+    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 -> Type -> [Id] -> DataCon -> CoreExpr -> CoreExpr
+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 arg_ty unpk_args boxing_con body
+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 
-    | res@(tycon, tycon_args, _, _)  <- splitProductType "mkUnpackCase" ty
+    | (tycon, tycon_args, _, _)  <- splitProductType "mkUnpackCase" ty
     , isNewTyCon tycon && not (isRecursiveTyCon tycon)
     = go (newTyConInstRhs tycon tycon_args) 
          (unwrapNewTypeBody tycon tycon_args arg)
@@ -647,7 +702,7 @@ reboxProduct :: [Unique]     -- uniques to create new local binders
                  [Id])       -- Ids being boxed into product
 reboxProduct us ty
   = let 
-       (tycon, tycon_args, pack_con, con_arg_tys) = deepSplitProductType "reboxProduct" ty
+       (_tycon, _tycon_args, _pack_con, con_arg_tys) = deepSplitProductType "reboxProduct" ty
  
         us' = dropList con_arg_tys us
 
@@ -662,7 +717,7 @@ mkProductBox :: [Id] -> Type -> CoreExpr
 mkProductBox arg_ids ty 
   = result_expr
   where 
-    (tycon, tycon_args, pack_con, con_arg_tys) = splitProductType "mkProductBox" ty
+    (tycon, tycon_args, pack_con, _con_arg_tys) = splitProductType "mkProductBox" ty
 
     result_expr
       | isNewTyCon tycon && not (isRecursiveTyCon tycon) 
@@ -705,7 +760,7 @@ mkReboxingAlt us con args rhs
   where
     stricts = dataConExStricts con ++ dataConStrictMarks con
 
-    go [] stricts us = ([], [])
+    go [] _stricts _us = ([], [])
 
        -- Type variable case
     go (arg:args) stricts us 
@@ -761,7 +816,7 @@ mkDictSelId name clas
        --      C a -> C a
        -- for a single-op class (after all, the selector is the identity)
        -- But it's type must expose the representation of the dictionary
-       -- to gat (say)         C a -> (a -> a)
+       -- to get (say)         C a -> (a -> a)
 
     info = noCafIdInfo
                `setArityInfo`          1
@@ -783,45 +838,92 @@ mkDictSelId name clas
     tycon      = classTyCon clas
     [data_con] = tyConDataCons tycon
     tyvars     = dataConUnivTyVars data_con
-    arg_tys    = ASSERT( isVanillaDataCon data_con ) dataConRepArgTys data_con
+    arg_tys    = {- ASSERT( isVanillaDataCon data_con ) -} dataConRepArgTys data_con
+    eq_theta   = dataConEqTheta        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)
+    pred       = mkClassPred clas (mkTyVarTys tyvars)
+    dict_id    = mkTemplateLocal     1 $ mkPredTy pred
+    (eq_ids,n) = mkCoVarLocals 2 $ mkPredTys eq_theta
+    arg_ids    = mkTemplateLocalsNum n arg_tys
+
+    mkCoVarLocals i []     = ([],i)
+    mkCoVarLocals i (x:xs) = let (ys,j) = mkCoVarLocals (i+1) xs
+                                 y      = mkCoVar (mkSysTvName (mkBuiltinUnique i) FSLIT("dc_co")) x
+                             in (y:ys,j)
 
-    rhs = mkLams tyvars (Lam dict_id rhs_body)
+    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)]
+                                      [(DataAlt data_con, eq_ids ++ arg_ids, Var the_arg_id)]
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+       Wrapping and unwrapping newtypes and type families
+%*                                                                     *
+%************************************************************************
 
+\begin{code}
 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` CoT 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]
+--     e `cast` (CoT [a])
 --
--- If a coercion constructor is prodivided in the newtype, then we use
+-- If a coercion constructor is provided 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
-  | Just co_con <- newTyConCo tycon
-  = Cast result_expr (mkTyConApp co_con args)
-  | otherwise
-  = 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 tycon
-  = Cast result_expr (mkSymCoercion (mkTyConApp co_con args))
+  | Just co_con <- newTyConCo_maybe tycon
+  = mkCoerce (mkTyConApp co_con args) result_expr
   | otherwise
   = result_expr
 
+-- 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.
+-- See Note [Wrappers for data instance tycons]
+wrapFamInstBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
+wrapFamInstBody tycon args body
+  | Just co_con <- tyConFamilyCoercion_maybe tycon
+  = mkCoerce (mkSymCoercion (mkTyConApp co_con args)) body
+  | otherwise
+  = body
 
+unwrapFamInstScrut :: TyCon -> [Type] -> CoreExpr -> CoreExpr
+unwrapFamInstScrut tycon args scrut
+  | Just co_con <- tyConFamilyCoercion_maybe tycon
+  = mkCoerce (mkTyConApp co_con args) scrut
+  | otherwise
+  = scrut
 \end{code}
 
 
@@ -840,7 +942,7 @@ mkPrimOpId 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
@@ -878,6 +980,29 @@ mkFCallId uniq fcall ty
     (arg_tys, _) = tcSplitFunTys tau
     arity       = length arg_tys
     strict_sig   = mkStrictSig (mkTopDmdType (replicate arity evalDmd) TopRes)
+
+-- Tick boxes and breakpoints are both represented as TickBoxOpIds,
+-- except for the type:
+--
+--    a plain HPC tick box has type (State# RealWorld)
+--    a breakpoint Id has type forall a.a
+--
+-- The breakpoint Id will be applied to a list of arbitrary free variables,
+-- which is why it needs a polymorphic type.
+
+mkTickBoxOpId :: Unique -> Module -> TickBoxId -> Id
+mkTickBoxOpId uniq mod ix = mkTickBox' uniq mod ix realWorldStatePrimTy
+
+mkBreakPointOpId :: Unique -> Module -> TickBoxId -> Id
+mkBreakPointOpId uniq mod ix = mkTickBox' uniq mod ix ty
+ where ty = mkSigmaTy [openAlphaTyVar] [] openAlphaTy
+
+mkTickBox' uniq mod ix ty = mkGlobalId (TickBoxOpId tickbox) name ty info    
+  where
+    tickbox = TickBox mod ix
+    occ_str = showSDoc (braces (ppr tickbox))
+    name    = mkTickBoxOpName uniq occ_str
+    info    = noCafIdInfo
 \end{code}
 
 
@@ -979,7 +1104,7 @@ another gun with which to shoot yourself in the foot.
 
 \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
@@ -1012,8 +1137,7 @@ unsafeCoerceId
                      (mkFunTy openAlphaTy openBetaTy)
     [x] = mkTemplateLocals [openAlphaTy]
     rhs = mkLams [openAlphaTyVar,openBetaTyVar,x] $
---       Note (Coerce openBetaTy openAlphaTy) (Var x)
-         Cast (Var x) (mkUnsafeCoercion openAlphaTy openBetaTy)
+          Cast (Var x) (mkUnsafeCoercion openAlphaTy openBetaTy)
 
 -- nullAddr# :: Addr#
 -- The reason is is here is because we don't provide 
@@ -1042,7 +1166,7 @@ seqId
 -- not from GHC.Base.hi.   This is important, because the strictness
 -- analyser will spot it as strict!
 --
--- Also no unfolding in lazyId: it gets "inlined" by a HACK in the worker/wrapper pass
+-- Also no unfolding in lazyId: it gets "inlined" by a HACK in the worker/wrapperpass
 --     (see WorkWrap.wwExpr)   
 -- We could use inline phases to do this, but that would be vulnerable to changes in 
 -- phase numbering....we must inline precisely after strictness analysis.
@@ -1171,9 +1295,5 @@ pc_bottoming_Id name ty
 
     strict_sig    = mkStrictSig (mkTopDmdType [evalDmd] BotRes)
        -- These "bottom" out, no matter what their arguments
-
-(openAlphaTyVar:openBetaTyVar:_) = openAlphaTyVars
-openAlphaTy  = mkTyVarTy openAlphaTyVar
-openBetaTy   = mkTyVarTy openBetaTyVar
 \end{code}