%
+% (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 ( tcPat, tcPats, tcOverloadedLit,
- PatCtxt(..), badFieldCon, polyPatSig ) where
+module TcPat ( tcLetPat, TcSigFun, TcSigInfo(..), TcPragFun
+ , LetBndrSpec(..), addInlinePrags, warnPrags
+ , tcPat, tcPats, newNoSigLetBndr, newSigLetBndr
+ , addDataConStupidTheta, badFieldCon, polyPatSig ) where
#include "HsVersions.h"
-import {-# SOURCE #-} TcExpr( tcSyntaxOp )
-import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..),
- LHsBinds, emptyLHsBinds, isEmptyLHsBinds,
- collectPatsBinders, nlHsLit )
-import TcHsSyn ( TcId, hsLitType )
+import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcInferRho)
+
+import HsSyn
+import TcHsSyn
import TcRnMonad
-import Inst ( InstOrigin(..), shortCutFracLit, shortCutIntLit,
- newDicts, instToId, tcInstStupidTheta, isHsVar
- )
-import Id ( Id, idType, mkLocalId )
-import CoreFVs ( idFreeTyVars )
-import Name ( Name, mkSystemVarName )
-import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
-import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
- tcLookupClass, tcLookupDataCon, tcLookupId, refineEnvironment,
- tcMetaTy )
-import TcMType ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, newBoxyTyVar, zonkTcType )
-import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType,
- SkolemInfo(PatSkol),
- BoxySigmaType, BoxyRhoType,
- pprSkolTvBinding, isRefineableTy, isRigidTy, tcTyVarsOfTypes, mkTyVarTy, lookupTyVar,
- emptyTvSubst, substTyVar, substTy, mkTopTvSubst, zipTopTvSubst, zipOpenTvSubst,
- mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy,
- mkFunTy, mkFunTys, exactTyVarsOfTypes,
- tidyOpenType, tidyOpenTypes )
-import VarSet ( elemVarSet, mkVarSet )
-import Kind ( liftedTypeKind, openTypeKind )
-import TcUnify ( boxySplitTyConApp, boxySplitListTy,
- unBox, stripBoxyType, zapToMonotype,
- boxyMatchTypes, boxyUnify, boxyUnifyList, checkSigTyVarsWrt )
-import TcHsType ( UserTypeCtxt(..), tcPatSig )
-import TysWiredIn ( boolTy, parrTyCon, tupleTyCon )
-import Unify ( MaybeErr(..), gadtRefineTys )
-import Type ( substTys, substTheta )
-import StaticFlags ( opt_IrrefutableTuples )
-import TyCon ( TyCon )
-import DataCon ( DataCon, dataConTyCon, isVanillaDataCon,
- dataConFieldLabels, dataConSourceArity, dataConSig )
-import PrelNames ( integralClassName, fromIntegerName, integerTyConName,
- fromRationalName, rationalTyConName )
-import BasicTypes ( isBoxed )
-import SrcLoc ( Located(..), SrcSpan, noLoc )
-import ErrUtils ( Message )
-import Util ( takeList, zipEqual )
+import Inst
+import Id
+import Var
+import Name
+import TcEnv
+import TcMType
+import TcType
+import TcUnify
+import TcHsType
+import TysWiredIn
+import Coercion
+import StaticFlags
+import TyCon
+import DataCon
+import PrelNames
+import BasicTypes hiding (SuccessFlag(..))
+import DynFlags
+import SrcLoc
+import ErrUtils
+import Util
import Outputable
import FastString
+import Control.Monad
\end{code}
%************************************************************************
\begin{code}
-tcPats :: PatCtxt
- -> [LPat Name] -- Patterns,
- -> [BoxySigmaType] -- and their types
- -> BoxyRhoType -- Result type,
- -> (BoxyRhoType -> TcM a) -- and the checker for the body
- -> TcM ([LPat TcId], a)
+tcLetPat :: TcSigFun -> LetBndrSpec
+ -> LPat Name -> TcSigmaType
+ -> TcM a
+ -> TcM (LPat TcId, a)
+tcLetPat sig_fn no_gen pat pat_ty thing_inside
+ = tc_lpat pat pat_ty penv thing_inside
+ where
+ penv = PE { pe_lazy = True
+ , pe_ctxt = LetPat sig_fn no_gen }
+
+-----------------
+tcPats :: HsMatchContext Name
+ -> [LPat Name] -- Patterns,
+ -> [TcSigmaType] -- and their types
+ -> TcM a -- and the checker for the body
+ -> TcM ([LPat TcId], a)
-- This is the externally-callable wrapper function
-- Typecheck the patterns, extend the environment to bind the variables,
-- 1. Initialise the PatState
-- 2. Check the patterns
--- 3. Apply the refinement
--- 4. Check the body
--- 5. Check that no existentials escape
+-- 3. Check the body
+-- 4. Check that no existentials escape
+
+tcPats ctxt pats pat_tys thing_inside
+ = tc_lpats penv pats pat_tys thing_inside
+ where
+ penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt }
-tcPats ctxt pats tys res_ty thing_inside
- = do { let init_state = PS { pat_ctxt = ctxt, pat_reft = emptyTvSubst }
+tcPat :: HsMatchContext Name
+ -> LPat Name -> TcSigmaType
+ -> TcM a -- Checker for body, given
+ -- its result type
+ -> TcM (LPat TcId, a)
+tcPat ctxt pat pat_ty thing_inside
+ = tc_lpat pat pat_ty penv thing_inside
+ where
+ penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt }
+
- ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' ->
- refineEnvironment (pat_reft pstate') $
- thing_inside (refineType (pat_reft pstate') res_ty)
+-----------------
+data PatEnv
+ = PE { pe_lazy :: Bool -- True <=> lazy context, so no existentials allowed
+ , pe_ctxt :: PatCtxt -- Context in which the whole pattern appears
+ }
- ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty
+data PatCtxt
+ = LamPat -- Used for lambdas, case etc
+ (HsMatchContext Name)
- ; returnM (pats', res) }
+ | LetPat -- Used only for let(rec) bindings
+ -- See Note [Let binders]
+ TcSigFun -- Tells type sig if any
+ LetBndrSpec -- True <=> no generalisation of this let
+data LetBndrSpec
+ = LetLclBndr -- The binder is just a local one;
+ -- an AbsBinds will provide the global version
------------------
-tcPat :: PatCtxt
- -> LPat Name -> BoxySigmaType
- -> BoxyRhoType -- Result type
- -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
- -> TcM (LPat TcId, a)
-tcPat ctxt pat pat_ty res_ty thing_inside
- = do { ([pat'],thing) <- tcPats ctxt [pat] [pat_ty] res_ty thing_inside
- ; return (pat', thing) }
+ | LetGblBndr TcPragFun -- There isn't going to be an AbsBinds;
+ -- here is the inline-pragma information
+makeLazy :: PatEnv -> PatEnv
+makeLazy penv = penv { pe_lazy = True }
------------------
-tcCheckExistentialPat :: PatCtxt
- -> [LPat TcId] -- Patterns (just for error message)
- -> [TcTyVar] -- Existentially quantified tyvars bound by pattern
- -> [BoxySigmaType] -- Types of the patterns
- -> BoxyRhoType -- Type of the body of the match
- -- Tyvars in either of these must not escape
- -> TcM ()
--- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat
--- For example, we must reject this program:
--- data C = forall a. C (a -> Int)
--- f (C g) x = g x
--- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
-
-tcCheckExistentialPat ctxt pats [] pat_tys body_ty
- = return () -- Short cut for case when there are no existentials
-
-tcCheckExistentialPat (LetPat _) pats ex_tvs pat_tys body_ty
- -- Don't know how to deal with pattern-bound existentials yet
- = failWithTc (existentialExplode pats)
-
-tcCheckExistentialPat ctxt pats ex_tvs pat_tys body_ty
- = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys body_ty) $
- checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
-
-data PatState = PS {
- pat_ctxt :: PatCtxt,
- pat_reft :: GadtRefinement -- Binds rigid TcTyVars to their refinements
- }
-
-data PatCtxt
- = LamPat
- | LetPat (Name -> Maybe TcRhoType) -- Used for let(rec) bindings
-
-patSigCtxt :: PatState -> UserTypeCtxt
-patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
-patSigCtxt other = LamPatSigCtxt
+patSigCtxt :: PatEnv -> UserTypeCtxt
+patSigCtxt (PE { pe_ctxt = LetPat {} }) = BindPatSigCtxt
+patSigCtxt (PE { pe_ctxt = LamPat {} }) = LamPatSigCtxt
+
+---------------
+type TcPragFun = Name -> [LSig Name]
+type TcSigFun = Name -> Maybe TcSigInfo
+
+data TcSigInfo
+ = TcSigInfo {
+ sig_id :: TcId, -- *Polymorphic* binder for this value...
+
+ sig_scoped :: [Name], -- Scoped type variables
+ -- 1-1 correspondence with a prefix of sig_tvs
+ -- However, may be fewer than sig_tvs;
+ -- see Note [More instantiated than scoped]
+ sig_tvs :: [TcTyVar], -- Instantiated type variables
+ -- See Note [Instantiate sig]
+
+ sig_theta :: TcThetaType, -- Instantiated theta
+
+ sig_tau :: TcSigmaType, -- Instantiated tau
+ -- See Note [sig_tau may be polymorphic]
+
+ sig_loc :: SrcSpan -- The location of the signature
+ }
+
+instance Outputable TcSigInfo where
+ ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
+ = ppr id <+> ptext (sLit "::") <+> ppr tyvars <+> pprThetaArrow theta <+> ppr tau
\end{code}
+Note [sig_tau may be polymorphic]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note that "sig_tau" might actually be a polymorphic type,
+if the original function had a signature like
+ forall a. Eq a => forall b. Ord b => ....
+But that's ok: tcMatchesFun (called by tcRhs) can deal with that
+It happens, too! See Note [Polymorphic methods] in TcClassDcl.
+
+Note [Let binders]
+~~~~~~~~~~~~~~~~~~
+eg x :: Int
+ y :: Bool
+ (x,y) = e
+
+...more notes to add here..
+
+
+Note [Existential check]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Lazy patterns can't bind existentials. They arise in two ways:
+ * Let bindings let { C a b = e } in b
+ * Twiddle patterns f ~(C a b) = e
+The pe_lazy field of PatEnv says whether we are inside a lazy
+pattern (perhaps deeply)
+
+If we aren't inside a lazy pattern then we can bind existentials,
+but we need to be careful about "extra" tyvars. Consider
+ (\C x -> d) : pat_ty -> res_ty
+When looking for existential escape we must check that the existential
+bound by C don't unify with the free variables of pat_ty, OR res_ty
+(or of course the environment). Hence we need to keep track of the
+res_ty free vars.
%************************************************************************
%************************************************************************
\begin{code}
-tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
-tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
- = do { pat_ty' <- unBox pat_ty
- -- We have an undecorated binder, so we do rule ABS1,
- -- by unboxing the boxy type, forcing any un-filled-in
- -- boxes to become monotypes
- -- NB that pat_ty' can still be a polytype:
- -- 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 (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) }
-
+tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (CoercionI, TcId)
+-- (coi, xp) = tcPatBndr penv x pat_ty
+-- Then coi : pat_ty ~ typeof(xp)
+--
+tcPatBndr (PE { pe_ctxt = LetPat lookup_sig no_gen}) bndr_name pat_ty
+ | Just sig <- lookup_sig bndr_name
+ = do { bndr_id <- newSigLetBndr no_gen bndr_name sig
+ ; coi <- unifyPatType (idType bndr_id) pat_ty
+ ; return (coi, bndr_id) }
+
| otherwise
- = do { pat_ty' <- unBox pat_ty
- ; mono_name <- newLocalName bndr_name
- ; return (mkLocalId mono_name pat_ty') }
+ = do { bndr_id <- newNoSigLetBndr no_gen bndr_name pat_ty
+ ; return (IdCo pat_ty, bndr_id) }
+
+tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
+ = do { bndr <- mkLocalBinder bndr_name pat_ty
+ ; return (IdCo pat_ty, bndr) }
+
+------------
+newSigLetBndr :: LetBndrSpec -> Name -> TcSigInfo -> TcM TcId
+newSigLetBndr LetLclBndr name sig
+ = do { mono_name <- newLocalName name
+ ; mkLocalBinder mono_name (sig_tau sig) }
+newSigLetBndr (LetGblBndr prags) name sig
+ = addInlinePrags (sig_id sig) (prags name)
+
+------------
+newNoSigLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
+-- In the polymorphic case (no_gen = False), generate a "monomorphic version"
+-- of the Id; the original name will be bound to the polymorphic version
+-- by the AbsBinds
+-- In the monomorphic case there is no AbsBinds, and we use the original
+-- name directly
+newNoSigLetBndr LetLclBndr name ty
+ =do { mono_name <- newLocalName name
+ ; mkLocalBinder mono_name ty }
+newNoSigLetBndr (LetGblBndr prags) name ty
+ = do { id <- mkLocalBinder name ty
+ ; addInlinePrags id (prags name) }
+
+----------
+addInlinePrags :: TcId -> [LSig Name] -> TcM TcId
+addInlinePrags poly_id prags
+ = tc_inl inl_sigs
+ where
+ inl_sigs = filter isInlineLSig prags
+ tc_inl [] = return poly_id
+ tc_inl (L loc (InlineSig _ prag) : other_inls)
+ = do { unless (null other_inls) (setSrcSpan loc warn_dup_inline)
+ ; return (poly_id `setInlinePragma` prag) }
+ tc_inl _ = panic "tc_inl"
+
+ warn_dup_inline = warnPrags poly_id inl_sigs $
+ ptext (sLit "Duplicate INLINE pragmas for")
+
+warnPrags :: Id -> [LSig Name] -> SDoc -> TcM ()
+warnPrags id bad_sigs herald
+ = addWarnTc (hang (herald <+> quotes (ppr id))
+ 2 (ppr_sigs bad_sigs))
+ where
+ ppr_sigs sigs = vcat (map (ppr . getLoc) sigs)
+-----------------
+mkLocalBinder :: Name -> TcType -> TcM TcId
+mkLocalBinder name ty
+ = do { checkUnboxedTuple ty $
+ ptext (sLit "The variable") <+> quotes (ppr name)
+ ; return (Id.mkLocalId name ty) }
+
+checkUnboxedTuple :: TcType -> SDoc -> TcM ()
+-- Check for an unboxed tuple type
+-- f = (# True, False #)
+-- Zonk first just in case it's hidden inside a meta type variable
+-- (This shows up as a (more obscure) kind error
+-- in the 'otherwise' case of tcMonoBinds.)
+checkUnboxedTuple ty what
+ = do { zonked_ty <- zonkTcTypeCarefully ty
+ ; checkTc (not (isUnboxedTupleType zonked_ty))
+ (unboxedTupleErr what zonked_ty) }
-------------------
-bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
+{- Only needed if we re-add Method constraints
+bindInstsOfPatId :: TcId -> TcM a -> TcM (a, TcEvBinds)
bindInstsOfPatId id thing_inside
| not (isOverloadedTy (idType id))
- = do { res <- thing_inside; return (res, emptyLHsBinds) }
+ = do { res <- thing_inside; return (res, emptyTcEvBinds) }
| otherwise
- = do { (res, lie) <- getLIE thing_inside
- ; binds <- bindInstsOfLocalFuns lie [id]
+ = do { (res, lie) <- captureConstraints thing_inside
+ ; binds <- bindLocalMethods lie [id]
; return (res, binds) }
+-}
\end{code}
+Note [Polymorphism and pattern bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When is_mono holds we are not generalising
+But the signature can still be polymoprhic!
+ data T = MkT (forall a. a->a)
+ x :: forall a. a->a
+ MkT x = <rhs>
+So the no_gen flag decides whether the pattern-bound variables should
+have exactly the type in the type signature (when not generalising) or
+the instantiated version (when generalising)
%************************************************************************
%* *
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.
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 tc_lpats.
+Hence the getErrCtxt/setErrCtxt stuff in tcMultiple
\begin{code}
--------------------
-tc_lpats :: PatState
- -> [LPat Name]
- -> [BoxySigmaType]
- -> (PatState -> TcM a)
- -> TcM ([LPat TcId], [TcTyVar], a)
-
-tc_lpats pstate pats pat_tys thing_inside
+type Checker inp out = forall r.
+ inp
+ -> PatEnv
+ -> TcM r
+ -> TcM (out, r)
+
+tcMultiple :: Checker inp out -> Checker [inp] [out]
+tcMultiple tc_pat args penv thing_inside
= do { err_ctxt <- getErrCtxt
- ; let loop pstate [] []
- = do { res <- thing_inside pstate
- ; return ([], [], res) }
+ ; let loop _ []
+ = do { res <- thing_inside
+ ; return ([], res) }
- loop pstate (p:ps) (ty:tys)
- = do { (p', p_tvs, (ps', ps_tvs, res))
- <- tc_lpat pstate p ty $ \ pstate' ->
+ loop penv (arg:args)
+ = do { (p', (ps', res))
+ <- tc_pat arg penv $
setErrCtxt err_ctxt $
- loop pstate' ps tys
+ loop penv args
-- setErrCtxt: restore context before doing the next pattern
-- See note [Nesting] above
- ; return (p':ps', p_tvs ++ ps_tvs, res) }
+ ; return (p':ps', res) }
- loop _ _ _ = pprPanic "tc_lpats" (ppr pats $$ ppr pat_tys)
-
- ; loop pstate pats pat_tys }
+ ; loop penv args }
--------------------
-tc_lpat :: PatState
- -> LPat Name
- -> BoxySigmaType
- -> (PatState -> TcM a)
- -> TcM (LPat TcId, [TcTyVar], a)
-tc_lpat pstate (L span pat) pat_ty thing_inside
+tc_lpat :: LPat Name
+ -> TcSigmaType
+ -> PatEnv
+ -> TcM a
+ -> TcM (LPat TcId, a)
+tc_lpat (L span pat) pat_ty penv thing_inside
= setSrcSpan span $
maybeAddErrCtxt (patCtxt pat) $
- do { let pat_ty' = refineType (pat_reft pstate) pat_ty
- -- Make sure the result type reflects the current refinement
- ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
- ; return (L span pat', tvs, res) }
-
+ do { (pat', res) <- tc_pat penv pat pat_ty thing_inside
+ ; return (L span pat', res) }
+
+tc_lpats :: PatEnv
+ -> [LPat Name] -> [TcSigmaType]
+ -> TcM a
+ -> TcM ([LPat TcId], a)
+tc_lpats penv pats tys thing_inside
+ = tcMultiple (\(p,t) -> tc_lpat p t)
+ (zipEqual "tc_lpats" pats tys)
+ penv thing_inside
--------------------
-tc_pat :: PatState
- -> Pat Name -> BoxySigmaType -- Fully refined result type
- -> (PatState -> TcM a) -- Thing inside
- -> TcM (Pat TcId, -- Translated pattern
- [TcTyVar], -- Existential binders
- a) -- Result of thing inside
-
-tc_pat pstate (VarPat name) pat_ty thing_inside
- = do { id <- tcPatBndr pstate name pat_ty
+tc_pat :: PatEnv
+ -> Pat Name
+ -> TcSigmaType -- Fully refined result type
+ -> TcM a -- Thing inside
+ -> TcM (Pat TcId, -- Translated pattern
+ a) -- Result of thing inside
+
+tc_pat penv (VarPat name) pat_ty thing_inside
+ = do { (coi, id) <- tcPatBndr penv name pat_ty
+ ; res <- tcExtendIdEnv1 name id thing_inside
+ ; return (mkHsWrapPatCoI coi (VarPat id) pat_ty, res) }
+
+{- Need this if we re-add Method constraints
; (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 pstate pat pat_ty thing_inside
- ; return (ParPat pat', tvs, res) }
-
-tc_pat pstate (BangPat pat) pat_ty thing_inside
- = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
- ; return (BangPat pat', tvs, res) }
-
--- There's a wrinkle with irrefutable 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 pstate lpat@(LazyPat pat) pat_ty thing_inside
- = do { (pat', pat_tvs, res) <- tc_lpat pstate pat pat_ty $ \ _ ->
- thing_inside pstate
- -- Ignore refined pstate',
- -- revert to pstate
- -- Check no existentials
- ; if (null pat_tvs) then return ()
- else lazyPatErr lpat pat_tvs
-
- -- Check that the pattern has a lifted type
- ; pat_tv <- newBoxyTyVar liftedTypeKind
- ; boxyUnify pat_ty (mkTyVarTy pat_tv)
-
- ; return (LazyPat pat', [], res) }
-
-tc_pat pstate (WildPat _) pat_ty thing_inside
- = do { pat_ty' <- unBox pat_ty -- Make sure it's filled in with monotypes
- ; 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 pstate pat (idType bndr_id) thing_inside
+ >> thing_inside)
+ ; let pat' | isEmptyTcEvBinds binds = VarPat id
+ | otherwise = VarPatOut id binds
+ ; return (mkHsWrapPatCoI coi pat' pat_ty, res) }
+-}
+
+tc_pat penv (ParPat pat) pat_ty thing_inside
+ = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
+ ; return (ParPat pat', res) }
+
+tc_pat penv (BangPat pat) pat_ty thing_inside
+ = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
+ ; return (BangPat pat', res) }
+
+tc_pat penv lpat@(LazyPat pat) pat_ty thing_inside
+ = do { (pat', (res, pat_ct))
+ <- tc_lpat pat pat_ty (makeLazy penv) $
+ captureConstraints thing_inside
+ -- Ignore refined penv', revert to penv
+
+ ; emitConstraints pat_ct
+ -- captureConstraints/extendConstraints:
+ -- see Note [Hopping the LIE in lazy patterns]
+
+ -- Check there are no unlifted types under the lazy pattern
+ ; when (any (isUnLiftedType . idType) $ collectPatBinders pat') $
+ lazyUnliftedPatErr lpat
+
+ -- Check that the expected pattern type is itself lifted
+ ; pat_ty' <- newFlexiTyVarTy liftedTypeKind
+ ; _ <- unifyType pat_ty pat_ty'
+
+ ; return (LazyPat pat', res) }
+
+tc_pat _ p@(QuasiQuotePat _) _ _
+ = pprPanic "Should never see QuasiQuotePat in type checker" (ppr p)
+
+tc_pat _ (WildPat _) pat_ty thing_inside
+ = do { checkUnboxedTuple pat_ty $
+ ptext (sLit "A wild-card pattern")
+ ; res <- thing_inside
+ ; return (WildPat pat_ty, res) }
+
+tc_pat penv (AsPat (L nm_loc name) pat) pat_ty thing_inside
+ = do { (coi, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty)
+ ; (pat', res) <- tcExtendIdEnv1 name bndr_id $
+ tc_lpat pat (idType bndr_id) penv 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
-- 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) }
+ ; return (mkHsWrapPatCoI coi (AsPat (L nm_loc bndr_id) pat') pat_ty, res) }
+
+tc_pat penv vpat@(ViewPat expr pat _) overall_pat_ty thing_inside
+ = do { checkUnboxedTuple overall_pat_ty $
+ ptext (sLit "The view pattern") <+> ppr vpat
+
+ -- Morally, expr must have type `forall a1...aN. OPT' -> B`
+ -- where overall_pat_ty is an instance of OPT'.
+ -- Here, we infer a rho type for it,
+ -- which replaces the leading foralls and constraints
+ -- with fresh unification variables.
+ ; (expr',expr'_inferred) <- tcInferRho expr
+
+ -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty`
+ -- NOTE: this forces pat_ty to be a monotype (because we use a unification
+ -- variable to find it). this means that in an example like
+ -- (view -> f) where view :: _ -> forall b. b
+ -- we will only be able to use view at one instantation in the
+ -- rest of the view
+ ; (expr_coi, pat_ty) <- tcInfer $ \ pat_ty ->
+ unifyPatType expr'_inferred (mkFunTy overall_pat_ty pat_ty)
+
+ -- pattern must have pat_ty
+ ; (pat', res) <- tc_lpat pat pat_ty penv thing_inside
+
+ ; return (ViewPat (mkLHsWrapCoI expr_coi expr') pat' overall_pat_ty, res) }
-- Type signatures in patterns
-- See Note [Pattern coercions] below
-tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
- = do { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
- ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
- tc_lpat pstate pat inner_ty thing_inside
- ; return (SigPatOut pat' inner_ty, tvs, res) }
+tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside
+ = do { (inner_ty, tv_binds, wrap) <- tcPatSig (patSigCtxt penv) sig_ty pat_ty
+ ; (pat', res) <- tcExtendTyVarEnv2 tv_binds $
+ tc_lpat pat inner_ty penv thing_inside
+
+ ; return (mkHsWrapPat wrap (SigPatOut pat' inner_ty) pat_ty, res) }
-tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
+tc_pat _ pat@(TypePat _) _ _
= failWithTc (badTypePat pat)
------------------------
-- Lists, tuples, arrays
-tc_pat pstate (ListPat pats _) pat_ty thing_inside
- = do { elt_ty <- boxySplitListTy pat_ty
- ; let elt_tys = takeList pats (repeat elt_ty)
- ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
- ; return (ListPat pats' elt_ty, pats_tvs, res) }
-
-tc_pat pstate (PArrPat pats _) pat_ty thing_inside
- = do { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty
- ; let elt_tys = takeList pats (repeat elt_ty)
- ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
- ; ifM (null pats) (zapToMonotype pat_ty) -- c.f. ExplicitPArr in TcExpr
- ; return (PArrPat pats' elt_ty, pats_tvs, res) }
-
-tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
- = do { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
- ; (pats', pats_tvs, res) <- tc_lpats pstate pats arg_tys thing_inside
+tc_pat penv (ListPat pats _) pat_ty thing_inside
+ = do { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy pat_ty
+ ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
+ pats penv thing_inside
+ ; return (mkHsWrapPat coi (ListPat pats' elt_ty) pat_ty, res)
+ }
+
+tc_pat penv (PArrPat pats _) pat_ty thing_inside
+ = do { (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTy pat_ty
+ ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty)
+ pats penv thing_inside
+ ; return (mkHsWrapPat coi (PArrPat pats' elt_ty) pat_ty, res)
+ }
+
+tc_pat penv (TuplePat pats boxity _) pat_ty thing_inside
+ = do { let tc = tupleTyCon boxity (length pats)
+ ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) pat_ty
+ ; (pats', res) <- tc_lpats penv 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 pat_ty
+ ; let pat_ty' = mkTyConApp tc arg_tys
+ -- pat_ty /= pat_ty iff coi /= IdCo
+ unmangled_result = TuplePat pats' boxity pat_ty'
possibly_mangled_result
- | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
- | otherwise = unmangled_result
+ | opt_IrrefutableTuples &&
+ isBoxed boxity = LazyPat (noLoc unmangled_result)
+ | otherwise = unmangled_result
- ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced
- return (possibly_mangled_result, pats_tvs, res) }
+ ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced
+ return (mkHsWrapPat coi possibly_mangled_result pat_ty, res)
+ }
------------------------
-- Data constructors
-tc_pat pstate 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
- ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
+tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside
+ = tcConPat penv con pat_ty arg_pats thing_inside
------------------------
-- Literal patterns
-tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
- = do { boxyUnify (hsLitType simple_lit) pat_ty
- ; res <- thing_inside pstate
- ; returnM (LitPat simple_lit, [], res) }
+tc_pat _ (LitPat simple_lit) pat_ty thing_inside
+ = do { let lit_ty = hsLitType simple_lit
+ ; coi <- unifyPatType lit_ty pat_ty
+ -- coi is of kind: pat_ty ~ lit_ty
+ ; res <- thing_inside
+ ; return ( mkHsWrapPatCoI coi (LitPat simple_lit) pat_ty
+ , res) }
------------------------
-- Overloaded patterns: n, and n+k
-tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside
+tc_pat _ (NPat over_lit mb_neg eq) pat_ty thing_inside
= do { let orig = LiteralOrigin over_lit
- ; lit' <- tcOverloadedLit orig over_lit pat_ty
+ ; lit' <- newOverloadedLit 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
-- The 'negate' is re-mappable syntax
do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
; return (Just neg') }
- ; res <- thing_inside pstate
- ; returnM (NPat lit' mb_neg' eq' pat_ty, [], res) }
+ ; res <- thing_inside
+ ; return (NPat lit' mb_neg' eq', res) }
-tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
- = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
+tc_pat penv (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
+ = do { (coi, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty)
; let pat_ty' = idType bndr_id
orig = LiteralOrigin lit
- ; lit' <- tcOverloadedLit orig lit pat_ty'
+ ; lit' <- newOverloadedLit orig lit pat_ty'
-- 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')
+ ; let pat' = NPlusKPat (L nm_loc bndr_id) lit' ge' minus'
-- The Report says that n+k patterns must be in Integral
-- We may not want this when using re-mappable syntax, though (ToDo?)
; icls <- tcLookupClass integralClassName
- ; dicts <- newDicts orig [mkClassPred icls [pat_ty']]
- ; extendLIEs dicts
+ ; instStupidTheta orig [mkClassPred icls [pat_ty']]
- ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
- ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
-
-tc_pat _ _other_pat _ _ = panic "tc_pat" -- DictPat, ConPatOut, SigPatOut, VarPatOut
+ ; res <- tcExtendIdEnv1 name bndr_id thing_inside
+ ; return (mkHsWrapPatCoI coi pat' pat_ty, res) }
+
+tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut, VarPatOut
+
+----------------
+unifyPatType :: TcType -> TcType -> TcM CoercionI
+-- In patterns we want a coercion from the
+-- context type (expected) to the actual pattern type
+-- But we don't want to reverse the args to unifyType because
+-- that controls the actual/expected stuff in error messages
+unifyPatType actual_ty expected_ty
+ = do { coi <- unifyType actual_ty expected_ty
+ ; return (mkSymCoI coi) }
\end{code}
+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 captureConstraints and emitConstraints.
+
+The same thing ensures that equality constraints in a lazy match
+are not made available in the RHS of the match. 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!
+
+Finally, a lazy pattern should not bind any existential type variables
+because they won't be in scope when we do the desugaring
+
%************************************************************************
%* *
%* *
%************************************************************************
+[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 -- Type of the pattern
- -> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
- -> TcM (Pat TcId, [TcTyVar], a)
-tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
- | isVanillaDataCon data_con
- = do { ty_args <- boxySplitTyConApp tycon pat_ty
- ; let (tvs, _, arg_tys, _, _) = dataConSig data_con
- arg_tvs = exactTyVarsOfTypes arg_tys
- -- See Note [Silly type synonyms in smart-app] in TcExpr
- -- for why we must use exactTyVarsOfTypes
- inst_prs = zipEqual "tcConPat" tvs ty_args
- subst = mkTopTvSubst inst_prs
- arg_tys' = substTys subst arg_tys
- unconstrained_ty_args = [ty_arg | (tv,ty_arg) <- inst_prs,
- not (tv `elemVarSet` arg_tvs)]
- ; mapM unBox unconstrained_ty_args -- Zap these to monotypes
- ; tcInstStupidTheta data_con ty_args
- ; traceTc (text "tcConPat" <+> vcat [ppr data_con, ppr ty_args, ppr arg_tys'])
- ; (arg_pats', tvs, res) <- tcConArgs pstate data_con arg_pats arg_tys' thing_inside
- ; return (ConPatOut (L con_span data_con) [] [] emptyLHsBinds
- arg_pats' (mkTyConApp tycon ty_args),
- tvs, res) }
-
- | otherwise -- GADT case
- = do { ty_args <- boxySplitTyConApp tycon pat_ty
- ; span <- getSrcSpanM -- The whole pattern
-
- -- Instantiate the constructor type variables and result type
- ; let (tvs, theta, arg_tys, _, res_tys) = dataConSig data_con
- arg_tvs = exactTyVarsOfTypes arg_tys
- -- See Note [Silly type synonyms in smart-app] in TcExpr
- -- for why we must use exactTyVarsOfTypes
- skol_info = PatSkol data_con span
- arg_flags = [ tv `elemVarSet` arg_tvs | tv <- tvs ]
- ; tvs' <- tcInstSkolTyVars skol_info tvs
- ; let res_tys' = substTys (zipTopTvSubst tvs (mkTyVarTys tvs')) res_tys
-
- -- Do type refinement!
- ; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', ppr res_tys',
- text "ty-args:" <+> ppr ty_args ])
- ; refineAlt pstate data_con tvs' arg_flags res_tys' ty_args
- $ \ pstate' tv_tys' -> do
-
- -- ToDo: arg_tys should be boxy, but I don't think theta' should be,
- -- or the tv_tys' in the call to tcInstStupidTheta
- { let tenv' = zipTopTvSubst tvs tv_tys'
- theta' = substTheta tenv' theta
- arg_tys' = substTys tenv' arg_tys -- Boxy types
-
- ; ((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 pstate' data_con arg_pats arg_tys' thing_inside }
-
- ; dicts <- newDicts (SigOrigin skol_info) theta'
- ; dict_binds <- tcSimplifyCheck doc tvs' dicts lie_req
-
- ; return (ConPatOut (L con_span data_con)
- tvs' (map instToId dicts) dict_binds
- arg_pats' (mkTyConApp tycon ty_args),
- tvs' ++ inner_tvs, res)
+-- Running example:
+-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
+-- with scrutinee of type (T ty)
+
+tcConPat :: PatEnv -> Located Name
+ -> TcRhoType -- Type of the pattern
+ -> HsConPatDetails Name -> TcM a
+ -> TcM (Pat TcId, a)
+tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
+ = do { data_con <- tcLookupDataCon con_name
+ ; let tycon = dataConTyCon data_con
+ -- For data families this is the representation tycon
+ (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _)
+ = dataConFullSig data_con
+
+ -- Instantiate the constructor type variables [a->ty]
+ -- This may involve doing a family-instance coercion,
+ -- and building a wrapper
+ ; (wrap, ctxt_res_tys) <- matchExpectedPatTy (matchExpectedConTy tycon) pat_ty
+
+ -- Add the stupid theta
+ ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
+
+ ; checkExistentials ex_tvs penv
+ ; let skol_info = case pe_ctxt penv of
+ LamPat mc -> PatSkol data_con mc
+ LetPat {} -> UnkSkol -- Doesn't matter
+ ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
+ -- Get location from monad, not from ex_tvs
+
+ ; let pat_ty' = mkTyConApp tycon ctxt_res_tys
+ -- pat_ty' is type of the actual constructor application
+ -- pat_ty' /= pat_ty iff coi /= IdCo
+
+ tenv = zipTopTvSubst (univ_tvs ++ ex_tvs)
+ (ctxt_res_tys ++ mkTyVarTys ex_tvs')
+ arg_tys' = substTys tenv arg_tys
+ full_theta = eq_theta ++ dict_theta
+
+ ; if null ex_tvs && null eq_spec && null full_theta
+ then do { -- The common case; no class bindings etc
+ -- (see Note [Arrows and patterns])
+ (arg_pats', res) <- tcConArgs data_con arg_tys'
+ arg_pats penv thing_inside
+ ; let res_pat = ConPatOut { pat_con = L con_span data_con,
+ pat_tvs = [], pat_dicts = [],
+ pat_binds = emptyTcEvBinds,
+ pat_args = arg_pats',
+ pat_ty = pat_ty' }
+
+ ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
+
+ else do -- The general case, with existential,
+ -- and local equality constraints
+ { let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
+ theta' = substTheta tenv (eq_preds ++ full_theta)
+ -- order is *important* as we generate the list of
+ -- dictionary binders from theta'
+ no_equalities = not (any isEqPred theta')
+
+ ; gadts_on <- xoptM Opt_GADTs
+ ; checkTc (no_equalities || gadts_on)
+ (ptext (sLit "A pattern match on a GADT requires -XGADTs"))
+ -- Trac #2905 decided that a *pattern-match* of a GADT
+ -- should require the GADT language flag
+
+ ; given <- newEvVars theta'
+ ; (ev_binds, (arg_pats', res))
+ <- checkConstraints skol_info ex_tvs' given $
+ tcConArgs data_con arg_tys' arg_pats penv thing_inside
+
+ ; let res_pat = ConPatOut { pat_con = L con_span data_con,
+ pat_tvs = ex_tvs',
+ pat_dicts = given,
+ pat_binds = ev_binds,
+ pat_args = arg_pats',
+ pat_ty = pat_ty' }
+ ; return (mkHsWrapPat wrap res_pat pat_ty, res)
} }
+
+----------------------------
+matchExpectedPatTy :: (TcRhoType -> TcM (CoercionI, a))
+ -> TcRhoType -> TcM (HsWrapper, a)
+-- See Note [Matching polytyped patterns]
+-- Returns a wrapper : pat_ty ~ inner_ty
+matchExpectedPatTy inner_match pat_ty
+ | null tvs && null theta
+ = do { (coi, res) <- inner_match pat_ty
+ ; return (coiToHsWrapper (mkSymCoI coi), res) }
+ -- The Sym is because the inner_match returns a coercion
+ -- that is the other way round to matchExpectedPatTy
+
+ | otherwise
+ = do { (_, tys, subst) <- tcInstTyVars tvs
+ ; wrap1 <- instCall PatOrigin tys (substTheta subst theta)
+ ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (substTy subst tau)
+ ; return (wrap2 <.> wrap1 , arg_tys) }
where
- doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
+ (tvs, theta, tau) = tcSplitSigmaTy pat_ty
+
+----------------------------
+matchExpectedConTy :: TyCon -- The TyCon that this data
+ -- constructor actually returns
+ -> TcRhoType -- The type of the pattern
+ -> TcM (CoercionI, [TcSigmaType])
+-- See Note [Matching constructor patterns]
+-- Returns a coercion : T ty1 ... tyn ~ pat_ty
+-- This is the same way round as matchExpectedListTy etc
+-- but the other way round to matchExpectedPatTy
+matchExpectedConTy data_tc pat_ty
+ | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc
+ -- Comments refer to Note [Matching constructor patterns]
+ -- co_tc :: forall a. T [a] ~ T7 a
+ = do { (_, tys, subst) <- tcInstTyVars (tyConTyVars data_tc)
+ -- tys = [ty1,ty2]
+
+ ; coi1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
+ -- coi1 : T (ty1,ty2) ~ pat_ty
+
+ ; let coi2 = ACo (mkTyConApp co_tc tys)
+ -- coi2 : T (ty1,ty2) ~ T7 ty1 ty2
+
+ ; return (mkTransCoI (mkSymCoI coi2) coi1, tys) }
+
+ | otherwise
+ = matchExpectedTyConApp data_tc pat_ty
+ -- coi : T tys ~ pat_ty
+\end{code}
+
+Noate [
+Note [Matching constructor patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose (coi, tys) = matchExpectedConType data_tc pat_ty
+
+ * In the simple case, pat_ty = tc tys
+
+ * If pat_ty is a polytype, we want to instantiate it
+ This is like part of a subsumption check. Eg
+ f :: (forall a. [a]) -> blah
+ f [] = blah
+
+ * In a type family case, suppose we have
+ data family T a
+ data instance T (p,q) = A p | B q
+ Then we'll have internally generated
+ data T7 p q = A p | B q
+ axiom coT7 p q :: T (p,q) ~ T7 p q
+
+ So if pat_ty = T (ty1,ty2), we return (coi, [ty1,ty2]) such that
+ coi = coi2 . coi1 : T7 t ~ pat_ty
+ coi1 : T (ty1,ty2) ~ pat_ty
+ coi2 : T7 ty1 ty2 ~ T (ty1,ty2)
+
+ For families we do all this matching here, not in the unifier,
+ because we never want a whisper of the data_tycon to appear in
+ error messages; it's a purely internal thing
-tcConArgs :: PatState -> DataCon
- -> HsConDetails Name (LPat Name) -> [TcSigmaType]
- -> (PatState -> TcM a)
- -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a)
+\begin{code}
+tcConArgs :: DataCon -> [TcSigmaType]
+ -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
-tcConArgs pstate data_con (PrefixCon arg_pats) arg_tys thing_inside
+tcConArgs data_con arg_tys (PrefixCon arg_pats) penv 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) <- tc_lpats pstate arg_pats arg_tys thing_inside
- ; return (PrefixCon arg_pats', tvs, res) }
+ ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
+ ; (arg_pats', res) <- tcMultiple tcConArg pats_w_tys
+ penv thing_inside
+ ; return (PrefixCon arg_pats', res) }
where
con_arity = dataConSourceArity data_con
no_of_args = length arg_pats
-tcConArgs pstate data_con (InfixCon p1 p2) arg_tys thing_inside
+tcConArgs data_con arg_tys (InfixCon p1 p2) penv thing_inside
= do { checkTc (con_arity == 2) -- Check correct arity
(arityErr "Constructor" data_con con_arity 2)
- ; ([p1',p2'], tvs, res) <- tc_lpats pstate [p1,p2] arg_tys thing_inside
- ; return (InfixCon p1' p2', tvs, res) }
+ ; let [arg_ty1,arg_ty2] = arg_tys -- This can't fail after the arity check
+ ; ([p1',p2'], res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
+ penv thing_inside
+ ; return (InfixCon p1' p2', res) }
where
con_arity = dataConSourceArity data_con
-tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside
- = do { (rpats', tvs, res) <- tc_fields pstate rpats thing_inside
- ; return (RecCon rpats', tvs, res) }
+tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) penv thing_inside
+ = do { (rpats', res) <- tcMultiple tc_field rpats penv thing_inside
+ ; return (RecCon (HsRecFields rpats' dd), res) }
where
- tc_fields :: PatState -> [(Located Name, LPat Name)]
- -> (PatState -> TcM a)
- -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a)
- tc_fields pstate [] thing_inside
- = do { res <- thing_inside pstate
- ; return ([], [], res) }
-
- tc_fields pstate (rpat : rpats) thing_inside
- = do { (rpat', tvs1, (rpats', tvs2, res))
- <- tc_field pstate rpat $ \ pstate' ->
- tc_fields pstate' rpats thing_inside
- ; return (rpat':rpats', tvs1 ++ tvs2, res) }
-
- tc_field pstate (field_lbl, pat) thing_inside
+ tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
+ tc_field (HsRecField field_lbl pat pun) penv thing_inside
= do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
- ; (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
- ; return ((sel_id, pat'), tvs, res) }
+ ; (pat', res) <- tcConArg (pat, pat_ty) penv thing_inside
+ ; return (HsRecField sel_id pat' pun, res) }
+ find_field_ty :: FieldLabel -> TcM (Id, TcType)
find_field_ty field_lbl
= case [ty | (f,ty) <- field_tys, f == field_lbl] of
-- The normal case, when the field comes from the right constructor
(pat_ty : extras) ->
ASSERT( null extras )
- do { sel_id <- tcLookupId field_lbl
+ do { sel_id <- tcLookupField field_lbl
; return (sel_id, pat_ty) }
+ field_tys :: [(FieldLabel, TcType)]
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}
-
-%************************************************************************
-%* *
- Type refinement
-%* *
-%************************************************************************
-
-\begin{code}
-refineAlt :: PatState
- -> DataCon -- For tracing only
- -> [TcTyVar] -- Type variables from pattern
- -> [Bool] -- Flags indicating which type variables occur
- -- in the type of at least one argument
- -> [TcType] -- Result types from the pattern
- -> [BoxySigmaType] -- Result types from the scrutinee (context)
- -> (PatState -> [BoxySigmaType] -> TcM a)
- -- Possibly-refined existentials
- -> TcM a
-refineAlt pstate con pat_tvs arg_flags pat_res_tys ctxt_res_tys thing_inside
- | not (all isRigidTy ctxt_res_tys)
- -- The context is not a rigid type, so we do no type refinement here.
- = do { let arg_tvs = mkVarSet [ tv | (tv, True) <- pat_tvs `zip` arg_flags]
- subst = boxyMatchTypes arg_tvs pat_res_tys ctxt_res_tys
-
- res_tvs = tcTyVarsOfTypes pat_res_tys
- -- The tvs are (already) all fresh skolems. We need a
- -- fresh skolem for each type variable (to bind in the pattern)
- -- even if it's refined away by the type refinement
- find_inst tv
- | not (tv `elemVarSet` res_tvs) = return (mkTyVarTy tv)
- | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty
- | otherwise = do { tv <- newBoxyTyVar openTypeKind
- ; return (mkTyVarTy tv) }
- ; pat_tys' <- mapM find_inst pat_tvs
-
- -- Do the thing inside
- ; res <- thing_inside pstate pat_tys'
-
- -- Unbox the types that have been filled in by the thing_inside
- -- I.e. the ones whose type variables are mentioned in at least one arg
- ; let strip ty in_arg_tv | in_arg_tv = stripBoxyType ty
- | otherwise = return ty
- ; pat_tys'' <- zipWithM strip pat_tys' arg_flags
- ; let subst = zipOpenTvSubst pat_tvs pat_tys''
- ; boxyUnifyList (substTys subst pat_res_tys) ctxt_res_tys
-
- ; return res } -- All boxes now filled
-
- | otherwise -- The context is rigid, so we can do type refinement
- = case gadtRefineTys (pat_reft pstate) con pat_tvs pat_res_tys ctxt_res_tys of
- Failed msg -> failWithTc (inaccessibleAlt msg)
- Succeeded (new_subst, all_bound_here)
- | all_bound_here -- All the new bindings are for pat_tvs, so no need
- -- to refine the environment or pstate
- -> do { traceTc trace_msg
- ; thing_inside pstate pat_tvs' }
- | otherwise -- New bindings affect the context, so pass down pstate'.
- -- DO NOT refine the envt, because we might be inside a
- -- lazy pattern
- -> do { traceTc trace_msg
- ; thing_inside pstate' pat_tvs' }
- where
- pat_tvs' = map (substTyVar new_subst) pat_tvs
- pstate' = pstate { pat_reft = new_subst }
- trace_msg = text "refineTypes:match" <+> ppr con <+> ppr new_subst
-
-refineType :: GadtRefinement -> BoxyRhoType -> BoxyRhoType
--- Refine the type if it is rigid
-refineType reft ty
- | isRefineableTy ty = substTy reft ty
- | otherwise = ty
+tcConArg :: Checker (LPat Name, TcSigmaType) (LPat Id)
+tcConArg (arg_pat, arg_ty) penv thing_inside
+ = tc_lpat arg_pat arg_ty penv thing_inside
\end{code}
-
-%************************************************************************
-%* *
- 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@(HsIntegral i fi) res_ty
- | not (fi `isHsVar` fromIntegerName) -- Do not generate a LitInst for rebindable syntax.
- -- Reason: If we do, tcSimplify will call lookupInst, which
- -- will call tcSyntaxName, which does unification,
- -- which tcSimplify doesn't like
- -- ToDo: noLoc sadness
- = do { integer_ty <- tcMetaTy integerTyConName
- ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
- ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) }
-
- | Just expr <- shortCutIntLit i res_ty
- = return (HsIntegral i expr)
-
- | otherwise
- = do { expr <- newLitInst orig lit res_ty
- ; return (HsIntegral i expr) }
-
-tcOverloadedLit orig lit@(HsFractional r fr) res_ty
- | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case
- = do { rat_ty <- tcMetaTy rationalTyConName
- ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
- -- Overloaded literals must have liftedTypeKind, because
- -- we're instantiating an overloaded function here,
- -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
- -- However this'll be picked up by tcSyntaxOp if necessary
- ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty)))) }
-
- | Just expr <- shortCutFracLit r res_ty
- = return (HsFractional r expr)
-
- | otherwise
- = do { expr <- newLitInst orig lit res_ty
- ; return (HsFractional r 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
- ; extendLIE lit_inst
- ; return (HsVar (instToId lit_inst)) }
+addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
+-- Instantiate the "stupid theta" of the data con, and throw
+-- the constraints into the constraint set
+addDataConStupidTheta data_con inst_tys
+ | null stupid_theta = return ()
+ | otherwise = instStupidTheta origin inst_theta
+ where
+ origin = OccurrenceOf (dataConName data_con)
+ -- The origin should always report "occurrence of C"
+ -- even when C occurs in a pattern
+ stupid_theta = dataConStupidTheta data_con
+ tenv = mkTopTvSubst (dataConUnivTyVars data_con `zip` inst_tys)
+ -- NB: inst_tys can be longer than the univ tyvars
+ -- because the constructor might have existentials
+ 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 short-cut 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.
%************************************************************************
%* *
%* *
%************************************************************************
-\begin{code}
-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("In the pattern:"))
- 4 (ppr pat))
-
------------------------------------------------
+{- This was used to improve the error message from
+ an existential escape. Need to think how to do this.
-existentialExplode pats
- = hang (vcat [text "My brain just exploded.",
- text "I can't handle pattern bindings for existentially-quantified constructors.",
- text "In the binding group for"])
- 4 (vcat (map ppr pats))
-
-sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env
+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
+ sep [ptext (sLit "When checking an existential match that binds"),
+ nest 2 (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` 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
+-}
+
+\begin{code}
+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 "In the pattern:"))
+ 2 (ppr pat))
+
+-----------------------------------------------
+checkExistentials :: [TyVar] -> PatEnv -> TcM ()
+ -- See Note [Arrows and patterns]
+checkExistentials [] _ = return ()
+checkExistentials _ (PE { pe_ctxt = LetPat {}}) = failWithTc existentialLetPat
+checkExistentials _ (PE { pe_ctxt = LamPat ProcExpr }) = failWithTc existentialProcPat
+checkExistentials _ (PE { pe_lazy = True }) = failWithTc existentialLazyPat
+checkExistentials _ _ = return ()
+
+existentialLazyPat :: SDoc
+existentialLazyPat
+ = hang (ptext (sLit "An existential or GADT data constructor cannot be used"))
+ 2 (ptext (sLit "inside a lazy (~) pattern"))
+
+existentialProcPat :: SDoc
+existentialProcPat
+ = ptext (sLit "Proc patterns cannot use existential or GADT data constructors")
+
+existentialLetPat :: SDoc
+existentialLetPat
+ = 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."]
badFieldCon :: DataCon -> Name -> SDoc
badFieldCon con field
- = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
- ptext SLIT("does not have field"), quotes (ppr 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:"))
- 4 (ppr sig_ty)
+ = hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
+ 2 (ppr sig_ty)
-badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
+badTypePat :: Pat Name -> SDoc
+badTypePat pat = ptext (sLit "Illegal type pattern") <+> ppr pat
-lazyPatErr pat tvs
+lazyUnliftedPatErr :: OutputableBndr name => Pat name -> TcM ()
+lazyUnliftedPatErr pat
= failWithTc $
- hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
- 2 (vcat (map pprSkolTvBinding tvs))
+ hang (ptext (sLit "A lazy (~) pattern cannot contain unlifted types:"))
+ 2 (ppr pat)
-inaccessibleAlt msg
- = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
+unboxedTupleErr :: SDoc -> Type -> SDoc
+unboxedTupleErr what ty
+ = hang (what <+> ptext (sLit "cannot have an unboxed tuple type:"))
+ 2 (ppr ty)
\end{code}
projects / ghc-hetmet.git / blobdiff