Major refactoring of the type inference engine
[ghc-hetmet.git] / compiler / types / FamInstEnv.lhs
index 50c827f..93a67a7 100644 (file)
@@ -36,8 +36,6 @@ import Outputable
 import Maybes
 import Util
 import FastString
-
-import Maybe
 \end{code}
 
 
@@ -90,14 +88,23 @@ pprFamInst famInst
        2 (ptext (sLit "--") <+> pprNameLoc (getName famInst))
 
 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
-    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)
@@ -148,13 +155,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
+     -- See Note [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
@@ -162,6 +187,9 @@ data FamilyInstEnv
                        --      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)
@@ -226,9 +254,10 @@ lookupFamInstEnv
     :: FamInstEnvs
     -> TyCon -> [Type]         -- What we are looking for
     -> [FamInstMatch]          -- Successful matches
+-- Precondition: the tycon is saturated (or over-saturated)
 
 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
 
@@ -243,9 +272,11 @@ lookupFamInstEnvConflicts
 -- 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
-  = 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"
@@ -275,12 +306,13 @@ lookupFamInstEnvConflicts envs fam_inst skol_tvs
       | otherwise      = not (old_rhs `tcEqType` new_rhs)
       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
-@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
@@ -297,16 +329,23 @@ type MatchFun =  FamInst          -- The FamInst template
              -> [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
+    -> OneSidedMatch
     -> 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
-  = 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 
@@ -323,7 +362,7 @@ lookup_fam_inst_env match_fun (pkg_ie, home_ie) fam 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
@@ -412,7 +451,7 @@ topNormaliseType env ty
                   | otherwise           = rec_nts
 
     go rec_nts (TyConApp tc tys)               -- Expand open tycons
-       | isOpenTyCon tc
+       | isFamilyTyCon tc
        , (ACo co, ty) <- normaliseTcApp env tc tys
        =       -- The ACo says "something happened"
                -- Note that normaliseType fully normalises, but it has do to so
@@ -430,25 +469,28 @@ topNormaliseType env ty
 ---------------
 normaliseTcApp :: FamInstEnvs -> TyCon -> [Type] -> (CoercionI, Type)
 normaliseTcApp env tc tys
-  = let        -- First normalise the arg types so that they'll match 
+  | 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              = mkTyConApp co_tycon inst_tys
+       first_coi       = mkTransCoI tycon_coi (ACo co)
+       (rest_coi, nty) = normaliseType env (mkTyConApp rep_tc inst_tys)
+       fix_coi         = mkTransCoI first_coi rest_coi
+    in 
+    (fix_coi, nty)
+
+  | otherwise
+  = (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    = 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;
-               -- we do not do anything
-       _ -> (tycon_coi, TyConApp tc ntys)
+    (cois, ntys) = mapAndUnzip (normaliseType env) tys
+    tycon_coi    = mkTyConAppCoI tc cois
+
 ---------------
 normaliseType :: FamInstEnvs           -- environment with family instances
              -> Type                   -- old type
@@ -464,16 +506,16 @@ normaliseType env (TyConApp tc tys)
 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  (mkAppTyCoI coi1 coi2, mkAppTy nty1 nty2)
 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  (mkFunTyCoI coi1 coi2, mkFunTy nty1 nty2)
 normaliseType env (ForAllTy tyvar ty1)
   = let (coi,nty1) = normaliseType env ty1
-    in  (mkForAllTyCoI tyvar coi,ForAllTy tyvar nty1)
+    in  (mkForAllTyCoI tyvar coi, ForAllTy tyvar nty1)
 normaliseType _   ty@(TyVarTy _)
-  = (IdCo,ty)
+  = (IdCo ty,ty)
 normaliseType env (PredTy predty)
   = normalisePred env predty
 
@@ -481,12 +523,12 @@ normaliseType env (PredTy predty)
 normalisePred :: FamInstEnvs -> PredType -> (CoercionI,Type)
 normalisePred env (ClassP cls tys)
   =    let (cois,tys') = mapAndUnzip (normaliseType env) tys
-       in  (mkClassPPredCoI cls tys' cois, PredTy $ ClassP cls tys')
+       in  (mkClassPPredCoI cls cois, PredTy $ ClassP cls tys')
 normalisePred env (IParam ipn ty)
   =    let (coi,ty') = normaliseType env ty
        in  (mkIParamPredCoI ipn coi, PredTy $ IParam ipn ty')
 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')
+       in  (mkEqPredCoI coi1 coi2, PredTy $ EqPred ty1' ty2')
 \end{code}