-- Typechecking kinded types
tcHsKindedContext, tcHsKindedType, tcHsBangType,
- tcTyVarBndrs, dsHsType,
+ tcTyVarBndrs, dsHsType, kcHsLPred, dsHsLPred,
tcDataKindSig, ExpKind(..), EkCtxt(..),
-- Pattern type signatures
import {- Kind parts of -} Type
import Var
import VarSet
-import Coercion
import TyCon
import Class
import Name
; checkValidType ctxt ty
; return ty }
-tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Type)
+tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Class, [Type])
-- Typecheck an instance head. We can't use
-- tcHsSigType, because it's not a valid user type.
-tcHsInstHead (L loc ty)
+tcHsInstHead (L loc hs_ty)
= setSrcSpan loc $ -- No need for an "In the type..." context
- tc_inst_head ty -- because that comes from the caller
+ -- because that comes from the caller
+ do { kinded_ty <- kc_inst_head hs_ty
+ ; ds_inst_head kinded_ty }
where
- -- tc_inst_head expects HsPredTy, which isn't usually even allowed
- tc_inst_head (HsPredTy pred)
- = do { pred' <- kcHsPred pred
- ; pred'' <- dsHsPred pred'
- ; return ([], [], mkPredTy pred'') }
-
- tc_inst_head (HsForAllTy _ tvs ctxt (L _ (HsPredTy pred)))
- = kcHsTyVars tvs $ \ tvs' ->
- do { ctxt' <- kcHsContext ctxt
- ; pred' <- kcHsPred pred
- ; tcTyVarBndrs tvs' $ \ tvs'' ->
- do { ctxt'' <- mapM dsHsLPred (unLoc ctxt')
- ; pred'' <- dsHsPred pred'
- ; return (tvs'', ctxt'', mkPredTy pred'') } }
-
- tc_inst_head _ = failWithTc (ptext (sLit "Malformed instance type"))
+ kc_inst_head ty@(HsPredTy pred@(HsClassP {}))
+ = do { (pred', kind) <- kc_pred pred
+ ; checkExpectedKind ty kind ekLifted
+ ; return (HsPredTy pred') }
+ kc_inst_head (HsForAllTy exp tv_names context (L loc ty))
+ = kcHsTyVars tv_names $ \ tv_names' ->
+ do { ctxt' <- kcHsContext context
+ ; ty' <- kc_inst_head ty
+ ; return (HsForAllTy exp tv_names' ctxt' (L loc ty')) }
+ kc_inst_head _ = failWithTc (ptext (sLit "Malformed instance type"))
+
+ ds_inst_head (HsPredTy (HsClassP cls_name tys))
+ = do { clas <- tcLookupClass cls_name
+ ; arg_tys <- dsHsTypes tys
+ ; return ([], [], clas, arg_tys) }
+ ds_inst_head (HsForAllTy _ tvs ctxt (L _ tau))
+ = tcTyVarBndrs tvs $ \ tvs' ->
+ do { ctxt' <- mapM dsHsLPred (unLoc ctxt)
+ ; (tvs_r, ctxt_r, cls, tys) <- ds_inst_head tau
+ ; return (tvs' ++ tvs_r, ctxt' ++ ctxt_r , cls, tys) }
+ ds_inst_head _ = panic "ds_inst_head"
tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
-- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
kc_hs_type (HsPredTy pred)
= wrongPredErr pred
+kc_hs_type (HsCoreTy ty)
+ = return (HsCoreTy ty, typeKind ty)
+
kc_hs_type (HsForAllTy exp tv_names context ty)
= kcHsTyVars tv_names $ \ tv_names' ->
do { ctxt' <- kcHsContext context
splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
splitFunKind _ _ fk [] = return ([], fk)
splitFunKind the_fun arg_no fk (arg:args)
- = do { mb_fk <- unifyFunKind fk
+ = do { mb_fk <- matchExpectedFunKind fk
; case mb_fk of
Nothing -> failWithTc too_many_args
Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
kcHsLPred = wrapLocM kcHsPred
kcHsPred :: HsPred Name -> TcM (HsPred Name)
-kcHsPred pred = do -- Checks that the result is of kind liftedType
+kcHsPred pred = do -- Checks that the result is a type kind
(pred', kind) <- kc_pred pred
- checkExpectedKind pred kind ekLifted
+ checkExpectedKind pred kind ekOpen
return pred'
---------------------------
-- application (reason: used from TcDeriv)
kc_pred (HsIParam name ty)
= do { (ty', kind) <- kc_lhs_type ty
- ; return (HsIParam name ty', kind)
- }
+ ; return (HsIParam name ty', kind) }
kc_pred (HsClassP cls tys)
= do { kind <- kcClass cls
; (tys', res_kind) <- kcApps cls kind tys
- ; return (HsClassP cls tys', res_kind)
- }
+ ; return (HsClassP cls tys', res_kind) }
kc_pred (HsEqualP ty1 ty2)
= do { (ty1', kind1) <- kc_lhs_type ty1
--- ; checkExpectedKind ty1 kind1 liftedTypeKind
; (ty2', kind2) <- kc_lhs_type ty2
--- ; checkExpectedKind ty2 kind2 liftedTypeKind
; checkExpectedKind ty2 kind2 (EK kind1 EkEqPred)
- ; return (HsEqualP ty1' ty2', liftedTypeKind)
- }
+ ; return (HsEqualP ty1' ty2', unliftedTypeKind) }
---------------------------
kcTyVar :: Name -> TcM TcKind
kcTyVar name = do -- Could be a tyvar or a tycon
- traceTc (text "lk1" <+> ppr name)
+ traceTc "lk1" (ppr name)
thing <- tcLookup name
- traceTc (text "lk2" <+> ppr name <+> ppr thing)
+ traceTc "lk2" (ppr name <+> ppr thing)
case thing of
ATyVar _ ty -> return (typeKind ty)
AThing kind -> return kind
; newFlexiTyVarTy kind' }
ds_type (HsQuasiQuoteTy {}) = panic "ds_type" -- Eliminated by renamer
+ds_type (HsCoreTy ty) = return ty
dsHsTypes :: [LHsType Name] -> TcM [Type]
dsHsTypes arg_tys = mapM dsHsType arg_tys
tcPatSig :: UserTypeCtxt
-> LHsType Name
- -> BoxySigmaType
+ -> TcSigmaType
-> TcM (TcType, -- The type to use for "inside" the signature
[(Name, TcType)], -- The new bit of type environment, binding
-- the scoped type variables
- CoercionI) -- Coercion due to unification with actual ty
+ HsWrapper) -- Coercion due to unification with actual ty
+ -- Of shape: res_ty ~ sig_ty
tcPatSig ctxt sig res_ty
= do { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
+ -- sig_tvs are the type variables free in 'sig',
+ -- and not already in scope. These are the ones
+ -- that should be brought into scope
; if null sig_tvs then do {
-- The type signature binds no type variables,
-- and hence is rigid, so use it to zap the res_ty
- coi <- boxyUnify sig_ty res_ty
- ; return (sig_ty, [], coi)
+ wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty
+ ; return (sig_ty, [], wrap)
} else do {
-- Type signature binds at least one scoped type variable
_ -> False
; ASSERT( not in_pat_bind || null sig_tvs ) return ()
- -- Check that pat_ty is rigid
- ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)
-
-- Check that all newly-in-scope tyvars are in fact
-- constrained by the pattern. This catches tiresome
-- cases like
; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs
; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
- -- Now match the pattern signature against res_ty
- -- For convenience, and uniform-looking error messages
- -- we do the matching by allocating meta type variables,
- -- unifying, and reading out the results.
- -- This is a strictly local operation.
- ; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
- ; coi <- boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty)
- res_ty
- ; sig_tv_tys <- mapM readFilledBox box_tvs
-
- -- Check that each is bound to a distinct type variable,
- -- and one that is not already in scope
- ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys
+ -- Now do a subsumption check of the pattern signature against res_ty
+ ; sig_tvs' <- tcInstSigTyVars sig_tvs
+ ; let sig_ty' = substTyWith sig_tvs sig_tv_tys' sig_ty
+ sig_tv_tys' = mkTyVarTys sig_tvs'
+ ; wrap <- tcSubType PatSigOrigin ctxt res_ty sig_ty'
+
+ -- Check that each is bound to a distinct type variable,
+ -- and one that is not already in scope
; binds_in_scope <- getScopedTyVarBinds
+ ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys'
; check binds_in_scope tv_binds
- -- Phew!
- ; return (res_ty, tv_binds, coi)
+ -- Phew!
+ ; return (sig_ty', tv_binds, wrap)
} }
where
check _ [] = return ()
; check ((n,ty):in_scope) rest }
check_one in_scope n ty
- = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
- -- Must bind to a type variable
-
- ; checkTc (null dups) (dupInScope n (head dups) ty)
+ = checkTc (null dups) (dupInScope n (head dups) ty)
-- Must not bind to the same type variable
-- as some other in-scope type variable
-
- ; return () }
where
dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
\end{code}
pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
-wobblyPatSig :: [Var] -> SDoc
-wobblyPatSig sig_tvs
- = hang (ptext (sLit "A pattern type signature cannot bind scoped type variables")
- <+> pprQuotedList sig_tvs)
- 2 (ptext (sLit "unless the pattern has a rigid type context"))
-
badPatSigTvs :: TcType -> [TyVar] -> SDoc
badPatSigTvs sig_ty bad_tvs
= vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs,
, ptext (sLit "To fix this, expand the type synonym")
, ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
-scopedNonVar :: Name -> Type -> SDoc
-scopedNonVar n ty
- = vcat [sep [ptext (sLit "The scoped type variable") <+> quotes (ppr n),
- nest 2 (ptext (sLit "is bound to the type") <+> quotes (ppr ty))],
- nest 2 (ptext (sLit "You can only bind scoped type variables to type variables"))]
-
dupInScope :: Name -> Name -> Type -> SDoc
dupInScope n n' _
= hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))