\section[TcPat]{Typechecking patterns}
\begin{code}
-module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig ) where
+module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig, refineTyVars ) where
#include "HsVersions.h"
-import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..),
- HsExpr(..), LHsBinds, emptyLHsBinds, isEmptyLHsBinds )
-import HsUtils
+import {-# SOURCE #-} TcExpr( tcSyntaxOp )
+import HsSyn ( Pat(..), LPat, HsConDetails(..),
+ LHsBinds, emptyLHsBinds, isEmptyLHsBinds )
import TcHsSyn ( TcId, hsLitType )
import TcRnMonad
-import Inst ( InstOrigin(..),
- newMethodFromName, newOverloadedLit, newDicts,
- instToId, tcInstStupidTheta, tcSyntaxName
+import Inst ( InstOrigin(..), tcOverloadedLit,
+ newDicts, instToId, tcInstStupidTheta
)
import Id ( Id, idType, mkLocalId )
+import Var ( tyVarName )
import Name ( Name )
import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
-import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv,
+import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
tcLookupClass, tcLookupDataCon, tcLookupId )
-import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars, isRigidType )
+import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars, readMetaTyVar )
import TcType ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst,
- SkolemInfo(PatSkol), isSkolemTyVar, pprSkolemTyVar,
- mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy )
+ SkolemInfo(PatSkol), isMetaTyVar, pprTcTyVar,
+ TvSubst, mkOpenTvSubst, substTyVar, substTy, MetaDetails(..),
+ mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy,
+ mkFunTy, mkFunTys )
+import VarEnv ( mkVarEnv ) -- ugly
import Kind ( argTypeKind, liftedTypeKind )
import TcUnify ( tcSubPat, Expected(..), zapExpectedType,
zapExpectedTo, zapToListTy, zapToTyConApp )
import TcHsType ( UserTypeCtxt(..), TcSigInfo( sig_tau ), TcSigFun, tcHsPatSigType )
-import TysWiredIn ( stringTy, parrTyCon, tupleTyCon )
-import Unify ( MaybeErr(..), tcRefineTys, tcMatchTys )
+import TysWiredIn ( boolTy, parrTyCon, tupleTyCon )
+import Unify ( MaybeErr(..), gadtRefineTys, BindFlag(..) )
import Type ( substTys, substTheta )
-import CmdLineOpts ( opt_IrrefutableTuples )
+import StaticFlags ( opt_IrrefutableTuples )
import TyCon ( TyCon )
import DataCon ( DataCon, dataConTyCon, isVanillaDataCon, dataConInstOrigArgTys,
dataConFieldLabels, dataConSourceArity, dataConSig )
-import PrelNames ( eqStringName, eqName, geName, negateName, minusName,
- integralClassName )
+import PrelNames ( integralClassName )
import BasicTypes ( isBoxed )
-import SrcLoc ( Located(..), noLoc, unLoc )
+import SrcLoc ( Located(..), SrcSpan, noLoc )
+import Maybes ( catMaybes )
import ErrUtils ( Message )
import Outputable
import FastString
[TcTyVar], -- Existential binders
a) -- Result of thing inside
-tcPat ctxt pat exp_ty thing_inside
- = do { err_ctxt <- getErrCtxt
- ; maybeAddErrCtxt (patCtxt (unLoc pat)) $
- tc_lpat ctxt pat exp_ty $
- setErrCtxt err_ctxt thing_inside }
- -- Restore error context before doing thing_inside
- -- See note [Nesting] above
+tcPat ctxt (L span pat) exp_ty thing_inside
+ = do { -- Restore error context before doing thing_inside
+ -- See note [Nesting] above
+ err_ctxt <- getErrCtxt
+ ; let real_thing_inside = setErrCtxt err_ctxt thing_inside
+
+ -- It's OK to keep setting the SrcSpan;
+ -- it just overwrites the previous value
+ ; (pat', tvs, res) <- setSrcSpan span $
+ maybeAddErrCtxt (patCtxt pat) $
+ tc_pat ctxt pat exp_ty $
+ real_thing_inside
+
+ ; return (L span pat', tvs, res)
+ }
--------------------
tcPats :: PatCtxt
%************************************************************************
\begin{code}
-data PatCtxt = LamPat Bool | LetPat TcSigFun
- -- True <=> we are checking the case expression,
- -- so can do full-blown refinement
- -- False <=> inferring, do no refinement
+data PatCtxt = LamPat -- Used for lambda, case, do-notation etc
+ | LetPat TcSigFun -- Used for let(rec) bindings
-------------------
tcPatBndr :: PatCtxt -> Name -> Expected TcSigmaType -> TcM TcId
-tcPatBndr (LamPat _) bndr_name pat_ty
+tcPatBndr LamPat bndr_name pat_ty
= do { pat_ty' <- zapExpectedType pat_ty argTypeKind
-- If pat_ty is Expected, this returns the appropriate
-- SigmaType. In Infer mode, we create a fresh type variable.
+ -- Note argTypeKind: the variable can have an unboxed type,
+ -- but not an unboxed tuple.
-- Note the SigmaType: we can get
-- data T = MkT (forall a. a->a)
-- f t = case t of { MkT g -> ... }
%************************************************************************
\begin{code}
-tc_lpat :: PatCtxt
- -> LPat Name -> Expected TcSigmaType
+tc_pat :: PatCtxt
+ -> Pat Name -> Expected TcSigmaType
-> TcM a -- Thing inside
- -> TcM (LPat TcId, -- Translated pattern
+ -> TcM (Pat TcId, -- Translated pattern
[TcTyVar], -- Existential binders
a) -- Result of thing inside
-tc_lpat ctxt (L span pat) pat_ty thing_inside
- = setSrcSpan span $
- -- It's OK to keep setting the SrcSpan;
- -- it just overwrites the previous value
- do { (pat', tvs, res) <- tc_pat ctxt pat pat_ty thing_inside
- ; return (L span pat', tvs, res) }
-
----------------------
tc_pat ctxt (VarPat name) pat_ty thing_inside
= do { id <- tcPatBndr ctxt name pat_ty
; (res, binds) <- bindInstsOfPatId id $
; return (pat', [], res) }
tc_pat ctxt (ParPat pat) pat_ty thing_inside
- = do { (pat', tvs, res) <- tc_lpat ctxt pat pat_ty thing_inside
+ = do { (pat', tvs, res) <- tcPat ctxt pat pat_ty thing_inside
; return (ParPat pat', tvs, res) }
-- There's a wrinkle with irrefuatable patterns, namely that we
-- because they won't be in scope when we do the desugaring
tc_pat ctxt lpat@(LazyPat pat) pat_ty thing_inside
= do { reft <- getTypeRefinement
- ; (pat', pat_tvs, res) <- tc_lpat ctxt pat pat_ty $
+ ; (pat', pat_tvs, res) <- tcPat ctxt pat pat_ty $
setTypeRefinement reft thing_inside
; if (null pat_tvs) then return ()
else lazyPatErr lpat pat_tvs
tc_pat ctxt (AsPat (L nm_loc name) pat) pat_ty thing_inside
= do { bndr_id <- setSrcSpan nm_loc (tcPatBndr ctxt name pat_ty)
; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
- tc_lpat ctxt pat (Check (idType bndr_id)) thing_inside
+ tcPat ctxt pat (Check (idType bndr_id)) 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
= do { -- See Note [Pattern coercions] below
(sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
; tcSubPat sig_ty pat_ty
- ; (pat', tvs, res) <- tcExtendTyVarEnv sig_tvs $
- tc_lpat ctxt pat (Check sig_ty) thing_inside
- ; return (SigPatOut pat' sig_ty, tvs, res) }
+ ; subst <- refineTyVars sig_tvs -- See note [Type matching]
+ ; let tv_binds = [(tyVarName tv, substTyVar subst tv) | tv <- sig_tvs]
+ sig_ty' = substTy subst sig_ty
+ ; (pat', tvs, res)
+ <- tcExtendTyVarEnv2 tv_binds $
+ tcPat ctxt pat (Check sig_ty') thing_inside
+
+ ; return (SigPatOut pat' sig_ty', tvs, res) }
tc_pat ctxt pat@(TypePat ty) pat_ty thing_inside
= failWithTc (badTypePat pat)
= do { data_con <- tcLookupDataCon con_name
; let tycon = dataConTyCon data_con
; ty_args <- zapToTyConApp tycon pat_ty
- ; (pat', tvs, res) <- tcConPat ctxt data_con tycon ty_args arg_pats thing_inside
+ ; (pat', tvs, res) <- tcConPat ctxt con_span data_con tycon ty_args arg_pats thing_inside
; return (pat', tvs, res) }
-
------------------------
-- Literal patterns
-tc_pat ctxt pat@(LitPat lit@(HsString _)) pat_ty thing_inside
- = do { -- Strings are mapped to NPatOuts, which have a guard expression
- zapExpectedTo pat_ty stringTy
- ; eq_id <- tcLookupId eqStringName
- ; res <- thing_inside
- ; returnM (NPatOut lit stringTy (nlHsVar eq_id `HsApp` nlHsLit lit), [], res) }
-
tc_pat ctxt (LitPat simple_lit) pat_ty thing_inside
= do { -- All other simple lits
zapExpectedTo pat_ty (hsLitType simple_lit)
------------------------
-- Overloaded patterns: n, and n+k
-tc_pat ctxt pat@(NPatIn over_lit mb_neg) pat_ty thing_inside
+tc_pat ctxt pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside
= do { pat_ty' <- zapExpectedType pat_ty liftedTypeKind
- ; let origin = LiteralOrigin over_lit
- ; pos_lit_expr <- newOverloadedLit origin over_lit pat_ty'
- ; eq <- newMethodFromName origin pat_ty' eqName
- ; lit_expr <- case mb_neg of
- Nothing -> returnM pos_lit_expr -- Positive literal
+ ; 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 -- Positive literal
Just neg -> -- Negative literal
-- The 'negate' is re-mappable syntax
- do { (_, neg_expr) <- tcSyntaxName origin pat_ty'
- (negateName, HsVar neg)
- ; returnM (mkHsApp (noLoc neg_expr) pos_lit_expr) }
-
- ; let -- The literal in an NPatIn is always positive...
- -- But in NPatOut, the literal is used to find identical patterns
- -- so we must negate the literal when necessary!
- lit' = case (over_lit, mb_neg) of
- (HsIntegral i _, Nothing) -> HsInteger i pat_ty'
- (HsIntegral i _, Just _) -> HsInteger (-i) pat_ty'
- (HsFractional f _, Nothing) -> HsRat f pat_ty'
- (HsFractional f _, Just _) -> HsRat (-f) pat_ty'
-
+ do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty' pat_ty')
+ ; return (Just neg') }
; res <- thing_inside
- ; returnM (NPatOut lit' pat_ty' (HsApp (nlHsVar eq) lit_expr), [], res) }
+ ; returnM (NPat lit' mb_neg' eq' pat_ty', [], res) }
-tc_pat ctxt pat@(NPlusKPatIn (L nm_loc name) lit@(HsIntegral i _) minus_name) pat_ty thing_inside
+tc_pat ctxt pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
= do { bndr_id <- setSrcSpan nm_loc (tcPatBndr ctxt name pat_ty)
; let pat_ty' = idType bndr_id
- origin = LiteralOrigin lit
- ; over_lit_expr <- newOverloadedLit origin lit pat_ty'
- ; ge <- newMethodFromName origin pat_ty' geName
+ orig = LiteralOrigin lit
+ ; lit' <- tcOverloadedLit orig lit pat_ty'
- -- The '-' part is re-mappable syntax
- ; (_, minus_expr) <- tcSyntaxName origin pat_ty' (minusName, HsVar minus_name)
+ -- The '>=' and '-' parts are re-mappable syntax
+ ; ge' <- tcSyntaxOp orig ge (mkFunTys [pat_ty', pat_ty'] boolTy)
+ ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
-- 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 origin [mkClassPred icls [pat_ty']]
+ ; dicts <- newDicts orig [mkClassPred icls [pat_ty']]
; extendLIEs dicts
; res <- tcExtendIdEnv1 name bndr_id thing_inside
- ; returnM (NPlusKPatOut (L nm_loc bndr_id) i
- (SectionR (nlHsVar ge) over_lit_expr)
- (SectionR (noLoc minus_expr) over_lit_expr),
- [], res) }
+ ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
\end{code}
%************************************************************************
\begin{code}
-tcConPat :: PatCtxt -> DataCon -> TyCon -> [TcTauType]
+tcConPat :: PatCtxt -> SrcSpan -> DataCon -> TyCon -> [TcTauType]
-> HsConDetails Name (LPat Name) -> TcM a
-> TcM (Pat TcId, [TcTyVar], a)
-tcConPat ctxt data_con tycon ty_args arg_pats thing_inside
+tcConPat ctxt span data_con tycon ty_args arg_pats thing_inside
| isVanillaDataCon data_con
= do { let arg_tys = dataConInstOrigArgTys data_con ty_args
; tcInstStupidTheta data_con ty_args
; traceTc (text "tcConPat" <+> vcat [ppr data_con, ppr ty_args, ppr arg_tys])
; (arg_pats', tvs, res) <- tcConArgs ctxt data_con arg_pats arg_tys thing_inside
- ; return (ConPatOut data_con [] [] emptyLHsBinds
+ ; return (ConPatOut (L span data_con) [] [] emptyLHsBinds
arg_pats' (mkTyConApp tycon ty_args),
tvs, res) }
| otherwise -- GADT case
= do { let (tvs, theta, arg_tys, _, res_tys) = dataConSig data_con
+ ; traceTc (text "tcConPat: GADT" <+> ppr data_con)
; span <- getSrcSpanM
; let rigid_info = PatSkol data_con span
; tvs' <- tcSkolTyVars rigid_info tvs
arg_tys' = substTys tenv arg_tys
res_tys' = substTys tenv res_tys
; dicts <- newDicts (SigOrigin rigid_info) theta'
- ; tcInstStupidTheta data_con tv_tys'
-- Do type refinement!
; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', ppr arg_tys', ppr res_tys',
text "ty-args:" <+> ppr ty_args ])
; refineAlt ctxt data_con tvs' ty_args res_tys' $ do
- { ((arg_pats', inner_tvs, res), lie_req)
- <- getLIE (tcConArgs ctxt data_con arg_pats arg_tys' thing_inside)
+ { ((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 ctxt data_con arg_pats arg_tys' thing_inside }
; dict_binds <- tcSimplifyCheck doc tvs' dicts lie_req
- ; return (ConPatOut data_con
+ ; return (ConPatOut (L span data_con)
tvs' (map instToId dicts) dict_binds
arg_pats' (mkTyConApp tycon ty_args),
tvs' ++ inner_tvs, res) } }
-> TcM a -> TcM a
refineAlt ctxt con ex_tvs ctxt_tys pat_tys thing_inside
= do { old_subst <- getTypeRefinement
- ; let refiner | can_i_refine ctxt = tcRefineTys
- | otherwise = tcMatchTys
- ; case refiner ex_tvs old_subst pat_tys ctxt_tys of
+ ; case gadtRefineTys bind_fn old_subst pat_tys ctxt_tys of
Failed msg -> failWithTc (inaccessibleAlt msg)
Succeeded new_subst -> do {
traceTc (text "refineTypes:match" <+> ppr con <+> ppr new_subst)
; setTypeRefinement new_subst thing_inside } }
where
- can_i_refine (LamPat can_refine) = can_refine
- can_i_refine other_ctxt = False
+ bind_fn tv | isMetaTyVar tv = WildCard -- Wobbly types behave as wild cards
+ | otherwise = BindMe
+\end{code}
+
+Note [Type matching]
+~~~~~~~~~~~~~~~~~~~~
+This little function @refineTyVars@ is a little tricky. Suppose we have a pattern type
+signature
+ f = \(x :: Term a) -> body
+Then 'a' should be bound to a wobbly type. But if we have
+ f :: Term b -> some-type
+ f = \(x :: Term a) -> body
+then 'a' should be bound to the rigid type 'b'. So we want to
+ * instantiate the type sig with fresh meta tyvars (e.g. \alpha)
+ * unify with the type coming from the context
+ * read out whatever information has been gleaned
+ from that unificaiton (e.g. unifying \alpha with 'b')
+ * and replace \alpha by 'b' in the type, when typechecking the
+ pattern inside the type sig (x in this case)
+It amounts to combining rigid info from the context and from the sig.
+
+Exactly the same thing happens for 'smart function application'.
+
+\begin{code}
+refineTyVars :: [TcTyVar] -- Newly instantiated meta-tyvars of the function
+ -> TcM TvSubst -- Substitution mapping any of the meta-tyvars that
+ -- has been unifies to what it was instantiated to
+-- Just one level of de-wobblification though. What a hack!
+refineTyVars tvs
+ = do { mb_prs <- mapM mk_pr tvs
+ ; return (mkOpenTvSubst (mkVarEnv (catMaybes mb_prs))) }
+ where
+ mk_pr tv = do { details <- readMetaTyVar tv
+ ; case details of
+ Indirect ty -> return (Just (tv,ty))
+ other -> return Nothing
+ }
\end{code}
%************************************************************************
lazyPatErr pat tvs
= failWithTc $
hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
- 2 (vcat (map get tvs))
- where
- get tv = ASSERT( isSkolemTyVar tv ) pprSkolemTyVar tv
+ 2 (vcat (map pprTcTyVar tvs))
inaccessibleAlt msg
= hang (ptext SLIT("Inaccessible case alternative:")) 2 msg