Commit 3d252037 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Respect Note [The tcType invariant]

I tried to do this with

    commit 0a12d92a
    Author: Simon Peyton Jones <simonpj@microsoft.com>
    Date:   Wed Dec 13 12:53:26 2017 +0000

    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.

But I didn't get it quite right as Trac #14873 showed.

This patch fixes the problem; although I am still a bit unhappy.
(See "A worry" in the HsApp case of tc_infer_hs_type.)
parent e7653bc3
......@@ -500,22 +500,31 @@ tc_infer_lhs_type mode (L span ty)
-- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking]
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
tc_infer_hs_type mode (HsParTy t) = tc_infer_lhs_type mode t
tc_infer_hs_type mode (HsTyVar _ (L _ tv)) = tcTyVar mode tv
tc_infer_hs_type mode (HsAppTy ty1 ty2)
= do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
; (fun_ty', fun_kind) <- tc_infer_lhs_type mode fun_ty
; fun_kind' <- zonkTcType fun_kind
; tcTyApps mode fun_ty fun_ty' fun_kind' arg_tys }
tc_infer_hs_type mode (HsParTy t) = tc_infer_lhs_type mode t
tc_infer_hs_type mode (HsOpTy lhs (L loc_op op) rhs)
| not (op `hasKey` funTyConKey)
= do { (op', op_kind) <- tcTyVar mode op
; op_kind' <- zonkTcType op_kind
; tcTyApps mode (noLoc $ HsTyVar NotPromoted (L loc_op op)) op' op_kind' [lhs, rhs] }
= do { let (hs_fun_ty, hs_arg_tys) = splitHsAppTys ty1 [ty2]
; (fun_ty, fun_kind) <- tc_infer_lhs_type mode hs_fun_ty
-- A worry: what if fun_kind needs zoonking?
-- We used to zonk it here, but that got fun_ty and fun_kind
-- out of sync (see the precondition to tcTyApps), which caused
-- Trac #14873. So I'm now zonking in tcTyVar, and not here.
-- Is that enough? Seems so, but I can't see how to be certain.
; tcTyApps mode hs_fun_ty fun_ty fun_kind hs_arg_tys }
tc_infer_hs_type mode (HsOpTy lhs lhs_op@(L _ hs_op) rhs)
| not (hs_op `hasKey` funTyConKey)
= do { (op, op_kind) <- tcTyVar mode hs_op
-- See "A worry" in the HsApp case
; tcTyApps mode (noLoc $ HsTyVar NotPromoted lhs_op) op op_kind [lhs, rhs] }
tc_infer_hs_type mode (HsKindSig ty sig)
= do { sig' <- tc_lhs_kind (kindLevel mode) sig
; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
; ty' <- tc_lhs_type mode ty sig'
; return (ty', sig') }
-- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
-- the splice location to the typechecker. Here we skip over it in order to have
-- the same kind inferred for a given expression whether it was produced from
......@@ -524,6 +533,7 @@ tc_infer_hs_type mode (HsKindSig ty sig)
-- See Note [Delaying modFinalizers in untyped splices].
tc_infer_hs_type mode (HsSpliceTy (HsSpliced _ (HsSplicedTy ty)) _)
= tc_infer_hs_type mode ty
tc_infer_hs_type mode (HsDocTy ty _) = tc_infer_lhs_type mode ty
tc_infer_hs_type _ (HsCoreTy ty) = return (ty, typeKind ty)
tc_infer_hs_type mode other_ty
......@@ -846,6 +856,10 @@ tcInferApps :: TcTyMode
-> TcKind -- ^ Function kind (zonked)
-> [LHsType GhcRn] -- ^ Args
-> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
-- Precondition: typeKind fun_ty = fun_ki
-- Reason: we will return a type application like (fun_ty arg1 ... argn),
-- and that type must be well-kinded
-- See Note [The tcType invariant]
tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
= do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
; stuff <- go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
......@@ -887,7 +901,8 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
tc_lhs_type mode arg (substTy subst $ tyBinderType ki_binder)
; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
; go (n+1) (arg' : acc_args) subst' (mkNakedAppTy fun arg')
; go (n+1) (arg' : acc_args) subst'
(mkNakedAppTy fun arg')
ki_binders inner_ki args }
-- We've run out of known binders in the functions's kind.
......@@ -924,8 +939,9 @@ tcTyApps :: TcTyMode
-> TcKind -- ^ Function kind (zonked)
-> [LHsType GhcRn] -- ^ Args
-> TcM (TcType, TcKind) -- ^ (f args, result kind)
tcTyApps mode orig_hs_ty ty ki args
= do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty ty ki args
-- Precondition: see precondition for tcInferApps
tcTyApps mode orig_hs_ty fun_ty fun_ki args
= do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty fun_ty fun_ki args
; return (ty', ki') }
--------------------------
......@@ -965,6 +981,12 @@ checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
, uo_visible = True } -- the hs_ty is visible
ty' = mkNakedAppTys ty new_args
; traceTc "checkExpectedKind" $
vcat [ pp_hs_ty
, text "act_kind:" <+> ppr act_kind
, text "act_kind':" <+> ppr act_kind'
, text "exp_kind:" <+> ppr exp_kind ]
; if act_kind' `tcEqType` exp_kind
then return (ty', new_args, mkTcNomReflCo exp_kind) -- This is very common
else do { co_k <- uType KindLevel origin act_kind' exp_kind
......@@ -1039,7 +1061,16 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
= do { traceTc "lk1" (ppr name)
; thing <- tcLookup name
; case thing of
ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
ATyVar _ tv -> -- Important: zonk before returning
-- We may have the application ((a::kappa) b)
-- where kappa is already unified to (k1 -> k2)
-- Then we want to see that arrow. Best done
-- here because we are also maintaining
-- Note [The tcType invariant], so we don't just
-- want to zonk the kind, leaving the TyVar
-- un-zonked (Trac #114873)
do { ty <- zonkTcTyVar tv
; return (ty, typeKind ty) }
ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference]
unless
......
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module T14873 where
import Data.Kind (Type)
data family Sing (a :: k)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
class SingI (a :: k) where
sing :: Sing a
data ColSym1 :: f a -> a ~> Bool
type instance Apply (ColSym1 x) y = Col x y
class PColumn (f :: Type -> Type) where
type Col (x :: f a) (y :: a) :: Bool
class SColumn (f :: Type -> Type) where
sCol :: forall (x :: f a) (y :: a).
Sing x -> Sing y -> Sing (Col x y :: Bool)
instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where
sing = SLambda (sCol (sing @_ @x))
{- When the bug was present, this smaller kind-incorrect version also
elicited the same piResultTy crash
But it's kind-incorrect, whereas the main test case should compile file
class SingI (a :: k) where
class SColumn (f :: Type -> Type) where
instance -- forall (f :: Type -> Type) a (x :: f a).
SColumn f => SingI (x :: f a)
-}
......@@ -185,4 +185,5 @@ test('T14580', normal, compile_fail, [''])
test('T14515', normal, compile, [''])
test('T14723', normal, compile, [''])
test('T14846', normal, compile_fail, [''])
test('T14873', normal, compile, [''])
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