Commit 8b36ed12 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Build only well-kinded types in type checker

During type inference, we maintain the invariant that every type is
well-kinded /without/ zonking; and in particular that typeKind does
not fail (as it can for ill-kinded types).

But TcHsType.tcInferApps was not guaranteeing this invariant,
resulting in Trac #14174 and #14520.

This patch fixes it, making things better -- but it does /not/
fix the program in Trac #14174 comment:5, which still crashes.
So more work to be done.

See Note [Ensure well-kinded types] in TcHsType
parent 716acbb5
......@@ -64,6 +64,7 @@ import TcSimplify ( solveEqualities )
import TcType
import TcHsSyn( zonkSigType )
import Inst ( tcInstBinders, tcInstBinder )
import TyCoRep( Type( CastTy ) )
import Type
import Kind
import RdrName( lookupLocalRdrOcc )
......@@ -869,16 +870,40 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
| otherwise
-- Even after substituting, still no binders. Use matchExpectedFunKind
= do { traceTc "tcInferApps (no binder)" (ppr new_inner_ki $$ ppr zapped_subst)
; (co, arg_k, res_k)
<- matchExpectedFunKind (mkHsAppTys orig_hs_ty (take (n-1) orig_hs_args))
substed_inner_ki
; let subst' = zapped_subst `extendTCvInScopeSet` tyCoVarsOfTypes [arg_k, res_k]
; go n acc_args subst' (fun `mkNakedCastTy` co)
[mkAnonBinder arg_k] res_k all_args }
; (co, arg_k, res_k) <- matchExpectedFunKind hs_ty substed_inner_ki
; let new_in_scope = tyCoVarsOfTypes [arg_k, res_k]
subst' = zapped_subst `extendTCvInScopeSet` new_in_scope
; go n acc_args subst'
(fun `CastTy` co) -- NB: CastTy, not mkCastTy or mkNakedCastTy!
-- See Note [Ensure well-kinded types]
[mkAnonBinder arg_k]
res_k all_args }
where
substed_inner_ki = substTy subst inner_ki
(new_ki_binders, new_inner_ki) = tcSplitPiTys substed_inner_ki
zapped_subst = zapTCvSubst subst
hs_ty = mkHsAppTys orig_hs_ty (take (n-1) orig_hs_args)
{- Note [Ensure well-kinded types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
During type inference, we maintain the invariant that every type is
well-kinded /without/ zonking; and in particular that typeKind does not
fail (as it can for ill-kinded types).
We need to be careful at this point. 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)
But that evidence is actually Refl, so if we use the smart constructor
mkNakedCastTy, we'll form the result type
((a::kappa) (Int::*))
which does not satisfy the invariant, and crashes TypeKind. This
caused Trac #14174 and #14520.
Solution: use an actual CastTy. Now everything is well-kinded.
The CastTy will be removed later, when we zonk. Still, it's
distressingly delicate.
-}
-- | Applies a type to a list of arguments.
-- Always consumes all the arguments, using 'matchExpectedFunKind' as
......@@ -1873,6 +1898,9 @@ tcTyClTyVars tycon_name thing_inside
res_kind = tyConResKind tycon
binders = correct_binders (tyConBinders tycon) res_kind
; traceTc "tcTyClTyVars" (vcat [ ppr tycon
, ppr (tyConBinders tycon)
, ppr (tcTyConScopedTyVars tycon) ])
-- See Note [Free-floating kind vars]
; zonked_scoped_tvs <- mapM zonkTcTyVarToTyVar scoped_tvs
; let still_sig_tvs = filter isSigTyVar zonked_scoped_tvs
......
{-# LANGUAGE TypeInType, RankNTypes, KindSignatures, PolyKinds #-}
module T14174 where
data T k (x :: k) = MkT
data S x = MkS (T (x Int) x)
T14174.hs:6:27: error:
• Expecting one more argument to ‘x’
Expected kind ‘x Int’, but ‘x’ has kind ‘* -> *’
• In the second argument of ‘T’, namely ‘x’
In the type ‘(T (x Int) x)’
In the definition of data constructor ‘MkS’
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module T14174a where
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@
data FunArrow = (:->) | (:~>)
class FunType (arr :: FunArrow) where
type Fun (k1 :: Type) arr (k2 :: Type) :: Type
class FunType arr => AppType (arr :: FunArrow) where
type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
type FunApp arr = (FunType arr, AppType arr)
instance FunType (:->) where
type Fun k1 (:->) k2 = k1 -> k2
instance AppType (:->) where
type App k1 (:->) k2 (f :: k1 -> k2) x = f x
instance FunType (:~>) where
type Fun k1 (:~>) k2 = k1 ~> k2
instance AppType (:~>) where
type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
infixr 0 -?>
type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
type family ElimBool (p :: Bool -> Type)
(z :: Bool)
(pFalse :: p False)
(pTrue :: p True)
:: p z where
-- Commenting out the line below makes the panic go away
ElimBool p z pFalse pTrue = ElimBoolPoly (:->) p z pFalse pTrue
type family ElimBoolPoly (arr :: FunArrow)
(p :: (Bool -?> Type) arr)
(z :: Bool)
(pFalse :: App Bool arr Type p False)
(pTrue :: App Bool arr Type p True)
:: App Bool arr Type p z
{-# Language TypeInType, TypeFamilies, TypeOperators #-}
module T14520 where
import Data.Kind
type a ~>> b = (a, b) -> Type
data family Sing (a::k)
type family XXX (f::a~>>b) (x::a) :: b
type family Id :: (kat :: a ~>> (a ~>> *)) `XXX` (b :: a) `XXX` b
sId :: Sing w -> Sing (Id :: bat w w)
sId = sId
T14520.hs:15:24: error:
• Expected kind ‘bat w w’, but ‘Id’ has kind ‘XXX (XXX kat0 b0) b0’
• In the first argument of ‘Sing’, namely ‘(Id :: bat w w)’
In the type signature: sId :: Sing w -> Sing (Id :: bat w w)
......@@ -174,3 +174,6 @@ test('T13391', normal, compile_fail, [''])
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('T14520', normal, compile_fail, [''])
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