Extend TyCons and DataCons to represent data instance decls
[ghc-hetmet.git] / compiler / basicTypes / MkId.lhs
index 1485f48..6af89b7 100644 (file)
@@ -26,7 +26,7 @@ module MkId (
        -- 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,
@@ -46,38 +46,41 @@ import TysPrim              ( openAlphaTyVars, alphaTyVar, alphaTy,
                        )
 import TysWiredIn      ( charTy, mkListTy )
 import PrelRules       ( primOpRules )
-import Type            ( TyThing(..), mkForAllTy, tyVarsOfTypes, newTyConInstRhs )
-import Coercion         ( mkSymCoercion, mkUnsafeCoercion, 
-                          splitRecNewTypeCo_maybe )
+import Type            ( TyThing(..), mkForAllTy, tyVarsOfTypes, 
+                         newTyConInstRhs, mkTopTvSubst, substTyVar, substTy )
+import TcGadt           ( gadtRefine, refineType, emptyRefinement )
+import HsBinds          ( ExprCoFn(..), isIdCoercion )
+import Coercion         ( mkSymCoercion, mkUnsafeCoercion, isEqPred )
 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
                        )
-import CoreUtils       ( exprType )
+import CoreUtils       ( exprType, dataConOrigInstPat, mkCoerce )
 import CoreUnfold      ( mkTopUnfolding, mkCompulsoryUnfolding )
 import Literal         ( nullAddrLit, mkStringLit )
 import TyCon           ( TyCon, isNewTyCon, tyConDataCons, FieldLabel,
-                          tyConStupidTheta, isProductTyCon, isDataTyCon, isRecursiveTyCon,
-                          newTyConCo, tyConArity )
+                          tyConStupidTheta, isProductTyCon, isDataTyCon,
+                          isRecursiveTyCon, tyConFamily_maybe, newTyConCo )
 import Class           ( Class, classTyCon, classSelIds )
-import Var             ( Id, TyVar, Var )
+import Var             ( Id, TyVar, Var, setIdType )
 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 DataCon         ( DataCon, DataConIds(..), dataConTyCon, dataConUnivTyVars,
+import DataCon         ( DataCon, DataConIds(..), dataConTyCon,
+                         dataConUnivTyVars, dataConInstTys,
                          dataConFieldLabels, dataConRepArity, dataConResTys,
-                         dataConRepArgTys, dataConRepType, 
-                         dataConSig, dataConStrictMarks, dataConExStricts, 
+                         dataConRepArgTys, dataConRepType, dataConFullSig,
+                         dataConStrictMarks, dataConExStricts, 
                          splitProductType, isVanillaDataCon, dataConFieldType,
-                         dataConInstOrigArgTys, deepSplitProductType
+                         deepSplitProductType, 
                        )
 import Id              ( idType, mkGlobalId, mkVanillaGlobal, mkSysLocal, 
                          mkTemplateLocals, mkTemplateLocalsNum, mkExportedLocalId,
-                         mkTemplateLocal, idName, mkWildId
+                         mkTemplateLocal, idName
                        )
 import IdInfo          ( IdInfo, noCafIdInfo,  setUnfoldingInfo, 
                          setArityInfo, setSpecInfo, setCafInfo,
@@ -90,12 +93,13 @@ import NewDemand    ( mkStrictSig, DmdResult(..),
 import DmdAnal         ( dmdAnalTopRhs )
 import CoreSyn
 import Unique          ( mkBuiltinUnique, mkPrimOpIdUnique )
+import Maybe           ( fromJust )
 import Maybes
 import PrelNames
 import Util             ( dropList, isSingleton )
 import Outputable
 import FastString
-import ListSetOps      ( assoc )
+import ListSetOps      ( assoc, minusList )
 \end{code}             
 
 %************************************************************************
@@ -190,27 +194,43 @@ Notice that
 mkDataConIds :: Name -> Name -> DataCon -> DataConIds
 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
+    || not (null eq_spec)
+    || isInst
+  = DCIds (Just alg_wrap_id) wrk_id
 
   | otherwise                                  -- Algebraic, no wrapper
-  = AlgDC Nothing wrk_id
+  = DCIds Nothing wrk_id
   where
-    (tvs, theta, orig_arg_tys) = dataConSig data_con
-    tycon       = dataConTyCon data_con
-
-    dict_tys    = mkPredTys theta
-    all_arg_tys = dict_tys ++ orig_arg_tys
-    tycon_args  = dataConUnivTyVars data_con
-    result_ty_args = (mkTyVarTys tycon_args)
-    result_ty   = mkTyConApp tycon result_ty_args
-
-    wrap_ty = mkForAllTys tvs (mkFunTys all_arg_tys result_ty)
+    (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
        -- 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
+    familyArgs     = map (substTy    subst) instTys
+    result_ty      = if isInst
+                    then mkTyConApp familyTyCon familyArgs  -- instance con
+                    else mkTyConApp tycon result_ty_args    -- ordinary con
+    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) --------------
        -- The *worker* for the data constructor is the function that
@@ -250,9 +270,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
 
-       ----------- 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 &&
@@ -260,7 +280,7 @@ 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 $ 
-                  mkLams tvs $ Lam id_arg1 $ 
+                  mkLams wrap_tvs $ Lam id_arg1 $ 
                   wrapNewTypeBody tycon result_ty_args
                        (Var id_arg1)
 
@@ -290,14 +310,16 @@ mkDataConIds wrap_name wkr_name data_con
        -- we want to see that w is strict in its two arguments
 
     alg_unf = mkTopUnfolding $ Note InlineMe $
-             mkLams tvs $ 
+             mkLams wrap_tvs $ 
              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 (tvs ++ reverse rep_ids))
+    con_app _ rep_ids = 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
@@ -318,7 +340,7 @@ mkDataConIds wrap_name wkr_name data_con
                        Case (Var arg) arg result_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)
 
@@ -461,7 +483,9 @@ mkRecordSelId tycon field_label
     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 
@@ -538,28 +562,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) (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
-       (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_tvs ++ mkTemplateLocalsNum arg_base (mkPredTys dc_theta),
-             mkTemplateLocalsNum arg_base' dc_arg_tys)
-
-       (dc_tvs, dc_theta, dc_arg_tys) = dataConSig data_con
-       arg_base' = arg_base + length dc_theta
-
-       unpack_base = arg_base' + length dc_arg_tys
-       uniqs = map mkBuiltinUnique [unpack_base..]
-
-       the_arg_id  = assoc "mkRecordSelId:mk_alt" (field_lbls `zip` arg_ids) field_label
+           -- 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
+               ExprCoFn co -> Cast (Var the_arg_id) co
+               id_co       -> ASSERT(isIdCoercion 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
 
-    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...
@@ -573,30 +606,36 @@ 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
-  = mkUnpackCase the_id arg con_args boxing_con rhs
+unboxProduct :: Int -> CoreExpr -> Type -> (Int -> [Id] -> CoreExpr) -> CoreExpr
+unboxProduct i arg arg_ty body
+  = result
   where 
-    (_, _, 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 -> [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 bndr (exprType body) [(DataAlt boxing_con, unpk_args, body)]
+  = Case cast_arg (setIdType bndr bndr_ty) (exprType body) [(DataAlt boxing_con, unpk_args, body)]
   where
-  cast_arg = go (idType bndr) arg
+  (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)
-    | otherwise = arg
+    | otherwise = (arg, ty)
 
 -- ...and the dual
 reboxProduct :: [Unique]     -- uniques to create new local binders
@@ -606,7 +645,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
 
@@ -621,10 +660,10 @@ 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 
+      | 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)
 
@@ -664,7 +703,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 
@@ -757,26 +796,26 @@ 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
 -- it, otherwise the wrap/unwrap are both no-ops 
 --
 wrapNewTypeBody tycon args result_expr
   | Just co_con <- newTyConCo tycon
-  = Cast result_expr (mkTyConApp co_con args)
+  = mkCoerce (mkSymCoercion (mkTyConApp co_con args)) result_expr
   | otherwise
   = result_expr
 
 unwrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
 unwrapNewTypeBody tycon args result_expr
   | Just co_con <- newTyConCo tycon
-  = Cast result_expr (mkSymCoercion (mkTyConApp co_con args))
+  = mkCoerce (mkTyConApp co_con args) result_expr
   | otherwise
   = result_expr