[Git][ghc/ghc][wip/T18300] Add proper axiom linter
Richard Eisenberg
gitlab at gitlab.haskell.org
Tue Jun 16 16:50:30 UTC 2020
Richard Eisenberg pushed to branch wip/T18300 at Glasgow Haskell Compiler / GHC
Commits:
559dd456 by Richard Eisenberg at 2020-06-16T17:49:14+01:00
Add proper axiom linter
Also, other small wibbles from reviewing !3507
- - - - -
14 changed files:
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Instance/Family.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/Types.hs
- docs/core-spec/CoreLint.ott
- docs/core-spec/CoreSyn.ott
- docs/core-spec/core-spec.mng
- docs/core-spec/core-spec.pdf
Changes:
=====================================
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
=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -1514,4 +1514,3 @@ splitDataProductType_maybe ty
= Just (tycon, ty_args, con, dataConInstArgTys con ty_args)
| otherwise
= Nothing
-
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -647,13 +647,13 @@ mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
-> CoAxBranch
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
- , cab_roles = roles
- , cab_rhs = tidyType env rhs
- , cab_loc = loc
- , cab_incomps = placeHolderIncomps }
+ , cab_eta_tvs = eta_tvs'
+ , cab_cvs = cvs'
+ , cab_lhs = tidyTypes env lhs
+ , cab_roles = roles
+ , cab_rhs = tidyType env rhs
+ , cab_loc = loc
+ , cab_incomps = placeHolderIncomps }
where
(env1, tvs') = tidyVarBndrs init_tidy_env tvs
(env2, eta_tvs') = tidyVarBndrs env1 eta_tvs
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -8,12 +8,12 @@ See Note [Core Lint guarantee].
-}
{-# LANGUAGE CPP #-}
-{-# LANGUAGE ScopedTypeVariables, DeriveFunctor #-}
+{-# LANGUAGE ScopedTypeVariables, DeriveFunctor, MultiWayIf #-}
module GHC.Core.Lint (
lintCoreBindings, lintUnfolding,
lintPassResult, lintInteractiveExpr, lintExpr,
- lintAnnots, lintAxiom,
+ lintAnnots, lintAxioms,
-- ** Debug output
endPass, endPassIO,
@@ -34,7 +34,7 @@ import GHC.Data.Bag
import GHC.Types.Literal
import GHC.Core.DataCon
import GHC.Builtin.Types.Prim
-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
@@ -51,9 +51,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
@@ -71,7 +72,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
@@ -1490,33 +1491,6 @@ lintIdBndr top_lvl bind_site id thing_inside
%************************************************************************
-}
-lintAxiom :: DynFlags
- -> CoAxiom Unbranched
- -> Maybe MsgDoc -- Nothing => OK
-lintAxiom dflags axiom
- | isEmptyBag errs = Nothing
- | otherwise = Just (pprMessageBag errs)
- where
- (_warns, errs) = initL dflags defaultLintFlags [] $
- lint_axiom axiom
-
-lint_axiom :: CoAxiom Unbranched -> LintM ()
-lint_axiom ax@(CoAxiom { co_ax_tc = fam_tc })
- = lintBinders LambdaBind (tvs ++ cvs) $ \_ ->
- do { let lhs = mkTyConApp fam_tc lhs_args
- ; lhs' <- lintType lhs
- ; rhs' <- lintType rhs
- ; let lhs_kind = typeKind lhs'
- rhs_kind = typeKind rhs'
- ; checkL (lhs_kind `eqType` rhs_kind) $
- hang (text "Inhomogeneous axiom")
- 2 (ppr ax $$ text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind
- $$ text "rhs:" <+> ppr rhs <+> dcolon <+> ppr rhs_kind) }
- where
- CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
- , cab_lhs = lhs_args, cab_rhs = rhs } = coAxiomSingleBranch ax
-
-
lintValueType :: Type -> LintM LintedType
-- Types only, not kinds
-- Check the type, and apply the substitution to it
@@ -2249,6 +2223,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 [] $
+ 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
{-
************************************************************************
@@ -2422,6 +2565,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
@@ -2664,6 +2808,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))
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -1257,34 +1257,21 @@ example,
newtype T a = MkT (a -> a)
-the NewTyCon for T will contain nt_co = CoT where CoT t : T t ~ t -> t.
+the NewTyCon for T will contain nt_co = CoT where CoT :: forall a. T a ~ a -> a.
-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.
-
-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.
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -3235,7 +3235,8 @@ data DataSort
-- 2. @k@ (where @k@ is a bare kind variable; see #12369)
--
-- See also Note [Datatype return kinds] in GHC.Tc.TyCl
-checkDataKindSig :: DataSort -> Kind -> TcM ()
+checkDataKindSig :: DataSort -> Kind -- any arguments in the kind are stripped off
+ -> TcM ()
checkDataKindSig data_sort kind
= do { dflags <- getDynFlags
; traceTc "checkDataKindSig" (ppr kind)
=====================================
compiler/GHC/Tc/Instance/Family.hs
=====================================
@@ -162,27 +162,13 @@ addressed yet.
newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
-- Freshen the type variables of the FamInst branches
newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
- = do { -- Use lintAxiom to check that the axiom is well formed
- dflags <- getDynFlags
- ; ifErrsM (return ()) $ -- Don't lint when there are errors, because
- -- errors might mean TcTyCons.
- -- See Note [Recover from validity error] in GHC.Tc.TyCl
- when (gopt Opt_DoCoreLinting dflags) $
- case lintAxiom dflags axiom of
- Nothing -> pure ()
- Just fail_msg -> pprPanic "Core Lint error in newFamInst" $
- vcat [ fail_msg
- , ppr fam_tc
- , ppr tvs
- , ppr cvs
- , ppr lhs
- , ppr rhs ]
-
- -- Freshen the type variables
- ; (subst, tvs') <- freshenTyVarBndrs tvs
+ = do {
+ -- Freshen the type variables
+ (subst, tvs') <- freshenTyVarBndrs tvs
; (subst, cvs') <- freshenCoVarBndrsX subst cvs
; let lhs' = substTys subst lhs
rhs' = substTy subst rhs
+
; return (FamInst { fi_fam = tyConName fam_tc
, fi_flavor = flavor
, fi_tcs = roughMatchTcs lhs
=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -268,6 +268,14 @@ tcRnModuleTcRnM hsc_env mod_sum
then tcRnHsBootDecls hsc_src local_decls
else {-# SCC "tcRnSrcDecls" #-}
tcRnSrcDecls explicit_mod_hdr local_decls export_ies
+
+ ; whenM (goptM Opt_DoCoreLinting) $
+ do { let (warns, errs) = lintGblEnv (hsc_dflags hsc_env) tcg_env
+ ; mapBagM_ (addWarn NoReason) warns
+ ; mapBagM_ addErr errs
+ ; failIfErrsM } -- if we have a lint error, we're only
+ -- going to get in deeper trouble by proceeding
+
; setGblEnv tcg_env
$ do { -- Process the export list
traceRn "rn4a: before exports" empty
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -1803,29 +1803,11 @@ DT1 Where this applies: Only GADT syntax for data/newtype/instance declarations
can have declared return kinds. This Note does not apply to Haskell98
syntax.
-DT2 Where these kinds come from: Return kinds are processed through several
- different code paths:
-
- Data/newtypes: The return kind is part of the TyCon kind, gotten either
+DT2 Where these kinds come from: The return kind is part of the TyCon kind, gotten either
by checkInitialKind (standalone kind signature / CUSK) or
inferInitialKind. It is extracted by bindTyClTyVars in tcTyClDecl1. It is
then passed to tcDataDefn.
- Families: The return kind is either written in a standalone signature
- or extracted from a family declaration in getInitialKind.
- If a family declaration is missing a result kind, it is assumed to be
- Type. This assumption is in getInitialKind for CUSKs or
- get_fam_decl_initial_kind for non-signature & non-CUSK cases.
-
- Instances: The data family already has a known kind. The return kind
- of an instance is then calculated by applying the data family tycon
- to the patterns provided, as computed by the typeKind lhs_ty in the
- end of tcDataFamInstHeader. In the case of an instance written in GADT
- syntax, there are potentially *two* return kinds: the one computed from
- applying the data family tycon to the patterns, and the one given by
- the user. This second kind is checked by the tc_kind_sig function within
- tcDataFamInstHeader.
-
DT3 Eta-expansion: Any forall-bound variables and function arguments in a result kind
become parameters to the type. That is, when we say
@@ -1833,9 +1815,7 @@ DT3 Eta-expansion: Any forall-bound variables and function arguments in a result
we really mean for T to have two parameters. The second parameter
is produced by processing the return kind in etaExpandAlgTyCon,
- called in tcDataDefn for data/newtypes and in tcDataFamInstDecl
- for instances. This is true for data families as well, though their
- arity only matters for pretty-printing.
+ called in tcDataDefn.
See also Note [TyConBinders for the result kind signatures of a data type]
in GHC.Tc.Gen.HsType.
@@ -1856,7 +1836,7 @@ DT4 Datatype return kind restriction: A data type return kind must end
Exactly the same applies to data instance (but not data family)
declarations. Examples
data instance D1 :: Type -- good
- data instance D2 :: Boool -> Type -- good
+ data instance D2 :: Bool -> Type -- good
We can "look through" type synonyms
type Star = Type
@@ -1886,7 +1866,6 @@ DT5 Newtype return kind restriction.
If -XUnliftedNewtypes is not on, then newtypes are treated just
like datatypes --- see (4) above.
-
If -XUnliftedNewtypes is on, then a newtype return kind must end in
TYPE xyz, for some xyz (after type synonym expansion). The "xyz"
may include type families, but the TYPE part must be visible
@@ -1921,7 +1900,24 @@ data family T a :: <kind> -- See Point DF56
data instance T [a] :: <kind> where ... -- See Point DF2
newtype instance T [a] :: <kind> where ... -- See Point DF2
-Here is the Plan for Data Families
+Here is the Plan for Data Families:
+
+DF0 Where these kinds come from:
+
+ Families: The return kind is either written in a standalone signature
+ or extracted from a family declaration in getInitialKind.
+ If a family declaration is missing a result kind, it is assumed to be
+ Type. This assumption is in getInitialKind for CUSKs or
+ get_fam_decl_initial_kind for non-signature & non-CUSK cases.
+
+ Instances: The data family already has a known kind. The return kind
+ of an instance is then calculated by applying the data family tycon
+ to the patterns provided, as computed by the typeKind lhs_ty in the
+ end of tcDataFamInstHeader. In the case of an instance written in GADT
+ syntax, there are potentially *two* return kinds: the one computed from
+ applying the data family tycon to the patterns, and the one given by
+ the user. This second kind is checked by the tc_kind_sig function within
+ tcDataFamInstHeader. See also DF3, below.
DF1 In a data/newtype instance, we treat the kind of the /data family/,
once instantiated, as the "master kind" for the representation
@@ -1933,14 +1929,16 @@ DF1 In a data/newtype instance, we treat the kind of the /data family/,
if we declared
data R:T1Int :: Type -> Type where ...
See Note [Liberalising data family return kinds] for an alternative
- plan. But this plan is simple, and ensures that all instances
- are simple instantiations of the matster, without strange casts.
+ plan. But this current plan is simple, and ensures that all instances
+ are simple instantiations of the master, without strange casts.
An example with non-trivial instantiation:
data family T2 :: forall k. Type -> k
- data instance T :: Type -> Type -> Type where ...
+ data instance T2 :: Type -> Type -> Type where ...
Here 'k' gets instantiated with (Type -> Type), driven by
- the signature on the 'data instance'
+ the signature on the 'data instance'. (See also DT3 of
+ Note [Datatype return kinds] about eta-expansion, which applies here,
+ too; see tcDataFamInstDecl's call of etaExpandAlgTyCon.)
A newtype example:
@@ -1960,7 +1958,7 @@ DF1 In a data/newtype instance, we treat the kind of the /data family/,
DF2 /After/ this instantiation, the return kind of the master kind
must obey the usual rules for data/newtype return kinds (DT4, DT5)
- above. Examples:
+ of Note [Datatype return kinds]. Examples:
data family T3 k :: k
data instance T3 Type where ... -- OK
data instance T3 (Type->Type) where ... -- OK
@@ -1983,25 +1981,25 @@ DF3 Any kind signatures on the data/newtype instance are checked for
data instance declaration
DF4 We also (redundantly) check that any user-specified return kind
- signature in the data instance also obeys (4). For example we
+ signature in the data instance also obeys DT4/DT5. For example we
reject
data family T1 :: Type -> Type -> Type
data instance T1 Int :: Type -> F Int
- even if (F Int ~ Bool). We could omit this check, because we
+ even if (F Int ~ Type). We could omit this check, because we
use the master kind; but it seems more uniform to check it, again
with checkDataKindSig.
DF5 Data /family/ return kind restrictions. Consider
data family D8 a :: F a
where F is a type family. No data/newtype instance can instantiate
- this so that it obeys the rules of (4) and (5). So GHC proactively
+ this so that it obeys the rules of DT4 or DT5. So GHC proactively
rejects the data /family/ declaration if it can never satisfy (DT4)/(DT5).
Remember that a data family supports both data and newtype instances.
More precisely, the return kind of a data family must be either
* TYPE xyz (for some type xyz) or
* a kind variable
- Only in these cases can a data/newtype instance possibly satisfy (4)/(5).
+ Only in these cases can a data/newtype instance possibly satisfy (DT4)/(DT5).
This is checked by the call to checkDataKindSig in tcFamDecl1. Examples:
data family D1 :: Type -- good
@@ -2014,7 +2012,7 @@ DF5 Data /family/ return kind restrictions. Consider
DF6 Two return kinds for instances: If an instance has two return kinds,
one from the family declaration and one from the instance declaration
- (see point (2) above), they are unified. More accurately, we make sure
+ (see point DF3 above), they are unified. More accurately, we make sure
that the kind of the applied data family is a subkind of the user-written
kind. GHC.Tc.Gen.HsType.checkExpectedKind normally does this check for types, but
that's overkill for our needs here. Instead, we just instantiate any
@@ -2025,8 +2023,6 @@ DF6 Two return kinds for instances: If an instance has two return kinds,
the kind annotation on the instance is redundant (except perhaps for
effects of unification).
-
-
This all is Wrinkle (3) in Note [Implementation of UnliftedNewtypes].
Note [Liberalising data family return kinds]
@@ -2058,7 +2054,7 @@ well. But there are lots of complications:
exactly dual way.
So yes, we could allow this, but we currently do not. That's
-why we have
+why we have DF2 in Note [Data family/instance return kinds].
Note [Implementation of UnliftedNewtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2175,7 +2171,7 @@ There are also some changes for dealing with families:
we use that kind signature.
3. A data family and its newtype instance may be declared with slightly
- different kinds. See point 7 in Note [Datatype return kinds].
+ different kinds. See point DF6 in Note [Data family/instance return kinds]
There's also a change in the renamer:
=====================================
compiler/GHC/Tc/Types.hs
=====================================
@@ -79,7 +79,10 @@ module GHC.Tc.Types(
-- Role annotations
RoleAnnotEnv, emptyRoleAnnotEnv, mkRoleAnnotEnv,
- lookupRoleAnnot, getRoleAnnots
+ lookupRoleAnnot, getRoleAnnots,
+
+ -- Linting
+ lintGblEnv
) where
#include "HsVersions.h"
@@ -93,6 +96,7 @@ import GHC.Tc.Types.Evidence
import GHC.Core.Type
import GHC.Core.TyCon ( TyCon, tyConKind )
import GHC.Core.PatSyn ( PatSyn )
+import GHC.Core.Lint ( lintAxioms )
import GHC.Types.Id ( idType, idName )
import GHC.Types.FieldLabel ( FieldLabel )
import GHC.Tc.Utils.TcType
@@ -1734,3 +1738,16 @@ lookupRoleAnnot = lookupNameEnv
getRoleAnnots :: [Name] -> RoleAnnotEnv -> [LRoleAnnotDecl GhcRn]
getRoleAnnots bndrs role_env
= mapMaybe (lookupRoleAnnot role_env) bndrs
+
+{- *********************************************************************
+* *
+ Linting a TcGblEnv
+* *
+********************************************************************* -}
+
+-- | Check the 'TcGblEnv' for consistency. Currently, only checks
+-- axioms, but should check other aspects, too.
+lintGblEnv :: DynFlags -> TcGblEnv -> (Bag SDoc, Bag SDoc)
+lintGblEnv dflags tcg_env = lintAxioms dflags axioms
+ where
+ axioms = typeEnvCoAxioms (tcg_type_env tcg_env)
=====================================
docs/core-spec/CoreLint.ott
=====================================
@@ -656,3 +656,43 @@ unify(</ tj // j />, </ t'j // j />) = subst
subst(s) = subst(s')
----------------------------------------- :: CompatCoincident
no_conflict(C, </ sj // j />, ind1, ind2)
+
+defn |- axiom C ok :: :: lint_axiom :: 'Ax_'
+ {{ com Coercion axiom linting, \coderef{GHC/Core/Lint.hs}{lint\_axiom} }}
+ {{ tex \labeledjudge{axiom} [[C]] [[ok]] }}
+by
+
+isNewTyCon T
+</ Ri // i /> = tyConRoles T
+</ alphai_ki // i /> |-ty T </ alphai$ // i /> : k0
+</ alphai_ki // i /> |-ty s : k0
+------------------------------ :: Newtype
+|-axiom T_Rep forall </ alphai_ki RAi // i />. (</ alphai$ // i /> ~> s) ok
+
+isOpenTypeFamilyTyCon T
+T |-branch b ok
+------------------------------ :: OpenTypeFamily
+|-axiom T_Nom b ok
+
+isClosedTypeFamilyTyCon T
+</ T |-branch bi ok // i />
+--------------------------- :: ClosedTypeFamily
+|-axiom T_Nom </ bi // i /> ok
+
+isDataFamilyTyCon T
+T |-branch b ok
+--------------------------- :: DataFamily
+|-axiom T_Rep b ok
+
+defn T |- branch b ok :: :: lint_family_branch :: 'Br_'
+ {{ com Type family branch linting, \coderef{GHC/Core/Lint.hs}{lint\_family\_branch} }}
+ {{ tex [[T]] \labeledjudge{branch} [[b]] [[ok]] }}
+by
+
+</ Ri = Nom // i />
+</ isTyFamFree tj // j />
+fv(</ tj // j />) = </ alphai$ // i />
+</ alphai_ki // i /> |-ty T </ tj // j /> : k0
+</ alphai_ki // i /> |-ty s : k0
+---------------------------------------------------------------- :: OK
+T |-branch forall </ alphai_ki RAi // i />. (</ tj // j /> ~> s) ok
=====================================
docs/core-spec/CoreSyn.ott
=====================================
@@ -52,10 +52,10 @@ l :: 'Label_' ::= {{ com Labels for join points, also \coderef{GHC/Types/Var.hs}
vars :: 'Vars_' ::= {{ com List of variables }}
| </ ni // , // i /> :: :: List
- | fv ( t ) :: M :: fv_t
- {{ tex \textit{fv}([[t]]) }}
| fv ( e ) :: M :: fv_e
{{ tex \textit{fv}([[e]]) }}
+ | fv ( types ) :: M :: fv_types
+ {{ tex \textit{fv}([[types]]) }}
| empty :: M :: empty
| vars1 \inter vars2 :: M :: intersection
{{ tex [[vars1]] \cap [[vars2]] }}
@@ -197,7 +197,7 @@ R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{GHC/Core/Coercion/Axiom.h
axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{GHC/Core/TyCon.hs}{CoAxBranch} }}
| forall </ ni RAi // i /> . ( </ tj // j /> ~> s ) :: :: CoAxBranch {{ com \ctor{CoAxBranch}: Axiom branch }}
- | ( </ axBranchi // i /> ) [ ind ] :: M :: lookup {{ com List lookup }}
+ | ( </ axBranchi // i /> ) [ ind ] :: M :: lookup {{ com List lookup }}
mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{GHC/Core/Coercion/Axiom.hs}{CoAxiomRule} }}
| M ( I , role_list , R' ) :: :: CoAxiomRule {{ com Named rule, with parameter info }}
@@ -376,6 +376,10 @@ terminals :: 'terminals_' ::=
| dataConTyCon :: :: dataConTyCon {{ tex \textsf{dataConTyCon} }}
| dataConRepType :: :: dataConRepType {{ tex \textsf{dataConRepType} }}
| isNewTyCon :: :: isNewTyCon {{ tex \textsf{isNewTyCon} }}
+ | isOpenTypeFamilyTyCon :: :: isOpenTypeFamilyTyCon {{ tex \textsf{isOpenTypeFamilyTyCon} }}
+ | isClosedTypeFamilyTyCon :: :: isClosedTypeFamilyTyCon {{ tex \textsf{isClosedTypeFamilyTyCon} }}
+ | isDataFamilyTyCon :: :: isDataFamilyTyCon {{ tex \textsf{isDataFamilyTyCon} }}
+ | isTyFamFree :: :: isTyFamFree {{ tex \textsf{isTyFamFree} }}
| Constraint :: :: Constraint {{ tex \textsf{Constraint} }}
| TYPE :: :: TYPE {{ tex \textsf{TYPE} }}
| RuntimeRep :: :: RuntimeRep {{ tex \textsf{RuntimeRep} }}
@@ -449,6 +453,10 @@ formula :: 'formula_' ::=
| G |- tylit lit : k :: :: lintTyLit
{{ tex [[G]] \labeledjudge{tylit} [[lit]] : [[k]] }}
| isNewTyCon T :: :: isNewTyCon
+ | isOpenTypeFamilyTyCon T :: :: isOpenTypeFamilyTyCon
+ | isClosedTypeFamilyTyCon T :: :: isClosedTypeFamilyTyCon
+ | isDataFamilyTyCon T :: :: isDataFamilyTyCon
+ | isTyFamFree t :: :: isTyFamFree
| k1 elt { </ ki // , // i /> } :: :: kind_elt
| e is_a_type :: :: is_a_type
{{ tex \exists \tau \text{ s.t.~} [[e]] = \tau }}
@@ -526,3 +534,4 @@ Expr_Coercion <= Subst_TmMapping
Type_CastTy <= Var_IdOrTyVar
+Expr_Type <= Vars_fv_e
=====================================
docs/core-spec/core-spec.mng
=====================================
@@ -573,6 +573,37 @@ taking care to map identical type family applications to the same fresh variable
The algorithm $[[unify]]$ is implemented in \coderef{GHC/Core/Unify.hs}{tcUnifyTys}.
It performs a standard unification, returning a substitution upon success.
+\subsection{Axioms}
+
+After type-checking the type and class declarations of a file, the axioms
+in the file are optionally linted. This is done from \coderef{GHC/Tc/Types.hs}{lintGblEnv},
+which calls \coderef{GHC/Core/Lint.hs}{lintAxioms}. That function ensures
+the following judgement on each axiom:
+
+\ottdefnlintXXaxiom{}
+
+\ottdefnlintXXfamilyXXbranch{}
+
+In addition to these checks, the linter will also check several other conditions:
+
+\begin{itemize}
+\item Every \texttt{CoAxBranch} has a \texttt{cab\_cvs} field. This is unused
+currently and should always be empty.
+\item Every \texttt{CoAxBranch} has a \texttt{cab\_eta\_tvs} field. This is used
+only for data family instances, but is not involved in type correctness. (It is
+used for pretty-printing.) The implemented linter checks to make sure this field
+is empty for axioms that are not associated with data family instances.
+\item Every \texttt{CoAxBranch} has a \texttt{cab\_incomps} field that stores
+a list of incompatible branches. The implemented linter checks that these
+branches are indeed incompatible with the current one.
+\item The linter checks that newtypes are associated with exactly one axiom,
+as are closed type families.
+\item The linter checks that all instances of the same open family are compatible.
+\end{itemize}
+
+A nice summary of the required checks is in Section F.1 of the \emph{Safe Coercions}
+paper (JFP'16).
+
\section{Operational semantics}
\subsection{Disclaimer}
=====================================
docs/core-spec/core-spec.pdf
=====================================
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/559dd456b071efbd2b5aff9492351a7fba237a54
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/559dd456b071efbd2b5aff9492351a7fba237a54
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200616/4a712705/attachment-0001.html>
More information about the ghc-commits
mailing list