Updated documentation; changed "group" to "branched" in type families
authorRichard Eisenberg <eir@cis.upenn.edu>
Thu, 25 Apr 2013 01:28:43 +0000 (21:28 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Thu, 25 Apr 2013 01:28:43 +0000 (21:28 -0400)
compiler/iface/IfaceSyn.lhs
compiler/iface/MkIface.lhs
compiler/iface/TcIface.lhs
compiler/typecheck/FamInst.lhs
compiler/types/CoAxiom.lhs
compiler/types/FamInstEnv.lhs
compiler/types/OptCoercion.lhs
compiler/types/Unify.lhs

index 7361f4b..a0e1a08 100644 (file)
@@ -177,11 +177,11 @@ data IfaceClsInst
 -- match types, one per branch... but each "rough match types" is itself
 -- a list of Maybe IfaceTyCon. So, we get [[Maybe IfaceTyCon]].
 data IfaceFamInst
-  = IfaceFamInst { ifFamInstFam   :: IfExtName            -- Family name
-                 , ifFamInstGroup :: Bool                 -- Is this a group?
-                 , ifFamInstTys   :: [[Maybe IfaceTyCon]] -- See above
-                 , ifFamInstAxiom :: IfExtName            -- The axiom
-                 , ifFamInstOrph  :: Maybe OccName        -- Just like IfaceClsInst
+  = IfaceFamInst { ifFamInstFam      :: IfExtName            -- Family name
+                 , ifFamInstBranched :: Bool                 -- Is this branched?
+                 , ifFamInstTys      :: [[Maybe IfaceTyCon]] -- See above
+                 , ifFamInstAxiom    :: IfExtName            -- The axiom
+                 , ifFamInstOrph     :: Maybe OccName        -- Just like IfaceClsInst
                  }
 
 data IfaceRule
index b11158c..e9676ac 100644 (file)
@@ -1640,14 +1640,14 @@ instanceToIfaceInst (ClsInst { is_dfun = dfun_id, is_flag = oflag
 --------------------------
 famInstToIfaceFamInst :: FamInst br -> IfaceFamInst
 famInstToIfaceFamInst (FamInst { fi_axiom    = axiom,
-                                 fi_group    = group,
+                                 fi_branched = branched,
                                  fi_fam      = fam,
                                  fi_branches = branches })
-  = IfaceFamInst { ifFamInstAxiom = coAxiomName axiom
-                 , ifFamInstFam   = fam
-                 , ifFamInstGroup = group
-                 , ifFamInstTys   = map (map do_rough) roughs
-                 , ifFamInstOrph  = orph }
+  = IfaceFamInst { ifFamInstAxiom    = coAxiomName axiom
+                 , ifFamInstFam      = fam
+                 , ifFamInstBranched = branched
+                 , ifFamInstTys      = map (map do_rough) roughs
+                 , ifFamInstOrph     = orph }
   where
     roughs = brListMap famInstBranchRoughMatch branches
 
index c47066d..7f0ad07 100644 (file)
@@ -659,11 +659,11 @@ tcIfaceInst (IfaceClsInst { ifDFun = dfun_occ, ifOFlag = oflag
 
 tcIfaceFamInst :: IfaceFamInst -> IfL (FamInst Branched)
 tcIfaceFamInst (IfaceFamInst { ifFamInstFam = fam, ifFamInstTys = mb_tcss
-                             , ifFamInstGroup = group, ifFamInstAxiom = axiom_name } )
+                             , ifFamInstBranched = branched, ifFamInstAxiom = axiom_name } )
     = do { axiom' <- forkM (ptext (sLit "Axiom") <+> ppr axiom_name) $
                      tcIfaceCoAxiom axiom_name
          ; let mb_tcss' = map (map (fmap ifaceTyConName)) mb_tcss
-         ; return (mkImportedFamInst fam group mb_tcss' axiom') }
+         ; return (mkImportedFamInst fam branched mb_tcss' axiom') }
 \end{code}
 
 
index 2f81ca6..e99133b 100644 (file)
@@ -56,13 +56,13 @@ import qualified Data.Map as Map
 newFamInst :: FamFlavor -> Bool -> CoAxiom br -> TcRnIf gbl lcl(FamInst br)
 -- Freshen the type variables of the FamInst branches
 -- Called from the vectoriser monad too, hence the rather general type
-newFamInst flavor is_group axiom@(CoAxiom { co_ax_tc       = fam_tc
-                                          , co_ax_branches = ax_branches })
+newFamInst flavor is_branched axiom@(CoAxiom { co_ax_tc       = fam_tc
+                                             , co_ax_branches = ax_branches })
   = do { fam_branches <- go ax_branches
        ; return (FamInst { fi_fam      = tyConName fam_tc
                          , fi_flavor   = flavor
                          , fi_branches = fam_branches
-                         , fi_group    = is_group
+                         , fi_branched = is_branched
                          , fi_axiom    = axiom }) }
   where
     go :: BranchList CoAxBranch br -> TcRnIf gbl lcl (BranchList FamInstBranch br)
@@ -347,8 +347,8 @@ environments (one for the EPS and one for the HPT).
 \begin{code}
 checkForConflicts :: FamInstEnvs -> FamInst Branched -> TcM Bool
 checkForConflicts inst_envs fam_inst@(FamInst { fi_branches = branches
-                                              , fi_group = group })
-  = do { let conflicts = brListMap (lookupFamInstEnvConflicts inst_envs group fam_tc) branches
+                                              , fi_branched = branched })
+  = do { let conflicts = brListMap (lookupFamInstEnvConflicts inst_envs branched fam_tc) branches
              no_conflicts = all null conflicts
        ; traceTc "checkForConflicts" (ppr conflicts $$ ppr fam_inst $$ ppr inst_envs)
        ; unless no_conflicts $
index bf432ca..365c653 100644 (file)
@@ -77,7 +77,7 @@ can unify with the supplied arguments. After all, it is possible that some
 of the type arguments are lambda-bound type variables whose instantiation may
 cause an earlier match among the branches. We wish to prohibit this behavior,
 so the type checker rules out the choice of a branch where a previous branch
-can unify. See also [Instance checking within groups] in FamInstEnv.hs.
+can unify. See also [Branched instance checking] in FamInstEnv.hs.
 
 For example, the following is malformed, where 'a' is a lambda-bound type
 variable:
index 4e9b27e..d7371d6 100644 (file)
@@ -77,25 +77,25 @@ Note [FamInsts and CoAxioms]
       F ty1 .. tyn where F is a type family
 
 * A FamInstBranch corresponds to a CoAxBranch -- it represents
-  one alternative in a family instance group. We could theoretically
+  one alternative in a branched family instance. We could theoretically
   not have FamInstBranches and just use the CoAxBranches within
   the CoAxiom stored in the FamInst, but for one problem: we want to
   cache the "rough match" top-level tycon names for quick matching.
   This data is not stored in a CoAxBranch, so we use FamInstBranches
   instead.
 
-Note [fi_group field]
-~~~~~~~~~~~~~~~~~~~~~
+Note [fi_branched field]
+~~~~~~~~~~~~~~~~~~~~~~~~
 A FamInst stores whether or not it was declared with "type instance where"
 for two reasons: 
   1. for accurate pretty-printing; and 
   2. because confluent overlap is disallowed between branches 
      declared in groups. 
-Note that this "group-ness" is properly associated with the FamInst,
+Note that this "branched-ness" is properly associated with the FamInst,
 which thinks about overlap, and not in the CoAxiom, which blindly
 assumes that it is part of a consistent axiom set.
 
-A "group" with fi_group=True can have just one element, however.
+A "branched" instance with fi_branched=True can have just one branch, however.
 
 Note [Why we need fib_rhs]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -114,8 +114,8 @@ data FamInst br -- See Note [FamInsts and CoAxioms], Note [Branched axioms] in C
   = FamInst { fi_axiom    :: CoAxiom br      -- The new coercion axiom introduced
                                              -- by this family instance
             , fi_flavor   :: FamFlavor
-            , fi_group    :: Bool            -- True <=> declared with "type instance where"
-                                             -- See Note [fi_group field]
+            , fi_branched :: Bool            -- True <=> declared with "type instance where"
+                                             -- See Note [fi_branched field]
 
             -- Everything below here is a redundant,
             -- cached version of the two things above,
@@ -213,12 +213,12 @@ instance Outputable (FamInst br) where
 -- Prints the FamInst as a family instance declaration
 pprFamInst :: FamInst br -> SDoc
 pprFamInst (FamInst { fi_branches = brs, fi_flavor = SynFamilyInst
-                    , fi_group = True, fi_axiom = axiom })
+                    , fi_branched = True, fi_axiom = axiom })
   = hang (ptext (sLit "type instance where"))
        2 (vcat [pprCoAxBranchHdr axiom i | i <- brListIndices brs])
 
 pprFamInst fi@(FamInst { fi_flavor = flavor
-                       , fi_group = False, fi_axiom = ax })
+                       , fi_branched = False, fi_axiom = ax })
   = pprFamFlavor flavor <+> pp_instance
     <+> pprCoAxBranchHdr ax 0
   where
@@ -265,16 +265,16 @@ also.
 -- interface file.  In particular, we get the rough match info from the iface
 -- (instead of computing it here).
 mkImportedFamInst :: Name               -- Name of the family
-                  -> Bool               -- is this a group?
+                  -> Bool               -- is this a branched instance?
                   -> [[Maybe Name]]     -- Rough match info, per branch
                   -> CoAxiom Branched   -- Axiom introduced
                   -> FamInst Branched   -- Resulting family instance
-mkImportedFamInst fam group roughs axiom
+mkImportedFamInst fam branched roughs axiom
   = FamInst {
       fi_fam      = fam,
       fi_axiom    = axiom,
       fi_flavor   = flavor,
-      fi_group    = group,
+      fi_branched = branched,
       fi_branches = branches }
   where
      -- Lazy match (See note [Lazy axiom match])
@@ -442,8 +442,8 @@ desugared to
 
 we return the matching instance '(FamInst{.., fi_tycon = :R42T}, Int)'.
 
-Note [Instance checking within groups]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Branched instance checking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Consider the following:
 
@@ -454,33 +454,47 @@ type instance where
 g :: Show a => a -> F a
 g x = length (show x)
 
-Should that type-check? No. We need to allow for the possibility
-that 'a' might be Int and therefore 'F a' should be Bool. We can
-simplify 'F a' to Int only when we can be sure that 'a' is not Int.
-
-To achieve this, after finding a possible match within an instance group, we
-have to go back to all previous FamInstBranchess and check that, under the
-substitution induced by the match, other matches are not possible. This is
-similar to what happens with class instance selection, when we need to
-guarantee that there is only a match and no unifiers. The exact algorithm is
-different here because the the potentially-overlapping group is closed.
-
-ALTERNATE APPROACH: As we are processing the branches, we could check if an
-instance unifies but does not match. If this happens, there is no possible
-match and we can fail right away. This might be more efficient.
-
-Note [Early failure optimisation for instance groups]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-As we're searching through the instances for a match, it is
-possible that we find an branch within an instance that matches, but
-a previous branch still unifies. In this case, we can abort the
-search, because any other instance that matches will necessarily
-overlap with the instance group we're currently searching. Because
-overlap among instance groups is disallowed, we know that that
-no such other instance exists.
-
-Note [Confluence checking within groups]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Should that type-check? No. We need to allow for the possibility that 'a'
+might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
+only when we can be sure that 'a' is not Int.
+
+To achieve this, after finding a possible match within an instance, we have to
+go back to all previous FamInstBranchess and check that, under the
+substitution induced by the match, other branches are surely apart. (See
+[Apartness] in types/Unify.lhs.) This is similar to what happens with class
+instance selection, when we need to guarantee that there is only a match and
+no unifiers. The exact algorithm is different here because the the
+potentially-overlapping group is closed.
+
+As another example, consider this:
+
+type family G x
+type instance where
+  G Int = Bool
+  G a   = Double
+
+type family H y
+-- no instances
+
+Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
+simplify to be Int. So, (G (H Char)) is stuck, for now.
+
+ALTERNATE APPROACH: As we are processing the branches, we could check if a
+branch is not surely apart from an application but does not match that
+application. If this happens, there is no possible match and we can fail right
+away. This might be more efficient.
+
+Note [Early failure optimisation for branched instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As we're searching through the instances for a match, it is possible that we
+find a branch within an instance that matches, but a previous branch is not
+surely apart from the target application. In this case, we can abort the
+search, because any other instance that matches will necessarily overlap with
+the instance we're currently searching. Because overlap among branched
+instances is disallowed, we know that that no such other instance exists.
+
+Note [Confluence checking within branched instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 GHC allows type family instances to have overlapping patterns as long as the
 right-hand sides are coincident in the region of overlap. Can we extend this
 notion of confluent overlap to branched instances? Not in any obvious way.
@@ -512,7 +526,7 @@ So, why is this not a problem with non-branched confluent overlap? Because
 we don't need to verify that an application is apart from anything. The
 non-branched confluent overlap check happens when we add the instance to the
 environment -- we're unifying among patterns, which cannot contain type family
-appplications. So, we're safe there and can continue supporting that feature.
+applications. So, we're safe there and can continue supporting that feature.
 
 \begin{code}
 -- when matching a type family application, we get a FamInst,
@@ -551,7 +565,7 @@ lookupFamInstEnv
           Just subst
             | checkConflict seen match_tys
             -> (Nothing, StopSearching) -- we found an incoherence, so stop searching
-            -- see Note [Early failure optimisation for instance groups]
+            -- see Note [Early failure optimisation for branched instances]
 
             | otherwise
             -> (Just subst, KeepSearching)
@@ -561,13 +575,13 @@ lookupFamInstEnv
       where
         tpl_tv_set = mkVarSet tpl_tvs
 
-    -- see Note [Instance checking within groups]
+    -- see Note [Branched instance checking]
     checkConflict :: [FamInstBranch] -- the previous branches in the instance that matched
                   -> [Type]          -- the types in the tyfam application we are matching
                   -> Bool            -- is there a conflict?
     checkConflict [] _ = False
     checkConflict ((FamInstBranch { fib_lhs = tpl_tys }) : rest) match_tys
-          -- see Note [Confluence checking within groups]
+          -- see Note [Confluence checking within branched instances]
       | SurelyApart <- tcApartTys instanceBindFun tpl_tys match_tys
       = checkConflict rest match_tys
       | otherwise
@@ -640,7 +654,7 @@ returned; if the instance is not relevant, Nothing is returned. The MatchFun
 also indicates what the search algorithm should do next: it could
 KeepSearching or StopSearching.
 
-When to StopSearching? See Note [Early failure optimisation for instance groups]
+When to StopSearching? See Note [Early failure optimisation for branched instances]
 
 For class instances, these two variants of lookup are combined into one
 function (cf, @InstEnv@).  We don't do that for family instances as the
@@ -671,7 +685,7 @@ data ContSearch = KeepSearching
 -- Might be a one-way match or a unifier
 type MatchFun =  [FamInstBranch]     -- the previous branches in the instance
               -> FamInstBranch       -- the individual branch to check
-              -> Bool                -- is this branch a part of a group?
+              -> Bool                -- is this branch a part of a branched instance?
               -> [Type]              -- the types to match against
               -> (Maybe TvSubst, ContSearch)
 
@@ -705,7 +719,7 @@ lookup_fam_inst_env' match_fun _one_sided ie fam tys
 
 find :: MatchFun -> [Type] -> [FamInst Branched] -> [FamInstMatch]
 find _         _         [] = []
-find match_fun match_tys (inst@(FamInst { fi_branches = branches, fi_group = is_group }) : rest)
+find match_fun match_tys (inst@(FamInst { fi_branches = branches, fi_branched = is_branched }) : rest)
   = case findBranch [] (fromBranchList branches) 0 of
       (Just match, StopSearching) -> [match]
       (Just match, KeepSearching) -> match : find match_fun match_tys rest
@@ -723,7 +737,7 @@ find match_fun match_tys (inst@(FamInst { fi_branches = branches, fi_group = is_
       | instanceCantMatch rough_tcs mb_tcs
       = findBranch seen rest (ind+1) -- branch won't unify later; no need to add to 'seen'
       | otherwise
-      = case match_fun seen branch is_group match_tys of
+      = case match_fun seen branch is_branched match_tys of
           (Nothing, KeepSearching) -> findBranch (branch : seen) rest (ind+1)
           (Nothing, StopSearching) -> (Nothing, StopSearching)
           (Just subst, cont)       -> (Just match, cont)
index c85746b..7eaab5c 100644 (file)
@@ -377,7 +377,7 @@ seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~ False) and that al
 OK. But, all is not OK: we want to use the first branch of the axiom in this case,
 not the second. The problem is that the parameters of the first branch can unify with
 the supplied coercions, thus meaning that the first branch should be taken. See also
-Note [Instance checking within groups] in types/FamInstEnv.lhs.
+Note [Branched instance checking] in types/FamInstEnv.lhs.
 
 \begin{code}
 -- | Check to make sure that an AxInstCo is internally consistent.
index 2410a02..67e748e 100644 (file)
@@ -356,11 +356,25 @@ typesCantMatch prs = any (\(s,t) -> cant_match s t) prs
 %*                                                                      *
 %************************************************************************
 
+Note [Apartness]
+~~~~~~~~~~~~~~~~
+
+Definition: Two types t1 and t2 are /apart/ when, for all well-kinded
+substitutions Q, there exists no safe coercion witnessing the equality
+between Q(t1) and Q(t2).
+
+- Every two types that unify are not apart.
+
+- A type family application (i.e. TyConApp F tys) might or might not be
+  apart from any given type; it depends on the instances available. Because
+  we can't know what instances are available (as they might be included in
+  another module), we conclude that a type family application is *maybe apart*
+  from any other type.
+
 Note [Unification and apartness]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The workhorse function behind unification actually is testing for apartness,
-not unification. Here, two types are apart if it is never possible to unify
-them or any types they are safely coercible to.(* see below) There are three
+not unification. (See [Apartness], above.) There are three
 possibilities here:
 
  - two types might be NotApart, which means a substitution can be found between