Commit 4bf18646 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Improve handling of data type return kinds

Following a long conversation with Richard, this patch tidies up the
handling of return kinds for data/newtype declarations (vanilla,
family, and instance).

I have substantially edited the Notes in TyCl, so they would
bear careful reading.

Fixes #18300, #18357

In GHC.Tc.Instance.Family.newFamInst we were checking some Lint-like
properties with ASSSERT.  Instead Richard and I have added
a proper linter for axioms, and called it from lintGblEnv, which in
turn is called in tcRnModuleTcRnM

New tests (T18300, T18357) cause an ASSERT failure in HEAD.
parent edc8d22b
Pipeline #21820 passed with stages
in 854 minutes and 19 seconds
......@@ -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
......
......@@ -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
......@@ -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)
{-
......
......@@ -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))
......
......@@ -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.
......
......@@ -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
{-
--------------------------------------------------------------------
......
......@@ -46,7 +46,8 @@ module GHC.Tc.Gen.HsType (
tcNamedWildCardBinders,
tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC,
tcInferLHsType, tcInferLHsTypeUnsaturated, tcCheckLHsType,
tcInferLHsTypeKind, tcInferLHsType, tcInferLHsTypeUnsaturated,
tcCheckLHsType,
tcHsMbContext, tcHsContext, tcLHsPredType,
failIfEmitsConstraints,
solveEqualities, -- useful re-export
......@@ -77,6 +78,7 @@ import GHC.Tc.Types.Origin
import GHC.Core.Predicate
import GHC.Tc.Types.Constraint
import GHC.Tc.Utils.Env
import GHC.Tc.Utils.Instantiate( tcInstInvisibleTyBinders )
import GHC.Tc.Utils.TcMType
import GHC.Tc.Validity
import GHC.Tc.Utils.Unify
......@@ -87,7 +89,7 @@ import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Tc.Errors ( reportAllUnsolved )
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBindersN, tcInstInvisibleTyBinder )
import GHC.Core.Type
import GHC.Builtin.Types.Prim
import GHC.Types.Name.Env
......@@ -617,12 +619,11 @@ tcHsOpenType, tcHsLiftedType,
tcHsOpenTypeNC, tcHsLiftedTypeNC :: LHsType GhcRn -> TcM TcType
-- Used for type signatures
-- Do not do validity checking
tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty
tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
tcHsOpenType hs_ty = addTypeCtxt hs_ty $ tcHsOpenTypeNC hs_ty
tcHsLiftedType hs_ty = addTypeCtxt hs_ty $ tcHsLiftedTypeNC hs_ty
tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind
; tcLHsType ty ek }
tcHsLiftedTypeNC ty = tcLHsType ty liftedTypeKind
tcHsOpenTypeNC hs_ty = do { ek <- newOpenTypeKind; tcLHsType hs_ty ek }
tcHsLiftedTypeNC hs_ty = tcLHsType hs_ty liftedTypeKind
-- Like tcHsType, but takes an expected kind
tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType
......@@ -632,15 +633,24 @@ tcCheckLHsType hs_ty exp_kind
; tcLHsType hs_ty ek }
tcInferLHsType :: LHsType GhcRn -> TcM TcType
-- Called from outside: set the context
tcInferLHsType hs_ty
= addTypeCtxt hs_ty $
do { (ty, _kind) <- tc_infer_lhs_type (mkMode TypeLevel) hs_ty
= do { (ty,_kind) <- tcInferLHsTypeKind hs_ty
; return ty }
tcInferLHsTypeKind :: LHsType GhcRn -> TcM (TcType, TcKind)
-- Called from outside: set the context
-- Eagerly instantiate any trailing invisible binders
tcInferLHsTypeKind lhs_ty@(L loc hs_ty)
= addTypeCtxt lhs_ty $
setSrcSpan loc $ -- Cover the tcInstInvisibleTyBinders
do { (res_ty, res_kind) <- tc_infer_hs_type (mkMode TypeLevel) hs_ty
; tcInstInvisibleTyBinders res_ty res_kind }
-- See Note [Do not always instantiate eagerly in types]
-- Used to check the argument of GHCi :kind
-- Allow and report wildcards, e.g. :kind T _
-- Do not saturate family applications: see Note [Dealing with :kind]
-- Does not instantiate eagerly; See Note [Do not always instantiate eagerly in types]
tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
tcInferLHsTypeUnsaturated hs_ty
= addTypeCtxt hs_ty $
......@@ -674,6 +684,19 @@ to switch off saturation.
So tcInferLHsTypeUnsaturated does a little special case for top level
applications. Actually the common case is a bare variable, as above.
Note [Do not always instantiate eagerly in types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Terms are eagerly instantiated. This means that if you say
x = id
then `id` gets instantiated to have type alpha -> alpha. The variable
alpha is then unconstrained and regeneralized. But we cannot do this
in types, as we have no type-level lambda. So, when we are sure
that we will not want to regeneralize later -- because we are done
checking a type, for example -- we can instantiate. But we do not
instantiate at variables, nor do we in tcInferLHsTypeUnsaturated,
which is used by :kind in GHCi.
************************************************************************
* *
......@@ -1648,14 +1671,14 @@ saturateFamApp :: TcType -> TcKind -> TcM (TcType, TcKind)
-- tcTypeKind ty = kind
--
-- If 'ty' is an unsaturated family application with trailing
-- invisible arguments, instanttiate them.
-- invisible arguments, instantiate them.
-- See Note [saturateFamApp]
saturateFamApp ty kind
| Just (tc, args) <- tcSplitTyConApp_maybe ty
, mustBeSaturated tc
, let n_to_inst = tyConArity tc - length args
= do { (extra_args, ki') <- tcInstInvisibleTyBinders n_to_inst kind
= do { (extra_args, ki') <- tcInstInvisibleTyBindersN n_to_inst kind
; return (ty `mkTcAppTys` extra_args, ki') }
| otherwise
= return (ty, kind)
......@@ -1712,7 +1735,7 @@ checkExpectedKind :: HasDebugCallStack
checkExpectedKind hs_ty ty act_kind exp_kind
= do { traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind)
; (new_args, act_kind') <- tcInstInvisibleTyBinders n_to_inst act_kind
; (new_args, act_kind') <- tcInstInvisibleTyBindersN n_to_inst act_kind
; let origin = TypeEqOrigin { uo_actual = act_kind'
, uo_expected = exp_kind
......@@ -1763,6 +1786,7 @@ tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
tcTyVar :: TcTyMode -> Name -> TcM (TcType, TcKind)
-- See Note [Type checking recursive type and class declarations]
-- in GHC.Tc.TyCl
-- This does not instantiate. See Note [Do not always instantiate eagerly in types]
tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
= do { traceTc "lk1" (ppr name)
; thing <- tcLookup name
......@@ -3293,12 +3317,18 @@ 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 data_sort kind = do
dflags <- getDynFlags
traceTc "checkDataKindSig" (ppr kind)
checkTc (is_TYPE_or_Type dflags || is_kind_var) (err_msg dflags)
checkDataKindSig :: DataSort -> Kind -- any arguments in the kind are stripped off
-> TcM ()
checkDataKindSig data_sort kind
= do { dflags <- getDynFlags
; traceTc "checkDataKindSig" (ppr kind)
; checkTc (is_TYPE_or_Type dflags || is_kind_var)
(err_msg dflags) }
where
res_kind = snd (tcSplitPiTys kind)
-- Look for the result kind after
-- peeling off any foralls and arrows
pp_dec :: SDoc
pp_dec = text $
case data_sort of
......@@ -3335,16 +3365,19 @@ checkDataKindSig data_sort kind = do
-- have return kind `TYPE r` unconditionally (#16827).
is_TYPE :: Bool
is_TYPE = tcIsRuntimeTypeKind kind
is_TYPE = tcIsRuntimeTypeKind res_kind
is_Type :: Bool
is_Type = tcIsLiftedTypeKind res_kind
is_TYPE_or_Type :: DynFlags -> Bool
is_TYPE_or_Type dflags | tYPE_ok dflags = is_TYPE
| otherwise = tcIsLiftedTypeKind kind
| otherwise = is_Type