diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-11-23 17:33:19 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-11-26 09:59:15 +0000 |
commit | 7f9e4281c86f2e69d0f85c67e4b268bc4851f3a9 (patch) | |
tree | 98f74570bc69693098cdf38313fb8819c4c2ddf6 | |
parent | 1c686e6ca79b9ac2f1ba19d1abc215937fb562fc (diff) | |
download | haskell-7f9e4281c86f2e69d0f85c67e4b268bc4851f3a9.tar.gz |
More wibbles
Plus rebased onto master
-rw-r--r-- | compiler/hsSyn/HsTypes.hs | 1 | ||||
-rw-r--r-- | compiler/typecheck/TcDeriv.hs | 23 | ||||
-rw-r--r-- | compiler/typecheck/TcHsType.hs | 6 | ||||
-rw-r--r-- | compiler/typecheck/TcInstDcls.hs | 40 | ||||
-rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 55 | ||||
-rw-r--r-- | compiler/types/TyCoRep.hs | 6 | ||||
-rw-r--r-- | compiler/types/Type.hs | 3 |
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 |