Implement overlapping type family instances.

An ordered, overlapping type family instance is introduced by 'type
instance
where', followed by equations. See the new section in the user manual
(7.7.2.2) for details. The canonical example is Boolean equality at the
type
level:

type family Equals (a :: k) (b :: k) :: Bool
type instance where
  Equals a a = True
  Equals a b = False

A branched family instance, such as this one, checks its equations in
order
and applies only the first the matches. As explained in the note
[Instance
checking within groups] in FamInstEnv.lhs, we must be careful not to
simplify,
say, (Equals Int b) to False, because b might later unify with Int.

This commit includes all of the commits on the overlapping-tyfams
branch. SPJ
requested that I combine all my commits over the past several months
into one
monolithic commit. The following GHC repos are affected: ghc, testsuite,
utils/haddock, libraries/template-haskell, and libraries/dph.

Here are some details for the interested:

- The definition of CoAxiom has been moved from TyCon.lhs to a
  new file CoAxiom.lhs. I made this decision because of the
  number of definitions necessary to support BranchList.

- BranchList is a GADT whose type tracks whether it is a
  singleton list or not-necessarily-a-singleton-list. The reason
  I introduced this type is to increase static checking of places
  where GHC code assumes that a FamInst or CoAxiom is indeed a
  singleton. This assumption takes place roughly 10 times
  throughout the code. I was worried that a future change to GHC
  would invalidate the assumption, and GHC might subtly fail to
  do the right thing. By explicitly labeling CoAxioms and
  FamInsts as being Unbranched (singleton) or
  Branched (not-necessarily-singleton), we make this assumption
  explicit and checkable. Furthermore, to enforce the accuracy of
  this label, the list of branches of a CoAxiom or FamInst is
  stored using a BranchList, whose constructors constrain its
  type index appropriately.

I think that the decision to use BranchList is probably the most
controversial decision I made from a code design point of view.
Although I provide conversions to/from ordinary lists, it is more
efficient to use the brList... functions provided in CoAxiom than
always to convert. The use of these functions does not wander far
from the core CoAxiom/FamInst logic.

BranchLists are motivated and explained in the note [Branched axioms] in
CoAxiom.lhs.

- The CoAxiom type has changed significantly. You can see the new
  type in CoAxiom.lhs. It uses a CoAxBranch type to track
  branches of the CoAxiom. Correspondingly various functions
  producing and consuming CoAxioms had to change, including the
  binary layout of interface files.

- To get branched axioms to work correctly, it is important to have a
  notion
  of type "apartness": two types are apart if they cannot unify, and no
  substitution of variables can ever get them to unify, even after type
family
  simplification. (This is different than the normal failure to unify
because
  of the type family bit.) This notion in encoded in tcApartTys, in
Unify.lhs.
  Because apartness is finer-grained than unification, the tcUnifyTys
now
  calls tcApartTys.

- CoreLinting axioms has been updated, both to reflect the new
  form of CoAxiom and to enforce the apartness rules of branch
  application. The formalization of the new rules is in
  docs/core-spec/core-spec.pdf.

- The FamInst type (in types/FamInstEnv.lhs) has changed
  significantly, paralleling the changes to CoAxiom. Of course,
  this forced minor changes in many files.

- There are several new Notes in FamInstEnv.lhs, including one
  discussing confluent overlap and why we're not doing it.

- lookupFamInstEnv, lookupFamInstEnvConflicts, and
  lookup_fam_inst_env' (the function that actually does the work)
  have all been more-or-less completely rewritten. There is a
  Note [lookup_fam_inst_env' implementation] describing the
  implementation. One of the changes that affects other files is
  to change the type of matches from a pair of (FamInst, [Type])
  to a new datatype (which now includes the index of the matching
  branch). This seemed a better design.

- The TySynInstD constructor in Template Haskell was updated to
  use the new datatype TySynEqn. I also bumped the TH version
  number, requiring changes to DPH cabal files. (That's why the
  DPH repo has an overlapping-tyfams branch.)

- As SPJ requested, I refactored some of the code in HsDecls:

 * splitting up TyDecl into SynDecl and DataDecl, correspondingly
   changing HsTyDefn to HsDataDefn (with only one constructor)

 * splitting FamInstD into TyFamInstD and DataFamInstD and
   splitting FamInstDecl into DataFamInstDecl and TyFamInstDecl

 * making the ClsInstD take a ClsInstDecl, for parallelism with
   InstDecl's other constructors

 * changing constructor TyFamily into FamDecl

 * creating a FamilyDecl type that stores the details for a family
   declaration; this is useful because FamilyDecls can appear in classes
but
   other decls cannot

 * restricting the associated types and associated type defaults for a
 * class
   to be the new, more restrictive types

 * splitting cid_fam_insts into cid_tyfam_insts and cid_datafam_insts,
   according to the new types

 * perhaps one or two more that I'm overlooking

None of these changes has far-reaching implications.

- The user manual, section 7.7.2.2, is updated to describe the new type
  family
  instances.

9 files changed, 47 insertions, 34 deletions

diff --git a/compiler/vectorise/Vectorise.hs b/compiler/vectorise/Vectorise.hs
index 8b7e817826..1d71dd7340 100644
--- a/compiler/vectorise/Vectorise.hs
+++ b/compiler/vectorise/Vectorise.hs
@@ -30,6 +30,7 @@ import BasicTypes           ( isStrongLoopBreaker )
 import Outputable
 import Util                 ( zipLazy )
 import MonadUtils
+import FamInstEnv           ( toBranchedFamInst )
 
 import Control.Monad
 import Data.Maybe
@@ -97,7 +98,7 @@ vectModule guts@(ModGuts { mg_tcs        = tycons
                         -- and dfuns
                       , mg_binds        = Rec tc_binds : (binds_top ++ binds_imp)
                       , mg_fam_inst_env = fam_inst_env
-                      , mg_fam_insts    = fam_insts ++ new_fam_insts
+                      , mg_fam_insts    = fam_insts ++ (map toBranchedFamInst new_fam_insts)
                       }
       }
 
diff --git a/compiler/vectorise/Vectorise/Env.hs b/compiler/vectorise/Vectorise/Env.hs
index a887e7736f..b23093e049 100644
--- a/compiler/vectorise/Vectorise/Env.hs
+++ b/compiler/vectorise/Vectorise/Env.hs
@@ -184,7 +184,7 @@ extendImportedVarsEnv ps genv
 
 -- |Extend the list of type family instances.
 --
-extendFamEnv :: [FamInst] -> GlobalEnv -> GlobalEnv
+extendFamEnv :: [FamInst Unbranched] -> GlobalEnv -> GlobalEnv
 extendFamEnv new genv
   = genv { global_fam_inst_env = (g_fam_inst, extendFamInstEnvList l_fam_inst new) }
   where (g_fam_inst, l_fam_inst) = global_fam_inst_env genv
diff --git a/compiler/vectorise/Vectorise/Generic/PADict.hs b/compiler/vectorise/Vectorise/Generic/PADict.hs
index da95884326..f70e796daa 100644
--- a/compiler/vectorise/Vectorise/Generic/PADict.hs
+++ b/compiler/vectorise/Vectorise/Generic/PADict.hs
@@ -15,6 +15,7 @@ import CoreUtils
 import CoreUnfold
 import Module
 import TyCon
+import CoAxiom
 import Type
 import Id
 import Var
@@ -47,7 +48,8 @@ import FastString
 --
 buildPADict
         :: TyCon        -- ^ tycon of the type being vectorised.
-        -> CoAxiom      -- ^ Coercion between the type and 
+        -> CoAxiom Unbranched
+                        -- ^ Coercion between the type and 
                         --     its vectorised representation.
         -> TyCon        -- ^ PData  instance tycon
         -> TyCon        -- ^ PDatas instance tycon
diff --git a/compiler/vectorise/Vectorise/Generic/PAMethods.hs b/compiler/vectorise/Vectorise/Generic/PAMethods.hs
index 61c07cd299..77880a6740 100644
--- a/compiler/vectorise/Vectorise/Generic/PAMethods.hs
+++ b/compiler/vectorise/Vectorise/Generic/PAMethods.hs
@@ -18,6 +18,7 @@ import CoreUtils
 import FamInstEnv
 import MkCore            ( mkWildCase )
 import TyCon
+import CoAxiom
 import Type
 import OccName
 import Coercion
@@ -30,12 +31,12 @@ import Control.Monad
 import Outputable
 
 
-buildPReprTyCon :: TyCon -> TyCon -> SumRepr -> VM FamInst
+buildPReprTyCon :: TyCon -> TyCon -> SumRepr -> VM (FamInst Unbranched)
 buildPReprTyCon orig_tc vect_tc repr
  = do name      <- mkLocalisedName mkPReprTyConOcc (tyConName orig_tc)
       rhs_ty    <- sumReprType repr
       prepr_tc  <- builtin preprTyCon
-      return $ mkSynFamInst name tyvars prepr_tc instTys rhs_ty
+      return $ mkSingleSynFamInst name tyvars prepr_tc instTys rhs_ty
   where
     tyvars = tyConTyVars vect_tc
     instTys = [mkTyConApp vect_tc . mkTyVarTys $ tyConTyVars vect_tc]
@@ -59,7 +60,8 @@ buildPReprTyCon orig_tc vect_tc repr
 --
 type PAInstanceBuilder
         =  TyCon        -- ^ Vectorised TyCon 
-        -> CoAxiom      -- ^ Coercion to the representation TyCon
+        -> CoAxiom Unbranched
+                        -- ^ Coercion to the representation TyCon
         -> TyCon        -- ^ 'PData'  TyCon
         -> TyCon        -- ^ 'PDatas' TyCon
         -> SumRepr      -- ^ Description of generic representation.
@@ -95,7 +97,7 @@ buildToPRepr vect_tc repr_ax _ _ repr
   where
     ty_args        = mkTyVarTys (tyConTyVars vect_tc)
 
-    wrap_repr_inst = wrapTypeFamInstBody repr_ax ty_args
+    wrap_repr_inst = wrapTypeUnbranchedFamInstBody repr_ax ty_args
 
     -- CoreExp to convert the given argument to the generic representation.
     -- We start by doing a case branch on the possible data constructors.
@@ -158,7 +160,7 @@ buildFromPRepr vect_tc repr_ax _ _ repr
       arg_ty <- mkPReprType res_ty
       arg <- newLocalVar (fsLit "x") arg_ty
 
-      result <- from_sum (unwrapTypeFamInstScrut repr_ax ty_args (Var arg))
+      result <- from_sum (unwrapTypeUnbranchedFamInstScrut repr_ax ty_args (Var arg))
                          repr
       return $ Lam arg result
   where
@@ -214,7 +216,7 @@ buildToArrPRepr vect_tc repr_co pdata_tc _ r
       pdata_co <- mkBuiltinCo pdataTyCon
       let co           = mkAppCo pdata_co
                        . mkSymCo
-                       $ mkAxInstCo repr_co ty_args
+                       $ mkUnbranchedAxInstCo repr_co ty_args
 
           scrut   = unwrapFamInstScrut pdata_tc ty_args (Var arg)
 
@@ -278,7 +280,7 @@ buildFromArrPRepr vect_tc repr_co pdata_tc _ r
 
       pdata_co <- mkBuiltinCo pdataTyCon
       let co           = mkAppCo pdata_co
-                       $ mkAxInstCo repr_co var_tys
+                       $ mkUnbranchedAxInstCo repr_co var_tys
 
       let scrut        = mkCast (Var arg) co
 
@@ -364,7 +366,7 @@ buildToArrPReprs vect_tc repr_co _ pdatas_tc r
     pdatas_co <- mkBuiltinCo pdatasTyCon
     let co           = mkAppCo pdatas_co
                      . mkSymCo
-                     $ mkAxInstCo repr_co ty_args
+                     $ mkUnbranchedAxInstCo repr_co ty_args
 
     let scrut        = unwrapFamInstScrut pdatas_tc ty_args (Var varg)
     (vars, result)  <- to_sum r
@@ -454,7 +456,7 @@ buildFromArrPReprs vect_tc repr_co _ pdatas_tc r
     -- Build the coercion between PRepr and the instance type
     pdatas_co <- mkBuiltinCo pdatasTyCon
     let co           = mkAppCo pdatas_co
-                     $ mkAxInstCo repr_co var_tys
+                     $ mkUnbranchedAxInstCo repr_co var_tys
 
     let scrut        = mkCast (Var varg) co
 
diff --git a/compiler/vectorise/Vectorise/Generic/PData.hs b/compiler/vectorise/Vectorise/Generic/PData.hs
index 49997f8502..0d3d650a1c 100644
--- a/compiler/vectorise/Vectorise/Generic/PData.hs
+++ b/compiler/vectorise/Vectorise/Generic/PData.hs
@@ -27,7 +27,7 @@ import Control.Monad
 
 -- buildPDataTyCon ------------------------------------------------------------
 -- | Build the PData instance tycon for a given type constructor.
-buildPDataTyCon :: TyCon -> TyCon -> SumRepr -> VM FamInst
+buildPDataTyCon :: TyCon -> TyCon -> SumRepr -> VM (FamInst Unbranched)
 buildPDataTyCon orig_tc vect_tc repr 
  = fixV $ \fam_inst ->
    do let repr_tc = dataFamInstRepTyCon fam_inst
@@ -38,7 +38,7 @@ buildPDataTyCon orig_tc vect_tc repr
  where
     orig_name = tyConName orig_tc
 
-buildDataFamInst :: Name -> TyCon -> TyCon -> AlgTyConRhs -> VM FamInst
+buildDataFamInst :: Name -> TyCon -> TyCon -> AlgTyConRhs -> VM (FamInst Unbranched)
 buildDataFamInst name' fam_tc vect_tc rhs
  = do { axiom_name <- mkDerivedName mkInstTyCoOcc name'
 
@@ -85,7 +85,7 @@ buildPDataDataCon orig_name vect_tc repr_tc repr
 
 -- buildPDatasTyCon -----------------------------------------------------------
 -- | Build the PDatas instance tycon for a given type constructor.
-buildPDatasTyCon :: TyCon -> TyCon -> SumRepr -> VM FamInst
+buildPDatasTyCon :: TyCon -> TyCon -> SumRepr -> VM (FamInst Unbranched)
 buildPDatasTyCon orig_tc vect_tc repr 
  = fixV $ \fam_inst ->
    do let repr_tc = dataFamInstRepTyCon fam_inst
diff --git a/compiler/vectorise/Vectorise/Monad/InstEnv.hs b/compiler/vectorise/Vectorise/Monad/InstEnv.hs
index fc12ee567c..0150415de9 100644
--- a/compiler/vectorise/Vectorise/Monad/InstEnv.hs
+++ b/compiler/vectorise/Vectorise/Monad/InstEnv.hs
@@ -56,12 +56,12 @@ lookupInst cls tys
 --
 -- which implies that :R42T was declared as 'data instance T [a]'.
 --
-lookupFamInst :: TyCon -> [Type] -> VM (FamInst, [Type])
+lookupFamInst :: TyCon -> [Type] -> VM FamInstMatch
 lookupFamInst tycon tys
   = ASSERT( isFamilyTyCon tycon )
     do { instEnv <- readGEnv global_fam_inst_env
        ; case lookupFamInstEnv instEnv tycon tys of
-           [(fam_inst, rep_tys)] -> return ( fam_inst, rep_tys)
+           [match] -> return match
            _other                -> 
              do dflags <- getDynFlags
                 cantVectorise dflags "VectMonad.lookupFamInst: not found: "
diff --git a/compiler/vectorise/Vectorise/Type/Env.hs b/compiler/vectorise/Vectorise/Type/Env.hs
index 5dfbaa5555..77aa8c5375 100644
--- a/compiler/vectorise/Vectorise/Type/Env.hs
+++ b/compiler/vectorise/Vectorise/Type/Env.hs
@@ -26,6 +26,7 @@ import CoreUtils
 import CoreUnfold
 import DataCon
 import TyCon
+import CoAxiom
 import Type
 import FamInstEnv
 import Id
@@ -139,12 +140,12 @@ import Data.List
 
 -- |Vectorise type constructor including class type constructors.
 --
-vectTypeEnv :: [TyCon]                  -- Type constructors defined in this module
-            -> [CoreVect]               -- All 'VECTORISE [SCALAR] type' declarations in this module
-            -> [CoreVect]               -- All 'VECTORISE class' declarations in this module
-            -> VM ( [TyCon]             -- old TyCons ++ new TyCons
-                  , [FamInst]           -- New type family instances.
-                  , [(Var, CoreExpr)])  -- New top level bindings.
+vectTypeEnv :: [TyCon]                   -- Type constructors defined in this module
+            -> [CoreVect]                -- All 'VECTORISE [SCALAR] type' declarations in this module
+            -> [CoreVect]                -- All 'VECTORISE class' declarations in this module
+            -> VM ( [TyCon]              -- old TyCons ++ new TyCons
+                  , [FamInst Unbranched] -- New type family instances.
+                  , [(Var, CoreExpr)])   -- New top level bindings.
 vectTypeEnv tycons vectTypeDecls vectClassDecls
   = do { traceVt "** vectTypeEnv" $ ppr tycons
 
@@ -339,7 +340,7 @@ vectTypeEnv tycons vectTypeDecls vectClassDecls
 
 -- Helpers --------------------------------------------------------------------
 
-buildTyConPADict :: TyCon -> CoAxiom -> TyCon -> TyCon -> VM Var
+buildTyConPADict :: TyCon -> CoAxiom Unbranched -> TyCon -> TyCon -> VM Var
 buildTyConPADict vect_tc prepr_ax pdata_tc pdatas_tc
  = tyConRepr vect_tc >>= buildPADict vect_tc prepr_ax pdata_tc pdatas_tc
 
diff --git a/compiler/vectorise/Vectorise/Utils/Base.hs b/compiler/vectorise/Vectorise/Utils/Base.hs
index a03875f116..d088f45355 100644
--- a/compiler/vectorise/Vectorise/Utils/Base.hs
+++ b/compiler/vectorise/Vectorise/Utils/Base.hs
@@ -39,6 +39,10 @@ import DataCon
 import MkId
 import DynFlags
 import FastString
+import Util
+import Panic
+
+#include "HsVersions.h"
 
 -- Simple Types ---------------------------------------------------------------
 
@@ -206,8 +210,11 @@ unwrapNewTypeBodyOfPDatasWrap e ty
 pdataReprTyCon :: Type -> VM (TyCon, [Type])
 pdataReprTyCon ty 
   = do 
-    { (famInst, tys) <- builtin pdataTyCon >>= (`lookupFamInst` [ty])
-    ; return (dataFamInstRepTyCon famInst, tys)
+    { FamInstMatch { fim_instance = famInst
+                   , fim_index    = index
+                   , fim_tys      = tys } <- builtin pdataTyCon >>= (`lookupFamInst` [ty])
+    ; ASSERT( index == 0 )
+      return (dataFamInstRepTyCon famInst, tys)
     }
 
 -- |Get the representation tycon of the 'PData' data family for a given type constructor.
@@ -231,8 +238,7 @@ pdataReprTyConExact tycon
 pdatasReprTyConExact :: TyCon -> VM TyCon
 pdatasReprTyConExact tycon
   = do {   -- look up the representation tycon; if there is a match at all, it will be be exact
-       ;   -- (i.e.,' _tys' will be distinct type variables)
-       ; (ptycon, _tys) <- pdatasReprTyCon (tycon `mkTyConApp` mkTyVarTys (tyConTyVars tycon))
+       ; (FamInstMatch { fim_instance = ptycon }) <- pdatasReprTyCon (tycon `mkTyConApp` mkTyVarTys (tyConTyVars tycon))
        ; return $ dataFamInstRepTyCon ptycon
        }
   where
@@ -254,5 +260,5 @@ pdataUnwrapScrut (ve, le)
 
 -- |Get the representation tycon of the 'PRepr' type family for a given type.
 --
-preprSynTyCon :: Type -> VM (FamInst, [Type])
+preprSynTyCon :: Type -> VM FamInstMatch
 preprSynTyCon ty = builtin preprTyCon >>= (`lookupFamInst` [ty])
diff --git a/compiler/vectorise/Vectorise/Utils/PADict.hs b/compiler/vectorise/Vectorise/Utils/PADict.hs
index 85060c477c..8029dfb466 100644
--- a/compiler/vectorise/Vectorise/Utils/PADict.hs
+++ b/compiler/vectorise/Vectorise/Utils/PADict.hs
@@ -17,6 +17,7 @@ import Coercion
 import Type
 import TypeRep
 import TyCon
+import CoAxiom
 import Var
 import Outputable
 import DynFlags
@@ -117,8 +118,8 @@ paMethod method _ ty
 prDictOfPReprInst :: Type -> VM CoreExpr
 prDictOfPReprInst ty
   = do
-    { (prepr_fam, prepr_args) <- preprSynTyCon ty
-    ; prDictOfPReprInstTyCon ty (famInstAxiom prepr_fam) prepr_args
+    { (FamInstMatch { fim_instance = prepr_fam, fim_tys = prepr_args }) <- preprSynTyCon ty
+    ; prDictOfPReprInstTyCon ty (famInstAxiom (toUnbranchedFamInst prepr_fam)) prepr_args
     }
 
 -- |Given a type @ty@, its PRepr synonym tycon and its type arguments,
@@ -136,15 +137,15 @@ prDictOfPReprInst ty
 --
 -- Note that @ty@ is only used for error messages
 --
-prDictOfPReprInstTyCon :: Type -> CoAxiom -> [Type] -> VM CoreExpr
+prDictOfPReprInstTyCon :: Type -> CoAxiom Unbranched -> [Type] -> VM CoreExpr
 prDictOfPReprInstTyCon _ty prepr_ax prepr_args
   = do
-      let rhs = mkAxInstRHS prepr_ax prepr_args
+      let rhs = mkUnbranchedAxInstRHS prepr_ax prepr_args
       dict <- prDictOfReprType' rhs
       pr_co <- mkBuiltinCo prTyCon
       let co = mkAppCo pr_co
              $ mkSymCo
-             $ mkAxInstCo prepr_ax prepr_args
+             $ mkUnbranchedAxInstCo prepr_ax prepr_args
       return $ mkCast dict co
 
 -- |Get the PR dictionary for a type. The argument must be a representation