diff options
Diffstat (limited to 'compiler/GHC/Core')
| -rw-r--r-- | compiler/GHC/Core/Coercion/Axiom.hs | 9 | ||||
| -rw-r--r-- | compiler/GHC/Core/DataCon.hs | 3 | ||||
| -rw-r--r-- | compiler/GHC/Core/FamInstEnv.hs | 11 | ||||
| -rw-r--r-- | compiler/GHC/Core/Lint.hs | 224 | ||||
| -rw-r--r-- | compiler/GHC/Core/TyCon.hs | 30 | ||||
| -rw-r--r-- | compiler/GHC/Core/Type.hs | 15 |
6 files changed, 227 insertions, 65 deletions
diff --git a/compiler/GHC/Core/Coercion/Axiom.hs b/compiler/GHC/Core/Coercion/Axiom.hs index 4ecbb6cc3d..7046273ae5 100644 --- a/compiler/GHC/Core/Coercion/Axiom.hs +++ b/compiler/GHC/Core/Coercion/Axiom.hs @@ -184,9 +184,10 @@ Note [Storing compatibility] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ During axiom application, we need to be aware of which branches are compatible with which others. The full explanation is in Note [Compatibility] in -FamInstEnv. (The code is placed there to avoid a dependency from CoAxiom on -the unification algorithm.) Although we could theoretically compute -compatibility on the fly, this is silly, so we store it in a CoAxiom. +GHc.Core.FamInstEnv. (The code is placed there to avoid a dependency from +GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could +theoretically compute compatibility on the fly, this is silly, so we store it +in a CoAxiom. Specifically, each branch refers to all other branches with which it is incompatible. This list might well be empty, and it will always be for the @@ -233,8 +234,8 @@ data CoAxBranch { cab_loc :: SrcSpan -- Location of the defining equation -- See Note [CoAxiom locations] , cab_tvs :: [TyVar] -- Bound type variables; not necessarily fresh - , cab_eta_tvs :: [TyVar] -- Eta-reduced tyvars -- See Note [CoAxBranch type variables] + , cab_eta_tvs :: [TyVar] -- Eta-reduced tyvars -- cab_tvs and cab_lhs may be eta-reduced; see -- Note [Eta reduction for data families] , cab_cvs :: [CoVar] -- Bound coercion variables diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs index 60a7052643..cc4b84faa9 100644 --- a/compiler/GHC/Core/DataCon.hs +++ b/compiler/GHC/Core/DataCon.hs @@ -425,7 +425,7 @@ data DataCon -- NB: for a data instance, the original user result type may -- differ from the DataCon's representation TyCon. Example -- data instance T [a] where MkT :: a -> T [a] - -- The OrigResTy is T [a], but the dcRepTyCon might be :T123 + -- The dcOrigResTy is T [a], but the dcRepTyCon might be R:TList -- Now the strictness annotations and field labels of the constructor dcSrcBangs :: [HsSrcBang], @@ -1576,4 +1576,3 @@ splitDataProductType_maybe ty = Just (tycon, ty_args, con, dataConInstArgTys con ty_args) | otherwise = Nothing - diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs index 8408bc5406..4a685ba096 100644 --- a/compiler/GHC/Core/FamInstEnv.hs +++ b/compiler/GHC/Core/FamInstEnv.hs @@ -640,16 +640,13 @@ that Note. mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars -> [TyVar] -- Extra eta tyvars -> [CoVar] -- possibly stale covars - -> TyCon -- family/newtype TyCon (for error-checking only) -> [Type] -- LHS patterns -> Type -- RHS -> [Role] -> SrcSpan -> CoAxBranch -mkCoAxBranch tvs eta_tvs cvs ax_tc lhs rhs roles loc - = -- See Note [CoAxioms are homogeneous] in "GHC.Core.Coercion.Axiom" - ASSERT( typeKind (mkTyConApp ax_tc lhs) `eqType` typeKind rhs ) - CoAxBranch { cab_tvs = tvs' +mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc + = CoAxBranch { cab_tvs = tvs' , cab_eta_tvs = eta_tvs' , cab_cvs = cvs' , cab_lhs = tidyTypes env lhs @@ -703,7 +700,7 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty , co_ax_implicit = False , co_ax_branches = unbranched (branch { cab_incomps = [] }) } where - branch = mkCoAxBranch tvs eta_tvs cvs fam_tc lhs_tys rhs_ty + branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty (map (const Nominal) tvs) (getSrcSpan ax_name) @@ -721,7 +718,7 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty , co_ax_tc = tycon , co_ax_branches = unbranched (branch { cab_incomps = [] }) } where - branch = mkCoAxBranch tvs [] [] tycon (mkTyVarTys tvs) rhs_ty + branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty roles (getSrcSpan name) {- diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index e7385be78f..32abec0521 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -8,13 +8,12 @@ See Note [Core Lint guarantee]. -} {-# LANGUAGE CPP #-} -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE ScopedTypeVariables, DeriveFunctor #-} +{-# LANGUAGE ViewPatterns, ScopedTypeVariables, DeriveFunctor, MultiWayIf #-} module GHC.Core.Lint ( lintCoreBindings, lintUnfolding, lintPassResult, lintInteractiveExpr, lintExpr, - lintAnnots, lintTypes, + lintAnnots, lintAxioms, -- ** Debug output endPass, endPassIO, @@ -36,7 +35,7 @@ import GHC.Types.Literal import GHC.Core.DataCon import GHC.Builtin.Types.Prim import GHC.Builtin.Types ( multiplicityTy ) -import GHC.Tc.Utils.TcType ( isFloatingTy ) +import GHC.Tc.Utils.TcType ( isFloatingTy, isTyFamFree ) import GHC.Types.Var as Var import GHC.Types.Var.Env import GHC.Types.Var.Set @@ -56,9 +55,10 @@ import GHC.Types.RepType import GHC.Core.TyCo.Rep -- checks validity of types/coercions import GHC.Core.TyCo.Subst import GHC.Core.TyCo.FVs -import GHC.Core.TyCo.Ppr ( pprTyVar ) +import GHC.Core.TyCo.Ppr ( pprTyVar, pprTyVars ) import GHC.Core.TyCon as TyCon import GHC.Core.Coercion.Axiom +import GHC.Core.Unify import GHC.Types.Basic import GHC.Utils.Error as Err import GHC.Data.List.SetOps @@ -76,7 +76,7 @@ import GHC.Driver.Session import Control.Monad import GHC.Utils.Monad import Data.Foldable ( toList ) -import Data.List.NonEmpty ( NonEmpty ) +import Data.List.NonEmpty ( NonEmpty(..), groupWith ) import Data.List ( partition ) import Data.Maybe import GHC.Data.Pair @@ -1587,18 +1587,6 @@ lintIdBndr top_lvl bind_site id thing_inside %************************************************************************ -} -lintTypes :: DynFlags - -> [TyCoVar] -- Treat these as in scope - -> [Type] - -> Maybe MsgDoc -- Nothing => OK -lintTypes dflags vars tys - | isEmptyBag errs = Nothing - | otherwise = Just (pprMessageBag errs) - where - (_warns, errs) = initL dflags (defaultLintFlags dflags) vars linter - linter = lintBinders LambdaBind vars $ \_ -> - mapM_ lintType tys - lintValueType :: Type -> LintM LintedType -- Types only, not kinds -- Check the type, and apply the substitution to it @@ -1617,7 +1605,7 @@ checkTyCon tc = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc) ------------------- -lintType :: LintedType -> LintM LintedType +lintType :: Type -> LintM LintedType -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] @@ -2342,6 +2330,175 @@ lintCoercion (HoleCo h) = do { addErrL $ text "Unfilled coercion hole:" <+> ppr h ; lintCoercion (CoVarCo (coHoleCoVar h)) } +{- +************************************************************************ +* * + Axioms +* * +************************************************************************ +-} + +lintAxioms :: DynFlags + -> [CoAxiom Branched] + -> WarnsAndErrs +lintAxioms dflags axioms + = initL dflags (defaultLintFlags dflags) [] $ + do { mapM_ lint_axiom axioms + ; let axiom_groups = groupWith coAxiomTyCon axioms + ; mapM_ lint_axiom_group axiom_groups } + +lint_axiom :: CoAxiom Branched -> LintM () +lint_axiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches + , co_ax_role = ax_role }) + = addLoc (InAxiom ax) $ + do { mapM_ (lint_branch tc) branch_list + ; extra_checks } + where + branch_list = fromBranches branches + + extra_checks + | isNewTyCon tc + = do { CoAxBranch { cab_tvs = tvs + , cab_eta_tvs = eta_tvs + , cab_cvs = cvs + , cab_roles = roles + , cab_lhs = lhs_tys } + <- case branch_list of + [branch] -> return branch + _ -> failWithL (text "multi-branch axiom with newtype") + ; let ax_lhs = mkInfForAllTys tvs $ + mkTyConApp tc lhs_tys + nt_tvs = takeList tvs (tyConTyVars tc) + -- axiom may be eta-reduced: Note [Newtype eta] in GHC.Core.TyCon + nt_lhs = mkInfForAllTys nt_tvs $ + mkTyConApp tc (mkTyVarTys nt_tvs) + -- See Note [Newtype eta] in GHC.Core.TyCon + ; lintL (ax_lhs `eqType` nt_lhs) + (text "Newtype axiom LHS does not match newtype definition") + ; lintL (null cvs) + (text "Newtype axiom binds coercion variables") + ; lintL (null eta_tvs) -- See Note [Eta reduction for data families] + -- which is not about newtype axioms + (text "Newtype axiom has eta-tvs") + ; lintL (ax_role == Representational) + (text "Newtype axiom role not representational") + ; lintL (roles `equalLength` tvs) + (text "Newtype axiom roles list is the wrong length." $$ + text "roles:" <+> sep (map ppr roles)) + ; lintL (roles == takeList roles (tyConRoles tc)) + (vcat [ text "Newtype axiom roles do not match newtype tycon's." + , text "axiom roles:" <+> sep (map ppr roles) + , text "tycon roles:" <+> sep (map ppr (tyConRoles tc)) ]) + } + + | isFamilyTyCon tc + = do { if | isTypeFamilyTyCon tc + -> lintL (ax_role == Nominal) + (text "type family axiom is not nominal") + + | isDataFamilyTyCon tc + -> lintL (ax_role == Representational) + (text "data family axiom is not representational") + + | otherwise + -> addErrL (text "A family TyCon is neither a type family nor a data family:" <+> ppr tc) + + ; mapM_ (lint_family_branch tc) branch_list } + + | otherwise + = addErrL (text "Axiom tycon is neither a newtype nor a family.") + +lint_branch :: TyCon -> CoAxBranch -> LintM () +lint_branch ax_tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs + , cab_lhs = lhs_args, cab_rhs = rhs }) + = lintBinders LambdaBind (tvs ++ cvs) $ \_ -> + do { let lhs = mkTyConApp ax_tc lhs_args + ; lhs' <- lintType lhs + ; rhs' <- lintType rhs + ; let lhs_kind = typeKind lhs' + rhs_kind = typeKind rhs' + ; lintL (lhs_kind `eqType` rhs_kind) $ + hang (text "Inhomogeneous axiom") + 2 (text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind $$ + text "rhs:" <+> ppr rhs <+> dcolon <+> ppr rhs_kind) } + +-- these checks do not apply to newtype axioms +lint_family_branch :: TyCon -> CoAxBranch -> LintM () +lint_family_branch fam_tc br@(CoAxBranch { cab_tvs = tvs + , cab_eta_tvs = eta_tvs + , cab_cvs = cvs + , cab_roles = roles + , cab_lhs = lhs + , cab_incomps = incomps }) + = do { lintL (isDataFamilyTyCon fam_tc || null eta_tvs) + (text "Type family axiom has eta-tvs") + ; lintL (all (`elemVarSet` tyCoVarsOfTypes lhs) tvs) + (text "Quantified variable in family axiom unused in LHS") + ; lintL (all isTyFamFree lhs) + (text "Type family application on LHS of family axiom") + ; lintL (all (== Nominal) roles) + (text "Non-nominal role in family axiom" $$ + text "roles:" <+> sep (map ppr roles)) + ; lintL (null cvs) + (text "Coercion variables bound in family axiom") + ; forM_ incomps $ \ br' -> + lintL (not (compatible_branches br br')) $ + text "Incorrect incompatible branch:" <+> ppr br' } + +lint_axiom_group :: NonEmpty (CoAxiom Branched) -> LintM () +lint_axiom_group (_ :| []) = return () +lint_axiom_group (ax :| axs) + = do { lintL (isOpenFamilyTyCon tc) + (text "Non-open-family with multiple axioms") + ; let all_pairs = [ (ax1, ax2) | ax1 <- all_axs + , ax2 <- all_axs ] + ; mapM_ (lint_axiom_pair tc) all_pairs } + where + all_axs = ax : axs + tc = coAxiomTyCon ax + +lint_axiom_pair :: TyCon -> (CoAxiom Branched, CoAxiom Branched) -> LintM () +lint_axiom_pair tc (ax1, ax2) + | Just br1@(CoAxBranch { cab_tvs = tvs1 + , cab_lhs = lhs1 + , cab_rhs = rhs1 }) <- coAxiomSingleBranch_maybe ax1 + , Just br2@(CoAxBranch { cab_tvs = tvs2 + , cab_lhs = lhs2 + , cab_rhs = rhs2 }) <- coAxiomSingleBranch_maybe ax2 + = lintL (compatible_branches br1 br2) $ + vcat [ hsep [ text "Axioms", ppr ax1, text "and", ppr ax2 + , text "are incompatible" ] + , text "tvs1 =" <+> pprTyVars tvs1 + , text "lhs1 =" <+> ppr (mkTyConApp tc lhs1) + , text "rhs1 =" <+> ppr rhs1 + , text "tvs2 =" <+> pprTyVars tvs2 + , text "lhs2 =" <+> ppr (mkTyConApp tc lhs2) + , text "rhs2 =" <+> ppr rhs2 ] + + | otherwise + = addErrL (text "Open type family axiom has more than one branch: either" <+> + ppr ax1 <+> text "or" <+> ppr ax2) + +compatible_branches :: CoAxBranch -> CoAxBranch -> Bool +-- True <=> branches are compatible. See Note [Compatibility] in GHC.Core.FamInstEnv. +compatible_branches (CoAxBranch { cab_tvs = tvs1 + , cab_lhs = lhs1 + , cab_rhs = rhs1 }) + (CoAxBranch { cab_tvs = tvs2 + , cab_lhs = lhs2 + , cab_rhs = rhs2 }) + = -- we need to freshen ax2 w.r.t. ax1 + -- do this by pretending tvs1 are in scope when processing tvs2 + let in_scope = mkInScopeSet (mkVarSet tvs1) + subst0 = mkEmptyTCvSubst in_scope + (subst, _) = substTyVarBndrs subst0 tvs2 + lhs2' = substTys subst lhs2 + rhs2' = substTy subst rhs2 + in + case tcUnifyTys (const BindMe) lhs1 lhs2' of + Just unifying_subst -> substTy unifying_subst rhs1 `eqType` + substTy unifying_subst rhs2' + Nothing -> True {- ************************************************************************ @@ -2539,6 +2696,7 @@ data LintLocInfo | TopLevelBindings | InType Type -- Inside a type | InCo Coercion -- Inside a coercion + | InAxiom (CoAxiom Branched) -- Inside a CoAxiom initL :: DynFlags -> LintFlags -> [Var] -> LintM a -> WarnsAndErrs -- Warnings and errors @@ -2822,6 +2980,34 @@ dumpLoc (InType ty) = (noSrcLoc, text "In the type" <+> quotes (ppr ty)) dumpLoc (InCo co) = (noSrcLoc, text "In the coercion" <+> quotes (ppr co)) +dumpLoc (InAxiom ax) + = (getSrcLoc ax_name, text "In the coercion axiom" <+> ppr ax_name <+> dcolon <+> pp_ax) + where + CoAxiom { co_ax_name = ax_name + , co_ax_tc = tc + , co_ax_role = ax_role + , co_ax_branches = branches } = ax + branch_list = fromBranches branches + + pp_ax + | [branch] <- branch_list + = pp_branch branch + + | otherwise + = braces $ vcat (map pp_branch branch_list) + + pp_branch (CoAxBranch { cab_tvs = tvs + , cab_cvs = cvs + , cab_lhs = lhs_tys + , cab_rhs = rhs_ty }) + = sep [ brackets (pprWithCommas pprTyVar (tvs ++ cvs)) <> dot + , ppr (mkTyConApp tc lhs_tys) + , text "~_" <> pp_role ax_role + , ppr rhs_ty ] + + pp_role Nominal = text "N" + pp_role Representational = text "R" + pp_role Phantom = text "P" pp_binders :: [Var] -> SDoc pp_binders bs = sep (punctuate comma (map pp_binder bs)) diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index aa5c3460b0..e4f31e9fe0 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -293,7 +293,14 @@ See also Note [Wrappers for data instance tycons] in GHC.Types.Id.Make Indeed the latter type is unknown to the programmer. - There *is* an instance for (T Int) in the type-family instance - environment, but it is only used for overlap checking + environment, but it is looked up (via tcLookupDataFamilyInst) + in can_eq_nc (via tcTopNormaliseNewTypeTF_maybe) when trying to + solve representational equalities like + T Int ~R# Bool + Here we look up (T Int), convert it to R:TInt, and then unwrap the + newtype R:TInt. + + It is also looked up in reduceTyFamApp_maybe. - It's fine to have T in the LHS of a type function: type instance F (T a) = [a] @@ -1251,34 +1258,21 @@ example, newtype T a = MkT (a -> a) -the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t -> t. - -In the case that the right hand side is a type application -ending with the same type variables as the left hand side, we -"eta-contract" the coercion. So if we had - - newtype S a = MkT [a] - -then we would generate the arity 0 axiom CoS : S ~ []. The -primary reason we do this is to make newtype deriving cleaner. +the NewTyCon for T will contain nt_co = CoT where CoT :: forall a. T a ~ a -> a. -In the paper we'd write - axiom CoT : (forall t. T t) ~ (forall t. [t]) -and then when we used CoT at a particular type, s, we'd say - CoT @ s -which encodes as (TyConApp instCoercionTyCon [TyConApp CoT [], s]) +We might also eta-contract the axiom: see Note [Newtype eta]. Note [Newtype eta] ~~~~~~~~~~~~~~~~~~ Consider newtype Parser a = MkParser (IO a) deriving Monad -Are these two types equal (to Core)? +Are these two types equal (that is, does a coercion exist between them)? Monad Parser Monad IO which we need to make the derived instance for Monad Parser. Well, yes. But to see that easily we eta-reduce the RHS type of -Parser, in this case to ([], Froogle), so that even unsaturated applications +Parser, in this case to IO, so that even unsaturated applications of Parser will work right. This eta reduction is done when the type constructor is built, and cached in NewTyCon. diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index 1ab1986d74..5bb11a9ee7 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -70,7 +70,6 @@ module GHC.Core.Type ( getRuntimeRep_maybe, kindRep_maybe, kindRep, mkCastTy, mkCoercionTy, splitCastTy_maybe, - discardCast, userTypeError_maybe, pprUserTypeErrorTy, @@ -1402,20 +1401,6 @@ tyConBindersTyCoBinders = map to_tyb to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis) to_tyb (Bndr tv (AnonTCB af)) = Anon af (tymult (varType tv)) --- | Drop the cast on a type, if any. If there is no --- cast, just return the original type. This is rarely what --- you want. The CastTy data constructor (in "GHC.Core.TyCo.Rep") has the --- invariant that another CastTy is not inside. See the --- data constructor for a full description of this invariant. --- Since CastTy cannot be nested, the result of discardCast --- cannot be a CastTy. -discardCast :: Type -> Type -discardCast (CastTy ty _) = ASSERT(not (isCastTy ty)) ty - where - isCastTy CastTy{} = True - isCastTy _ = False -discardCast ty = ty - {- -------------------------------------------------------------------- |