Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : overlapping-tyfams
http://hackage.haskell.org/trac/ghc/changeset/4f08c12fc7457926e325342b5f0d9f450f8f4e2f >--------------------------------------------------------------- commit 4f08c12fc7457926e325342b5f0d9f450f8f4e2f Merge: 86e4ca3... e6ce335... Author: Richard Eisenberg <e...@cis.upenn.edu> Date: Tue Dec 4 13:58:04 2012 -0500 Merge branch 'master' into overlapping-tyfams Conflicts: compiler/types/TyCon.lhs .gitignore | 1 - .gitmodules | 3 + boot | 43 ---- compiler/cmm/CmmPipeline.hs | 19 ++- compiler/coreSyn/CoreLint.lhs | 55 ++++- compiler/coreSyn/CoreSyn.lhs | 20 ++ compiler/ghc.cabal.in | 2 +- compiler/ghc.mk | 3 + compiler/ghci/ByteCodeGen.lhs | 2 +- compiler/ghci/ByteCodeLink.lhs | 2 +- compiler/ghci/LibFFI.hsc | 34 +-- compiler/ghci/Linker.lhs | 26 +- compiler/iface/BinIface.hs | 2 +- compiler/iface/IfaceSyn.lhs | 2 +- compiler/iface/LoadIface.lhs | 2 +- compiler/iface/MkIface.lhs | 2 +- compiler/main/DriverMkDepend.hs | 4 +- compiler/main/DriverPipeline.hs | 6 +- compiler/main/DynFlags.hs | 8 +- compiler/main/GHC.hs | 2 +- compiler/main/GhcMake.hs | 4 +- compiler/main/InteractiveEval.hs | 20 +- compiler/main/Packages.lhs | 12 +- compiler/main/StaticFlagParser.hs | 6 +- compiler/main/StaticFlags.hs | 2 +- compiler/main/SysTools.lhs | 8 +- compiler/parser/Parser.y.pp | 1 + compiler/prelude/TysPrim.lhs | 2 + compiler/types/Coercion.lhs | 4 + compiler/types/Kind.lhs | 5 + compiler/types/TyCon.lhs | 6 + compiler/types/Type.lhs | 2 + compiler/types/TypeRep.lhs | 3 + compiler/utils/Outputable.lhs | 3 +- compiler/utils/Panic.lhs | 6 +- configure.ac | 59 +++++- docs/core-spec/.gitignore | 5 + docs/core-spec/CoreLint.ott | 400 ++++++++++++++++++++++++++++++++ docs/core-spec/CoreSyn.ott | 283 ++++++++++++++++++++++ docs/core-spec/Makefile | 17 ++ docs/core-spec/README | 83 +++++++ docs/core-spec/core-spec.mng | 306 ++++++++++++++++++++++++ docs/core-spec/core-spec.pdf | Bin 0 -> 303537 bytes ghc.mk | 3 +- ghc/GhciTags.hs | 8 +- ghc/InteractiveUI.hs | 68 +++--- ghc/Main.hs | 18 +- ghc/ghc-bin.cabal.in | 2 +- libraries/Cabal | 2 +- libraries/haskeline | 2 +- libraries/tarballs/time-1.4.0.1.tar.gz | Bin 87466 -> 0 bytes libraries/time | 1 + mk/config.mk.in | 8 +- packages | 24 +- rts/ghc.mk | 53 ++++- rts/package.conf.in | 3 + rts/posix/OSThreads.c | 3 +- sync-all | 40 +++- utils/ghc-pkg/Main.hs | 11 +- utils/ghc-pkg/ghc-pkg.cabal | 2 +- utils/runghc/runghc.cabal.in | 2 +- 61 files changed, 1510 insertions(+), 215 deletions(-) diff --cc compiler/types/TyCon.lhs index 98c100d,c686847..36b93d8 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@@ -718,122 -709,20 +721,125 @@@ so the coercion tycon CoT must hav %* * %************************************************************************ +Note [Coercion axiom branches] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In order to allow type family instance groups, an axiom needs to contain an +ordered list of alternatives, called branches. The kind of the coercion is +chosen based on which branch contains patterns that match the type variables +the axiom is instantiated with. The first such match is chosen. + +For type-checking, it is also necessary to check that no previous pattern +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. + +Note [Singleton axioms] +~~~~~~~~~~~~~~~~~~~~~~~ +Although a CoAxiom has the capacity to store many branches, in many cases, +we want only one. Furthermore, these so-called singleton axioms are used +in a variety of places throughout GHC, and it would difficult to generalize +all of that code to deal with branched axioms, especially when the code can +be sure of the fact that an axiom is indeed a singleton. At the same time, +it seems dangerous to assume singlehood in various places through GHC. + +The solution to this is to label a CoAxiom (and FamInst) with a phantom +type variable declaring whether it is known to be a singleton or not. The +list of branches is stored using a special form of list, declared below, +that ensures that the type variable is accurate. + +As of this writing (Dec 2012), it would not be appropriate to use a promoted +type as the phantom type, so we use empty datatypes. We wish to have GHC +remain compilable with GHC 7.2.1. If you are revising this code and GHC no +longer needs to remain compatible with GHC 7.2.x, then please update this +code to use promoted types. + \begin{code} + +-- the phantom type labels +data Unbranched deriving Typeable +data Branched deriving Typeable + +data BranchList a br where + FirstBranch :: a -> BranchList a br + NextBranch :: a -> BranchList a br -> BranchList a Branched + +-- convert to/from lists +toBranchList :: [a] -> BranchList a Branched +toBranchList [] = pprPanic "toBranchList" empty +toBranchList [b] = FirstBranch b +toBranchList (h:t) = NextBranch h (toBranchList t) + +fromBranchList :: BranchList a br -> [a] +fromBranchList (FirstBranch b) = [b] +fromBranchList (NextBranch h t) = h : (fromBranchList t) + +-- convert from any BranchList to a Branched BranchList +toBranchedList :: BranchList a br -> BranchList a Branched +toBranchedList (FirstBranch b) = FirstBranch b +toBranchedList (NextBranch h t) = NextBranch h t + +-- convert from any BranchList to an Unbranched BranchList +toUnbranchedList :: BranchList a br -> BranchList a Unbranched +toUnbranchedList (FirstBranch b) = FirstBranch b +toUnbranchedList _ = pprPanic "toUnbranchedList" empty + +-- length +brListLength :: BranchList a br -> Int +brListLength (FirstBranch _) = 1 +brListLength (NextBranch _ t) = 1 + brListLength t + +-- lookup +brListNth :: BranchList a br -> Int -> a +brListNth (FirstBranch b) 0 = b +brListNth (NextBranch h _) 0 = h +brListNth (NextBranch _ t) n = brListNth t (n-1) +brListNth _ _ = pprPanic "brListNth" empty + +-- map, fold +brListMap :: (a -> b) -> BranchList a br -> [b] +brListMap f (FirstBranch b) = [f b] +brListMap f (NextBranch h t) = f h : (brListMap f t) + +brListFoldr :: (a -> b -> b) -> b -> BranchList a br -> b +brListFoldr f x (FirstBranch b) = f b x +brListFoldr f x (NextBranch h t) = f h (brListFoldr f x t) + +-- zipWith +brListZipWith :: (a -> b -> c) -> BranchList a br1 -> BranchList b br2 -> [c] +brListZipWith f (FirstBranch a) (FirstBranch b) = [f a b] +brListZipWith f (FirstBranch a) (NextBranch b _) = [f a b] +brListZipWith f (NextBranch a _) (FirstBranch b) = [f a b] +brListZipWith f (NextBranch a ta) (NextBranch b tb) = f a b : brListZipWith f ta tb + +-- pretty-printing + +instance Outputable a => Outputable (BranchList a br) where + ppr = ppr . fromBranchList + -- | A 'CoAxiom' is a \"coercion constructor\", i.e. a named equality axiom. + + -- If you edit this type, you may need to update the GHC formalism + -- See Note [GHC Formalism] in coreSyn/CoreLint.lhs -data CoAxiom +data CoAxiom br = CoAxiom -- Type equality axiom. - { co_ax_unique :: Unique -- unique identifier - , co_ax_name :: Name -- name for pretty-printing - , co_ax_tvs :: [TyVar] -- bound type variables - , co_ax_lhs :: Type -- left-hand side of the equality - , co_ax_rhs :: Type -- right-hand side of the equality - , co_ax_implicit :: Bool -- True <=> the axiom is "implicit" - -- See Note [Implicit axioms] + { co_ax_unique :: Unique -- unique identifier + , co_ax_name :: Name -- name for pretty-printing + , co_ax_tc :: TyCon -- the head of the LHS patterns + , co_ax_branches :: BranchList CoAxBranch br + -- the branches that form this axiom + , co_ax_implicit :: Bool -- True <=> the axiom is "implicit" + -- See Note [Implicit axioms] + -- INVARIANT: co_ax_implicit == True implies length co_ax_branches == 1. + } + deriving Typeable + +data CoAxBranch + = CoAxBranch + { cab_tvs :: [TyVar] -- bound type variables + , cab_lhs :: [Type] -- type patterns to match against + , cab_rhs :: Type -- right-hand side of the equality } deriving Typeable _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
