2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcPat]{Typechecking patterns}
7 module TcPat ( tcPat, tcPats, tcOverloadedLit,
8 PatCtxt(..), badFieldCon, polyPatSig ) where
10 #include "HsVersions.h"
12 import {-# SOURCE #-} TcExpr( tcSyntaxOp )
13 import HsSyn ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..),
14 LHsBinds, emptyLHsBinds, isEmptyLHsBinds,
15 collectPatsBinders, nlHsLit )
16 import TcHsSyn ( TcId, hsLitType )
18 import Inst ( InstOrigin(..), shortCutFracLit, shortCutIntLit,
19 newDicts, instToId, tcInstStupidTheta, isHsVar
21 import Id ( Id, idType, mkLocalId )
22 import CoreFVs ( idFreeTyVars )
23 import Name ( Name, mkSystemVarName )
24 import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
25 import TcEnv ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
26 tcLookupClass, tcLookupDataCon, tcLookupId, refineEnvironment,
28 import TcMType ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, newBoxyTyVar, zonkTcType )
29 import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType, BoxyType,
31 BoxySigmaType, BoxyRhoType, argTypeKind, typeKind,
32 pprSkolTvBinding, isRefineableTy, isRigidTy, tcTyVarsOfTypes, mkTyVarTy, lookupTyVar,
33 emptyTvSubst, substTyVar, substTy, mkTopTvSubst, zipTopTvSubst, zipOpenTvSubst,
34 mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy, isArgTypeKind, isUnboxedTupleType,
35 mkFunTy, mkFunTys, exactTyVarsOfTypes, tidyOpenType, tidyOpenTypes )
36 import VarSet ( elemVarSet, mkVarSet )
37 import Kind ( liftedTypeKind, openTypeKind )
38 import TcUnify ( boxySplitTyConApp, boxySplitListTy, unifyType,
39 unBox, stripBoxyType, zapToMonotype,
40 boxyMatchTypes, boxyUnify, boxyUnifyList, checkSigTyVarsWrt )
41 import TcHsType ( UserTypeCtxt(..), tcPatSig )
42 import TysWiredIn ( boolTy, parrTyCon, tupleTyCon )
43 import Unify ( MaybeErr(..), gadtRefineTys )
44 import Type ( substTys, substTheta )
45 import StaticFlags ( opt_IrrefutableTuples )
46 import TyCon ( TyCon )
47 import DataCon ( DataCon, dataConTyCon, isVanillaDataCon,
48 dataConFieldLabels, dataConSourceArity, dataConSig )
49 import PrelNames ( integralClassName, fromIntegerName, integerTyConName,
50 fromRationalName, rationalTyConName )
51 import BasicTypes ( isBoxed )
52 import SrcLoc ( Located(..), SrcSpan, noLoc )
53 import ErrUtils ( Message )
54 import Util ( takeList, zipEqual )
60 %************************************************************************
64 %************************************************************************
68 -> [LPat Name] -- Patterns,
69 -> [BoxySigmaType] -- and their types
70 -> BoxyRhoType -- Result type,
71 -> (BoxyRhoType -> TcM a) -- and the checker for the body
72 -> TcM ([LPat TcId], a)
74 -- This is the externally-callable wrapper function
75 -- Typecheck the patterns, extend the environment to bind the variables,
76 -- do the thing inside, use any existentially-bound dictionaries to
77 -- discharge parts of the returning LIE, and deal with pattern type
80 -- 1. Initialise the PatState
81 -- 2. Check the patterns
82 -- 3. Apply the refinement
84 -- 5. Check that no existentials escape
86 tcPats ctxt pats tys res_ty thing_inside
87 = do { let init_state = PS { pat_ctxt = ctxt, pat_reft = emptyTvSubst }
89 ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' ->
90 refineEnvironment (pat_reft pstate') $
91 thing_inside (refineType (pat_reft pstate') res_ty)
93 ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty
95 ; returnM (pats', res) }
100 -> LPat Name -> BoxySigmaType
101 -> BoxyRhoType -- Result type
102 -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
103 -> TcM (LPat TcId, a)
104 tcPat ctxt pat pat_ty res_ty thing_inside
105 = do { ([pat'],thing) <- tcPats ctxt [pat] [pat_ty] res_ty thing_inside
106 ; return (pat', thing) }
110 tcCheckExistentialPat :: PatCtxt
111 -> [LPat TcId] -- Patterns (just for error message)
112 -> [TcTyVar] -- Existentially quantified tyvars bound by pattern
113 -> [BoxySigmaType] -- Types of the patterns
114 -> BoxyRhoType -- Type of the body of the match
115 -- Tyvars in either of these must not escape
117 -- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat
118 -- For example, we must reject this program:
119 -- data C = forall a. C (a -> Int)
121 -- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
123 tcCheckExistentialPat ctxt pats [] pat_tys body_ty
124 = return () -- Short cut for case when there are no existentials
126 tcCheckExistentialPat (LetPat _) pats ex_tvs pat_tys body_ty
127 -- Don't know how to deal with pattern-bound existentials yet
128 = failWithTc (existentialExplode pats)
130 tcCheckExistentialPat ctxt pats ex_tvs pat_tys body_ty
131 = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys body_ty) $
132 checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
136 pat_reft :: GadtRefinement -- Binds rigid TcTyVars to their refinements
141 | LetPat (Name -> Maybe TcRhoType) -- Used for let(rec) bindings
143 patSigCtxt :: PatState -> UserTypeCtxt
144 patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
145 patSigCtxt other = LamPatSigCtxt
150 %************************************************************************
154 %************************************************************************
157 tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
158 tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
159 = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
160 -- We have an undecorated binder, so we do rule ABS1,
161 -- by unboxing the boxy type, forcing any un-filled-in
162 -- boxes to become monotypes
163 -- NB that pat_ty' can still be a polytype:
164 -- data T = MkT (forall a. a->a)
165 -- f t = case t of { MkT g -> ... }
166 -- Here, the 'g' must get type (forall a. a->a) from the
168 ; return (mkLocalId bndr_name pat_ty') }
170 tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
171 | Just mono_ty <- lookup_sig bndr_name
172 = do { mono_name <- newLocalName bndr_name
173 ; boxyUnify mono_ty pat_ty
174 ; return (mkLocalId mono_name mono_ty) }
177 = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
178 ; mono_name <- newLocalName bndr_name
179 ; return (mkLocalId mono_name pat_ty') }
183 bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
184 bindInstsOfPatId id thing_inside
185 | not (isOverloadedTy (idType id))
186 = do { res <- thing_inside; return (res, emptyLHsBinds) }
188 = do { (res, lie) <- getLIE thing_inside
189 ; binds <- bindInstsOfLocalFuns lie [id]
190 ; return (res, binds) }
193 unBoxPatBndrType ty name = unBoxArgType ty (ptext SLIT("The variable") <+> quotes (ppr name))
194 unBoxWildCardType ty = unBoxArgType ty (ptext SLIT("A wild-card pattern"))
196 unBoxArgType :: BoxyType -> SDoc -> TcM TcType
197 -- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind;
198 -- that is, it can't be an unboxed tuple. For example,
199 -- case (f x) of r -> ...
200 -- should fail if 'f' returns an unboxed tuple.
201 unBoxArgType ty pp_this
202 = do { ty' <- unBox ty -- Returns a zonked type
204 -- Neither conditional is strictly necesssary (the unify alone will do)
205 -- but they improve error messages, and allocate fewer tyvars
206 ; if isUnboxedTupleType ty' then
208 else if isArgTypeKind (typeKind ty') then
210 else do -- OpenTypeKind, so constrain it
211 { ty2 <- newFlexiTyVarTy argTypeKind
215 msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple")
219 %************************************************************************
221 The main worker functions
223 %************************************************************************
227 tcPat takes a "thing inside" over which the patter scopes. This is partly
228 so that tcPat can extend the environment for the thing_inside, but also
229 so that constraints arising in the thing_inside can be discharged by the
232 This does not work so well for the ErrCtxt carried by the monad: we don't
233 want the error-context for the pattern to scope over the RHS.
234 Hence the getErrCtxt/setErrCtxt stuff in tc_lpats.
241 -> (PatState -> TcM a)
242 -> TcM ([LPat TcId], [TcTyVar], a)
244 tc_lpats pstate pats pat_tys thing_inside
245 = do { err_ctxt <- getErrCtxt
246 ; let loop pstate [] []
247 = do { res <- thing_inside pstate
248 ; return ([], [], res) }
250 loop pstate (p:ps) (ty:tys)
251 = do { (p', p_tvs, (ps', ps_tvs, res))
252 <- tc_lpat pstate p ty $ \ pstate' ->
253 setErrCtxt err_ctxt $
255 -- setErrCtxt: restore context before doing the next pattern
256 -- See note [Nesting] above
258 ; return (p':ps', p_tvs ++ ps_tvs, res) }
260 loop _ _ _ = pprPanic "tc_lpats" (ppr pats $$ ppr pat_tys)
262 ; loop pstate pats pat_tys }
268 -> (PatState -> TcM a)
269 -> TcM (LPat TcId, [TcTyVar], a)
270 tc_lpat pstate (L span pat) pat_ty thing_inside
272 maybeAddErrCtxt (patCtxt pat) $
273 do { let pat_ty' = refineType (pat_reft pstate) pat_ty
274 -- Make sure the result type reflects the current refinement
275 ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
276 ; return (L span pat', tvs, res) }
281 -> Pat Name -> BoxySigmaType -- Fully refined result type
282 -> (PatState -> TcM a) -- Thing inside
283 -> TcM (Pat TcId, -- Translated pattern
284 [TcTyVar], -- Existential binders
285 a) -- Result of thing inside
287 tc_pat pstate (VarPat name) pat_ty thing_inside
288 = do { id <- tcPatBndr pstate name pat_ty
289 ; (res, binds) <- bindInstsOfPatId id $
290 tcExtendIdEnv1 name id $
291 (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
292 >> thing_inside pstate)
293 ; let pat' | isEmptyLHsBinds binds = VarPat id
294 | otherwise = VarPatOut id binds
295 ; return (pat', [], res) }
297 tc_pat pstate (ParPat pat) pat_ty thing_inside
298 = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
299 ; return (ParPat pat', tvs, res) }
301 tc_pat pstate (BangPat pat) pat_ty thing_inside
302 = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
303 ; return (BangPat pat', tvs, res) }
305 -- There's a wrinkle with irrefutable patterns, namely that we
306 -- must not propagate type refinement from them. For example
307 -- data T a where { T1 :: Int -> T Int; ... }
308 -- f :: T a -> Int -> a
310 -- It's obviously not sound to refine a to Int in the right
311 -- hand side, because the arugment might not match T1 at all!
313 -- Nor should a lazy pattern bind any existential type variables
314 -- because they won't be in scope when we do the desugaring
315 tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
316 = do { (pat', pat_tvs, res) <- tc_lpat pstate pat pat_ty $ \ _ ->
318 -- Ignore refined pstate',
320 -- Check no existentials
321 ; if (null pat_tvs) then return ()
322 else lazyPatErr lpat pat_tvs
324 -- Check that the pattern has a lifted type
325 ; pat_tv <- newBoxyTyVar liftedTypeKind
326 ; boxyUnify pat_ty (mkTyVarTy pat_tv)
328 ; return (LazyPat pat', [], res) }
330 tc_pat pstate (WildPat _) pat_ty thing_inside
331 = do { pat_ty' <- unBoxWildCardType pat_ty -- Make sure it's filled in with monotypes
332 ; res <- thing_inside pstate
333 ; return (WildPat pat_ty', [], res) }
335 tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
336 = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
337 ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
338 tc_lpat pstate pat (idType bndr_id) thing_inside
339 -- NB: if we do inference on:
340 -- \ (y@(x::forall a. a->a)) = e
341 -- we'll fail. The as-pattern infers a monotype for 'y', which then
342 -- fails to unify with the polymorphic type for 'x'. This could
343 -- perhaps be fixed, but only with a bit more work.
345 -- If you fix it, don't forget the bindInstsOfPatIds!
346 ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
348 -- Type signatures in patterns
349 -- See Note [Pattern coercions] below
350 tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
351 = do { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
352 ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
353 tc_lpat pstate pat inner_ty thing_inside
354 ; return (SigPatOut pat' inner_ty, tvs, res) }
356 tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
357 = failWithTc (badTypePat pat)
359 ------------------------
360 -- Lists, tuples, arrays
361 tc_pat pstate (ListPat pats _) pat_ty thing_inside
362 = do { elt_ty <- boxySplitListTy pat_ty
363 ; let elt_tys = takeList pats (repeat elt_ty)
364 ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
365 ; return (ListPat pats' elt_ty, pats_tvs, res) }
367 tc_pat pstate (PArrPat pats _) pat_ty thing_inside
368 = do { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty
369 ; let elt_tys = takeList pats (repeat elt_ty)
370 ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
371 ; ifM (null pats) (zapToMonotype pat_ty) -- c.f. ExplicitPArr in TcExpr
372 ; return (PArrPat pats' elt_ty, pats_tvs, res) }
374 tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
375 = do { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
376 ; (pats', pats_tvs, res) <- tc_lpats pstate pats arg_tys thing_inside
378 -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
379 -- so that we can experiment with lazy tuple-matching.
380 -- This is a pretty odd place to make the switch, but
381 -- it was easy to do.
382 ; let unmangled_result = TuplePat pats' boxity pat_ty
383 possibly_mangled_result
384 | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
385 | otherwise = unmangled_result
387 ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced
388 return (possibly_mangled_result, pats_tvs, res) }
390 ------------------------
392 tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
393 = do { data_con <- tcLookupDataCon con_name
394 ; let tycon = dataConTyCon data_con
395 ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
397 ------------------------
399 tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
400 = do { boxyUnify (hsLitType simple_lit) pat_ty
401 ; res <- thing_inside pstate
402 ; returnM (LitPat simple_lit, [], res) }
404 ------------------------
405 -- Overloaded patterns: n, and n+k
406 tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside
407 = do { let orig = LiteralOrigin over_lit
408 ; lit' <- tcOverloadedLit orig over_lit pat_ty
409 ; eq' <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
410 ; mb_neg' <- case mb_neg of
411 Nothing -> return Nothing -- Positive literal
412 Just neg -> -- Negative literal
413 -- The 'negate' is re-mappable syntax
414 do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
415 ; return (Just neg') }
416 ; res <- thing_inside pstate
417 ; returnM (NPat lit' mb_neg' eq' pat_ty, [], res) }
419 tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
420 = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
421 ; let pat_ty' = idType bndr_id
422 orig = LiteralOrigin lit
423 ; lit' <- tcOverloadedLit orig lit pat_ty'
425 -- The '>=' and '-' parts are re-mappable syntax
426 ; ge' <- tcSyntaxOp orig ge (mkFunTys [pat_ty', pat_ty'] boolTy)
427 ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
429 -- The Report says that n+k patterns must be in Integral
430 -- We may not want this when using re-mappable syntax, though (ToDo?)
431 ; icls <- tcLookupClass integralClassName
432 ; dicts <- newDicts orig [mkClassPred icls [pat_ty']]
435 ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
436 ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
438 tc_pat _ _other_pat _ _ = panic "tc_pat" -- DictPat, ConPatOut, SigPatOut, VarPatOut
442 %************************************************************************
444 Most of the work for constructors is here
445 (the rest is in the ConPatIn case of tc_pat)
447 %************************************************************************
450 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
451 -> BoxySigmaType -- Type of the pattern
452 -> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
453 -> TcM (Pat TcId, [TcTyVar], a)
454 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
455 | isVanillaDataCon data_con
456 = do { ty_args <- boxySplitTyConApp tycon pat_ty
457 ; let (tvs, _, arg_tys, _, _) = dataConSig data_con
458 arg_tvs = exactTyVarsOfTypes arg_tys
459 -- See Note [Silly type synonyms in smart-app] in TcExpr
460 -- for why we must use exactTyVarsOfTypes
461 inst_prs = zipEqual "tcConPat" tvs ty_args
462 subst = mkTopTvSubst inst_prs
463 arg_tys' = substTys subst arg_tys
464 unconstrained_ty_args = [ty_arg | (tv,ty_arg) <- inst_prs,
465 not (tv `elemVarSet` arg_tvs)]
466 ; mapM unBox unconstrained_ty_args -- Zap these to monotypes
467 ; tcInstStupidTheta data_con ty_args
468 ; traceTc (text "tcConPat" <+> vcat [ppr data_con, ppr ty_args, ppr arg_tys'])
469 ; (arg_pats', tvs, res) <- tcConArgs pstate data_con arg_pats arg_tys' thing_inside
470 ; return (ConPatOut (L con_span data_con) [] [] emptyLHsBinds
471 arg_pats' (mkTyConApp tycon ty_args),
474 | otherwise -- GADT case
475 = do { ty_args <- boxySplitTyConApp tycon pat_ty
476 ; span <- getSrcSpanM -- The whole pattern
478 -- Instantiate the constructor type variables and result type
479 ; let (tvs, theta, arg_tys, _, res_tys) = dataConSig data_con
480 arg_tvs = exactTyVarsOfTypes arg_tys
481 -- See Note [Silly type synonyms in smart-app] in TcExpr
482 -- for why we must use exactTyVarsOfTypes
483 skol_info = PatSkol data_con span
484 arg_flags = [ tv `elemVarSet` arg_tvs | tv <- tvs ]
485 ; tvs' <- tcInstSkolTyVars skol_info tvs
486 ; let res_tys' = substTys (zipTopTvSubst tvs (mkTyVarTys tvs')) res_tys
488 -- Do type refinement!
489 ; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', ppr res_tys',
490 text "ty-args:" <+> ppr ty_args ])
491 ; refineAlt pstate data_con tvs' arg_flags res_tys' ty_args
492 $ \ pstate' tv_tys' -> do
494 -- ToDo: arg_tys should be boxy, but I don't think theta' should be,
495 -- or the tv_tys' in the call to tcInstStupidTheta
496 { let tenv' = zipTopTvSubst tvs tv_tys'
497 theta' = substTheta tenv' theta
498 arg_tys' = substTys tenv' arg_tys -- Boxy types
500 ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
501 do { tcInstStupidTheta data_con tv_tys'
502 -- The stupid-theta mentions the newly-bound tyvars, so
503 -- it must live inside the getLIE, so that the
504 -- tcSimplifyCheck will apply the type refinement to it
505 ; tcConArgs pstate' data_con arg_pats arg_tys' thing_inside }
507 ; dicts <- newDicts (SigOrigin skol_info) theta'
508 ; dict_binds <- tcSimplifyCheck doc tvs' dicts lie_req
510 ; return (ConPatOut (L con_span data_con)
511 tvs' (map instToId dicts) dict_binds
512 arg_pats' (mkTyConApp tycon ty_args),
513 tvs' ++ inner_tvs, res)
516 doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
518 tcConArgs :: PatState -> DataCon
519 -> HsConDetails Name (LPat Name) -> [TcSigmaType]
520 -> (PatState -> TcM a)
521 -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a)
523 tcConArgs pstate data_con (PrefixCon arg_pats) arg_tys thing_inside
524 = do { checkTc (con_arity == no_of_args) -- Check correct arity
525 (arityErr "Constructor" data_con con_arity no_of_args)
526 ; (arg_pats', tvs, res) <- tc_lpats pstate arg_pats arg_tys thing_inside
527 ; return (PrefixCon arg_pats', tvs, res) }
529 con_arity = dataConSourceArity data_con
530 no_of_args = length arg_pats
532 tcConArgs pstate data_con (InfixCon p1 p2) arg_tys thing_inside
533 = do { checkTc (con_arity == 2) -- Check correct arity
534 (arityErr "Constructor" data_con con_arity 2)
535 ; ([p1',p2'], tvs, res) <- tc_lpats pstate [p1,p2] arg_tys thing_inside
536 ; return (InfixCon p1' p2', tvs, res) }
538 con_arity = dataConSourceArity data_con
540 tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside
541 = do { (rpats', tvs, res) <- tc_fields pstate rpats thing_inside
542 ; return (RecCon rpats', tvs, res) }
544 tc_fields :: PatState -> [(Located Name, LPat Name)]
545 -> (PatState -> TcM a)
546 -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a)
547 tc_fields pstate [] thing_inside
548 = do { res <- thing_inside pstate
549 ; return ([], [], res) }
551 tc_fields pstate (rpat : rpats) thing_inside
552 = do { (rpat', tvs1, (rpats', tvs2, res))
553 <- tc_field pstate rpat $ \ pstate' ->
554 tc_fields pstate' rpats thing_inside
555 ; return (rpat':rpats', tvs1 ++ tvs2, res) }
557 tc_field pstate (field_lbl, pat) thing_inside
558 = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
559 ; (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
560 ; return ((sel_id, pat'), tvs, res) }
562 find_field_ty field_lbl
563 = case [ty | (f,ty) <- field_tys, f == field_lbl] of
565 -- No matching field; chances are this field label comes from some
566 -- other record type (or maybe none). As well as reporting an
567 -- error we still want to typecheck the pattern, principally to
568 -- make sure that all the variables it binds are put into the
569 -- environment, else the type checker crashes later:
570 -- f (R { foo = (a,b) }) = a+b
571 -- If foo isn't one of R's fields, we don't want to crash when
572 -- typechecking the "a+b".
573 [] -> do { addErrTc (badFieldCon data_con field_lbl)
574 ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
575 ; return (error "Bogus selector Id", bogus_ty) }
577 -- The normal case, when the field comes from the right constructor
579 ASSERT( null extras )
580 do { sel_id <- tcLookupId field_lbl
581 ; return (sel_id, pat_ty) }
583 field_tys = zip (dataConFieldLabels data_con) arg_tys
584 -- Don't use zipEqual! If the constructor isn't really a record, then
585 -- dataConFieldLabels will be empty (and each field in the pattern
586 -- will generate an error below).
590 %************************************************************************
594 %************************************************************************
597 refineAlt :: PatState
598 -> DataCon -- For tracing only
599 -> [TcTyVar] -- Type variables from pattern
600 -> [Bool] -- Flags indicating which type variables occur
601 -- in the type of at least one argument
602 -> [TcType] -- Result types from the pattern
603 -> [BoxySigmaType] -- Result types from the scrutinee (context)
604 -> (PatState -> [BoxySigmaType] -> TcM a)
605 -- Possibly-refined existentials
607 refineAlt pstate con pat_tvs arg_flags pat_res_tys ctxt_res_tys thing_inside
608 | not (all isRigidTy ctxt_res_tys)
609 -- The context is not a rigid type, so we do no type refinement here.
610 = do { let arg_tvs = mkVarSet [ tv | (tv, True) <- pat_tvs `zip` arg_flags]
611 subst = boxyMatchTypes arg_tvs pat_res_tys ctxt_res_tys
613 res_tvs = tcTyVarsOfTypes pat_res_tys
614 -- The tvs are (already) all fresh skolems. We need a
615 -- fresh skolem for each type variable (to bind in the pattern)
616 -- even if it's refined away by the type refinement
618 | not (tv `elemVarSet` res_tvs) = return (mkTyVarTy tv)
619 | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty
620 | otherwise = do { tv <- newBoxyTyVar openTypeKind
621 ; return (mkTyVarTy tv) }
622 ; pat_tys' <- mapM find_inst pat_tvs
624 -- Do the thing inside
625 ; res <- thing_inside pstate pat_tys'
627 -- Unbox the types that have been filled in by the thing_inside
628 -- I.e. the ones whose type variables are mentioned in at least one arg
629 ; let strip ty in_arg_tv | in_arg_tv = stripBoxyType ty
630 | otherwise = return ty
631 ; pat_tys'' <- zipWithM strip pat_tys' arg_flags
632 ; let subst = zipOpenTvSubst pat_tvs pat_tys''
633 ; boxyUnifyList (substTys subst pat_res_tys) ctxt_res_tys
635 ; return res } -- All boxes now filled
637 | otherwise -- The context is rigid, so we can do type refinement
638 = case gadtRefineTys (pat_reft pstate) con pat_tvs pat_res_tys ctxt_res_tys of
639 Failed msg -> failWithTc (inaccessibleAlt msg)
640 Succeeded (new_subst, all_bound_here)
641 | all_bound_here -- All the new bindings are for pat_tvs, so no need
642 -- to refine the environment or pstate
643 -> do { traceTc trace_msg
644 ; thing_inside pstate pat_tvs' }
645 | otherwise -- New bindings affect the context, so pass down pstate'.
646 -- DO NOT refine the envt, because we might be inside a
648 -> do { traceTc trace_msg
649 ; thing_inside pstate' pat_tvs' }
651 pat_tvs' = map (substTyVar new_subst) pat_tvs
652 pstate' = pstate { pat_reft = new_subst }
653 trace_msg = text "refineTypes:match" <+> ppr con <+> ppr new_subst
655 refineType :: GadtRefinement -> BoxyRhoType -> BoxyRhoType
656 -- Refine the type if it is rigid
658 | isRefineableTy ty = substTy reft ty
663 %************************************************************************
667 %************************************************************************
669 In tcOverloadedLit we convert directly to an Int or Integer if we
670 know that's what we want. This may save some time, by not
671 temporarily generating overloaded literals, but it won't catch all
672 cases (the rest are caught in lookupInst).
675 tcOverloadedLit :: InstOrigin
678 -> TcM (HsOverLit TcId)
679 tcOverloadedLit orig lit@(HsIntegral i fi) res_ty
680 | not (fi `isHsVar` fromIntegerName) -- Do not generate a LitInst for rebindable syntax.
681 -- Reason: If we do, tcSimplify will call lookupInst, which
682 -- will call tcSyntaxName, which does unification,
683 -- which tcSimplify doesn't like
684 -- ToDo: noLoc sadness
685 = do { integer_ty <- tcMetaTy integerTyConName
686 ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
687 ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) }
689 | Just expr <- shortCutIntLit i res_ty
690 = return (HsIntegral i expr)
693 = do { expr <- newLitInst orig lit res_ty
694 ; return (HsIntegral i expr) }
696 tcOverloadedLit orig lit@(HsFractional r fr) res_ty
697 | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case
698 = do { rat_ty <- tcMetaTy rationalTyConName
699 ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
700 -- Overloaded literals must have liftedTypeKind, because
701 -- we're instantiating an overloaded function here,
702 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
703 -- However this'll be picked up by tcSyntaxOp if necessary
704 ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty)))) }
706 | Just expr <- shortCutFracLit r res_ty
707 = return (HsFractional r expr)
710 = do { expr <- newLitInst orig lit res_ty
711 ; return (HsFractional r expr) }
713 newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
714 newLitInst orig lit res_ty -- Make a LitInst
715 = do { loc <- getInstLoc orig
716 ; res_tau <- zapToMonotype res_ty
717 ; new_uniq <- newUnique
718 ; let lit_nm = mkSystemVarName new_uniq FSLIT("lit")
719 lit_inst = LitInst lit_nm lit res_tau loc
721 ; return (HsVar (instToId lit_inst)) }
725 %************************************************************************
727 Note [Pattern coercions]
729 %************************************************************************
731 In principle, these program would be reasonable:
733 f :: (forall a. a->a) -> Int
734 f (x :: Int->Int) = x 3
736 g :: (forall a. [a]) -> Bool
739 In both cases, the function type signature restricts what arguments can be passed
740 in a call (to polymorphic ones). The pattern type signature then instantiates this
741 type. For example, in the first case, (forall a. a->a) <= Int -> Int, and we
742 generate the translated term
743 f = \x' :: (forall a. a->a). let x = x' Int in x 3
745 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
746 And it requires a significant amount of code to implement, becuase we need to decorate
747 the translated pattern with coercion functions (generated from the subsumption check
750 So for now I'm just insisting on type *equality* in patterns. No subsumption.
752 Old notes about desugaring, at a time when pattern coercions were handled:
754 A SigPat is a type coercion and must be handled one at at time. We can't
755 combine them unless the type of the pattern inside is identical, and we don't
756 bother to check for that. For example:
758 data T = T1 Int | T2 Bool
759 f :: (forall a. a -> a) -> T -> t
760 f (g::Int->Int) (T1 i) = T1 (g i)
761 f (g::Bool->Bool) (T2 b) = T2 (g b)
763 We desugar this as follows:
765 f = \ g::(forall a. a->a) t::T ->
767 in case t of { T1 i -> T1 (gi i)
770 in case t of { T2 b -> T2 (gb b)
773 Note that we do not treat the first column of patterns as a
774 column of variables, because the coerced variables (gi, gb)
775 would be of different types. So we get rather grotty code.
776 But I don't think this is a common case, and if it was we could
777 doubtless improve it.
779 Meanwhile, the strategy is:
780 * treat each SigPat coercion (always non-identity coercions)
782 * deal with the stuff inside, and then wrap a binding round
783 the result to bind the new variable (gi, gb, etc)
786 %************************************************************************
788 \subsection{Errors and contexts}
790 %************************************************************************
793 patCtxt :: Pat Name -> Maybe Message -- Not all patterns are worth pushing a context
794 patCtxt (VarPat _) = Nothing
795 patCtxt (ParPat _) = Nothing
796 patCtxt (AsPat _ _) = Nothing
797 patCtxt pat = Just (hang (ptext SLIT("In the pattern:"))
800 -----------------------------------------------
802 existentialExplode pats
803 = hang (vcat [text "My brain just exploded.",
804 text "I can't handle pattern bindings for existentially-quantified constructors.",
805 text "In the binding group for"])
806 4 (vcat (map ppr pats))
808 sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env
809 = do { pat_tys' <- mapM zonkTcType pat_tys
810 ; body_ty' <- zonkTcType body_ty
811 ; let (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
812 (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
813 (env3, tidy_body_ty) = tidyOpenType env2 body_ty'
815 sep [ptext SLIT("When checking an existential match that binds"),
816 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
817 ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
818 ptext SLIT("The body has type:") <+> ppr tidy_body_ty
821 show_ids = filter is_interesting bound_ids
822 is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
824 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
825 -- Don't zonk the types so we get the separate, un-unified versions
827 badFieldCon :: DataCon -> Name -> SDoc
828 badFieldCon con field
829 = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
830 ptext SLIT("does not have field"), quotes (ppr field)]
832 polyPatSig :: TcType -> SDoc
834 = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
837 badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
841 hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
842 2 (vcat (map pprSkolTvBinding tvs))
845 = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg