diff options
| -rw-r--r-- | compiler/typecheck/Inst.lhs | 77 | ||||
| -rw-r--r-- | compiler/typecheck/TcArrows.lhs | 45 | ||||
| -rw-r--r-- | compiler/typecheck/TcBinds.lhs | 21 | ||||
| -rw-r--r-- | compiler/typecheck/TcDeriv.lhs | 6 | ||||
| -rw-r--r-- | compiler/typecheck/TcEnv.lhs | 62 | ||||
| -rw-r--r-- | compiler/typecheck/TcExpr.lhs | 164 | ||||
| -rw-r--r-- | compiler/typecheck/TcHsSyn.lhs | 114 | ||||
| -rw-r--r-- | compiler/typecheck/TcHsType.lhs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcMType.lhs | 95 | ||||
| -rw-r--r-- | compiler/typecheck/TcMatches.lhs | 96 | ||||
| -rw-r--r-- | compiler/typecheck/TcPat.lhs | 440 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnDriver.lhs | 10 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnMonad.lhs | 55 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.lhs | 21 | ||||
| -rw-r--r-- | compiler/typecheck/TcSimplify.lhs | 13 | ||||
| -rw-r--r-- | compiler/typecheck/TcSplice.lhs | 6 | ||||
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.lhs | 160 | ||||
| -rw-r--r-- | compiler/typecheck/TcType.lhs | 79 | ||||
| -rw-r--r-- | compiler/typecheck/TcType.lhs-boot | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcUnify.lhs | 106 |
20 files changed, 832 insertions, 742 deletions
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 77ca56a10e..8971320491 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -12,7 +12,7 @@ module Inst ( tidyInsts, tidyMoreInsts, - newDicts, newDictAtLoc, newDictsAtLoc, cloneDict, + newDicts, newDictsAtLoc, cloneDict, shortCutFracLit, shortCutIntLit, newIPDict, newMethod, newMethodFromName, newMethodWithGivenTy, tcInstClassOp, tcInstStupidTheta, @@ -22,6 +22,7 @@ module Inst ( ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts, instLoc, getDictClassTys, dictPred, + mkInstCoFn, lookupInst, LookupInstResult(..), lookupPred, tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag, @@ -30,7 +31,7 @@ module Inst ( isTyVarDict, isMethodFor, zonkInst, zonkInsts, - instToId, instName, + instToId, instToVar, instName, InstOrigin(..), InstLoc(..), pprInstLoc ) where @@ -40,8 +41,8 @@ module Inst ( 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(..), @@ -69,10 +70,11 @@ import Type ( TvSubst, substTy, substTyVar, substTyWith, substTheta, zipTopTvSub 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 ) @@ -95,13 +97,23 @@ import Outputable 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 @@ -207,29 +219,28 @@ newDicts orig theta = 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 @@ -265,7 +276,7 @@ tcInstStupidTheta data_con inst_tys ; 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 @@ -580,8 +591,9 @@ lookupInst :: Inst -> TcM LookupInstResult -- 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 @@ -654,14 +666,15 @@ lookupInst (Dict _ pred 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)) }}}} --------------- diff --git a/compiler/typecheck/TcArrows.lhs b/compiler/typecheck/TcArrows.lhs index 3bfa9b4757..b4afcaf30a 100644 --- a/compiler/typecheck/TcArrows.lhs +++ b/compiler/typecheck/TcArrows.lhs @@ -22,7 +22,8 @@ import TcType ( TcType, TcTauType, BoxyRhoType, mkFunTys, mkTyConApp, 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 ) @@ -32,7 +33,7 @@ import VarSet import TysPrim ( alphaTyVar ) import Type ( Kind, mkArrowKinds, liftedTypeKind, openTypeKind, tyVarsOfTypes ) -import SrcLoc ( Located(..) ) +import SrcLoc ( Located(..), noLoc, unLoc ) import Outputable import Util ( lengthAtLeast ) @@ -54,8 +55,8 @@ tcProc pat cmd exp_ty 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} @@ -79,20 +80,29 @@ mkCmdArrTy env t1 t2 = mkAppTys (cmd_arr env) [t1, t2] --------------------------------------- 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 @@ -120,7 +130,7 @@ tc_cmd env in_cmd@(HsCase scrut matches) (stk, 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 @@ -169,7 +179,6 @@ tc_cmd env cmd@(HsApp fun arg) (cmd_stk, res_ty) ------------------------------------------- -- 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) $ @@ -180,7 +189,7 @@ tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats maybe_rhs_sig g -- 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') @@ -199,9 +208,8 @@ tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats maybe_rhs_sig g ; 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') } ------------------------------------------- @@ -209,8 +217,8 @@ tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats maybe_rhs_sig g 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 @@ -256,7 +264,9 @@ tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty) -- 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 @@ -264,7 +274,6 @@ tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty) 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 @@ -284,7 +293,7 @@ tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty) 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]) diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs index 7b4e5ecb43..9cc66e3951 100644 --- a/compiler/typecheck/TcBinds.lhs +++ b/compiler/typecheck/TcBinds.lhs @@ -30,14 +30,14 @@ import TcHsSyn ( zonkId ) 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, @@ -48,9 +48,8 @@ import TcType ( TcType, TcTyVar, TcThetaType, 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 ) @@ -323,7 +322,7 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc binds 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) @@ -448,15 +447,14 @@ tcSpecPrag poly_id hs_ty inl -- 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) @@ -651,9 +649,8 @@ tcLhs sig_fn bind@(PatBind { pat_lhs = pat, pat_rhs = grhss }) | (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. diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs index 0a8a498232..46e702c9a3 100644 --- a/compiler/typecheck/TcDeriv.lhs +++ b/compiler/typecheck/TcDeriv.lhs @@ -39,14 +39,14 @@ import Maybes ( catMaybes ) 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 @@ -653,7 +653,7 @@ cond_typeableOK :: Condition -- (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") diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs index be1ce9b964..19deca9e4c 100644 --- a/compiler/typecheck/TcEnv.lhs +++ b/compiler/typecheck/TcEnv.lhs @@ -19,7 +19,7 @@ module TcEnv( tcExtendKindEnv, tcExtendKindEnvTvs, tcExtendTyVarEnv, tcExtendTyVarEnv2, tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2, - tcLookup, tcLookupLocated, tcLookupLocalIds, tcLookupLocalId_maybe, + tcLookup, tcLookupLocated, tcLookupLocalIds, tcLookupId, tcLookupTyVar, getScopedTyVarBinds, lclEnvElts, getInLocalScope, findGlobals, wrongThingErr, pprBinders, @@ -44,7 +44,8 @@ module TcEnv( #include "HsVersions.h" import HsSyn ( LRuleDecl, LHsBinds, LSig, - LHsTyVarBndr, HsTyVarBndr(..), pprLHsBinds ) + LHsTyVarBndr, HsTyVarBndr(..), pprLHsBinds, + ExprCoFn(..), idCoercion, (<.>) ) import TcIface ( tcImportDecl ) import IfaceEnv ( newGlobalBinder ) import TcRnMonad @@ -54,6 +55,7 @@ import TcType ( Type, TcKind, TcTyVar, TcTyVarSet, TcType, TvSubst, 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 ) @@ -216,21 +218,16 @@ tcLookupTyVar name 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 @@ -241,8 +238,9 @@ tcLookupLocalIds ns 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) @@ -322,8 +320,13 @@ tcExtendIdEnv2 names_w_ids thing_inside 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 @@ -360,7 +363,7 @@ findGlobals tvs tidy_env 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) @@ -393,16 +396,20 @@ find_thing _ _ thing = pprPanic "find_thing" (ppr thing) \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} %************************************************************************ @@ -415,11 +422,6 @@ refineEnvironment reft thing_inside 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. diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index 0da370bd4e..43360c7edf 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -21,39 +21,47 @@ import qualified DsMeta #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 ) @@ -68,7 +76,7 @@ import PrimOp ( tagToEnumKey ) 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 ) @@ -282,7 +290,7 @@ tcExpr (HsCase scrut matches) exp_ty ; 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) $ @@ -440,7 +448,7 @@ tcExpr expr@(RecordUpd record_expr rbinds _ _) res_ty -- 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 @@ -633,10 +641,11 @@ tcIdApp :: Name -- Function -- 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 @@ -678,7 +687,7 @@ tcIdApp fun_name n_args arg_checker res_ty -- 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} @@ -707,10 +716,10 @@ tcId :: InstOrigin -> 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 @@ -722,7 +731,7 @@ tcId orig fun_name 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] @@ -756,49 +765,49 @@ tcSyntaxOp orig (HsVar op) ty = tcId orig op ty 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] @@ -925,40 +934,53 @@ tagToEnumError tys %************************************************************************ \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) @@ -1005,6 +1027,8 @@ thBrackId orig id_name id ps_var lie_var ; writeMutVar ps_var ((id_name, nlHsApp (nlHsVar lift) (nlHsVar id)) : ps) ; return id } } + where + id_name = idName id #endif /* GHCI */ \end{code} @@ -1048,7 +1072,7 @@ tcRecordBinds data_con arg_tys rbinds | 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 diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs index bfec766e20..8ab91ce893 100644 --- a/compiler/typecheck/TcHsSyn.lhs +++ b/compiler/typecheck/TcHsSyn.lhs @@ -8,9 +8,9 @@ checker. \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, @@ -30,9 +30,8 @@ import HsSyn -- oodles of it 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, @@ -42,7 +41,7 @@ import TysWiredIn ( charTy, stringTy, intTy, 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 @@ -63,33 +62,34 @@ import Outputable %* * %************************************************************************ -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) @@ -495,28 +495,6 @@ zonkExpr env (HsCoreAnn lbl expr) = 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 @@ -554,24 +532,21 @@ zonk_cmd_top env (HsCmdTop cmd stack_tys ty ids) ------------------------------------------------------------------------- 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') } ------------------------------------------------------------------------- @@ -739,14 +714,15 @@ zonk_pat env (TuplePat pats boxed ty) ; (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) @@ -953,7 +929,7 @@ mkArbitraryType tv 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 diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index 8411631d8a..6a43e2396c 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -45,7 +45,7 @@ import TcType ( Type, PredType(..), ThetaType, BoxySigmaType, 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 ) diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 11ec9d9232..4542a34a0a 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -23,6 +23,10 @@ module TcMType ( newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, -------------------------------- + -- Creating new coercion variables + newCoVars, + + -------------------------------- -- Instantiation tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, tcInstSigTyVars, zonkSigTyVar, @@ -58,10 +62,11 @@ import TypeRep ( Type(..), PredType(..), -- Friend; can see representation 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, @@ -70,21 +75,23 @@ import TcType ( TcType, TcThetaType, TcTauType, TcPredType, 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: @@ -95,6 +102,7 @@ import VarSet import DynFlags ( dopt, DynFlag(..) ) import Util ( nOfThem, isSingleton, notNull ) import ListSetOps ( removeDups ) +import UniqSupply ( uniqsFromSupply ) import Outputable import Control.Monad ( when ) @@ -139,10 +147,17 @@ tcInstType inst_tyvars ty %************************************************************************ \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 ()) @@ -442,6 +457,10 @@ zonkTcPredType (ClassP c ts) 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 @@ -566,10 +585,13 @@ zonkType unbound_var_fn ty 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 @@ -593,35 +615,20 @@ zonk_tc_tyvar unbound_var_fn tyvar %************************************************************************ \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} %************************************************************************ @@ -686,11 +693,11 @@ checkValidType ctxt ty 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 @@ -776,7 +783,7 @@ check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty -- 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) @@ -888,12 +895,12 @@ check_valid_theta ctxt [] 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_` @@ -909,7 +916,7 @@ check_source_ty dflags ctxt pred@(ClassP cls tys) 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 @@ -920,7 +927,7 @@ check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty -- 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 @@ -1024,7 +1031,7 @@ checkThetaCtxt ctxt theta = 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) @@ -1184,6 +1191,7 @@ fvTypes tys = concat (map fvType tys) 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 @@ -1202,4 +1210,5 @@ sizeTypes xs = sum (map sizeType xs) sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' sizePred (IParam _ ty) = sizeType ty +sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 \end{code} diff --git a/compiler/typecheck/TcMatches.lhs b/compiler/typecheck/TcMatches.lhs index 27d1e9b3b6..61faca8d3e 100644 --- a/compiler/typecheck/TcMatches.lhs +++ b/compiler/typecheck/TcMatches.lhs @@ -6,7 +6,7 @@ \begin{code} module TcMatches ( tcMatchesFun, tcGRHSsPat, tcMatchesCase, tcMatchLambda, matchCtxt, TcMatchCtxt(..), - tcStmts, tcDoStmts, + tcStmts, tcDoStmts, tcBody, tcDoStmt, tcMDoStmt, tcGuardStmt ) where @@ -16,16 +16,18 @@ import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcInferRho, tcMonoExpr, tcPolyExpr ) 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, @@ -42,7 +44,6 @@ import Id ( idType, mkLocalId ) import TyCon ( TyCon ) import Outputable import SrcLoc ( Located(..), getLoc ) -import ErrUtils ( Message ) \end{code} %************************************************************************ @@ -85,7 +86,7 @@ tcMatchesFun fun_name matches exp_ty 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 @@ -112,17 +113,19 @@ tcMatchLambda match res_ty -- 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} @@ -142,7 +145,7 @@ tcMatches :: TcMatchCtxt 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 _) @@ -161,7 +164,7 @@ tcMatch ctxt pat_tys rhs_ty match 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') } @@ -169,13 +172,14 @@ tcMatch ctxt pat_tys rhs_ty match = 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 @@ -190,7 +194,7 @@ tcGRHSs ctxt (GRHSs grhss binds) res_ty ; 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 $ @@ -215,21 +219,24 @@ tcDoStmts :: HsStmtContext Name -> 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 @@ -238,8 +245,9 @@ 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 @@ -247,10 +255,12 @@ tcDoStmts ctxt@(MDoExpr _) stmts body res_ty 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} @@ -262,11 +272,11 @@ tcBody ctxt body res_ty \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 @@ -274,8 +284,8 @@ type TcStmtChecker 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 @@ -312,7 +322,7 @@ tcGuardStmt ctxt (ExprStmt guard _ _) res_ty thing_inside 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 @@ -329,7 +339,7 @@ tcLcStmt :: TyCon -- The list/Parray type constructor ([] or PArray) 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 @@ -385,7 +395,7 @@ tcLcStmt m_tc ctxt stmt elt_ty thing_inside 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. @@ -395,7 +405,7 @@ tcDoStmt m_ty ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside -- 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, @@ -409,14 +419,14 @@ tcDoStmt m_ty ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside ; 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 @@ -432,7 +442,7 @@ tcMDoStmt :: (LHsExpr Name -> TcM (LHsExpr TcId, TcType)) -- RHS inference -> 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 @@ -506,10 +516,6 @@ checkArgs fun other = panic "TcPat.checkArgs" -- Matches always non-empty 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} diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 56c525831e..33b76302c9 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -4,13 +4,14 @@ \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 ) @@ -23,35 +24,37 @@ import CoreFVs ( idFreeTyVars ) 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} @@ -64,12 +67,26 @@ import FastString %************************************************************************ \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, @@ -79,36 +96,42 @@ tcPats :: PatCtxt -- 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 @@ -120,20 +143,16 @@ tcCheckExistentialPat :: PatCtxt -- 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 @@ -235,46 +254,57 @@ Hence the getErrCtxt/setErrCtxt stuff in tc_lpats. \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 @@ -295,11 +325,11 @@ tc_pat pstate (VarPat name) pat_ty thing_inside ; 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 @@ -313,7 +343,7 @@ tc_pat pstate (BangPat pat) pat_ty thing_inside -- 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 @@ -335,7 +365,7 @@ tc_pat pstate (WildPat _) pat_ty thing_inside 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 @@ -350,7 +380,7 @@ tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside 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 @@ -360,20 +390,21 @@ 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. @@ -447,118 +478,82 @@ tc_pat _ _other_pat _ _ = panic "tc_pat" -- DictPat, ConPatOut, SigPatOut, VarP %************************************************************************ \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 @@ -577,13 +572,21 @@ tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside -- 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} @@ -594,69 +597,44 @@ tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside %************************************************************************ \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} @@ -799,11 +777,11 @@ patCtxt pat = Just (hang (ptext SLIT("In the pattern:")) ----------------------------------------------- -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 @@ -841,6 +819,10 @@ lazyPatErr pat tvs 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} diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs index 9e1bfb97a5..0a4895f63a 100644 --- a/compiler/typecheck/TcRnDriver.lhs +++ b/compiler/typecheck/TcRnDriver.lhs @@ -113,7 +113,7 @@ import MkId ( unsafeCoerceId ) 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 ) @@ -997,10 +997,12 @@ tcGhciStmts stmts -- 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 diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs index 0b5e4fc72a..af75fe6e49 100644 --- a/compiler/typecheck/TcRnMonad.lhs +++ b/compiler/typecheck/TcRnMonad.lhs @@ -132,33 +132,8 @@ initTc hsc_env hsc_src mod do_this -- 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 } ; @@ -191,6 +166,32 @@ initTcPrintErrors env mod todo = do 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} %************************************************************************ %* * diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index 3b1247790a..f66abdc679 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -21,7 +21,6 @@ module TcRnTypes( -- Typechecker types TcTyThing(..), pprTcTyThingCategory, - GadtRefinement, -- Template Haskell ThStage(..), topStage, topSpliceStage, @@ -44,7 +43,7 @@ module TcRnTypes( import HsSyn ( PendingSplice, HsOverLit, LRuleDecl, LForeignDecl, ArithSeqInfo, DictBinds, LHsBinds, LImportDecl, HsGroup, - IE ) + ExprCoFn, IE ) import HscTypes ( FixityEnv, HscEnv, TypeEnv, TyThing, GenAvailInfo(..), AvailInfo, HscSource(..), @@ -324,7 +323,6 @@ data TcLclEnv -- Changes as we move inside an expression tcl_lie :: TcRef LIE -- Place to accumulate type constraints } -type GadtRefinement = TvSubst {- Note [Given Insts] ~~~~~~~~~~~~~~~~~~ @@ -419,9 +417,15 @@ escapeArrowScope 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 @@ -432,8 +436,9 @@ data TcTyThing 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 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 1998cd2bc4..8f062704aa 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -21,8 +21,9 @@ module TcSimplify ( #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(..), @@ -31,7 +32,7 @@ import Inst ( lookupInst, LookupInstResult(..), isMethodFor, isMethod, instToId, tyVarsOfInsts, cloneDict, ipNamesOfInsts, ipNamesOfInst, dictPred, - fdPredsOfInst, + fdPredsOfInst, mkInstCoFn, newDictsAtLoc, tcInstClassOp, getDictClassTys, isTyVarDict, instLoc, zonkInst, tidyInsts, tidyMoreInsts, @@ -1468,6 +1469,7 @@ extractResults avails wanteds 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') @@ -1540,7 +1542,7 @@ split n split_id root_id wanted 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) @@ -1922,7 +1924,8 @@ addSCs is_loop avails dict | 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 diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs index 6ac66d6ea8..d59b0f8852 100644 --- a/compiler/typecheck/TcSplice.lhs +++ b/compiler/typecheck/TcSplice.lhs @@ -567,9 +567,9 @@ reifyThing (AGlobal (ADataCon dc)) ; 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) } diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index 090db01ca6..3cf6145a5c 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -33,21 +33,20 @@ import TcHsType ( kcHsTyVars, kcHsLiftedSigType, kcHsType, 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 ) @@ -58,7 +57,7 @@ import Unify ( tcMatchTys, tcMatchTyX ) 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, @@ -427,8 +426,11 @@ tcTyClDecl1 calc_isrec -- 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) @@ -440,16 +442,16 @@ tcTyClDecl1 calc_isrec { 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) } @@ -498,10 +500,12 @@ tcConDecl unbox_strict NewType tycon tc_tvs -- Newtypes = 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) @@ -517,27 +521,16 @@ tcConDecl unbox_strict DataType tycon tc_tvs -- Data types (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. @@ -551,19 +544,48 @@ tcConDecl unbox_strict DataType tycon tc_tvs -- Data types } -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 @@ -634,7 +656,7 @@ checkValidTyCl decl -- of the constructor. checkValidTyCon :: TyCon -> TcM () -checkValidTyCon tc +checkValidTyCon tc | isSynTyCon tc = checkValidType syn_ctxt syn_rhs | otherwise @@ -658,14 +680,20 @@ checkValidTyCon tc 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 @@ -674,7 +702,7 @@ checkValidTyCon tc -- 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 @@ -682,7 +710,7 @@ checkValidTyCon tc = 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 @@ -699,18 +727,9 @@ checkValidDataCon tc con = 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 () @@ -840,6 +859,9 @@ badGadtDecl tc_name = 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 ] diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index a21f0fba8b..06eb0dcc08 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -42,7 +42,7 @@ module TcType ( 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, @@ -50,6 +50,7 @@ module TcType ( -- Predicates. -- Again, newtypes are opaque tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX, + eqKind, isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy, isDoubleTy, isFloatTy, isIntTy, isStringTy, isIntegerTy, isBoolTy, isUnitTy, @@ -64,7 +65,7 @@ module TcType ( --------------------------------- -- Predicate types getClassPredTys_maybe, getClassPredTys, - isClassPred, isTyVarClassPred, + isClassPred, isTyVarClassPred, isEqPred, mkDictTy, tcSplitPredTy_maybe, isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, @@ -90,8 +91,9 @@ module TcType ( 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, @@ -101,7 +103,7 @@ module TcType ( -- 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, @@ -127,16 +129,18 @@ module TcType ( #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, @@ -151,7 +155,7 @@ import Type ( -- Re-exports isSubKind, tcView, tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, - tcEqPred, tcCmpPred, tcEqTypeX, + tcEqPred, tcCmpPred, tcEqTypeX, eqKind, TvSubst(..), TvSubstEnv, emptyTvSubst, mkTvSubst, zipTyEnv, @@ -161,7 +165,7 @@ import Type ( -- Re-exports 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 @@ -176,10 +180,10 @@ import VarSet -- 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 ) @@ -385,6 +389,31 @@ data UserTypeCtxt -- 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} %************************************************************************ @@ -708,13 +737,9 @@ tcFunResultTy ty = snd (tcSplitFunTy ty) ----------------------- 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) @@ -820,6 +845,10 @@ getClassPredTys :: PredType -> (Class, [Type]) 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) @@ -853,6 +882,13 @@ isLinearPred (IParam (Linear n) _) = True 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} @@ -937,7 +973,8 @@ deNoteType ty = ty \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 diff --git a/compiler/typecheck/TcType.lhs-boot b/compiler/typecheck/TcType.lhs-boot index 191badd943..15c23676bc 100644 --- a/compiler/typecheck/TcType.lhs-boot +++ b/compiler/typecheck/TcType.lhs-boot @@ -2,6 +2,8 @@ module TcType where import Outputable( SDoc ) +data MetaDetails + data TcTyVarDetails pprTcTyVarDetails :: TcTyVarDetails -> SDoc \end{code} diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 5b02241ce2..1295ab3dfe 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -54,13 +54,14 @@ import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType, 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 ) @@ -601,11 +602,13 @@ tcSubExp actual_ty expected_ty -- 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 @@ -700,8 +703,7 @@ tc_sub1 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty -- 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) } ----------------------------------- @@ -746,7 +748,7 @@ wrapFunResCoercion arg_tys co_fn_res | 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} @@ -807,11 +809,9 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall ; 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 @@ -921,8 +921,10 @@ uTysOuter, uTys :: 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 } -------------- @@ -1101,7 +1103,7 @@ uVar outer swapped tv1 nb2 ps_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 @@ -1581,20 +1583,15 @@ Unifying kinds is much, much simpler than unifying types. 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 () @@ -1608,19 +1605,19 @@ uKVar :: Bool -> KindVar -> 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 @@ -1637,9 +1634,9 @@ uUnboundKVar swapped kv1 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 @@ -1649,14 +1646,16 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind 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 @@ -1685,17 +1684,18 @@ unifyKindMisMatch ty1 ty2 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} %************************************************************************ |