%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
-\section[TcPat]{Typechecking patterns}
+
+TcPat: Typechecking patterns
\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,
- LHsBinds, emptyLHsBinds, isEmptyLHsBinds,
- collectPatsBinders, nlHsLit )
-import TcHsSyn ( TcId, hsLitType )
+
+import HsSyn
+import TcHsSyn
import TcRnMonad
-import Inst ( InstOrigin(..), shortCutFracLit, shortCutIntLit,
- newDicts, instToId, tcInstStupidTheta, isHsVar
- )
-import Id ( Id, idType, mkLocalId )
-import CoreFVs ( idFreeTyVars )
-import Name ( Name, mkSystemVarName )
-import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
-import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
- 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, 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 Type ( substTys, substTheta )
-import StaticFlags ( opt_IrrefutableTuples )
-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 ( zipEqual )
-import Maybes ( MaybeErr(..) )
+import Inst
+import Id
+import Var
+import CoreFVs
+import Name
+import TcSimplify
+import TcEnv
+import TcMType
+import TcType
+import VarSet
+import TcUnify
+import TcHsType
+import TysWiredIn
+import TcGadt
+import Type
+import StaticFlags
+import TyCon
+import DataCon
+import PrelNames
+import BasicTypes hiding (SuccessFlag(..))
+import SrcLoc
+import ErrUtils
+import Util
+import Maybes
import Outputable
import FastString
\end{code}
-- f t = case t of { MkT g -> ... }
-- Here, the 'g' must get type (forall a. a->a) from the
-- MkT context
- ; return (mkLocalId bndr_name pat_ty') }
+ ; return (Id.mkLocalId bndr_name pat_ty') }
tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
| Just mono_ty <- lookup_sig bndr_name
= do { mono_name <- newLocalName bndr_name
; boxyUnify mono_ty pat_ty
- ; return (mkLocalId mono_name mono_ty) }
+ ; return (Id.mkLocalId mono_name mono_ty) }
| otherwise
= do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
; mono_name <- newLocalName bndr_name
- ; return (mkLocalId mono_name pat_ty') }
+ ; return (Id.mkLocalId mono_name pat_ty') }
-------------------
-- 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
-- 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) }
%* *
%************************************************************************
+[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
= 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')
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
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) }
where
- tc_field :: Checker (Located Name, LPat Name) (Located TcId, LPat TcId)
- tc_field (field_lbl, pat) pstate thing_inside
+ -- doc comments are typechecked to Nothing here
+ tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
+ tc_field (HsRecField field_lbl pat _) pstate thing_inside
= do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
- ; return ((sel_id, pat'), tvs, res) }
+ ; return (mkRecField sel_id pat', tvs, res) }
find_field_ty :: FieldLabel -> TcM (Id, TcType)
find_field_ty field_lbl
-- 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}
+
%************************************************************************
%* *
-- 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}
projects / ghc-hetmet.git / blobdiff