%
+% (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,
#include "HsVersions.h"
import {-# SOURCE #-} TcExpr( tcSyntaxOp )
-import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..),
- HsOverLit(..), HsExpr(..), ExprCoFn(..),
- mkCoPat,
- LHsBinds, emptyLHsBinds, isEmptyLHsBinds,
- collectPatsBinders, nlHsLit )
-import TcHsSyn ( TcId, hsLitType )
+
+import HsSyn
+import TcHsSyn
import TcRnMonad
-import Inst ( InstOrigin(..), shortCutFracLit, shortCutIntLit,
- newDictBndrs, instToId, instStupidTheta, isHsVar
- )
-import Id ( Id, idType, mkLocalId )
-import Var ( CoVar, tyVarKind )
-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, tcInstTyVars, newBoxyTyVar )
-import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType, BoxyType,
- SkolemInfo(PatSkol),
- BoxySigmaType, BoxyRhoType, argTypeKind, typeKind,
- pprSkolTvBinding, isRigidTy, tcTyVarsOfTypes,
- zipTopTvSubst, isSubArgTypeKind, isUnboxedTupleType,
- mkTyVarTys, mkClassPred, isOverloadedTy, substEqSpec,
- mkFunTy, mkFunTys, tidyOpenType, tidyOpenTypes,
- mkTyVarTy )
-import VarSet ( elemVarSet )
-import {- Kind parts of -}
- Type ( liftedTypeKind )
-import TcUnify ( boxySplitTyConApp, boxySplitListTy, unBox,
- zapToMonotype, boxyUnify, boxyUnifyList,
- checkSigTyVarsWrt, unifyType )
-import TcHsType ( UserTypeCtxt(..), tcPatSig )
-import TysWiredIn ( boolTy, parrTyCon, tupleTyCon )
-import TcGadt ( Refinement, emptyRefinement, gadtRefine, refineType )
-import Type ( Type, mkTyConApp, substTys, substTheta )
-import StaticFlags ( opt_IrrefutableTuples )
-import TyCon ( TyCon, FieldLabel, tyConFamInst_maybe,
- tyConFamilyCoercion_maybe, tyConTyVars )
-import DataCon ( DataCon, dataConTyCon, dataConFullSig,
- dataConFieldLabels, dataConSourceArity,
- dataConStupidTheta, dataConUnivTyVars )
-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 Coercion
+import StaticFlags
+import TyCon
+import DataCon
+import DynFlags
+import PrelNames
+import BasicTypes hiding (SuccessFlag(..))
+import SrcLoc
+import ErrUtils
+import Util
+import Maybes
import Outputable
import FastString
\end{code}
-> 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_reft = emptyRefinement,
+ pat_eqs = False }
; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)
-- Don't know how to deal with pattern-bound existentials yet
-> ((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 }
+ = do { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft, pat_eqs = False }
; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
- refineEnvironment (pat_reft pstate') $
- thing_inside (pat_reft pstate', res_ty)
+ refineEnvironment (pat_reft pstate') (pat_eqs pstate') $
+ if (pat_eqs pstate' && (not $ isRigidTy res_ty))
+ then failWithTc (nonRigidResult res_ty)
+ else thing_inside (pat_reft pstate', res_ty)
; let tys = map snd pat_ty_prs
; tcCheckExistentialPat pats' ex_tvs tys res_ty
= return () -- Short cut for case when there are no existentials
tcCheckExistentialPat pats ex_tvs pat_tys body_ty
- = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys body_ty) $
+ = addErrCtxtM (sigPatCtxt pats ex_tvs pat_tys body_ty) $
checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
data PatState = PS {
pat_ctxt :: PatCtxt,
- pat_reft :: Refinement -- Binds rigid TcTyVars to their refinements
+ pat_reft :: Refinement, -- Binds rigid TcTyVars to their refinements
+ pat_eqs :: Bool -- <=> there are GADT equational constraints
+ -- for refinement
}
data PatCtxt
-- 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') }
-------------------
Note [Nesting]
~~~~~~~~~~~~~~
-tcPat takes a "thing inside" over which the patter scopes. This is partly
+tcPat takes a "thing inside" over which the pattern scopes. This is partly
so that tcPat can extend the environment for the thing_inside, but also
so that constraints arising in the thing_inside can be discharged by the
pattern.
tc_lpat (L span pat) pat_ty pstate thing_inside
= setSrcSpan span $
maybeAddErrCtxt (patCtxt pat) $
- do { let (coercion, pat_ty') = refineType (pat_reft pstate) pat_ty
+ do { let mb_reft = refineType (pat_reft pstate) pat_ty
+ pat_ty' = case mb_reft of { Just (_, ty') -> ty'; Nothing -> pat_ty }
+
-- Make sure the result type reflects the current refinement
-- We must do this here, so that it correctly ``sees'' all
-- the refinements to the left. Example:
-- 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) }
+ ; let final_pat = case mb_reft of
+ Nothing -> pat'
+ Just (co,_) -> CoPat (WpCo co) pat' pat_ty
+ ; return (L span final_pat, tvs, res) }
--------------------
tc_pat :: PatState
--
-- Nor should a lazy pattern bind any existential type variables
-- because they won't be in scope when we do the desugaring
+--
+-- Note [Hopping the LIE in lazy patterns]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- In a lazy pattern, we must *not* discharge constraints from the RHS
+-- from dictionaries bound in the pattern. E.g.
+-- f ~(C x) = 3
+-- We can't discharge the Num constraint from dictionaries bound by
+-- the pattern C!
+--
+-- So we have to make the constraints from thing_inside "hop around"
+-- the pattern. Hence the getLLE and extendLIEs later.
+
tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
- = do { (pat', pat_tvs, res) <- tc_lpat pat pat_ty pstate $ \ _ ->
- thing_inside pstate
- -- Ignore refined pstate',
- -- revert to pstate
+ = do { (pat', pat_tvs, (res,lie))
+ <- tc_lpat pat pat_ty pstate $ \ _ ->
+ getLIE (thing_inside pstate)
+ -- Ignore refined pstate', revert to pstate
+ ; extendLIEs lie
+ -- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns]
+
-- Check no existentials
; if (null pat_tvs) then return ()
else lazyPatErr lpat pat_tvs
------------------------
-- Literal patterns
tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
- = do { boxyUnify (hsLitType simple_lit) pat_ty
+ = do { let lit_ty = hsLitType simple_lit
+ ; coi <- boxyUnify lit_ty pat_ty
+ -- coi is of kind: lit_ty ~ pat_ty
; res <- thing_inside pstate
- ; returnM (LitPat simple_lit, [], res) }
+ ; span <- getSrcSpanM
+ -- pattern coercions have to
+ -- be of kind: pat_ty ~ lit_ty
+ -- hence, sym coi
+ ; returnM (wrapPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, [], res) }
------------------------
-- Overloaded patterns: n, and n+k
; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
-tc_pat _ _other_pat _ _ = panic "tc_pat" -- DictPat, ConPatOut, SigPatOut, VarPatOut
+tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut, VarPatOut
\end{code}
tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
-> BoxySigmaType -- Type of the pattern
- -> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
+ -> HsConPatDetails Name -> (PatState -> TcM a)
-> TcM (Pat TcId, [TcTyVar], a)
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
+ = do { let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _) = dataConFullSig data_con
+ skol_info = PatSkol data_con
origin = SigOrigin skol_info
-- Instantiate the constructor type variables [a->ty]
; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty
- ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
+ ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs -- Get location from monad,
+ -- not from ex_tvs
; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs)
- (ctxt_res_tys ++ mkTyVarTys ex_tvs')
+ (ctxt_res_tys ++ mkTyVarTys ex_tvs')
eq_spec' = substEqSpec tenv eq_spec
- theta' = substTheta tenv theta
+ theta' = substTheta tenv (eq_theta ++ dict_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 $
tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
; loc <- getInstLoc origin
; dicts <- newDictBndrs loc theta'
- ; dict_binds <- tcSimplifyCheck doc ex_tvs' dicts lie_req
+ ; dict_binds <- tcSimplifyCheckPat loc co_vars (pat_reft pstate')
+ ex_tvs' dicts lie_req
- ; addDataConStupidTheta origin data_con ctxt_res_tys
+ ; addDataConStupidTheta data_con ctxt_res_tys
; return
(unwrapFamInstScrutinee tycon ctxt_res_tys $
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.
- --
+ -- Split against the family tycon if the pattern constructor
+ -- belongs to a family instance tycon.
boxySplitTyConAppWithFamily tycon pat_ty =
traceTc traceMsg >>
case tyConFamInst_maybe tycon of
-- 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 (ExprCoFn $ mkTyConApp co_con args) -- co fam ty to repr ty
+ = 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
tcConArgs :: DataCon -> [TcSigmaType]
- -> Checker (HsConDetails Name (LPat Name))
- (HsConDetails Id (LPat Id))
+ -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
= do { checkTc (con_arity == no_of_args) -- Check correct arity
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
+tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
= do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
- ; return (RecCon rpats', tvs, res) }
+ ; return (RecCon (HsRecFields rpats' dd), tvs, res) }
where
- tc_field :: Checker (Located Name, LPat Name) (Located TcId, LPat TcId)
- tc_field (field_lbl, pat) pstate thing_inside
+ tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
+ tc_field (HsRecField field_lbl pat pun) 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 (HsRecField sel_id pat' pun, tvs, res) }
find_field_ty :: FieldLabel -> TcM (Id, TcType)
find_field_ty field_lbl
\end{code}
\begin{code}
-addDataConStupidTheta :: InstOrigin -> DataCon -> [TcType] -> TcM ()
+addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
-- Instantiate the "stupid theta" of the data con, and throw
-- the constraints into the constraint set
-addDataConStupidTheta origin data_con inst_tys
+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
-> TcM PatState
refineAlt con pstate ex_tvs [] pat_ty
+ | null $ dataConEqTheta con
= return pstate -- Common case: no equational constraints
refineAlt con pstate ex_tvs co_vars pat_ty
- | not (isRigidTy pat_ty)
- = failWithTc (nonRigidMatch con)
+ = do { opt_gadt <- doptM Opt_GADTs -- No type-refinement unless GADTs are on
+ ; if (not opt_gadt) then return pstate
+ else do
+
+ { checkTc (isRigidTy pat_ty) (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:
-- 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 {
+ -- 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 }) }
+ ; return (pstate { pat_reft = reft, pat_eqs = (pat_eqs pstate || not (null $ dataConEqTheta con)) }) }
-- DO NOT refine the envt right away, because we
-- might be inside a lazy pattern. Instead, refine pstate
where
vcat [ ppr con <+> ppr ex_tvs,
ppr [(v, tyVarKind v) | v <- co_vars],
ppr reft]
- }
+ } } }
\end{code}
= do { expr <- newLitInst orig lit res_ty
; return (HsFractional r expr) }
+tcOverloadedLit orig lit@(HsIsString s fr) res_ty
+ | not (fr `isHsVar` fromStringName) -- c.f. HsIntegral case
+ = do { str_ty <- tcMetaTy stringTyConName
+ ; fr' <- tcSyntaxOp orig fr (mkFunTy str_ty res_ty)
+ ; return (HsIsString s (HsApp (noLoc fr') (nlHsLit (HsString s)))) }
+
+ | Just expr <- shortCutStringLit s res_ty
+ = return (HsIsString s expr)
+
+ | otherwise
+ = do { expr <- newLitInst orig lit res_ty
+ ; return (HsIsString s expr) }
+
newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
newLitInst orig lit res_ty -- Make a LitInst
= do { loc <- getInstLoc orig
; res_tau <- zapToMonotype res_ty
; new_uniq <- newUnique
; let lit_nm = mkSystemVarName new_uniq FSLIT("lit")
- lit_inst = LitInst lit_nm lit res_tau loc
+ lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit,
+ tci_ty = res_tau, tci_loc = loc}
; extendLIE lit_inst
; return (HsVar (instToId lit_inst)) }
\end{code}
existentialExplode pat
= hang (vcat [text "My brain just exploded.",
text "I can't handle pattern bindings for existentially-quantified constructors.",
+ text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
text "In the binding group for"])
4 (ppr pat)
-sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env
+sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env
= do { pat_tys' <- mapM zonkTcType pat_tys
; body_ty' <- zonkTcType body_ty
; let (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
ptext SLIT("The body has type:") <+> ppr tidy_body_ty
]) }
where
+ bound_ids = collectPatsBinders pats
show_ids = filter is_interesting bound_ids
- is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
+ is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
ppr_id id ty = ppr id <+> dcolon <+> ppr ty
-- Don't zonk the types so we get the separate, un-unified versions
lazyPatErr pat tvs
= failWithTc $
- hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
+ hang (ptext SLIT("A lazy (~) pattern cannot 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"))
+nonRigidResult res_ty
+ = hang (ptext SLIT("GADT pattern match with non-rigid result type") <+> quotes (ppr res_ty))
+ 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}
+
+\begin{code}
+wrapPatCoI :: CoercionI -> Pat a -> TcType -> Pat a
+wrapPatCoI IdCo pat ty = pat
+wrapPatCoI (ACo co) pat ty = CoPat (WpCo co) pat ty
+\end{code}
projects / ghc-hetmet.git / blobdiff