[Git][ghc/ghc][wip/T17923] Significant refactor of Lint
Simon Peyton Jones
gitlab at gitlab.haskell.org
Wed Mar 25 13:48:42 UTC 2020
Simon Peyton Jones pushed to branch wip/T17923 at Glasgow Haskell Compiler / GHC
Commits:
8ae203c7 by Simon Peyton Jones at 2020-03-25T13:48:00+00:00
Significant refactor of Lint
This refactoring of Lint was triggered by #17923, which is
fixed by this patch.
The main change is this. Instead of
lintType :: Type -> LintM LintedKind
we now have
lintType :: Type -> LintM LintedType
Previously, all of typeKind was effectively duplicate in lintType.
Moreover, since we have an ambient substitution, we still had to
apply the substition here and there, sometimes more than once. It
was all very tricky, in the end, and made my head hurt.
Now, lintType returns a fully linted type, with all substitutions
performed on it. This is much simpler.
The same thing is needed for Coercions. Instead of
lintCoercion :: OutCoercion
-> LintM (LintedKind, LintedKind,
LintedType, LintedType, Role)
we now have
lintCoercion :: Coercion -> LintM LintedCoercion
Much simpler! The code is shorter and less bug-prone.
There are a lot of knock on effects. But life is now better.
- - - - -
4 changed files:
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Type.hs
- + testsuite/tests/indexed-types/should_compile/T17923.hs
- testsuite/tests/indexed-types/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -8,7 +8,7 @@ See Note [Core Lint guarantee].
-}
{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE ScopedTypeVariables, DeriveFunctor #-}
module GHC.Core.Lint (
lintCoreBindings, lintUnfolding,
@@ -33,7 +33,6 @@ import GHC.Core.Op.Monad
import Bag
import Literal
import GHC.Core.DataCon
-import TysWiredIn
import TysPrim
import TcType ( isFloatingTy )
import Var
@@ -461,14 +460,17 @@ lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc,
lintCoreBindings dflags pass local_in_scope binds
= initL dflags flags local_in_scope $
addLoc TopLevelBindings $
- lintLetBndrs TopLevel binders $
- -- Put all the top-level binders in scope at the start
- -- This is because transformation rules can bring something
- -- into use 'unexpectedly'
do { checkL (null dups) (dupVars dups)
; checkL (null ext_dups) (dupExtVars ext_dups)
- ; mapM lint_bind binds }
+ ; lintRecBindings TopLevel all_pairs $
+ return () }
where
+ all_pairs = flattenBinds binds
+ -- Put all the top-level binders in scope at the start
+ -- This is because transformation rules can bring something
+ -- into use 'unexpectedly'; see Note [Glomming] in OccurAnal
+ binders = map fst all_pairs
+
flags = defaultLintFlags
{ lf_check_global_ids = check_globals
, lf_check_inline_loop_breakers = check_lbs
@@ -494,7 +496,6 @@ lintCoreBindings dflags pass local_in_scope binds
CorePrep -> AllowAtTopLevel
_ -> AllowAnywhere
- binders = bindersOfBinds binds
(_, dups) = removeDups compare binders
-- dups_ext checks for names with different uniques
@@ -509,11 +510,6 @@ lintCoreBindings dflags pass local_in_scope binds
= compare (m1, nameOccName n1) (m2, nameOccName n2)
| otherwise = LT
- -- If you edit this function, you may need to update the GHC formalism
- -- See Note [GHC Formalism]
- lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
- lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
-
{-
************************************************************************
* *
@@ -576,28 +572,32 @@ lintExpr dflags vars expr
Check a core binding, returning the list of variables bound.
-}
-lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
--- If you edit this function, you may need to update the GHC formalism
--- See Note [GHC Formalism]
-lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
- = addLoc (RhsOf binder) $
- -- Check the rhs
- do { ty <- lintRhs binder rhs
- ; binder_ty <- applySubstTy (idType binder)
- ; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty)
+lintRecBindings :: TopLevelFlag -> [(Id, CoreExpr)]
+ -> LintM a -> LintM a
+lintRecBindings top_lvl pairs thing_inside
+ = lintIdBndrs top_lvl bndrs $ \ bndrs' ->
+ do { zipWithM_ lint_pair bndrs' rhss
+ ; thing_inside }
+ where
+ (bndrs, rhss) = unzip pairs
+ lint_pair bndr' rhs
+ = addLoc (RhsOf bndr') $
+ do { rhs_ty <- lintRhs bndr' rhs -- Check the rhs
+ ; lintLetBind top_lvl Recursive bndr' rhs rhs_ty }
+
+lintLetBind :: TopLevelFlag -> RecFlag -> LintedId
+ -> CoreExpr -> LintedType -> LintM ()
+-- Binder's type, and the RHS, have already been linted
+-- This function checks other invariants
+lintLetBind top_lvl rec_flag binder rhs rhs_ty
+ = do { let binder_ty = idType binder
+ ; ensureEqTys binder_ty rhs_ty (mkRhsMsg binder (text "RHS") rhs_ty)
-- If the binding is for a CoVar, the RHS should be (Coercion co)
-- See Note [Core type and coercion invariant] in GHC.Core
; checkL (not (isCoVar binder) || isCoArg rhs)
(mkLetErr binder rhs)
- -- Check that it's not levity-polymorphic
- -- Do this first, because otherwise isUnliftedType panics
- -- Annoyingly, this duplicates the test in lintIdBdr,
- -- because for non-rec lets we call lintSingleBinding first
- ; checkL (isJoinId binder || not (isTypeLevPoly binder_ty))
- (badBndrTyMsg binder (text "levity-polymorphic"))
-
-- Check the let/app invariant
-- See Note [Core let/app invariant] in GHC.Core
; checkL ( isJoinId binder
@@ -610,14 +610,14 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
-- demanded. Primitive string literals are exempt as there is no
-- computation to perform, see Note [Core top-level string literals].
; checkL (not (isStrictId binder)
- || (isNonRec rec_flag && not (isTopLevel top_lvl_flag))
+ || (isNonRec rec_flag && not (isTopLevel top_lvl))
|| exprIsTickedString rhs)
(mkStrictMsg binder)
-- Check that if the binder is at the top level and has type Addr#,
-- that it is a string literal, see
-- Note [Core top-level string literals].
- ; checkL (not (isTopLevel top_lvl_flag && binder_ty `eqType` addrPrimTy)
+ ; checkL (not (isTopLevel top_lvl && binder_ty `eqType` addrPrimTy)
|| exprIsTickedString rhs)
(mkTopNonLitStrMsg binder)
@@ -674,7 +674,9 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
-- join point.
--
-- See Note [Checking StaticPtrs].
-lintRhs :: Id -> CoreExpr -> LintM OutType
+lintRhs :: Id -> CoreExpr -> LintM LintedType
+-- NB: the Id can be Linted or not -- it's only used for
+-- its OccInfo and join-pointer-hood
lintRhs bndr rhs
| Just arity <- isJoinId_maybe bndr
= lint_join_lams arity arity True rhs
@@ -761,13 +763,14 @@ hurts us here.
************************************************************************
-}
--- For OutType, OutKind, the substitution has been applied,
--- but has not been linted yet
+-- Linted things: substitution applied, and type is linted
+type LintedType = Type
+type LintedKind = Kind
+type LintedCoercion = Coercion
+type LintedTyCoVar = TyCoVar
+type LintedId = Id
-type LintedType = Type -- Substitution applied, and type is linted
-type LintedKind = Kind
-
-lintCoreExpr :: CoreExpr -> LintM OutType
+lintCoreExpr :: CoreExpr -> LintM LintedType
-- The returned type has the substitution from the monad
-- already applied to it:
-- lintCoreExpr e subst = exprType (subst e)
@@ -776,6 +779,7 @@ lintCoreExpr :: CoreExpr -> LintM OutType
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
+
lintCoreExpr (Var var)
= lintVarOcc var 0
@@ -784,10 +788,11 @@ lintCoreExpr (Lit lit)
lintCoreExpr (Cast expr co)
= do { expr_ty <- markAllJoinsBad $ lintCoreExpr expr
- ; co' <- applySubstCo co
- ; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
- ; checkValueKind k2 (text "target of cast" <+> quotes (ppr co))
- ; lintRole co' Representational r
+ ; co' <- lintCoercion co
+ ; let (Pair from_ty to_ty, role) = coercionKindRole co'
+ ; checkValueType to_ty $
+ text "target of cast" <+> quotes (ppr co')
+ ; lintRole co' Representational role
; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
; return to_ty }
@@ -809,7 +814,7 @@ lintCoreExpr (Tick tickish expr)
lintCoreExpr (Let (NonRec tv (Type ty)) body)
| isTyVar tv
= -- See Note [Linting type lets]
- do { ty' <- applySubstTy ty
+ do { ty' <- lintType ty
; lintTyBndr tv $ \ tv' ->
do { addLoc (RhsOf tv) $ lintTyKind tv' ty'
-- Now extend the substitution so we
@@ -820,33 +825,34 @@ lintCoreExpr (Let (NonRec tv (Type ty)) body)
lintCoreExpr (Let (NonRec bndr rhs) body)
| isId bndr
- = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
- ; addLoc (BodyOfLetRec [bndr])
- (lintBinder LetBind bndr $ \_ ->
- addGoodJoins [bndr] $
- lintCoreExpr body) }
+ = do { -- First Lint the RHS, before bringing the binder into scope
+ rhs_ty <- lintRhs bndr rhs
+
+ -- Now lint the binder
+ ; lintBinder LetBind bndr $ \bndr' ->
+ do { lintLetBind NotTopLevel NonRecursive bndr' rhs rhs_ty
+ ; addLoc (BodyOfLetRec [bndr]) (lintCoreExpr body) } }
| otherwise
= failWithL (mkLetErr bndr rhs) -- Not quite accurate
lintCoreExpr e@(Let (Rec pairs) body)
- = lintLetBndrs NotTopLevel bndrs $
- addGoodJoins bndrs $
- do { -- Check that the list of pairs is non-empty
+ = do { -- Check that the list of pairs is non-empty
checkL (not (null pairs)) (emptyRec e)
-- Check that there are no duplicated binders
+ ; let (_, dups) = removeDups compare bndrs
; checkL (null dups) (dupVars dups)
-- Check that either all the binders are joins, or none
; checkL (all isJoinId bndrs || all (not . isJoinId) bndrs) $
- mkInconsistentRecMsg bndrs
+ mkInconsistentRecMsg bndrs
- ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
- ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
+ ; lintRecBindings NotTopLevel pairs $
+ addLoc (BodyOfLetRec bndrs) $
+ lintCoreExpr body }
where
bndrs = map fst pairs
- (_, dups) = removeDups compare bndrs
lintCoreExpr e@(App _ _)
= do { fun_ty <- lintCoreFun fun (length args)
@@ -867,20 +873,27 @@ lintCoreExpr (Type ty)
= failWithL (text "Type found as expression" <+> ppr ty)
lintCoreExpr (Coercion co)
- = do { (k1, k2, ty1, ty2, role) <- lintInCo co
- ; return (mkHeteroCoercionType role k1 k2 ty1 ty2) }
+ = do { co' <- addLoc (InCo co) $
+ lintCoercion co
+ ; return (coercionType co') }
----------------------
lintVarOcc :: Var -> Int -- Number of arguments (type or value) being passed
- -> LintM Type -- returns type of the *variable*
+ -> LintM LintedType -- returns type of the *variable*
lintVarOcc var nargs
- = do { checkL (isNonCoVarId var)
+ = addLoc (OccOf var) $
+ do { checkL (isNonCoVarId var)
(text "Non term variable" <+> ppr var)
-- See GHC.Core Note [Variable occurrences in Core]
-- Check that the type of the occurrence is the same
- -- as the type of the binding site
- ; ty <- applySubstTy (idType var)
+ -- as the type of the binding site. We lint the type so that
+ -- we apply the substitution. Actually this will get into trouble
+ -- with /\a. \(x::Maybe a). /\a. ...(x::Maybe a)...
+ -- The "::Maybe a" on the occurrence is referring to the /outer/ a.
+ -- But this naive check will treat it like the inner one.
+ -- This looks like a bug waiting to happen.
+ ; ty <- lintType (idType var)
; var' <- lookupIdInScope var
; let ty' = idType var'
; ensureEqTys ty ty' $ mkBndrOccTypeMismatchMsg var' var ty' ty
@@ -898,8 +911,8 @@ lintVarOcc var nargs
; return (idType var') }
lintCoreFun :: CoreExpr
- -> Int -- Number of arguments (type or val) being passed
- -> LintM Type -- Returns type of the *function*
+ -> Int -- Number of arguments (type or val) being passed
+ -> LintM LintedType -- Returns type of the *function*
lintCoreFun (Var var) nargs
= lintVarOcc var nargs
@@ -941,7 +954,9 @@ checkJoinOcc var n_args
= do { mb_join_arity_bndr <- lookupJoinId var
; case mb_join_arity_bndr of {
Nothing -> -- Binder is not a join point
- addErrL (invalidJoinOcc var) ;
+ do { join_set <- getValidJoins
+ ; addErrL (text "join set " <+> ppr join_set $$
+ invalidJoinOcc var) } ;
Just join_arity_bndr ->
@@ -1038,15 +1053,15 @@ subtype of the required type, as one would expect.
-}
-lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
+lintCoreArgs :: LintedType -> [CoreArg] -> LintM LintedType
lintCoreArgs fun_ty args = foldM lintCoreArg fun_ty args
-lintCoreArg :: OutType -> CoreArg -> LintM OutType
+lintCoreArg :: LintedType -> CoreArg -> LintM LintedType
lintCoreArg fun_ty (Type arg_ty)
= do { checkL (not (isCoercionTy arg_ty))
(text "Unnecessary coercion-to-type injection:"
<+> ppr arg_ty)
- ; arg_ty' <- applySubstTy arg_ty
+ ; arg_ty' <- lintType arg_ty
; lintTyApp fun_ty arg_ty' }
lintCoreArg fun_ty arg
@@ -1060,11 +1075,12 @@ lintCoreArg fun_ty arg
; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
(mkLetAppMsg arg)
+
; lintValApp arg fun_ty arg_ty }
-----------------
-lintAltBinders :: OutType -- Scrutinee type
- -> OutType -- Constructor type
+lintAltBinders :: LintedType -- Scrutinee type
+ -> LintedType -- Constructor type
-> [OutVar] -- Binders
-> LintM ()
-- If you edit this function, you may need to update the GHC formalism
@@ -1080,7 +1096,7 @@ lintAltBinders scrut_ty con_ty (bndr:bndrs)
; lintAltBinders scrut_ty con_ty' bndrs }
-----------------
-lintTyApp :: OutType -> OutType -> LintM OutType
+lintTyApp :: LintedType -> LintedType -> LintM LintedType
lintTyApp fun_ty arg_ty
| Just (tv,body_ty) <- splitForAllTy_maybe fun_ty
= do { lintTyKind tv arg_ty
@@ -1094,7 +1110,7 @@ lintTyApp fun_ty arg_ty
= failWithL (mkTyAppMsg fun_ty arg_ty)
-----------------
-lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
+lintValApp :: CoreExpr -> LintedType -> LintedType -> LintM LintedType
lintValApp arg fun_ty arg_ty
| Just (arg,res) <- splitFunTy_maybe fun_ty
= do { ensureEqTys arg arg_ty err1
@@ -1105,17 +1121,17 @@ lintValApp arg fun_ty arg_ty
err1 = mkAppMsg fun_ty arg_ty arg
err2 = mkNonFunAppMsg fun_ty arg_ty arg
-lintTyKind :: OutTyVar -> OutType -> LintM ()
+lintTyKind :: OutTyVar -> LintedType -> LintM ()
-- Both args have had substitution applied
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintTyKind tyvar arg_ty
- = do { arg_kind <- lintType arg_ty
- ; unless (arg_kind `eqType` tyvar_kind)
- (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "Linted Arg kind:" <+> ppr arg_kind))) }
+ = unless (arg_kind `eqType` tyvar_kind) $
+ addErrL (mkKindErrMsg tyvar arg_ty $$ (text "Linted Arg kind:" <+> ppr arg_kind))
where
tyvar_kind = tyVarKind tyvar
+ arg_kind = typeKind arg_ty
{-
************************************************************************
@@ -1125,7 +1141,7 @@ lintTyKind tyvar arg_ty
************************************************************************
-}
-lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM OutType
+lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM LintedType
lintCaseExpr scrut var alt_ty alts =
do { let e = Case scrut var alt_ty alts -- Just for error messages
@@ -1134,10 +1150,10 @@ lintCaseExpr scrut var alt_ty alts =
-- See Note [Join points are less general than the paper]
-- in GHC.Core
- ; (alt_ty, _) <- addLoc (CaseTy scrut) $
- lintInTy alt_ty
- ; (var_ty, _) <- addLoc (IdTy var) $
- lintInTy (idType var)
+ ; alt_ty <- addLoc (CaseTy scrut) $
+ lintValueType alt_ty
+ ; var_ty <- addLoc (IdTy var) $
+ lintValueType (idType var)
-- We used to try to check whether a case expression with no
-- alternatives was legitimate, but this didn't work.
@@ -1179,7 +1195,7 @@ lintCaseExpr scrut var alt_ty alts =
; checkCaseAlts e scrut_ty alts
; return alt_ty } }
-checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
+checkCaseAlts :: CoreExpr -> LintedType -> [CoreAlt] -> LintM ()
-- a) Check that the alts are non-empty
-- b1) Check that the DEFAULT comes first, if it exists
-- b2) Check that the others are in increasing order
@@ -1219,14 +1235,14 @@ checkCaseAlts e ty alts =
Nothing -> False
Just tycon -> isPrimTyCon tycon
-lintAltExpr :: CoreExpr -> OutType -> LintM ()
+lintAltExpr :: CoreExpr -> LintedType -> LintM ()
lintAltExpr expr ann_ty
= do { actual_ty <- lintCoreExpr expr
; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
-- See GHC.Core Note [Case expression invariants] item (6)
-lintCoreAlt :: OutType -- Type of scrutinee
- -> OutType -- Type of the alternative
+lintCoreAlt :: LintedType -- Type of scrutinee
+ -> LintedType -- Type of the alternative
-> CoreAlt
-> LintM ()
-- If you edit this function, you may need to update the GHC formalism
@@ -1286,33 +1302,36 @@ lintBinders site (var:vars) linterF = lintBinder site var $ \var' ->
-- See Note [GHC Formalism]
lintBinder :: BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder site var linterF
- | isTyVar var = lintTyBndr var linterF
- | isCoVar var = lintCoBndr var linterF
- | otherwise = lintIdBndr NotTopLevel site var linterF
+ | isTyCoVar var = lintTyCoBndr var linterF
+ | otherwise = lintIdBndr NotTopLevel site var linterF
-lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
-lintTyBndr tv thing_inside
- = do { subst <- getTCvSubst
- ; let (subst', tv') = substTyVarBndr subst tv
- ; lintKind (varType tv')
- ; updateTCvSubst subst' (thing_inside tv') }
+lintTyBndr :: TyVar -> (LintedTyCoVar -> LintM a) -> LintM a
+lintTyBndr = lintTyCoBndr -- We could specialise it, I guess
-lintCoBndr :: InCoVar -> (OutCoVar -> LintM a) -> LintM a
-lintCoBndr cv thing_inside
+-- lintCoBndr :: CoVar -> (LintedTyCoVar -> LintM a) -> LintM a
+-- lintCoBndr = lintTyCoBndr -- We could specialise it, I guess
+
+lintTyCoBndr :: TyCoVar -> (LintedTyCoVar -> LintM a) -> LintM a
+lintTyCoBndr tcv thing_inside
= do { subst <- getTCvSubst
- ; let (subst', cv') = substCoVarBndr subst cv
- ; lintKind (varType cv')
- ; lintL (isCoVarType (varType cv'))
- (text "CoVar with non-coercion type:" <+> pprTyVar cv)
- ; updateTCvSubst subst' (thing_inside cv') }
-
-lintLetBndrs :: TopLevelFlag -> [Var] -> LintM a -> LintM a
-lintLetBndrs top_lvl ids linterF
- = go ids
+ ; kind' <- lintType (varType tcv)
+ ; let tcv' = uniqAway (getTCvInScope subst) $
+ setVarType tcv kind'
+ subst' = extendTCvSubstWithClone subst tcv tcv'
+ ; when (isCoVar tcv) $
+ lintL (isCoVarType kind')
+ (text "CoVar with non-coercion type:" <+> pprTyVar tcv)
+ ; updateTCvSubst subst' (thing_inside tcv') }
+
+lintIdBndrs :: forall a. TopLevelFlag -> [Id] -> ([LintedId] -> LintM a) -> LintM a
+lintIdBndrs top_lvl ids thing_inside
+ = go ids thing_inside
where
- go [] = linterF
- go (id:ids) = lintIdBndr top_lvl LetBind id $ \_ ->
- go ids
+ go :: [Id] -> ([Id] -> LintM a) -> LintM a
+ go [] thing_inside = thing_inside []
+ go (id:ids) thing_inside = lintIdBndr top_lvl LetBind id $ \id' ->
+ go ids $ \ids' ->
+ thing_inside (id' : ids')
lintIdBndr :: TopLevelFlag -> BindingSite
-> InVar -> (OutVar -> LintM a) -> LintM a
@@ -1334,14 +1353,15 @@ lintIdBndr top_lvl bind_site id linterF
; checkL (not (isExternalName (Var.varName id)) || is_top_lvl)
(mkNonTopExternalNameMsg id)
- ; (id_ty, k) <- addLoc (IdTy id) $
- lintInTy (idType id)
+ ; id_ty <- addLoc (IdTy id) $
+ lintValueType (idType id)
; let id' = setIdType id id_ty
-- See Note [Levity polymorphism invariants] in GHC.Core
- ; lintL (isJoinId id || not (lf_check_levity_poly flags) || not (isKindLevPoly k))
- (text "Levity-polymorphic binder:" <+>
- (ppr id <+> dcolon <+> parens (ppr id_ty <+> dcolon <+> ppr k)))
+ ; lintL (isJoinId id || not (lf_check_levity_poly flags)
+ || not (isTypeLevPoly id_ty)) $
+ text "Levity-polymorphic binder:" <+> ppr id <+> dcolon <+>
+ parens (ppr id_ty <+> dcolon <+> ppr (typeKind id_ty))
-- Check that a join-id is a not-top-level let-binding
; when (isJoinId id) $
@@ -1378,45 +1398,52 @@ lintTypes dflags vars tys
where
(_warns, errs) = initL dflags defaultLintFlags vars linter
linter = lintBinders LambdaBind vars $ \_ ->
- mapM_ lintInTy tys
+ mapM_ lintType tys
-lintInTy :: InType -> LintM (LintedType, LintedKind)
+lintValueType :: Type -> LintM LintedType
-- Types only, not kinds
-- Check the type, and apply the substitution to it
-- See Note [Linting type lets]
-lintInTy ty
+lintValueType ty
= addLoc (InType ty) $
- do { ty' <- applySubstTy ty
- ; k <- lintType ty'
- ; addLoc (InKind ty' k) $
- lintKind k -- The kind returned by lintType is already
- -- a LintedKind but we also want to check that
- -- k :: *, which lintKind does
- ; return (ty', k) }
+ do { ty' <- lintType ty
+ ; let sk = typeKind ty'
+ ; lintL (classifiesTypeWithValues sk) $
+ hang (text "Ill-kinded type:" <+> ppr ty)
+ 2 (text "has kind:" <+> ppr sk)
+ ; return ty' }
checkTyCon :: TyCon -> LintM ()
checkTyCon tc
= checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
-------------------
-lintType :: OutType -> LintM LintedKind
--- The returned Kind has itself been linted
+lintType :: LintedType -> LintM LintedType
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintType (TyVarTy tv)
- = do { checkL (isTyVar tv) (mkBadTyVarMsg tv)
- ; tv' <- lintTyCoVarInScope tv
- ; return (tyVarKind tv') }
- -- We checked its kind when we added it to the envt
+ | not (isTyVar tv)
+ = failWithL (mkBadTyVarMsg tv)
+
+ | otherwise
+ = do { subst <- getTCvSubst
+ ; case lookupTyVar subst tv of
+ Just linted_ty -> return linted_ty ;
+ Nothing -> -- lintTyBndr always extends the substitition
+ failWithL $
+ hang (text "The type variable" <+> pprBndr LetBind tv)
+ 2 (text "is out of scope")
+ }
lintType ty@(AppTy t1 t2)
| TyConApp {} <- t1
= failWithL $ text "TyConApp to the left of AppTy:" <+> ppr ty
| otherwise
- = do { k1 <- lintType t1
- ; k2 <- lintType t2
- ; lint_ty_app ty k1 [(t2,k2)] }
+ = do { t1' <- lintType t1
+ ; t2' <- lintType t2
+ ; lint_ty_app ty (typeKind t1') [t2']
+ ; return (AppTy t1' t2') }
lintType ty@(TyConApp tc tys)
| isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
@@ -1433,71 +1460,73 @@ lintType ty@(TyConApp tc tys)
| otherwise -- Data types, data families, primitive types
= do { checkTyCon tc
- ; ks <- mapM lintType tys
- ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
+ ; tys' <- mapM lintType tys
+ ; lint_ty_app ty (tyConKind tc) tys'
+ ; return (TyConApp tc tys') }
-- arrows can related *unlifted* kinds, so this has to be separate from
-- a dependent forall.
-lintType ty@(FunTy _ t1 t2)
- = do { k1 <- lintType t1
- ; k2 <- lintType t2
- ; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 }
+lintType ty@(FunTy af t1 t2)
+ = do { t1' <- lintType t1
+ ; t2' <- lintType t2
+ ; lintArrow (text "type or kind" <+> quotes (ppr ty)) t1' t2'
+ ; return (FunTy af t1' t2') }
-lintType t@(ForAllTy (Bndr tv _vis) ty)
- -- forall over types
- | isTyVar tv
- = lintTyBndr tv $ \tv' ->
- do { k <- lintType ty
- ; checkValueKind k (text "the body of forall:" <+> ppr t)
- ; case occCheckExpand [tv'] k of -- See Note [Stupid type synonyms]
- Just k' -> return k'
- Nothing -> failWithL (hang (text "Variable escape in forall:")
- 2 (vcat [ text "type:" <+> ppr t
- , text "kind:" <+> ppr k ]))
- }
+lintType (ForAllTy (Bndr tcv vis) body_ty)
+ = lintTyCoBndr tcv $ \tcv' ->
+ do { body_ty' <- lintType body_ty
+ ; lintForAllBody tcv' body_ty'
+ ; return (ForAllTy (Bndr tcv' vis) body_ty') }
-lintType t@(ForAllTy (Bndr cv _vis) ty)
- -- forall over coercions
- = do { lintL (isCoVar cv)
- (text "Non-Tyvar or Non-Covar bound in type:" <+> ppr t)
- ; lintL (cv `elemVarSet` tyCoVarsOfType ty)
- (text "Covar does not occur in the body:" <+> ppr t)
- ; lintCoBndr cv $ \_ ->
- do { k <- lintType ty
- ; checkValueKind k (text "the body of forall:" <+> ppr t)
- ; return liftedTypeKind
- -- We don't check variable escape here. Namely, k could refer to cv'
- }}
-
-lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
+lintType ty@(LitTy l)
+ = do { lintTyLit l; return ty }
lintType (CastTy ty co)
- = do { k1 <- lintType ty
- ; (k1', k2) <- lintStarCoercion co
- ; ensureEqTys k1 k1' (mkCastTyErr ty co k1' k1)
- ; return k2 }
+ = do { ty' <- lintType ty
+ ; co' <- lintStarCoercion co
+ ; let tyk = typeKind ty'
+ cok = coercionLKind co'
+ ; ensureEqTys tyk cok (mkCastTyErr ty co tyk cok)
+ ; return (CastTy ty' co') }
lintType (CoercionTy co)
- = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
- ; return $ mkHeteroCoercionType r k1 k2 ty1 ty2 }
-
-{- Note [Stupid type synonyms]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (#14939)
- type Alg cls ob = ob
- f :: forall (cls :: * -> Constraint) (b :: Alg cls *). b
-
-Here 'cls' appears free in b's kind, which would usually be illegal
-(because in (forall a. ty), ty's kind should not mention 'a'). But
-#in this case (Alg cls *) = *, so all is well. Currently we allow
-this, and make Lint expand synonyms where necessary to make it so.
-
-c.f. TcUnify.occCheckExpand and GHC.Core.Utils.coreAltsType which deal
-with the same problem. A single systematic solution eludes me.
--}
+ = do { co' <- lintCoercion co
+ ; return (CoercionTy co') }
-----------------
-lintTySynFamApp :: Bool -> Type -> TyCon -> [Type] -> LintM LintedKind
+lintForAllBody :: LintedTyCoVar -> LintedType -> LintM ()
+-- Do the checks for the body of a forall-type
+lintForAllBody tcv body_ty
+ | isTyVar tcv
+ = do { checkValueType body_ty (text "the body of forall:" <+> ppr body_ty)
+
+ -- Check for skolem escape
+ -- See Note [Phantom type variables in kinds] in GHC.Core.Type
+ ; let body_kind = typeKind body_ty
+ ; case occCheckExpand [tcv] body_kind of
+ Just {} -> return ()
+ Nothing -> failWithL $
+ hang (text "Variable escape in forall:")
+ 2 (vcat [ text "tyvar:" <+> ppr tcv
+ , text "type:" <+> ppr body_ty
+ , text "kind:" <+> ppr body_kind ])
+ }
+
+ | isCoVar tcv
+ = do { checkValueType body_ty (text "the body of forall:" <+> ppr body_ty)
+
+ ; lintL (tcv `elemVarSet` tyCoVarsOfType body_ty) $
+ text "Covar does not occur in the body:" <+> (ppr tcv $$ ppr body_ty)
+
+ -- The kind of (forall cv. th) is liftedTypeKind, so no
+ -- need to check for skolem-escape, as we must do in the tyvar case
+ }
+
+ | otherwise
+ = failWithL (text "Non-Tyvar or Non-Covar bound in type:" <+> ppr tcv)
+
+-----------------
+lintTySynFamApp :: Bool -> InType -> TyCon -> [InType] -> LintM LintedType
-- The TyCon is a type synonym or a type family (not a data family)
-- See Note [Linting type synonym applications]
-- c.f. TcValidity.check_syn_tc_app
@@ -1511,58 +1540,54 @@ lintTySynFamApp report_unsat ty tc tys
, let expanded_ty = mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys'
= do { -- Kind-check the argument types, but without reporting
-- un-saturated type families/synonyms
- ks <- setReportUnsat False (mapM lintType tys)
+ tys' <- setReportUnsat False (mapM lintType tys)
; when report_unsat $
do { _ <- lintType expanded_ty
; return () }
- ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
+ ; lint_ty_app ty (tyConKind tc) tys'
+ ; return (TyConApp tc tys') }
-- Otherwise this must be a type family
| otherwise
- = do { ks <- mapM lintType tys
- ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
-
------------------
-lintKind :: OutKind -> LintM ()
--- If you edit this function, you may need to update the GHC formalism
--- See Note [GHC Formalism]
-lintKind k = do { sk <- lintType k
- ; unless (classifiesTypeWithValues sk)
- (addErrL (hang (text "Ill-kinded kind:" <+> ppr k)
- 2 (text "has kind:" <+> ppr sk))) }
+ = do { tys' <- mapM lintType tys
+ ; lint_ty_app ty (tyConKind tc) tys'
+ ; return (TyConApp tc tys') }
-----------------
-- Confirms that a type is really *, #, Constraint etc
-checkValueKind :: OutKind -> SDoc -> LintM ()
-checkValueKind k doc
- = lintL (classifiesTypeWithValues k)
- (text "Non-*-like kind when *-like expected:" <+> ppr k $$
+checkValueType :: LintedType -> SDoc -> LintM ()
+checkValueType ty doc
+ = lintL (classifiesTypeWithValues kind)
+ (text "Non-*-like kind when *-like expected:" <+> ppr kind $$
text "when checking" <+> doc)
+ where
+ kind = typeKind ty
-----------------
-lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
+lintArrow :: SDoc -> LintedType -> LintedType -> LintM ()
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
-lintArrow what k1 k2 -- Eg lintArrow "type or kind `blah'" k1 k2
+lintArrow what t1 t2 -- Eg lintArrow "type or kind `blah'" k1 k2
-- or lintArrow "coercion `blah'" k1 k2
= do { unless (classifiesTypeWithValues k1) (addErrL (msg (text "argument") k1))
- ; unless (classifiesTypeWithValues k2) (addErrL (msg (text "result") k2))
- ; return liftedTypeKind }
+ ; unless (classifiesTypeWithValues k2) (addErrL (msg (text "result") k2)) }
where
+ k1 = typeKind t1
+ k2 = typeKind t2
msg ar k
= vcat [ hang (text "Ill-kinded" <+> ar)
2 (text "in" <+> what)
, what <+> text "kind:" <+> ppr k ]
-----------------
-lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
+lint_ty_app :: Type -> LintedKind -> [LintedType] -> LintM ()
lint_ty_app ty k tys
= lint_app (text "type" <+> quotes (ppr ty)) k tys
----------------
-lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
+lint_co_app :: Coercion -> LintedKind -> [LintedType] -> LintM ()
lint_co_app ty k tys
= lint_app (text "coercion" <+> quotes (ppr ty)) k tys
@@ -1574,42 +1599,45 @@ lintTyLit (NumTyLit n)
where msg = text "Negative type literal:" <+> integer n
lintTyLit (StrTyLit _) = return ()
-lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
+lint_app :: SDoc -> LintedKind -> [LintedType] -> LintM ()
-- (lint_app d fun_kind arg_tys)
-- We have an application (f arg_ty1 .. arg_tyn),
-- where f :: fun_kind
--- Takes care of linting the OutTypes
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
-lint_app doc kfn kas
+lint_app doc kfn arg_tys
= do { in_scope <- getInScope
-- We need the in_scope set to satisfy the invariant in
-- Note [The substitution invariant] in GHC.Core.TyCo.Subst
- ; foldlM (go_app in_scope) kfn kas }
+ ; _ <- foldlM (go_app in_scope) kfn arg_tys
+ ; return () }
where
fail_msg extra = vcat [ hang (text "Kind application error in") 2 doc
, nest 2 (text "Function kind =" <+> ppr kfn)
- , nest 2 (text "Arg kinds =" <+> ppr kas)
+ , nest 2 (text "Arg types =" <+> ppr arg_tys)
, extra ]
- go_app in_scope kfn tka
+ go_app in_scope kfn ta
| Just kfn' <- coreView kfn
- = go_app in_scope kfn' tka
+ = go_app in_scope kfn' ta
- go_app _ (FunTy _ kfa kfb) tka@(_,ka)
- = do { unless (ka `eqType` kfa) $
- addErrL (fail_msg (text "Fun:" <+> (ppr kfa $$ ppr tka)))
+ go_app _ fun_kind@(FunTy _ kfa kfb) ta
+ = do { let ka = typeKind ta
+ ; unless (ka `eqType` kfa) $
+ addErrL (fail_msg (text "Fun:" <+> (ppr fun_kind $$ ppr ta <+> dcolon <+> ppr ka)))
; return kfb }
- go_app in_scope (ForAllTy (Bndr kv _vis) kfn) tka@(ta,ka)
+ go_app in_scope (ForAllTy (Bndr kv _vis) kfn) ta
= do { let kv_kind = varType kv
+ ka = typeKind ta
; unless (ka `eqType` kv_kind) $
- addErrL (fail_msg (text "Forall:" <+> (ppr kv $$ ppr kv_kind $$ ppr tka)))
+ addErrL (fail_msg (text "Forall:" <+> (ppr kv $$ ppr kv_kind $$
+ ppr ta <+> dcolon <+> ppr ka)))
; return $ substTy (extendTCvSubst (mkEmptyTCvSubst in_scope) kv ta) kfn }
- go_app _ kfn ka
- = failWithL (fail_msg (text "Not a fun:" <+> (ppr kfn $$ ppr ka)))
+ go_app _ kfn ta
+ = failWithL (fail_msg (text "Not a fun:" <+> (ppr kfn $$ ppr ta)))
{- *********************************************************************
* *
@@ -1617,7 +1645,7 @@ lint_app doc kfn kas
* *
********************************************************************* -}
-lintCoreRule :: OutVar -> OutType -> CoreRule -> LintM ()
+lintCoreRule :: OutVar -> LintedType -> CoreRule -> LintM ()
lintCoreRule _ _ (BuiltinRule {})
= return () -- Don't bother
@@ -1710,68 +1738,94 @@ Note [Rules and join points] in OccurAnal for further discussion.
************************************************************************
-}
-lintInCo :: InCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
--- Check the coercion, and apply the substitution to it
--- See Note [Linting type lets]
-lintInCo co
- = addLoc (InCo co) $
- do { co' <- applySubstCo co
- ; lintCoercion co' }
+{- Note [Asymptotic efficiency]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When linting coercions (and types actually) we return a linted
+(substituted) coercion. Then we often have to take the coercionKind of
+that returned coercion. If we get long chains, that can be asymptotically
+inefficient, notably in
+* TransCo
+* InstCo
+* NthCo (cf #9233)
+* LRCo
+
+But the code is simple. And this is only Lint. Let's wait to see if
+the bad perf bites us in practice.
+
+A solution would be to return the kind and role of the coercion,
+as well as the linted coercion. Or perhaps even *only* the kind and role,
+which is what used to happen. But that proved tricky and error prone
+(#17923), so now we return the coercion.
+-}
+
-- lints a coercion, confirming that its lh kind and its rh kind are both *
-- also ensures that the role is Nominal
-lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType)
+lintStarCoercion :: InCoercion -> LintM LintedCoercion
lintStarCoercion g
- = do { (k1, k2, t1, t2, r) <- lintCoercion g
- ; checkValueKind k1 (text "the kind of the left type in" <+> ppr g)
- ; checkValueKind k2 (text "the kind of the right type in" <+> ppr g)
- ; lintRole g Nominal r
- ; return (t1, t2) }
-
-lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
--- Check the kind of a coercion term, returning the kind
--- Post-condition: the returned OutTypes are lint-free
---
--- If lintCoercion co = (k1, k2, s1, s2, r)
--- then co :: s1 ~r s2
--- s1 :: k1
--- s2 :: k2
-
+ = do { g' <- lintCoercion g
+ ; let Pair t1 t2 = coercionKind g'
+ ; checkValueType t1 (text "the kind of the left type in" <+> ppr g)
+ ; checkValueType t2 (text "the kind of the right type in" <+> ppr g)
+ ; lintRole g Nominal (coercionRole g)
+ ; return g' }
+
+lintCoercion :: InCoercion -> LintM LintedCoercion
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
+
+lintCoercion (CoVarCo cv)
+ | not (isCoVar cv)
+ = failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
+ 2 (text "With offending type:" <+> ppr (varType cv)))
+
+ | otherwise
+ = do { subst <- getTCvSubst
+ ; case lookupCoVar subst cv of
+ Just linted_co -> return linted_co ;
+ Nothing -> -- lintCoBndr always extends the substitition
+ failWithL $
+ hang (text "The coercion variable" <+> pprBndr LetBind cv)
+ 2 (text "is out of scope")
+ }
+
+
lintCoercion (Refl ty)
- = do { k <- lintType ty
- ; return (k, k, ty, ty, Nominal) }
+ = do { ty' <- lintType ty
+ ; return (Refl ty') }
lintCoercion (GRefl r ty MRefl)
- = do { k <- lintType ty
- ; return (k, k, ty, ty, r) }
+ = do { ty' <- lintType ty
+ ; return (GRefl r ty' MRefl) }
lintCoercion (GRefl r ty (MCo co))
- = do { k <- lintType ty
- ; (_, _, k1, k2, r') <- lintCoercion co
- ; ensureEqTys k k1
- (hang (text "GRefl coercion kind mis-match:" <+> ppr co)
- 2 (vcat [ppr ty, ppr k, ppr k1]))
- ; lintRole co Nominal r'
- ; return (k1, k2, ty, mkCastTy ty co, r) }
+ = do { ty' <- lintType ty
+ ; co' <- lintCoercion co
+ ; let tk = typeKind ty'
+ tl = coercionLKind co'
+ ; ensureEqTys tk tl $
+ hang (text "GRefl coercion kind mis-match:" <+> ppr co)
+ 2 (vcat [ppr ty', ppr tk, ppr tl])
+ ; lintRole co' Nominal (coercionRole co')
+ ; return (GRefl r ty' (MCo co')) }
lintCoercion co@(TyConAppCo r tc cos)
| tc `hasKey` funTyConKey
, [_rep1,_rep2,_co1,_co2] <- cos
- = do { failWithL (text "Saturated TyConAppCo (->):" <+> ppr co)
- } -- All saturated TyConAppCos should be FunCos
+ = failWithL (text "Saturated TyConAppCo (->):" <+> ppr co)
+ -- All saturated TyConAppCos should be FunCos
| Just {} <- synTyConDefn_maybe tc
= failWithL (text "Synonym in TyConAppCo:" <+> ppr co)
| otherwise
= do { checkTyCon tc
- ; (k's, ks, ss, ts, rs) <- mapAndUnzip5M lintCoercion cos
- ; k' <- lint_co_app co (tyConKind tc) (ss `zip` k's)
- ; k <- lint_co_app co (tyConKind tc) (ts `zip` ks)
- ; _ <- zipWith3M lintRole cos (tyConRolesX r tc) rs
- ; return (k', k, mkTyConApp tc ss, mkTyConApp tc ts, r) }
+ ; cos' <- mapM lintCoercion cos
+ ; let (co_kinds, co_roles) = unzip (map coercionKindRole cos')
+ ; lint_co_app co (tyConKind tc) (map pFst co_kinds)
+ ; lint_co_app co (tyConKind tc) (map pSnd co_kinds)
+ ; zipWithM_ (lintRole co) (tyConRolesX r tc) co_roles
+ ; return (TyConAppCo r tc cos') }
lintCoercion co@(AppCo co1 co2)
| TyConAppCo {} <- co1
@@ -1779,111 +1833,66 @@ lintCoercion co@(AppCo co1 co2)
| Just (TyConApp {}, _) <- isReflCo_maybe co1
= failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co)
| otherwise
- = do { (k1, k2, s1, s2, r1) <- lintCoercion co1
- ; (k'1, k'2, t1, t2, r2) <- lintCoercion co2
- ; k3 <- lint_co_app co k1 [(t1,k'1)]
- ; k4 <- lint_co_app co k2 [(t2,k'2)]
+ = do { co1' <- lintCoercion co1
+ ; co2' <- lintCoercion co2
+ ; let (Pair lk1 rk1, r1) = coercionKindRole co1'
+ (Pair lk2 rk2, r2) = coercionKindRole co2'
+ ; lint_co_app co (typeKind lk1) [lk2]
+ ; lint_co_app co (typeKind rk1) [rk2]
+
; if r1 == Phantom
then lintL (r2 == Phantom || r2 == Nominal)
(text "Second argument in AppCo cannot be R:" $$
ppr co)
else lintRole co Nominal r2
- ; return (k3, k4, mkAppTy s1 t1, mkAppTy s2 t2, r1) }
+
+ ; return (AppCo co1' co2') }
----------
-lintCoercion (ForAllCo tv1 kind_co co)
- -- forall over types
- | isTyVar tv1
- = do { (_, k2) <- lintStarCoercion kind_co
- ; let tv2 = setTyVarKind tv1 k2
- ; addInScopeTyCoVar tv1 $
- do {
- ; (k3, k4, t1, t2, r) <- lintCoercion co
- ; in_scope <- getInScope
- ; let tyl = mkInvForAllTy tv1 t1
- subst = mkTvSubst in_scope $
- -- We need both the free vars of the `t2` and the
- -- free vars of the range of the substitution in
- -- scope. All the free vars of `t2` and `kind_co` should
- -- already be in `in_scope`, because they've been
- -- linted and `tv2` has the same unique as `tv1`.
- -- See Note [The substitution invariant] in GHC.Core.TyCo.Subst.
- unitVarEnv tv1 (TyVarTy tv2 `mkCastTy` mkSymCo kind_co)
- tyr = mkInvForAllTy tv2 $
- substTy subst t2
- ; return (k3, k4, tyl, tyr, r) } }
-
-lintCoercion (ForAllCo cv1 kind_co co)
- -- forall over coercions
- = ASSERT( isCoVar cv1 )
- do { lintL (almostDevoidCoVarOfCo cv1 co)
+lintCoercion co@(ForAllCo tcv1 kind_co body_co)
+ | not (isTyCoVar tcv1)
+ = failWithL (text "Non tyco binder in ForAllCo:" <+> ppr co)
+ | otherwise
+ = do { kind_co' <- lintStarCoercion kind_co
+ ; lintTyCoBndr tcv1 $ \tcv1' ->
+ do { body_co' <- lintCoercion body_co
+ ; ensureEqTys (varType tcv1') (coercionLKind kind_co') $
+ text "Kind mis-match in ForallCo" <+> ppr co
+
+ ; lintForAllBody tcv1' (coercionLKind body_co')
+
+ ; when (isCoVar tcv1) $
+ lintL (almostDevoidCoVarOfCo tcv1 body_co)
(text "Covar can only appear in Refl and GRefl: " <+> ppr co)
- ; (_, k2) <- lintStarCoercion kind_co
- ; let cv2 = setVarType cv1 k2
- ; addInScopeTyCoVar cv1 $
- do {
- ; (k3, k4, t1, t2, r) <- lintCoercion co
- ; checkValueKind k3 (text "the body of a ForAllCo over covar:" <+> ppr co)
- ; checkValueKind k4 (text "the body of a ForAllCo over covar:" <+> ppr co)
- -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
- ; in_scope <- getInScope
- ; let tyl = mkTyCoInvForAllTy cv1 t1
- r2 = coVarRole cv1
- kind_co' = downgradeRole r2 Nominal kind_co
- eta1 = mkNthCo r2 2 kind_co'
- eta2 = mkNthCo r2 3 kind_co'
- subst = mkCvSubst in_scope $
- -- We need both the free vars of the `t2` and the
- -- free vars of the range of the substitution in
- -- scope. All the free vars of `t2` and `kind_co` should
- -- already be in `in_scope`, because they've been
- -- linted and `cv2` has the same unique as `cv1`.
- -- See Note [The substitution invariant] in GHC.Core.TyCo.Subst.
- unitVarEnv cv1 (eta1 `mkTransCo` (mkCoVarCo cv2)
- `mkTransCo` (mkSymCo eta2))
- tyr = mkTyCoInvForAllTy cv2 $
- substTy subst t2
- ; return (liftedTypeKind, liftedTypeKind, tyl, tyr, r) } }
- -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
+ -- See "last wrinkle" in GHC.Core.Coercion
+ -- Note [Unused coercion variable in ForAllCo]
-lintCoercion co@(FunCo r co1 co2)
- = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
- ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
- ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2
- ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
- ; lintRole co1 r r1
- ; lintRole co2 r r2
- ; return (k, k', mkVisFunTy s1 s2, mkVisFunTy t1 t2, r) }
+ ; return (ForAllCo tcv1' kind_co' body_co') } }
-lintCoercion (CoVarCo cv)
- | not (isCoVar cv)
- = failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
- 2 (text "With offending type:" <+> ppr (varType cv)))
- | otherwise
- = do { cv' <- lintTyCoVarInScope cv
- ; lintUnliftedCoVar cv'
- ; return $ coVarKindsTypesRole cv' }
+lintCoercion co@(FunCo r co1 co2)
+ = do { co1' <- lintCoercion co1
+ ; co2' <- lintCoercion co2
+ ; let Pair lt1 rt1 = coercionKind co1
+ Pair lt2 rt2 = coercionKind co2
+ ; lintArrow (text "coercion" <+> quotes (ppr co)) lt1 lt2
+ ; lintArrow (text "coercion" <+> quotes (ppr co)) rt1 rt2
+ ; lintRole co1 r (coercionRole co1)
+ ; lintRole co2 r (coercionRole co2)
+ ; return (FunCo r co1' co2') }
-- See Note [Bad unsafe coercion]
lintCoercion co@(UnivCo prov r ty1 ty2)
- = do { k1 <- lintType ty1
- ; k2 <- lintType ty2
- ; case prov of
- PhantomProv kco -> do { lintRole co Phantom r
- ; check_kinds kco k1 k2 }
-
- ProofIrrelProv kco -> do { lintL (isCoercionTy ty1) $
- mkBadProofIrrelMsg ty1 co
- ; lintL (isCoercionTy ty2) $
- mkBadProofIrrelMsg ty2 co
- ; check_kinds kco k1 k2 }
-
- PluginProv _ -> return () -- no extra checks
+ = do { ty1' <- lintType ty1
+ ; ty2' <- lintType ty2
+ ; let k1 = typeKind ty1'
+ k2 = typeKind ty2'
+ ; prov' <- lint_prov k1 k2 prov
; when (r /= Phantom && classifiesTypeWithValues k1
&& classifiesTypeWithValues k2)
(checkTypes ty1 ty2)
- ; return (k1, k2, ty1, ty2, r) }
+
+ ; return (UnivCo prov' r ty1' ty2') }
where
report s = hang (text $ "Unsafe coercion: " ++ s)
2 (vcat [ text "From:" <+> ppr ty1
@@ -1926,39 +1935,53 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
_ -> return ()
}
- check_kinds kco k1 k2 = do { (k1', k2') <- lintStarCoercion kco
- ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft co)
- ; ensureEqTys k2 k2' (mkBadUnivCoMsg CRight co) }
+ lint_prov k1 k2 (PhantomProv kco)
+ = do { kco' <- lintStarCoercion kco
+ ; lintRole co Phantom r
+ ; check_kinds kco' k1 k2
+ ; return (PhantomProv kco') }
+
+ lint_prov k1 k2 (ProofIrrelProv kco)
+ = do { lintL (isCoercionTy ty1) (mkBadProofIrrelMsg ty1 co)
+ ; lintL (isCoercionTy ty2) (mkBadProofIrrelMsg ty2 co)
+ ; kco' <- lintStarCoercion kco
+ ; check_kinds kco k1 k2
+ ; return (ProofIrrelProv kco') }
+
+ lint_prov _ _ prov@(PluginProv _) = return prov
+
+ check_kinds kco k1 k2
+ = do { let Pair k1' k2' = coercionKind kco
+ ; ensureEqTys k1 k1' (mkBadUnivCoMsg CLeft co)
+ ; ensureEqTys k2 k2' (mkBadUnivCoMsg CRight co) }
lintCoercion (SymCo co)
- = do { (k1, k2, ty1, ty2, r) <- lintCoercion co
- ; return (k2, k1, ty2, ty1, r) }
+ = do { co' <- lintCoercion co
+ ; return (SymCo co') }
lintCoercion co@(TransCo co1 co2)
- = do { (k1a, _k1b, ty1a, ty1b, r1) <- lintCoercion co1
- ; (_k2a, k2b, ty2a, ty2b, r2) <- lintCoercion co2
+ = do { co1' <- lintCoercion co1
+ ; co2' <- lintCoercion co2
+ ; let ty1b = coercionRKind co1'
+ ty2a = coercionLKind co2'
; ensureEqTys ty1b ty2a
(hang (text "Trans coercion mis-match:" <+> ppr co)
- 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
- ; lintRole co r1 r2
- ; return (k1a, k2b, ty1a, ty2b, r1) }
+ 2 (vcat [ppr (coercionKind co1'), ppr (coercionKind co2')]))
+ ; lintRole co (coercionRole co1) (coercionRole co2)
+ ; return (TransCo co1' co2') }
lintCoercion the_co@(NthCo r0 n co)
- = do { (_, _, s, t, r) <- lintCoercion co
+ = do { co' <- lintCoercion co
+ ; let (Pair s t, r) = coercionKindRole co'
; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
- { (Just (tcv_s, _ty_s), Just (tcv_t, _ty_t))
+ { (Just _, Just _)
-- works for both tyvar and covar
| n == 0
, (isForAllTy_ty s && isForAllTy_ty t)
|| (isForAllTy_co s && isForAllTy_co t)
-> do { lintRole the_co Nominal r0
- ; return (ks, kt, ts, tt, r0) }
- where
- ts = varType tcv_s
- tt = varType tcv_t
- ks = typeKind ts
- kt = typeKind tt
+ ; return (NthCo r0 n co') }
; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
{ (Just (tc_s, tys_s), Just (tc_t, tys_t))
@@ -1968,62 +1991,51 @@ lintCoercion the_co@(NthCo r0 n co)
, tys_s `equalLength` tys_t
, tys_s `lengthExceeds` n
-> do { lintRole the_co tr r0
- ; return (ks, kt, ts, tt, r0) }
- where
- ts = getNth tys_s n
- tt = getNth tys_t n
- tr = nthRole r tc_s n
- ks = typeKind ts
- kt = typeKind tt
+ ; return (NthCo r0 n co') }
+ where
+ tr = nthRole r tc_s n
; _ -> failWithL (hang (text "Bad getNth:")
2 (ppr the_co $$ ppr s $$ ppr t)) }}}
lintCoercion the_co@(LRCo lr co)
- = do { (_,_,s,t,r) <- lintCoercion co
+ = do { co' <- lintCoercion co
+ ; let Pair s t = coercionKind co'
+ r = coercionRole co'
; lintRole co Nominal r
; case (splitAppTy_maybe s, splitAppTy_maybe t) of
- (Just s_pr, Just t_pr)
- -> return (ks_pick, kt_pick, s_pick, t_pick, Nominal)
- where
- s_pick = pickLR lr s_pr
- t_pick = pickLR lr t_pr
- ks_pick = typeKind s_pick
- kt_pick = typeKind t_pick
-
+ (Just _, Just _) -> return (LRCo lr co')
_ -> failWithL (hang (text "Bad LRCo:")
2 (ppr the_co $$ ppr s $$ ppr t)) }
lintCoercion (InstCo co arg)
- = do { (k3, k4, t1',t2', r) <- lintCoercion co
- ; (k1',k2',s1,s2, r') <- lintCoercion arg
- ; lintRole arg Nominal r'
- ; in_scope <- getInScope
- ; case (splitForAllTy_ty_maybe t1', splitForAllTy_ty_maybe t2') of
+ = do { co' <- lintCoercion co
+ ; arg' <- lintCoercion arg
+ ; let Pair t1' t2' = coercionKind co'
+ Pair s1 s2 = coercionKind arg
+
+ ; lintRole arg Nominal (coercionRole arg')
+
+ ; case (splitForAllTy_ty_maybe t1', splitForAllTy_ty_maybe t2') of
-- forall over tvar
- { (Just (tv1,t1), Just (tv2,t2))
- | k1' `eqType` tyVarKind tv1
- , k2' `eqType` tyVarKind tv2
- -> return (k3, k4,
- substTyWithInScope in_scope [tv1] [s1] t1,
- substTyWithInScope in_scope [tv2] [s2] t2, r)
+ { (Just (tv1,_), Just (tv2,_))
+ | typeKind s1 `eqType` tyVarKind tv1
+ , typeKind s2 `eqType` tyVarKind tv2
+ -> return (InstCo co' arg')
| otherwise
-> failWithL (text "Kind mis-match in inst coercion")
+
; _ -> case (splitForAllTy_co_maybe t1', splitForAllTy_co_maybe t2') of
-- forall over covar
- { (Just (cv1, t1), Just (cv2, t2))
- | k1' `eqType` varType cv1
- , k2' `eqType` varType cv2
- , CoercionTy s1' <- s1
- , CoercionTy s2' <- s2
- -> do { return $
- (liftedTypeKind, liftedTypeKind
- -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
- , substTy (mkCvSubst in_scope $ unitVarEnv cv1 s1') t1
- , substTy (mkCvSubst in_scope $ unitVarEnv cv2 s2') t2
- , r) }
+ { (Just (cv1, _), Just (cv2, _))
+ | typeKind s1 `eqType` varType cv1
+ , typeKind s2 `eqType` varType cv2
+ , CoercionTy _ <- s1
+ , CoercionTy _ <- s2
+ -> return (InstCo co' arg')
| otherwise
-> failWithL (text "Kind mis-match in inst coercion")
+
; _ -> failWithL (text "Bad argument of inst") }}}
lintCoercion co@(AxiomInstCo con ind cos)
@@ -2031,73 +2043,69 @@ lintCoercion co@(AxiomInstCo con ind cos)
(bad_ax (text "index out of range"))
; let CoAxBranch { cab_tvs = ktvs
, cab_cvs = cvs
- , cab_roles = roles
- , cab_lhs = lhs
- , cab_rhs = rhs } = coAxiomNthBranch con ind
+ , cab_roles = roles } = coAxiomNthBranch con ind
; unless (cos `equalLength` (ktvs ++ cvs)) $
bad_ax (text "lengths")
+ ; cos' <- mapM lintCoercion cos
; subst <- getTCvSubst
; let empty_subst = zapTCvSubst subst
- ; (subst_l, subst_r) <- foldlM check_ki
- (empty_subst, empty_subst)
- (zip3 (ktvs ++ cvs) roles cos)
- ; let lhs' = substTys subst_l lhs
- rhs' = substTy subst_r rhs
- fam_tc = coAxiomTyCon con
+ ; _ <- foldlM check_ki (empty_subst, empty_subst)
+ (zip3 (ktvs ++ cvs) roles cos')
+ ; let fam_tc = coAxiomTyCon con
; case checkAxInstCo co of
Just bad_branch -> bad_ax $ text "inconsistent with" <+>
pprCoAxBranch fam_tc bad_branch
Nothing -> return ()
- ; let s2 = mkTyConApp fam_tc lhs'
- ; return (typeKind s2, typeKind rhs', s2, rhs', coAxiomRole con) }
+ ; return (AxiomInstCo con ind cos') }
where
bad_ax what = addErrL (hang (text "Bad axiom application" <+> parens what)
2 (ppr co))
- check_ki (subst_l, subst_r) (ktv, role, arg)
- = do { (k', k'', s', t', r) <- lintCoercion arg
- ; lintRole arg role r
+ check_ki (subst_l, subst_r) (ktv, role, arg')
+ = do { let Pair s' t' = coercionKind arg'
+ sk' = typeKind s'
+ tk' = typeKind t'
+ ; lintRole arg' role (coercionRole arg')
; let ktv_kind_l = substTy subst_l (tyVarKind ktv)
ktv_kind_r = substTy subst_r (tyVarKind ktv)
- ; unless (k' `eqType` ktv_kind_l)
- (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr k', ppr ktv, ppr ktv_kind_l ] ))
- ; unless (k'' `eqType` ktv_kind_r)
- (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr k'', ppr ktv, ppr ktv_kind_r ] ))
+ ; unless (sk' `eqType` ktv_kind_l)
+ (bad_ax (text "check_ki1" <+> vcat [ ppr co, ppr sk', ppr ktv, ppr ktv_kind_l ] ))
+ ; unless (tk' `eqType` ktv_kind_r)
+ (bad_ax (text "check_ki2" <+> vcat [ ppr co, ppr tk', ppr ktv, ppr ktv_kind_r ] ))
; return (extendTCvSubst subst_l ktv s',
extendTCvSubst subst_r ktv t') }
lintCoercion (KindCo co)
- = do { (k1, k2, _, _, _) <- lintCoercion co
- ; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) }
+ = do { co' <- lintCoercion co
+ ; return (KindCo co') }
lintCoercion (SubCo co')
- = do { (k1,k2,s,t,r) <- lintCoercion co'
- ; lintRole co' Nominal r
- ; return (k1,k2,s,t,Representational) }
-
-lintCoercion this@(AxiomRuleCo co cs)
- = do { eqs <- mapM lintCoercion cs
- ; lintRoles 0 (coaxrAsmpRoles co) eqs
- ; case coaxrProves co [ Pair l r | (_,_,l,r,_) <- eqs ] of
+ = do { co' <- lintCoercion co'
+ ; lintRole co' Nominal (coercionRole co')
+ ; return (SubCo co') }
+
+lintCoercion this@(AxiomRuleCo ax cos)
+ = do { cos' <- mapM lintCoercion cos
+ ; lint_roles 0 (coaxrAsmpRoles ax) cos'
+ ; case coaxrProves ax (map coercionKind cos') of
Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
- Just (Pair l r) ->
- return (typeKind l, typeKind r, l, r, coaxrRole co) }
+ Just _ -> return (AxiomRuleCo ax cos') }
where
err m xs = failWithL $
- hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName co) : xs)
+ hang (text m) 2 $ vcat (text "Rule:" <+> ppr (coaxrName ax) : xs)
- lintRoles n (e : es) ((_,_,_,_,r) : rs)
- | e == r = lintRoles (n+1) es rs
+ lint_roles n (e : es) (co : cos)
+ | e == coercionRole co = lint_roles (n+1) es cos
| otherwise = err "Argument roles mismatch"
[ text "In argument:" <+> int (n+1)
, text "Expected:" <+> ppr e
- , text "Found:" <+> ppr r ]
- lintRoles _ [] [] = return ()
- lintRoles n [] rs = err "Too many coercion arguments"
+ , text "Found:" <+> ppr (coercionRole co) ]
+ lint_roles _ [] [] = return ()
+ lint_roles n [] rs = err "Too many coercion arguments"
[ text "Expected:" <+> int n
, text "Provided:" <+> int (n + length rs) ]
- lintRoles n es [] = err "Not enough coercion arguments"
+ lint_roles n es [] = err "Not enough coercion arguments"
[ text "Expected:" <+> int (n + length es)
, text "Provided:" <+> int n ]
@@ -2106,13 +2114,6 @@ lintCoercion (HoleCo h)
; lintCoercion (CoVarCo (coHoleCoVar h)) }
-----------
-lintUnliftedCoVar :: CoVar -> LintM ()
-lintUnliftedCoVar cv
- = when (not (isUnliftedType (coVarKind cv))) $
- failWithL (text "Bad lifted equality:" <+> ppr cv
- <+> dcolon <+> ppr (coVarKind cv))
-
{-
************************************************************************
* *
@@ -2129,12 +2130,13 @@ data LintEnv
, le_subst :: TCvSubst -- Current TyCo substitution
-- See Note [Linting type lets]
- -- /Only/ substitutes for type variables;
- -- but might clone CoVars
- -- We also use le_subst to keep track of
- -- in-scope TyVars and CoVars
+ -- /Only/ substitutes for type variables;
+ -- but might clone CoVars
+ -- We also use le_subst to keep track of
+ -- in-scope TyVars and CoVars (but not Ids)
+ -- Range of the TCvSubst is LintedType/LintedCo
- , le_ids :: IdSet -- In-scope Ids
+ , le_ids :: IdSet -- In-scope Ids; all Linted
, le_joins :: IdSet -- Join points in scope that are valid
-- A subset of the InScopeSet in le_subst
-- See Note [Join points]
@@ -2266,6 +2268,7 @@ instance HasDynFlags LintM where
data LintLocInfo
= RhsOf Id -- The variable bound
+ | OccOf Id -- Occurrence of id
| LambdaBodyOf Id -- The lambda-binder
| UnfoldingOf Id -- Unfolding of a binder
| BodyOfLetRec [Id] -- One of the binders
@@ -2278,7 +2281,6 @@ data LintLocInfo
| ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
| TopLevelBindings
| InType Type -- Inside a type
- | InKind Type Kind -- Inside a kind
| InCo Coercion -- Inside a coercion
initL :: DynFlags -> LintFlags -> [Var]
@@ -2341,7 +2343,7 @@ addWarnL msg = LintM $ \ env (warns,errs) ->
addMsg :: Bool -> LintEnv -> Bag MsgDoc -> MsgDoc -> Bag MsgDoc
addMsg is_error env msgs msg
- = ASSERT( notNull loc_msgs )
+ = ASSERT2( notNull loc_msgs, msg )
msgs `snocBag` mk_msg msg
where
loc_msgs :: [(SrcLoc, SDoc)] -- Innermost first
@@ -2373,16 +2375,15 @@ inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
is_case_pat (LE { le_loc = CasePat {} : _ }) = True
is_case_pat _other = False
-addInScopeTyCoVar :: Var -> LintM a -> LintM a
-addInScopeTyCoVar var m
- = LintM $ \ env errs ->
- unLintM m (env { le_subst = extendTCvInScope (le_subst env) var }) errs
-
addInScopeId :: Id -> LintM a -> LintM a
addInScopeId id m
- = LintM $ \ env errs ->
- unLintM m (env { le_ids = extendVarSet (le_ids env) id
- , le_joins = delVarSet (le_joins env) id }) errs
+ = LintM $ \ env@(LE { le_ids = id_set, le_joins = join_set }) errs ->
+ unLintM m (env { le_ids = extendVarSet id_set id
+ , le_joins = add_joins join_set }) errs
+ where
+ add_joins join_set
+ | isJoinId id = extendVarSet join_set id -- Overwrite with new arity
+ | otherwise = delVarSet join_set id -- Remove any existing binding
getInScopeIds :: LintM IdSet
getInScopeIds = LintM (\env errs -> (Just (le_ids env), errs))
@@ -2404,13 +2405,6 @@ markAllJoinsBadIf :: Bool -> LintM a -> LintM a
markAllJoinsBadIf True m = markAllJoinsBad m
markAllJoinsBadIf False m = m
-addGoodJoins :: [Var] -> LintM a -> LintM a
-addGoodJoins vars thing_inside
- = LintM $ \ env errs -> unLintM thing_inside (add_joins env) errs
- where
- add_joins env = env { le_joins = le_joins env `extendVarSetList` join_ids }
- join_ids = filter isJoinId vars
-
getValidJoins :: LintM IdSet
getValidJoins = LintM (\ env errs -> (Just (le_joins env), errs))
@@ -2420,12 +2414,6 @@ getTCvSubst = LintM (\ env errs -> (Just (le_subst env), errs))
getInScope :: LintM InScopeSet
getInScope = LintM (\ env errs -> (Just (getTCvInScope $ le_subst env), errs))
-applySubstTy :: InType -> LintM OutType
-applySubstTy ty = do { subst <- getTCvSubst; return (substTy subst ty) }
-
-applySubstCo :: InCoercion -> LintM OutCoercion
-applySubstCo co = do { subst <- getTCvSubst; return (substCo subst co) }
-
lookupIdInScope :: Id -> LintM Id
lookupIdInScope id_occ
= do { in_scope_ids <- getInScopeIds
@@ -2461,16 +2449,7 @@ lookupJoinId id
Just id' -> return (isJoinId_maybe id')
Nothing -> return Nothing }
-lintTyCoVarInScope :: TyCoVar -> LintM TyCoVar
-lintTyCoVarInScope var
- = do { subst <- getTCvSubst
- ; case lookupInScope (getTCvInScope subst) var of
- Just var' -> return var'
- Nothing -> failWithL $
- hang (text "The TyCo variable" <+> pprBndr LetBind var)
- 2 (text "is out of scope") }
-
-ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
+ensureEqTys :: LintedType -> LintedType -> MsgDoc -> LintM ()
-- check ty2 is subtype of ty1 (ie, has same structure but usage
-- annotations need only be consistent, not equal)
-- Assumes ty1,ty2 are have already had the substitution applied
@@ -2500,6 +2479,9 @@ dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
dumpLoc (RhsOf v)
= (getSrcLoc v, text "In the RHS of" <+> pp_binders [v])
+dumpLoc (OccOf v)
+ = (getSrcLoc v, text "In an occurrence of" <+> pp_binder v)
+
dumpLoc (LambdaBodyOf b)
= (getSrcLoc b, text "In the body of lambda with binder" <+> pp_binder b)
@@ -2534,8 +2516,6 @@ dumpLoc TopLevelBindings
= (noSrcLoc, Outputable.empty)
dumpLoc (InType ty)
= (noSrcLoc, text "In the type" <+> quotes (ppr ty))
-dumpLoc (InKind ty ki)
- = (noSrcLoc, text "In the kind of" <+> parens (ppr ty <+> dcolon <+> ppr ki))
dumpLoc (InCo co)
= (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
@@ -2780,7 +2760,7 @@ mkJoinBndrOccMismatchMsg bndr join_arity_bndr join_arity_occ
, text "Arity at binding site:" <+> ppr join_arity_bndr
, text "Arity at occurrence: " <+> ppr join_arity_occ ]
-mkBndrOccTypeMismatchMsg :: Var -> Var -> OutType -> OutType -> SDoc
+mkBndrOccTypeMismatchMsg :: Var -> Var -> LintedType -> LintedType -> SDoc
mkBndrOccTypeMismatchMsg bndr var bndr_ty var_ty
= vcat [ text "Mismatch in type between binder and occurrence"
, text "Binder:" <+> ppr bndr <+> dcolon <+> ppr bndr_ty
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -2447,7 +2447,7 @@ normally it would make no sense to have
forall r. (ty :: K r)
because the kind of the forall would escape the binding
of 'r'. But in this case it's fine because (K r) exapands
-to Type, so we expliclity /permit/ the type
+to Type, so we explicitly /permit/ the type
forall r. T r
To accommodate such a type, in typeKind (forall a.ty) we use
@@ -2455,8 +2455,13 @@ occCheckExpand to expand any type synonyms in the kind of 'ty'
to eliminate 'a'. See kinding rule (FORALL) in
Note [Kinding rules for types]
-And in TcValidity.checkEscapingKind, we use also use
-occCheckExpand, for the same reason.
+See also
+ * TcUnify.occCheckExpand
+ * GHC.Core.Utils.coreAltsType
+ * TcValidity.checkEscapingKind
+all of which grapple with with the same problem.
+
+See #14939.
-}
-----------------------------
=====================================
testsuite/tests/indexed-types/should_compile/T17923.hs
=====================================
@@ -0,0 +1,44 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wall #-}
+module Bug where
+
+import Data.Kind
+
+-- type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
+type SingFunction2 f = forall t1. Sing t1 -> forall t2. Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
+singFun2 :: forall f. SingFunction2 f -> Sing f
+singFun2 f = SLambda (\x -> SLambda (f x))
+
+type family Sing :: k -> Type
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: a ~> b) (x :: a) :: b
+data Sym4 a
+data Sym3 a
+
+type instance Apply Sym3 _ = Sym4
+
+newtype SLambda (f :: k1 ~> k2) =
+ SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
+type instance Sing = SLambda
+
+und :: a
+und = undefined
+
+data E
+data ShowCharSym0 :: E ~> E ~> E
+
+sShow_tuple :: SLambda Sym4
+sShow_tuple
+ = applySing (singFun2 @Sym3 und)
+ (und (singFun2 @Sym3
+ (und (applySing (singFun2 @Sym3 und)
+ (applySing (singFun2 @ShowCharSym0 und) und)))))
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -294,3 +294,4 @@ test('T16828', normal, compile, [''])
test('T17008b', normal, compile, [''])
test('T17056', normal, compile, [''])
test('T17405', normal, multimod_compile, ['T17405c', '-v0'])
+test('T17923', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8ae203c70bbaec128264fa4a25e4af3b1685843a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8ae203c70bbaec128264fa4a25e4af3b1685843a
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/20200325/0ff03b4b/attachment-0001.html>
More information about the ghc-commits
mailing list