Whitespace only in nativeGen/RegAlloc/Linear/Main.hs
[ghc-hetmet.git] / compiler / types / FamInstEnv.lhs
index 50c827f..5b4374a 100644 (file)
@@ -29,15 +29,12 @@ import TypeRep
 import TyCon
 import Coercion
 import VarSet
 import TyCon
 import Coercion
 import VarSet
-import Var
 import Name
 import UniqFM
 import Outputable
 import Maybes
 import Util
 import FastString
 import Name
 import UniqFM
 import Outputable
 import Maybes
 import Util
 import FastString
-
-import Maybe
 \end{code}
 
 
 \end{code}
 
 
@@ -87,17 +84,31 @@ instance Outputable FamInst where
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)
 pprFamInst :: FamInst -> SDoc
 pprFamInst famInst
   = hang (pprFamInstHdr famInst)
-       2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))
+       2 (vcat [ ifPprDebug (ptext (sLit "Coercion axiom:") <+> pp_ax)
+               , ptext (sLit "--") <+> pprNameLoc (getName famInst)])
+  where
+    pp_ax = case tyConFamilyCoercion_maybe (fi_tycon famInst) of
+              Just ax -> ppr ax
+              Nothing -> ptext (sLit "<not there!>")
 
 pprFamInstHdr :: FamInst -> SDoc
 
 pprFamInstHdr :: FamInst -> SDoc
-pprFamInstHdr (FamInst {fi_fam = fam, fi_tys = tys, fi_tycon = tycon})
-  = pprTyConSort <+> pprHead
+pprFamInstHdr (FamInst {fi_tycon = rep_tc})
+  = pprTyConSort <+> pp_instance <+> pprHead
   where
   where
-    pprHead = pprTypeApp fam tys
-    pprTyConSort | isDataTyCon tycon = ptext (sLit "data instance")
-                | isNewTyCon  tycon = ptext (sLit "newtype instance")
-                | isSynTyCon  tycon = ptext (sLit "type instance")
-                | otherwise         = panic "FamInstEnv.pprFamInstHdr"
+    Just (fam_tc, tys) = tyConFamInst_maybe rep_tc 
+    
+    -- For *associated* types, say "type T Int = blah" 
+    -- For *top level* type instances, say "type instance T Int = blah"
+    pp_instance 
+      | isTyConAssoc fam_tc = empty
+      | otherwise           = ptext (sLit "instance")
+
+    pprHead = pprTypeApp fam_tc tys
+    pprTyConSort | isDataTyCon     rep_tc = ptext (sLit "data")
+                | isNewTyCon      rep_tc = ptext (sLit "newtype")
+                | isSynTyCon      rep_tc = ptext (sLit "type")
+                | isAbstractTyCon rep_tc = ptext (sLit "data")
+                | otherwise              = panic "FamInstEnv.pprFamInstHdr"
 
 pprFamInsts :: [FamInst] -> SDoc
 pprFamInsts finsts = vcat (map pprFamInst finsts)
 
 pprFamInsts :: [FamInst] -> SDoc
 pprFamInsts finsts = vcat (map pprFamInst finsts)
@@ -148,13 +159,31 @@ mkImportedFamInst fam mb_tcs tycon
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 
-InstEnv maps a family name to the list of known instances for that family.
+Note [FamInstEnv]
+~~~~~~~~~~~~~~~~~~~~~
+A FamInstEnv maps a family name to the list of known instances for that family.
+
+The same FamInstEnv includes both 'data family' and 'type family' instances.
+Type families are reduced during type inference, but not data families;
+the user explains when to use a data family instance by using contructors
+and pattern matching.
+
+Neverthless it is still useful to have data families in the FamInstEnv:
+
+ - For finding overlaps and conflicts
+
+ - For finding the representation type...see FamInstEnv.topNormaliseType
+   and its call site in Simplify
+
+ - In standalone deriving instance Eq (T [Int]) we need to find the 
+   representation type for T [Int]
 
 \begin{code}
 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
 
 \begin{code}
 type FamInstEnv = UniqFM FamilyInstEnv -- Maps a family to its instances
+     -- See Note [FamInstEnv]
 
 type FamInstEnvs = (FamInstEnv, FamInstEnv)
 
 type FamInstEnvs = (FamInstEnv, FamInstEnv)
-       -- External package inst-env, Home-package inst-env
+     -- External package inst-env, Home-package inst-env
 
 data FamilyInstEnv
   = FamIE [FamInst]    -- The instances for a particular family, in any order
 
 data FamilyInstEnv
   = FamIE [FamInst]    -- The instances for a particular family, in any order
@@ -162,6 +191,9 @@ data FamilyInstEnv
                        --      If *not* then the common case of looking up
                        --      (T a b c) can fail immediately
 
                        --      If *not* then the common case of looking up
                        --      (T a b c) can fail immediately
 
+instance Outputable FamilyInstEnv where
+  ppr (FamIE fs b) = ptext (sLit "FamIE") <+> ppr b <+> vcat (map ppr fs)
+
 -- INVARIANTS:
 --  * The fs_tvs are distinct in each FamInst
 --     of a range value of the map (so we can safely unify them)
 -- INVARIANTS:
 --  * The fs_tvs are distinct in each FamInst
 --     of a range value of the map (so we can safely unify them)
@@ -226,9 +258,10 @@ lookupFamInstEnv
     :: FamInstEnvs
     -> TyCon -> [Type]         -- What we are looking for
     -> [FamInstMatch]          -- Successful matches
     :: FamInstEnvs
     -> TyCon -> [Type]         -- What we are looking for
     -> [FamInstMatch]          -- Successful matches
+-- Precondition: the tycon is saturated (or over-saturated)
 
 lookupFamInstEnv
 
 lookupFamInstEnv
-   = lookup_fam_inst_env match
+   = lookup_fam_inst_env match True
    where
      match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
 
    where
      match _ tpl_tvs tpl_tys tys = tcMatchTys tpl_tvs tpl_tys tys
 
@@ -243,9 +276,11 @@ lookupFamInstEnvConflicts
 -- to find conflicting matches
 -- The skolem tyvars are needed because we don't have a 
 -- unique supply to hand
 -- to find conflicting matches
 -- The skolem tyvars are needed because we don't have a 
 -- unique supply to hand
+--
+-- Precondition: the tycon is saturated (or over-saturated)
 
 lookupFamInstEnvConflicts envs fam_inst skol_tvs
 
 lookupFamInstEnvConflicts envs fam_inst skol_tvs
-  = lookup_fam_inst_env my_unify envs fam tys'
+  = lookup_fam_inst_env my_unify False envs fam tys'
   where
     inst_tycon = famInstTyCon fam_inst
     (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
   where
     inst_tycon = famInstTyCon fam_inst
     (fam, tys) = expectJust "FamInstEnv.lookuFamInstEnvConflicts"
@@ -272,15 +307,16 @@ lookupFamInstEnvConflicts envs fam_inst skol_tvs
       --   anything else would be difficult to test for at this stage.
     conflicting old_fam_inst subst 
       | isAlgTyCon fam = True
       --   anything else would be difficult to test for at this stage.
     conflicting old_fam_inst subst 
       | isAlgTyCon fam = True
-      | otherwise      = not (old_rhs `tcEqType` new_rhs)
+      | otherwise      = not (old_rhs `eqType` new_rhs)
       where
         old_tycon = famInstTyCon old_fam_inst
       where
         old_tycon = famInstTyCon old_fam_inst
-        old_rhs   = mkTyConApp old_tycon (substTyVars subst (tyConTyVars old_tycon))
+        old_tvs   = tyConTyVars old_tycon
+        old_rhs   = mkTyConApp old_tycon  (substTyVars subst old_tvs)
         new_rhs   = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
 \end{code}
 
 While @lookupFamInstEnv@ uses a one-way match, the next function
         new_rhs   = mkTyConApp inst_tycon (substTyVars subst skol_tvs)
 \end{code}
 
 While @lookupFamInstEnv@ uses a one-way match, the next function
-@lookupFamInstEnvUnify@ uses two-way matching (ie, unification).  This is
+@lookupFamInstEnvConflicts@ uses two-way matching (ie, unification).  This is
 needed to check for overlapping instances.
 
 For class instances, these two variants of lookup are combined into one
 needed to check for overlapping instances.
 
 For class instances, these two variants of lookup are combined into one
@@ -297,16 +333,23 @@ type MatchFun =  FamInst          -- The FamInst template
              -> [Type]                 -- Target to match against
              -> Maybe TvSubst
 
              -> [Type]                 -- Target to match against
              -> Maybe TvSubst
 
+type OneSidedMatch = Bool     -- Are optimisations that are only valid for
+                              -- one sided matches allowed?
+
 lookup_fam_inst_env          -- The worker, local to this module
     :: MatchFun
 lookup_fam_inst_env          -- The worker, local to this module
     :: MatchFun
+    -> OneSidedMatch
     -> FamInstEnvs
     -> TyCon -> [Type]         -- What we are looking for
     -> [FamInstMatch]          -- Successful matches
     -> FamInstEnvs
     -> TyCon -> [Type]         -- What we are looking for
     -> [FamInstMatch]          -- Successful matches
-lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
-  | not (isOpenTyCon fam) 
+
+-- Precondition: the tycon is saturated (or over-saturated)
+
+lookup_fam_inst_env match_fun one_sided (pkg_ie, home_ie) fam tys
+  | not (isFamilyTyCon fam) 
   = []
   | otherwise
   = []
   | otherwise
-  = ASSERT( n_tys >= arity )   -- Family type applications must be saturated
+  = ASSERT2( n_tys >= arity, ppr fam <+> ppr tys )     -- Family type applications must be saturated
     home_matches ++ pkg_matches
   where
     home_matches = lookup home_ie 
     home_matches ++ pkg_matches
   where
     home_matches = lookup home_ie 
@@ -323,7 +366,7 @@ lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam tys
 
     --------------
     rough_tcs = roughMatchTcs match_tys
 
     --------------
     rough_tcs = roughMatchTcs match_tys
-    all_tvs   = all isNothing rough_tcs
+    all_tvs   = all isNothing rough_tcs && one_sided
 
     --------------
     lookup env = case lookupUFM env fam of
 
     --------------
     lookup env = case lookupUFM env fam of
@@ -400,62 +443,65 @@ topNormaliseType env ty
     go rec_nts ty | Just ty' <- coreView ty    -- Expand synonyms
        = go rec_nts ty'        
 
     go rec_nts ty | Just ty' <- coreView ty    -- Expand synonyms
        = go rec_nts ty'        
 
-    go rec_nts (TyConApp tc tys)               -- Expand newtypes
-       | Just co_con <- newTyConCo_maybe tc    -- See Note [Expanding newtypes]
-       = if tc `elem` rec_nts                  --  in Type.lhs
+    go rec_nts (TyConApp tc tys)
+        | isNewTyCon tc                -- Expand newtypes
+       = if tc `elem` rec_nts  -- See Note [Expanding newtypes] in Type.lhs
          then Nothing
          then Nothing
-         else let nt_co = mkTyConApp co_con tys
-              in add_co nt_co rec_nts' nt_rhs
-       where
-         nt_rhs = newTyConInstRhs tc tys
-         rec_nts' | isRecursiveTyCon tc = tc:rec_nts
-                  | otherwise           = rec_nts
-
-    go rec_nts (TyConApp tc tys)               -- Expand open tycons
-       | isOpenTyCon tc
-       , (ACo co, ty) <- normaliseTcApp env tc tys
-       =       -- The ACo says "something happened"
-               -- Note that normaliseType fully normalises, but it has do to so
-               -- to be sure that 
-          add_co co rec_nts ty
+          else let nt_co = mkAxInstCo (newTyConCo tc) tys
+               in add_co nt_co rec_nts' nt_rhs
+
+       | isFamilyTyCon tc              -- Expand open tycons
+       , (co, ty) <- normaliseTcApp env tc tys
+               -- Note that normaliseType fully normalises, 
+               -- but it has do to so to be sure that 
+        , not (isReflCo co)
+        = add_co co rec_nts ty
+        where
+          nt_rhs = newTyConInstRhs tc tys
+          rec_nts' | isRecursiveTyCon tc = tc:rec_nts
+                   | otherwise           = rec_nts
 
     go _ _ = Nothing
 
     add_co co rec_nts ty 
        = case go rec_nts ty of
                Nothing         -> Just (co, ty)
 
     go _ _ = Nothing
 
     add_co co rec_nts ty 
        = case go rec_nts ty of
                Nothing         -> Just (co, ty)
-               Just (co', ty') -> Just (mkTransCoercion co co', ty')
+               Just (co', ty') -> Just (mkTransCo co co', ty')
         
 
 ---------------
         
 
 ---------------
-normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
+normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (Coercion, Type)
 normaliseTcApp env tc tys
 normaliseTcApp env tc tys
-  = let        -- First normalise the arg types so that they'll match 
-       -- when we lookup in in the instance envt
-       (cois, ntys) = mapAndUnzip (normaliseType env) tys
-       tycon_coi    = mkTyConAppCoI tc ntys cois
-    in         -- Now try the top-level redex
-    case lookupFamInstEnv env tc ntys of
-               -- A matching family instance exists
-       [(fam_inst, tys)] -> (fix_coi, nty)
-           where
-               rep_tc         = famInstTyCon fam_inst
-               co_tycon       = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
-               co             = mkTyConApp co_tycon tys
-               first_coi      = mkTransCoI tycon_coi (ACo co)
-               (rest_coi,nty) = normaliseType env (mkTyConApp rep_tc tys)
-               fix_coi        = mkTransCoI first_coi rest_coi
-
-               -- No unique matching family instance exists;
+  | isFamilyTyCon tc
+  , tyConArity tc <= length tys           -- Unsaturated data families are possible
+  , [(fam_inst, inst_tys)] <- lookupFamInstEnv env tc ntys 
+  = let    -- A matching family instance exists
+       rep_tc          = famInstTyCon fam_inst
+       co_tycon        = expectJust "lookupFamInst" (tyConFamilyCoercion_maybe rep_tc)
+       co              = mkAxInstCo co_tycon inst_tys
+       first_coi       = mkTransCo tycon_coi co
+       (rest_coi,nty)  = normaliseType env (mkTyConApp rep_tc inst_tys)
+       fix_coi         = mkTransCo first_coi rest_coi
+    in 
+    (fix_coi, nty)
+
+  | otherwise   -- No unique matching family instance exists;
                -- we do not do anything
                -- we do not do anything
-       _ -> (tycon_coi, TyConApp tc ntys)
+  = (tycon_coi, TyConApp tc ntys)
+
+  where
+       -- Normalise the arg types so that they'll match 
+       -- when we lookup in in the instance envt
+    (cois, ntys) = mapAndUnzip (normaliseType env) tys
+    tycon_coi    = mkTyConAppCo tc cois
+
 ---------------
 normaliseType :: FamInstEnvs           -- environment with family instances
              -> Type                   -- old type
 ---------------
 normaliseType :: FamInstEnvs           -- environment with family instances
              -> Type                   -- old type
-             -> (CoercionI, Type)      -- (coercion,new type), where
+             -> (Coercion, Type)       -- (coercion,new type), where
                                        -- co :: old-type ~ new_type
 -- Normalise the input type, by eliminating *all* type-function redexes
                                        -- co :: old-type ~ new_type
 -- Normalise the input type, by eliminating *all* type-function redexes
--- Returns with IdCo if nothing happens
+-- Returns with Refl if nothing happens
 
 normaliseType env ty 
   | Just ty' <- coreView ty = normaliseType env ty' 
 
 normaliseType env ty 
   | Just ty' <- coreView ty = normaliseType env ty' 
@@ -464,29 +510,29 @@ normaliseType env (TyConApp tc tys)
 normaliseType env (AppTy ty1 ty2)
   = let (coi1,nty1) = normaliseType env ty1
         (coi2,nty2) = normaliseType env ty2
 normaliseType env (AppTy ty1 ty2)
   = let (coi1,nty1) = normaliseType env ty1
         (coi2,nty2) = normaliseType env ty2
-    in  (mkAppTyCoI nty1 coi1 nty2 coi2, AppTy nty1 nty2)
+    in  (mkAppCo coi1 coi2, mkAppTy nty1 nty2)
 normaliseType env (FunTy ty1 ty2)
   = let (coi1,nty1) = normaliseType env ty1
         (coi2,nty2) = normaliseType env ty2
 normaliseType env (FunTy ty1 ty2)
   = let (coi1,nty1) = normaliseType env ty1
         (coi2,nty2) = normaliseType env ty2
-    in  (mkFunTyCoI nty1 coi1 nty2 coi2, FunTy nty1 nty2)
+    in  (mkFunCo coi1 coi2, mkFunTy nty1 nty2)
 normaliseType env (ForAllTy tyvar ty1)
   = let (coi,nty1) = normaliseType env ty1
 normaliseType env (ForAllTy tyvar ty1)
   = let (coi,nty1) = normaliseType env ty1
-    in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+    in  (mkForAllCo tyvar coi, ForAllTy tyvar nty1)
 normaliseType _   ty@(TyVarTy _)
 normaliseType _   ty@(TyVarTy _)
-  = (IdCo,ty)
+  = (Refl ty,ty)
 normaliseType env (PredTy predty)
   = normalisePred env predty
 
 ---------------
 normaliseType env (PredTy predty)
   = normalisePred env predty
 
 ---------------
-normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
+normalisePred :: FamInstEnvs -> PredType -> (Coercion,Type)
 normalisePred env (ClassP cls tys)
 normalisePred env (ClassP cls tys)
-  =    let (cois,tys') = mapAndUnzip (normaliseType env) tys
-       in  (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
+  = let (cos,tys') = mapAndUnzip (normaliseType env) tys
+    in  (mkPredCo $ ClassP cls cos, PredTy $ ClassP cls tys')
 normalisePred env (IParam ipn ty)
 normalisePred env (IParam ipn ty)
-  =    let (coi,ty') = normaliseType env ty
-       in  (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
+  = let (co,ty') = normaliseType env ty
+    in  (mkPredCo $ (IParam ipn co), PredTy $ IParam ipn ty')
 normalisePred env (EqPred ty1 ty2)
 normalisePred env (EqPred ty1 ty2)
-  =    let (coi1,ty1') = normaliseType env ty1
-            (coi2,ty2') = normaliseType env ty2
-       in  (mkEqPredCoI ty1' coi1 ty2' coi2, PredTy $ EqPred ty1' ty2')
+  = let (co1,ty1') = normaliseType env ty1
+        (co2,ty2') = normaliseType env ty2
+    in  (mkPredCo $ (EqPred co1 co2), PredTy $ EqPred ty1' ty2')
 \end{code}
 \end{code}