Commit 0a12d92a authored by Simon Peyton Jones's avatar Simon Peyton Jones

Further improvements to well-kinded types

The typechecker has the invariant that every type should be well-kinded
as it stands, without zonking.  See Note [The well-kinded type invariant]
in TcType.

That invariant was not being upheld, which led to Trac #14174.  I fixed
part of it, but T14174a showed that there was more.  This patch finishes
the job.

* See Note [The tcType invariant] in TcHsType, which articulates an
  invariant that was very nearly, but not quite, true.  One place that
  falisified it was the HsWildCardTy case of tc_hs_type, so I fixed that.

* mkNakedCastTy now makes no attempt to eliminate casts; indeed it cannot
  lest it break Note [The well-kinded type invariant].  The prior comment
  suggested that it was crucial for performance but happily it seems not
  to be. The extra Refls are eliminated by the zonker.

* I found I could tidy up TcHsType.instantiateTyN and instantiateTyUntilN
  by eliminating one of its parameters.  That led to a cascade of minor
  improvements in TcTyClsDecls. Hooray.
parent 63e968a9
This diff is collapsed.
......@@ -1143,9 +1143,8 @@ tcDefaultAssocDecl _ (d1:_:_)
= failWithTc (text "More than one default declaration for"
<+> ppr (feqn_tycon (unLoc d1)))
tcDefaultAssocDecl fam_tc [L loc (FamEqn { feqn_tycon = lname@(L _ tc_name)
tcDefaultAssocDecl fam_tc [L loc (FamEqn { feqn_tycon = L _ tc_name
, feqn_pats = hs_tvs
, feqn_fixity = fixity
, feqn_rhs = rhs })]
| HsQTvs { hsq_implicit = imp_vars, hsq_explicit = exp_vars } <- hs_tvs
= -- See Note [Type-checking default assoc decls]
......@@ -1166,7 +1165,6 @@ tcDefaultAssocDecl fam_tc [L loc (FamEqn { feqn_tycon = lname@(L _ tc_name)
-- Typecheck RHS
; let all_vars = imp_vars ++ map hsLTyVarName exp_vars
pats = map hsLTyVarBndrToType exp_vars
pp_lhs = pprFamInstLHS lname pats fixity [] Nothing
-- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
-- the LHsQTyVars used for declaring a tycon, but the names here
......@@ -1178,7 +1176,7 @@ tcDefaultAssocDecl fam_tc [L loc (FamEqn { feqn_tycon = lname@(L _ tc_name)
-- enclosing class. So it's treated more as a freestanding beast.
; (pats', rhs_ty)
<- tcFamTyPats fam_tc Nothing all_vars pats
(kcTyFamEqnRhs Nothing pp_lhs rhs) $
(kcTyFamEqnRhs Nothing rhs) $
\tvs pats rhs_kind ->
do { rhs_ty <- solveEqualities $
tcCheckLHsType rhs rhs_kind
......@@ -1222,55 +1220,62 @@ proper tcMatchTys here.) -}
kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM ()
kcTyFamInstEqn tc_fam_tc
(L loc (HsIB { hsib_vars = tv_names
, hsib_body = FamEqn { feqn_tycon = lname@(L _ eqn_tc_name)
, hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
, feqn_pats = pats
, feqn_fixity = fixity
, feqn_rhs = hs_ty }}))
= setSrcSpan loc $
do { checkTc (fam_name == eqn_tc_name)
do { traceTc "kcTyFamInstEqn" (vcat
[ text "tc_name =" <+> ppr eqn_tc_name
, text "fam_tc =" <+> ppr tc_fam_tc <+> dcolon <+> ppr (tyConKind tc_fam_tc)
, text "hsib_vars =" <+> ppr tv_names
, text "feqn_pats =" <+> ppr pats ])
; checkTc (fam_name == eqn_tc_name)
(wrongTyFamName fam_name eqn_tc_name)
; discardResult $
tc_fam_ty_pats tc_fam_tc Nothing -- not an associated type
tv_names pats (kcTyFamEqnRhs Nothing pp_lhs hs_ty) }
tv_names pats (kcTyFamEqnRhs Nothing hs_ty) }
where
fam_name = tyConName tc_fam_tc
pp_lhs = pprFamInstLHS lname pats fixity [] Nothing
-- Infer the kind of the type on the RHS of a type family eqn. Then use
-- this kind to check the kind of the LHS of the equation. This is useful
-- as the callback to tc_fam_ty_pats and the kind-checker to
-- tcFamTyPats.
kcTyFamEqnRhs :: Maybe ClsInstInfo
-> SDoc -- ^ Eqn LHS (for errors only)
-> LHsType GhcRn -- ^ Eqn RHS
-> TcKind -- ^ Inferred kind of left-hand side
-> TcM ([TcType], TcKind) -- ^ New pats, inst'ed kind of left-hand side
kcTyFamEqnRhs mb_clsinfo pp_lhs_ty rhs_hs_ty lhs_ki
kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki
= do { -- It's still possible the lhs_ki has some foralls. Instantiate these away.
(_lhs_ty', new_pats, insted_lhs_ki)
<- instantiateTyUntilN mb_kind_env 0 bogus_ty lhs_ki
(new_pats, insted_lhs_ki)
<- instantiateTyUntilN mb_kind_env 0 lhs_ki
; traceTc "kcTyFamEqnRhs" (vcat
[ text "rhs_hs_ty =" <+> ppr rhs_hs_ty
, text "lhs_ki =" <+> ppr lhs_ki
, text "insted_lhs_ki =" <+> ppr insted_lhs_ki
, text "new_pats =" <+> ppr new_pats
])
; _ <- tcCheckLHsType rhs_hs_ty insted_lhs_ki
; return (new_pats, insted_lhs_ki) }
where
mb_kind_env = thdOf3 <$> mb_clsinfo
bogus_ty = pprPanic "kcTyFamEqnRhs" (pp_lhs_ty $$ ppr rhs_hs_ty)
tcTyFamInstEqn :: TcTyCon -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn
-> TcM CoAxBranch
-- Needs to be here, not in TcInstDcls, because closed families
-- (typechecked here) have TyFamInstEqns
tcTyFamInstEqn fam_tc mb_clsinfo
(L loc (HsIB { hsib_vars = tv_names
, hsib_body = FamEqn { feqn_tycon = lname@(L _ eqn_tc_name)
, hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
, feqn_pats = pats
, feqn_fixity = fixity
, feqn_rhs = hs_ty }}))
= ASSERT( getName fam_tc == eqn_tc_name )
setSrcSpan loc $
tcFamTyPats fam_tc mb_clsinfo tv_names pats
(kcTyFamEqnRhs mb_clsinfo pp_lhs hs_ty) $
(kcTyFamEqnRhs mb_clsinfo hs_ty) $
\tvs pats res_kind ->
do { rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
......@@ -1282,8 +1287,6 @@ tcTyFamInstEqn fam_tc mb_clsinfo
; return (mkCoAxBranch tvs' [] pats' rhs_ty'
(map (const Nominal) tvs')
loc) }
where
pp_lhs = pprFamInstLHS lname pats fixity [] Nothing
kcDataDefn :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
-- (associated types only)
......
......@@ -1383,17 +1383,44 @@ mkNakedAppTy :: Type -> Type -> Type
mkNakedAppTy ty1 ty2 = mkNakedAppTys ty1 [ty2]
mkNakedCastTy :: Type -> Coercion -> Type
-- Do simple, fast compaction; especially dealing with Refl
-- for which it's plain stupid to create a cast
-- This simple function killed off a huge number of Refl casts
-- in types, at birth.
-- Note that it's fine to do this even for a "mkNaked" function,
-- because we don't look at TyCons. isReflCo checks if the coercion
-- is structurally Refl; it does not check for shape k ~ k.
mkNakedCastTy ty co | isReflCo co = ty
mkNakedCastTy (CastTy ty co1) co2 = CastTy ty (co1 `mkTransCo` co2)
-- Do /not/ attempt to get rid of the cast altogether,
-- even if it is Refl: see Note [The well-kinded type invariant]
-- Even doing (t |> co1) |> co2 ---> t |> (co1;co2)
-- does not seem worth the bother
--
-- NB: zonking will get rid of these casts, because it uses mkCastTy
--
-- In fact the calls to mkNakedCastTy ar pretty few and far between.
mkNakedCastTy ty co = CastTy ty co
{- Note [The well-kinded type invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
During type inference, we maintain the invariant that
INVARIANT: every type is well-kinded /without/ zonking
and in particular that typeKind does not fail (as it can for
ill-kinded types).
Now suppose we are kind-checking the type (a Int), where (a :: kappa).
Then in tcInferApps we'll run out of binders on a's kind, so
we'll call matchExpectedFunKind, and unify
kappa := kappa1 -> kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2)
That evidence is actually Refl, but we must not discard the cast to
form the result type
((a::kappa) (Int::*))
bacause that does not satisfy the invariant, and crashes TypeKind. This
caused Trac #14174 and #14520.
Solution: make mkNakedCastTy use an actual CastTy, without optimising
for Refl. Now everything is well-kinded. The CastTy will be removed
later, when we zonk. Still, it's distressingly delicate.
NB: mkNakedCastTy is only called in two places:
in tcInferApps and in checkExpectedResultKind.
See Note [The tcType invariant] in TcHsType.
-}
{-
************************************************************************
* *
......@@ -1707,10 +1734,10 @@ tcSplitMethodTy ty
* *
********************************************************************* -}
tcEqKind :: TcKind -> TcKind -> Bool
tcEqKind :: HasDebugCallStack => TcKind -> TcKind -> Bool
tcEqKind = tcEqType
tcEqType :: TcType -> TcType -> Bool
tcEqType :: HasDebugCallStack => TcType -> TcType -> Bool
-- tcEqType is a proper implements the same Note [Non-trivial definitional
-- equality] (in TyCoRep) as `eqType`, but Type.eqType believes (* ==
-- Constraint), and that is NOT what we want in the type checker!
......
......@@ -2,5 +2,5 @@
T7524.hs:5:15: error:
Conflicting family instance declarations:
forall k2 (a :: k2). F a a = Int -- Defined at T7524.hs:5:15
forall k2 k1 (a :: k1) (b :: k2).
forall k1 k2 (a :: k1) (b :: k2).
F a b = Bool -- Defined at T7524.hs:6:15
......@@ -175,7 +175,7 @@ test('T13391a', normal, compile, [''])
test('T14270', normal, compile, [''])
test('T14450', normal, compile_fail, [''])
test('T14174', normal, compile_fail, [''])
test('T14174a', expect_broken(14174), compile_fail, [''])
test('T14174a', normal, compile, [''])
test('T14520', normal, compile_fail, [''])
test('T11203', normal, compile_fail, [''])
test('T14555', normal, compile_fail, [''])
......
......@@ -24,11 +24,11 @@ T6018failclosed.hs:19:5: error:
T6018failclosed.hs:25:5: error:
• Type family equation violates injectivity annotation.
Type and kind variables ‘k2’, ‘b’
Type and kind variables ‘k1’, ‘b’
cannot be inferred from the right-hand side.
Use -fprint-explicit-kinds to see the kind arguments
In the type family equation:
forall k1 k2 (b :: k2) (c :: k1).
forall k1 k2 (b :: k1) (c :: k2).
JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5
• In the equations for closed type family ‘JClosed’
In the type family declaration for ‘JClosed’
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment