2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
6 TcPat: Typechecking patterns
10 -- The above warning supression flag is a temporary kludge.
11 -- While working on this module you are encouraged to remove it and fix
12 -- any warnings in the module. See
13 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
16 module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit,
17 addDataConStupidTheta, badFieldCon, polyPatSig ) where
19 #include "HsVersions.h"
21 import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcInferRho)
47 import BasicTypes hiding (SuccessFlag(..))
57 %************************************************************************
61 %************************************************************************
64 tcLetPat :: (Name -> Maybe TcRhoType)
65 -> LPat Name -> BoxySigmaType
68 tcLetPat sig_fn pat pat_ty thing_inside
69 = do { let init_state = PS { pat_ctxt = LetPat sig_fn,
70 pat_reft = emptyRefinement,
72 ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)
74 -- Don't know how to deal with pattern-bound existentials yet
75 ; checkTc (null ex_tvs) (existentialExplode pat)
77 ; return (pat', res) }
80 tcLamPats :: [LPat Name] -- Patterns,
81 -> [BoxySigmaType] -- and their types
82 -> BoxyRhoType -- Result type,
83 -> ((Refinement, BoxyRhoType) -> TcM a) -- and the checker for the body
84 -> TcM ([LPat TcId], a)
86 -- This is the externally-callable wrapper function
87 -- Typecheck the patterns, extend the environment to bind the variables,
88 -- do the thing inside, use any existentially-bound dictionaries to
89 -- discharge parts of the returning LIE, and deal with pattern type
92 -- 1. Initialise the PatState
93 -- 2. Check the patterns
94 -- 3. Apply the refinement to the environment and result type
96 -- 5. Check that no existentials escape
98 tcLamPats pats tys res_ty thing_inside
99 = tc_lam_pats (zipEqual "tcLamPats" pats tys)
100 (emptyRefinement, res_ty) thing_inside
102 tcLamPat :: LPat Name -> BoxySigmaType
103 -> (Refinement,BoxyRhoType) -- Result type
104 -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
105 -> TcM (LPat TcId, a)
106 tcLamPat pat pat_ty res_ty thing_inside
107 = do { ([pat'],thing) <- tc_lam_pats [(pat, pat_ty)] res_ty thing_inside
108 ; return (pat', thing) }
111 tc_lam_pats :: [(LPat Name,BoxySigmaType)]
112 -> (Refinement,BoxyRhoType) -- Result type
113 -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
114 -> TcM ([LPat TcId], a)
115 tc_lam_pats pat_ty_prs (reft, res_ty) thing_inside
116 = do { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft, pat_eqs = False }
118 ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
119 refineEnvironment (pat_reft pstate') (pat_eqs pstate') $
120 if (pat_eqs pstate' && (not $ isRigidTy res_ty))
121 then failWithTc (nonRigidResult res_ty)
122 else thing_inside (pat_reft pstate', res_ty)
124 ; let tys = map snd pat_ty_prs
125 ; tcCheckExistentialPat pats' ex_tvs tys res_ty
127 ; returnM (pats', res) }
131 tcCheckExistentialPat :: [LPat TcId] -- Patterns (just for error message)
132 -> [TcTyVar] -- Existentially quantified tyvars bound by pattern
133 -> [BoxySigmaType] -- Types of the patterns
134 -> BoxyRhoType -- Type of the body of the match
135 -- Tyvars in either of these must not escape
137 -- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat
138 -- For example, we must reject this program:
139 -- data C = forall a. C (a -> Int)
141 -- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
143 tcCheckExistentialPat pats [] pat_tys body_ty
144 = return () -- Short cut for case when there are no existentials
146 tcCheckExistentialPat pats ex_tvs pat_tys body_ty
147 = addErrCtxtM (sigPatCtxt pats ex_tvs pat_tys body_ty) $
148 checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
152 pat_reft :: Refinement, -- Binds rigid TcTyVars to their refinements
153 pat_eqs :: Bool -- <=> there are GADT equational constraints
159 | LetPat (Name -> Maybe TcRhoType) -- Used for let(rec) bindings
161 patSigCtxt :: PatState -> UserTypeCtxt
162 patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
163 patSigCtxt other = LamPatSigCtxt
168 %************************************************************************
172 %************************************************************************
175 tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
176 tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
177 = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
178 -- We have an undecorated binder, so we do rule ABS1,
179 -- by unboxing the boxy type, forcing any un-filled-in
180 -- boxes to become monotypes
181 -- NB that pat_ty' can still be a polytype:
182 -- data T = MkT (forall a. a->a)
183 -- f t = case t of { MkT g -> ... }
184 -- Here, the 'g' must get type (forall a. a->a) from the
186 ; return (Id.mkLocalId bndr_name pat_ty') }
188 tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
189 | Just mono_ty <- lookup_sig bndr_name
190 = do { mono_name <- newLocalName bndr_name
191 ; boxyUnify mono_ty pat_ty
192 ; return (Id.mkLocalId mono_name mono_ty) }
195 = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
196 ; mono_name <- newLocalName bndr_name
197 ; return (Id.mkLocalId mono_name pat_ty') }
201 bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
202 bindInstsOfPatId id thing_inside
203 | not (isOverloadedTy (idType id))
204 = do { res <- thing_inside; return (res, emptyLHsBinds) }
206 = do { (res, lie) <- getLIE thing_inside
207 ; binds <- bindInstsOfLocalFuns lie [id]
208 ; return (res, binds) }
211 unBoxPatBndrType ty name = unBoxArgType ty (ptext SLIT("The variable") <+> quotes (ppr name))
212 unBoxWildCardType ty = unBoxArgType ty (ptext SLIT("A wild-card pattern"))
213 unBoxViewPatType ty pat = unBoxArgType ty (ptext SLIT("The view pattern") <+> ppr pat)
215 unBoxArgType :: BoxyType -> SDoc -> TcM TcType
216 -- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind;
217 -- that is, it can't be an unboxed tuple. For example,
218 -- case (f x) of r -> ...
219 -- should fail if 'f' returns an unboxed tuple.
220 unBoxArgType ty pp_this
221 = do { ty' <- unBox ty -- Returns a zonked type
223 -- Neither conditional is strictly necesssary (the unify alone will do)
224 -- but they improve error messages, and allocate fewer tyvars
225 ; if isUnboxedTupleType ty' then
227 else if isSubArgTypeKind (typeKind ty') then
229 else do -- OpenTypeKind, so constrain it
230 { ty2 <- newFlexiTyVarTy argTypeKind
234 msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple")
238 %************************************************************************
240 The main worker functions
242 %************************************************************************
246 tcPat takes a "thing inside" over which the pattern scopes. This is partly
247 so that tcPat can extend the environment for the thing_inside, but also
248 so that constraints arising in the thing_inside can be discharged by the
251 This does not work so well for the ErrCtxt carried by the monad: we don't
252 want the error-context for the pattern to scope over the RHS.
253 Hence the getErrCtxt/setErrCtxt stuff in tc_lpats.
257 type Checker inp out = forall r.
260 -> (PatState -> TcM r)
261 -> TcM (out, [TcTyVar], r)
263 tcMultiple :: Checker inp out -> Checker [inp] [out]
264 tcMultiple tc_pat args pstate thing_inside
265 = do { err_ctxt <- getErrCtxt
267 = do { res <- thing_inside pstate
268 ; return ([], [], res) }
270 loop pstate (arg:args)
271 = do { (p', p_tvs, (ps', ps_tvs, res))
272 <- tc_pat arg pstate $ \ pstate' ->
273 setErrCtxt err_ctxt $
275 -- setErrCtxt: restore context before doing the next pattern
276 -- See note [Nesting] above
278 ; return (p':ps', p_tvs ++ ps_tvs, res) }
283 tc_lpat_pr :: (LPat Name, BoxySigmaType)
285 -> (PatState -> TcM a)
286 -> TcM (LPat TcId, [TcTyVar], a)
287 tc_lpat_pr (pat, ty) = tc_lpat pat ty
292 -> (PatState -> TcM a)
293 -> TcM (LPat TcId, [TcTyVar], a)
294 tc_lpat (L span pat) pat_ty pstate thing_inside
296 maybeAddErrCtxt (patCtxt pat) $
297 do { let mb_reft = refineType (pat_reft pstate) pat_ty
298 pat_ty' = case mb_reft of { Just (_, ty') -> ty'; Nothing -> pat_ty }
300 -- Make sure the result type reflects the current refinement
301 -- We must do this here, so that it correctly ``sees'' all
302 -- the refinements to the left. Example:
303 -- Suppose C :: forall a. T a -> a -> Foo
304 -- Pattern C a p1 True
305 -- So p1 might refine 'a' to True, and the True
306 -- pattern had better see it.
308 ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
309 ; let final_pat = case mb_reft of
311 Just (co,_) -> CoPat (WpCo co) pat' pat_ty
312 ; return (L span final_pat, tvs, res) }
317 -> BoxySigmaType -- Fully refined result type
318 -> (PatState -> TcM a) -- Thing inside
319 -> TcM (Pat TcId, -- Translated pattern
320 [TcTyVar], -- Existential binders
321 a) -- Result of thing inside
323 tc_pat pstate (VarPat name) pat_ty thing_inside
324 = do { id <- tcPatBndr pstate name pat_ty
325 ; (res, binds) <- bindInstsOfPatId id $
326 tcExtendIdEnv1 name id $
327 (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
328 >> thing_inside pstate)
329 ; let pat' | isEmptyLHsBinds binds = VarPat id
330 | otherwise = VarPatOut id binds
331 ; return (pat', [], res) }
333 tc_pat pstate (ParPat pat) pat_ty thing_inside
334 = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
335 ; return (ParPat pat', tvs, res) }
337 tc_pat pstate (BangPat pat) pat_ty thing_inside
338 = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
339 ; return (BangPat pat', tvs, res) }
341 -- There's a wrinkle with irrefutable patterns, namely that we
342 -- must not propagate type refinement from them. For example
343 -- data T a where { T1 :: Int -> T Int; ... }
344 -- f :: T a -> Int -> a
346 -- It's obviously not sound to refine a to Int in the right
347 -- hand side, because the arugment might not match T1 at all!
349 -- Nor should a lazy pattern bind any existential type variables
350 -- because they won't be in scope when we do the desugaring
352 -- Note [Hopping the LIE in lazy patterns]
353 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
354 -- In a lazy pattern, we must *not* discharge constraints from the RHS
355 -- from dictionaries bound in the pattern. E.g.
357 -- We can't discharge the Num constraint from dictionaries bound by
360 -- So we have to make the constraints from thing_inside "hop around"
361 -- the pattern. Hence the getLLE and extendLIEs later.
363 tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
364 = do { (pat', pat_tvs, (res,lie))
365 <- tc_lpat pat pat_ty pstate $ \ _ ->
366 getLIE (thing_inside pstate)
367 -- Ignore refined pstate', revert to pstate
369 -- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns]
371 -- Check no existentials
372 ; if (null pat_tvs) then return ()
373 else lazyPatErr lpat pat_tvs
375 -- Check that the pattern has a lifted type
376 ; pat_tv <- newBoxyTyVar liftedTypeKind
377 ; boxyUnify pat_ty (mkTyVarTy pat_tv)
379 ; return (LazyPat pat', [], res) }
381 tc_pat pstate (WildPat _) pat_ty thing_inside
382 = do { pat_ty' <- unBoxWildCardType pat_ty -- Make sure it's filled in with monotypes
383 ; res <- thing_inside pstate
384 ; return (WildPat pat_ty', [], res) }
386 tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
387 = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
388 ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
389 tc_lpat pat (idType bndr_id) pstate thing_inside
390 -- NB: if we do inference on:
391 -- \ (y@(x::forall a. a->a)) = e
392 -- we'll fail. The as-pattern infers a monotype for 'y', which then
393 -- fails to unify with the polymorphic type for 'x'. This could
394 -- perhaps be fixed, but only with a bit more work.
396 -- If you fix it, don't forget the bindInstsOfPatIds!
397 ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
399 tc_pat pstate (orig@(ViewPat expr pat _)) overall_pat_ty thing_inside
400 = do { -- morally, expr must have type
401 -- `forall a1...aN. OPT' -> B`
402 -- where overall_pat_ty is an instance of OPT'.
403 -- Here, we infer a rho type for it,
404 -- which replaces the leading foralls and constraints
405 -- with fresh unification variables.
406 (expr',expr'_inferred) <- tcInferRho expr
407 -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty`
408 ; let expr'_expected = \ pat_ty -> (mkFunTy overall_pat_ty pat_ty)
409 -- tcSubExp: expected first, offered second
412 -- NOTE: this forces pat_ty to be a monotype (because we use a unification
413 -- variable to find it). this means that in an example like
414 -- (view -> f) where view :: _ -> forall b. b
415 -- we will only be able to use view at one instantation in the
417 ; (expr_coerc, pat_ty) <- tcInfer (\ pat_ty -> tcSubExp (expr'_expected pat_ty) expr'_inferred)
418 -- pattern must have pat_ty
419 ; (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
420 -- this should get zonked later on, but we unBox it here
421 -- so that we do the same checks as above
422 ; annotation_ty <- unBoxViewPatType overall_pat_ty orig
423 ; return (ViewPat (mkLHsWrap expr_coerc expr') pat' annotation_ty, tvs, res) }
425 -- Type signatures in patterns
426 -- See Note [Pattern coercions] below
427 tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
428 = do { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
429 ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
430 tc_lpat pat inner_ty pstate thing_inside
431 ; return (SigPatOut pat' inner_ty, tvs, res) }
433 tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
434 = failWithTc (badTypePat pat)
436 ------------------------
437 -- Lists, tuples, arrays
438 tc_pat pstate (ListPat pats _) pat_ty thing_inside
439 = do { (elt_ty, coi) <- boxySplitListTy pat_ty
440 ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
441 pats pstate thing_inside
442 ; return (mkCoPatCoI coi (ListPat pats' elt_ty) pat_ty, pats_tvs, res) }
444 tc_pat pstate (PArrPat pats _) pat_ty thing_inside
445 = do { (elt_ty, coi) <- boxySplitPArrTy pat_ty
446 ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
447 pats pstate thing_inside
448 ; ifM (null pats) (zapToMonotype pat_ty) -- c.f. ExplicitPArr in TcExpr
449 ; return (mkCoPatCoI coi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res) }
451 tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
452 = do { let tc = tupleTyCon boxity (length pats)
453 ; (arg_tys, coi) <- boxySplitTyConApp tc pat_ty
454 ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
457 -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
458 -- so that we can experiment with lazy tuple-matching.
459 -- This is a pretty odd place to make the switch, but
460 -- it was easy to do.
461 ; let pat_ty' = mkTyConApp tc arg_tys
462 -- pat_ty /= pat_ty iff coi /= IdCo
463 unmangled_result = TuplePat pats' boxity pat_ty'
464 possibly_mangled_result
465 | opt_IrrefutableTuples &&
466 isBoxed boxity = LazyPat (noLoc unmangled_result)
467 | otherwise = unmangled_result
469 ; ASSERT( length arg_tys == length pats ) -- Syntactically enforced
470 return (mkCoPatCoI coi possibly_mangled_result pat_ty, pats_tvs, res)
473 ------------------------
475 tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
476 = do { data_con <- tcLookupDataCon con_name
477 ; let tycon = dataConTyCon data_con
478 ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
480 ------------------------
482 tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
483 = do { let lit_ty = hsLitType simple_lit
484 ; coi <- boxyUnify lit_ty pat_ty
485 -- coi is of kind: lit_ty ~ pat_ty
486 ; res <- thing_inside pstate
487 ; span <- getSrcSpanM
488 -- pattern coercions have to
489 -- be of kind: pat_ty ~ lit_ty
491 ; returnM (mkCoPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty,
494 ------------------------
495 -- Overloaded patterns: n, and n+k
496 tc_pat pstate pat@(NPat over_lit mb_neg eq) pat_ty thing_inside
497 = do { let orig = LiteralOrigin over_lit
498 ; lit' <- tcOverloadedLit orig over_lit pat_ty
499 ; eq' <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
500 ; mb_neg' <- case mb_neg of
501 Nothing -> return Nothing -- Positive literal
502 Just neg -> -- Negative literal
503 -- The 'negate' is re-mappable syntax
504 do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
505 ; return (Just neg') }
506 ; res <- thing_inside pstate
507 ; returnM (NPat lit' mb_neg' eq', [], res) }
509 tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
510 = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
511 ; let pat_ty' = idType bndr_id
512 orig = LiteralOrigin lit
513 ; lit' <- tcOverloadedLit orig lit pat_ty'
515 -- The '>=' and '-' parts are re-mappable syntax
516 ; ge' <- tcSyntaxOp orig ge (mkFunTys [pat_ty', pat_ty'] boolTy)
517 ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
519 -- The Report says that n+k patterns must be in Integral
520 -- We may not want this when using re-mappable syntax, though (ToDo?)
521 ; icls <- tcLookupClass integralClassName
522 ; instStupidTheta orig [mkClassPred icls [pat_ty']]
524 ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
525 ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
527 tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut, VarPatOut
531 %************************************************************************
533 Most of the work for constructors is here
534 (the rest is in the ConPatIn case of tc_pat)
536 %************************************************************************
538 [Pattern matching indexed data types]
539 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
540 Consider the following declarations:
542 data family Map k :: * -> *
543 data instance Map (a, b) v = MapPair (Map a (Pair b v))
545 and a case expression
547 case x :: Map (Int, c) w of MapPair m -> ...
549 As explained by [Wrappers for data instance tycons] in MkIds.lhs, the
550 worker/wrapper types for MapPair are
552 $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
553 $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
555 So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
556 :R123Map, which means the straight use of boxySplitTyConApp would give a type
557 error. Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
558 boxySplitTyConApp with the family tycon Map instead, which gives us the family
559 type list {(Int, c), w}. To get the correct split for :R123Map, we need to
560 unify the family type list {(Int, c), w} with the instance types {(a, b), v}
561 (provided by tyConFamInst_maybe together with the family tycon). This
562 unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
563 the split arguments for the representation tycon :R123Map as {Int, c, w}
565 In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
567 Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
569 moving between representation and family type into account. To produce type
570 correct Core, this coercion needs to be used to case the type of the scrutinee
571 from the family to the representation type. This is achieved by
572 unwrapFamInstScrutinee using a CoPat around the result pattern.
574 Now it might appear seem as if we could have used the existing GADT type
575 refinement infrastructure of refineAlt and friends instead of the explicit
576 unification and CoPat generation. However, that would be wrong. Why? The
577 whole point of GADT refinement is that the refinement is local to the case
578 alternative. In contrast, the substitution generated by the unification of
579 the family type list and instance types needs to be propagated to the outside.
580 Imagine that in the above example, the type of the scrutinee would have been
581 (Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
582 substitution [x -> (a, b), v -> w]. In contrast to GADT matching, the
583 instantiation of x with (a, b) must be global; ie, it must be valid in *all*
584 alternatives of the case expression, whereas in the GADT case it might vary
585 between alternatives.
587 In fact, if we have a data instance declaration defining a GADT, eq_spec will
588 be non-empty and we will get a mixture of global instantiations and local
589 refinement from a single match. This neatly reflects that, as soon as we
590 have constrained the type of the scrutinee to the required type index, all
591 further type refinement is local to the alternative.
595 -- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
596 -- with scrutinee of type (T ty)
598 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
599 -> BoxySigmaType -- Type of the pattern
600 -> HsConPatDetails Name -> (PatState -> TcM a)
601 -> TcM (Pat TcId, [TcTyVar], a)
602 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
603 = do { let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _) = dataConFullSig data_con
604 skol_info = PatSkol data_con
605 origin = SigOrigin skol_info
606 full_theta = eq_theta ++ dict_theta
608 -- Instantiate the constructor type variables [a->ty]
609 -- This may involve doing a family-instance coercion, and building a wrapper
610 ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty
611 ; let pat_ty' = mkTyConApp tycon ctxt_res_tys
612 -- pat_ty /= pat_ty iff coi /= IdCo
614 = mkCoPatCoI coi (unwrapFamInstScrutinee tycon ctxt_res_tys res_pat) pat_ty
616 -- Add the stupid theta
617 ; addDataConStupidTheta data_con ctxt_res_tys
619 ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs -- Get location from monad,
621 ; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs)
622 (ctxt_res_tys ++ mkTyVarTys ex_tvs')
623 arg_tys' = substTys tenv arg_tys
625 ; if null ex_tvs && null eq_spec && null full_theta
626 then do { -- The common case; no class bindings etc (see Note [Arrows and patterns])
627 (arg_pats', inner_tvs, res) <- tcConArgs data_con arg_tys'
628 arg_pats pstate thing_inside
629 ; let res_pat = ConPatOut { pat_con = L con_span data_con,
630 pat_tvs = [], pat_dicts = [], pat_binds = emptyLHsBinds,
631 pat_args = arg_pats', pat_ty = pat_ty' }
633 ; return (wrap_res_pat res_pat, inner_tvs, res) }
635 else do -- The general case, with existential, and local equality constraints
636 { let eq_spec' = substEqSpec tenv eq_spec
637 theta' = substTheta tenv full_theta
638 ; co_vars <- newCoVars eq_spec' -- Make coercion variables
639 ; traceTc (text "tcConPat: refineAlt")
640 ; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty
641 ; traceTc (text "tcConPat: refineAlt done!")
643 ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
644 tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
646 ; loc <- getInstLoc origin
647 ; dicts <- newDictBndrs loc theta'
648 ; dict_binds <- tcSimplifyCheckPat loc co_vars (pat_reft pstate')
649 ex_tvs' dicts lie_req
651 ; let res_pat = ConPatOut { pat_con = L con_span data_con,
652 pat_tvs = ex_tvs' ++ co_vars,
653 pat_dicts = map instToVar dicts,
654 pat_binds = dict_binds,
655 pat_args = arg_pats', pat_ty = pat_ty' }
656 ; return (wrap_res_pat res_pat, ex_tvs' ++ inner_tvs, res)
659 -- Split against the family tycon if the pattern constructor
660 -- belongs to a family instance tycon.
661 boxySplitTyConAppWithFamily tycon pat_ty =
663 case tyConFamInst_maybe tycon of
664 Nothing -> boxySplitTyConApp tycon pat_ty
665 Just (fam_tycon, instTys) ->
666 do { (scrutinee_arg_tys, coi) <- boxySplitTyConApp fam_tycon pat_ty
667 ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
668 ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
669 ; return (freshTvs, coi)
672 traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
673 ppr tycon <+> ppr pat_ty
674 , text " family instance:" <+>
675 ppr (tyConFamInst_maybe tycon)
678 -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
679 -- pattern if the tycon is an instance of a family.
681 unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id
682 unwrapFamInstScrutinee tycon args pat
683 | Just co_con <- tyConFamilyCoercion_maybe tycon
684 -- , not (isNewTyCon tycon) -- newtypes are explicitly unwrapped by
686 -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
687 -- coercion is not the identity; mkCoPat is inconvenient as it
688 -- wants a located pattern.
689 = CoPat (WpCo $ mkTyConApp co_con args) -- co fam ty to repr ty
690 (pat {pat_ty = mkTyConApp tycon args}) -- representation type
691 pat_ty -- family inst type
696 tcConArgs :: DataCon -> [TcSigmaType]
697 -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
699 tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
700 = do { checkTc (con_arity == no_of_args) -- Check correct arity
701 (arityErr "Constructor" data_con con_arity no_of_args)
702 ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
703 ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
705 ; return (PrefixCon arg_pats', tvs, res) }
707 con_arity = dataConSourceArity data_con
708 no_of_args = length arg_pats
710 tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside
711 = do { checkTc (con_arity == 2) -- Check correct arity
712 (arityErr "Constructor" data_con con_arity 2)
713 ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
715 ; return (InfixCon p1' p2', tvs, res) }
717 con_arity = dataConSourceArity data_con
719 tcConArgs data_con other_args (InfixCon p1 p2) pstate thing_inside
720 = pprPanic "tcConArgs" (ppr data_con) -- InfixCon always has two arguments
722 tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
723 = do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
724 ; return (RecCon (HsRecFields rpats' dd), tvs, res) }
726 tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
727 tc_field (HsRecField field_lbl pat pun) pstate thing_inside
728 = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
729 ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
730 ; return (HsRecField sel_id pat' pun, tvs, res) }
732 find_field_ty :: FieldLabel -> TcM (Id, TcType)
733 find_field_ty field_lbl
734 = case [ty | (f,ty) <- field_tys, f == field_lbl] of
736 -- No matching field; chances are this field label comes from some
737 -- other record type (or maybe none). As well as reporting an
738 -- error we still want to typecheck the pattern, principally to
739 -- make sure that all the variables it binds are put into the
740 -- environment, else the type checker crashes later:
741 -- f (R { foo = (a,b) }) = a+b
742 -- If foo isn't one of R's fields, we don't want to crash when
743 -- typechecking the "a+b".
744 [] -> do { addErrTc (badFieldCon data_con field_lbl)
745 ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
746 ; return (error "Bogus selector Id", bogus_ty) }
748 -- The normal case, when the field comes from the right constructor
750 ASSERT( null extras )
751 do { sel_id <- tcLookupField field_lbl
752 ; return (sel_id, pat_ty) }
754 field_tys :: [(FieldLabel, TcType)]
755 field_tys = zip (dataConFieldLabels data_con) arg_tys
756 -- Don't use zipEqual! If the constructor isn't really a record, then
757 -- dataConFieldLabels will be empty (and each field in the pattern
758 -- will generate an error below).
760 tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
761 tcConArg (arg_pat, arg_ty) pstate thing_inside
762 = tc_lpat arg_pat arg_ty pstate thing_inside
763 -- NB: the tc_lpat will refine pat_ty if necessary
764 -- based on the current pstate, which may include
765 -- refinements from peer argument patterns to the left
769 addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
770 -- Instantiate the "stupid theta" of the data con, and throw
771 -- the constraints into the constraint set
772 addDataConStupidTheta data_con inst_tys
773 | null stupid_theta = return ()
774 | otherwise = instStupidTheta origin inst_theta
776 origin = OccurrenceOf (dataConName data_con)
777 -- The origin should always report "occurrence of C"
778 -- even when C occurs in a pattern
779 stupid_theta = dataConStupidTheta data_con
780 tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
781 inst_theta = substTheta tenv stupid_theta
784 Note [Arrows and patterns]
785 ~~~~~~~~~~~~~~~~~~~~~~~~~~
786 (Oct 07) Arrow noation has the odd property that it involves "holes in the scope".
788 expr :: Arrow a => a () Int
789 expr = proc (y,z) -> do
793 Here the 'proc (y,z)' binding scopes over the arrow tails but not the
794 arrow body (e.g 'term'). As things stand (bogusly) all the
795 constraints from the proc body are gathered together, so constraints
796 from 'term' will be seen by the tcPat for (y,z). But we must *not*
797 bind constraints from 'term' here, becuase the desugarer will not make
798 these bindings scope over 'term'.
800 The Right Thing is not to confuse these constraints together. But for
801 now the Easy Thing is to ensure that we do not have existential or
802 GADT constraints in a 'proc', and to short-cut the constraint
803 simplification for such vanilla patterns so that it binds no
804 constraints. Hence the 'fast path' in tcConPat; but it's also a good
805 plan for ordinary vanilla patterns to bypass the constraint
809 %************************************************************************
813 %************************************************************************
816 refineAlt :: DataCon -- For tracing only
818 -> [TcTyVar] -- Existentials
819 -> [CoVar] -- Equational constraints
820 -> BoxySigmaType -- Pattern type
823 refineAlt con pstate ex_tvs [] pat_ty
824 | null $ dataConEqTheta con
825 = return pstate -- Common case: no equational constraints
827 refineAlt con pstate ex_tvs co_vars pat_ty
828 = do { opt_gadt <- doptM Opt_GADTs -- No type-refinement unless GADTs are on
829 ; if (not opt_gadt) then return pstate
832 { checkTc (isRigidTy pat_ty) (nonRigidMatch con)
833 -- We are matching against a GADT constructor with non-trivial
834 -- constraints, but pattern type is wobbly. For now we fail.
835 -- We can make sense of this, however:
836 -- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a
837 -- (\x -> case x of { MkT v -> v })
838 -- We can infer that x must have type T [c], for some wobbly 'c'
840 -- (\(x::T [c]) -> case x of
841 -- MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g
842 -- To implement this, we'd first instantiate the equational
843 -- constraints with *wobbly* type variables for the existentials;
844 -- then unify these constraints to make pat_ty the right shape;
845 -- then proceed exactly as in the rigid case
847 -- In the rigid case, we perform type refinement
848 ; case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
849 Failed msg -> failWithTc (inaccessibleAlt msg) ;
850 Succeeded reft -> do { traceTc trace_msg
851 ; return (pstate { pat_reft = reft, pat_eqs = (pat_eqs pstate || not (null $ dataConEqTheta con)) }) }
852 -- DO NOT refine the envt right away, because we
853 -- might be inside a lazy pattern. Instead, refine pstate
856 trace_msg = text "refineAlt:match" <+>
857 vcat [ ppr con <+> ppr ex_tvs,
858 ppr [(v, tyVarKind v) | v <- co_vars],
864 %************************************************************************
868 %************************************************************************
870 In tcOverloadedLit we convert directly to an Int or Integer if we
871 know that's what we want. This may save some time, by not
872 temporarily generating overloaded literals, but it won't catch all
873 cases (the rest are caught in lookupInst).
876 tcOverloadedLit :: InstOrigin
879 -> TcM (HsOverLit TcId)
880 tcOverloadedLit orig lit@(HsIntegral i fi _) res_ty
881 | not (fi `isHsVar` fromIntegerName) -- Do not generate a LitInst for rebindable syntax.
882 -- Reason: If we do, tcSimplify will call lookupInst, which
883 -- will call tcSyntaxName, which does unification,
884 -- which tcSimplify doesn't like
885 -- ToDo: noLoc sadness
886 = do { integer_ty <- tcMetaTy integerTyConName
887 ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
888 ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty))) res_ty) }
890 | Just expr <- shortCutIntLit i res_ty
891 = return (HsIntegral i expr res_ty)
894 = do { expr <- newLitInst orig lit res_ty
895 ; return (HsIntegral i expr res_ty) }
897 tcOverloadedLit orig lit@(HsFractional r fr _) res_ty
898 | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case
899 = do { rat_ty <- tcMetaTy rationalTyConName
900 ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
901 -- Overloaded literals must have liftedTypeKind, because
902 -- we're instantiating an overloaded function here,
903 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
904 -- However this'll be picked up by tcSyntaxOp if necessary
905 ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty))) res_ty) }
907 | Just expr <- shortCutFracLit r res_ty
908 = return (HsFractional r expr res_ty)
911 = do { expr <- newLitInst orig lit res_ty
912 ; return (HsFractional r expr res_ty) }
914 tcOverloadedLit orig lit@(HsIsString s fr _) res_ty
915 | not (fr `isHsVar` fromStringName) -- c.f. HsIntegral case
916 = do { str_ty <- tcMetaTy stringTyConName
917 ; fr' <- tcSyntaxOp orig fr (mkFunTy str_ty res_ty)
918 ; return (HsIsString s (HsApp (noLoc fr') (nlHsLit (HsString s))) res_ty) }
920 | Just expr <- shortCutStringLit s res_ty
921 = return (HsIsString s expr res_ty)
924 = do { expr <- newLitInst orig lit res_ty
925 ; return (HsIsString s expr res_ty) }
927 newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
928 newLitInst orig lit res_ty -- Make a LitInst
929 = do { loc <- getInstLoc orig
930 ; res_tau <- zapToMonotype res_ty
931 ; new_uniq <- newUnique
932 ; let lit_nm = mkSystemVarName new_uniq FSLIT("lit")
933 lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit,
934 tci_ty = res_tau, tci_loc = loc}
936 ; return (HsVar (instToId lit_inst)) }
940 %************************************************************************
942 Note [Pattern coercions]
944 %************************************************************************
946 In principle, these program would be reasonable:
948 f :: (forall a. a->a) -> Int
949 f (x :: Int->Int) = x 3
951 g :: (forall a. [a]) -> Bool
954 In both cases, the function type signature restricts what arguments can be passed
955 in a call (to polymorphic ones). The pattern type signature then instantiates this
956 type. For example, in the first case, (forall a. a->a) <= Int -> Int, and we
957 generate the translated term
958 f = \x' :: (forall a. a->a). let x = x' Int in x 3
960 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
961 And it requires a significant amount of code to implement, becuase we need to decorate
962 the translated pattern with coercion functions (generated from the subsumption check
965 So for now I'm just insisting on type *equality* in patterns. No subsumption.
967 Old notes about desugaring, at a time when pattern coercions were handled:
969 A SigPat is a type coercion and must be handled one at at time. We can't
970 combine them unless the type of the pattern inside is identical, and we don't
971 bother to check for that. For example:
973 data T = T1 Int | T2 Bool
974 f :: (forall a. a -> a) -> T -> t
975 f (g::Int->Int) (T1 i) = T1 (g i)
976 f (g::Bool->Bool) (T2 b) = T2 (g b)
978 We desugar this as follows:
980 f = \ g::(forall a. a->a) t::T ->
982 in case t of { T1 i -> T1 (gi i)
985 in case t of { T2 b -> T2 (gb b)
988 Note that we do not treat the first column of patterns as a
989 column of variables, because the coerced variables (gi, gb)
990 would be of different types. So we get rather grotty code.
991 But I don't think this is a common case, and if it was we could
992 doubtless improve it.
994 Meanwhile, the strategy is:
995 * treat each SigPat coercion (always non-identity coercions)
997 * deal with the stuff inside, and then wrap a binding round
998 the result to bind the new variable (gi, gb, etc)
1001 %************************************************************************
1003 \subsection{Errors and contexts}
1005 %************************************************************************
1008 patCtxt :: Pat Name -> Maybe Message -- Not all patterns are worth pushing a context
1009 patCtxt (VarPat _) = Nothing
1010 patCtxt (ParPat _) = Nothing
1011 patCtxt (AsPat _ _) = Nothing
1012 patCtxt pat = Just (hang (ptext SLIT("In the pattern:"))
1015 -----------------------------------------------
1017 existentialExplode pat
1018 = hang (vcat [text "My brain just exploded.",
1019 text "I can't handle pattern bindings for existentially-quantified constructors.",
1020 text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
1021 text "In the binding group for"])
1024 sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env
1025 = do { pat_tys' <- mapM zonkTcType pat_tys
1026 ; body_ty' <- zonkTcType body_ty
1027 ; let (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
1028 (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
1029 (env3, tidy_body_ty) = tidyOpenType env2 body_ty'
1031 sep [ptext SLIT("When checking an existential match that binds"),
1032 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
1033 ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
1034 ptext SLIT("The body has type:") <+> ppr tidy_body_ty
1037 bound_ids = collectPatsBinders pats
1038 show_ids = filter is_interesting bound_ids
1039 is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
1041 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
1042 -- Don't zonk the types so we get the separate, un-unified versions
1044 badFieldCon :: DataCon -> Name -> SDoc
1045 badFieldCon con field
1046 = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
1047 ptext SLIT("does not have field"), quotes (ppr field)]
1049 polyPatSig :: TcType -> SDoc
1051 = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
1054 badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
1058 hang (ptext SLIT("A lazy (~) pattern cannot bind existential type variables"))
1059 2 (vcat (map pprSkolTvBinding tvs))
1062 = hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
1063 2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
1065 nonRigidResult res_ty
1066 = hang (ptext SLIT("GADT pattern match with non-rigid result type") <+> quotes (ppr res_ty))
1067 2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
1070 = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg