Revert "Checkpoint. Working in FamInst on newFamInst."

This reverts commit 9b8dc72.

compiler/rename/RnSource.lhs

@@ -562,7 +562,7 @@ rnTyFamInstDecl Nothing (TyFamInstBranched { tfid_eqns = eqns, tfid_space = mspa
   where rn_space Nothing = (Nothing, emptyFVs)
         rn_space (Just (TyFamInstSpace { tfis_tycon = tycon
                                        , tfis_pats  = pats }))
-          = do { (tycon', pats', fvs) <- rnFamInstLHS (TySynCtx tycon) Nothing tycon pats
+          = do { (tycon', pats', fvs) <- rnFamInstLHS ??? Nothing tycon pats
                ; return (TyFamInstSpace { tfis_tycon = tycon'
                                         , tfis_pats  = pats' }, fvs) }
 

compiler/typecheck/FamInst.lhs

@@ -53,19 +53,14 @@ import qualified Data.Map as Map
 -- 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                  -- is this a branched instance?
-           -> Maybe ([TyVar], Type) -- declared type space for branched instances
-           -> CoAxiom br
-           -> TcRnIf gbl lcl (FamInst br)
+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_branched mb_space 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_space    = space
                          , fi_branches = fam_branches
                          , fi_branched = is_branched
                          , fi_axiom    = axiom }) }
@@ -86,17 +81,6 @@ newFamInst flavor is_branched mb_space axiom@(CoAxiom { co_ax_tc       = fam_tc
                                     , fib_lhs   = substTys subst lhs
                                     , fib_rhs   = substTy  subst rhs
                                     , fib_tcs   = roughMatchTcs lhs }) }
-
-    space
-      | False <- is_branched
-      , FirstBranch (FamInstBranch { fib_tvs = tvs, fib_lhs = lhs, fib_tcs = tcs })
-          <- fam_branches
-      = Just (FamInstSpace { fis_tvs = tvs, fis_tys = lhs, fis_tcs = tcs })
-
-      | Nothing <- mb_space
-      = Nothing
-
-      | Just (tvs, 
 \end{code}
 
 

compiler/typecheck/TcDeriv.lhs

@@ -552,7 +552,7 @@ deriveFamInst decl@(DataFamInstDecl { dfid_tycon = L _ tc_name, dfid_pats = pats
                                     , dfid_defn = HsDataDefn { dd_derivs = Just preds } })
   = tcAddDataFamInstCtxt decl $
     do { fam_tc <- tcLookupTyCon tc_name
-       ; tcFamTyPats fam_tc pats Nothing $ \ tvs' pats' _ ->
+       ; tcFamTyPats fam_tc pats (\_ -> return ()) $ \ tvs' pats' _ ->
          mapM (deriveTyData tvs' fam_tc pats') preds }
         -- Tiresomely we must figure out the "lhs", which is awkward for type families
         -- E.g.   data T a b = .. deriving( Eq )

compiler/typecheck/TcInstDcls.lhs

@@ -623,10 +623,13 @@ tcFamInstDeclCombined mb_clsinfo fam_tc_lname
 tcTyFamInstDecl :: Maybe (Class, VarEnv Type) -- the class & mini_env if applicable
                 -> LTyFamInstDecl Name -> TcM (FamInst Branched)
   -- "type instance"
-tcTyFamInstDecl mb_clsinfo (L loc decl)
+tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_group = group
+                                                      , tfid_eqns = eqns }))
   = setSrcSpan loc           $
     tcAddTyFamInstCtxt decl  $
-    do { fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname
+    do { let (eqn1:_) = eqns
+             fam_lname = tfie_tycon (unLoc eqn1)
+       ; fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname
 
          -- (0) Check it's an open type family
        ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
@@ -635,36 +638,25 @@ tcTyFamInstDecl mb_clsinfo (L loc decl)
                  (notOpenFamily fam_tc)
 
          -- (1) do the work of verifying the synonym group
-       ; (mb_space, co_ax_branches) <- tcSynFamInstDecl fam_tc decl
+       ; co_ax_branches <- tcSynFamInstDecl fam_tc decl
 
          -- (2) check for validity and inaccessibility
-       ; checkValidTypeSpace mb_space
-       ; foldlM_ (check_valid_branch fam_tc mb_space) [] co_ax_branches
+       ; foldlM_ (check_valid_branch fam_tc) [] co_ax_branches
 
          -- (3) construct coercion axiom
        ; rep_tc_name <- newFamInstAxiomName loc
                                             (tyFamInstDeclName decl)
                                             (map cab_lhs co_ax_branches)
        ; let axiom = mkBranchedCoAxiom rep_tc_name fam_tc co_ax_branches
-       ; newFamInst SynFamilyInst branched axiom }
-    where
-      eqn1
-        | TyFamInstSingle { tfid_eqn = eqn } <- decl        = eqn
-        | TyFamInstBranched { tfid_eqns = (eqn:_) } <- decl = eqn
-      fam_lname = tfie_tycon (unLoc eqn1)
-
-      branched
-        | TyFamInstSingle {} <- decl   = False
-        | TyFamInstBranched {} <- decl = True
-
+       ; newFamInst SynFamilyInst group axiom }
+    where 
       check_valid_branch :: TyCon
-                         -> Maybe ([TKVar], Type) -- type space
                          -> [CoAxBranch]     -- previous
                          -> CoAxBranch       -- current
                          -> TcM [CoAxBranch] -- current : previous
-      check_valid_branch fam_tc mb_space prev_branches cur_branch
+      check_valid_branch fam_tc prev_branches cur_branch
         = do { -- Check the well-formedness of the instance
-               checkValidTyFamInst mb_clsinfo mb_space branched fam_tc cur_branch
+               checkValidTyFamInst mb_clsinfo fam_tc cur_branch
 
                -- Check whether the branch is dominated by earlier
                -- ones and hence is inaccessible
@@ -692,13 +684,13 @@ tcDataFamInstDecl mb_clsinfo
        ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)
 
          -- Kind check type patterns
-       ; tcFamTyPats fam_tc pats (Just $ kcDataDefn defn) $ 
+       ; tcFamTyPats fam_tc pats (kcDataDefn defn) $ 
            \tvs' pats' res_kind -> do
 
        { -- Check that left-hand side contains no type family applications
          -- (vanilla synonyms are fine, though, and we checked for
          --  foralls earlier)
-         checkValidFamPats False fam_tc tvs' pats'
+         checkValidFamPats fam_tc tvs' pats'
          -- Check that type patterns match class instance head, if any
        ; checkConsistentFamInst mb_clsinfo fam_tc tvs' pats'
          

compiler/typecheck/TcTyClsDecls.lhs

@@ -785,37 +785,17 @@ tcDefaultAssocDecl fam_tc (L loc decl)
     -- We check for well-formedness and validity later, in checkValidClass
 
 -------------------------
--- returns an optional type space specifier along with the branches
-tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name
-                 -> TcM (Maybe ([TKVar], Type), [CoAxBranch])
+tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM [CoAxBranch]
 -- Placed here because type family instances appear as
 -- default decls in class declarations
-tcSynFamInstDecl fam_tc (TyFamInstSingle { tfid_eqn = eqn })
-  = do { checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
-       ; eqn' <- tcTyFamInstEqn fam_tc eqn
-       ; return (Nothing, [eqn']) }
-tcSynFamInstDecl fam_tc (TyFamInstBranched { tfid_eqns  = eqns
-                                           , tfid_space = mspace })
+tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqns = eqns })
   -- we know the first equation matches the fam_tc because of the lookup logic
   -- now, just check that all other names match the first
-  = do { tcSynFamInstNames first names
+  = do { let names = map (tfie_tycon . unLoc) eqns
+             first = head names
+       ; tcSynFamInstNames first names
        ; checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
-       ; mspace' <- check_space mspace
-       ; eqns' <- mapM (tcTyFamInstEqn fam_tc) eqns
-       ; return (mspace', eqns') }
-  where
-    names = map (tfie_tycon . unLoc) eqns
-    first = head names
-
-    check_space :: Maybe LTyFamInstSpace -> TcM (Maybe ([TKVar], Type))
-    check_space Nothing = return Nothing
-    check_space (Just (L loc (TyFamInstSpace { tfis_tycon = tycon
-                                             , tfis_pats  = pats })))
-      = setSrcSpan loc $
-        tcAddTyFamInstSpaceCtxt $
-        do { checkTc (tycon == first) (badTypeSpace tycon first)
-           ; tcFamTyPats fam_tc pats Nothing $
-               \tvs pats' _kind -> Just (tvs, mkTyConApp fam_tc pats) }
+       ; mapM (tcTyFamInstEqn fam_tc) eqns }
 
 -- Checks to make sure that all the names in an instance group are the same
 tcSynFamInstNames :: Located Name -> [Located Name] -> TcM ()
@@ -832,7 +812,7 @@ tcTyFamInstEqn :: TyCon -> LTyFamInstEqn Name -> TcM CoAxBranch
 tcTyFamInstEqn fam_tc
     (L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
   = setSrcSpan loc $
-    tcFamTyPats fam_tc pats (Just $ discardResult . (tcCheckLHsType hs_ty)) $
+    tcFamTyPats fam_tc pats (discardResult . (tcCheckLHsType hs_ty)) $
        \tvs' pats' res_kind ->
     do { rhs_ty <- tcCheckLHsType hs_ty res_kind
        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
@@ -868,8 +848,8 @@ kcResultKind (Just k) res_k
 -----------------
 tcFamTyPats :: TyCon
             -> HsWithBndrs [LHsType Name] -- Patterns
-            -> Maybe (TcKind -> TcM ())       -- Kind checker for RHS
-                                              -- result is ignored
+            -> (TcKind -> TcM ())       -- Kind checker for RHS
+                                        -- result is ignored
             -> ([TKVar] -> [TcType] -> Kind -> TcM a)
             -> TcM a
 -- Check the type patterns of a type or data family instance
@@ -884,7 +864,7 @@ tcFamTyPats :: TyCon
 -- (and, if C is poly-kinded, so will its kind parameter).
 
 tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
-            mb_kind_checker thing_inside
+            kind_checker thing_inside
   = do { -- A family instance must have exactly the same number of type
          -- parameters as the family declaration.  You can't write
          --     type family F a :: * -> *
@@ -907,7 +887,7 @@ tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tva
          -- Kind-check and quantify
          -- See Note [Quantifying over family patterns]
        ; typats <- tcHsTyVarBndrs hs_tvs $ \ _ ->
-                   do { maybe_do kind_checker res_kind
+                   do { kind_checker res_kind
                       ; tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds }
        ; let all_args = fam_arg_kinds ++ typats
 
@@ -925,9 +905,6 @@ tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tva
        ; traceTc "tcFamTyPats" (pprTvBndrs qtkvs' $$ ppr all_args' $$ ppr res_kind')
        ; tcExtendTyVarEnv qtkvs' $
          thing_inside qtkvs' all_args' res_kind' }
-  where maybe_do :: Monad m => Maybe (a -> m ()) -> a -> m ()
-        maybe_do Nothing  _ = return ()
-        maybe_do (Just f) a = f a
 \end{code}
 
 Note [Quantifying over family patterns]
@@ -1490,7 +1467,7 @@ checkValidClass cls
 
     check_at_defs (fam_tc, defs)
       = tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $
-        mapM_ (checkValidTyFamInst mb_clsinfo Nothing fam_tc) defs
+        mapM_ (checkValidTyFamInst mb_clsinfo fam_tc) defs
 
     mb_clsinfo = Just (cls, mkVarEnv [ (tv, mkTyVarTy tv) | tv <- tyvars ])
 

compiler/typecheck/TcValidity.lhs

@@ -1078,15 +1078,12 @@ wrongATArgErr ty instTy =
 -- unless -XUndecidableInstances is given).
 --
 checkValidTyFamInst :: Maybe ( Class, VarEnv Type )
-                    -> Maybe ([TKVar], Type)   -- type space for branched instances
-                    -> Bool          -- is this part of a branched instance?
                     -> TyCon -> CoAxBranch -> TcM ()
-checkValidTyFamInst mb_clsinfo mb_space branched fam_tc 
+checkValidTyFamInst mb_clsinfo fam_tc 
                     (CoAxBranch { cab_tvs = tvs, cab_lhs = typats
                                 , cab_rhs = rhs, cab_loc = loc })
-  = ASSERT( not (isJust mb_space && not branched) )
-    setSrcSpan loc $ 
-    do { checkValidFamPats branched fam_tc tvs typats
+  = setSrcSpan loc $ 
+    do { checkValidFamPats fam_tc tvs typats
 
          -- The right-hand side is a tau type
        ; checkValidMonoType rhs
@@ -1097,29 +1094,7 @@ checkValidTyFamInst mb_clsinfo mb_space branched fam_tc
            mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs))
 
          -- Check that type patterns match the class instance head
-       ; checkConsistentFamInst mb_clsinfo fam_tc tvs typats
-
-         -- Check that branch fits within type space
-       ; checkPatsWithinTypeSpace mb_space fam_tc typats }
-
--- checks to make sure that a declared type space has *linear* patterns
-checkValidTypeSpace :: Maybe ([TyVar], Type) -> TcM ()
-checkValidTypeSpace Nothing = return ()
-checkValidTypeSpace (Just (_, ty))
-  = checkTc (hasNoDups $ fvType ty) $
-      nonLinearTypeSpace ty
-
--- checks to make sure that patterns in a branched type family instance
--- fit within the declared type space.
--- i.e. type instance Foo [x] where { Foo Int = Bool } should fail
-checkPatsWithinTypeSpace :: Maybe ([TyVar], Type)
-                         -> TyCon -> [Type]
-                         -> TcM ()
-checkPatsWithinTypeSpace Nothing _ _ = return ()
-checkPatsWithinTypeSpace (Just (tvs, space)) fam_tc pats
-  = checkTc (isJust $ tcMatchTy tvs space lhs) $
-      branchOutOfTypeSpace space lhs
-  where lhs = mkTyConApp fam_tc pats
+       ; checkConsistentFamInst mb_clsinfo fam_tc tvs typats }
 
 -- Make sure that each type family application is 
 --   (1) strictly smaller than the lhs,
@@ -1150,22 +1125,18 @@ checkFamInstRhs lhsTys famInsts
              -- excessive occurrences of *type* variables.
              -- e.g. type instance Demote {T k} a = T (Demote {k} (Any {k}))
 
-checkValidFamPats :: Bool -- allow non-linear patterns?
-                  -> TyCon -> [TyVar] -> [Type] -> TcM ()
+checkValidFamPats :: TyCon -> [TyVar] -> [Type] -> TcM ()
 -- Patterns in a 'type instance' or 'data instance' decl should
 -- a) contain no type family applications
 --    (vanilla synonyms are fine, though)
 -- b) properly bind all their free type variables
 --    e.g. we disallow (Trac #7536)
 --         type T a = Int
 --         type instance F (T a) = a
-checkValidFamPats allow_nonlinear fam_tc tvs ty_pats
+checkValidFamPats fam_tc tvs ty_pats
   = do { mapM_ checkTyFamFreeness ty_pats
        ; let unbound_tvs = filterOut (`elemVarSet` exactTyVarsOfTypes ty_pats) tvs
-       ; checkTc (null unbound_tvs) (famPatErr fam_tc unbound_tvs ty_pats)
-       ; unless allow_nonlinear $
-           checkTc (hasNoDups $ fvTypes ty_pats) (nonLinearPattern fam_tc ty_pats)
- }
+       ; checkTc (null unbound_tvs) (famPatErr fam_tc unbound_tvs ty_pats) }
 
 -- Ensure that no type family instances occur in a type.
 --
@@ -1200,21 +1171,6 @@ famPatErr fam_tc tvs pats
        2 (hang (ptext (sLit "but the real LHS (expanding synonyms) is:"))
              2 (pprTypeApp fam_tc (map expandTypeSynonyms pats) <+> ptext (sLit "= ...")))
 
-nonLinearPattern :: TyCon -> [Type] -> SDoc
-nonLinearPattern fam_tc ty_pats
-  = hang (ptext (sLit "Repeated variable in standalone instance not allowed:"))
-         2 (pprTypeApp fam_tc ty_pats)
-
-nonLinearTypeSpace :: Type -> SDoc
-nonLinearTypeSpace ty
-  = hang (ptext (sLit "Repeated variable in branched instance type region not allowed:"))
-       2 (ppr ty)
-
-branchOutOfTypeSpace :: Type -> Type -> SDoc
-branchOutOfTypeSpace space lhs
-  = ptext (sLit "The declared type space") <+> quotes (ppr space) <+>
-    ptext (sLit "does not include the type") <+> quotes (ppr lhs)
-
 nestedMsg, smallerAppMsg :: SDoc
 nestedMsg     = ptext (sLit "Nested type family application")
 smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
@@ -1235,7 +1191,7 @@ fvType (TyConApp _ tys)    = fvTypes tys
 fvType (LitTy {})          = []
 fvType (FunTy arg res)     = fvType arg ++ fvType res
 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
-fvType (ForAllTy tyvar ty) = fvType (tyVarKind tyvar) ++ filter (/= tyvar) (fvType ty)
+fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
 
 fvTypes :: [Type] -> [TyVar]
 fvTypes tys                = concat (map fvType tys)