More refactoring of FamInst/FamInstEnv; finally fixes Trac #7524
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 28 Jan 2013 08:18:28 +0000 (08:18 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 28 Jan 2013 08:18:28 +0000 (08:18 +0000)
Quite a bit of tidying up here; the fix to #7524 is actually
only a small part.

* Be fully clear that the cab_tvs in a CoAxBranch are not
  fresh.  See Note [CoAxBranch type variables] in CoAxiom.

* Use CoAxBranch to replace the ATDfeault type in Class.
  CoAxBranch is perfect here.  This change allowed me to
  delete quite a bit of boilerplate code, including the
  corresponding IfaceSynType.

* Tidy up the construction of CoAxBranches, and when FamIntBranch is
  freshened.  The latter onw happens only in FamInst.newFamInst.

* Tidy the tyvars of a CoAxBranch when we build them, done in
  FamInst.mkCoAxBranch.  See Note [Tidy axioms when we build them]
  in that module.  This is what fixes #7524.

Much niceer now.

15 files changed:
compiler/iface/BinIface.hs
compiler/iface/IfaceSyn.lhs
compiler/iface/MkIface.lhs
compiler/iface/TcIface.lhs
compiler/typecheck/FamInst.lhs
compiler/typecheck/TcGenGenerics.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcRnDriver.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/types/Class.lhs
compiler/types/CoAxiom.lhs
compiler/types/Coercion.lhs
compiler/types/FamInstEnv.lhs
compiler/vectorise/Vectorise/Generic/PAMethods.hs
compiler/vectorise/Vectorise/Generic/PData.hs

index ac244fa..7f9b24e 100644 (file)
@@ -1426,13 +1426,6 @@ instance Binary IfaceAT where
         defs <- get bh
         return (IfaceAT dec defs)
 
-instance Binary IfaceATDefault where
-    put_ bh (IfaceATD tvs pat_tys ty) = do
-        put_ bh tvs
-        put_ bh pat_tys
-        put_ bh ty
-    get bh = liftM3 IfaceATD (get bh) (get bh) (get bh)
-
 instance Binary IfaceClassOp where
     put_ bh (IfaceClassOp n def ty) = do 
         put_ bh (occNameFS n)
index 8ba5e86..d8b3b95 100644 (file)
@@ -14,7 +14,7 @@
 module IfaceSyn (
         module IfaceType,
 
-        IfaceDecl(..), IfaceClassOp(..), IfaceAT(..), IfaceATDefault(..),
+        IfaceDecl(..), IfaceClassOp(..), IfaceAT(..), 
         IfaceConDecl(..), IfaceConDecls(..),
         IfaceExpr(..), IfaceAlt, IfaceLetBndr(..),
         IfaceBinding(..), IfaceConAlt(..),
@@ -118,15 +118,13 @@ data IfaceClassOp = IfaceClassOp OccName DefMethSpec IfaceType
         -- Just False => ordinary polymorphic default method
         -- Just True  => generic default method
 
-data IfaceAT = IfaceAT IfaceDecl [IfaceATDefault]
+data IfaceAT = IfaceAT IfaceDecl [IfaceAxBranch]
         -- Nothing => no default associated type instance
         -- Just ds => default associated type instance from these templates
 
-data IfaceATDefault = IfaceATD [IfaceTvBndr] [IfaceType] IfaceType
-        -- Each associated type default template is a triple of:
-        --   1. TyVars of the RHS and family arguments (including the class TVs)
-        --   3. The instantiated family arguments
-        --   2. The RHS of the synonym
+instance Outputable IfaceAxBranch where
+   ppr (IfaceAxBranch { ifaxbTyVars = tvs, ifaxbLHS = pat_tys, ifaxbRHS = ty }) 
+      = ppr tvs <+> hsep (map ppr pat_tys) <+> char '=' <+> ppr ty
 
 -- this is just like CoAxBranch
 data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr]
@@ -538,11 +536,10 @@ pprIfaceDecl (IfaceClass {ifCtxt = context, ifName = clas, ifTyVars = tyvars,
 
 pprIfaceDecl (IfaceAxiom {ifName = name, ifTyCon = tycon, ifAxBranches = branches })
   = hang (ptext (sLit "axiom") <+> ppr name <> colon)
-       2 (vcat $ map (pprIfaceAxBranch tycon) branches)
-
-pprIfaceAxBranch :: IfaceTyCon -> IfaceAxBranch -> SDoc
-pprIfaceAxBranch tc (IfaceAxBranch { ifaxbTyVars = tyvars, ifaxbLHS = lhs, ifaxbRHS = rhs })
-  = pprIfaceTvBndrs tyvars <> dot <+> ppr (IfaceTyConApp tc lhs) <+> text "~#" <+> ppr rhs
+       2 (vcat $ map ppr_branch branches)
+  where
+     ppr_branch (IfaceAxBranch { ifaxbTyVars = tyvars, ifaxbLHS = lhs, ifaxbRHS = rhs })
+        = pprIfaceTvBndrs tyvars <> dot <+> ppr (IfaceTyConApp tycon lhs) <+> text "~#" <+> ppr rhs
 
 pprCType :: Maybe CType -> SDoc
 pprCType Nothing = ptext (sLit "No C type associated")
@@ -561,9 +558,6 @@ instance Outputable IfaceClassOp where
 instance Outputable IfaceAT where
    ppr (IfaceAT d defs) = hang (ppr d) 2 (vcat (map ppr defs))
 
-instance Outputable IfaceATDefault where
-   ppr (IfaceATD tvs pat_tys ty) = ppr tvs <+> hsep (map ppr pat_tys) <+> char '=' <+> ppr ty
-
 pprIfaceDeclHead :: IfaceContext -> OccName -> [IfaceTvBndr] -> SDoc
 pprIfaceDeclHead context thing tyvars
   = hsep [pprIfaceContext context, parenSymOcc thing (ppr thing),
@@ -837,12 +831,7 @@ freeNamesIfContext = fnList freeNamesIfType
 freeNamesIfAT :: IfaceAT -> NameSet
 freeNamesIfAT (IfaceAT decl defs)
   = freeNamesIfDecl decl &&&
-    fnList fn_at_def defs
-  where
-    fn_at_def (IfaceATD tvs pat_tys ty)
-      = freeNamesIfTvBndrs tvs &&&
-        fnList freeNamesIfType pat_tys &&&
-        freeNamesIfType ty
+    fnList freeNamesIfAxBranch defs
 
 freeNamesIfClsSig :: IfaceClassOp -> NameSet
 freeNamesIfClsSig (IfaceClassOp _n _dm ty) = freeNamesIfType ty
index f145ec1..5297e83 100644 (file)
@@ -1444,18 +1444,18 @@ coAxiomToIfaceDecl :: CoAxiom br -> IfaceDecl
 coAxiomToIfaceDecl ax@(CoAxiom { co_ax_tc = tycon, co_ax_branches = branches })
  = IfaceAxiom { ifName       = name
               , ifTyCon      = toIfaceTyCon tycon
-              , ifAxBranches = brListMap coAxBranchToIfaceBranch branches }
+              , ifAxBranches = brListMap (coAxBranchToIfaceBranch emptyTidyEnv) branches }
  where
    name = getOccName ax
 
 
-coAxBranchToIfaceBranch :: CoAxBranch -> IfaceAxBranch
-coAxBranchToIfaceBranch (CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs })
+coAxBranchToIfaceBranch :: TidyEnv -> CoAxBranch -> IfaceAxBranch
+coAxBranchToIfaceBranch env0 (CoAxBranch { cab_tvs = tvs, cab_lhs = lhs, cab_rhs = rhs })
   = IfaceAxBranch { ifaxbTyVars = toIfaceTvBndrs tv_bndrs
-                  , ifaxbLHS    = map (tidyToIfaceType env) lhs
-                  , ifaxbRHS    = tidyToIfaceType env rhs }
+                  , ifaxbLHS    = map (tidyToIfaceType env1) lhs
+                  , ifaxbRHS    = tidyToIfaceType env1 rhs }
   where
-    (env, tv_bndrs) = tidyTyVarBndrs emptyTidyEnv tvs
+    (env1, tv_bndrs) = tidyTyVarBndrs env0 tvs
 
 -----------------
 tyConToIfaceDecl :: TidyEnv -> TyCon -> IfaceDecl
@@ -1549,14 +1549,7 @@ classToIfaceDecl env clas
     
     toIfaceAT :: ClassATItem -> IfaceAT
     toIfaceAT (tc, defs)
-      = IfaceAT (tyConToIfaceDecl env1 tc) (map to_if_at_def defs)
-      where
-        to_if_at_def (ATD tvs pat_tys ty _loc)
-          = IfaceATD (toIfaceTvBndrs tvs') 
-                     (map (tidyToIfaceType env2) pat_tys) 
-                     (tidyToIfaceType env2 ty)
-          where
-            (env2, tvs') = tidyTyClTyVarBndrs env1 tvs
+      = IfaceAT (tyConToIfaceDecl env1 tc) (map (coAxBranchToIfaceBranch env1) defs)
 
     toIfaceClassOp (sel_id, def_meth)
         = ASSERT(sel_tyvars == clas_tyvars)
index 3ef0ddc..947e4f1 100644 (file)
@@ -525,14 +525,9 @@ tc_iface_decl _parent ignore_prags
 
    tc_at cls (IfaceAT tc_decl defs_decls)
      = do ATyCon tc <- tc_iface_decl (AssocFamilyTyCon cls) ignore_prags tc_decl
-          defs <- mapM tc_iface_at_def defs_decls
+          defs <- mapM tc_ax_branch defs_decls
           return (tc, defs)
 
-   tc_iface_at_def (IfaceATD tvs pat_tys ty) =
-       bindIfaceTyVars_AT tvs $
-         \tvs' -> liftM2 (\pats tys -> ATD tvs' pats tys noSrcSpan)
-                           (mapM tcIfaceType pat_tys) (tcIfaceType ty)
-
    mk_op_doc op_name op_ty = ptext (sLit "Class op") <+> sep [ppr op_name, ppr op_ty]
 
    tc_fd (tvs1, tvs2) = do { tvs1' <- mapM tcIfaceTyVar tvs1
@@ -547,23 +542,23 @@ tc_iface_decl _ _ (IfaceForeign {ifName = rdr_name, ifExtName = ext_name})
 tc_iface_decl _ _ (IfaceAxiom {ifName = ax_occ, ifTyCon = tc, ifAxBranches = branches})
   = do { tc_name     <- lookupIfaceTop ax_occ
        ; tc_tycon    <- tcIfaceTyCon tc
-       ; tc_branches <- mapM tc_branch branches
+       ; tc_branches <- mapM tc_ax_branch branches
        ; let axiom = CoAxiom { co_ax_unique   = nameUnique tc_name
                              , co_ax_name     = tc_name
                              , co_ax_tc       = tc_tycon
                              , co_ax_branches = toBranchList tc_branches
                              , co_ax_implicit = False }
        ; return (ACoAxiom axiom) }
-  where tc_branch :: IfaceAxBranch -> IfL CoAxBranch
-        tc_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs, ifaxbLHS = lhs, ifaxbRHS = rhs })
-          = bindIfaceTyVars tv_bndrs $ \ tvs -> do
-            { tc_lhs <- mapM tcIfaceType lhs
-            ; tc_rhs <- tcIfaceType rhs
-            ; let branch = CoAxBranch { cab_loc = noSrcSpan
-                                      , cab_tvs = tvs
-                                      , cab_lhs = tc_lhs
-                                      , cab_rhs = tc_rhs }
-            ; return branch }
+
+tc_ax_branch :: IfaceAxBranch -> IfL CoAxBranch
+tc_ax_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs, ifaxbLHS = lhs, ifaxbRHS = rhs })
+  = bindIfaceTyVars tv_bndrs $ \ tvs -> do  -- Variables will all be fresh
+    { tc_lhs <- mapM tcIfaceType lhs
+    ; tc_rhs <- tcIfaceType rhs
+    ; return (CoAxBranch { cab_loc = noSrcSpan
+                         , cab_tvs = tvs
+                         , cab_lhs = tc_lhs
+                         , cab_rhs = tc_rhs } ) }
 
 tcIfaceDataCons :: Name -> TyCon -> [TyVar] -> IfaceConDecls -> IfL AlgTyConRhs
 tcIfaceDataCons tycon_name tycon _ if_cons
index f667cd5..c6a7eaf 100644 (file)
@@ -1,6 +1,7 @@
 The @FamInst@ type: family instance heads
 
 \begin{code}
+{-# LANGUAGE GADTs #-}
 {-# OPTIONS -fno-warn-tabs #-}
 -- The above warning supression flag is a temporary kludge.
 -- While working on this module you are encouraged to remove it and
@@ -12,20 +13,19 @@ module FamInst (
         checkFamInstConsistency, tcExtendLocalFamInstEnv,
        tcLookupFamInst, tcLookupDataFamInst,
         tcGetFamInstEnvs,
-
-        freshenFamInstEqn, freshenFamInstEqnLoc,
-        mkFreshenedSynInst, mkFreshenedSynInstLoc
+        newFamInst,
+        mkCoAxBranch, mkBranchedCoAxiom, mkSingleCoAxiom
     ) where
 
 import HscTypes
 import FamInstEnv
+import InstEnv( roughMatchTcs )
 import LoadIface
 import TypeRep
 import TcRnMonad
 import TyCon
 import CoAxiom
 import DynFlags
-import SrcLoc
 import Module
 import Outputable
 import UniqFM
@@ -33,7 +33,10 @@ import FastString
 import Util
 import Maybes
 import TcMType
+import TcType
+import VarEnv( emptyTidyEnv )
 import Type
+import SrcLoc
 import Name
 import Control.Monad
 import Data.Map (Map)
@@ -42,6 +45,47 @@ import qualified Data.Map as Map
 #include "HsVersions.h"
 \end{code}
 
+%************************************************************************
+%*                                                                     *
+                 Making a FamInst
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+-- All type variables in a FamInst must be fresh. This function
+-- creates the fresh variables and applies the necessary substitution
+-- It is defined here to avoid a dependency from FamInstEnv on the monad
+-- code.
+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 })
+  = 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_axiom    = axiom }) }
+  where
+    go :: BranchList CoAxBranch br -> TcRnIf gbl lcl (BranchList FamInstBranch br)
+    go (FirstBranch br) = do { br' <- go_branch br
+                             ; return (FirstBranch br') }
+    go (NextBranch br brs) = do { br' <- go_branch br
+                                ; brs' <- go brs
+                                ;return (NextBranch br' brs') }
+    go_branch :: CoAxBranch -> TcRnIf gbl lcl FamInstBranch 
+    go_branch (CoAxBranch { cab_tvs = tvs1
+                          , cab_lhs = lhs
+                          , cab_loc = loc
+                          , cab_rhs = rhs })
+       = do { (subst, tvs2) <- tcInstSkolTyVarsLoc loc tvs1
+            ; return (FamInstBranch { fib_tvs   = tvs2
+                                    , fib_lhs   = substTys subst lhs
+                                    , fib_rhs   = substTy  subst rhs
+                                    , fib_tcs   = roughMatchTcs lhs }) }
+\end{code}
+
 
 %************************************************************************
 %*                                                                     *
@@ -350,51 +394,53 @@ tcGetFamInstEnvs
 \end{code}
 
 %************************************************************************
-%*                                                                     *
-       Freshening type variables
-%*                                                                     *
+%*                                                                      *
+           Constructing axioms
+    These functions are here because tidyType etc 
+    are not available in CoAxiom
+%*                                                                      *
 %************************************************************************
 
+Note [Tidy axioms when we build them]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We print out axioms and don't want to print stuff like
+    F k k a b = ...
+Instead we must tidy those kind variables.  See Trac #7524.
+
+
 \begin{code}
+mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
+             -> [Type]  -- LHS patterns
+             -> Type    -- RHS
+             -> SrcSpan
+             -> CoAxBranch
+mkCoAxBranch tvs lhs rhs loc
+  = CoAxBranch { cab_tvs = tvs1
+               , cab_lhs = tidyTypes env lhs
+               , cab_rhs = tidyType  env rhs
+               , cab_loc = loc }
+  where
+    (env, tvs1) = tidyTyVarBndrs emptyTidyEnv tvs
+    -- See Note [Tidy axioms when we build them]
+  
+
+mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
+mkBranchedCoAxiom ax_name fam_tc branches
+  = CoAxiom { co_ax_unique   = nameUnique ax_name
+            , co_ax_name     = ax_name
+            , co_ax_tc       = fam_tc
+            , co_ax_implicit = False
+            , co_ax_branches = toBranchList branches }
+
+mkSingleCoAxiom :: Name -> [TyVar] -> TyCon -> [Type] -> Type -> CoAxiom Unbranched
+mkSingleCoAxiom ax_name tvs fam_tc lhs_tys rhs_ty
+  = CoAxiom { co_ax_unique   = nameUnique ax_name
+            , co_ax_name     = ax_name
+            , co_ax_tc       = fam_tc
+            , co_ax_implicit = False
+            , co_ax_branches = FirstBranch branch }
+  where
+    branch = mkCoAxBranch tvs lhs_tys rhs_ty (getSrcSpan ax_name)
+\end{code}
+
 
--- All type variables in a FamInst/CoAxiom must be fresh. This function
--- creates the fresh variables and applies the necessary substitution
--- It is defined here to avoid a dependency from FamInstEnv on the monad
--- code.
-freshenFamInstEqn :: [TyVar] -- original, possibly stale, tyvars
-                  -> [Type]  -- LHS patterns
-                  -> Type    -- RHS
-                  -> TcM ([TyVar], [Type], Type)
-freshenFamInstEqn tvs lhs rhs
-  = do { loc <- getSrcSpanM
-       ; freshenFamInstEqnLoc loc tvs lhs rhs }
-
--- freshenFamInstEqn needs to be called outside the TcM monad:
-freshenFamInstEqnLoc :: SrcSpan
-                     -> [TyVar] -> [Type] -> Type
-                     -> TcRnIf gbl lcl ([TyVar], [Type], Type)
-freshenFamInstEqnLoc loc tvs lhs rhs
-  = do { (subst, tvs') <- tcInstSkolTyVarsLoc loc tvs
-       ; let lhs' = substTys subst lhs
-             rhs' = substTy  subst rhs
-       ; return (tvs', lhs', rhs') }
-
--- Makes an unbranched synonym FamInst, with freshened tyvars
-mkFreshenedSynInst :: Name    -- Unique name for the coercion tycon
-                   -> [TyVar] -- possibly stale tyvars of the coercion
-                   -> TyCon   -- Family tycon
-                   -> [Type]  -- LHS patterns
-                   -> Type    -- RHS
-                   -> TcM (FamInst Unbranched)
-mkFreshenedSynInst name tvs fam_tc inst_tys rep_ty
-  = do { loc <- getSrcSpanM
-       ; mkFreshenedSynInstLoc loc name tvs fam_tc inst_tys rep_ty }
-
-mkFreshenedSynInstLoc :: SrcSpan
-                      -> Name -> [TyVar] -> TyCon -> [Type] -> Type
-                      -> TcRnIf gbl lcl (FamInst Unbranched)
-mkFreshenedSynInstLoc loc name tvs fam_tc inst_tys rep_ty
-  = do { (tvs', inst_tys', rep_ty') <- freshenFamInstEqnLoc loc tvs inst_tys rep_ty
-       ; return $ mkSingleSynFamInst name tvs' fam_tc inst_tys' rep_ty' }
-
-\end{code}
\ No newline at end of file
index 3095dac..77bac8f 100644 (file)
@@ -28,7 +28,7 @@ import TcGenDeriv
 import DataCon
 import TyCon
 import CoAxiom
-import FamInstEnv       ( FamInst )
+import FamInstEnv       ( FamInst, FamFlavor(..) )
 import FamInst
 import Module           ( Module, moduleName, moduleNameString )
 import IfaceEnv         ( newGlobalBinder )
@@ -419,7 +419,7 @@ tc_mkRepFamInsts gk tycon metaDts mod =
        -- Also consider `R:DInt`, where { data family D x y :: * -> *
        --                               ; data instance D Int a b = D_ a }
   do { -- `rep` = GHC.Generics.Rep or GHC.Generics.Rep1 (type family)
-       rep <- case gk of
+       fam_tc <- case gk of
          Gen0 -> tcLookupTyCon repTyConName
          Gen1 -> tcLookupTyCon rep1TyConName
 
@@ -432,6 +432,7 @@ tc_mkRepFamInsts gk tycon metaDts mod =
 
            tyvar_args = mkTyVarTys tyvars
 
+           appT :: [Type]
            appT = case tyConFamInst_maybe tycon of
                      -- `appT` = D Int a b (data families case)
                      Just (famtycon, apps) ->
@@ -452,8 +453,8 @@ tc_mkRepFamInsts gk tycon metaDts mod =
                    in newGlobalBinder mod (mkGen (nameOccName (tyConName tycon)))
                         (nameSrcSpan (tyConName tycon))
 
-     ; mkFreshenedSynInst rep_name tyvars rep appT repTy
-     }
+     ; let axiom = mkSingleCoAxiom rep_name tyvars fam_tc appT repTy
+     ; newFamInst SynFamilyInst False axiom  }
 
 --------------------------------------------------------------------------------
 -- Type representation
index 26b6c75..46090f8 100644 (file)
@@ -531,14 +531,15 @@ tcClsInstDecl (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                  --            instance C [x]
                  -- Then we want to generate the decl:   type F [x] b = ()
                 | otherwise 
-                = forM defs $ \(ATD _tvs pat_tys rhs _loc) ->
+                = forM defs $ \(CoAxBranch { cab_lhs = pat_tys, cab_rhs = rhs }) ->
                   do { let pat_tys' = substTys mini_subst pat_tys
                            rhs'     = substTy  mini_subst rhs
                            tv_set'  = tyVarsOfTypes pat_tys'
                            tvs'     = varSetElems tv_set'
                      ; rep_tc_name <- newFamInstTyConName (noLoc (tyConName fam_tc)) pat_tys'
+                     ; let axiom = mkSingleCoAxiom rep_tc_name tvs' fam_tc pat_tys' rhs'
                      ; ASSERT( tyVarsOfType rhs' `subVarSet` tv_set' ) 
-                       mkFreshenedSynInst rep_tc_name tvs' fam_tc pat_tys' rhs' }
+                       newFamInst SynFamilyInst False {- group -} axiom }
 
         ; tyfam_insts1 <- mapM mk_deflt_at_instances (classATItems clas)
         
@@ -622,38 +623,29 @@ tcTyFamInstDecl mb_clsinfo fam_tc (L loc decl@(TyFamInstDecl { tfid_group = grou
                  (notOpenFamily fam_tc)
 
          -- (1) do the work of verifying the synonym group
-       ; quads <- tcSynFamInstDecl fam_tc decl
+       ; co_ax_branches <- tcSynFamInstDecl fam_tc decl
 
-         -- (2) create the branches
-       ; co_ax_branches <- mapM check_valid_mk_branch quads
+         -- (2) check for validity and inaccessibility
+       ; mapM_   check_valid_mk_branch co_ax_branches
+       ; foldlM_ check_inaccessible_branches [] co_ax_branches
 
-         -- (3) construct coercion tycon
+         -- (3) construct coercion axiom
        ; rep_tc_name <- newFamInstAxiomName loc
                                             (tyFamInstDeclName decl)
-                                            (get_typats quads)
-
-         -- (4) check to see if earlier equations dominate a later one
-       ; foldlM_ check_inaccessible_branches [] co_ax_branches
-
-         -- now, build the FamInst
-       ; return $ mkSynFamInst rep_tc_name fam_tc group co_ax_branches }
-
+                                            (map cab_lhs co_ax_branches)
+       ; let axiom = mkBranchedCoAxiom rep_tc_name fam_tc co_ax_branches
+       ; newFamInst SynFamilyInst group axiom }
     where 
-      check_valid_mk_branch :: ([TyVar], [Type], Type, SrcSpan)
-                            -> TcM CoAxBranch
-      check_valid_mk_branch (t_tvs, t_typats, t_rhs, loc)
+      check_valid_mk_branch :: CoAxBranch -> TcM ()
+      check_valid_mk_branch (CoAxBranch { cab_tvs = t_tvs, cab_lhs = t_typats
+                                        , cab_rhs = t_rhs, cab_loc = loc })
         = setSrcSpan loc $
           do { -- check the well-formedness of the instance
                checkValidTyFamInst fam_tc t_tvs t_typats t_rhs
 
                -- check that type patterns match the class instance head
-             ; tcAssocFamInst mb_clsinfo loc (ptext (sLit "type")) fam_tc t_typats
-
-               -- make fresh tyvars for axiom
-             ; (t_tvs', t_typats', t_rhs')
-                 <- freshenFamInstEqn t_tvs t_typats t_rhs
+             ; tcAssocFamInst mb_clsinfo loc (ptext (sLit "type")) fam_tc t_typats }
 
-             ; return $ mkCoAxBranch loc t_tvs' t_typats' t_rhs' }
 
       check_inaccessible_branches :: [CoAxBranch]     -- previous
                                   -> CoAxBranch       -- current
@@ -665,8 +657,6 @@ tcTyFamInstDecl mb_clsinfo fam_tc (L loc decl@(TyFamInstDecl { tfid_group = grou
                     addErrTc $ inaccessibleCoAxBranch fam_tc cur_branch
              ; return $ cur_branch : prev_branches }
 
-      get_typats = map (\(_, tys, _, _) -> tys)
-
 tcDataFamInstDecl :: Maybe (Class, VarEnv Type)
                   -> TyCon -> LDataFamInstDecl Name -> TcM (FamInst Unbranched)
   -- "newtype instance" and "data instance"
@@ -710,11 +700,10 @@ tcDataFamInstDecl mb_clsinfo fam_tc
                      NewType  -> ASSERT( not (null data_cons) )
                                  mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
               -- freshen tyvars
-              ; (subst, tvs'') <- tcInstSkolTyVars tvs'
-              ; let pats''   = substTys subst pats'
-                    fam_inst = mkDataFamInst axiom_name tvs'' fam_tc pats'' rep_tc
-                    parent   = FamInstTyCon (famInstAxiom fam_inst) fam_tc pats''
-                    rep_tc   = buildAlgTyCon rep_tc_name tvs'' cType stupid_theta tc_rhs 
+              ; let axiom    = mkSingleCoAxiom axiom_name tvs' fam_tc pats' 
+                                               (mkTyConApp rep_tc (mkTyVarTys tvs'))
+                    parent   = FamInstTyCon axiom fam_tc pats'
+                    rep_tc   = buildAlgTyCon rep_tc_name tvs' cType stupid_theta tc_rhs 
                                              Recursive 
                                              False      -- No promotable to the kind level
                                              h98_syntax parent
@@ -723,6 +712,7 @@ tcDataFamInstDecl mb_clsinfo fam_tc
                  -- further instance might not introduce a new recursive
                  -- dependency.  (2) They are always valid loop breakers as
                  -- they involve a coercion.
+              ; fam_inst <- newFamInst (DataFamilyInst rep_tc) False axiom
               ; return (rep_tc, fam_inst) }
 
          -- Remember to check validity; no recursion to worry about here
index 2da7023..ef3af4f 100644 (file)
@@ -77,6 +77,7 @@ import Outputable
 import DataCon
 import Type
 import Class
+import CoAxiom  ( CoAxBranch(..) )
 import TcType   ( orphNamesOfDFunHead )
 import Inst     ( tcGetInstEnvs )
 import Data.List ( sortBy )
@@ -748,7 +749,8 @@ checkBootTyCon tc1 tc2
            eqListBy eqATDef def_ats1 def_ats2
 
        -- Ignore the location of the defaults
-       eqATDef (ATD tvs1 ty_pats1 ty1 _loc1) (ATD tvs2 ty_pats2 ty2 _loc2)
+       eqATDef (CoAxBranch { cab_tvs = tvs1, cab_lhs =  ty_pats1, cab_rhs = ty1 })
+               (CoAxBranch { cab_tvs = tvs2, cab_lhs =  ty_pats2, cab_rhs = ty2 })
          | Just env <- eqTyVarBndrs emptyRnEnv2 tvs1 tvs2
          = eqListBy (eqTypeX env) ty_pats1 ty_pats2 &&
            eqTypeX env ty1 ty2
index 24ca540..16a2373 100644 (file)
@@ -46,6 +46,7 @@ import FamInst
 import Type
 import Kind
 import Class
+import CoAxiom( CoAxBranch(..) )
 import TyCon
 import DataCon
 import Id
@@ -788,19 +789,16 @@ tcClassATs class_name parent ats at_defs
 -------------------------
 tcDefaultAssocDecl :: TyCon                -- ^ Family TyCon
                    -> LTyFamInstDecl Name  -- ^ RHS
-                   -> TcM [ATDefault]      -- ^ Type checked RHS and free TyVars
+                   -> TcM [CoAxBranch]     -- ^ Type checked RHS and free TyVars
 tcDefaultAssocDecl fam_tc (L loc decl)
   = setSrcSpan loc $
     tcAddTyFamInstCtxt decl $
     do { traceTc "tcDefaultAssocDecl" (ppr decl)
-       ; quads <- tcSynFamInstDecl fam_tc decl
-       ; return $ map (uncurry4 ATD) quads }
--- We check for well-formedness and validity later, in checkValidClass
-    where uncurry4 :: (a -> b -> c -> d -> e) -> (a, b, c, d) -> e
-          uncurry4 f (a, b, c, d) = f a b c d
+       ; tcSynFamInstDecl fam_tc decl }
+    -- We check for well-formedness and validity later, in checkValidClass
 
 -------------------------
-tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM [([TyVar], [Type], Type, SrcSpan)]
+tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM [CoAxBranch]
 -- Placed here because type family instances appear as 
 -- default decls in class declarations 
 tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqns = eqns })
@@ -823,7 +821,7 @@ tcSynFamInstNames (L _ first) names
       = setSrcSpan loc $
         failWithTc (msg_fun name)
 
-tcTyFamInstEqn :: TyCon -> LTyFamInstEqn Name -> TcM ([TyVar], [Type], Type, SrcSpan)
+tcTyFamInstEqn :: TyCon -> LTyFamInstEqn Name -> TcM CoAxBranch
 tcTyFamInstEqn fam_tc 
     (L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
   = setSrcSpan loc $
@@ -832,7 +830,7 @@ tcTyFamInstEqn fam_tc
     do { rhs_ty <- tcCheckLHsType hs_ty res_kind
        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
        ; traceTc "tcSynFamInstEqn" (ppr fam_tc <+> (ppr tvs' $$ ppr pats' $$ ppr rhs_ty))
-       ; return (tvs', pats', rhs_ty, loc) }
+       ; return (mkCoAxBranch tvs' pats' rhs_ty loc) }
 
 kcDataDefn :: HsDataDefn Name -> TcKind -> TcM ()
 -- Used for 'data instance' only
@@ -1505,7 +1503,8 @@ checkValidClass cls
                -- type variable.  What a mess!
 
     check_at_defs (fam_tc, defs)
-      = do { mapM_ (\(ATD tvs pats rhs _loc) -> checkValidTyFamInst fam_tc tvs pats rhs) defs
+      = do { mapM_ (\(CoAxBranch { cab_tvs = tvs, cab_lhs = pats, cab_rhs = rhs })
+                    -> checkValidTyFamInst fam_tc tvs pats rhs) defs
            ; tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $ 
              mapM_ (check_loc_at_def fam_tc) defs }
 
@@ -1520,7 +1519,7 @@ checkValidClass cls
     --  the (C Int Bool)  header
     -- This is not to do with soundness; it's just checking that the
     -- type instance arg is the sam
-    check_loc_at_def fam_tc (ATD _tvs pats _rhs loc)
+    check_loc_at_def fam_tc (CoAxBranch { cab_lhs = pats, cab_loc = loc })
       -- Set the location for each of the default declarations
       = setSrcSpan loc $ zipWithM_ check_arg (tyConTyVars fam_tc) pats
 
index 6ceb779..312ce84 100644 (file)
@@ -16,7 +16,7 @@ The @Class@ datatype
 module Class (
        Class,
         ClassOpItem, DefMeth (..),
-        ClassATItem, ATDefault (..),
+        ClassATItem,
        defMethSpecOfDefMeth,
 
        FunDep, pprFundeps, pprFunDep,
@@ -31,15 +31,14 @@ module Class (
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TyCon    ( TyCon, tyConName, tyConUnique )
-import {-# SOURCE #-} TypeRep  ( Type, PredType )
-
+import {-# SOURCE #-} TypeRep  ( PredType )
+import CoAxiom
 import Var
 import Name
 import BasicTypes
 import Unique
 import Util
 import Outputable
-import SrcLoc
 import FastString
 
 import Data.Typeable (Typeable)
@@ -97,21 +96,10 @@ data DefMeth = NoDefMeth            -- No default method
              deriving Eq
 
 type ClassATItem = (TyCon,           -- See Note [Associated type tyvar names]
-                    [ATDefault])     -- Default associated types from these templates 
+                    [CoAxBranch])    -- Default associated types from these templates 
   -- We can have more than one default per type; see
   -- Note [Associated type defaults] in TcTyClsDecls
 
--- Each associated type default template is a quad of:
-data ATDefault = ATD { -- TyVars of the RHS and family arguments 
-                       -- (including, but perhaps more than, the class TVs)
-                       atDefaultTys     :: [TyVar],
-                       -- The instantiated family arguments
-                       atDefaultPats    :: [Type],
-                       -- The RHS of the synonym
-                       atDefaultRhs     :: Type,
-                       -- The source location of the synonym
-                       atDefaultSrcSpan :: SrcSpan }
-
 -- | Convert a `DefMethSpec` to a `DefMeth`, which discards the name field in
 --   the `DefMeth` constructor of the `DefMeth`.
 defMethSpecOfDefMeth :: DefMeth -> DefMethSpec
index 04e63ef..bf432ca 100644 (file)
@@ -16,7 +16,7 @@ module CoAxiom (
        brListLength, brListNth, brListMap, brListFoldr,
        brListZipWith, brListIndices,
 
-       CoAxiom(..), CoAxBranch(..), mkCoAxBranch,
+       CoAxiom(..), CoAxBranch(..), 
 
        toBranchedAxiom, toUnbranchedAxiom,
        coAxiomName, coAxiomArity, coAxiomBranches,
@@ -219,7 +219,8 @@ data CoAxBranch
   = CoAxBranch
     { cab_loc      :: SrcSpan      -- Location of the defining equation
                                    -- See Note [CoAxiom locations]
-    , cab_tvs      :: [TyVar]      -- Bound type variables
+    , cab_tvs      :: [TyVar]      -- Bound type variables; not necessarily fresh
+                                   -- See Note [CoAxBranch type variables]
     , cab_lhs      :: [Type]       -- Type patterns to match against
     , cab_rhs      :: Type         -- Right-hand side of the equality
     }
@@ -275,12 +276,30 @@ coAxBranchSpan = cab_loc
 isImplicitCoAxiom :: CoAxiom br -> Bool
 isImplicitCoAxiom = co_ax_implicit
 
--- The tyvars must be *fresh*. This CoAxBranch will be put into a
--- FamInst. See Note [Template tyvars are fresh] in InstEnv
-mkCoAxBranch :: SrcSpan -> [TyVar] -> [Type] -> Type -> CoAxBranch
-mkCoAxBranch = CoAxBranch
 \end{code}
 
+Note [CoAxBranch type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In the case of a CoAxBranch of an associated type-family instance, 
+we use the *same* type variables (where possible) as the
+enclosing class or instance.  Consider
+   class C a b where
+     type F x b 
+     type F [y] b = ...     -- Second param must be b
+
+   instance C Int [z] where
+     type F Int [z] = ...   -- Second param must be [z]
+
+In the CoAxBranch in the instance decl (F Int [z]) we use the
+same 'z', so that it's easy to check that that type is the same
+as that in the instance header.  
+
+Similarly in the CoAxBranch for the default decl for F in the
+class decl, we use the same 'b' to make the same check easy.
+
+So, unlike FamInsts, there is no expectation that the cab_tvs
+are fresh wrt each other, or any other CoAxBranch.
+
 Note [CoAxiom locations]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 The source location of a CoAxiom is stored in two places in the
index abaf7dd..4672026 100644 (file)
@@ -593,7 +593,6 @@ mkAxInstLHS ax index tys
   , (tys1, tys2) <- splitAtList tvs tys
   = ASSERT( tvs `equalLength` tys1 ) 
     mkTyConApp (coAxiomTyCon ax) (substTysWith tvs tys1 lhs ++ tys2)
-  where
 
 mkAxInstRHS ax index tys
   | CoAxBranch { cab_tvs = tvs, cab_rhs = rhs } <- coAxiomNthBranch ax index
index 617cfa0..f4f06ec 100644 (file)
@@ -8,6 +8,8 @@ FamInstEnv: Type checked family instance declarations
 module FamInstEnv (
         Branched, Unbranched,
 
+        pprCoAxBranch, pprCoAxBranchHdr, 
+
         FamInst(..), FamFlavor(..), FamInstBranch(..), 
 
         famInstAxiom, famInstBranchRoughMatch,
@@ -17,9 +19,7 @@ module FamInstEnv (
         famInstTyCon, famInstRepTyCon_maybe, dataFamInstRepTyCon, 
         pprFamInst, pprFamInsts, 
         pprFamFlavor, 
-        pprCoAxBranch, pprCoAxBranchHdr, 
-        mkSynFamInst, mkSingleSynFamInst,
-        mkDataFamInst, mkImportedFamInst, 
+        mkImportedFamInst, 
 
         FamInstEnv, FamInstEnvs,
         emptyFamInstEnvs, emptyFamInstEnv, famInstEnvElts, familyInstances,
@@ -58,7 +58,7 @@ import SrcLoc
 
 %************************************************************************
 %*                                                                      *
-\subsection{Type checked family instance heads}
+           Type checked family instance heads
 %*                                                                      *
 %************************************************************************
 
@@ -130,8 +130,8 @@ data FamInst br -- See Note [FamInsts and CoAxioms], Note [Branched axioms] in C
 
 data FamInstBranch
   = FamInstBranch
-    { fib_tvs    :: [TyVar]      -- bound type variables
-                                 -- like ClsInsts, these variables are always
+    { fib_tvs    :: [TyVar]      -- Bound type variables
+                                 -- Like ClsInsts, these variables are always
                                  -- fresh. See Note [Template tyvars are fresh]
                                  -- in InstEnv
     , fib_lhs    :: [Type]       -- type patterns
@@ -264,100 +264,6 @@ pprCoAxBranchHdr ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_name = name }) index
 
 pprFamInsts :: [FamInst br] -> SDoc
 pprFamInsts finsts = vcat (map pprFamInst finsts)
-
-mk_fam_inst_branch :: CoAxBranch -> FamInstBranch
-mk_fam_inst_branch (CoAxBranch { cab_tvs = tvs
-                               , cab_lhs = lhs
-                               , cab_rhs = rhs })
-  = FamInstBranch { fib_tvs   = tvs
-                  , fib_lhs   = lhs
-                  , fib_rhs   = rhs
-                  , fib_tcs   = roughMatchTcs lhs }
-
--- | Create a coercion identifying a @type@ family instance.
--- It has the form @Co tvs :: F ts ~ R@, where @Co@ is
--- the coercion constructor built here, @F@ the family tycon and @R@ the
--- right-hand side of the type family instance.
-mkSynFamInst :: Name            -- ^ Unique name for the coercion tycon
-             -> TyCon           -- ^ Family tycon (@F@)
-             -> Bool            -- ^ Was this declared as a branched group?
-             -> [CoAxBranch]    -- ^ the branches of the CoAxiom
-             -> FamInst Branched
-mkSynFamInst name fam_tc group branches
-  = ASSERT( length branches >= 1 )
-    FamInst { fi_fam      = tyConName fam_tc
-            , fi_flavor   = SynFamilyInst
-            , fi_branches = toBranchList (map mk_fam_inst_branch branches)
-            , fi_group    = group
-            , fi_axiom    = axiom }
-  where
-    axiom = CoAxiom { co_ax_unique   = nameUnique name
-                    , co_ax_name     = name
-                    , co_ax_tc       = fam_tc
-                    , co_ax_implicit = False
-                    , co_ax_branches = toBranchList branches }
-
-
--- | Create a coercion identifying a @type@ family instance, but with only
--- one equation (branch).
-mkSingleSynFamInst :: Name        -- ^ Unique name for the coercion tycon
-                   -> [TyVar]     -- ^ *Fresh* tyvars of the coercion (@tvs@)
-                   -> TyCon       -- ^ Family tycon (@F@)
-                   -> [Type]      -- ^ Type instance (@ts@)
-                   -> Type        -- ^ right-hand side
-                   -> FamInst Unbranched
--- See note [Branched axioms] in CoAxiom.lhs
-mkSingleSynFamInst name tvs fam_tc inst_tys rep_ty
-  = FamInst { fi_fam      = tyConName fam_tc
-            , fi_flavor   = SynFamilyInst
-            , fi_branches = FirstBranch branch
-            , fi_group    = False
-            , fi_axiom    = axiom }
-  where
-    -- See note [FamInst Locations]
-    branch = mk_fam_inst_branch axBranch
-    axiom = CoAxiom { co_ax_unique   = nameUnique name
-                    , co_ax_name     = name
-                    , co_ax_tc       = fam_tc
-                    , co_ax_implicit = False
-                    , co_ax_branches = FirstBranch axBranch }
-    axBranch = CoAxBranch { cab_loc = getSrcSpan name
-                          , cab_tvs = tvs
-                          , cab_lhs = inst_tys
-                          , cab_rhs = rep_ty }
-    
--- | Create a coercion identifying a @data@ or @newtype@ representation type
--- and its family instance.  It has the form @Co tvs :: F ts ~ R tvs@,
--- where @Co@ is the coercion constructor built here, @F@ the family tycon
--- and @R@ the (derived) representation tycon.
-mkDataFamInst :: Name         -- ^ Unique name for the coercion tycon
-              -> [TyVar]      -- ^ *Fresh* parameters of the coercion (@tvs@)
-              -> TyCon        -- ^ Family tycon (@F@)
-              -> [Type]       -- ^ Type instance (@ts@)
-              -> TyCon        -- ^ Representation tycon (@R@)
-              -> FamInst Unbranched
-mkDataFamInst name tvs fam_tc inst_tys rep_tc
-  = FamInst { fi_fam      = tyConName fam_tc
-            , fi_flavor   = DataFamilyInst rep_tc
-            , fi_group    = False
-            , fi_branches = FirstBranch branch
-            , fi_axiom    = axiom }
-  where
-    rhs = mkTyConApp rep_tc (mkTyVarTys tvs)
-
-                               -- See Note [FamInst locations]
-    branch = mk_fam_inst_branch axBranch
-    axiom = CoAxiom { co_ax_unique   = nameUnique name
-                    , co_ax_name     = name
-                    , co_ax_tc       = fam_tc
-                    , co_ax_branches = FirstBranch axBranch
-                    , co_ax_implicit = False }
-
-    axBranch = CoAxBranch { cab_loc = getSrcSpan name
-                          , cab_tvs = tvs
-                          , cab_lhs = inst_tys
-                          , cab_rhs = rhs }
-
 \end{code}
 
 Note [Lazy axiom match]
index f5cbf93..af815c9 100644 (file)
@@ -23,7 +23,6 @@ import Type
 import OccName
 import Coercion
 import MkId
-import Name
 import FamInst
 
 import DynFlags
@@ -38,7 +37,8 @@ buildPReprTyCon orig_tc vect_tc repr
  = do name      <- mkLocalisedName mkPReprTyConOcc (tyConName orig_tc)
       rhs_ty    <- sumReprType repr
       prepr_tc  <- builtin preprTyCon
-      liftDs $ mkFreshenedSynInstLoc (getSrcSpan name) name tyvars prepr_tc instTys rhs_ty
+      let axiom = mkSingleCoAxiom name tyvars prepr_tc instTys rhs_ty
+      liftDs $ newFamInst SynFamilyInst False axiom
   where
     tyvars = tyConTyVars vect_tc
     instTys = [mkTyConApp vect_tc . mkTyVarTys $ tyConTyVars vect_tc]
index cbedf8d..f2b9f7a 100644 (file)
@@ -19,6 +19,7 @@ import BuildTyCl
 import DataCon
 import TyCon
 import Type
+import FamInst
 import FamInstEnv
 import TcMType
 import Name
@@ -45,9 +46,10 @@ buildDataFamInst name' fam_tc vect_tc rhs
  = do { axiom_name <- mkDerivedName mkInstTyCoOcc name'
 
       ; (_, tyvars') <- liftDs $ tcInstSkolTyVarsLoc (getSrcSpan name') tyvars
-      ; let fam_inst = mkDataFamInst axiom_name tyvars' fam_tc pat_tys rep_tc
-            ax       = famInstAxiom fam_inst
-            pat_tys  = [mkTyConApp vect_tc (mkTyVarTys tyvars')]
+      ; let ax       = mkSingleCoAxiom axiom_name tyvars' fam_tc pat_tys rep_ty
+            tys'     = mkTyVarTys tyvars'
+            rep_ty   = mkTyConApp rep_tc tys'
+            pat_tys  = [mkTyConApp vect_tc tys']
             rep_tc   = buildAlgTyCon name'
                            tyvars'
                            Nothing
@@ -57,7 +59,7 @@ buildDataFamInst name' fam_tc vect_tc rhs
                            False       -- Not promotable
                            False       -- not GADT syntax
                            (FamInstTyCon ax fam_tc pat_tys)
-      ; return fam_inst }
+      ; liftDs $ newFamInst (DataFamilyInst rep_tc) False ax }
  where
     tyvars    = tyConTyVars vect_tc
     rec_flag  = boolToRecFlag (isRecursiveTyCon vect_tc)