%
+% (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, tcLamPat, tcLamPats, tcOverloadedLit,
+ 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 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,
- 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 CoreFVs
+import Name
+import TcSimplify
+import TcEnv
+import TcMType
+import TcType
+import VarSet
+import TcUnify
+import TcHsType
+import TysWiredIn
+import TcGadt
+import Type
+import StaticFlags
+import TyCon
+import DataCon
+import DynFlags
+import PrelNames
+import BasicTypes hiding (SuccessFlag(..))
+import SrcLoc
+import ErrUtils
+import Util
+import Maybes
import Outputable
import FastString
\end{code}
%************************************************************************
\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 :: (Name -> Maybe TcRhoType)
+ -> LPat Name -> BoxySigmaType
+ -> TcM a
+ -> TcM (LPat TcId, a)
+tcLetPat sig_fn pat pat_ty thing_inside
+ = do { let init_state = PS { pat_ctxt = LetPat sig_fn,
+ pat_reft = emptyRefinement }
+ ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)
+
+ -- Don't know how to deal with pattern-bound existentials yet
+ ; checkTc (null ex_tvs) (existentialExplode pat)
+
+ ; return (pat', res) }
+
+-----------------
+tcLamPats :: [LPat Name] -- Patterns,
+ -> [BoxySigmaType] -- and their types
+ -> BoxyRhoType -- Result type,
+ -> ((Refinement, BoxyRhoType) -> 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
+-- 3. Apply the refinement to the environment and result type
-- 4. Check the body
-- 5. Check that no existentials escape
-tcPats ctxt pats tys res_ty thing_inside
- = do { let init_state = PS { pat_ctxt = ctxt, pat_reft = emptyTvSubst }
+tcLamPats pats tys res_ty thing_inside
+ = tc_lam_pats (zipEqual "tcLamPats" pats tys)
+ (emptyRefinement, res_ty) thing_inside
+
+tcLamPat :: LPat Name -> BoxySigmaType
+ -> (Refinement,BoxyRhoType) -- Result type
+ -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
+ -> TcM (LPat TcId, a)
+tcLamPat pat pat_ty res_ty thing_inside
+ = do { ([pat'],thing) <- tc_lam_pats [(pat, pat_ty)] res_ty thing_inside
+ ; return (pat', thing) }
- ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' ->
+-----------------
+tc_lam_pats :: [(LPat Name,BoxySigmaType)]
+ -> (Refinement,BoxyRhoType) -- Result type
+ -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
+ -> TcM ([LPat TcId], a)
+tc_lam_pats pat_ty_prs (reft, res_ty) thing_inside
+ = do { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft }
+
+ ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
refineEnvironment (pat_reft pstate') $
- thing_inside (refineType (pat_reft pstate') res_ty)
+ thing_inside (pat_reft pstate', res_ty)
- ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty
+ ; let tys = map snd pat_ty_prs
+ ; tcCheckExistentialPat pats' ex_tvs tys res_ty
; returnM (pats', res) }
-----------------
-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) }
-
-
------------------
-tcCheckExistentialPat :: PatCtxt
- -> [LPat TcId] -- Patterns (just for error message)
+tcCheckExistentialPat :: [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
-- 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
+tcCheckExistentialPat 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) $
+tcCheckExistentialPat pats ex_tvs pat_tys body_ty
+ = addErrCtxtM (sigPatCtxt pats ex_tvs pat_tys body_ty) $
checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
data PatState = PS {
pat_ctxt :: PatCtxt,
- pat_reft :: GadtRefinement -- Binds rigid TcTyVars to their refinements
+ pat_reft :: Refinement -- Binds rigid TcTyVars to their refinements
}
data PatCtxt
\begin{code}
tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
- = do { pat_ty' <- unBox pat_ty
+ = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
-- We have an undecorated binder, so we do rule ABS1,
-- by unboxing the boxy type, forcing any un-filled-in
-- boxes to become monotypes
-- f t = case t of { MkT g -> ... }
-- Here, the 'g' must get type (forall a. a->a) from the
-- MkT context
- ; return (mkLocalId bndr_name pat_ty') }
+ ; return (Id.mkLocalId bndr_name pat_ty') }
tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
| Just mono_ty <- lookup_sig bndr_name
= do { mono_name <- newLocalName bndr_name
; boxyUnify mono_ty pat_ty
- ; return (mkLocalId mono_name mono_ty) }
+ ; return (Id.mkLocalId mono_name mono_ty) }
| otherwise
- = do { pat_ty' <- unBox pat_ty
+ = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
; mono_name <- newLocalName bndr_name
- ; return (mkLocalId mono_name pat_ty') }
+ ; return (Id.mkLocalId mono_name pat_ty') }
-------------------
= do { (res, lie) <- getLIE thing_inside
; binds <- bindInstsOfLocalFuns lie [id]
; return (res, binds) }
+
+-------------------
+unBoxPatBndrType ty name = unBoxArgType ty (ptext SLIT("The variable") <+> quotes (ppr name))
+unBoxWildCardType ty = unBoxArgType ty (ptext SLIT("A wild-card pattern"))
+
+unBoxArgType :: BoxyType -> SDoc -> TcM TcType
+-- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind;
+-- that is, it can't be an unboxed tuple. For example,
+-- case (f x) of r -> ...
+-- should fail if 'f' returns an unboxed tuple.
+unBoxArgType ty pp_this
+ = do { ty' <- unBox ty -- Returns a zonked type
+
+ -- Neither conditional is strictly necesssary (the unify alone will do)
+ -- but they improve error messages, and allocate fewer tyvars
+ ; if isUnboxedTupleType ty' then
+ failWithTc msg
+ else if isSubArgTypeKind (typeKind ty') then
+ return ty'
+ else do -- OpenTypeKind, so constrain it
+ { ty2 <- newFlexiTyVarTy argTypeKind
+ ; unifyType ty' ty2
+ ; return ty' }}
+ where
+ msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple")
\end{code}
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.
\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
+ -> PatState
+ -> (PatState -> TcM r)
+ -> TcM (out, [TcTyVar], r)
+
+tcMultiple :: Checker inp out -> Checker [inp] [out]
+tcMultiple tc_pat args pstate thing_inside
= do { err_ctxt <- getErrCtxt
- ; let loop pstate [] []
+ ; let loop pstate []
= do { res <- thing_inside pstate
; return ([], [], res) }
- loop pstate (p:ps) (ty:tys)
+ loop pstate (arg:args)
= do { (p', p_tvs, (ps', ps_tvs, res))
- <- tc_lpat pstate p ty $ \ pstate' ->
+ <- tc_pat arg pstate $ \ pstate' ->
setErrCtxt err_ctxt $
- loop pstate' ps tys
+ loop pstate' args
-- setErrCtxt: restore context before doing the next pattern
-- See note [Nesting] above
; return (p':ps', p_tvs ++ ps_tvs, res) }
- loop _ _ _ = pprPanic "tc_lpats" (ppr pats $$ ppr pat_tys)
-
- ; loop pstate pats pat_tys }
+ ; loop pstate 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_pr :: (LPat Name, BoxySigmaType)
+ -> PatState
+ -> (PatState -> TcM a)
+ -> TcM (LPat TcId, [TcTyVar], a)
+tc_lpat_pr (pat, ty) = tc_lpat pat ty
+
+tc_lpat :: LPat Name
+ -> BoxySigmaType
+ -> PatState
+ -> (PatState -> TcM a)
+ -> TcM (LPat TcId, [TcTyVar], a)
+tc_lpat (L span pat) pat_ty pstate thing_inside
= setSrcSpan span $
maybeAddErrCtxt (patCtxt pat) $
- do { let pat_ty' = refineType (pat_reft pstate) pat_ty
+ do { let mb_reft = refineType (pat_reft pstate) pat_ty
+ pat_ty' = case mb_reft of { Just (_, ty') -> ty'; Nothing -> pat_ty }
+
-- Make sure the result type reflects the current refinement
- ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
- ; return (L span pat', tvs, res) }
+ -- We must do this here, so that it correctly ``sees'' all
+ -- the refinements to the left. Example:
+ -- Suppose C :: forall a. T a -> a -> Foo
+ -- Pattern C a p1 True
+ -- So p1 might refine 'a' to True, and the True
+ -- pattern had better see it.
+ ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
+ ; let final_pat = case mb_reft of
+ Nothing -> pat'
+ Just (co,_) -> CoPat (WpCo co) pat' pat_ty
+ ; return (L span final_pat, tvs, res) }
--------------------
tc_pat :: PatState
; return (pat', [], res) }
tc_pat pstate (ParPat pat) pat_ty thing_inside
- = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+ = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
; return (ParPat pat', tvs, res) }
tc_pat pstate (BangPat pat) pat_ty thing_inside
- = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+ = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
; return (BangPat pat', tvs, res) }
-- There's a wrinkle with irrefutable patterns, namely that we
--
-- Nor should a lazy pattern bind any existential type variables
-- because they won't be in scope when we do the desugaring
+--
+-- Note [Hopping the LIE in lazy patterns]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- In a lazy pattern, we must *not* discharge constraints from the RHS
+-- from dictionaries bound in the pattern. E.g.
+-- f ~(C x) = 3
+-- We can't discharge the Num constraint from dictionaries bound by
+-- the pattern C!
+--
+-- So we have to make the constraints from thing_inside "hop around"
+-- the pattern. Hence the getLLE and extendLIEs later.
+
tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
- = do { (pat', pat_tvs, res) <- tc_lpat pstate pat pat_ty $ \ _ ->
- thing_inside pstate
- -- Ignore refined pstate',
- -- revert to pstate
+ = do { (pat', pat_tvs, (res,lie))
+ <- tc_lpat pat pat_ty pstate $ \ _ ->
+ getLIE (thing_inside pstate)
+ -- Ignore refined pstate', revert to pstate
+ ; extendLIEs lie
+ -- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns]
+
-- Check no existentials
; if (null pat_tvs) then return ()
else lazyPatErr lpat pat_tvs
; 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
+ = do { pat_ty' <- unBoxWildCardType 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
+ tc_lpat pat (idType bndr_id) pstate 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
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
+ tc_lpat pat inner_ty pstate thing_inside
; return (SigPatOut pat' inner_ty, tvs, res) }
tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
-- 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
+ ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
+ pats pstate 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
+ ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
+ pats pstate 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
+ ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
+ pstate thing_inside
-- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
-- so that we can experiment with lazy tuple-matching.
-- 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" -- ConPatOut, SigPatOut, VarPatOut
\end{code}
%* *
%************************************************************************
+[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 existing 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.
+
+In fact, if we have a data instance declaration defining a GADT, eq_spec will
+be non-empty and we will get a mixture of global instantiations and local
+refinement from a single match. This neatly reflects that, as soon as we
+have constrained the type of the scrutinee to the required type index, all
+further type refinement is local to the alternative.
+
\begin{code}
+-- Running example:
+-- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
+-- with scrutinee of type (T ty)
+
tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
-> BoxySigmaType -- Type of the pattern
- -> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
+ -> HsConPatDetails Name -> (PatState -> TcM a)
-> TcM (Pat TcId, [TcTyVar], a)
tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
- | 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
+ = do { let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _) = dataConFullSig data_con
+ skol_info = PatSkol data_con
+ origin = SigOrigin skol_info
+
+ -- Instantiate the constructor type variables [a->ty]
+ ; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty
+ ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs -- Get location from monad,
+ -- not from ex_tvs
+ ; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs)
+ (ctxt_res_tys ++ mkTyVarTys ex_tvs')
+ eq_spec' = substEqSpec tenv eq_spec
+ theta' = substTheta tenv theta
+ arg_tys' = substTys tenv arg_tys
+
+ ; co_vars <- newCoVars eq_spec' -- Make coercion variables
+ ; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty
; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
- 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)
- } }
+ tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
+
+ ; loc <- getInstLoc origin
+ ; dicts <- newDictBndrs loc theta'
+ ; dict_binds <- tcSimplifyCheckPat loc co_vars (pat_reft pstate')
+ ex_tvs' dicts lie_req
+
+ ; addDataConStupidTheta data_con ctxt_res_tys
+
+ ; return
+ (unwrapFamInstScrutinee tycon ctxt_res_tys $
+ ConPatOut { pat_con = L con_span data_con,
+ pat_tvs = ex_tvs' ++ co_vars,
+ pat_dicts = map instToId dicts,
+ pat_binds = dict_binds,
+ pat_args = arg_pats', pat_ty = pat_ty },
+ ex_tvs' ++ inner_tvs, res)
+ }
where
- doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
-
-tcConArgs :: PatState -> DataCon
- -> HsConDetails Name (LPat Name) -> [TcSigmaType]
- -> (PatState -> TcM a)
- -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a)
-
-tcConArgs pstate data_con (PrefixCon arg_pats) arg_tys thing_inside
+ -- Split against the family tycon if the pattern constructor
+ -- belongs to a family instance tycon.
+ boxySplitTyConAppWithFamily tycon pat_ty =
+ traceTc traceMsg >>
+ case tyConFamInst_maybe tycon of
+ Nothing -> boxySplitTyConApp tycon pat_ty
+ Just (fam_tycon, instTys) ->
+ do { scrutinee_arg_tys <- boxySplitTyConApp fam_tycon pat_ty
+ ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
+ ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
+ ; return freshTvs
+ }
+ where
+ traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
+ ppr tycon <+> ppr pat_ty
+ , text " family instance:" <+>
+ ppr (tyConFamInst_maybe tycon)
+ ]
+
+ -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
+ -- pattern if the tycon is an instance of a family.
+ --
+ unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id
+ unwrapFamInstScrutinee tycon args pat
+ | Just co_con <- tyConFamilyCoercion_maybe tycon
+-- , not (isNewTyCon tycon) -- newtypes are explicitly unwrapped by
+ -- the desugarer
+ -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
+ -- coercion is not the identity; mkCoPat is inconvenient as it
+ -- wants a located pattern.
+ = CoPat (WpCo $ mkTyConApp co_con args) -- co fam ty to repr ty
+ (pat {pat_ty = mkTyConApp tycon args}) -- representation type
+ pat_ty -- family inst type
+ | otherwise
+ = pat
+
+
+tcConArgs :: DataCon -> [TcSigmaType]
+ -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
+
+tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
= do { checkTc (con_arity == no_of_args) -- 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
+ ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
+ ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
+ pstate thing_inside
; return (PrefixCon arg_pats', tvs, res) }
where
con_arity = dataConSourceArity data_con
no_of_args = length arg_pats
-tcConArgs pstate data_con (InfixCon p1 p2) arg_tys thing_inside
+tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate 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
+ ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
+ pstate thing_inside
; return (InfixCon p1' p2', tvs, res) }
where
con_arity = dataConSourceArity data_con
-tcConArgs 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 other_args (InfixCon p1 p2) pstate thing_inside
+ = pprPanic "tcConArgs" (ppr data_con) -- InfixCon always has two arguments
+
+tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
+ = do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
+ ; return (RecCon (HsRecFields rpats' dd), tvs, res) }
where
- tc_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) pstate 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', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
+ ; return (HsRecField sel_id pat' pun, tvs, res) }
+ find_field_ty :: FieldLabel -> TcM (Id, TcType)
find_field_ty field_lbl
= case [ty | (f,ty) <- field_tys, f == field_lbl] of
-- 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).
+
+tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
+tcConArg (arg_pat, arg_ty) pstate thing_inside
+ = tc_lpat arg_pat arg_ty pstate thing_inside
+ -- NB: the tc_lpat will refine pat_ty if necessary
+ -- based on the current pstate, which may include
+ -- refinements from peer argument patterns to the left
+\end{code}
+
+\begin{code}
+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 = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
+ inst_theta = substTheta tenv stupid_theta
\end{code}
%************************************************************************
\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
+refineAlt :: DataCon -- For tracing only
+ -> PatState
+ -> [TcTyVar] -- Existentials
+ -> [CoVar] -- Equational constraints
+ -> BoxySigmaType -- Pattern type
+ -> TcM PatState
+
+refineAlt con pstate ex_tvs [] pat_ty
+ = return pstate -- Common case: no equational constraints
+
+refineAlt con pstate ex_tvs co_vars pat_ty
+ = do { opt_gadt <- doptM Opt_GADTs -- No type-refinement unless GADTs are on
+ ; if (not opt_gadt) then return pstate
+ else do
+
+ { checkTc (isRigidTy pat_ty) (nonRigidMatch con)
+ -- We are matching against a GADT constructor with non-trivial
+ -- constraints, but pattern type is wobbly. For now we fail.
+ -- We can make sense of this, however:
+ -- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a
+ -- (\x -> case x of { MkT v -> v })
+ -- We can infer that x must have type T [c], for some wobbly 'c'
+ -- and translate to
+ -- (\(x::T [c]) -> case x of
+ -- MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g
+ -- To implement this, we'd first instantiate the equational
+ -- constraints with *wobbly* type variables for the existentials;
+ -- then unify these constraints to make pat_ty the right shape;
+ -- then proceed exactly as in the rigid case
+
+ -- In the rigid case, we perform type refinement
+ ; case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
+ Failed msg -> failWithTc (inaccessibleAlt msg) ;
+ Succeeded reft -> do { traceTc trace_msg
+ ; return (pstate { pat_reft = reft }) }
+ -- DO NOT refine the envt right away, because we
+ -- might be inside a lazy pattern. Instead, refine pstate
+ where
+
+ trace_msg = text "refineAlt:match" <+>
+ vcat [ ppr con <+> ppr ex_tvs,
+ ppr [(v, tyVarKind v) | v <- co_vars],
+ ppr reft]
+ } } }
\end{code}
= do { expr <- newLitInst orig lit res_ty
; return (HsFractional r expr) }
+tcOverloadedLit orig lit@(HsIsString s fr) res_ty
+ | not (fr `isHsVar` fromStringName) -- c.f. HsIntegral case
+ = do { str_ty <- tcMetaTy stringTyConName
+ ; fr' <- tcSyntaxOp orig fr (mkFunTy str_ty res_ty)
+ ; return (HsIsString s (HsApp (noLoc fr') (nlHsLit (HsString s)))) }
+
+ | Just expr <- shortCutStringLit s res_ty
+ = return (HsIsString s expr)
+
+ | otherwise
+ = do { expr <- newLitInst orig lit res_ty
+ ; return (HsIsString s expr) }
+
newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
newLitInst orig lit res_ty -- Make a LitInst
= do { loc <- getInstLoc orig
; res_tau <- zapToMonotype res_ty
; new_uniq <- newUnique
; let lit_nm = mkSystemVarName new_uniq FSLIT("lit")
- lit_inst = LitInst lit_nm lit res_tau loc
+ lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit,
+ tci_ty = res_tau, tci_loc = loc}
; extendLIE lit_inst
; return (HsVar (instToId lit_inst)) }
\end{code}
-----------------------------------------------
-existentialExplode pats
+existentialExplode pat
= hang (vcat [text "My brain just exploded.",
text "I can't handle pattern bindings for existentially-quantified constructors.",
+ text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
text "In the binding group for"])
- 4 (vcat (map ppr pats))
-
-sigPatCtxt bound_ids bound_tvs tys tidy_env
- = -- tys is (body_ty : pat_tys)
- mapM zonkTcType tys `thenM` \ tys' ->
- let
- (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
- (_env2, tidy_body_ty : tidy_pat_tys) = tidyOpenTypes env1 tys'
- in
- returnM (env1,
+ 4 (ppr pat)
+
+sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env
+ = do { pat_tys' <- mapM zonkTcType pat_tys
+ ; body_ty' <- zonkTcType body_ty
+ ; let (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
+ (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
+ (env3, tidy_body_ty) = tidyOpenType env2 body_ty'
+ ; return (env3,
sep [ptext SLIT("When checking an existential match that binds"),
nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
ptext SLIT("The body has type:") <+> ppr tidy_body_ty
- ])
+ ]) }
where
+ bound_ids = collectPatsBinders pats
show_ids = filter is_interesting bound_ids
- is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
+ is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
ppr_id id ty = ppr id <+> dcolon <+> ppr ty
-- Don't zonk the types so we get the separate, un-unified versions
lazyPatErr pat tvs
= failWithTc $
- hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
+ hang (ptext SLIT("A lazy (~) pattern cannot bind existential type variables"))
2 (vcat (map pprSkolTvBinding tvs))
+nonRigidMatch con
+ = hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
+ 2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
+
inaccessibleAlt msg
= hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
\end{code}