%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 19921998
%
TcPat: Typechecking patterns
\begin{code}
module TcPat ( tcLetPat, tcPat, tcPats, tcOverloadedLit,
addDataConStupidTheta, badFieldCon, polyPatSig ) where
#include "HsVersions.h"
import TcExpr( tcSyntaxOp, tcInferRho)
import HsSyn
import TcHsSyn
import TcRnMonad
import Inst
import Id
import Var
import CoreFVs
import Name
import TcSimplify
import TcEnv
import TcMType
import TcType
import VarEnv
import VarSet
import TcUnify
import TcHsType
import TysWiredIn
import Coercion
import StaticFlags
import TyCon
import DataCon
import PrelNames
import BasicTypes hiding (SuccessFlag(..))
import DynFlags ( DynFlag( Opt_GADTs ) )
import SrcLoc
import ErrUtils
import Util
import Outputable
import FastString
import Control.Monad
\end{code}
%************************************************************************
%* *
External interface
%* *
%************************************************************************
\begin{code}
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_eqs = False }
; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state
(\ _ -> thing_inside)
; checkTc (null ex_tvs) (existentialExplode pat)
; return (pat', res) }
tcPats :: HsMatchContext Name
-> [LPat Name]
-> [BoxySigmaType]
-> BoxyRhoType
-> (BoxyRhoType -> TcM a)
-> TcM ([LPat TcId], a)
tcPats ctxt pats tys res_ty thing_inside
= tc_lam_pats (APat ctxt) (zipEqual "tcLamPats" pats tys)
res_ty thing_inside
tcPat :: HsMatchContext Name
-> LPat Name -> BoxySigmaType
-> BoxyRhoType
-> (BoxyRhoType -> TcM a)
-> TcM (LPat TcId, a)
tcPat ctxt = tc_lam_pat (APat ctxt)
tc_lam_pat :: PatCtxt -> LPat Name -> BoxySigmaType -> BoxyRhoType
-> (BoxyRhoType -> TcM a) -> TcM (LPat TcId, a)
tc_lam_pat ctxt pat pat_ty res_ty thing_inside
= do { ([pat'],thing) <- tc_lam_pats ctxt [(pat, pat_ty)] res_ty thing_inside
; return (pat', thing) }
tc_lam_pats :: PatCtxt
-> [(LPat Name,BoxySigmaType)]
-> BoxyRhoType
-> (BoxyRhoType -> TcM a)
-> TcM ([LPat TcId], a)
tc_lam_pats ctxt pat_ty_prs res_ty thing_inside
= do { let init_state = PS { pat_ctxt = ctxt, pat_eqs = False }
; (pats', ex_tvs, res) <- do { traceTc (text "tc_lam_pats" <+> (ppr pat_ty_prs $$ ppr res_ty))
; tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
if (pat_eqs pstate' && (not $ isRigidTy res_ty))
then nonRigidResult ctxt res_ty
else thing_inside res_ty }
; let tys = map snd pat_ty_prs
; tcCheckExistentialPat pats' ex_tvs tys res_ty
; return (pats', res) }
tcCheckExistentialPat :: [LPat TcId]
-> [TcTyVar]
-> [BoxySigmaType]
-> BoxyRhoType
-> TcM ()
tcCheckExistentialPat _ [] _ _
= return ()
tcCheckExistentialPat 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_eqs :: Bool
}
data PatCtxt
= APat (HsMatchContext Name)
| LetPat (Name -> Maybe TcRhoType)
notProcPat :: PatCtxt -> Bool
notProcPat (APat ProcExpr) = False
notProcPat _ = True
patSigCtxt :: PatState -> UserTypeCtxt
patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
patSigCtxt _ = LamPatSigCtxt
\end{code}
%************************************************************************
%* *
Binders
%* *
%************************************************************************
\begin{code}
tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
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 (Id.mkLocalId mono_name mono_ty) }
| otherwise
= do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
; mono_name <- newLocalName bndr_name
; return (Id.mkLocalId mono_name pat_ty') }
tcPatBndr (PS { pat_ctxt = _lam_or_proc }) bndr_name pat_ty
= do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
; return (Id.mkLocalId bndr_name pat_ty') }
bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
bindInstsOfPatId id thing_inside
| not (isOverloadedTy (idType id))
= do { res <- thing_inside; return (res, emptyLHsBinds) }
| otherwise
= do { (res, lie) <- getLIE thing_inside
; binds <- bindInstsOfLocalFuns lie [id]
; return (res, binds) }
unBoxPatBndrType :: BoxyType -> Name -> TcM TcType
unBoxPatBndrType ty name = unBoxArgType ty (ptext (sLit "The variable") <+> quotes (ppr name))
unBoxWildCardType :: BoxyType -> TcM TcType
unBoxWildCardType ty = unBoxArgType ty (ptext (sLit "A wild-card pattern"))
unBoxViewPatType :: BoxyType -> Pat Name -> TcM TcType
unBoxViewPatType ty pat = unBoxArgType ty (ptext (sLit "The view pattern") <+> ppr pat)
unBoxArgType :: BoxyType -> SDoc -> TcM TcType
unBoxArgType ty pp_this
= do { ty' <- unBox ty
; if isUnboxedTupleType ty' then
failWithTc msg
else if isSubArgTypeKind (typeKind ty') then
return ty'
else do
{ ty2 <- newFlexiTyVarTy argTypeKind
; _ <- unifyType ty' ty2
; return ty' }}
where
msg = pp_this <+> ptext (sLit "cannot be bound to an unboxed tuple")
\end{code}
%************************************************************************
%* *
The main worker functions
%* *
%************************************************************************
Note [Nesting]
~~~~~~~~~~~~~~
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.
This does not work so well for the ErrCtxt carried by the monad: we don't
want the errorcontext for the pattern to scope over the RHS.
Hence the getErrCtxt/setErrCtxt stuff in tc_lpats.
\begin{code}
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 []
= do { res <- thing_inside pstate
; return ([], [], res) }
loop pstate (arg:args)
= do { (p', p_tvs, (ps', ps_tvs, res))
<- tc_pat arg pstate $ \ pstate' ->
setErrCtxt err_ctxt $
loop pstate' args
; return (p':ps', p_tvs ++ ps_tvs, res) }
; loop pstate args }
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 { (pat', tvs, res) <- tc_pat pstate pat pat_ty thing_inside
; return (L span pat', tvs, res) }
tc_pat :: PatState
-> Pat Name
-> BoxySigmaType
-> (PatState -> TcM a)
-> TcM (Pat TcId,
[TcTyVar],
a)
tc_pat pstate (VarPat name) pat_ty thing_inside
= do { id <- tcPatBndr pstate name pat_ty
; (res, binds) <- bindInstsOfPatId id $
tcExtendIdEnv1 name id $
(traceTc (text "binding" <+> ppr name <+> ppr (idType id))
>> thing_inside pstate)
; let pat' | isEmptyLHsBinds binds = VarPat id
| otherwise = VarPatOut id binds
; return (pat', [], res) }
tc_pat pstate (ParPat 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 pat pat_ty pstate thing_inside
; return (BangPat pat', tvs, res) }
tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
= do { (pat', pat_tvs, (res,lie))
<- tc_lpat pat pat_ty pstate $ \ _ ->
getLIE (thing_inside pstate)
; extendLIEs lie
; unless (null pat_tvs) $ lazyPatErr lpat pat_tvs
; when (any (isUnLiftedType . idType) $ collectPatBinders pat') $
lazyUnliftedPatErr lpat
; pat_tv <- newBoxyTyVar liftedTypeKind
; _ <- boxyUnify pat_ty (mkTyVarTy pat_tv)
; return (LazyPat pat', [], res) }
tc_pat _ p@(QuasiQuotePat _) _ _
= pprPanic "Should never see QuasiQuotePat in type checker" (ppr p)
tc_pat pstate (WildPat _) pat_ty thing_inside
= do { pat_ty' <- unBoxWildCardType pat_ty
; res <- thing_inside pstate
; return (WildPat pat_ty', [], res) }
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 pat (idType bndr_id) pstate thing_inside
; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
tc_pat pstate (orig@(ViewPat expr pat _)) overall_pat_ty thing_inside
= do {
(expr',expr'_inferred) <- tcInferRho expr
; let expr'_expected = \ pat_ty -> (mkFunTy overall_pat_ty pat_ty)
; (expr_coerc, pat_ty) <- tcInfer $ \ pat_ty ->
tcSubExp ViewPatOrigin (expr'_expected pat_ty) expr'_inferred
; (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
; annotation_ty <- unBoxViewPatType overall_pat_ty orig
; return (ViewPat (mkLHsWrap expr_coerc expr') pat' annotation_ty, tvs, res) }
tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
= do { (inner_ty, tv_binds, coi) <- tcPatSig (patSigCtxt pstate) sig_ty
pat_ty
; unless (isIdentityCoI coi) $
failWithTc (badSigPat pat_ty)
; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
tc_lpat pat inner_ty pstate thing_inside
; return (SigPatOut pat' inner_ty, tvs, res) }
tc_pat _ pat@(TypePat _) _ _
= failWithTc (badTypePat pat)
tc_pat pstate (ListPat pats _) pat_ty thing_inside
= do { (elt_ty, coi) <- boxySplitListTy pat_ty
; let scoi = mkSymCoI coi
; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
pats pstate thing_inside
; return (mkCoPatCoI scoi (ListPat pats' elt_ty) pat_ty, pats_tvs, res)
}
tc_pat pstate (PArrPat pats _) pat_ty thing_inside
= do { (elt_ty, coi) <- boxySplitPArrTy pat_ty
; let scoi = mkSymCoI coi
; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
pats pstate thing_inside
; when (null pats) (zapToMonotype pat_ty >> return ())
; return (mkCoPatCoI scoi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res)
}
tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
= do { let tc = tupleTyCon boxity (length pats)
; (arg_tys, coi) <- boxySplitTyConApp tc pat_ty
; let scoi = mkSymCoI coi
; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
pstate thing_inside
; let pat_ty' = mkTyConApp tc arg_tys
unmangled_result = TuplePat pats' boxity pat_ty'
possibly_mangled_result
| opt_IrrefutableTuples &&
isBoxed boxity = LazyPat (noLoc unmangled_result)
| otherwise = unmangled_result
; ASSERT( length arg_tys == length pats )
return (mkCoPatCoI scoi possibly_mangled_result pat_ty, pats_tvs, res)
}
tc_pat pstate (ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
= do { data_con <- tcLookupDataCon con_name
; let tycon = dataConTyCon data_con
; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
= do { let lit_ty = hsLitType simple_lit
; coi <- boxyUnify lit_ty pat_ty
; res <- thing_inside pstate
; return (mkCoPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty,
[], res) }
tc_pat pstate (NPat over_lit mb_neg eq) pat_ty thing_inside
= do { let orig = LiteralOrigin over_lit
; lit' <- tcOverloadedLit orig over_lit pat_ty
; eq' <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
; mb_neg' <- case mb_neg of
Nothing -> return Nothing
Just neg ->
do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
; return (Just neg') }
; res <- thing_inside pstate
; return (NPat lit' mb_neg' eq', [], res) }
tc_pat pstate (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
= do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
; let pat_ty' = idType bndr_id
orig = LiteralOrigin lit
; lit' <- tcOverloadedLit orig lit pat_ty'
; ge' <- tcSyntaxOp orig ge (mkFunTys [pat_ty', pat_ty'] boolTy)
; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
; icls <- tcLookupClass integralClassName
; instStupidTheta orig [mkClassPred icls [pat_ty']]
; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
; return (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
tc_pat _ _other_pat _ _ = panic "tc_pat"
\end{code}
%************************************************************************
%* *
Most of the work for constructors is here
(the rest is in the ConPatIn case of tc_pat)
%* *
%************************************************************************
[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 previous 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.
RIP GADT refinement: refinements have been replaced by the use of explicit
equality constraints that are used in conjunction with implication constraints
to express the local scope of GADT refinements.
\begin{code}
tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
-> BoxySigmaType
-> HsConPatDetails Name -> (PatState -> TcM a)
-> TcM (Pat TcId, [TcTyVar], a)
tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
= 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
full_theta = eq_theta ++ dict_theta
; (ctxt_res_tys, coi, unwrap_ty) <- boxySplitTyConAppWithFamily tycon
pat_ty
; let sym_coi = mkSymCoI coi
pat_ty' = mkTyConApp tycon ctxt_res_tys
wrap_res_pat res_pat = mkCoPatCoI sym_coi uwScrut pat_ty
where
uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys
unwrap_ty res_pat
; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
; 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
; if null ex_tvs && null eq_spec && null full_theta
then do {
(arg_pats', inner_tvs, res) <- tcConArgs data_con arg_tys'
arg_pats pstate thing_inside
; let res_pat = ConPatOut { pat_con = L con_span data_con,
pat_tvs = [], pat_dicts = [],
pat_binds = emptyLHsBinds,
pat_args = arg_pats',
pat_ty = pat_ty' }
; return (wrap_res_pat res_pat, inner_tvs, res) }
else do
{ checkTc (notProcPat (pat_ctxt pstate))
(existentialProcPat data_con)
; let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
theta' = substTheta tenv (eq_preds ++ full_theta)
no_equalities = not (any isEqPred theta')
pstate' | no_equalities = pstate
| otherwise = pstate { pat_eqs = True }
; gadts_on <- doptM Opt_GADTs
; checkTc (no_equalities || gadts_on)
(ptext (sLit "A pattern match on a GADT requires -XGADTs"))
; unless no_equalities $ checkTc (isRigidTy pat_ty) $
nonRigidMatch (pat_ctxt pstate) data_con
; ((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 <- tcSimplifyCheckPat loc ex_tvs' dicts lie_req
; let res_pat = ConPatOut { pat_con = L con_span data_con,
pat_tvs = ex_tvs',
pat_dicts = map instToVar dicts,
pat_binds = dict_binds,
pat_args = arg_pats', pat_ty = pat_ty' }
; return (wrap_res_pat res_pat, ex_tvs' ++ inner_tvs, res)
} }
where
boxySplitTyConAppWithFamily tycon pat_ty =
traceTc traceMsg >>
case tyConFamInst_maybe tycon of
Nothing ->
do { (scrutinee_arg_tys, coi1) <- boxySplitTyConApp tycon pat_ty
; return (scrutinee_arg_tys, coi1, pat_ty)
}
Just (fam_tycon, instTys) ->
do { (scrutinee_arg_tys, coi1) <- boxySplitTyConApp fam_tycon pat_ty
; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
; let instTys' = substTys subst instTys
; cois <- boxyUnifyList instTys' scrutinee_arg_tys
; let coi = if isIdentityCoI coi1
then
mkTyConAppCoI fam_tycon instTys' cois
else
coi1
; return (freshTvs, coi, mkTyConApp fam_tycon instTys')
}
where
traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
ppr tycon <+> ppr pat_ty
, text " family instance:" <+>
ppr (tyConFamInst_maybe tycon)
]
unwrapFamInstScrutinee :: TyCon -> [Type] -> Type -> Pat Id -> Pat Id
unwrapFamInstScrutinee tycon args unwrap_ty pat
| Just co_con <- tyConFamilyCoercion_maybe tycon
= CoPat (WpCast $ mkTyConApp co_con args)
(pat {pat_ty = mkTyConApp tycon args})
unwrap_ty
| otherwise
= pat
tcConArgs :: DataCon -> [TcSigmaType]
-> Checker (HsConPatDetails Name) (HsConPatDetails Id)
tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
= do { checkTc (con_arity == no_of_args)
(arityErr "Constructor" data_con con_arity no_of_args)
; 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 data_con arg_tys (InfixCon p1 p2) pstate thing_inside
= do { checkTc (con_arity == 2)
(arityErr "Constructor" data_con con_arity 2)
; let [arg_ty1,arg_ty2] = arg_tys
; ([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 data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
= do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
; return (RecCon (HsRecFields rpats' dd), tvs, res) }
where
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 (HsRecField sel_id pat' pun, tvs, res) }
find_field_ty :: FieldLabel -> TcM (Id, TcType)
find_field_ty field_lbl
= case [ty | (f,ty) <- field_tys, f == field_lbl] of
[] -> do { addErrTc (badFieldCon data_con field_lbl)
; bogus_ty <- newFlexiTyVarTy liftedTypeKind
; return (error "Bogus selector Id", bogus_ty) }
(pat_ty : extras) ->
ASSERT( null extras )
do { sel_id <- tcLookupField field_lbl
; return (sel_id, pat_ty) }
field_tys :: [(FieldLabel, TcType)]
field_tys = zip (dataConFieldLabels data_con) arg_tys
tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
tcConArg (arg_pat, arg_ty) pstate thing_inside
= tc_lpat arg_pat arg_ty pstate thing_inside
\end{code}
\begin{code}
addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
addDataConStupidTheta data_con inst_tys
| null stupid_theta = return ()
| otherwise = instStupidTheta origin inst_theta
where
origin = OccurrenceOf (dataConName data_con)
stupid_theta = dataConStupidTheta data_con
tenv = mkTopTvSubst (dataConUnivTyVars data_con `zip` inst_tys)
inst_theta = substTheta tenv stupid_theta
\end{code}
Note [Arrows and patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~
(Oct 07) Arrow noation has the odd property that it involves "holes in the scope".
For example:
expr :: Arrow a => a () Int
expr = proc (y,z) -> do
x <- term -< y
expr' -< x
Here the 'proc (y,z)' binding scopes over the arrow tails but not the
arrow body (e.g 'term'). As things stand (bogusly) all the
constraints from the proc body are gathered together, so constraints
from 'term' will be seen by the tcPat for (y,z). But we must *not*
bind constraints from 'term' here, becuase the desugarer will not make
these bindings scope over 'term'.
The Right Thing is not to confuse these constraints together. But for
now the Easy Thing is to ensure that we do not have existential or
GADT constraints in a 'proc', and to shortcut the constraint
simplification for such vanilla patterns so that it binds no
constraints. Hence the 'fast path' in tcConPat; but it's also a good
plan for ordinary vanilla patterns to bypass the constraint
simplification step.
%************************************************************************
%* *
Overloaded literals
%* *
%************************************************************************
In tcOverloadedLit we convert directly to an Int or Integer if we
know that's what we want. This may save some time, by not
temporarily generating overloaded literals, but it won't catch all
cases (the rest are caught in lookupInst).
\begin{code}
tcOverloadedLit :: InstOrigin
-> HsOverLit Name
-> BoxyRhoType
-> TcM (HsOverLit TcId)
tcOverloadedLit orig lit@(OverLit { ol_val = val, ol_rebindable = rebindable
, ol_witness = meth_name }) res_ty
| rebindable
= do { hs_lit <- mkOverLit val
; let lit_ty = hsLitType hs_lit
; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
; return (lit { ol_witness = witness, ol_type = res_ty }) }
| Just expr <- shortCutLit val res_ty
= return (lit { ol_witness = expr, ol_type = res_ty })
| otherwise
= do { loc <- getInstLoc orig
; res_tau <- zapToMonotype res_ty
; new_uniq <- newUnique
; let lit_nm = mkSystemVarName new_uniq (fsLit "lit")
lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit,
tci_ty = res_tau, tci_loc = loc}
witness = HsVar (instToId lit_inst)
; extendLIE lit_inst
; return (lit { ol_witness = witness, ol_type = res_ty }) }
\end{code}
%************************************************************************
%* *
Note [Pattern coercions]
%* *
%************************************************************************
In principle, these program would be reasonable:
f :: (forall a. a->a) -> Int
f (x :: Int->Int) = x 3
g :: (forall a. [a]) -> Bool
g [] = True
In both cases, the function type signature restricts what arguments can be passed
in a call (to polymorphic ones). The pattern type signature then instantiates this
type. For example, in the first case, (forall a. a->a) <= Int -> Int, and we
generate the translated term
f = \x' :: (forall a. a->a). let x = x' Int in x 3
From a typesystem point of view, this is perfectly fine, but it's *very* seldom useful.
And it requires a significant amount of code to implement, becuase we need to decorate
the translated pattern with coercion functions (generated from the subsumption check
by tcSub).
So for now I'm just insisting on type *equality* in patterns. No subsumption.
Old notes about desugaring, at a time when pattern coercions were handled:
A SigPat is a type coercion and must be handled one at at time. We can't
combine them unless the type of the pattern inside is identical, and we don't
bother to check for that. For example:
data T = T1 Int | T2 Bool
f :: (forall a. a -> a) -> T -> t
f (g::Int->Int) (T1 i) = T1 (g i)
f (g::Bool->Bool) (T2 b) = T2 (g b)
We desugar this as follows:
f = \ g::(forall a. a->a) t::T ->
let gi = g Int
in case t of { T1 i -> T1 (gi i)
other ->
let gb = g Bool
in case t of { T2 b -> T2 (gb b)
other -> fail }}
Note that we do not treat the first column of patterns as a
column of variables, because the coerced variables (gi, gb)
would be of different types. So we get rather grotty code.
But I don't think this is a common case, and if it was we could
doubtless improve it.
Meanwhile, the strategy is:
* treat each SigPat coercion (always nonidentity coercions)
as a separate block
* deal with the stuff inside, and then wrap a binding round
the result to bind the new variable (gi, gb, etc)
%************************************************************************
%* *
\subsection{Errors and contexts}
%* *
%************************************************************************
\begin{code}
patCtxt :: Pat Name -> Maybe Message
patCtxt (VarPat _) = Nothing
patCtxt (ParPat _) = Nothing
patCtxt (AsPat _ _) = Nothing
patCtxt pat = Just (hang (ptext (sLit "In the pattern:"))
4 (ppr pat))
existentialExplode :: LPat Name -> SDoc
existentialExplode pat
= hang (vcat [text "My brain just exploded.",
text "I can't handle pattern bindings for existential or GADT data constructors.",
text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
text "In the binding group for"])
4 (ppr pat)
sigPatCtxt :: [LPat Var] -> [Var] -> [TcType] -> TcType -> TidyEnv
-> TcM (TidyEnv, SDoc)
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)
(env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
(env3, tidy_body_ty) = tidyOpenType env2 body_ty'
; return (env3,
sep [ptext (sLit "When checking an existential match that binds"),
nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
ptext (sLit "The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
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` varTypeTyVars id) bound_tvs
ppr_id id ty = ppr id <+> dcolon <+> ppr ty
badFieldCon :: DataCon -> Name -> SDoc
badFieldCon con field
= hsep [ptext (sLit "Constructor") <+> quotes (ppr con),
ptext (sLit "does not have field"), quotes (ppr field)]
polyPatSig :: TcType -> SDoc
polyPatSig sig_ty
= hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
2 (ppr sig_ty)
badSigPat :: TcType -> SDoc
badSigPat pat_ty = ptext (sLit "Pattern signature must exactly match:") <+>
ppr pat_ty
badTypePat :: Pat Name -> SDoc
badTypePat pat = ptext (sLit "Illegal type pattern") <+> ppr pat
existentialProcPat :: DataCon -> SDoc
existentialProcPat con
= hang (ptext (sLit "Illegal constructor") <+> quotes (ppr con) <+> ptext (sLit "in a 'proc' pattern"))
2 (ptext (sLit "Proc patterns cannot use existentials or GADTs"))
lazyPatErr :: Pat name -> [TcTyVar] -> TcM ()
lazyPatErr _ tvs
= failWithTc $
hang (ptext (sLit "A lazy (~) pattern cannot match existential or GADT data constructors"))
2 (vcat (map pprSkolTvBinding tvs))
lazyUnliftedPatErr :: OutputableBndr name => Pat name -> TcM ()
lazyUnliftedPatErr pat
= failWithTc $
hang (ptext (sLit "A lazy (~) pattern cannot contain unlifted types"))
2 (ppr pat)
nonRigidMatch :: PatCtxt -> DataCon -> SDoc
nonRigidMatch ctxt con
= hang (ptext (sLit "GADT pattern match in non-rigid context for") <+> quotes (ppr con))
2 (ptext (sLit "Probable solution: add a type signature for") <+> what ctxt)
where
what (APat (FunRhs f _)) = quotes (ppr f)
what (APat CaseAlt) = ptext (sLit "the scrutinee of the case expression")
what (APat LambdaExpr ) = ptext (sLit "the lambda expression")
what (APat (StmtCtxt _)) = ptext (sLit "the right hand side of a do/comprehension binding")
what _other = ptext (sLit "something")
nonRigidResult :: PatCtxt -> Type -> TcM a
nonRigidResult ctxt res_ty
= do { env0 <- tcInitTidyEnv
; let (env1, res_ty') = tidyOpenType env0 res_ty
msg = hang (ptext (sLit "GADT pattern match with non-rigid result type")
<+> quotes (ppr res_ty'))
2 (ptext (sLit "Solution: add a type signature for")
<+> what ctxt )
; failWithTcM (env1, msg) }
where
what (APat (FunRhs f _)) = quotes (ppr f)
what (APat CaseAlt) = ptext (sLit "the entire case expression")
what (APat LambdaExpr) = ptext (sLit "the lambda exression")
what (APat (StmtCtxt _)) = ptext (sLit "the entire do/comprehension expression")
what _other = ptext (sLit "something")
\end{code}