tidyInsts, tidyMoreInsts,
- newDicts, newDictAtLoc, newDictsAtLoc, cloneDict,
+ newDicts, newDictsAtLoc, cloneDict,
shortCutFracLit, shortCutIntLit, newIPDict,
newMethod, newMethodFromName, newMethodWithGivenTy,
tcInstClassOp, tcInstStupidTheta,
ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
instLoc, getDictClassTys, dictPred,
+ mkInstCoFn,
lookupInst, LookupInstResult(..), lookupPred,
tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
isTyVarDict, isMethodFor,
zonkInst, zonkInsts,
- instToId, instName,
+ instToId, instToVar, instName,
InstOrigin(..), InstLoc(..), pprInstLoc
) where
import {-# SOURCE #-} TcExpr( tcPolyExpr )
import HsSyn ( HsLit(..), HsOverLit(..), HsExpr(..), LHsExpr, mkHsApp,
- nlHsLit, nlHsVar )
-import TcHsSyn ( mkHsTyApp, mkHsDictApp, zonkId )
+ ExprCoFn(..), (<.>), nlHsLit, nlHsVar )
+import TcHsSyn ( zonkId )
import TcRnMonad
import TcEnv ( tcLookupId, checkWellStaged, topIdLvl, tcMetaTy )
import InstEnv ( DFunId, InstEnv, Instance(..), OverlapFlag(..),
notElemTvSubst, extendTvSubstList )
import Unify ( tcMatchTys )
import Module ( modulePackageId )
-import Kind ( isSubKind )
+import {- Kind parts of -} Type ( isSubKind )
import HscTypes ( ExternalPackageState(..), HscEnv(..) )
import CoreFVs ( idFreeTyVars )
-import DataCon ( DataCon, dataConTyVars, dataConStupidTheta, dataConName, dataConWrapId )
+import DataCon ( DataCon, dataConStupidTheta, dataConName,
+ dataConWrapId, dataConUnivTyVars )
import Id ( Id, idName, idType, mkUserLocal, mkLocalId )
import Name ( Name, mkMethodOcc, getOccName, getSrcLoc, nameModule,
isInternalName, setNameUnique )
Selection
~~~~~~~~~
\begin{code}
+mkInstCoFn :: [TcType] -> [Inst] -> ExprCoFn
+mkInstCoFn tys dicts = CoApps (map instToId dicts) <.> CoTyApps tys
+
instName :: Inst -> Name
instName inst = idName (instToId inst)
instToId :: Inst -> TcId
-instToId (LitInst nm _ ty _) = mkLocalId nm ty
-instToId (Dict nm pred _) = mkLocalId nm (mkPredTy pred)
-instToId (Method id _ _ _ _) = id
+instToId inst = ASSERT2( isId id, ppr inst ) id
+ where
+ id = instToVar inst
+
+instToVar :: Inst -> Var
+instToVar (LitInst nm _ ty _) = mkLocalId nm ty
+instToVar (Method id _ _ _ _) = id
+instToVar (Dict nm pred _)
+ | isEqPred pred = mkTyVar nm (mkPredTy pred)
+ | otherwise = mkLocalId nm (mkPredTy pred)
instLoc (Dict _ _ loc) = loc
instLoc (Method _ _ _ _ loc) = loc
= getInstLoc orig `thenM` \ loc ->
newDictsAtLoc loc theta
-cloneDict :: Inst -> TcM Inst
+cloneDict :: Inst -> TcM Inst -- Only used for linear implicit params
cloneDict (Dict nm ty loc) = newUnique `thenM` \ uniq ->
returnM (Dict (setNameUnique nm uniq) ty loc)
-newDictAtLoc :: InstLoc -> TcPredType -> TcM Inst
-newDictAtLoc inst_loc pred
- = do { uniq <- newUnique
- ; return (mkDict inst_loc uniq pred) }
-
newDictsAtLoc :: InstLoc -> TcThetaType -> TcM [Inst]
-newDictsAtLoc inst_loc theta
- = newUniqueSupply `thenM` \ us ->
- returnM (zipWith (mkDict inst_loc) (uniqsFromSupply us) theta)
-
-mkDict inst_loc uniq pred
- = Dict name pred inst_loc
- where
- name = mkPredName uniq (instLocSrcLoc inst_loc) pred
+newDictsAtLoc inst_loc theta = mapM (newDictAtLoc inst_loc) theta
+
+{-
+newDictOcc :: InstLoc -> TcPredType -> TcM Inst
+newDictOcc inst_loc (EqPred ty1 ty2)
+ = do { unifyType ty1 ty2 -- We insist that they unify right away
+ ; return ty1 } -- And return the relexive coercion
+-}
+newDictAtLoc inst_loc pred
+ = do { uniq <- newUnique
+ ; let name = mkPredName uniq (instLocSrcLoc inst_loc) pred
+ ; return (Dict name pred inst_loc) }
-- For vanilla implicit parameters, there is only one in scope
-- at any time, so we used to use the name of the implicit parameter itself
-- But with splittable implicit parameters there may be many in
--- scope, so we make up a new name.
+-- scope, so we make up a new namea.
newIPDict :: InstOrigin -> IPName Name -> Type
-> TcM (IPName Id, Inst)
newIPDict orig ip_name ty
; extendLIEs stupid_dicts }
where
stupid_theta = dataConStupidTheta data_con
- tenv = zipTopTvSubst (dataConTyVars data_con) inst_tys
+ tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
newMethodFromName :: InstOrigin -> BoxyRhoType -> Name -> TcM TcId
newMethodFromName origin ty name
-- Methods
lookupInst inst@(Method _ id tys theta loc)
- = newDictsAtLoc loc theta `thenM` \ dicts ->
- returnM (GenInst dicts (mkHsDictApp (mkHsTyApp (L span (HsVar id)) tys) (map instToId dicts)))
+ = do { dicts <- newDictsAtLoc loc theta
+ ; let co_fn = mkInstCoFn tys dicts
+ ; return (GenInst dicts (L span $ HsCoerce co_fn (HsVar id))) }
where
span = instLocSrcSpan loc
-- any nested for-alls in rho. So the in-scope set is unchanged
dfun_rho = substTy tenv' rho
(theta, _) = tcSplitPhiTy dfun_rho
- ty_app = mkHsTyApp (L (instLocSrcSpan loc) (HsVar dfun_id))
- (map (substTyVar tenv') tyvars)
+ src_loc = instLocSrcSpan loc
+ dfun = HsVar dfun_id
+ tys = map (substTyVar tenv') tyvars
; if null theta then
- returnM (SimpleInst ty_app)
+ returnM (SimpleInst (L src_loc $ HsCoerce (CoTyApps tys) dfun))
else do
{ dicts <- newDictsAtLoc loc theta
- ; let rhs = mkHsDictApp ty_app (map instToId dicts)
- ; returnM (GenInst dicts rhs)
+ ; let co_fn = mkInstCoFn tys dicts
+ ; returnM (GenInst dicts (L src_loc $ HsCoerce co_fn dfun))
}}}}
---------------
import TcMType ( newFlexiTyVarTy, tcInstSkolTyVars, zonkTcType )
import TcBinds ( tcLocalBinds )
import TcSimplify ( tcSimplifyCheck )
-import TcPat ( tcPat, tcPats, PatCtxt(..) )
+import TcGadt ( Refinement, emptyRefinement, refineResType )
+import TcPat ( tcLamPat, tcLamPats )
import TcUnify ( checkSigTyVarsWrt, boxySplitAppTy )
import TcRnMonad
import Inst ( tcSyntaxName )
import TysPrim ( alphaTyVar )
import Type ( Kind, mkArrowKinds, liftedTypeKind, openTypeKind, tyVarsOfTypes )
-import SrcLoc ( Located(..) )
+import SrcLoc ( Located(..), noLoc, unLoc )
import Outputable
import Util ( lengthAtLeast )
do { (exp_ty1, res_ty) <- boxySplitAppTy exp_ty
; (arr_ty, arg_ty) <- boxySplitAppTy exp_ty1
; let cmd_env = CmdEnv { cmd_arr = arr_ty }
- ; (pat', cmd') <- tcPat LamPat pat arg_ty res_ty $ \ res_ty' ->
- tcCmdTop cmd_env cmd ([], res_ty')
+ ; (pat', cmd') <- tcLamPat pat arg_ty (emptyRefinement, res_ty) $
+ tcCmdTop cmd_env cmd []
; return (pat', cmd') }
\end{code}
---------------------------------------
tcCmdTop :: CmdEnv
-> LHsCmdTop Name
- -> (CmdStack, TcTauType) -- Expected result type; always a monotype
+ -> CmdStack
+ -> (Refinement, TcTauType) -- Expected result type; always a monotype
-- We know exactly how many cmd args are expected,
-- albeit perhaps not their types; so we can pass
-- in a CmdStack
-> TcM (LHsCmdTop TcId)
-tcCmdTop env (L loc (HsCmdTop cmd _ _ names)) (cmd_stk, res_ty)
+tcCmdTop env (L loc (HsCmdTop cmd _ _ names)) cmd_stk reft_res_ty@(_,res_ty)
= setSrcSpan loc $
- do { cmd' <- tcCmd env cmd (cmd_stk, res_ty)
+ do { cmd' <- tcGuardedCmd env cmd cmd_stk reft_res_ty
; names' <- mapM (tcSyntaxName ProcOrigin (cmd_arr env)) names
; return (L loc $ HsCmdTop cmd' cmd_stk res_ty names') }
----------------------------------------
+tcGuardedCmd :: CmdEnv -> LHsExpr Name -> CmdStack
+ -> (Refinement, TcTauType) -> TcM (LHsExpr TcId)
+-- A wrapper that deals with the refinement (if any)
+tcGuardedCmd env expr stk (reft, res_ty)
+ = do { let (co, res_ty') = refineResType reft res_ty
+ ; body <- tcCmd env expr (stk, res_ty')
+ ; return (mkLHsCoerce co body) }
+
tcCmd :: CmdEnv -> LHsExpr Name -> (CmdStack, TcTauType) -> TcM (LHsExpr TcId)
-- The main recursive function
tcCmd env (L loc expr) res_ty
where
match_ctxt = MC { mc_what = CaseAlt,
mc_body = mc_body }
- mc_body body res_ty' = tcCmd env body (stk, res_ty')
+ mc_body body res_ty' = tcGuardedCmd env body stk res_ty'
tc_cmd env (HsIf pred b1 b2) res_ty
= do { pred' <- tcMonoExpr pred boolTy
-------------------------------------------
-- Lambda
--- gaw 2004
tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats maybe_rhs_sig grhss))] _))
(cmd_stk, res_ty)
= addErrCtxt (matchCtxt match_ctxt match) $
-- Check the patterns, and the GRHSs inside
; (pats', grhss') <- setSrcSpan mtch_loc $
- tcPats LamPat pats cmd_stk res_ty $
+ tcLamPats pats cmd_stk res_ty $
tc_grhss grhss
; let match' = L mtch_loc (Match pats' Nothing grhss')
; return (GRHSs grhss' binds') }
tc_grhs res_ty (GRHS guards body)
- = do { (guards', rhs') <- tcStmts pg_ctxt tcGuardStmt
- guards res_ty
- (\res_ty' -> tcCmd env body (stk', res_ty'))
+ = do { (guards', rhs') <- tcStmts pg_ctxt tcGuardStmt guards res_ty $
+ tcGuardedCmd env body stk'
; return (GRHS guards' rhs') }
-------------------------------------------
tc_cmd env cmd@(HsDo do_or_lc stmts body ty) (cmd_stk, res_ty)
= do { checkTc (null cmd_stk) (nonEmptyCmdStkErr cmd)
- ; (stmts', body') <- tcStmts do_or_lc tc_stmt stmts res_ty $ \ res_ty' ->
- tcCmd env body ([], res_ty')
+ ; (stmts', body') <- tcStmts do_or_lc tc_stmt stmts (emptyRefinement, res_ty) $
+ tcGuardedCmd env body []
; return (HsDo do_or_lc stmts' body' res_ty) }
where
tc_stmt = tcMDoStmt tc_rhs
-- the s1..sm and check each cmd
; cmds' <- mapM (tc_cmd w_tv) cmds_w_tys
- ; returnM (HsArrForm (mkHsTyLam [w_tv] (mkHsDictLet inst_binds expr')) fixity cmds')
+ ; returnM (HsArrForm (noLoc $ HsCoerce (CoTyLams [w_tv])
+ (unLoc $ mkHsDictLet inst_binds expr'))
+ fixity cmds')
}
where
-- Make the types
new_cmd_ty :: LHsCmdTop Name -> Int
-> TcM (LHsCmdTop Name, Int, TcType, TcType, TcType)
new_cmd_ty cmd i
--- gaw 2004 FIX?
= do { b_ty <- newFlexiTyVarTy arrowTyConKind
; tup_ty <- newFlexiTyVarTy liftedTypeKind
-- We actually make a type variable for the tuple
not (w_tv `elemVarSet` tyVarsOfTypes arg_tys))
(badFormFun i tup_ty')
- ; tcCmdTop (env { cmd_arr = b }) cmd (arg_tys, s) }
+ ; tcCmdTop (env { cmd_arr = b }) cmd arg_tys (emptyRefinement, s) }
unscramble :: TcType -> (TcType, [TcType])
-- unscramble ((w,s1) .. sn) = (w, [s1..sn])
import TcRnMonad
import Inst ( newDictsAtLoc, newIPDict, instToId )
import TcEnv ( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2,
- pprBinders, tcLookupLocalId_maybe, tcLookupId,
+ pprBinders, tcLookupId,
tcGetGlobalTyVars )
import TcUnify ( tcInfer, tcSubExp, unifyTheta,
bleatEscapedTvs, sigCtxt )
import TcSimplify ( tcSimplifyInfer, tcSimplifyInferCheck,
tcSimplifyRestricted, tcSimplifyIPs )
import TcHsType ( tcHsSigType, UserTypeCtxt(..) )
-import TcPat ( tcPat, PatCtxt(..) )
+import TcPat ( tcLetPat )
import TcSimplify ( bindInstsOfLocalFuns )
import TcMType ( newFlexiTyVarTy, zonkQuantifiedTyVar, zonkSigTyVar,
tcInstSigTyVars, tcInstSkolTyVars, tcInstType,
mkTyVarTy, mkForAllTys, mkFunTys, exactTyVarsOfType,
mkForAllTy, isUnLiftedType, tcGetTyVar,
mkTyVarTys, tidyOpenTyVar )
-import Kind ( argTypeKind )
+import {- Kind parts of -} Type ( argTypeKind )
import VarEnv ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv )
-import TysWiredIn ( unitTy )
import TysPrim ( alphaTyVar )
import Id ( Id, mkLocalId, mkVanillaGlobal )
import IdInfo ( vanillaIdInfo )
in
-- SET UP THE MAIN RECOVERY; take advantage of any type sigs
setSrcSpan loc $
- recoverM (recoveryCode binder_names) $ do
+ recoverM (recoveryCode binder_names sig_fn) $ do
{ traceTc (ptext SLIT("------------------------------------------------"))
; traceTc (ptext SLIT("Bindings for") <+> ppr binder_names)
-- If typechecking the binds fails, then return with each
-- signature-less binder given type (forall a.a), to minimise
-- subsequent error messages
-recoveryCode binder_names
+recoveryCode binder_names sig_fn
= do { traceTc (text "tcBindsWithSigs: error recovery" <+> ppr binder_names)
; poly_ids <- mapM mk_dummy binder_names
; return ([], poly_ids) }
where
- mk_dummy name = do { mb_id <- tcLookupLocalId_maybe name
- ; case mb_id of
- Just id -> return id -- Had signature, was in envt
- Nothing -> return (mkLocalId name forall_a_a) } -- No signature
+ mk_dummy name
+ | isJust (sig_fn name) = tcLookupId name -- Had signature; look it up
+ | otherwise = return (mkLocalId name forall_a_a) -- No signature
forall_a_a :: TcType
forall_a_a = mkForAllTy alphaTyVar (mkTyVarTy alphaTyVar)
| (name, Just sig) <- nm_sig_prs]
sig_tau_fn = lookupNameEnv tau_sig_env
- tc_pat exp_ty = tcPat (LetPat sig_tau_fn) pat exp_ty unitTy $ \ _ ->
+ tc_pat exp_ty = tcLetPat sig_tau_fn pat exp_ty $
mapM lookup_info nm_sig_prs
- -- The unitTy is a bit bogus; it's the "result type" for lookup_info.
-- After typechecking the pattern, look up the binder
-- names, which the pattern has brought into scope.
import RdrName ( RdrName )
import Name ( Name, getSrcLoc )
import NameSet ( duDefs )
-import Kind ( splitKindFunTys )
+import Type ( splitKindFunTys )
import TyCon ( tyConTyVars, tyConDataCons, tyConArity, tyConHasGenerics,
tyConStupidTheta, isProductTyCon, isDataTyCon, newTyConRhs,
isEnumerationTyCon, isRecursiveTyCon, TyCon
)
import TcType ( TcType, ThetaType, mkTyVarTys, mkTyConApp, tcTyConAppTyCon,
isUnLiftedType, mkClassPred, tyVarsOfType,
- isArgTypeKind, tcEqTypes, tcSplitAppTys, mkAppTys )
+ isSubArgTypeKind, tcEqTypes, tcSplitAppTys, mkAppTys )
import Var ( TyVar, tyVarKind, varName )
import VarSet ( mkVarSet, subVarSet )
import PrelNames
-- (b) 7 or fewer args
cond_typeableOK (gla_exts, tycon)
| tyConArity tycon > 7 = Just too_many
- | not (all (isArgTypeKind . tyVarKind) (tyConTyVars tycon)) = Just bad_kind
+ | not (all (isSubArgTypeKind . tyVarKind) (tyConTyVars tycon)) = Just bad_kind
| otherwise = Nothing
where
too_many = quotes (ppr tycon) <+> ptext SLIT("has too many arguments")
tcExtendKindEnv, tcExtendKindEnvTvs,
tcExtendTyVarEnv, tcExtendTyVarEnv2,
tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2,
- tcLookup, tcLookupLocated, tcLookupLocalIds, tcLookupLocalId_maybe,
+ tcLookup, tcLookupLocated, tcLookupLocalIds,
tcLookupId, tcLookupTyVar, getScopedTyVarBinds,
lclEnvElts, getInLocalScope, findGlobals,
wrongThingErr, pprBinders,
#include "HsVersions.h"
import HsSyn ( LRuleDecl, LHsBinds, LSig,
- LHsTyVarBndr, HsTyVarBndr(..), pprLHsBinds )
+ LHsTyVarBndr, HsTyVarBndr(..), pprLHsBinds,
+ ExprCoFn(..), idCoercion, (<.>) )
import TcIface ( tcImportDecl )
import IfaceEnv ( newGlobalBinder )
import TcRnMonad
getDFunTyKey, tcTyConAppTyCon, tcGetTyVar, mkTyVarTy,
tidyOpenType, isRefineableTy
)
+import TcGadt ( Refinement, refineType )
import qualified Type ( getTyVar_maybe )
import Id ( idName, isLocalId, setIdType )
import Var ( TyVar, Id, idType, tyVarName )
other -> pprPanic "tcLookupTyVar" (ppr name)
tcLookupId :: Name -> TcM Id
--- Used when we aren't interested in the binding level
--- Never a DataCon. (Why does that matter? see TcExpr.tcId)
+-- Used when we aren't interested in the binding level, nor refinement.
+-- The "no refinement" part means that we return the un-refined Id regardless
+--
+-- The Id is never a DataCon. (Why does that matter? see TcExpr.tcId)
tcLookupId name
= tcLookup name `thenM` \ thing ->
case thing of
- ATcId tc_id _ _ -> returnM tc_id
- AGlobal (AnId id) -> returnM id
- other -> pprPanic "tcLookupId" (ppr name)
-
-tcLookupLocalId_maybe :: Name -> TcM (Maybe Id)
-tcLookupLocalId_maybe name
- = getLclEnv `thenM` \ local_env ->
- case lookupNameEnv (tcl_env local_env) name of
- Just (ATcId tc_id _ _) -> return (Just tc_id)
- other -> return Nothing
+ ATcId { tct_id = id} -> returnM id
+ AGlobal (AnId id) -> returnM id
+ other -> pprPanic "tcLookupId" (ppr name)
tcLookupLocalIds :: [Name] -> TcM [TcId]
-- We expect the variables to all be bound, and all at
where
lookup lenv lvl name
= case lookupNameEnv lenv name of
- Just (ATcId id lvl1 _) -> ASSERT( lvl == lvl1 ) id
- other -> pprPanic "tcLookupLocalIds" (ppr name)
+ Just (ATcId { tct_id = id, tct_level = lvl1 })
+ -> ASSERT( lvl == lvl1 ) id
+ other -> pprPanic "tcLookupLocalIds" (ppr name)
lclEnvElts :: TcLclEnv -> [TcTyThing]
lclEnvElts env = nameEnvElts (tcl_env env)
let
extra_global_tyvars = tcTyVarsOfTypes [idType id | (_,id) <- names_w_ids]
th_lvl = thLevel (tcl_th_ctxt env)
- extra_env = [ (name, ATcId id th_lvl (isRefineableTy (idType id)))
- | (name,id) <- names_w_ids]
+ extra_env = [ (name, ATcId { tct_id = id,
+ tct_level = th_lvl,
+ tct_type = id_ty,
+ tct_co = if isRefineableTy id_ty
+ then Just idCoercion
+ else Nothing })
+ | (name,id) <- names_w_ids, let id_ty = idType id]
le' = extendNameEnvList (tcl_env env) extra_env
rdr_env' = extendLocalRdrEnv (tcl_rdr env) [name | (name,_) <- names_w_ids]
in
ignore_it ty = not (tvs `intersectsVarSet` tyVarsOfType ty)
-----------------------
-find_thing ignore_it tidy_env (ATcId id _ _)
+find_thing ignore_it tidy_env (ATcId { tct_id = id })
= zonkTcType (idType id) `thenM` \ id_ty ->
if ignore_it id_ty then
returnM (tidy_env, Nothing)
\end{code}
\begin{code}
-refineEnvironment :: TvSubst -> TcM a -> TcM a
+refineEnvironment :: Refinement -> TcM a -> TcM a
+-- I don't think I have to refine the set of global type variables in scope
+-- Reason: the refinement never increases that set
refineEnvironment reft thing_inside
= do { env <- getLclEnv
; let le' = mapNameEnv refine (tcl_env env)
- ; gtvs' <- refineGlobalTyVars reft (tcl_tyvars env)
- ; setLclEnv (env {tcl_env = le', tcl_tyvars = gtvs'}) thing_inside }
+ ; setLclEnv (env {tcl_env = le'}) thing_inside }
where
- refine (ATcId id lvl True) = ATcId (setIdType id (substTy reft (idType id))) lvl True
- refine (ATyVar tv ty) = ATyVar tv (substTy reft ty)
- refine elt = elt
+ refine elt@(ATcId { tct_co = Just co, tct_type = ty })
+ = let (co', ty') = refineType reft ty
+ in elt { tct_co = Just (co' <.> co), tct_type = ty' }
+ refine (ATyVar tv ty) = ATyVar tv (snd (refineType reft ty))
+ -- Ignore the coercion that refineType returns
+ refine elt = elt
\end{code}
%************************************************************************
tc_extend_gtvs gtvs extra_global_tvs
= readMutVar gtvs `thenM` \ global_tvs ->
newMutVar (global_tvs `unionVarSet` extra_global_tvs)
-
-refineGlobalTyVars :: GadtRefinement -> TcRef TcTyVarSet -> TcM (TcRef TcTyVarSet)
-refineGlobalTyVars reft gtv_var
- = readMutVar gtv_var `thenM` \ gbl_tvs ->
- newMutVar (tcTyVarsOfTypes (map (substTyVar reft) (varSetElems gbl_tvs)))
\end{code}
@tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
#endif
import HsSyn ( HsExpr(..), LHsExpr, ArithSeqInfo(..), recBindFields,
- HsMatchContext(..), HsRecordBinds,
- mkHsCoerce, mkHsApp, mkHsDictApp, mkHsTyApp )
+ HsMatchContext(..), HsRecordBinds, mkHsCoerce,
+ mkHsApp )
import TcHsSyn ( hsLitType )
import TcRnMonad
import TcUnify ( tcInfer, tcSubExp, tcFunResTy, tcGen, boxyUnify, subFunTys, zapToMonotype, stripBoxyType,
boxySplitListTy, boxySplitTyConApp, wrapFunResCoercion, preSubType,
unBox )
import BasicTypes ( Arity, isMarkedStrict )
-import Inst ( newMethodFromName, newIPDict, instToId,
+import Inst ( newMethodFromName, newIPDict, mkInstCoFn,
newDicts, newMethodWithGivenTy, tcInstStupidTheta )
import TcBinds ( tcLocalBinds )
-import TcEnv ( tcLookup, tcLookupId, tcLookupDataCon, tcLookupField )
+import TcEnv ( tcLookup, tcLookupDataCon, tcLookupField )
import TcArrows ( tcProc )
-import TcMatches ( tcMatchesCase, tcMatchLambda, tcDoStmts, TcMatchCtxt(..) )
+import TcMatches ( tcMatchesCase, tcMatchLambda, tcDoStmts, tcBody,
+ TcMatchCtxt(..) )
import TcHsType ( tcHsSigType, UserTypeCtxt(..) )
import TcPat ( tcOverloadedLit, badFieldCon )
-import TcMType ( tcInstTyVars, newFlexiTyVarTy, newBoxyTyVars, readFilledBox, zonkTcTypes )
-import TcType ( TcType, TcSigmaType, TcRhoType,
+import TcMType ( tcInstTyVars, newFlexiTyVarTy, newBoxyTyVars,
+ readFilledBox, zonkTcTypes )
+import TcType ( TcType, TcSigmaType, TcRhoType, TvSubst,
BoxySigmaType, BoxyRhoType, ThetaType,
mkTyVarTys, mkFunTys,
- tcMultiSplitSigmaTy, tcSplitFunTysN, tcSplitTyConApp_maybe,
+ tcMultiSplitSigmaTy, tcSplitFunTysN,
+ tcSplitTyConApp_maybe,
isSigmaTy, mkFunTy, mkTyConApp, isLinearPred,
exactTyVarsOfType, exactTyVarsOfTypes,
zipTopTvSubst, zipOpenTvSubst, substTys, substTyVar
)
-import Kind ( argTypeKind )
-
-import Id ( Id, idType, idName, recordSelectorFieldLabel,
- isRecordSelector, isNaughtyRecordSelector, isDataConId_maybe )
-import DataCon ( DataCon, dataConFieldLabels, dataConStrictMarks, dataConSourceArity,
- dataConWrapId, isVanillaDataCon, dataConTyVars, dataConOrigArgTys )
+import {- Kind parts of -}
+ Type ( argTypeKind )
+
+import Id ( Id, idType, recordSelectorFieldLabel,
+ isRecordSelector, isNaughtyRecordSelector,
+ isDataConId_maybe )
+import DataCon ( DataCon, dataConFieldLabels, dataConStrictMarks,
+ dataConSourceArity,
+ dataConWrapId, isVanillaDataCon, dataConUnivTyVars,
+ dataConOrigArgTys )
import Name ( Name )
-import TyCon ( FieldLabel, tyConStupidTheta, tyConDataCons, isEnumerationTyCon )
+import TyCon ( FieldLabel, tyConStupidTheta, tyConDataCons,
+ isEnumerationTyCon )
import Type ( substTheta, substTy )
import Var ( TyVar, tyVarKind )
import VarSet ( emptyVarSet, elemVarSet, unionVarSet )
import DynFlags
import StaticFlags ( opt_NoMethodSharing )
import HscTypes ( TyThing(..) )
-import SrcLoc ( Located(..), unLoc, noLoc, getLoc )
+import SrcLoc ( Located(..), unLoc, getLoc )
import Util
import ListSetOps ( assocMaybe )
import Maybes ( catMaybes )
; return (HsCase scrut' matches') }
where
match_ctxt = MC { mc_what = CaseAlt,
- mc_body = tcPolyExpr }
+ mc_body = tcBody }
tcExpr (HsIf pred b1 b2) res_ty
= do { pred' <- addErrCtxt (predCtxt pred) $
-- A constructor is only relevant to this process if
-- it contains *all* the fields that are being updated
con1 = head relevant_cons -- A representative constructor
- con1_tyvars = dataConTyVars con1
+ con1_tyvars = dataConUnivTyVars con1
con1_flds = dataConFieldLabels con1
con1_arg_tys = dataConOrigArgTys con1
common_tyvars = exactTyVarsOfTypes [ty | (fld,ty) <- con1_flds `zip` con1_arg_tys
-- Then fres <= bx_(k+1) -> ... -> bx_n -> res_ty
tcIdApp fun_name n_args arg_checker res_ty
- = do { fun_id <- lookupFun (OccurrenceOf fun_name) fun_name
+ = do { let orig = OccurrenceOf fun_name
+ ; (fun, fun_ty) <- lookupFun orig fun_name
-- Split up the function type
- ; let (tv_theta_prs, rho) = tcMultiSplitSigmaTy (idType fun_id)
+ ; let (tv_theta_prs, rho) = tcMultiSplitSigmaTy fun_ty
(fun_arg_tys, fun_res_ty) = tcSplitFunTysN rho n_args
qtvs = concatMap fst tv_theta_prs -- Quantified tyvars
-- And pack up the results
-- By applying the coercion just to the *function* we can make
-- tcFun work nicely for OpApp and Sections too
- ; fun' <- instFun fun_id qtvs qtys'' tv_theta_prs
+ ; fun' <- instFun orig fun res_subst tv_theta_prs
; co_fn' <- wrapFunResCoercion fun_arg_tys' co_fn
; return (mkHsCoerce co_fn' fun', args') }
\end{code}
-> TcM (HsExpr TcId)
tcId orig fun_name res_ty
= do { traceTc (text "tcId" <+> ppr fun_name <+> ppr res_ty)
- ; fun_id <- lookupFun orig fun_name
+ ; (fun, fun_ty) <- lookupFun orig fun_name
-- Split up the function type
- ; let (tv_theta_prs, fun_tau) = tcMultiSplitSigmaTy (idType fun_id)
+ ; let (tv_theta_prs, fun_tau) = tcMultiSplitSigmaTy fun_ty
qtvs = concatMap fst tv_theta_prs -- Quantified tyvars
tau_qtvs = exactTyVarsOfType fun_tau -- Mentioned in the tau part
; qtv_tys <- preSubType qtvs tau_qtvs fun_tau res_ty
; co_fn <- tcFunResTy fun_name fun_tau' res_ty
-- And pack up the results
- ; fun' <- instFun fun_id qtvs qtv_tys tv_theta_prs
+ ; fun' <- instFun orig fun res_subst tv_theta_prs
; return (mkHsCoerce co_fn fun') }
-- Note [Push result type in]
tcSyntaxOp orig other ty = pprPanic "tcSyntaxOp" (ppr other)
---------------------------
-instFun :: TcId
- -> [TyVar] -> [TcType] -- Quantified type variables and
- -- their instantiating types
- -> [([TyVar], ThetaType)] -- Stuff to instantiate
+instFun :: InstOrigin
+ -> HsExpr TcId
+ -> TvSubst -- The instantiating substitution
+ -> [([TyVar], ThetaType)] -- Stuff to instantiate
-> TcM (HsExpr TcId)
-instFun fun_id qtvs qtv_tys []
- = return (HsVar fun_id) -- Common short cut
-instFun fun_id qtvs qtv_tys tv_theta_prs
- = do { -- Horrid check for tagToEnum; see Note [tagToEnum#]
- checkBadTagToEnumCall fun_id qtv_tys
+instFun orig fun subst []
+ = return fun -- Common short cut
- ; let subst = zipOpenTvSubst qtvs qtv_tys
- ty_theta_prs' = map subst_pr tv_theta_prs
- subst_pr (tvs, theta) = (map (substTyVar subst) tvs,
- substTheta subst theta)
+instFun orig fun subst tv_theta_prs
+ = do {-- !!!SPJ: -- Horrid check for tagToEnum; see Note [tagToEnum#]
+ -- !!!SPJ: checkBadTagToEnumCall fun_id qtv_tys
+
+ ; let ty_theta_prs' = map subst_pr tv_theta_prs
- -- The ty_theta_prs' is always non-empty
- ((tys1',theta1') : further_prs') = ty_theta_prs'
-
-- First, chuck in the constraints from
-- the "stupid theta" of a data constructor (sigh)
- ; case isDataConId_maybe fun_id of
- Just con -> tcInstStupidTheta con tys1'
- Nothing -> return ()
-
- ; if want_method_inst theta1'
- then do { meth_id <- newMethodWithGivenTy orig fun_id tys1'
- -- See Note [Multiple instantiation]
- ; go (HsVar meth_id) further_prs' }
- else go (HsVar fun_id) ty_theta_prs'
- }
+ ; inst_stupid fun ty_theta_prs'
+
+ -- Now do normal instantiation
+ ; go True fun ty_theta_prs' }
where
- orig = OccurrenceOf (idName fun_id)
+ subst_pr (tvs, theta)
+ = (map (substTyVar subst) tvs, substTheta subst theta)
+
+ inst_stupid (HsVar fun_id) ((tys,_):_)
+ | Just con <- isDataConId_maybe fun_id = tcInstStupidTheta con tys
+ inst_stupid _ _ = return ()
+
+ go _ fun [] = return fun
- go fun [] = return fun
+ go True (HsVar fun_id) ((tys,theta) : prs)
+ | want_method_inst theta
+ = do { meth_id <- newMethodWithGivenTy orig fun_id tys
+ ; go False (HsVar meth_id) prs }
+ -- Go round with 'False' to prevent further use
+ -- of newMethod: see Note [Multiple instantiation]
- go fun ((tys, theta) : prs)
+ go _ fun ((tys, theta) : prs)
= do { dicts <- newDicts orig theta
; extendLIEs dicts
- ; let the_app = unLoc $ mkHsDictApp (mkHsTyApp (noLoc fun) tys)
- (map instToId dicts)
- ; go the_app prs }
+ ; let co_fn = mkInstCoFn tys dicts
+ ; go False (HsCoerce co_fn fun) prs }
-- Hack Alert (want_method_inst)!
-- See Note [No method sharing]
%************************************************************************
\begin{code}
-lookupFun :: InstOrigin -> Name -> TcM TcId
+lookupFun :: InstOrigin -> Name -> TcM (HsExpr TcId, TcType)
lookupFun orig id_name
= do { thing <- tcLookup id_name
; case thing of
- AGlobal (ADataCon con) -> return (dataConWrapId con)
+ AGlobal (ADataCon con) -> return (HsVar wrap_id, idType wrap_id)
+ where
+ wrap_id = dataConWrapId con
AGlobal (AnId id)
| isNaughtyRecordSelector id -> failWithTc (naughtyRecordSel id)
- | otherwise -> return id
+ | otherwise -> return (HsVar id, idType id)
-- A global cannot possibly be ill-staged
-- nor does it need the 'lifting' treatment
-#ifndef GHCI
- ATcId id th_level _ -> return id -- Non-TH case
-#else
- ATcId id th_level _ -> do { use_stage <- getStage -- TH case
- ; thLocalId orig id_name id th_level use_stage }
-#endif
+ ATcId { tct_id = id, tct_type = ty, tct_co = mb_co, tct_level = lvl }
+ -> do { thLocalId orig id ty lvl
+ ; case mb_co of
+ Nothing -> return (HsVar id, ty) -- Wobbly, or no free vars
+ Just co -> return (mkHsCoerce co (HsVar id), ty) }
other -> failWithTc (ppr other <+> ptext SLIT("used where a value identifer was expected"))
}
-#ifdef GHCI /* GHCI and TH is on */
+#ifndef GHCI /* GHCI and TH is off */
--------------------------------------
-- thLocalId : Check for cross-stage lifting
+thLocalId orig id id_ty th_bind_lvl
+ = return ()
+
+#else /* GHCI and TH is on */
+thLocalId orig id id_ty th_bind_lvl
+ = do { use_stage <- getStage -- TH case
+ ; case use_stage of
+ Brack use_lvl ps_var lie_var | use_lvl > th_bind_lvl
+ -> thBrackId orig id ps_var lie_var
+ other -> checkWellStaged (quotes (ppr id)) th_bind_lvl use_stage
+ }
+
thLocalId orig id_name id th_bind_lvl (Brack use_lvl ps_var lie_var)
| use_lvl > th_bind_lvl
- = thBrackId orig id_name id ps_var lie_var
+ = thBrackId
thLocalId orig id_name id th_bind_lvl use_stage
- = do { checkWellStaged (quotes (ppr id)) th_bind_lvl use_stage
+ = do { checkWellStaged
; return id }
--------------------------------------
-thBrackId orig id_name id ps_var lie_var
+thBrackId orig id ps_var lie_var
| isExternalName id_name
= -- Top-level identifiers in this module,
-- (which have External Names)
; writeMutVar ps_var ((id_name, nlHsApp (nlHsVar lift) (nlHsVar id)) : ps)
; return id } }
+ where
+ id_name = idName id
#endif /* GHCI */
\end{code}
| Just field_ty <- assocMaybe flds_w_tys field_lbl
= addErrCtxt (fieldCtxt field_lbl) $
do { rhs' <- tcPolyExprNC rhs field_ty
- ; sel_id <- tcLookupId field_lbl
+ ; sel_id <- tcLookupField field_lbl
; ASSERT( isRecordSelector sel_id )
return (Just (L loc sel_id, rhs')) }
| otherwise
\begin{code}
module TcHsSyn (
- mkHsTyApp, mkHsDictApp, mkHsConApp,
- mkHsTyLam, mkHsDictLam, mkHsDictLet, mkHsApp,
- hsLitType, hsPatType, mkHsAppTy, mkSimpleHsAlt,
+ mkHsConApp, mkHsDictLet, mkHsApp,
+ hsLitType, hsLPatType, hsPatType,
+ mkHsAppTy, mkSimpleHsAlt,
nlHsIntLit, mkVanillaTuplePat,
import Id ( idType, setIdType, Id )
import TcRnMonad
-import Type ( Type )
+import Type ( Type, isLiftedTypeKind, liftedTypeKind, isSubKind, eqKind )
import TcType ( TcType, TcTyVar, mkTyVarTy, mkTyConApp, isImmutableTyVar )
-import Kind ( isLiftedTypeKind, liftedTypeKind, isSubKind )
import qualified Type
import TcMType ( zonkQuantifiedTyVar, zonkType, zonkTcType, writeMetaTyVar )
import TysPrim ( charPrimTy, intPrimTy, floatPrimTy,
mkListTy, mkPArrTy, mkTupleTy, unitTy,
voidTy, listTyCon, tupleTyCon )
import TyCon ( mkPrimTyCon, tyConKind, PrimRep(..) )
-import Kind ( splitKindFunTys )
+import {- Kind parts of -} Type ( splitKindFunTys )
import Name ( Name, getOccName, mkInternalName, mkDerivedTyConOcc )
import Var ( Var, isId, isLocalVar, tyVarKind )
import VarSet
%* *
%************************************************************************
-Note: If @hsPatType@ doesn't bear a strong resemblance to @exprType@,
+Note: If @hsLPatType@ doesn't bear a strong resemblance to @exprType@,
then something is wrong.
\begin{code}
mkVanillaTuplePat :: [OutPat Id] -> Boxity -> Pat Id
-- A vanilla tuple pattern simply gets its type from its sub-patterns
mkVanillaTuplePat pats box
- = TuplePat pats box (mkTupleTy box (length pats) (map hsPatType pats))
-
-hsPatType :: OutPat Id -> Type
-hsPatType (L _ pat) = pat_type pat
-
-pat_type (ParPat pat) = hsPatType pat
-pat_type (WildPat ty) = ty
-pat_type (VarPat var) = idType var
-pat_type (VarPatOut var _) = idType var
-pat_type (BangPat pat) = hsPatType pat
-pat_type (LazyPat pat) = hsPatType pat
-pat_type (LitPat lit) = hsLitType lit
-pat_type (AsPat var pat) = idType (unLoc var)
-pat_type (ListPat _ ty) = mkListTy ty
-pat_type (PArrPat _ ty) = mkPArrTy ty
-pat_type (TuplePat pats box ty) = ty
-pat_type (ConPatOut _ _ _ _ _ ty) = ty
-pat_type (SigPatOut pat ty) = ty
-pat_type (NPat lit _ _ ty) = ty
-pat_type (NPlusKPat id _ _ _) = idType (unLoc id)
-pat_type (DictPat ds ms) = case (ds ++ ms) of
+ = TuplePat pats box (mkTupleTy box (length pats) (map hsLPatType pats))
+
+hsLPatType :: OutPat Id -> Type
+hsLPatType (L _ pat) = hsPatType pat
+
+hsPatType (ParPat pat) = hsLPatType pat
+hsPatType (WildPat ty) = ty
+hsPatType (VarPat var) = idType var
+hsPatType (VarPatOut var _) = idType var
+hsPatType (BangPat pat) = hsLPatType pat
+hsPatType (LazyPat pat) = hsLPatType pat
+hsPatType (LitPat lit) = hsLitType lit
+hsPatType (AsPat var pat) = idType (unLoc var)
+hsPatType (ListPat _ ty) = mkListTy ty
+hsPatType (PArrPat _ ty) = mkPArrTy ty
+hsPatType (TuplePat pats box ty) = ty
+hsPatType (ConPatOut{ pat_ty = ty })= ty
+hsPatType (SigPatOut pat ty) = ty
+hsPatType (NPat lit _ _ ty) = ty
+hsPatType (NPlusKPat id _ _ _) = idType (unLoc id)
+hsPatType (CoPat _ _ ty) = ty
+hsPatType (DictPat ds ms) = case (ds ++ ms) of
[] -> unitTy
[d] -> idType d
ds -> mkTupleTy Boxed (length ds) (map idType ds)
= zonkLExpr env expr `thenM` \ new_expr ->
returnM (HsCoreAnn lbl new_expr)
-zonkExpr env (TyLam tyvars expr)
- = ASSERT( all isImmutableTyVar tyvars )
- zonkLExpr env expr `thenM` \ new_expr ->
- returnM (TyLam tyvars new_expr)
-
-zonkExpr env (TyApp expr tys)
- = zonkLExpr env expr `thenM` \ new_expr ->
- zonkTcTypeToTypes env tys `thenM` \ new_tys ->
- returnM (TyApp new_expr new_tys)
-
-zonkExpr env (DictLam dicts expr)
- = zonkIdBndrs env dicts `thenM` \ new_dicts ->
- let
- env1 = extendZonkEnv env new_dicts
- in
- zonkLExpr env1 expr `thenM` \ new_expr ->
- returnM (DictLam new_dicts new_expr)
-
-zonkExpr env (DictApp expr dicts)
- = zonkLExpr env expr `thenM` \ new_expr ->
- returnM (DictApp new_expr (zonkIdOccs env dicts))
-
-- arrow notation extensions
zonkExpr env (HsProc pat body)
= do { (env1, new_pat) <- zonkPat env pat
-------------------------------------------------------------------------
zonkCoFn :: ZonkEnv -> ExprCoFn -> TcM (ZonkEnv, ExprCoFn)
zonkCoFn env CoHole = return (env, CoHole)
+zonkCoFn env (ExprCoFn co) = do { co' <- zonkTcTypeToType env co
+ ; return (env, ExprCoFn co') }
zonkCoFn env (CoCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
; (env2, c2') <- zonkCoFn env1 c2
; return (env2, CoCompose c1' c2') }
-zonkCoFn env (CoLams ids c) = do { ids' <- zonkIdBndrs env ids
+zonkCoFn env (CoLams ids) = do { ids' <- zonkIdBndrs env ids
; let env1 = extendZonkEnv env ids'
- ; (env2, c') <- zonkCoFn env1 c
- ; return (env2, CoLams ids' c') }
-zonkCoFn env (CoTyLams tvs c) = ASSERT( all isImmutableTyVar tvs )
- do { (env1, c') <- zonkCoFn env c
- ; return (env1, CoTyLams tvs c') }
-zonkCoFn env (CoApps c ids) = do { (env1, c') <- zonkCoFn env c
- ; return (env1, CoApps c' (zonkIdOccs env ids)) }
-zonkCoFn env (CoTyApps c tys) = do { tys' <- zonkTcTypeToTypes env tys
- ; (env1, c') <- zonkCoFn env c
- ; return (env1, CoTyApps c' tys') }
-zonkCoFn env (CoLet bs c) = do { (env1, bs') <- zonkRecMonoBinds env bs
- ; (env2, c') <- zonkCoFn env1 c
- ; return (env2, CoLet bs' c') }
+ ; return (env1, CoLams ids') }
+zonkCoFn env (CoTyLams tvs) = ASSERT( all isImmutableTyVar tvs )
+ do { return (env, CoTyLams tvs) }
+zonkCoFn env (CoApps ids) = do { return (env, CoApps (zonkIdOccs env ids)) }
+zonkCoFn env (CoTyApps tys) = do { tys' <- zonkTcTypeToTypes env tys
+ ; return (env, CoTyApps tys') }
+zonkCoFn env (CoLet bs) = do { (env1, bs') <- zonkRecMonoBinds env bs
+ ; return (env1, CoLet bs') }
-------------------------------------------------------------------------
; (env', pats') <- zonkPats env pats
; return (env', TuplePat pats' boxed ty') }
-zonk_pat env (ConPatOut n tvs dicts binds stuff ty)
- = ASSERT( all isImmutableTyVar tvs )
+zonk_pat env p@(ConPatOut { pat_ty = ty, pat_dicts = dicts, pat_binds = binds, pat_args = args })
+ = ASSERT( all isImmutableTyVar (pat_tvs p) )
do { new_ty <- zonkTcTypeToType env ty
; new_dicts <- zonkIdBndrs env dicts
; let env1 = extendZonkEnv env new_dicts
; (env2, new_binds) <- zonkRecMonoBinds env1 binds
- ; (env', new_stuff) <- zonkConStuff env2 stuff
- ; returnM (env', ConPatOut n tvs new_dicts new_binds new_stuff new_ty) }
+ ; (env', new_args) <- zonkConStuff env2 args
+ ; returnM (env', p { pat_ty = new_ty, pat_dicts = new_dicts,
+ pat_binds = new_binds, pat_args = new_args }) }
zonk_pat env (LitPat lit) = return (env, LitPat lit)
kind = tyVarKind tv
(args,res) = splitKindFunTys kind
- tycon | kind == tyConKind listTyCon -- *->*
+ tycon | eqKind kind (tyConKind listTyCon) -- *->*
= listTyCon -- No tuples this size
| all isLiftedTypeKind args && isLiftedTypeKind res
substTyWith, mkTyVarTys, tcEqType,
tcIsTyVarTy, mkFunTy, mkSigmaTy, mkPredTy,
mkTyConApp, mkAppTys, typeKind )
-import Kind ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind,
+import {- Kind parts of -} Type ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind,
openTypeKind, argTypeKind, splitKindFunTys )
import Var ( TyVar, mkTyVar, tyVarName )
import TyCon ( TyCon, tyConKind )
newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
--------------------------------
+ -- Creating new coercion variables
+ newCoVars,
+
+ --------------------------------
-- Instantiation
tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
tcInstSigTyVars, zonkSigTyVar,
import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
MetaDetails(..), SkolemInfo(..), BoxInfo(..),
- BoxyTyVar, BoxyType, UserTypeCtxt(..),
- isMetaTyVar, isSigTyVar, metaTvRef,
+ BoxyTyVar, BoxyType, UserTypeCtxt(..), kindVarRef,
+ mkKindVar, isMetaTyVar, isSigTyVar, metaTvRef,
tcCmpPred, isClassPred, tcGetTyVar,
- tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
+ tcSplitPhiTy, tcSplitPredTy_maybe,
+ tcSplitAppTy_maybe,
tcValidInstHeadTy, tcSplitForAllTys,
tcIsTyVarTy, tcSplitSigmaTy,
isUnLiftedType, isIPPred,
tyVarsOfPred, getClassPredTys_maybe,
tyVarsOfType, tyVarsOfTypes, tcView,
pprPred, pprTheta, pprClassPred )
-import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar,
- isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
+import Type ( Kind, KindVar,
+ isLiftedTypeKind, isSubArgTypeKind, isSubOpenTypeKind,
liftedTypeKind, defaultKind
)
import Type ( TvSubst, zipTopTvSubst, substTy )
+import Coercion ( mkCoKind )
import Class ( Class, classArity, className )
import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
tyConArity, tyConName )
import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar,
- mkTyVar, mkTcTyVar, tcTyVarDetails )
+ mkTyVar, mkTcTyVar, tcTyVarDetails,
+ CoVar, mkCoVar )
-- Assertions
#ifdef DEBUG
import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar )
-import Kind ( isSubKind )
+import Type ( isSubKind )
#endif
-- others:
import DynFlags ( dopt, DynFlag(..) )
import Util ( nOfThem, isSingleton, notNull )
import ListSetOps ( removeDups )
+import UniqSupply ( uniqsFromSupply )
import Outputable
import Control.Monad ( when )
%************************************************************************
\begin{code}
+newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
+newCoVars spec
+ = do { us <- newUniqueSupply
+ ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
+ (mkCoKind ty1 ty2)
+ | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
+
newKindVar :: TcM TcKind
newKindVar = do { uniq <- newUnique
- ; ref <- newMutVar Nothing
- ; return (KindVar (mkKindVar uniq ref)) }
+ ; ref <- newMutVar Flexi
+ ; return (mkTyVarTy (mkKindVar uniq ref)) }
newKindVars :: Int -> TcM [TcKind]
newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
zonkTcPredType (IParam n t)
= zonkTcType t `thenM` \ new_t ->
returnM (IParam n new_t)
+zonkTcPredType (EqPred t1 t2)
+ = zonkTcType t1 `thenM` \ new_t1 ->
+ zonkTcType t2 `thenM` \ new_t2 ->
+ returnM (EqPred new_t1 new_t2)
\end{code}
------------------- These ...ToType, ...ToKind versions
go ty `thenM` \ ty' ->
returnM (ForAllTy tyvar ty')
- go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
- returnM (ClassP c tys')
- go_pred (IParam n ty) = go ty `thenM` \ ty' ->
- returnM (IParam n ty')
+ go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
+ returnM (ClassP c tys')
+ go_pred (IParam n ty) = go ty `thenM` \ ty' ->
+ returnM (IParam n ty')
+ go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' ->
+ go ty2 `thenM` \ ty2' ->
+ returnM (EqPred ty1' ty2')
zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
-> TcTyVar -> TcM TcType
%************************************************************************
\begin{code}
-readKindVar :: KindVar -> TcM (Maybe TcKind)
+readKindVar :: KindVar -> TcM (MetaDetails)
writeKindVar :: KindVar -> TcKind -> TcM ()
readKindVar kv = readMutVar (kindVarRef kv)
-writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
+writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
-------------
zonkTcKind :: TcKind -> TcM TcKind
-zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
- ; k2' <- zonkTcKind k2
- ; returnM (FunKind k1' k2') }
-zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
- ; case mb_kind of
- Nothing -> returnM k
- Just k -> zonkTcKind k }
-zonkTcKind other_kind = returnM other_kind
+zonkTcKind k = zonkTcType k
-------------
zonkTcKindToKind :: TcKind -> TcM Kind
-zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
- ; k2' <- zonkTcKindToKind k2
- ; returnM (FunKind k1' k2') }
-
-zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
- ; case mb_kind of
- Nothing -> return liftedTypeKind
- Just k -> zonkTcKindToKind k }
-
-zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
-zonkTcKindToKind other_kind = returnM other_kind
+-- When zonking a TcKind to a kind, we need to instantiate kind variables,
+-- Haskell specifies that * is to be used, so we follow that.
+zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
\end{code}
%************************************************************************
kind_ok = case ctxt of
TySynCtxt _ -> True -- Any kind will do
- ResSigCtxt -> isOpenTypeKind actual_kind
- ExprSigCtxt -> isOpenTypeKind actual_kind
+ ResSigCtxt -> isSubOpenTypeKind actual_kind
+ ExprSigCtxt -> isSubOpenTypeKind actual_kind
GenPatCtxt -> isLiftedTypeKind actual_kind
ForSigCtxt _ -> isLiftedTypeKind actual_kind
- other -> isArgTypeKind actual_kind
+ other -> isSubArgTypeKind actual_kind
ubx_tup | not gla_exts = UT_NotOk
| otherwise = case ctxt of
-- The Right Thing would be to fix the way that SPECIALISE instance pragmas
-- are handled, but the quick thing is just to permit PredTys here.
check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
- check_source_ty dflags TypeCtxt sty
+ check_pred_ty dflags TypeCtxt sty
check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
check_valid_theta ctxt theta
= getDOpts `thenM` \ dflags ->
warnTc (notNull dups) (dupPredWarn dups) `thenM_`
- mappM_ (check_source_ty dflags ctxt) theta
+ mappM_ (check_pred_ty dflags ctxt) theta
where
(_,dups) = removeDups tcCmpPred theta
-------------------------
-check_source_ty dflags ctxt pred@(ClassP cls tys)
+check_pred_ty dflags ctxt pred@(ClassP cls tys)
= -- Class predicates are valid in all contexts
checkTc (arity == n_tys) arity_err `thenM_`
arity_err = arityErr "Class" class_name arity n_tys
how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
-check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
+check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
-- Implicit parameters only allows in type
-- signatures; not in instance decls, superclasses etc
-- The reason for not allowing implicit params in instances is a bit subtle
-- instance decl would show up two uses of ?x.
-- Catch-all
-check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
+check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
-------------------------
check_class_pred_tys dflags ctxt tys
= vcat [ptext SLIT("In the context:") <+> pprTheta theta,
ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
-badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
+badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
fvPred :: PredType -> [TyVar]
fvPred (ClassP _ tys') = fvTypes tys'
fvPred (IParam _ ty) = fvType ty
+fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2
-- Size of a type: the number of variables and constructors
sizeType :: Type -> Int
sizePred :: PredType -> Int
sizePred (ClassP _ tys') = sizeTypes tys'
sizePred (IParam _ ty) = sizeType ty
+sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2
\end{code}
\begin{code}
module TcMatches ( tcMatchesFun, tcGRHSsPat, tcMatchesCase, tcMatchLambda,
matchCtxt, TcMatchCtxt(..),
- tcStmts, tcDoStmts,
+ tcStmts, tcDoStmts, tcBody,
tcDoStmt, tcMDoStmt, tcGuardStmt
) where
import HsSyn ( HsExpr(..), LHsExpr, MatchGroup(..),
Match(..), LMatch, GRHSs(..), GRHS(..),
- Stmt(..), LStmt, HsMatchContext(..), HsStmtContext(..),
+ Stmt(..), LStmt, HsMatchContext(..),
+ HsStmtContext(..),
pprMatch, isIrrefutableHsPat, mkHsCoerce,
- pprMatchContext, pprStmtContext,
+ mkLHsCoerce, pprMatchContext, pprStmtContext,
noSyntaxExpr, matchGroupArity, pprMatches,
ExprCoFn )
import TcRnMonad
+import TcGadt ( Refinement, emptyRefinement, refineResType )
import Inst ( newMethodFromName )
import TcEnv ( TcId, tcLookupLocalIds, tcLookupId, tcExtendIdEnv )
-import TcPat ( PatCtxt(..), tcPats, tcPat )
+import TcPat ( tcLamPats, tcLamPat )
import TcMType ( newFlexiTyVarTy, newFlexiTyVarTys )
import TcType ( TcType, TcRhoType,
BoxySigmaType, BoxyRhoType,
import TyCon ( TyCon )
import Outputable
import SrcLoc ( Located(..), getLoc )
-import ErrUtils ( Message )
\end{code}
%************************************************************************
doc = ptext SLIT("The equation(s) for") <+> quotes (ppr fun_name)
<+> ptext SLIT("have") <+> speakNOf n_pats (ptext SLIT("argument"))
n_pats = matchGroupArity matches
- match_ctxt = MC { mc_what = FunRhs fun_name, mc_body = tcPolyExpr }
+ match_ctxt = MC { mc_what = FunRhs fun_name, mc_body = tcBody }
\end{code}
@tcMatchesCase@ doesn't do the argument-count check because the
-- The pprSetDepth makes the abstraction print briefly
ptext SLIT("has") <+> speakNOf n_pats (ptext SLIT("argument"))]
match_ctxt = MC { mc_what = LambdaExpr,
- mc_body = tcPolyExpr }
+ mc_body = tcBody }
\end{code}
@tcGRHSsPat@ typechecks @[GRHSs]@ that occur in a @PatMonoBind@.
\begin{code}
tcGRHSsPat :: GRHSs Name -> BoxyRhoType -> TcM (GRHSs TcId)
-tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss res_ty
+-- Used for pattern bindings
+tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss (emptyRefinement, res_ty)
+ -- emptyRefinement: no refinement in a pattern binding
where
match_ctxt = MC { mc_what = PatBindRhs,
- mc_body = tcPolyExpr }
+ mc_body = tcBody }
\end{code}
data TcMatchCtxt -- c.f. TcStmtCtxt, also in this module
= MC { mc_what :: HsMatchContext Name, -- What kind of thing this is
mc_body :: LHsExpr Name -- Type checker for a body of an alternative
- -> BoxyRhoType
+ -> (Refinement, BoxyRhoType)
-> TcM (LHsExpr TcId) }
tcMatches ctxt pat_tys rhs_ty (MatchGroup matches _)
where
tc_match ctxt pat_tys rhs_ty match@(Match pats maybe_rhs_sig grhss)
= addErrCtxt (matchCtxt (mc_what ctxt) match) $
- do { (pats', grhss') <- tcPats LamPat pats pat_tys rhs_ty $
+ do { (pats', grhss') <- tcLamPats pats pat_tys rhs_ty $
tc_grhss ctxt maybe_rhs_sig grhss
; return (Match pats' Nothing grhss') }
= tcGRHSs ctxt grhss rhs_ty -- No result signature
-- Result type sigs are no longer supported
- tc_grhss ctxt (Just res_sig) grhss rhs_ty
+ tc_grhss ctxt (Just res_sig) grhss (co,rhs_ty)
= do { addErr (ptext SLIT("Ignoring (deprecated) result type signature")
<+> ppr res_sig)
- ; tcGRHSs ctxt grhss rhs_ty }
+ tcGRHSs ctxt grhss (co, inner_ty) }
-------------
-tcGRHSs :: TcMatchCtxt -> GRHSs Name -> BoxyRhoType -> TcM (GRHSs TcId)
+tcGRHSs :: TcMatchCtxt -> GRHSs Name -> (Refinement, BoxyRhoType)
+ -> TcM (GRHSs TcId)
-- Notice that we pass in the full res_ty, so that we get
-- good inference from simple things like
; returnM (GRHSs grhss' binds') }
-------------
-tcGRHS :: TcMatchCtxt -> BoxyRhoType -> GRHS Name -> TcM (GRHS TcId)
+tcGRHS :: TcMatchCtxt -> (Refinement, BoxyRhoType) -> GRHS Name -> TcM (GRHS TcId)
tcGRHS ctxt res_ty (GRHS guards rhs)
= do { (guards', rhs') <- tcStmts stmt_ctxt tcGuardStmt guards res_ty $
-> TcM (HsExpr TcId) -- Returns a HsDo
tcDoStmts ListComp stmts body res_ty
= do { elt_ty <- boxySplitListTy res_ty
- ; (stmts', body') <- tcStmts ListComp (tcLcStmt listTyCon) stmts elt_ty $
- tcBody (doBodyCtxt ListComp body) body
+ ; (stmts', body') <- tcStmts ListComp (tcLcStmt listTyCon) stmts
+ (emptyRefinement,elt_ty) $
+ tcBody body
; return (HsDo ListComp stmts' body' (mkListTy elt_ty)) }
tcDoStmts PArrComp stmts body res_ty
= do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty
- ; (stmts', body') <- tcStmts PArrComp (tcLcStmt parrTyCon) stmts elt_ty $
- tcBody (doBodyCtxt PArrComp body) body
+ ; (stmts', body') <- tcStmts PArrComp (tcLcStmt parrTyCon) stmts
+ (emptyRefinement, elt_ty) $
+ tcBody body
; return (HsDo PArrComp stmts' body' (mkPArrTy elt_ty)) }
tcDoStmts DoExpr stmts body res_ty
= do { (m_ty, elt_ty) <- boxySplitAppTy res_ty
; let res_ty' = mkAppTy m_ty elt_ty -- The boxySplit consumes res_ty
- ; (stmts', body') <- tcStmts DoExpr (tcDoStmt m_ty) stmts res_ty' $
- tcBody (doBodyCtxt DoExpr body) body
+ ; (stmts', body') <- tcStmts DoExpr (tcDoStmt m_ty) stmts
+ (emptyRefinement, res_ty') $
+ tcBody body
; return (HsDo DoExpr stmts' body' res_ty') }
tcDoStmts ctxt@(MDoExpr _) stmts body res_ty
tc_rhs rhs = withBox liftedTypeKind $ \ pat_ty ->
tcMonoExpr rhs (mkAppTy m_ty pat_ty)
- ; (stmts', body') <- tcStmts ctxt (tcMDoStmt tc_rhs) stmts res_ty' $
- tcBody (doBodyCtxt ctxt body) body
+ ; (stmts', body') <- tcStmts ctxt (tcMDoStmt tc_rhs) stmts
+ (emptyRefinement, res_ty') $
+ tcBody body
; let names = [mfixName, bindMName, thenMName, returnMName, failMName]
; insts <- mapM (newMethodFromName DoOrigin m_ty) names
tcDoStmts ctxt stmts body res_ty = pprPanic "tcDoStmts" (pprStmtContext ctxt)
-tcBody :: Message -> LHsExpr Name -> BoxyRhoType -> TcM (LHsExpr TcId)
-tcBody ctxt body res_ty
- = -- addErrCtxt ctxt $ -- This context adds little that is useful
- tcPolyExpr body res_ty
+tcBody :: LHsExpr Name -> (Refinement, BoxyRhoType) -> TcM (LHsExpr TcId)
+tcBody body (reft, res_ty)
+ = do { traceTc (text "tcBody" <+> ppr res_ty <+> ppr reft)
+ ; let (co, res_ty') = refineResType reft res_ty
+ ; body' <- tcPolyExpr body res_ty'
+ ; return (mkLHsCoerce co body') }
\end{code}
\begin{code}
type TcStmtChecker
- = forall thing. HsStmtContext Name
- -> Stmt Name
- -> BoxyRhoType -- Result type for comprehension
- -> (BoxyRhoType -> TcM thing) -- Checker for what follows the stmt
- -> TcM (Stmt TcId, thing)
+ = forall thing. HsStmtContext Name
+ -> Stmt Name
+ -> (Refinement, BoxyRhoType) -- Result type for comprehension
+ -> ((Refinement,BoxyRhoType) -> TcM thing) -- Checker for what follows the stmt
+ -> TcM (Stmt TcId, thing)
-- The incoming BoxyRhoType may be refined by type refinements
-- before being passed to the thing_inside
tcStmts :: HsStmtContext Name
-> TcStmtChecker -- NB: higher-rank type
-> [LStmt Name]
- -> BoxyRhoType
- -> (BoxyRhoType -> TcM thing)
+ -> (Refinement, BoxyRhoType)
+ -> ((Refinement, BoxyRhoType) -> TcM thing)
-> TcM ([LStmt TcId], thing)
-- Note the higher-rank type. stmt_chk is applied at different
tcGuardStmt ctxt (BindStmt pat rhs _ _) res_ty thing_inside
= do { (rhs', rhs_ty) <- tcInferRho rhs
- ; (pat', thing) <- tcPat LamPat pat rhs_ty res_ty thing_inside
+ ; (pat', thing) <- tcLamPat pat rhs_ty res_ty thing_inside
; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
tcGuardStmt ctxt stmt res_ty thing_inside
tcLcStmt m_tc ctxt (BindStmt pat rhs _ _) res_ty thing_inside
= do { (rhs', pat_ty) <- withBox liftedTypeKind $ \ ty ->
tcMonoExpr rhs (mkTyConApp m_tc [ty])
- ; (pat', thing) <- tcPat LamPat pat pat_ty res_ty thing_inside
+ ; (pat', thing) <- tcLamPat pat pat_ty res_ty thing_inside
; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
-- A boolean guard
tcDoStmt :: TcType -- Monad type, m
-> TcStmtChecker
-tcDoStmt m_ty ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside
+tcDoStmt m_ty ctxt (BindStmt pat rhs bind_op fail_op) reft_res_ty@(_,res_ty) thing_inside
= do { (rhs', pat_ty) <- withBox liftedTypeKind $ \ pat_ty ->
tcMonoExpr rhs (mkAppTy m_ty pat_ty)
-- We should use type *inference* for the RHS computations, becuase of GADTs.
-- We do inference on rhs, so that information about its type can be refined
-- when type-checking the pattern.
- ; (pat', thing) <- tcPat LamPat pat pat_ty res_ty thing_inside
+ ; (pat', thing) <- tcLamPat pat pat_ty reft_res_ty thing_inside
-- Deal with rebindable syntax; (>>=) :: m a -> (a -> m b) -> m b
; let bind_ty = mkFunTys [mkAppTy m_ty pat_ty,
; return (BindStmt pat' rhs' bind_op' fail_op', thing) }
-tcDoStmt m_ty ctxt (ExprStmt rhs then_op _) res_ty thing_inside
+tcDoStmt m_ty ctxt (ExprStmt rhs then_op _) reft_res_ty@(_,res_ty) thing_inside
= do { -- Deal with rebindable syntax; (>>) :: m a -> m b -> m b
a_ty <- newFlexiTyVarTy liftedTypeKind
; let rhs_ty = mkAppTy m_ty a_ty
then_ty = mkFunTys [rhs_ty, res_ty] res_ty
; then_op' <- tcSyntaxOp DoOrigin then_op then_ty
; rhs' <- tcPolyExpr rhs rhs_ty
- ; thing <- thing_inside res_ty
+ ; thing <- thing_inside reft_res_ty
; return (ExprStmt rhs' then_op' rhs_ty, thing) }
tcDoStmt m_ty ctxt stmt res_ty thing_inside
-> TcStmtChecker
tcMDoStmt tc_rhs ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside
= do { (rhs', pat_ty) <- tc_rhs rhs
- ; (pat', thing) <- tcPat LamPat pat pat_ty res_ty thing_inside
+ ; (pat', thing) <- tcLamPat pat pat_ty res_ty thing_inside
; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
tcMDoStmt tc_rhs ctxt (ExprStmt rhs then_op _) res_ty thing_inside
matchCtxt ctxt match = hang (ptext SLIT("In") <+> pprMatchContext ctxt <> colon)
4 (pprMatch ctxt match)
-doBodyCtxt :: HsStmtContext Name -> LHsExpr Name -> SDoc
-doBodyCtxt ctxt body = hang (ptext SLIT("In the result of") <+> pprStmtContext ctxt <> colon)
- 4 (ppr body)
-
stmtCtxt ctxt stmt = hang (ptext SLIT("In") <+> pprStmtContext ctxt <> colon)
4 (ppr stmt)
\end{code}
\section[TcPat]{Typechecking patterns}
\begin{code}
-module TcPat ( tcPat, tcPats, tcOverloadedLit,
- PatCtxt(..), badFieldCon, polyPatSig ) where
+module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit,
+ badFieldCon, polyPatSig ) where
#include "HsVersions.h"
import {-# SOURCE #-} TcExpr( tcSyntaxOp )
import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..),
+ mkCoPat, idCoercion,
LHsBinds, emptyLHsBinds, isEmptyLHsBinds,
collectPatsBinders, nlHsLit )
import TcHsSyn ( TcId, hsLitType )
import Name ( Name, mkSystemVarName )
import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
- tcLookupClass, tcLookupDataCon, tcLookupId, refineEnvironment,
- tcMetaTy )
-import TcMType ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, newBoxyTyVar, zonkTcType )
+ tcLookupClass, tcLookupDataCon, refineEnvironment,
+ tcLookupField, tcMetaTy )
+import TcMType ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars,
++ newCoVars, zonkTcType )
import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType, BoxyType,
SkolemInfo(PatSkol),
BoxySigmaType, BoxyRhoType, argTypeKind, typeKind,
- pprSkolTvBinding, isRefineableTy, isRigidTy, tcTyVarsOfTypes, mkTyVarTy, lookupTyVar,
- emptyTvSubst, substTyVar, substTy, mkTopTvSubst, zipTopTvSubst, zipOpenTvSubst,
- mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy, isArgTypeKind, isUnboxedTupleType,
- mkFunTy, mkFunTys, exactTyVarsOfTypes, tidyOpenType, tidyOpenTypes )
-import VarSet ( elemVarSet, mkVarSet )
-import Kind ( liftedTypeKind, openTypeKind )
-import TcUnify ( boxySplitTyConApp, boxySplitListTy, unifyType,
- unBox, stripBoxyType, zapToMonotype,
- boxyMatchTypes, boxyUnify, boxyUnifyList, checkSigTyVarsWrt )
+ pprSkolTvBinding, isRigidTy, tcTyVarsOfTypes,
+ zipTopTvSubst, isArgTypeKind, isUnboxedTupleType,
+ mkTyVarTys, mkClassPred, isOverloadedTy, substEqSpec,
+ mkFunTy, mkFunTys, tidyOpenType, tidyOpenTypes )
+import VarSet ( elemVarSet )
+import {- Kind parts of -}
+ Type ( liftedTypeKind )
+import TcUnify ( boxySplitTyConApp, boxySplitListTy, unBox,
+ zapToMonotype, boxyUnify, checkSigTyVarsWrt,
+ unifyType )
import TcHsType ( UserTypeCtxt(..), tcPatSig )
import TysWiredIn ( boolTy, parrTyCon, tupleTyCon )
-import Unify ( MaybeErr(..), gadtRefineTys )
import Type ( substTys, substTheta )
import StaticFlags ( opt_IrrefutableTuples )
-import TyCon ( TyCon )
-import DataCon ( DataCon, dataConTyCon, isVanillaDataCon,
- dataConFieldLabels, dataConSourceArity, dataConSig )
+import TyCon ( TyCon, FieldLabel )
+import DataCon ( DataCon, dataConTyCon, dataConFullSig, dataConName,
+ dataConFieldLabels, dataConSourceArity )
import PrelNames ( integralClassName, fromIntegerName, integerTyConName,
fromRationalName, rationalTyConName )
import BasicTypes ( isBoxed )
import SrcLoc ( Located(..), SrcSpan, noLoc )
import ErrUtils ( Message )
-import Util ( takeList, zipEqual )
+import Util ( zipEqual )
+import Maybes ( MaybeErr(..) )
import Outputable
import FastString
\end{code}
%************************************************************************
\begin{code}
-tcPats :: PatCtxt
- -> [LPat Name] -- Patterns,
- -> [BoxySigmaType] -- and their types
- -> BoxyRhoType -- Result type,
- -> (BoxyRhoType -> TcM a) -- and the checker for the body
- -> TcM ([LPat TcId], a)
+tcLetPat :: (Name -> Maybe TcRhoType)
+ -> LPat Name -> BoxySigmaType
+ -> TcM a
+ -> TcM (LPat TcId, a)
+tcLetPat sig_fn pat pat_ty thing_inside
+ = do { let init_state = PS { pat_ctxt = LetPat sig_fn,
+ pat_reft = emptyRefinement }
+ ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)
+
+ -- Don't know how to deal with pattern-bound existentials yet
+ ; checkTc (null ex_tvs) (existentialExplode pat)
+
+ ; return (pat', res) }
+
+-----------------
+tcLamPats :: [LPat Name] -- Patterns,
+ -> [BoxySigmaType] -- and their types
+ -> BoxyRhoType -- Result type,
+ -> ((Refinement, BoxyRhoType) -> TcM a) -- and the checker for the body
+ -> TcM ([LPat TcId], a)
-- This is the externally-callable wrapper function
-- Typecheck the patterns, extend the environment to bind the variables,
-- 1. Initialise the PatState
-- 2. Check the patterns
--- 3. Apply the refinement
+-- 3. Apply the refinement to the environment and result type
-- 4. Check the body
-- 5. Check that no existentials escape
-tcPats ctxt pats tys res_ty thing_inside
- = do { let init_state = PS { pat_ctxt = ctxt, pat_reft = emptyTvSubst }
+tcLamPats pats tys res_ty thing_inside
+ = tc_lam_pats (zipEqual "tcLamPats" pats tys)
+ (emptyRefinement, res_ty) thing_inside
+
+tcLamPat :: LPat Name -> BoxySigmaType
+ -> (Refinement,BoxyRhoType) -- Result type
+ -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
+ -> TcM (LPat TcId, a)
+tcLamPat pat pat_ty res_ty thing_inside
+ = do { ([pat'],thing) <- tc_lam_pats [(pat, pat_ty)] res_ty thing_inside
+ ; return (pat', thing) }
- ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' ->
+-----------------
+tc_lam_pats :: [(LPat Name,BoxySigmaType)]
+ -> (Refinement,BoxyRhoType) -- Result type
+ -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
+ -> TcM ([LPat TcId], a)
+tc_lam_pats pat_ty_prs (reft, res_ty) thing_inside
+ = do { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft }
+
+ ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
refineEnvironment (pat_reft pstate') $
- thing_inside (refineType (pat_reft pstate') res_ty)
+ thing_inside (pat_reft pstate', res_ty)
- ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty
+ ; let tys = map snd pat_ty_prs
+ ; tcCheckExistentialPat pats' ex_tvs tys res_ty
; returnM (pats', res) }
-----------------
-tcPat :: PatCtxt
- -> LPat Name -> BoxySigmaType
- -> BoxyRhoType -- Result type
- -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
- -> TcM (LPat TcId, a)
-tcPat ctxt pat pat_ty res_ty thing_inside
- = do { ([pat'],thing) <- tcPats ctxt [pat] [pat_ty] res_ty thing_inside
- ; return (pat', thing) }
-
-
------------------
-tcCheckExistentialPat :: PatCtxt
- -> [LPat TcId] -- Patterns (just for error message)
+tcCheckExistentialPat :: [LPat TcId] -- Patterns (just for error message)
-> [TcTyVar] -- Existentially quantified tyvars bound by pattern
-> [BoxySigmaType] -- Types of the patterns
-> BoxyRhoType -- Type of the body of the match
-- f (C g) x = g x
-- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
-tcCheckExistentialPat ctxt pats [] pat_tys body_ty
+tcCheckExistentialPat pats [] pat_tys body_ty
= return () -- Short cut for case when there are no existentials
-tcCheckExistentialPat (LetPat _) pats ex_tvs pat_tys body_ty
- -- Don't know how to deal with pattern-bound existentials yet
- = failWithTc (existentialExplode pats)
-
-tcCheckExistentialPat ctxt pats ex_tvs pat_tys body_ty
+tcCheckExistentialPat pats ex_tvs pat_tys body_ty
= addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys body_ty) $
checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
data PatState = PS {
pat_ctxt :: PatCtxt,
- pat_reft :: GadtRefinement -- Binds rigid TcTyVars to their refinements
+ pat_reft :: Refinement -- Binds rigid TcTyVars to their refinements
}
data PatCtxt
\begin{code}
--------------------
-tc_lpats :: PatState
- -> [LPat Name]
- -> [BoxySigmaType]
- -> (PatState -> TcM a)
- -> TcM ([LPat TcId], [TcTyVar], a)
-
-tc_lpats pstate pats pat_tys thing_inside
+type Checker inp out = forall r.
+ inp
+ -> PatState
+ -> (PatState -> TcM r)
+ -> TcM (out, [TcTyVar], r)
+
+tcMultiple :: Checker inp out -> Checker [inp] [out]
+tcMultiple tc_pat args pstate thing_inside
= do { err_ctxt <- getErrCtxt
- ; let loop pstate [] []
+ ; let loop pstate []
= do { res <- thing_inside pstate
; return ([], [], res) }
- loop pstate (p:ps) (ty:tys)
+ loop pstate (arg:args)
= do { (p', p_tvs, (ps', ps_tvs, res))
- <- tc_lpat pstate p ty $ \ pstate' ->
+ <- tc_pat arg pstate $ \ pstate' ->
setErrCtxt err_ctxt $
- loop pstate' ps tys
+ loop pstate' args
-- setErrCtxt: restore context before doing the next pattern
-- See note [Nesting] above
; return (p':ps', p_tvs ++ ps_tvs, res) }
- loop _ _ _ = pprPanic "tc_lpats" (ppr pats $$ ppr pat_tys)
-
- ; loop pstate pats pat_tys }
+ ; loop pstate args }
--------------------
-tc_lpat :: PatState
- -> LPat Name
- -> BoxySigmaType
- -> (PatState -> TcM a)
- -> TcM (LPat TcId, [TcTyVar], a)
-tc_lpat pstate (L span pat) pat_ty thing_inside
+tc_lpat_pr :: (LPat Name, BoxySigmaType)
+ -> PatState
+ -> (PatState -> TcM a)
+ -> TcM (LPat TcId, [TcTyVar], a)
+tc_lpat_pr (pat, ty) = tc_lpat pat ty
+
+tc_lpat :: LPat Name
+ -> BoxySigmaType
+ -> PatState
+ -> (PatState -> TcM a)
+ -> TcM (LPat TcId, [TcTyVar], a)
+tc_lpat (L span pat) pat_ty pstate thing_inside
= setSrcSpan span $
maybeAddErrCtxt (patCtxt pat) $
- do { let pat_ty' = refineType (pat_reft pstate) pat_ty
+ do { let (coercion, pat_ty') = refineType (pat_reft pstate) pat_ty
-- Make sure the result type reflects the current refinement
- ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
- ; return (L span pat', tvs, res) }
+ -- We must do this here, so that it correctly ``sees'' all
+ -- the refinements to the left. Example:
+ -- Suppose C :: forall a. T a -> a -> Foo
+ -- Pattern C a p1 True
+ -- So p1 might refine 'a' to True, and the True
+ -- pattern had better see it.
+ ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
+ ; return (mkCoPat coercion (L span pat') pat_ty, tvs, res) }
--------------------
tc_pat :: PatState
; return (pat', [], res) }
tc_pat pstate (ParPat pat) pat_ty thing_inside
- = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+ = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
; return (ParPat pat', tvs, res) }
tc_pat pstate (BangPat pat) pat_ty thing_inside
- = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+ = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
; return (BangPat pat', tvs, res) }
-- There's a wrinkle with irrefutable patterns, namely that we
-- Nor should a lazy pattern bind any existential type variables
-- because they won't be in scope when we do the desugaring
tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
- = do { (pat', pat_tvs, res) <- tc_lpat pstate pat pat_ty $ \ _ ->
+ = do { (pat', pat_tvs, res) <- tc_lpat pat pat_ty pstate $ \ _ ->
thing_inside pstate
-- Ignore refined pstate',
-- revert to pstate
tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
= do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
- tc_lpat pstate pat (idType bndr_id) thing_inside
+ tc_lpat pat (idType bndr_id) pstate thing_inside
-- NB: if we do inference on:
-- \ (y@(x::forall a. a->a)) = e
-- we'll fail. The as-pattern infers a monotype for 'y', which then
tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
= do { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
- tc_lpat pstate pat inner_ty thing_inside
+ tc_lpat pat inner_ty pstate thing_inside
; return (SigPatOut pat' inner_ty, tvs, res) }
tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
-- Lists, tuples, arrays
tc_pat pstate (ListPat pats _) pat_ty thing_inside
= do { elt_ty <- boxySplitListTy pat_ty
- ; let elt_tys = takeList pats (repeat elt_ty)
- ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
+ ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
+ pats pstate thing_inside
; return (ListPat pats' elt_ty, pats_tvs, res) }
tc_pat pstate (PArrPat pats _) pat_ty thing_inside
= do { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty
- ; let elt_tys = takeList pats (repeat elt_ty)
- ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
+ ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
+ pats pstate thing_inside
; ifM (null pats) (zapToMonotype pat_ty) -- c.f. ExplicitPArr in TcExpr
; return (PArrPat pats' elt_ty, pats_tvs, res) }
tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
= do { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
- ; (pats', pats_tvs, res) <- tc_lpats pstate pats arg_tys thing_inside
+ ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
+ pstate thing_inside
-- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
-- so that we can experiment with lazy tuple-matching.
%************************************************************************
\begin{code}
+-- Running example:
+-- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
+-- with scrutinee of type (T ty)
+
tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
-> BoxySigmaType -- Type of the pattern
-> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
-> TcM (Pat TcId, [TcTyVar], a)
tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
- | isVanillaDataCon data_con
- = do { ty_args <- boxySplitTyConApp tycon pat_ty
- ; let (tvs, _, arg_tys, _, _) = dataConSig data_con
- arg_tvs = exactTyVarsOfTypes arg_tys
- -- See Note [Silly type synonyms in smart-app] in TcExpr
- -- for why we must use exactTyVarsOfTypes
- inst_prs = zipEqual "tcConPat" tvs ty_args
- subst = mkTopTvSubst inst_prs
- arg_tys' = substTys subst arg_tys
- unconstrained_ty_args = [ty_arg | (tv,ty_arg) <- inst_prs,
- not (tv `elemVarSet` arg_tvs)]
- ; mapM unBox unconstrained_ty_args -- Zap these to monotypes
- ; tcInstStupidTheta data_con ty_args
- ; traceTc (text "tcConPat" <+> vcat [ppr data_con, ppr ty_args, ppr arg_tys'])
- ; (arg_pats', tvs, res) <- tcConArgs pstate data_con arg_pats arg_tys' thing_inside
- ; return (ConPatOut (L con_span data_con) [] [] emptyLHsBinds
- arg_pats' (mkTyConApp tycon ty_args),
- tvs, res) }
-
- | otherwise -- GADT case
- = do { ty_args <- boxySplitTyConApp tycon pat_ty
- ; span <- getSrcSpanM -- The whole pattern
-
- -- Instantiate the constructor type variables and result type
- ; let (tvs, theta, arg_tys, _, res_tys) = dataConSig data_con
- arg_tvs = exactTyVarsOfTypes arg_tys
- -- See Note [Silly type synonyms in smart-app] in TcExpr
- -- for why we must use exactTyVarsOfTypes
+ = do { span <- getSrcSpanM -- Span for the whole pattern
+ ; let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys) = dataConFullSig data_con
skol_info = PatSkol data_con span
- arg_flags = [ tv `elemVarSet` arg_tvs | tv <- tvs ]
- ; tvs' <- tcInstSkolTyVars skol_info tvs
- ; let res_tys' = substTys (zipTopTvSubst tvs (mkTyVarTys tvs')) res_tys
-
- -- Do type refinement!
- ; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', ppr res_tys',
- text "ty-args:" <+> ppr ty_args ])
- ; refineAlt pstate data_con tvs' arg_flags res_tys' ty_args
- $ \ pstate' tv_tys' -> do
-
- -- ToDo: arg_tys should be boxy, but I don't think theta' should be,
- -- or the tv_tys' in the call to tcInstStupidTheta
- { let tenv' = zipTopTvSubst tvs tv_tys'
- theta' = substTheta tenv' theta
- arg_tys' = substTys tenv' arg_tys -- Boxy types
+
+ -- Instantiate the constructor type variables [a->ty]
+ ; ctxt_res_tys <- boxySplitTyConApp tycon pat_ty
+ ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
+ ; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs)
+ (ctxt_res_tys ++ mkTyVarTys ex_tvs')
+ eq_spec' = substEqSpec tenv eq_spec
+ theta' = substTheta tenv theta
+ arg_tys' = substTys tenv arg_tys
+
+ ; co_vars <- newCoVars eq_spec' -- Make coercion variables
+ ; pstate' <- refineAlt data_con pstate ex_tvs co_vars pat_ty
; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
- do { tcInstStupidTheta data_con tv_tys'
- -- The stupid-theta mentions the newly-bound tyvars, so
- -- it must live inside the getLIE, so that the
- -- tcSimplifyCheck will apply the type refinement to it
- ; tcConArgs pstate' data_con arg_pats arg_tys' thing_inside }
+ tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
; dicts <- newDicts (SigOrigin skol_info) theta'
- ; dict_binds <- tcSimplifyCheck doc tvs' dicts lie_req
+ ; dict_binds <- tcSimplifyCheck doc ex_tvs' dicts lie_req
+
+ ; tcInstStupidTheta data_con ctxt_res_tys
- ; return (ConPatOut (L con_span data_con)
- tvs' (map instToId dicts) dict_binds
- arg_pats' (mkTyConApp tycon ty_args),
- tvs' ++ inner_tvs, res)
- } }
+ ; return (ConPatOut { pat_con = L con_span data_con,
+ pat_tvs = ex_tvs' ++ co_vars,
+ pat_dicts = map instToId dicts, pat_binds = dict_binds,
+ pat_args = arg_pats', pat_ty = pat_ty },
+ ex_tvs' ++ inner_tvs, res)
+ }
where
doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
-tcConArgs :: PatState -> DataCon
- -> HsConDetails Name (LPat Name) -> [TcSigmaType]
- -> (PatState -> TcM a)
- -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a)
+tcConArgs :: DataCon -> [TcSigmaType]
+ -> Checker (HsConDetails Name (LPat Name)) (HsConDetails Id (LPat Id))
-tcConArgs pstate data_con (PrefixCon arg_pats) arg_tys thing_inside
+tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
= do { checkTc (con_arity == no_of_args) -- Check correct arity
(arityErr "Constructor" data_con con_arity no_of_args)
- ; (arg_pats', tvs, res) <- tc_lpats pstate arg_pats arg_tys thing_inside
+ ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
+ ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
+ pstate thing_inside
; return (PrefixCon arg_pats', tvs, res) }
where
con_arity = dataConSourceArity data_con
no_of_args = length arg_pats
-tcConArgs pstate data_con (InfixCon p1 p2) arg_tys thing_inside
+tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside
= do { checkTc (con_arity == 2) -- Check correct arity
(arityErr "Constructor" data_con con_arity 2)
- ; ([p1',p2'], tvs, res) <- tc_lpats pstate [p1,p2] arg_tys thing_inside
+ ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
+ pstate thing_inside
; return (InfixCon p1' p2', tvs, res) }
where
con_arity = dataConSourceArity data_con
-tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside
- = do { (rpats', tvs, res) <- tc_fields pstate rpats thing_inside
+tcConArgs data_con arg_tys (RecCon rpats) pstate thing_inside
+ = do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
; return (RecCon rpats', tvs, res) }
where
- tc_fields :: PatState -> [(Located Name, LPat Name)]
- -> (PatState -> TcM a)
- -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a)
- tc_fields pstate [] thing_inside
- = do { res <- thing_inside pstate
- ; return ([], [], res) }
-
- tc_fields pstate (rpat : rpats) thing_inside
- = do { (rpat', tvs1, (rpats', tvs2, res))
- <- tc_field pstate rpat $ \ pstate' ->
- tc_fields pstate' rpats thing_inside
- ; return (rpat':rpats', tvs1 ++ tvs2, res) }
-
- tc_field pstate (field_lbl, pat) thing_inside
+ tc_field :: Checker (Located Name, LPat Name) (Located TcId, LPat TcId)
+ tc_field (field_lbl, pat) pstate thing_inside
= do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
- ; (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+ ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
; return ((sel_id, pat'), tvs, res) }
+ find_field_ty :: FieldLabel -> TcM (Id, TcType)
find_field_ty field_lbl
= case [ty | (f,ty) <- field_tys, f == field_lbl] of
-- The normal case, when the field comes from the right constructor
(pat_ty : extras) ->
ASSERT( null extras )
- do { sel_id <- tcLookupId field_lbl
+ do { sel_id <- tcLookupField field_lbl
; return (sel_id, pat_ty) }
+ field_tys :: [(FieldLabel, TcType)]
field_tys = zip (dataConFieldLabels data_con) arg_tys
-- Don't use zipEqual! If the constructor isn't really a record, then
-- dataConFieldLabels will be empty (and each field in the pattern
-- will generate an error below).
+
+tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
+tcConArg (arg_pat, arg_ty) pstate thing_inside
+ = tc_lpat arg_pat arg_ty pstate thing_inside
+ -- NB: the tc_lpat will refine pat_ty if necessary
+ -- based on the current pstate, which may include
+ -- refinements from peer argument patterns to the left
\end{code}
%************************************************************************
\begin{code}
-refineAlt :: PatState
- -> DataCon -- For tracing only
- -> [TcTyVar] -- Type variables from pattern
- -> [Bool] -- Flags indicating which type variables occur
- -- in the type of at least one argument
- -> [TcType] -- Result types from the pattern
- -> [BoxySigmaType] -- Result types from the scrutinee (context)
- -> (PatState -> [BoxySigmaType] -> TcM a)
- -- Possibly-refined existentials
- -> TcM a
-refineAlt pstate con pat_tvs arg_flags pat_res_tys ctxt_res_tys thing_inside
- | not (all isRigidTy ctxt_res_tys)
- -- The context is not a rigid type, so we do no type refinement here.
- = do { let arg_tvs = mkVarSet [ tv | (tv, True) <- pat_tvs `zip` arg_flags]
- subst = boxyMatchTypes arg_tvs pat_res_tys ctxt_res_tys
-
- res_tvs = tcTyVarsOfTypes pat_res_tys
- -- The tvs are (already) all fresh skolems. We need a
- -- fresh skolem for each type variable (to bind in the pattern)
- -- even if it's refined away by the type refinement
- find_inst tv
- | not (tv `elemVarSet` res_tvs) = return (mkTyVarTy tv)
- | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty
- | otherwise = do { tv <- newBoxyTyVar openTypeKind
- ; return (mkTyVarTy tv) }
- ; pat_tys' <- mapM find_inst pat_tvs
-
- -- Do the thing inside
- ; res <- thing_inside pstate pat_tys'
-
- -- Unbox the types that have been filled in by the thing_inside
- -- I.e. the ones whose type variables are mentioned in at least one arg
- ; let strip ty in_arg_tv | in_arg_tv = stripBoxyType ty
- | otherwise = return ty
- ; pat_tys'' <- zipWithM strip pat_tys' arg_flags
- ; let subst = zipOpenTvSubst pat_tvs pat_tys''
- ; boxyUnifyList (substTys subst pat_res_tys) ctxt_res_tys
-
- ; return res } -- All boxes now filled
-
- | otherwise -- The context is rigid, so we can do type refinement
- = case gadtRefineTys (pat_reft pstate) con pat_tvs pat_res_tys ctxt_res_tys of
- Failed msg -> failWithTc (inaccessibleAlt msg)
- Succeeded (new_subst, all_bound_here)
- | all_bound_here -- All the new bindings are for pat_tvs, so no need
- -- to refine the environment or pstate
- -> do { traceTc trace_msg
- ; thing_inside pstate pat_tvs' }
- | otherwise -- New bindings affect the context, so pass down pstate'.
- -- DO NOT refine the envt, because we might be inside a
- -- lazy pattern
- -> do { traceTc trace_msg
- ; thing_inside pstate' pat_tvs' }
- where
- pat_tvs' = map (substTyVar new_subst) pat_tvs
- pstate' = pstate { pat_reft = new_subst }
- trace_msg = text "refineTypes:match" <+> ppr con <+> ppr new_subst
-
-refineType :: GadtRefinement -> BoxyRhoType -> BoxyRhoType
--- Refine the type if it is rigid
-refineType reft ty
- | isRefineableTy ty = substTy reft ty
- | otherwise = ty
+refineAlt :: DataCon -- For tracing only
+ -> PatState
+ -> [TcTyVar] -- Existentials
+ -> [CoVar] -- Equational constraints
+ -> BoxySigmaType -- Pattern type
+ -> TcM PatState
+
+refineAlt con pstate ex_tvs [] pat_ty
+ = return pstate -- Common case: no equational constraints
+
+refineAlt con pstate ex_tvs co_vars pat_ty
+ | not (isRigidTy pat_ty)
+ = failWithTc (nonRigidMatch con)
+ -- We are matching against a GADT constructor with non-trivial
+ -- constraints, but pattern type is wobbly. For now we fail.
+ -- We can make sense of this, however:
+ -- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a
+ -- (\x -> case x of { MkT v -> v })
+ -- We can infer that x must have type T [c], for some wobbly 'c'
+ -- and translate to
+ -- (\(x::T [c]) -> case x of
+ -- MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g
+ -- To implement this, we'd first instantiate the equational
+ -- constraints with *wobbly* type variables for the existentials;
+ -- then unify these constraints to make pat_ty the right shape;
+ -- then proceed exactly as in the rigid case
+
+ | otherwise -- In the rigid case, we perform type refinement
+ = case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
+ Failed msg -> failWithTc (inaccessibleAlt msg) ;
+ Succeeded reft -> do { traceTc trace_msg
+ ; return (pstate { pat_reft = reft }) }
+ -- DO NOT refine the envt right away, because we
+ -- might be inside a lazy pattern. Instead, refine pstate
+ where
+
+ trace_msg = text "refineAlt:match" <+> ppr con <+> ppr reft
+ }
\end{code}
-----------------------------------------------
-existentialExplode pats
+existentialExplode pat
= hang (vcat [text "My brain just exploded.",
text "I can't handle pattern bindings for existentially-quantified constructors.",
text "In the binding group for"])
- 4 (vcat (map ppr pats))
+ 4 (ppr pat)
sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env
= do { pat_tys' <- mapM zonkTcType pat_tys
hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
2 (vcat (map pprSkolTvBinding tvs))
+nonRigidMatch con
+ = hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
+ 2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
+
inaccessibleAlt msg
= hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
\end{code}
import TyCon ( tyConName )
import TysWiredIn ( mkListTy, unitTy )
import IdInfo ( GlobalIdDetails(..) )
-import Kind ( Kind )
+import {- Kind parts of -} Type ( Kind, eqKind )
import Var ( globaliseId )
import Name ( isBuiltInSyntax, isInternalName )
import OccName ( isTcOcc )
-- then the type checker would instantiate x..z, and we wouldn't
-- get their *polymorphic* values. (And we'd get ambiguity errs
-- if they were overloaded, since they aren't applied to anything.)
- mk_return ids = nlHsApp (noLoc $ TyApp (nlHsVar ret_id) [ret_ty])
+ mk_return ids = nlHsApp (mkHsTyApp ret_id [ret_ty])
(noLoc $ ExplicitList unitTy (map mk_item ids)) ;
- mk_item id = nlHsApp (noLoc $ TyApp (nlHsVar unsafeCoerceId) [idType id, unitTy])
- (nlHsVar id)
+ mk_item id = nlHsApp (noLoc $ unsafeCoerce)
+ (nlHsVar id)
+
+ unsafeCoerce x = Cast x (mkUnsafeCoercion [idType id, unitTy])
} ;
-- OK, we're ready to typecheck the stmts
-- OK, here's the business end!
maybe_res <- initTcRnIf 'a' hsc_env gbl_env lcl_env $
- do {
-#if defined(GHCI) && defined(BREAKPOINT)
- unique <- newUnique ;
- let { var = mkInternalName unique (mkOccName tvName "a") noSrcLoc;
- tyvar = mkTyVar var liftedTypeKind;
- basicType extra = (FunTy intTy
- (FunTy (mkListTy unitTy)
- (FunTy stringTy
- (ForAllTy tyvar
- (extra
- (FunTy (TyVarTy tyvar)
- (TyVarTy tyvar)))))));
- breakpointJumpType
- = mkGlobalId VanillaGlobal breakpointJumpName
- (basicType id) vanillaIdInfo;
- breakpointCondJumpType
- = mkGlobalId VanillaGlobal breakpointCondJumpName
- (basicType (FunTy boolTy)) vanillaIdInfo;
- new_env = mkNameEnv [(breakpointJumpName
- , ATcId breakpointJumpType topLevel False)
- ,(breakpointCondJumpName
- , ATcId breakpointCondJumpType topLevel False)];
- };
- r <- tryM (updLclEnv (\gbl -> gbl{tcl_env=new_env}) do_this)
-#else
- r <- tryM do_this
-#endif
+ addBreakpointBindings $
+ do { r <- tryM do_this
; case r of
Right res -> return (Just res)
Left _ -> return Nothing } ;
return res
\end{code}
+\begin{code}
+addBreakpointBindings :: TcM a -> TcM a
+addBreakpointBindings thing_inside
+#if defined(GHCI) && defined(BREAKPOINT)
+ = do { unique <- newUnique
+ ; let { var = mkInternalName unique (mkOccName tvName "a") noSrcLoc;
+ tyvar = mkTyVar var liftedTypeKind;
+ basicType extra = (FunTy intTy
+ (FunTy (mkListTy unitTy)
+ (FunTy stringTy
+ (ForAllTy tyvar
+ (extra
+ (FunTy (TyVarTy tyvar)
+ (TyVarTy tyvar)))))));
+ breakpointJumpId
+ = mkGlobalId VanillaGlobal breakpointJumpName
+ (basicType id) vanillaIdInfo;
+ breakpointCondJumpId
+ = mkGlobalId VanillaGlobal breakpointCondJumpName
+ (basicType (FunTy boolTy)) vanillaIdInfo
+ }
+ ; extendIdEnv [breakpoingJumpId, breakpointCondJumpId] thing_inside}
+#else
+ = thing_inside
+#endif
+\end{code}
%************************************************************************
%* *
-- Typechecker types
TcTyThing(..), pprTcTyThingCategory,
- GadtRefinement,
-- Template Haskell
ThStage(..), topStage, topSpliceStage,
import HsSyn ( PendingSplice, HsOverLit, LRuleDecl, LForeignDecl,
ArithSeqInfo, DictBinds, LHsBinds, LImportDecl, HsGroup,
- IE )
+ ExprCoFn, IE )
import HscTypes ( FixityEnv,
HscEnv, TypeEnv, TyThing,
GenAvailInfo(..), AvailInfo, HscSource(..),
tcl_lie :: TcRef LIE -- Place to accumulate type constraints
}
-type GadtRefinement = TvSubst
{- Note [Given Insts]
~~~~~~~~~~~~~~~~~~
data TcTyThing
= AGlobal TyThing -- Used only in the return type of a lookup
- | ATcId TcId -- Ids defined in this module; may not be fully zonked
- ThLevel
- Bool -- True <=> apply the type refinement to me
+ | ATcId { -- Ids defined in this module; may not be fully zonked
+ tct_id :: TcId,
+ tct_co :: Maybe ExprCoFn, -- Nothing <=> Do not apply a GADT type refinement
+ -- I am wobbly, or have no free
+ -- type variables
+ -- Just co <=> Apply any type refinement to me,
+ -- and record it in the coercion
+ tct_type :: TcType, -- Type of (coercion applied to id)
+ tct_level :: ThLevel }
| ATyVar Name TcType -- The type to which the lexically scoped type vaiable
-- is currently refined. We only need the Name
instance Outputable TcTyThing where -- Debugging only
ppr (AGlobal g) = ppr g
- ppr (ATcId g tl rig) = text "Identifier" <>
- ifPprDebug (brackets (ppr g <> comma <> ppr tl <+> ppr rig))
+ ppr elt@(ATcId {}) = text "Identifier" <>
+ ifPprDebug (brackets (ppr (tct_id elt) <> dcolon <> ppr (tct_type elt) <> comma
+ <+> ppr (tct_level elt) <+> ppr (tct_co elt)))
ppr (ATyVar tv _) = text "Type variable" <+> quotes (ppr tv)
ppr (AThing k) = text "AThing" <+> ppr k
#include "HsVersions.h"
import {-# SOURCE #-} TcUnify( unifyType )
-import HsSyn ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
-import TcHsSyn ( mkHsApp, mkHsTyApp, mkHsDictApp )
+import HsSyn ( HsBind(..), HsExpr(..), LHsExpr,
+ ExprCoFn(..), (<.>), nlHsTyApp, emptyLHsBinds )
+import TcHsSyn ( mkHsApp )
import TcRnMonad
import Inst ( lookupInst, LookupInstResult(..),
isMethodFor, isMethod,
instToId, tyVarsOfInsts, cloneDict,
ipNamesOfInsts, ipNamesOfInst, dictPred,
- fdPredsOfInst,
+ fdPredsOfInst, mkInstCoFn,
newDictsAtLoc, tcInstClassOp,
getDictClassTys, isTyVarDict, instLoc,
zonkInst, tidyInsts, tidyMoreInsts,
new_binds = addBind binds w rhs
new_avails = addToFM avails w (LinRhss rhss)
+ -- get_root is just used for Linear
get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
get_root irreds frees Irred w = cloneDict w `thenM` \ w' ->
returnM (w':irreds, frees, instToId w')
returnM (L span (VarBind x (mk_app span split_id rhs)),
[mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
-mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
+mk_fs_app span id ty var = nlHsTyApp id [ty,ty] `mkHsApp` (L span (HsVar var))
mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
| is_given sc_dict = return avails
| otherwise = addSCs is_loop avails' sc_dict
where
- sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
+ sc_sel_rhs = L (instSpan dict) (HsCoerce co_fn (HsVar sc_sel))
+ co_fn = mkInstCoFn tys [dict]
avails' = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
is_given :: Inst -> Bool
; fix <- reifyFixity name
; return (TH.DataConI (reifyName name) ty (reifyName (dataConTyCon dc)) fix) }
-reifyThing (ATcId id _ _)
- = do { ty1 <- zonkTcType (idType id) -- Make use of all the info we have, even
- -- though it may be incomplete
+reifyThing (ATcId {tct_id = id, tct_ty = ty})
+ = do { ty1 <- zonkTcType ty -- Make use of all the info we have, even
+ -- though it may be incomplete
; ty2 <- reifyType ty1
; fix <- reifyFixity (idName id)
; return (TH.VarI (reifyName id) ty2 Nothing fix) }
import TcMType ( newKindVar, checkValidTheta, checkValidType,
-- checkFreeness,
UserTypeCtxt(..), SourceTyCtxt(..) )
-import TcType ( TcKind, TcType, tyVarsOfType, mkPhiTy,
+import TcType ( TcKind, TcType, Type, tyVarsOfType, mkPhiTy,
mkArrowKind, liftedTypeKind, mkTyVarTys,
tcSplitSigmaTy, tcEqTypes, tcGetTyVar_maybe )
-import Type ( splitTyConApp_maybe,
+import Type ( PredType(..), splitTyConApp_maybe, mkTyVarTy
-- pprParendType, pprThetaArrow
)
-import Kind ( mkArrowKinds, splitKindFunTys )
import Generics ( validGenericMethodType, canDoGenerics )
import Class ( Class, className, classTyCon, DefMeth(..), classBigSig, classTyVars )
import TyCon ( TyCon, AlgTyConRhs( AbstractTyCon ),
tyConDataCons, mkForeignTyCon, isProductTyCon, isRecursiveTyCon,
tyConStupidTheta, synTyConRhs, isSynTyCon, tyConName )
-import DataCon ( DataCon, dataConWrapId, dataConName,
- dataConFieldLabels, dataConTyCon,
- dataConTyVars, dataConFieldType, dataConResTys )
+import DataCon ( DataCon, dataConUserType, dataConName,
+ dataConFieldLabels, dataConTyCon, dataConAllTyVars,
+ dataConFieldType, dataConResTys )
import Var ( TyVar, idType, idName )
import VarSet ( elemVarSet, mkVarSet )
import Name ( Name, getSrcLoc )
import Util ( zipLazy, isSingleton, notNull, sortLe )
import List ( partition )
import SrcLoc ( Located(..), unLoc, getLoc, srcLocSpan )
-import ListSetOps ( equivClasses )
+import ListSetOps ( equivClasses, minusList )
import List ( delete )
import Digraph ( SCC(..) )
import DynFlags ( DynFlag( Opt_GlasgowExts, Opt_Generics,
-- Check that we don't use GADT syntax in H98 world
; checkTc (gla_exts || h98_syntax) (badGadtDecl tc_name)
+ -- Check that the stupid theta is empty for a GADT-style declaration
+ ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
+
-- Check that there's at least one condecl,
- -- or else we're reading an interface file, or -fglasgow-exts
+ -- or else we're reading an hs-boot file, or -fglasgow-exts
; checkTc (not (null cons) || gla_exts || is_boot)
(emptyConDeclsErr tc_name)
{ data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data
tycon final_tvs))
cons
- ; let tc_rhs
- | null cons && is_boot -- In a hs-boot file, empty cons means
- = AbstractTyCon -- "don't know"; hence Abstract
- | otherwise
- = case new_or_data of
- DataType -> mkDataTyConRhs data_cons
- NewType -> ASSERT( isSingleton data_cons )
- mkNewTyConRhs tycon (head data_cons)
+ ; tc_rhs <-
+ if null cons && is_boot -- In a hs-boot file, empty cons means
+ then return AbstractTyCon -- "don't know"; hence Abstract
+ else case new_or_data of
+ DataType -> return (mkDataTyConRhs data_cons)
+ NewType ->
+ ASSERT( isSingleton data_cons )
+ mkNewTyConRhs tc_name tycon (head data_cons)
; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
- (want_generic && canDoGenerics data_cons)
+ (want_generic && canDoGenerics data_cons) h98_syntax
})
; return (ATyCon tycon)
}
= do { let tc_datacon field_lbls arg_ty
= do { arg_ty' <- tcHsKindedType arg_ty -- No bang on newtype
; buildDataCon (unLoc name) False {- Prefix -}
- True {- Vanilla -} [NotMarkedStrict]
+ [NotMarkedStrict]
(map unLoc field_lbls)
- tc_tvs [] [arg_ty']
- tycon (mkTyVarTys tc_tvs) }
+ tc_tvs [] -- No existentials
+ [] [] -- No equalities, predicates
+ [arg_ty']
+ tycon }
-- Check that a newtype has no existential stuff
; checkTc (null ex_tvs && null (unLoc ex_ctxt)) (newtypeExError name)
(ConDecl name _ tvs ctxt details res_ty)
= tcTyVarBndrs tvs $ \ tvs' -> do
{ ctxt' <- tcHsKindedContext ctxt
- ; (data_tc, res_ty_args) <- tcResultType tycon tc_tvs res_ty
+ ; (univ_tvs, ex_tvs, eq_preds, data_tc) <- tcResultType tycon tc_tvs tvs' res_ty
; let
- con_tvs = case res_ty of
- ResTyH98 -> tc_tvs ++ tvs'
- ResTyGADT _ -> tryVanilla tvs' res_ty_args
-
- -- Vanilla iff result type matches the quantified vars exactly,
- -- and there is no existential context
- -- Must check the context too because of implicit params; e.g.
- -- data T = (?x::Int) => MkT Int
- is_vanilla = res_ty_args `tcEqTypes` mkTyVarTys con_tvs
- && null (unLoc ctxt)
-
tc_datacon is_infix field_lbls btys
= do { let bangs = map getBangStrictness btys
; arg_tys <- mappM tcHsBangType btys
- ; buildDataCon (unLoc name) is_infix is_vanilla
+ ; buildDataCon (unLoc name) is_infix
(argStrictness unbox_strict tycon bangs arg_tys)
(map unLoc field_lbls)
- con_tvs ctxt' arg_tys
- data_tc res_ty_args }
+ univ_tvs ex_tvs eq_preds ctxt' arg_tys
+ data_tc }
-- NB: we put data_tc, the type constructor gotten from the constructor
-- type signature into the data constructor; that way
-- checkValidDataCon can complain if it's wrong.
}
-tcResultType :: TyCon -> [TyVar] -> ResType Name -> TcM (TyCon, [TcType])
-tcResultType tycon tvs ResTyH98 = return (tycon, mkTyVarTys tvs)
-tcResultType _ _ (ResTyGADT res_ty) = tcLHsConResTy res_ty
-
-tryVanilla :: [TyVar] -> [TcType] -> [TyVar]
--- (tryVanilla tvs tys) returns a permutation of tvs.
--- It tries to re-order the tvs so that it exactly
--- matches the [Type], if that is possible
-tryVanilla tvs (ty:tys) | Just tv <- tcGetTyVar_maybe ty -- The type is a tyvar
- , tv `elem` tvs -- That tyvar is in the list
- = tv : tryVanilla (delete tv tvs) tys
-tryVanilla tvs tys = tvs -- Fall through case
-
+tcResultType :: TyCon
+ -> [TyVar] -- data T a b c = ...
+ -> [TyVar] -- where MkT :: forall a b c. ...
+ -> ResType Name
+ -> TcM ([TyVar], -- Universal
+ [TyVar], -- Existential
+ [(TyVar,Type)], -- Equality predicates
+ TyCon) -- TyCon given in the ResTy
+ -- We don't check that the TyCon given in the ResTy is
+ -- the same as the parent tycon, becuase we are in the middle
+ -- of a recursive knot; so it's postponed until checkValidDataCon
+
+tcResultType decl_tycon tc_tvs dc_tvs ResTyH98
+ = return (tc_tvs, dc_tvs, [], decl_tycon)
+ -- In H98 syntax the dc_tvs are the existential ones
+ -- data T a b c = forall d e. MkT ...
+ -- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
+
+tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
+ -- E.g. data T a b c where
+ -- MkT :: forall x y z. T (x,y) z z
+ -- Then we generate
+ -- ([a,z,c], [x,y], [a:=:(x,y), c:=:z], T)
+
+ = do { (dc_tycon, res_tys) <- tcLHsConResTy res_ty
+ -- NB: tc_tvs and dc_tvs are distinct
+ ; let univ_tvs = choose_univs [] tc_tvs res_tys
+ -- Each univ_tv is either a dc_tv or a tc_tv
+ ex_tvs = dc_tvs `minusList` univ_tvs
+ eq_spec = [ (tv, ty) | (tv,ty) <- univ_tvs `zip` res_tys,
+ tv `elem` tc_tvs]
+ ; return (univ_tvs, ex_tvs, eq_spec, dc_tycon) }
+ where
+ -- choose_univs uses the res_ty itself if it's a type variable
+ -- and hasn't already been used; otherwise it uses one of the tc_tvs
+ choose_univs used tc_tvs []
+ = ASSERT( null tc_tvs ) []
+ choose_univs used (tc_tv:tc_tvs) (res_ty:res_tys)
+ | Just tv <- tcGetTyVar_maybe res_ty, not (tv `elem` used)
+ = tv : choose_univs (tv:used) tc_tvs res_tys
+ | otherwise
+ = tc_tv : choose_univs used tc_tvs res_tys
-------------------
argStrictness :: Bool -- True <=> -funbox-strict_fields
-- of the constructor.
checkValidTyCon :: TyCon -> TcM ()
-checkValidTyCon tc
+checkValidTyCon tc
| isSynTyCon tc
= checkValidType syn_ctxt syn_rhs
| otherwise
get_fields con = dataConFieldLabels con `zip` repeat con
-- dataConFieldLabels may return the empty list, which is fine
- -- Note: The complicated checkOne logic below is there to accomodate
- -- for different return types. Add res_ty to the mix,
- -- comparing them in two steps, all for good error messages.
- -- Plan: Use Unify.tcMatchTys to compare the first candidate's
- -- result type against other candidates' types (check bothways).
- -- If they magically agrees, take the substitution and
- -- apply them to the latter ones, and see if they match perfectly.
- -- check_fields fields@((first_field_label, field_ty) : other_fields)
+ -- See Note [GADT record selectors] in MkId.lhs
+ -- We must check (a) that the named field has the same
+ -- type in each constructor
+ -- (b) that those constructors have the same result type
+ --
+ -- However, the constructors may have differently named type variable
+ -- and (worse) we don't know how the correspond to each other. E.g.
+ -- C1 :: forall a b. { f :: a, g :: b } -> T a b
+ -- C2 :: forall d c. { f :: c, g :: c } -> T c d
+ --
+ -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
+ -- result type against other candidates' types BOTH WAYS ROUND.
+ -- If they magically agrees, take the substitution and
+ -- apply them to the latter ones, and see if they match perfectly.
check_fields fields@((label, con1) : other_fields)
-- These fields all have the same name, but are from
-- different constructors in the data type
-- NB: this check assumes that all the constructors of a given
-- data type use the same type variables
where
- tvs1 = mkVarSet (dataConTyVars con1)
+ tvs1 = mkVarSet (dataConAllTyVars con1)
res1 = dataConResTys con1
fty1 = dataConFieldType con1 label
= do { checkFieldCompat label con1 con2 tvs1 res1 res2 fty1 fty2
; checkFieldCompat label con2 con1 tvs2 res2 res1 fty2 fty1 }
where
- tvs2 = mkVarSet (dataConTyVars con2)
+ tvs2 = mkVarSet (dataConAllTyVars con2)
res2 = dataConResTys con2
fty2 = dataConFieldType con2 label
= setSrcSpan (srcLocSpan (getSrcLoc con)) $
addErrCtxt (dataConCtxt con) $
do { checkTc (dataConTyCon con == tc) (badDataConTyCon con)
- ; checkValidType ctxt (idType (dataConWrapId con)) }
-
- -- This checks the argument types and
- -- ambiguity of the existential context (if any)
- --
- -- Note [Sept 04] Now that tvs is all the tvs, this
- -- test doesn't actually check anything
--- ; checkFreeness tvs ex_theta }
+ ; checkValidType ctxt (dataConUserType con) }
where
ctxt = ConArgCtxt (dataConName con)
--- (tvs, ex_theta, _, _, _) = dataConSig con
-
-------------------------------
checkValidClass :: Class -> TcM ()
= vcat [ ptext SLIT("Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
, nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow GADTs")) ]
+badStupidTheta tc_name
+ = ptext SLIT("A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
+
newtypeConError tycon n
= sep [ptext SLIT("A newtype must have exactly one constructor,"),
nest 2 $ ptext SLIT("but") <+> quotes (ppr tycon) <+> ptext SLIT("has") <+> speakN n ]
tcSplitForAllTys, tcSplitPhiTy,
tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
- tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys,
+ tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
tcValidInstHeadTy, tcGetTyVar_maybe, tcGetTyVar,
tcSplitSigmaTy, tcMultiSplitSigmaTy,
-- Predicates.
-- Again, newtypes are opaque
tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
+ eqKind,
isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
isDoubleTy, isFloatTy, isIntTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy,
---------------------------------
-- Predicate types
getClassPredTys_maybe, getClassPredTys,
- isClassPred, isTyVarClassPred,
+ isClassPred, isTyVarClassPred, isEqPred,
mkDictTy, tcSplitPredTy_maybe,
isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
unliftedTypeKind, liftedTypeKind, unboxedTypeKind, argTypeKind,
openTypeKind, mkArrowKind, mkArrowKinds,
- isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
- isArgTypeKind, isSubKind, defaultKind,
+ isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind,
+ isSubArgTypeKind, isSubKind, defaultKind,
+ kindVarRef, mkKindVar,
Type, PredType(..), ThetaType,
mkForAllTy, mkForAllTys,
-- Type substitutions
TvSubst(..), -- Representation visible to a few friends
- TvSubstEnv, emptyTvSubst,
+ TvSubstEnv, emptyTvSubst, substEqSpec,
mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
#include "HsVersions.h"
-- friends:
-import TypeRep ( Type(..), funTyCon ) -- friend
+import TypeRep ( Type(..), funTyCon, Kind ) -- friend
import Type ( -- Re-exports
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
- tyVarsOfTheta, Kind, PredType(..),
- ThetaType, unliftedTypeKind, unboxedTypeKind, argTypeKind,
+ tyVarsOfTheta, Kind, PredType(..), KindVar,
+ ThetaType, isUnliftedTypeKind, unliftedTypeKind,
+-- ??? unboxedTypeKind,
+ argTypeKind,
liftedTypeKind, openTypeKind, mkArrowKind,
- isLiftedTypeKind, isUnliftedTypeKind,
+ tySuperKind, isLiftedTypeKind,
mkArrowKinds, mkForAllTy, mkForAllTys,
- defaultKind, isArgTypeKind, isOpenTypeKind,
+ defaultKind, isSubArgTypeKind, isSubOpenTypeKind,
mkFunTy, mkFunTys, zipFunTys,
mkTyConApp, mkAppTy,
mkAppTys, applyTy, applyTys,
isSubKind, tcView,
tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
- tcEqPred, tcCmpPred, tcEqTypeX,
+ tcEqPred, tcCmpPred, tcEqTypeX, eqKind,
TvSubst(..),
TvSubstEnv, emptyTvSubst, mkTvSubst, zipTyEnv,
substTy, substTys, substTyWith, substTheta,
substTyVar, substTyVarBndr, substPred, lookupTyVar,
- typeKind, repType, coreView,
+ typeKind, repType, coreView, repSplitAppTy_maybe,
pprKind, pprParendKind,
pprType, pprParendType, pprTyThingCategory,
pprPred, pprTheta, pprThetaArrow, pprClassPred
-- others:
import DynFlags ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
-import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
+import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc, mkSystemName )
import NameSet
import VarEnv ( TidyEnv )
-import OccName ( OccName, mkDictOcc )
+import OccName ( OccName, mkDictOcc, mkOccName, tvName )
import PrelNames -- Lots (e.g. in isFFIArgumentTy)
import TysWiredIn ( unitTyCon, charTyCon, listTyCon )
import BasicTypes ( IPName(..), Arity, ipNameName )
-- will become type T = forall a. a->a
--
-- With gla-exts that's right, but for H98 we should complain.
+
+---------------------------------
+-- Kind variables:
+
+mkKindName :: Unique -> Name
+mkKindName unique = mkSystemName unique kind_var_occ
+
+kindVarRef :: KindVar -> IORef MetaDetails
+kindVarRef tc =
+ case tcTyVarDetails tc of
+ MetaTv TauTv ref -> ref
+ other -> pprPanic "kindVarRef" (ppr tc)
+
+mkKindVar :: Unique -> IORef MetaDetails -> KindVar
+mkKindVar u r
+ = mkTcTyVar (mkKindName u)
+ tySuperKind -- not sure this is right,
+ -- do we need kind vars for
+ -- coercions?
+ (MetaTv TauTv r)
+
+kind_var_occ :: OccName -- Just one for all KindVars
+ -- They may be jiggled by tidying
+kind_var_occ = mkOccName tvName "k"
+\end{code}
\end{code}
%************************************************************************
-----------------------
tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
-tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
-tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
-tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
- Just (tys', ty') -> Just (TyConApp tc tys', ty')
- Nothing -> Nothing
-tcSplitAppTy_maybe other = Nothing
+tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
+tcSplitAppTy :: Type -> (Type, Type)
tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
Just stuff -> stuff
Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
getClassPredTys (ClassP clas tys) = (clas, tys)
getClassPredTys other = panic "getClassPredTys"
+isEqPred :: PredType -> Bool
+isEqPred (EqPred {}) = True
+isEqPred _ = False
+
mkDictTy :: Class -> [Type] -> Type
mkDictTy clas tys = mkPredTy (ClassP clas tys)
isLinearPred other = False
\end{code}
+--------------------- Equality predicates ---------------------------------
+\begin{code}
+substEqSpec :: TvSubst -> [(TyVar,Type)] -> [(TcType,TcType)]
+substEqSpec subst eq_spec = [ (substTyVar subst tv, substTy subst ty)
+ | (tv,ty) <- eq_spec]
+\end{code}
+
--------------------- The stupid theta (sigh) ---------------------------------
\begin{code}
\begin{code}
tcTyVarsOfType :: Type -> TcTyVarSet
--- Just the tc type variables free in the type
+-- Just the *TcTyVars* free in the type
+-- (Types.tyVarsOfTypes finds all free TyVars)
tcTyVarsOfType (TyVarTy tv) = if isTcTyVar tv then unitVarSet tv
else emptyVarSet
tcTyVarsOfType (TyConApp tycon tys) = tcTyVarsOfTypes tys
module TcType where
import Outputable( SDoc )
+data MetaDetails
+
data TcTyVarDetails
pprTcTyVarDetails :: TcTyVarDetails -> SDoc
\end{code}
TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst,
substTy, substTheta,
lookupTyVar, extendTvSubst )
-import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
+import Type ( Kind, SimpleKind, KindVar,
openTypeKind, liftedTypeKind, unliftedTypeKind,
mkArrowKind, defaultKind,
- isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
- isSubKind, pprKind, splitKindFunTys )
+ argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
+ isSubKind, pprKind, splitKindFunTys, isSubKindCon,
+ isOpenTypeKind, isArgTypeKind )
import TysPrim ( alphaTy, betaTy )
-import Inst ( newDicts, instToId )
+import Inst ( newDicts, instToId, mkInstCoFn )
import TyCon ( TyCon, tyConArity, tyConTyVars, isSynTyCon )
import TysWiredIn ( listTyCon )
import Id ( Id, mkSysLocal )
-- Adding the error context here leads to some very confusing error
-- messages, such as "can't match foarall a. a->a with forall a. a->a"
-- So instead I'm adding it when moving from tc_sub to u_tys
+ traceTc (text "tcSubExp" <+> ppr actual_ty <+> ppr expected_ty) >>
tc_sub Nothing actual_ty actual_ty False expected_ty expected_ty
tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only
tcFunResTy fun actual_ty expected_ty
- = tc_sub (Just fun) actual_ty actual_ty False expected_ty expected_ty
+ = traceTc (text "tcFunResTy" <+> ppr actual_ty <+> ppr expected_ty) >>
+ tc_sub (Just fun) actual_ty actual_ty False expected_ty expected_ty
-----------------
tc_sub :: Maybe Name -- Just fun => we're looking at a function result type
-- Deal with the dictionaries
; dicts <- newDicts InstSigOrigin (substTheta subst' theta)
; extendLIEs dicts
- ; let inst_fn = CoApps (CoTyApps CoHole inst_tys)
- (map instToId dicts)
+ ; let inst_fn = mkInstCoFn inst_tys dicts
; return (co_fn <.> inst_fn) }
-----------------------------------
| otherwise
= do { us <- newUniqueSupply
; let arg_ids = zipWith (mkSysLocal FSLIT("sub")) (uniqsFromSupply us) arg_tys
- ; return (CoLams arg_ids (co_fn_res <.> (CoApps CoHole arg_ids))) }
+ ; return (CoLams arg_ids <.> co_fn_res <.> CoApps arg_ids) }
\end{code}
; traceTc (text "tcGen:done")
; let
- -- This HsLet binds any Insts which came out of the simplification.
- -- It's a bit out of place here, but using AbsBind involves inventing
- -- a couple of new names which seems worse.
- dict_ids = map instToId dicts
- co_fn = CoTyLams forall_tvs $ CoLams dict_ids $ CoLet inst_binds CoHole
+ -- The CoLet binds any Insts which came out of the simplification.
+ dict_ids = map instToId dicts
+ co_fn = CoTyLams forall_tvs <.> CoLams dict_ids <.> CoLet inst_binds
; returnM (co_fn, result) }
where
free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
:: InBox -> TcType -- ty1 is the *expected* type
-> InBox -> TcType -- ty2 is the *actual* type
-> TcM ()
-uTysOuter nb1 ty1 nb2 ty2 = u_tys True nb1 ty1 ty1 nb2 ty2 ty2
-uTys nb1 ty1 nb2 ty2 = u_tys False nb1 ty1 ty1 nb2 ty2 ty2
+uTysOuter nb1 ty1 nb2 ty2 = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
+ ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 }
+uTys nb1 ty1 nb2 ty2 = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
+ ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 }
--------------
| otherwise = brackets (equals <+> ppr ty2)
; traceTc (text "uVar" <+> ppr swapped <+>
sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ),
- nest 2 (ptext SLIT(" :=: ")),
+ nest 2 (ptext SLIT(" <-> ")),
ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion])
; details <- lookupTcTyVar tv1
; case details of
unifyKind :: TcKind -- Expected
-> TcKind -- Actual
-> TcM ()
-unifyKind LiftedTypeKind LiftedTypeKind = returnM ()
-unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
+unifyKind (TyConApp kc1 []) (TyConApp kc2 [])
+ | isSubKindCon kc2 kc1 = returnM ()
-unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
-unifyKind ArgTypeKind k2 | isArgTypeKind k2 = returnM ()
- -- Respect sub-kinding
-
-unifyKind (FunKind a1 r1) (FunKind a2 r2)
- = do { unifyKind a2 a1; unifyKind r1 r2 }
+unifyKind (FunTy a1 r1) (FunTy a2 r2)
+ = do { unifyKind a2 a1; unifyKind r1 r2 }
-- Notice the flip in the argument,
-- so that the sub-kinding works right
-
-unifyKind (KindVar kv1) k2 = uKVar False kv1 k2
-unifyKind k1 (KindVar kv2) = uKVar True kv2 k1
+unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2
+unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1
unifyKind k1 k2 = unifyKindMisMatch k1 k2
unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
uKVar swapped kv1 k2
= do { mb_k1 <- readKindVar kv1
; case mb_k1 of
- Nothing -> uUnboundKVar swapped kv1 k2
- Just k1 | swapped -> unifyKind k2 k1
- | otherwise -> unifyKind k1 k2 }
+ Flexi -> uUnboundKVar swapped kv1 k2
+ Indirect k1 | swapped -> unifyKind k2 k1
+ | otherwise -> unifyKind k1 k2 }
----------------
uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
-uUnboundKVar swapped kv1 k2@(KindVar kv2)
+uUnboundKVar swapped kv1 k2@(TyVarTy kv2)
| kv1 == kv2 = returnM ()
| otherwise -- Distinct kind variables
= do { mb_k2 <- readKindVar kv2
; case mb_k2 of
- Just k2 -> uUnboundKVar swapped kv1 k2
- Nothing -> writeKindVar kv1 k2 }
+ Indirect k2 -> uUnboundKVar swapped kv1 k2
+ Flexi -> writeKindVar kv1 k2 }
uUnboundKVar swapped kv1 non_var_k2
= do { k2' <- zonkTcKind non_var_k2
kindOccurCheck kv1 k2 -- k2 is zonked
= checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
where
- not_in (KindVar kv2) = kv1 /= kv2
- not_in (FunKind a2 r2) = not_in a2 && not_in r2
- not_in other = True
+ not_in (TyVarTy kv2) = kv1 /= kv2
+ not_in (FunTy a2 r2) = not_in a2 && not_in r2
+ not_in other = True
kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
-- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
kindSimpleKind orig_swapped orig_kind
= go orig_swapped orig_kind
where
- go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1
- ; k2' <- go sw k2
- ; return (FunKind k1' k2') }
- go True OpenTypeKind = return liftedTypeKind
- go True ArgTypeKind = return liftedTypeKind
- go sw LiftedTypeKind = return liftedTypeKind
- go sw UnliftedTypeKind = return unliftedTypeKind
- go sw k@(KindVar _) = return k -- KindVars are always simple
+ go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1
+ ; k2' <- go sw k2
+ ; return (mkArrowKind k1' k2') }
+ go True k
+ | isOpenTypeKind k = return liftedTypeKind
+ | isArgTypeKind k = return liftedTypeKind
+ go sw k
+ | isLiftedTypeKind k = return liftedTypeKind
+ | isUnliftedTypeKind k = return unliftedTypeKind
+ go sw k@(TyVarTy _) = return k -- KindVars are always simple
go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
<+> ppr orig_swapped <+> ppr orig_kind)
-- I think this can't actually happen
unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
-- Like unifyFunTy, but does not fail; instead just returns Nothing
-unifyFunKind (KindVar kvar)
- = readKindVar kvar `thenM` \ maybe_kind ->
+unifyFunKind (TyVarTy kvar)
+ = readKindVar kvar `thenM` \ maybe_kind ->
case maybe_kind of
- Just fun_kind -> unifyFunKind fun_kind
- Nothing -> do { arg_kind <- newKindVar
- ; res_kind <- newKindVar
- ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
- ; returnM (Just (arg_kind,res_kind)) }
+ Indirect fun_kind -> unifyFunKind fun_kind
+ Flexi ->
+ do { arg_kind <- newKindVar
+ ; res_kind <- newKindVar
+ ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
+ ; returnM (Just (arg_kind,res_kind)) }
-unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
-unifyFunKind other = returnM Nothing
+unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
+unifyFunKind other = returnM Nothing
\end{code}
%************************************************************************
projects / ghc-hetmet.git / commitdiff