More wibbles

Plus rebased onto master

7 files changed, 90 insertions, 44 deletions

diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index 6094fe13c0..993b0202d8 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -90,7 +90,6 @@ import FastString
 import Maybes( isJust )
 
 import Data.Data hiding ( Fixity, Prefix, Infix )
-import Data.List ( foldl' )
 
 {-
 ************************************************************************
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index f8cc7adb7c..e2a314c6a2 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -746,7 +746,8 @@ warnUselessTypeable
 
 ------------------------------------------------------------------
 deriveTyData :: [TyVar] -> TyCon -> [Type]   -- LHS of data or data instance
-                                             --   Can be a data instance, hence [Type] args
+                    -- Can be a data instance, hence [Type] args
+                    -- and in that case the TyCon is the /family/ tycon
              -> Maybe (DerivStrategy GhcRn)  -- The optional deriving strategy
              -> LHsSigType GhcRn             -- The deriving predicate
              -> TcM (Maybe EarlyDerivSpec)
@@ -784,6 +785,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
           let (arg_kinds, _)  = splitFunTys cls_arg_kind
               n_args_to_drop  = length arg_kinds
               n_args_to_keep  = length tc_args - n_args_to_drop
+                                -- See Note [tc_args and tycon arity]
               (tc_args_to_keep, args_to_drop)
                               = splitAt n_args_to_keep tc_args
               inst_ty_kind    = typeKind (mkTyConApp tc tc_args_to_keep)
@@ -888,7 +890,24 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
         ; return $ Just spec } }
 
 
-{-
+{- Note [tc_args and tycon arity]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+You might wonder if we could use (tyConArity tc) at this point, rather
+than (length tc_args).  But for data families the two can differ!  The
+tc and tc_args passed into 'deriveTyData' come from 'deriveClause' which
+in turn gets them from 'tyConFamInstSig_maybe' which in turn gets them
+from DataFamInstTyCon:
+
+| DataFamInstTyCon          -- See Note [Data type families]
+      (CoAxiom Unbranched)
+      TyCon   -- The family TyCon
+      [Type]  -- Argument types (mentions the tyConTyVars of this TyCon)
+              -- No shorter in length than the tyConTyVars of the family TyCon
+              -- How could it be longer? See [Arity of data families] in FamInstEnv
+
+Notice that the arg tys might not be the same as the family tycon arity
+(= length tyConTyVars).
+
 Note [Unify kinds in deriving]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider (Trac #8534)
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 2a4f6dc4da..5e821883ad 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -232,9 +232,9 @@ tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
 tc_hs_sig_type skol_info hs_sig_type ctxt_kind
   | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
   = do { (tc_lvl, (wanted, (spec_tkvs, ty)))
-              <- pushTcLevelM                                   $
-                 solveLocalEqualitiesX "tc_hs_sig_type_and_gen" $
-                 bindImplicitTKBndrs_Skol sig_vars              $
+              <- pushTcLevelM                           $
+                 solveLocalEqualitiesX "tc_hs_sig_type" $
+                 bindImplicitTKBndrs_Skol sig_vars      $
                  do { kind <- newExpectedKind ctxt_kind
 
                     ; tc_lhs_type typeLevelMode hs_ty kind }
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 9a481400a4..fc2ea052e4 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -68,6 +68,7 @@ import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
 import Maybes
+import Data.List( mapAccumL )
 
 
 {-
@@ -612,7 +613,7 @@ tcDataFamInstDecl mb_clsinfo
        ; rep_tc_name <- newFamInstTyConName lfam_name pats
        ; axiom_name  <- newFamInstAxiomName lfam_name [pats]
 
-       ; let (eta_pats, etad_tvs) = eta_reduce pats
+       ; let (eta_pats, etad_tvs) = eta_reduce fam_tc pats
              eta_tvs              = filterOut (`elem` etad_tvs) qtvs
                  -- NB: the "extra" tvs from tcDataKindSig would always be eta-reduced
 
@@ -632,8 +633,16 @@ tcDataFamInstDecl mb_clsinfo
              orig_res_ty = mkTyConApp fam_tc all_pats
              ty_binders  = full_tcbs `chkAppend` extra_tcbs
 
-       ; traceTc "tcDataFamInstDecl" (ppr fam_tc $$ ppr pats $$ ppr imp_vars $$ ppr mb_bndrs
-                                      $$ ppr hs_cons)
+       ; traceTc "tcDataFamInstDecl" $
+         vcat [ text "Fam tycon:" <+> ppr fam_tc
+              , text "Pats:" <+> ppr pats
+              , text "all_pats:" <+> ppr all_pats
+              , text "ty_binders" <+> ppr ty_binders
+              , text "fam_tc_binders:" <+> ppr (tyConBinders fam_tc)
+              , text "deps:" <+> ppr (map isNamedTyConBinder (tyConBinders fam_tc))
+              , text "eta_pats" <+> ppr eta_pats
+              , text "eta_tvs" <+> ppr eta_tvs ]
+
        ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
            do { data_cons <- tcExtendTyVarEnv qtvs $
                              -- For H98 decls, the tyvars scope
@@ -682,20 +691,31 @@ tcDataFamInstDecl mb_clsinfo
        ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
        ; return (fam_inst, m_deriv_info) }
   where
-    eta_reduce :: [Type] -> ([Type], [TyVar])
+    eta_reduce :: TyCon -> [Type] -> ([Type], [TyVar])
     -- See Note [Eta reduction for data families] in FamInstEnv
     -- Splits the incoming patterns into two: the [TyVar]
     -- are the patterns that can be eta-reduced away.
     -- e.g.     T [a] Int a d c   ==>  (T [a] Int a, [d,c])
     --
     -- NB: quadratic algorithm, but types are small here
-    eta_reduce pats
-      = go (reverse pats) []
-    go (pat:pats) etad_tvs
-      | Just tv <- getTyVar_maybe pat
-      , not (tv `elemVarSet` tyCoVarsOfTypes pats)
+    eta_reduce fam_tc pats
+        = go (reverse (zip3 pats fvs_s deps)) []
+        where
+          fvs_s :: [TyCoVarSet]  -- 1-1 correspondence with pats
+                                 -- Each elt is the free vars of all /earlier/ pats
+          (_, fvs_s) = mapAccumL add_fvs emptyVarSet pats
+          add_fvs fvs pat = (fvs `unionVarSet` tyCoVarsOfType pat, fvs)
+
+          deps :: [Bool]
+          deps = map isNamedBinder tc_bndrs ++ repeat False
+          (tc_bndrs, _) = splitPiTys (tyConKind fam_tc)
+
+    go ((pat, fvs_to_the_left, is_dep):pats) etad_tvs
+      | not is_dep
+      , Just tv <- getTyVar_maybe pat
+      , not (tv `elemVarSet` fvs_to_the_left)
       = go pats (tv : etad_tvs)
-    go pats etad_tvs = (reverse pats, etad_tvs)
+    go pats etad_tvs = (reverse (map fstOf3 pats), etad_tvs)
 
 tcDataFamInstDecl _ _ = panic "tcDataFamInstDecl"
 
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 45da98a6c0..41504d6840 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1440,9 +1440,9 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
           -- at an associated type. But this would be wrong, because an associated
           -- type default LHS can mention *different* type variables than the
           -- enclosing class. So it's treated more as a freestanding beast.
-       ; (qtvs, pats, rhs_ty) <- tcFamTyPatsAndGen fam_tc NotAssociated
-                                                   imp_vars exp_vars
-                                                   hs_pats hs_rhs_ty
+       ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc NotAssociated
+                                                    imp_vars exp_vars
+                                                    hs_pats hs_rhs_ty
 
          -- See Note [Type-checking default assoc decls]
        ; traceTc "tcDefault" (vcat [ppr (tyConTyVars fam_tc), ppr qtvs, ppr pats])
@@ -1781,7 +1781,7 @@ tcTyFamInstEqn fam_tc mb_clsinfo
        ; checkTc (hs_pats `lengthIs` vis_arity) $
          wrongNumberOfParmsErr vis_arity
 
-       ; (qtvs, pats, rhs_ty) <- tcFamTyPatsAndGen fam_tc mb_clsinfo
+       ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc mb_clsinfo
                                       imp_vars (mb_expl_bndrs `orElse` [])
                                       hs_pats hs_rhs_ty
 
@@ -1854,14 +1854,14 @@ Simple, neat, but a little non-obvious!
 -}
 
 --------------------------
-tcFamTyPatsAndGen :: TyCon -> AssocInstInfo
-                  -> [Name] -> [LHsTyVarBndr GhcRn]  -- Implicit and explicicit binder
-                  -> HsTyPats GhcRn                  -- Patterns
-                  -> LHsType GhcRn                   -- RHS
-                  -> TcM ([TyVar], [TcType], TcType)      -- (tyvars, pats, rhs)
+tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo
+                   -> [Name] -> [LHsTyVarBndr GhcRn]  -- Implicit and explicicit binder
+                   -> HsTyPats GhcRn                  -- Patterns
+                   -> LHsType GhcRn                   -- RHS
+                   -> TcM ([TyVar], [TcType], TcType)      -- (tyvars, pats, rhs)
 -- Used only for type families, not data families
-tcFamTyPatsAndGen fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
-  = do { traceTc "tcFamTyPatsAndGen {" (vcat [ ppr fam_tc <+> ppr hs_pats ])
+tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
+  = do { traceTc "tcTyFamInstEqnGuts {" (vcat [ ppr fam_tc <+> ppr hs_pats ])
 
        -- By now, for type families (but not data families) we should
        -- have checked that the number of patterns matches tyConArity
@@ -1887,7 +1887,7 @@ tcFamTyPatsAndGen fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
        ; rhs_ty     <- zonkTcTypeToTypeX ze rhs_ty
 
        ; let pats = unravelFamInstPats lhs_ty
-       ; traceTc "tcFamTyPatsAndGen }" (ppr fam_tc <+> pprTyVars qtvs)
+       ; traceTc "tcTyFamInstEqnGuts }" (ppr fam_tc <+> pprTyVars qtvs)
        ; return (qtvs, pats, rhs_ty) }
   where
     tc_lhs | null hs_pats
@@ -3260,14 +3260,15 @@ checkFamFlag tc_name
 
 -- | Extra information about the parent instance declaration, needed
 -- when type-checking associated types. The 'Class' is the enclosing
--- class, the [TyVar] are the type variable of the instance decl,
--- and and the @VarEnv Type@ maps class variables to their instance
--- types.
+-- class, the [TyVar] are the /scoped/ type variable of the instance decl.
+-- The @VarEnv Type@ maps class variables to their instance types.
 data AssocInstInfo
   = NotAssociated
   | InClsInst { ai_class    :: Class
-              , ai_tyvars   :: [TyVar]
-              , ai_inst_env :: VarEnv Type }
+              , ai_tyvars   :: [TyVar]      -- ^ The /scoped/ tyvars of the instance
+              , ai_inst_env :: VarEnv Type  -- ^ Maps /class/ tyvars to their instance types
+                -- See Note [Matching in the consistent-instantation check]
+    }
 
 isNotAssociated :: AssocInstInfo -> Bool
 isNotAssociated NotAssociated  = True
@@ -3307,9 +3308,11 @@ checkConsistentFamInst (InClsInst { ai_class = clas
                                at_arg_tys
                   , Just cls_arg_ty <- [lookupVarEnv mini_env fam_tc_tv] ]
 
-    pp_wrong_at_arg = vcat [ text "Type indexes must match class instance head"
-                           , text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
-                           , text "  Actual:" <+> ppr (mkTyConApp fam_tc at_arg_tys) ]
+    pp_wrong_at_arg vis
+      = pprWithExplicitKindsWhen (isInvisibleArgFlag vis) $
+        vcat [ text "Type indexes must match class instance head"
+             , text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
+             , text "  Actual:" <+> ppr (mkTyConApp fam_tc at_arg_tys) ]
 
     expected_args = [ lookupVarEnv mini_env at_tv `orElse` underscore at_tv
                     | at_tv <- tyConTyVars fam_tc ]
@@ -3327,13 +3330,10 @@ checkConsistentFamInst (InClsInst { ai_class = clas
       , Just rl_subst1 <- tcMatchTyX_BM bind_me rl_subst ty2 ty1
       = go lr_subst1 rl_subst1 triples
       | otherwise
-      = addErrTc (pp_wrong_at_arg $$
-                  ppWhen (isInvisibleArgFlag vis) ppSuggestExplicitKinds)
+      = addErrTc (pp_wrong_at_arg vis)
 
-    -- A variable that is /both/ in the class-instance header,
-    -- /and/ in family instance must be one of the scoped variables
-    -- shared between the two.  Don't let these alpha-raneme to
-    -- anything else.
+    -- The scoped type variables from the class-isntance header
+    -- should not be alpha-raenamed.
     no_bind_set = mkVarSet inst_tvs
     bind_me tv | tv `elemVarSet` no_bind_set = Skolem
                | otherwise                   = BindMe
@@ -3360,6 +3360,9 @@ while the type-family instance is       T (a -> Either @a @b)
 So we allow alpha-renaming of variables that don't come
 from the class-instance header.
 
+We track the lexically-scoped type variables from the
+class-instance header in ai_tyvars.
+
 Here's another example (Trac #14045a)
     class C (a :: k) where
       data S (a :: k)
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 8138214eee..09f459c452 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -55,7 +55,7 @@ module TyCoRep (
         delBinderVar,
         isInvisibleArgFlag, isVisibleArgFlag,
         isInvisibleBinder, isVisibleBinder,
-        isTyBinder,
+        isTyBinder, isNamedBinder,
 
         -- * Functions over coercions
         pickLR,
@@ -542,6 +542,10 @@ isInvisibleBinder (Anon ty)            = isPredTy ty
 isVisibleBinder :: TyCoBinder -> Bool
 isVisibleBinder = not . isInvisibleBinder
 
+isNamedBinder :: TyCoBinder -> Bool
+isNamedBinder (Named {}) = True
+isNamedBinder (Anon {})  = False
+
 -- | If its a named binder, is the binder a tyvar?
 -- Returns True for nondependent binder.
 isTyBinder :: TyCoBinder -> Bool
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 22caa1aec8..f20aaf7678 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -106,7 +106,8 @@ module Type (
         tyCoBinderType, tyCoBinderVar_maybe,
         tyBinderType,
         binderRelevantType_maybe, caseBinder,
-        isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
+        isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder,
+        isInvisibleBinder, isNamedBinder,
         tyConBindersTyCoBinders,
 
         -- ** Common type constructors