\section[TcPat]{Typechecking patterns}
\begin{code}
-module TcPat ( tcPat, tcMonoPatBndr, tcSubPat,
- badFieldCon, polyPatSig
- ) where
+module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig, refineTyVars ) where
#include "HsVersions.h"
-import HsSyn ( InPat(..), OutPat(..), HsLit(..), HsOverLit(..), HsExpr(..) )
-import RnHsSyn ( RenamedPat )
-import TcHsSyn ( TcPat, TcId, simpleHsLitTy )
-
-import TcMonad
+import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..),
+ HsExpr(..), LHsBinds, emptyLHsBinds, isEmptyLHsBinds )
+import HsUtils
+import TcHsSyn ( TcId, hsLitType )
+import TcRnMonad
import Inst ( InstOrigin(..),
- emptyLIE, plusLIE, LIE, mkLIE, unitLIE, instToId, isEmptyLIE,
- newMethod, newOverloadedLit, newDicts
+ newMethodFromName, newOverloadedLit, newDicts,
+ instToId, tcInstStupidTheta, tcSyntaxName
)
-import Id ( mkLocalId, mkSysLocal )
+import Id ( Id, idType, mkLocalId )
+import Var ( tyVarName )
import Name ( Name )
-import FieldLabel ( fieldLabelName )
-import TcEnv ( tcLookupClass, tcLookupDataCon, tcLookupGlobalId, tcLookupId )
-import TcMType ( tcInstTyVars, newTyVarTy, getTcTyVar, putTcTyVar )
-import TcType ( TcType, TcTyVar, TcSigmaType,
- mkTyConApp, mkClassPred, liftedTypeKind, tcGetTyVar_maybe,
- isHoleTyVar, openTypeKind )
-import TcUnify ( tcSub, unifyTauTy, unifyListTy, unifyPArrTy,
- unifyTupleTy, mkCoercion, idCoercion, isIdCoercion,
- (<$>), PatCoFn )
-import TcMonoType ( tcHsSigType, UserTypeCtxt(..) )
-
-import TysWiredIn ( stringTy )
+import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
+import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
+ tcLookupClass, tcLookupDataCon, tcLookupId )
+import TcMType ( newTyFlexiVarTy, arityErr, tcSkolTyVars, readMetaTyVar )
+import TcType ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst,
+ SkolemInfo(PatSkol), isSkolemTyVar, isMetaTyVar, pprTcTyVar,
+ TvSubst, mkOpenTvSubst, substTyVar, substTy, MetaDetails(..),
+ mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy )
+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(..), gadtRefineTys, BindFlag(..) )
+import Type ( substTys, substTheta )
import CmdLineOpts ( opt_IrrefutableTuples )
-import DataCon ( dataConSig, dataConFieldLabels,
- dataConSourceArity
- )
-import Subst ( substTy, substTheta )
-import PrelNames ( eqStringName, eqName, geName, cCallableClassName )
+import TyCon ( TyCon )
+import DataCon ( DataCon, dataConTyCon, isVanillaDataCon, dataConInstOrigArgTys,
+ dataConFieldLabels, dataConSourceArity, dataConSig )
+import PrelNames ( eqStringName, eqName, geName, negateName, minusName,
+ integralClassName )
import BasicTypes ( isBoxed )
-import Bag
+import SrcLoc ( Located(..), SrcSpan, noLoc, unLoc )
+import Maybes ( catMaybes )
+import ErrUtils ( Message )
import Outputable
+import FastString
\end{code}
%************************************************************************
%* *
-\subsection{Variable patterns}
+ External interface
%* *
%************************************************************************
-\begin{code}
-type BinderChecker = Name -> TcSigmaType -> TcM (PatCoFn, LIE, TcId)
- -- How to construct a suitable (monomorphic)
- -- Id for variables found in the pattern
- -- The TcSigmaType is the expected type
- -- from the pattern context
-
--- The Id may have a sigma type (e.g. f (x::forall a. a->a))
--- so we want to *create* it during pattern type checking.
--- We don't want to make Ids first with a type-variable type
--- and then unify... becuase we can't unify a sigma type with a type variable.
-
-tcMonoPatBndr :: BinderChecker
- -- This is the right function to pass to tcPat when
- -- we're looking at a lambda-bound pattern,
- -- so there's no polymorphic guy to worry about
-
-tcMonoPatBndr binder_name pat_ty
- | Just tv <- tcGetTyVar_maybe pat_ty,
- isHoleTyVar tv
- -- If there are *no constraints* on the pattern type, we
- -- revert to good old H-M typechecking, making
- -- the type of the binder into an *ordinary*
- -- type variable. We find out if there are no constraints
- -- by seeing if we are given an "open hole" as our info.
- -- What we are trying to avoid here is giving a binder
- -- a type that is a 'hole'. The only place holes should
- -- appear is as an argument to tcPat and tcExpr/tcMonoExpr.
- = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Just ty -> tcMonoPatBndr binder_name ty
- Nothing -> newTyVarTy openTypeKind `thenNF_Tc` \ ty ->
- putTcTyVar tv ty `thenNF_Tc_`
- returnTc (idCoercion, emptyLIE, mkLocalId binder_name ty)
- | otherwise
- = returnTc (idCoercion, emptyLIE, mkLocalId binder_name pat_ty)
-\end{code}
+Note [Nesting]
+tcPat takes a "thing inside" over which the patter 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.
-%************************************************************************
-%* *
-\subsection{Typechecking patterns}
-%* *
-%************************************************************************
+This does not work so well for the ErrCtxt carried by the monad: we don't
+want the error-context for the pattern to scope over the RHS.
+Hence the getErrCtxt/setErrCtxt stuff in tcPat.
\begin{code}
-tcPat :: BinderChecker
- -> RenamedPat
-
- -> TcSigmaType -- Expected type derived from the context
- -- In the case of a function with a rank-2 signature,
- -- this type might be a forall type.
-
- -> TcM (TcPat,
- LIE, -- Required by n+k and literal pats
- Bag TcTyVar, -- TyVars bound by the pattern
- -- These are just the existentially-bound ones.
- -- Any tyvars bound by *type signatures* in the
- -- patterns are brought into scope before we begin.
- Bag (Name, TcId), -- Ids bound by the pattern, along with the Name under
- -- which it occurs in the pattern
- -- The two aren't the same because we conjure up a new
- -- local name for each variable.
- LIE) -- Dicts or methods [see below] bound by the pattern
- -- from existential constructor patterns
+tcPat :: PatCtxt
+ -> LPat Name -> Expected TcSigmaType
+ -> TcM a -- Thing inside
+ -> TcM (LPat TcId, -- Translated pattern
+ [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
+
+--------------------
+tcPats :: PatCtxt
+ -> [LPat Name]
+ -> [Expected TcSigmaType] -- Excess types discarded
+ -> TcM a
+ -> TcM ([LPat TcId], [TcTyVar], a)
+
+tcPats ctxt [] _ thing_inside
+ = do { res <- thing_inside
+ ; return ([], [], res) }
+
+tcPats ctxt (p:ps) (ty:tys) thing_inside
+ = do { (p', p_tvs, (ps', ps_tvs, res))
+ <- tcPat ctxt p ty $
+ tcPats ctxt ps tys thing_inside
+ ; return (p':ps', p_tvs ++ ps_tvs, res) }
+
+--------------------
+tcCheckPats :: PatCtxt
+ -> [LPat Name] -> [TcSigmaType]
+ -> TcM a
+ -> TcM ([LPat TcId], [TcTyVar], a)
+tcCheckPats ctxt pats tys thing_inside -- A trivial wrapper
+ = tcPats ctxt pats (map Check tys) thing_inside
\end{code}
%************************************************************************
%* *
-\subsection{Variables, wildcards, lazy pats, as-pats}
+ Binders
%* *
%************************************************************************
\begin{code}
-tcPat tc_bndr pat@(TypePatIn ty) pat_ty
- = failWithTc (badTypePat pat)
+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
+ = 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 the SigmaType: we can get
+ -- data T = MkT (forall a. a->a)
+ -- 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') }
+
+tcPatBndr (LetPat lookup_sig) bndr_name pat_ty
+ | Just sig <- lookup_sig bndr_name
+ = do { let mono_ty = sig_tau sig
+ ; mono_name <- newLocalName bndr_name
+ ; tcSubPat mono_ty pat_ty
+ ; return (mkLocalId mono_name mono_ty) }
+
+ | otherwise
+ = do { mono_name <- newLocalName bndr_name
+ ; pat_ty' <- zapExpectedType pat_ty argTypeKind
+ ; return (mkLocalId mono_name pat_ty') }
-tcPat tc_bndr (VarPatIn name) pat_ty
- = tc_bndr name pat_ty `thenTc` \ (co_fn, lie_req, bndr_id) ->
- returnTc (co_fn <$> VarPat bndr_id, lie_req,
- emptyBag, unitBag (name, bndr_id), emptyLIE)
-
-tcPat tc_bndr (LazyPatIn pat) pat_ty
- = tcPat tc_bndr pat pat_ty `thenTc` \ (pat', lie_req, tvs, ids, lie_avail) ->
- returnTc (LazyPat pat', lie_req, tvs, ids, lie_avail)
-
-tcPat tc_bndr pat_in@(AsPatIn name pat) pat_ty
- = tc_bndr name pat_ty `thenTc` \ (co_fn, lie_req1, bndr_id) ->
- tcPat tc_bndr pat pat_ty `thenTc` \ (pat', lie_req2, tvs, ids, lie_avail) ->
- returnTc (co_fn <$> (AsPat bndr_id pat'), lie_req1 `plusLIE` lie_req2,
- tvs, (name, bndr_id) `consBag` ids, lie_avail)
-
-tcPat tc_bndr WildPatIn pat_ty
- = returnTc (WildPat pat_ty, emptyLIE, emptyBag, emptyBag, emptyLIE)
-
-tcPat tc_bndr (ParPatIn parend_pat) pat_ty
- = tcPat tc_bndr parend_pat pat_ty
-
-tcPat tc_bndr pat_in@(SigPatIn pat sig) pat_ty
- = tcAddErrCtxt (patCtxt pat_in) $
- tcHsSigType PatSigCtxt sig `thenTc` \ sig_ty ->
- tcSubPat sig_ty pat_ty `thenTc` \ (co_fn, lie_sig) ->
- tcPat tc_bndr pat sig_ty `thenTc` \ (pat', lie_req, tvs, ids, lie_avail) ->
- returnTc (co_fn <$> pat', lie_req `plusLIE` lie_sig, tvs, ids, lie_avail)
+
+-------------------
+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) }
\end{code}
%************************************************************************
%* *
-\subsection{Explicit lists, parallel arrays, and tuples}
+ tc_pat: the main worker function
%* *
%************************************************************************
\begin{code}
-tcPat tc_bndr pat_in@(ListPatIn pats) pat_ty
- = tcAddErrCtxt (patCtxt pat_in) $
- unifyListTy pat_ty `thenTc` \ elem_ty ->
- tcPats tc_bndr pats (repeat elem_ty) `thenTc` \ (pats', lie_req, tvs, ids, lie_avail) ->
- returnTc (ListPat elem_ty pats', lie_req, tvs, ids, lie_avail)
-
-tcPat tc_bndr pat_in@(PArrPatIn pats) pat_ty
- = tcAddErrCtxt (patCtxt pat_in) $
- unifyPArrTy pat_ty `thenTc` \ elem_ty ->
- tcPats tc_bndr pats (repeat elem_ty) `thenTc` \ (pats', lie_req, tvs, ids, lie_avail) ->
- returnTc (PArrPat elem_ty pats', lie_req, tvs, ids, lie_avail)
+tc_lpat :: PatCtxt
+ -> LPat Name -> Expected TcSigmaType
+ -> TcM a -- Thing inside
+ -> TcM (LPat 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 $
+ tcExtendIdEnv1 name id $
+ (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
+ >> thing_inside)
+ ; let pat' | isEmptyLHsBinds binds = VarPat id
+ | otherwise = VarPatOut id binds
+ ; return (pat', [], res) }
+
+tc_pat ctxt (ParPat pat) pat_ty thing_inside
+ = do { (pat', tvs, res) <- tc_lpat ctxt pat pat_ty thing_inside
+ ; return (ParPat pat', tvs, res) }
+
+-- There's a wrinkle with irrefuatable patterns, namely that we
+-- must not propagate type refinement from them. For example
+-- data T a where { T1 :: Int -> T Int; ... }
+-- f :: T a -> Int -> a
+-- f ~(T1 i) y = y
+-- It's obviously not sound to refine a to Int in the right
+-- hand side, because the arugment might not match T1 at all!
+--
+-- Nor should a lazy pattern bind any existential type variables
+-- 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 $
+ setTypeRefinement reft thing_inside
+ ; if (null pat_tvs) then return ()
+ else lazyPatErr lpat pat_tvs
+ ; return (LazyPat pat', [], res) }
+
+tc_pat ctxt (WildPat _) pat_ty thing_inside
+ = do { pat_ty' <- zapExpectedType pat_ty argTypeKind
+ -- Note argTypeKind, so that
+ -- f _ = 3
+ -- is rejected when f applied to an unboxed tuple
+ -- However, this means that
+ -- (case g x of _ -> ...)
+ -- is rejected g returns an unboxed tuple, which is perhpas
+ -- annoying. I suppose we could pass the context into tc_pat...
+ ; res <- thing_inside
+ ; return (WildPat pat_ty', [], res) }
+
+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
+ -- 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
+ -- fails to unify with the polymorphic type for 'x'. This could
+ -- perhaps be fixed, but only with a bit more work.
+ --
+ -- If you fix it, don't forget the bindInstsOfPatIds!
+ ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
+
+tc_pat ctxt (SigPatIn pat sig) pat_ty thing_inside
+ = do { -- See Note [Pattern coercions] below
+ (sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
+ ; tcSubPat sig_ty pat_ty
+ ; 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 $
+ tc_lpat 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)
-tcPat tc_bndr pat_in@(TuplePatIn pats boxity) pat_ty
- = tcAddErrCtxt (patCtxt pat_in) $
+------------------------
+-- Lists, tuples, arrays
+tc_pat ctxt (ListPat pats _) pat_ty thing_inside
+ = do { elem_ty <- zapToListTy pat_ty
+ ; (pats', pats_tvs, res) <- tcCheckPats ctxt pats (repeat elem_ty) thing_inside
+ ; return (ListPat pats' elem_ty, pats_tvs, res) }
- unifyTupleTy boxity arity pat_ty `thenTc` \ arg_tys ->
- tcPats tc_bndr pats arg_tys `thenTc` \ (pats', lie_req, tvs, ids, lie_avail) ->
+tc_pat ctxt (PArrPat pats _) pat_ty thing_inside
+ = do { [elem_ty] <- zapToTyConApp parrTyCon pat_ty
+ ; (pats', pats_tvs, res) <- tcCheckPats ctxt pats (repeat elem_ty) thing_inside
+ ; return (PArrPat pats' elem_ty, pats_tvs, res) }
- -- possibly do the "make all tuple-pats irrefutable" test:
- let
- unmangled_result = TuplePat pats' boxity
+tc_pat ctxt (TuplePat pats boxity) pat_ty thing_inside
+ = do { let arity = length pats
+ tycon = tupleTyCon boxity arity
+ ; arg_tys <- zapToTyConApp tycon pat_ty
+ ; (pats', pats_tvs, res) <- tcCheckPats ctxt pats arg_tys thing_inside
-- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
-- so that we can experiment with lazy tuple-matching.
-- This is a pretty odd place to make the switch, but
-- it was easy to do.
+ ; let unmangled_result = TuplePat pats' boxity
+ possibly_mangled_result
+ | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
+ | otherwise = unmangled_result
+
+ ; ASSERT( length arg_tys == arity ) -- Syntactically enforced
+ return (possibly_mangled_result, pats_tvs, res) }
+
+------------------------
+-- Data constructors
+tc_pat ctxt pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
+ = do { data_con <- tcLookupDataCon con_name
+ ; let tycon = dataConTyCon data_con
+ ; ty_args <- zapToTyConApp tycon pat_ty
+ ; (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)
+ ; res <- thing_inside
+ ; returnM (LitPat simple_lit, [], res) }
+
+------------------------
+-- Overloaded patterns: n, and n+k
+tc_pat ctxt pat@(NPatIn over_lit mb_neg) 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
+ 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'
+
+ ; res <- thing_inside
+ ; returnM (NPatOut lit' pat_ty' (HsApp (nlHsVar eq) lit_expr), [], res) }
+
+tc_pat ctxt pat@(NPlusKPatIn (L nm_loc name) lit@(HsIntegral i _) minus_name) 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
- possibly_mangled_result
- | opt_IrrefutableTuples && isBoxed boxity = LazyPat unmangled_result
- | otherwise = unmangled_result
- in
- returnTc (possibly_mangled_result, lie_req, tvs, ids, lie_avail)
- where
- arity = length pats
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{Other constructors}
-%* *
-
-%************************************************************************
-
-\begin{code}
-tcPat tc_bndr pat@(ConPatIn name arg_pats) pat_ty
- = tcConPat tc_bndr pat name arg_pats pat_ty
-
-tcPat tc_bndr pat@(ConOpPatIn pat1 op _ pat2) pat_ty
- = tcConPat tc_bndr pat op [pat1, pat2] pat_ty
+ -- The '-' part is re-mappable syntax
+ ; (_, minus_expr) <- tcSyntaxName origin pat_ty' (minusName, HsVar minus_name)
+
+ -- 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']]
+ ; 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) }
\end{code}
%************************************************************************
%* *
-\subsection{Records}
+ Most of the work for constructors is here
+ (the rest is in the ConPatIn case of tc_pat)
%* *
%************************************************************************
\begin{code}
-tcPat tc_bndr pat@(RecPatIn name rpats) pat_ty
- = tcAddErrCtxt (patCtxt pat) $
-
- -- Check the constructor itself
- tcConstructor pat name `thenTc` \ (data_con, ex_tvs, dicts, lie_avail1, arg_tys, con_res_ty) ->
-
- -- Check overall type matches (c.f. tcConPat)
- tcSubPat con_res_ty pat_ty `thenTc` \ (co_fn, lie_req1) ->
- let
- -- Don't use zipEqual! If the constructor isn't really a record, then
- -- dataConFieldLabels will be empty (and each field in the pattern
- -- will generate an error below).
- field_tys = zip (map fieldLabelName (dataConFieldLabels data_con))
- arg_tys
- in
-
- -- Check the fields
- tc_fields field_tys rpats `thenTc` \ (rpats', lie_req2, tvs, ids, lie_avail2) ->
-
- returnTc (RecPat data_con pat_ty ex_tvs dicts rpats',
- lie_req1 `plusLIE` lie_req2,
- listToBag ex_tvs `unionBags` tvs,
- ids,
- lie_avail1 `plusLIE` lie_avail2)
+tcConPat :: PatCtxt -> SrcSpan -> DataCon -> TyCon -> [TcTauType]
+ -> HsConDetails Name (LPat Name) -> TcM a
+ -> TcM (Pat TcId, [TcTyVar], a)
+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 (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
+ ; span <- getSrcSpanM
+ ; let rigid_info = PatSkol data_con span
+ ; tvs' <- tcSkolTyVars rigid_info tvs
+ ; let tv_tys' = mkTyVarTys tvs'
+ tenv = zipTopTvSubst tvs tv_tys'
+ theta' = substTheta tenv theta
+ arg_tys' = substTys tenv arg_tys
+ res_tys' = substTys tenv res_tys
+ ; dicts <- newDicts (SigOrigin rigid_info) theta'
+
+ -- 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 $
+ 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 (L span data_con)
+ tvs' (map instToId dicts) dict_binds
+ arg_pats' (mkTyConApp tycon ty_args),
+ tvs' ++ inner_tvs, res) } }
+ where
+ doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
+
+tcConArgs :: PatCtxt -> DataCon
+ -> HsConDetails Name (LPat Name) -> [TcSigmaType]
+ -> TcM a
+ -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a)
+
+tcConArgs ctxt data_con (PrefixCon arg_pats) arg_tys thing_inside
+ = do { checkTc (con_arity == no_of_args) -- Check correct arity
+ (arityErr "Constructor" data_con con_arity no_of_args)
+ ; (arg_pats', tvs, res) <- tcCheckPats ctxt arg_pats arg_tys thing_inside
+ ; return (PrefixCon arg_pats', tvs, res) }
+ where
+ con_arity = dataConSourceArity data_con
+ no_of_args = length arg_pats
+
+tcConArgs ctxt data_con (InfixCon p1 p2) arg_tys thing_inside
+ = do { checkTc (con_arity == 2) -- Check correct arity
+ (arityErr "Constructor" data_con con_arity 2)
+ ; ([p1',p2'], tvs, res) <- tcCheckPats ctxt [p1,p2] arg_tys thing_inside
+ ; return (InfixCon p1' p2', tvs, res) }
+ where
+ con_arity = dataConSourceArity data_con
+tcConArgs ctxt data_con (RecCon rpats) arg_tys thing_inside
+ = do { (rpats', tvs, res) <- tc_fields rpats thing_inside
+ ; return (RecCon rpats', tvs, res) }
where
- tc_fields field_tys []
- = returnTc ([], emptyLIE, emptyBag, emptyBag, emptyLIE)
+ tc_fields :: [(Located Name, LPat Name)] -> TcM a
+ -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a)
+ tc_fields [] thing_inside
+ = do { res <- thing_inside
+ ; return ([], [], res) }
- tc_fields field_tys ((field_label, rhs_pat, pun_flag) : rpats)
- = tc_fields field_tys rpats `thenTc` \ (rpats', lie_req1, tvs1, ids1, lie_avail1) ->
+ tc_fields (rpat : rpats) thing_inside
+ = do { (rpat', tvs1, (rpats', tvs2, res))
+ <- tc_field rpat (tc_fields rpats thing_inside)
+ ; return (rpat':rpats', tvs1 ++ tvs2, res) }
- (case [ty | (f,ty) <- field_tys, f == field_label] of
+ tc_field (field_lbl, pat) thing_inside
+ = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
+ ; (pat', tvs, res) <- tcPat ctxt pat (Check pat_ty) thing_inside
+ ; return ((sel_id, pat'), tvs, res) }
+
+ find_field_ty field_lbl
+ = case [ty | (f,ty) <- field_tys, f == field_lbl] of
-- No matching field; chances are this field label comes from some
-- other record type (or maybe none). As well as reporting an
-- f (R { foo = (a,b) }) = a+b
-- If foo isn't one of R's fields, we don't want to crash when
-- typechecking the "a+b".
- [] -> addErrTc (badFieldCon name field_label) `thenNF_Tc_`
- newTyVarTy liftedTypeKind `thenNF_Tc_`
- returnTc (error "Bogus selector Id", pat_ty)
+ [] -> do { addErrTc (badFieldCon data_con field_lbl)
+ ; bogus_ty <- newTyFlexiVarTy liftedTypeKind
+ ; return (error "Bogus selector Id", bogus_ty) }
-- The normal case, when the field comes from the right constructor
(pat_ty : extras) ->
ASSERT( null extras )
- tcLookupGlobalId field_label `thenNF_Tc` \ sel_id ->
- returnTc (sel_id, pat_ty)
- ) `thenTc` \ (sel_id, pat_ty) ->
-
- tcPat tc_bndr rhs_pat pat_ty `thenTc` \ (rhs_pat', lie_req2, tvs2, ids2, lie_avail2) ->
+ do { sel_id <- tcLookupId field_lbl
+ ; return (sel_id, pat_ty) }
- returnTc ((sel_id, rhs_pat', pun_flag) : rpats',
- lie_req1 `plusLIE` lie_req2,
- tvs1 `unionBags` tvs2,
- ids1 `unionBags` ids2,
- lie_avail1 `plusLIE` lie_avail2)
+ field_tys = zip (dataConFieldLabels data_con) arg_tys
+ -- Don't use zipEqual! If the constructor isn't really a record, then
+ -- dataConFieldLabels will be empty (and each field in the pattern
+ -- will generate an error below).
\end{code}
+
%************************************************************************
%* *
-\subsection{Literals}
+ Type refinement
%* *
%************************************************************************
\begin{code}
-tcPat tc_bndr (LitPatIn lit@(HsLitLit s _)) pat_ty
- -- cf tcExpr on LitLits
- = tcLookupClass cCallableClassName `thenNF_Tc` \ cCallableClass ->
- newDicts (LitLitOrigin (_UNPK_ s))
- [mkClassPred cCallableClass [pat_ty]] `thenNF_Tc` \ dicts ->
- returnTc (LitPat (HsLitLit s pat_ty) pat_ty, mkLIE dicts, emptyBag, emptyBag, emptyLIE)
-
-tcPat tc_bndr pat@(LitPatIn lit@(HsString _)) pat_ty
- = unifyTauTy pat_ty stringTy `thenTc_`
- tcLookupGlobalId eqStringName `thenNF_Tc` \ eq_id ->
- returnTc (NPat lit stringTy (HsVar eq_id `HsApp` HsLit lit),
- emptyLIE, emptyBag, emptyBag, emptyLIE)
-
-tcPat tc_bndr (LitPatIn simple_lit) pat_ty
- = unifyTauTy pat_ty (simpleHsLitTy simple_lit) `thenTc_`
- returnTc (LitPat simple_lit pat_ty, emptyLIE, emptyBag, emptyBag, emptyLIE)
-
-tcPat tc_bndr pat@(NPatIn over_lit) pat_ty
- = newOverloadedLit (PatOrigin pat) over_lit pat_ty `thenNF_Tc` \ (over_lit_expr, lie1) ->
- tcLookupGlobalId eqName `thenNF_Tc` \ eq_sel_id ->
- newMethod origin eq_sel_id [pat_ty] `thenNF_Tc` \ eq ->
-
- returnTc (NPat lit' pat_ty (HsApp (HsVar (instToId eq)) over_lit_expr),
- lie1 `plusLIE` unitLIE eq,
- emptyBag, emptyBag, emptyLIE)
+refineAlt :: PatCtxt -> DataCon
+ -> [TcTyVar] -- Freshly bound type variables
+ -> [TcType] -- Types from the scrutinee (context)
+ -> [TcType] -- Types from the pattern
+ -> TcM a -> TcM a
+refineAlt ctxt con ex_tvs ctxt_tys pat_tys thing_inside
+ = do { old_subst <- getTypeRefinement
+ ; 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
- origin = PatOrigin pat
- lit' = case over_lit of
- HsIntegral i _ -> HsInteger i
- HsFractional f _ -> HsRat f pat_ty
+ bind_fn tv | isMetaTyVar tv = WildCard -- Wobbly types behave as wild cards
+ | otherwise = BindMe
\end{code}
-%************************************************************************
-%* *
-\subsection{n+k patterns}
-%* *
-%************************************************************************
+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}
-tcPat tc_bndr pat@(NPlusKPatIn name lit@(HsIntegral i _) minus_name) pat_ty
- = tc_bndr name pat_ty `thenTc` \ (co_fn, lie1, bndr_id) ->
- -- The '-' part is re-mappable syntax
- tcLookupId minus_name `thenNF_Tc` \ minus_sel_id ->
- tcLookupGlobalId geName `thenNF_Tc` \ ge_sel_id ->
- newOverloadedLit origin lit pat_ty `thenNF_Tc` \ (over_lit_expr, lie2) ->
- newMethod origin ge_sel_id [pat_ty] `thenNF_Tc` \ ge ->
- newMethod origin minus_sel_id [pat_ty] `thenNF_Tc` \ minus ->
-
- returnTc (NPlusKPat bndr_id i pat_ty
- (SectionR (HsVar (instToId ge)) over_lit_expr)
- (SectionR (HsVar (instToId minus)) over_lit_expr),
- lie1 `plusLIE` lie2 `plusLIE` mkLIE [ge,minus],
- emptyBag, unitBag (name, bndr_id), emptyLIE)
+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
- origin = PatOrigin pat
+ mk_pr tv = do { details <- readMetaTyVar tv
+ ; case details of
+ Indirect ty -> return (Just (tv,ty))
+ other -> return Nothing
+ }
\end{code}
%************************************************************************
%* *
-\subsection{Lists of patterns}
+ Note [Pattern coercions]
%* *
%************************************************************************
-Helper functions
+In principle, these program would be reasonable:
+
+ f :: (forall a. a->a) -> Int
+ f (x :: Int->Int) = x 3
-\begin{code}
-tcPats :: BinderChecker -- How to deal with variables
- -> [RenamedPat] -> [TcType] -- Excess 'expected types' discarded
- -> TcM ([TcPat],
- LIE, -- Required by n+k and literal pats
- Bag TcTyVar,
- Bag (Name, TcId), -- Ids bound by the pattern
- LIE) -- Dicts bound by the pattern
-
-tcPats tc_bndr [] tys = returnTc ([], emptyLIE, emptyBag, emptyBag, emptyLIE)
-
-tcPats tc_bndr (ty:tys) (pat:pats)
- = tcPat tc_bndr ty pat `thenTc` \ (pat', lie_req1, tvs1, ids1, lie_avail1) ->
- tcPats tc_bndr tys pats `thenTc` \ (pats', lie_req2, tvs2, ids2, lie_avail2) ->
-
- returnTc (pat':pats', lie_req1 `plusLIE` lie_req2,
- tvs1 `unionBags` tvs2, ids1 `unionBags` ids2,
- lie_avail1 `plusLIE` lie_avail2)
-\end{code}
+ g :: (forall a. [a]) -> Bool
+ g [] = True
-------------------------------------------------------
-\begin{code}
-tcConstructor pat con_name
- = -- Check that it's a constructor
- tcLookupDataCon con_name `thenNF_Tc` \ data_con ->
-
- -- Instantiate it
- let
- (tvs, _, ex_tvs, ex_theta, arg_tys, tycon) = dataConSig data_con
- -- Ignore the theta; overloaded constructors only
- -- behave differently when called, not when used for
- -- matching.
- in
- tcInstTyVars (ex_tvs ++ tvs) `thenNF_Tc` \ (all_tvs', ty_args', tenv) ->
- let
- ex_theta' = substTheta tenv ex_theta
- arg_tys' = map (substTy tenv) arg_tys
-
- n_ex_tvs = length ex_tvs
- ex_tvs' = take n_ex_tvs all_tvs'
- result_ty = mkTyConApp tycon (drop n_ex_tvs ty_args')
- in
- newDicts (PatOrigin pat) ex_theta' `thenNF_Tc` \ dicts ->
-
- returnTc (data_con, ex_tvs', map instToId dicts, mkLIE dicts, arg_tys', result_ty)
-\end{code}
-
-------------------------------------------------------
-\begin{code}
-tcConPat tc_bndr pat con_name arg_pats pat_ty
- = tcAddErrCtxt (patCtxt pat) $
-
- -- Check the constructor itself
- tcConstructor pat con_name `thenTc` \ (data_con, ex_tvs, dicts, lie_avail1, arg_tys, con_res_ty) ->
-
- -- Check overall type matches.
- -- The pat_ty might be a for-all type, in which
- -- case we must instantiate to match
- tcSubPat con_res_ty pat_ty `thenTc` \ (co_fn, lie_req1) ->
-
- -- Check correct arity
- let
- con_arity = dataConSourceArity data_con
- no_of_args = length arg_pats
- in
- checkTc (con_arity == no_of_args)
- (arityErr "Constructor" data_con con_arity no_of_args) `thenTc_`
-
- -- Check arguments
- tcPats tc_bndr arg_pats arg_tys `thenTc` \ (arg_pats', lie_req2, tvs, ids, lie_avail2) ->
-
- returnTc (co_fn <$> ConPat data_con pat_ty ex_tvs dicts arg_pats',
- lie_req1 `plusLIE` lie_req2,
- listToBag ex_tvs `unionBags` tvs,
- ids,
- lie_avail1 `plusLIE` lie_avail2)
-\end{code}
+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 type-system 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).
-%************************************************************************
-%* *
-\subsection{Subsumption}
-%* *
-%************************************************************************
+So for now I'm just insisting on type *equality* in patterns. No subsumption.
-Example:
- f :: (forall a. a->a) -> Int -> Int
- f (g::Int->Int) y = g y
-This is ok: the type signature allows fewer callers than
-the (more general) signature f :: (Int->Int) -> Int -> Int
-I.e. (forall a. a->a) <= Int -> Int
-We end up translating this to:
- f = \g' :: (forall a. a->a). let g = g' Int in g' y
-
-tcSubPat does the work
- sig_ty is the signature on the pattern itself
- (Int->Int in the example)
- expected_ty is the type passed inwards from the context
- (forall a. a->a in the example)
+Old notes about desugaring, at a time when pattern coercions were handled:
-\begin{code}
-tcSubPat :: TcSigmaType -> TcSigmaType -> TcM (PatCoFn, LIE)
-
-tcSubPat sig_ty exp_ty
- = tcSub sig_ty exp_ty `thenTc` \ (co_fn, lie) ->
- -- co_fn is a coercion on *expressions*, and we
- -- need to make a coercion on *patterns*
- if isIdCoercion co_fn then
- ASSERT( isEmptyLIE lie )
- returnNF_Tc (idCoercion, emptyLIE)
- else
- tcGetUnique `thenNF_Tc` \ uniq ->
- let
- arg_id = mkSysLocal FSLIT("sub") uniq exp_ty
- the_fn = DictLam [arg_id] (co_fn <$> HsVar arg_id)
- pat_co_fn p = SigPat p exp_ty the_fn
- in
- returnNF_Tc (mkCoercion pat_co_fn, lie)
-\end{code}
+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 non-identity 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)
%************************************************************************
%************************************************************************
\begin{code}
-patCtxt pat = hang (ptext SLIT("When checking the pattern:"))
- 4 (ppr pat)
-
-badFieldCon :: Name -> Name -> SDoc
+patCtxt :: Pat Name -> Maybe Message -- Not all patterns are worth pushing a context
+patCtxt (VarPat _) = Nothing
+patCtxt (ParPat _) = Nothing
+patCtxt (AsPat _ _) = Nothing
+patCtxt pat = Just (hang (ptext SLIT("When checking the pattern:"))
+ 4 (ppr pat))
+
+badFieldCon :: DataCon -> Name -> SDoc
badFieldCon con field
= hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
ptext SLIT("does not have field"), quotes (ppr field)]
4 (ppr sig_ty)
badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
-\end{code}
+lazyPatErr pat tvs
+ = failWithTc $
+ hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
+ 2 (vcat (map pprTcTyVar tvs))
+
+inaccessibleAlt msg
+ = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
+\end{code}
projects / ghc-hetmet.git / blobdiff