X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcPat.lhs;h=a4f3a82521385903f2bf4e57a42c9b83d1caf658;hb=bf40e268d916947786c56ec38db86190854a2d2c;hp=33b76302c9199e6b220feb625bca768522f9cd3d;hpb=3e83dfb21b2f2220dce97427fff5c19459ae68d1;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index 33b7630..a4f3a82 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -5,21 +5,23 @@ \begin{code} module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit, - badFieldCon, polyPatSig ) where + addDataConStupidTheta, badFieldCon, polyPatSig ) where #include "HsVersions.h" import {-# SOURCE #-} TcExpr( tcSyntaxOp ) -import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..), - mkCoPat, idCoercion, +import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), + HsOverLit(..), HsExpr(..), HsWrapper(..), + mkCoPat, LHsBinds, emptyLHsBinds, isEmptyLHsBinds, collectPatsBinders, nlHsLit ) import TcHsSyn ( TcId, hsLitType ) import TcRnMonad import Inst ( InstOrigin(..), shortCutFracLit, shortCutIntLit, - newDicts, instToId, tcInstStupidTheta, isHsVar + newDictBndrs, instToId, instStupidTheta, isHsVar ) import Id ( Id, idType, mkLocalId ) +import Var ( CoVar, tyVarKind ) import CoreFVs ( idFreeTyVars ) import Name ( Name, mkSystemVarName ) import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns ) @@ -27,27 +29,31 @@ import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2, tcLookupClass, tcLookupDataCon, refineEnvironment, tcLookupField, tcMetaTy ) import TcMType ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, -+ newCoVars, zonkTcType ) + newCoVars, zonkTcType, tcInstTyVars, newBoxyTyVar ) import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType, BoxyType, SkolemInfo(PatSkol), BoxySigmaType, BoxyRhoType, argTypeKind, typeKind, pprSkolTvBinding, isRigidTy, tcTyVarsOfTypes, - zipTopTvSubst, isArgTypeKind, isUnboxedTupleType, + zipTopTvSubst, isSubArgTypeKind, isUnboxedTupleType, mkTyVarTys, mkClassPred, isOverloadedTy, substEqSpec, - mkFunTy, mkFunTys, tidyOpenType, tidyOpenTypes ) + mkFunTy, mkFunTys, tidyOpenType, tidyOpenTypes, + mkTyVarTy ) import VarSet ( elemVarSet ) import {- Kind parts of -} Type ( liftedTypeKind ) import TcUnify ( boxySplitTyConApp, boxySplitListTy, unBox, - zapToMonotype, boxyUnify, checkSigTyVarsWrt, - unifyType ) + zapToMonotype, boxyUnify, boxyUnifyList, + checkSigTyVarsWrt, unifyType ) import TcHsType ( UserTypeCtxt(..), tcPatSig ) import TysWiredIn ( boolTy, parrTyCon, tupleTyCon ) -import Type ( substTys, substTheta ) +import TcGadt ( Refinement, emptyRefinement, gadtRefine, refineType ) +import Type ( Type, mkTyConApp, substTys, substTheta ) import StaticFlags ( opt_IrrefutableTuples ) -import TyCon ( TyCon, FieldLabel ) +import TyCon ( TyCon, FieldLabel, tyConFamInst_maybe, + tyConFamilyCoercion_maybe, tyConTyVars ) import DataCon ( DataCon, dataConTyCon, dataConFullSig, dataConName, - dataConFieldLabels, dataConSourceArity ) + dataConFieldLabels, dataConSourceArity, + dataConStupidTheta, dataConUnivTyVars ) import PrelNames ( integralClassName, fromIntegerName, integerTyConName, fromRationalName, rationalTyConName ) import BasicTypes ( isBoxed ) @@ -224,7 +230,7 @@ unBoxArgType ty pp_this -- but they improve error messages, and allocate fewer tyvars ; if isUnboxedTupleType ty' then failWithTc msg - else if isArgTypeKind (typeKind ty') then + else if isSubArgTypeKind (typeKind ty') then return ty' else do -- OpenTypeKind, so constrain it { ty2 <- newFlexiTyVarTy argTypeKind @@ -460,8 +466,7 @@ tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside -- The Report says that n+k patterns must be in Integral -- We may not want this when using re-mappable syntax, though (ToDo?) ; icls <- tcLookupClass integralClassName - ; dicts <- newDicts orig [mkClassPred icls [pat_ty']] - ; extendLIEs dicts + ; instStupidTheta orig [mkClassPred icls [pat_ty']] ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate) ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) } @@ -477,6 +482,61 @@ tc_pat _ _other_pat _ _ = panic "tc_pat" -- DictPat, ConPatOut, SigPatOut, VarP %* * %************************************************************************ +[Pattern matching indexed data types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider the following declarations: + + data family Map k :: * -> * + data instance Map (a, b) v = MapPair (Map a (Pair b v)) + +and a case expression + + case x :: Map (Int, c) w of MapPair m -> ... + +As explained by [Wrappers for data instance tycons] in MkIds.lhs, the +worker/wrapper types for MapPair are + + $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v + $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v + +So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is +:R123Map, which means the straight use of boxySplitTyConApp would give a type +error. Hence, the smart wrapper function boxySplitTyConAppWithFamily calls +boxySplitTyConApp with the family tycon Map instead, which gives us the family +type list {(Int, c), w}. To get the correct split for :R123Map, we need to +unify the family type list {(Int, c), w} with the instance types {(a, b), v} +(provided by tyConFamInst_maybe together with the family tycon). This +unification yields the substitution [a -> Int, b -> c, v -> w], which gives us +the split arguments for the representation tycon :R123Map as {Int, c, w} + +In other words, boxySplitTyConAppWithFamily implicitly takes the coercion + + Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v} + +moving between representation and family type into account. To produce type +correct Core, this coercion needs to be used to case the type of the scrutinee +from the family to the representation type. This is achieved by +unwrapFamInstScrutinee using a CoPat around the result pattern. + +Now it might appear seem as if we could have used the existing GADT type +refinement infrastructure of refineAlt and friends instead of the explicit +unification and CoPat generation. However, that would be wrong. Why? The +whole point of GADT refinement is that the refinement is local to the case +alternative. In contrast, the substitution generated by the unification of +the family type list and instance types needs to be propagated to the outside. +Imagine that in the above example, the type of the scrutinee would have been +(Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the +substitution [x -> (a, b), v -> w]. In contrast to GADT matching, the +instantiation of x with (a, b) must be global; ie, it must be valid in *all* +alternatives of the case expression, whereas in the GADT case it might vary +between alternatives. + +In fact, if we have a data instance declaration defining a GADT, eq_spec will +be non-empty and we will get a mixture of global instantiations and local +refinement from a single match. This neatly reflects that, as soon as we +have constrained the type of the scrutinee to the required type index, all +further type refinement is local to the alternative. + \begin{code} -- Running example: -- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a @@ -490,9 +550,10 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside = 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 + origin = SigOrigin skol_info -- Instantiate the constructor type variables [a->ty] - ; ctxt_res_tys <- boxySplitTyConApp tycon pat_ty + ; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs ; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs) (ctxt_res_tys ++ mkTyVarTys ex_tvs') @@ -501,27 +562,70 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside 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 + ; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $ tcConArgs data_con arg_tys' arg_pats pstate' thing_inside - ; dicts <- newDicts (SigOrigin skol_info) theta' + ; loc <- getInstLoc origin + ; dicts <- newDictBndrs loc theta' ; dict_binds <- tcSimplifyCheck doc ex_tvs' dicts lie_req - ; tcInstStupidTheta data_con ctxt_res_tys + ; addDataConStupidTheta data_con ctxt_res_tys - ; 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) + ; return + (unwrapFamInstScrutinee tycon ctxt_res_tys $ + 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) + -- Split against the family tycon if the pattern constructor belongs to a + -- representation tycon. + -- + boxySplitTyConAppWithFamily tycon pat_ty = + traceTc traceMsg >> + case tyConFamInst_maybe tycon of + Nothing -> boxySplitTyConApp tycon pat_ty + Just (fam_tycon, instTys) -> + do { scrutinee_arg_tys <- boxySplitTyConApp fam_tycon pat_ty + ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon) + ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys + ; return freshTvs + } + where + traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+> + ppr tycon <+> ppr pat_ty + , text " family instance:" <+> + ppr (tyConFamInst_maybe tycon) + ] + + -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion + -- pattern if the tycon is an instance of a family. + -- + unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id + unwrapFamInstScrutinee tycon args pat + | Just co_con <- tyConFamilyCoercion_maybe tycon +-- , not (isNewTyCon tycon) -- newtypes are explicitly unwrapped by + -- the desugarer + -- NB: We can use CoPat directly, rather than mkCoPat, as we know the + -- coercion is not the identity; mkCoPat is inconvenient as it + -- wants a located pattern. + = CoPat (WpCo $ mkTyConApp co_con args) -- co fam ty to repr ty + (pat {pat_ty = mkTyConApp tycon args}) -- representation type + pat_ty -- family inst type + | otherwise + = pat + + tcConArgs :: DataCon -> [TcSigmaType] - -> Checker (HsConDetails Name (LPat Name)) (HsConDetails Id (LPat Id)) + -> Checker (HsConDetails Name (LPat Name)) + (HsConDetails Id (LPat Id)) tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside = do { checkTc (con_arity == no_of_args) -- Check correct arity @@ -543,6 +647,9 @@ tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside where con_arity = dataConSourceArity data_con +tcConArgs data_con other_args (InfixCon p1 p2) pstate thing_inside + = pprPanic "tcConArgs" (ppr data_con) -- InfixCon always has two arguments + 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) } @@ -589,6 +696,22 @@ tcConArg (arg_pat, arg_ty) pstate thing_inside -- refinements from peer argument patterns to the left \end{code} +\begin{code} +addDataConStupidTheta :: DataCon -> [TcType] -> TcM () +-- Instantiate the "stupid theta" of the data con, and throw +-- the constraints into the constraint set +addDataConStupidTheta data_con inst_tys + | null stupid_theta = return () + | otherwise = instStupidTheta origin inst_theta + where + origin = OccurrenceOf (dataConName data_con) + -- The origin should always report "occurrence of C" + -- even when C occurs in a pattern + stupid_theta = dataConStupidTheta data_con + tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys + inst_theta = substTheta tenv stupid_theta +\end{code} + %************************************************************************ %* * @@ -633,7 +756,10 @@ refineAlt con pstate ex_tvs co_vars pat_ty -- might be inside a lazy pattern. Instead, refine pstate where - trace_msg = text "refineAlt:match" <+> ppr con <+> ppr reft + trace_msg = text "refineAlt:match" <+> + vcat [ ppr con <+> ppr ex_tvs, + ppr [(v, tyVarKind v) | v <- co_vars], + ppr reft] } \end{code}