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, tcProcPat, tcOverloadedLit,
17 addDataConStupidTheta, badFieldCon, polyPatSig ) where
19 #include "HsVersions.h"
21 import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcInferRho)
46 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,
71 ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state
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 -> (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
95 -- 4. Check that no existentials escape
97 tcLamPats pats tys res_ty thing_inside
98 = tc_lam_pats LamPat (zipEqual "tcLamPats" pats tys)
101 tcLamPat :: LPat Name -> BoxySigmaType
102 -> BoxyRhoType -- Result type
103 -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
104 -> TcM (LPat TcId, a)
106 tcProcPat = tc_lam_pat ProcPat
107 tcLamPat = tc_lam_pat LamPat
109 tc_lam_pat ctxt pat pat_ty res_ty thing_inside
110 = do { ([pat'],thing) <- tc_lam_pats ctxt [(pat, pat_ty)] res_ty thing_inside
111 ; return (pat', thing) }
114 tc_lam_pats :: PatCtxt
115 -> [(LPat Name,BoxySigmaType)]
116 -> BoxyRhoType -- Result type
117 -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
118 -> TcM ([LPat TcId], a)
119 tc_lam_pats ctxt pat_ty_prs res_ty thing_inside
120 = do { let init_state = PS { pat_ctxt = ctxt, pat_eqs = False }
122 ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
123 if (pat_eqs pstate' && (not $ isRigidTy res_ty))
124 then failWithTc (nonRigidResult res_ty)
125 else thing_inside res_ty
127 ; let tys = map snd pat_ty_prs
128 ; tcCheckExistentialPat pats' ex_tvs tys res_ty
130 ; return (pats', res) }
134 tcCheckExistentialPat :: [LPat TcId] -- Patterns (just for error message)
135 -> [TcTyVar] -- Existentially quantified tyvars bound by pattern
136 -> [BoxySigmaType] -- Types of the patterns
137 -> BoxyRhoType -- Type of the body of the match
138 -- Tyvars in either of these must not escape
140 -- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat
141 -- For example, we must reject this program:
142 -- data C = forall a. C (a -> Int)
144 -- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
146 tcCheckExistentialPat pats [] pat_tys body_ty
147 = return () -- Short cut for case when there are no existentials
149 tcCheckExistentialPat pats ex_tvs pat_tys body_ty
150 = addErrCtxtM (sigPatCtxt pats ex_tvs pat_tys body_ty) $
151 checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
155 pat_eqs :: Bool -- <=> there are GADT equational constraints
161 | ProcPat -- The pattern in (proc pat -> ...)
162 -- see Note [Arrows and patterns]
163 | LetPat (Name -> Maybe TcRhoType) -- Used for let(rec) bindings
165 patSigCtxt :: PatState -> UserTypeCtxt
166 patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
167 patSigCtxt other = LamPatSigCtxt
172 %************************************************************************
176 %************************************************************************
179 tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
180 tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
181 | Just mono_ty <- lookup_sig bndr_name
182 = do { mono_name <- newLocalName bndr_name
183 ; boxyUnify mono_ty pat_ty
184 ; return (Id.mkLocalId mono_name mono_ty) }
187 = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
188 ; mono_name <- newLocalName bndr_name
189 ; return (Id.mkLocalId mono_name pat_ty') }
191 tcPatBndr (PS { pat_ctxt = _lam_or_proc }) bndr_name pat_ty
192 = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
193 -- We have an undecorated binder, so we do rule ABS1,
194 -- by unboxing the boxy type, forcing any un-filled-in
195 -- boxes to become monotypes
196 -- NB that pat_ty' can still be a polytype:
197 -- data T = MkT (forall a. a->a)
198 -- f t = case t of { MkT g -> ... }
199 -- Here, the 'g' must get type (forall a. a->a) from the
201 ; return (Id.mkLocalId bndr_name pat_ty') }
205 bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
206 bindInstsOfPatId id thing_inside
207 | not (isOverloadedTy (idType id))
208 = do { res <- thing_inside; return (res, emptyLHsBinds) }
210 = do { (res, lie) <- getLIE thing_inside
211 ; binds <- bindInstsOfLocalFuns lie [id]
212 ; return (res, binds) }
215 unBoxPatBndrType ty name = unBoxArgType ty (ptext SLIT("The variable") <+> quotes (ppr name))
216 unBoxWildCardType ty = unBoxArgType ty (ptext SLIT("A wild-card pattern"))
217 unBoxViewPatType ty pat = unBoxArgType ty (ptext SLIT("The view pattern") <+> ppr pat)
219 unBoxArgType :: BoxyType -> SDoc -> TcM TcType
220 -- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind;
221 -- that is, it can't be an unboxed tuple. For example,
222 -- case (f x) of r -> ...
223 -- should fail if 'f' returns an unboxed tuple.
224 unBoxArgType ty pp_this
225 = do { ty' <- unBox ty -- Returns a zonked type
227 -- Neither conditional is strictly necesssary (the unify alone will do)
228 -- but they improve error messages, and allocate fewer tyvars
229 ; if isUnboxedTupleType ty' then
231 else if isSubArgTypeKind (typeKind ty') then
233 else do -- OpenTypeKind, so constrain it
234 { ty2 <- newFlexiTyVarTy argTypeKind
238 msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple")
242 %************************************************************************
244 The main worker functions
246 %************************************************************************
250 tcPat takes a "thing inside" over which the pattern scopes. This is partly
251 so that tcPat can extend the environment for the thing_inside, but also
252 so that constraints arising in the thing_inside can be discharged by the
255 This does not work so well for the ErrCtxt carried by the monad: we don't
256 want the error-context for the pattern to scope over the RHS.
257 Hence the getErrCtxt/setErrCtxt stuff in tc_lpats.
261 type Checker inp out = forall r.
264 -> (PatState -> TcM r)
265 -> TcM (out, [TcTyVar], r)
267 tcMultiple :: Checker inp out -> Checker [inp] [out]
268 tcMultiple tc_pat args pstate thing_inside
269 = do { err_ctxt <- getErrCtxt
271 = do { res <- thing_inside pstate
272 ; return ([], [], res) }
274 loop pstate (arg:args)
275 = do { (p', p_tvs, (ps', ps_tvs, res))
276 <- tc_pat arg pstate $ \ pstate' ->
277 setErrCtxt err_ctxt $
279 -- setErrCtxt: restore context before doing the next pattern
280 -- See note [Nesting] above
282 ; return (p':ps', p_tvs ++ ps_tvs, res) }
287 tc_lpat_pr :: (LPat Name, BoxySigmaType)
289 -> (PatState -> TcM a)
290 -> TcM (LPat TcId, [TcTyVar], a)
291 tc_lpat_pr (pat, ty) = tc_lpat pat ty
296 -> (PatState -> TcM a)
297 -> TcM (LPat TcId, [TcTyVar], a)
298 tc_lpat (L span pat) pat_ty pstate thing_inside
300 maybeAddErrCtxt (patCtxt pat) $
301 do { (pat', tvs, res) <- tc_pat pstate pat pat_ty thing_inside
302 ; return (L span pat', tvs, res) }
307 -> BoxySigmaType -- Fully refined result type
308 -> (PatState -> TcM a) -- Thing inside
309 -> TcM (Pat TcId, -- Translated pattern
310 [TcTyVar], -- Existential binders
311 a) -- Result of thing inside
313 tc_pat pstate (VarPat name) pat_ty thing_inside
314 = do { id <- tcPatBndr pstate name pat_ty
315 ; (res, binds) <- bindInstsOfPatId id $
316 tcExtendIdEnv1 name id $
317 (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
318 >> thing_inside pstate)
319 ; let pat' | isEmptyLHsBinds binds = VarPat id
320 | otherwise = VarPatOut id binds
321 ; return (pat', [], res) }
323 tc_pat pstate (ParPat pat) pat_ty thing_inside
324 = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
325 ; return (ParPat pat', tvs, res) }
327 tc_pat pstate (BangPat pat) pat_ty thing_inside
328 = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
329 ; return (BangPat pat', tvs, res) }
331 -- There's a wrinkle with irrefutable patterns, namely that we
332 -- must not propagate type refinement from them. For example
333 -- data T a where { T1 :: Int -> T Int; ... }
334 -- f :: T a -> Int -> a
336 -- It's obviously not sound to refine a to Int in the right
337 -- hand side, because the arugment might not match T1 at all!
339 -- Nor should a lazy pattern bind any existential type variables
340 -- because they won't be in scope when we do the desugaring
342 -- Note [Hopping the LIE in lazy patterns]
343 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
344 -- In a lazy pattern, we must *not* discharge constraints from the RHS
345 -- from dictionaries bound in the pattern. E.g.
347 -- We can't discharge the Num constraint from dictionaries bound by
350 -- So we have to make the constraints from thing_inside "hop around"
351 -- the pattern. Hence the getLLE and extendLIEs later.
353 tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
354 = do { (pat', pat_tvs, (res,lie))
355 <- tc_lpat pat pat_ty pstate $ \ _ ->
356 getLIE (thing_inside pstate)
357 -- Ignore refined pstate', revert to pstate
359 -- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns]
361 -- Check no existentials
362 ; if (null pat_tvs) then return ()
363 else lazyPatErr lpat pat_tvs
365 -- Check that the pattern has a lifted type
366 ; pat_tv <- newBoxyTyVar liftedTypeKind
367 ; boxyUnify pat_ty (mkTyVarTy pat_tv)
369 ; return (LazyPat pat', [], res) }
371 tc_pat _ p@(QuasiQuotePat _) _ _
372 = pprPanic "Should never see QuasiQuotePat in type checker" (ppr p)
374 tc_pat pstate (WildPat _) pat_ty thing_inside
375 = do { pat_ty' <- unBoxWildCardType pat_ty -- Make sure it's filled in with monotypes
376 ; res <- thing_inside pstate
377 ; return (WildPat pat_ty', [], res) }
379 tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
380 = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
381 ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
382 tc_lpat pat (idType bndr_id) pstate thing_inside
383 -- NB: if we do inference on:
384 -- \ (y@(x::forall a. a->a)) = e
385 -- we'll fail. The as-pattern infers a monotype for 'y', which then
386 -- fails to unify with the polymorphic type for 'x'. This could
387 -- perhaps be fixed, but only with a bit more work.
389 -- If you fix it, don't forget the bindInstsOfPatIds!
390 ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
392 tc_pat pstate (orig@(ViewPat expr pat _)) overall_pat_ty thing_inside
393 = do { -- morally, expr must have type
394 -- `forall a1...aN. OPT' -> B`
395 -- where overall_pat_ty is an instance of OPT'.
396 -- Here, we infer a rho type for it,
397 -- which replaces the leading foralls and constraints
398 -- with fresh unification variables.
399 (expr',expr'_inferred) <- tcInferRho expr
400 -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty`
401 ; let expr'_expected = \ pat_ty -> (mkFunTy overall_pat_ty pat_ty)
402 -- tcSubExp: expected first, offered second
405 -- NOTE: this forces pat_ty to be a monotype (because we use a unification
406 -- variable to find it). this means that in an example like
407 -- (view -> f) where view :: _ -> forall b. b
408 -- we will only be able to use view at one instantation in the
410 ; (expr_coerc, pat_ty) <- tcInfer $ \ pat_ty ->
411 tcSubExp ViewPatOrigin (expr'_expected pat_ty) expr'_inferred
413 -- pattern must have pat_ty
414 ; (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
415 -- this should get zonked later on, but we unBox it here
416 -- so that we do the same checks as above
417 ; annotation_ty <- unBoxViewPatType overall_pat_ty orig
418 ; return (ViewPat (mkLHsWrap expr_coerc expr') pat' annotation_ty, tvs, res) }
420 -- Type signatures in patterns
421 -- See Note [Pattern coercions] below
422 tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
423 = do { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
424 ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
425 tc_lpat pat inner_ty pstate thing_inside
426 ; return (SigPatOut pat' inner_ty, tvs, res) }
428 tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
429 = failWithTc (badTypePat pat)
431 ------------------------
432 -- Lists, tuples, arrays
433 tc_pat pstate (ListPat pats _) pat_ty thing_inside
434 = do { (elt_ty, coi) <- boxySplitListTy pat_ty
435 ; let scoi = mkSymCoI coi
436 ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
437 pats pstate thing_inside
438 ; return (mkCoPatCoI scoi (ListPat pats' elt_ty) pat_ty, pats_tvs, res)
441 tc_pat pstate (PArrPat pats _) pat_ty thing_inside
442 = do { (elt_ty, coi) <- boxySplitPArrTy pat_ty
443 ; let scoi = mkSymCoI coi
444 ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
445 pats pstate thing_inside
446 ; when (null pats) (zapToMonotype pat_ty >> return ()) -- c.f. ExplicitPArr in TcExpr
447 ; return (mkCoPatCoI scoi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res)
450 tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
451 = do { let tc = tupleTyCon boxity (length pats)
452 ; (arg_tys, coi) <- boxySplitTyConApp tc pat_ty
453 ; let scoi = mkSymCoI coi
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 scoi 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 ; return (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 ; return (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 ; return (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 previous 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 RIP GADT refinement: refinements have been replaced by the use of explicit
588 equality constraints that are used in conjunction with implication constraints
589 to express the local scope of GADT refinements.
593 -- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
594 -- with scrutinee of type (T ty)
596 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
597 -> BoxySigmaType -- Type of the pattern
598 -> HsConPatDetails Name -> (PatState -> TcM a)
599 -> TcM (Pat TcId, [TcTyVar], a)
600 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
601 = do { let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _)
602 = dataConFullSig data_con
603 skol_info = PatSkol data_con
604 origin = SigOrigin skol_info
605 full_theta = eq_theta ++ dict_theta
607 -- Instantiate the constructor type variables [a->ty]
608 -- This may involve doing a family-instance coercion, and building a
610 ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty
611 ; let sym_coi = mkSymCoI coi -- boxy split coercion oriented wrongly
612 pat_ty' = mkTyConApp tycon ctxt_res_tys
613 -- pat_ty' /= pat_ty iff coi /= IdCo
615 wrap_res_pat res_pat = mkCoPatCoI sym_coi uwScrut pat_ty
617 uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys res_pat
619 ; traceTc $ case sym_coi of
620 IdCo -> text "sym_coi:IdCo"
621 ACo co -> text "sym_coi: ACoI" <+> ppr co
623 -- Add the stupid theta
624 ; addDataConStupidTheta data_con ctxt_res_tys
626 ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
627 -- Get location from monad, not from ex_tvs
629 ; let tenv = zipTopTvSubst (univ_tvs ++ ex_tvs)
630 (ctxt_res_tys ++ mkTyVarTys ex_tvs')
631 arg_tys' = substTys tenv arg_tys
633 ; if null ex_tvs && null eq_spec && null full_theta
634 then do { -- The common case; no class bindings etc
635 -- (see Note [Arrows and patterns])
636 (arg_pats', inner_tvs, res) <- tcConArgs data_con arg_tys'
637 arg_pats pstate thing_inside
638 ; let res_pat = ConPatOut { pat_con = L con_span data_con,
639 pat_tvs = [], pat_dicts = [],
640 pat_binds = emptyLHsBinds,
641 pat_args = arg_pats',
644 ; return (wrap_res_pat res_pat, inner_tvs, res) }
646 else do -- The general case, with existential, and local equality
648 { let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
649 theta' = substTheta tenv (eq_preds ++ full_theta)
650 -- order is *important* as we generate the list of
651 -- dictionary binders from theta'
652 ctxt = pat_ctxt pstate
653 ; checkTc (case ctxt of { ProcPat -> False; other -> True })
654 (existentialProcPat data_con)
656 -- Need to test for rigidity if *any* constraints in theta as class
657 -- constraints may have superclass equality constraints. However,
658 -- we don't want to check for rigidity if we got here only because
659 -- ex_tvs was non-null.
660 -- ; unless (null theta') $
661 -- FIXME: AT THE MOMENT WE CHEAT! We only perform the rigidity test
662 -- if we explicit or implicit (by a GADT def) have equality
664 ; unless (all (not . isEqPred) theta') $
665 checkTc (isRigidTy pat_ty) (nonRigidMatch data_con)
667 ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
668 tcConArgs data_con arg_tys' arg_pats pstate thing_inside
670 ; loc <- getInstLoc origin
671 ; dicts <- newDictBndrs loc theta'
672 ; dict_binds <- tcSimplifyCheckPat loc ex_tvs' dicts lie_req
674 ; let res_pat = ConPatOut { pat_con = L con_span data_con,
676 pat_dicts = map instToVar dicts,
677 pat_binds = dict_binds,
678 pat_args = arg_pats', pat_ty = pat_ty' }
679 ; return (wrap_res_pat res_pat, ex_tvs' ++ inner_tvs, res)
682 -- Split against the family tycon if the pattern constructor
683 -- belongs to a family instance tycon.
684 boxySplitTyConAppWithFamily tycon pat_ty =
686 case tyConFamInst_maybe tycon of
687 Nothing -> boxySplitTyConApp tycon pat_ty
688 Just (fam_tycon, instTys) ->
689 do { (scrutinee_arg_tys, coi) <- boxySplitTyConApp fam_tycon pat_ty
690 ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
691 ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
692 ; return (freshTvs, coi)
695 traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
696 ppr tycon <+> ppr pat_ty
697 , text " family instance:" <+>
698 ppr (tyConFamInst_maybe tycon)
701 -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
702 -- pattern if the tycon is an instance of a family.
704 unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id
705 unwrapFamInstScrutinee tycon args pat
706 | Just co_con <- tyConFamilyCoercion_maybe tycon
707 -- , not (isNewTyCon tycon) -- newtypes are explicitly unwrapped by
709 -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
710 -- coercion is not the identity; mkCoPat is inconvenient as it
711 -- wants a located pattern.
712 = CoPat (WpCo $ mkTyConApp co_con args) -- co fam ty to repr ty
713 (pat {pat_ty = mkTyConApp tycon args}) -- representation type
714 pat_ty -- family inst type
719 tcConArgs :: DataCon -> [TcSigmaType]
720 -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
722 tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
723 = do { checkTc (con_arity == no_of_args) -- Check correct arity
724 (arityErr "Constructor" data_con con_arity no_of_args)
725 ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
726 ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
728 ; return (PrefixCon arg_pats', tvs, res) }
730 con_arity = dataConSourceArity data_con
731 no_of_args = length arg_pats
733 tcConArgs data_con arg_tys (InfixCon p1 p2) pstate thing_inside
734 = do { checkTc (con_arity == 2) -- Check correct arity
735 (arityErr "Constructor" data_con con_arity 2)
736 ; let [arg_ty1,arg_ty2] = arg_tys -- This can't fail after the arity check
737 ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
739 ; return (InfixCon p1' p2', tvs, res) }
741 con_arity = dataConSourceArity data_con
743 tcConArgs data_con other_args (InfixCon p1 p2) pstate thing_inside
744 = pprPanic "tcConArgs" (ppr data_con) -- InfixCon always has two arguments
746 tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
747 = do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
748 ; return (RecCon (HsRecFields rpats' dd), tvs, res) }
750 tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
751 tc_field (HsRecField field_lbl pat pun) pstate thing_inside
752 = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
753 ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
754 ; return (HsRecField sel_id pat' pun, tvs, res) }
756 find_field_ty :: FieldLabel -> TcM (Id, TcType)
757 find_field_ty field_lbl
758 = case [ty | (f,ty) <- field_tys, f == field_lbl] of
760 -- No matching field; chances are this field label comes from some
761 -- other record type (or maybe none). As well as reporting an
762 -- error we still want to typecheck the pattern, principally to
763 -- make sure that all the variables it binds are put into the
764 -- environment, else the type checker crashes later:
765 -- f (R { foo = (a,b) }) = a+b
766 -- If foo isn't one of R's fields, we don't want to crash when
767 -- typechecking the "a+b".
768 [] -> do { addErrTc (badFieldCon data_con field_lbl)
769 ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
770 ; return (error "Bogus selector Id", bogus_ty) }
772 -- The normal case, when the field comes from the right constructor
774 ASSERT( null extras )
775 do { sel_id <- tcLookupField field_lbl
776 ; return (sel_id, pat_ty) }
778 field_tys :: [(FieldLabel, TcType)]
779 field_tys = zip (dataConFieldLabels data_con) arg_tys
780 -- Don't use zipEqual! If the constructor isn't really a record, then
781 -- dataConFieldLabels will be empty (and each field in the pattern
782 -- will generate an error below).
784 tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
785 tcConArg (arg_pat, arg_ty) pstate thing_inside
786 = tc_lpat arg_pat arg_ty pstate thing_inside
790 addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
791 -- Instantiate the "stupid theta" of the data con, and throw
792 -- the constraints into the constraint set
793 addDataConStupidTheta data_con inst_tys
794 | null stupid_theta = return ()
795 | otherwise = instStupidTheta origin inst_theta
797 origin = OccurrenceOf (dataConName data_con)
798 -- The origin should always report "occurrence of C"
799 -- even when C occurs in a pattern
800 stupid_theta = dataConStupidTheta data_con
801 tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
802 inst_theta = substTheta tenv stupid_theta
805 Note [Arrows and patterns]
806 ~~~~~~~~~~~~~~~~~~~~~~~~~~
807 (Oct 07) Arrow noation has the odd property that it involves "holes in the scope".
809 expr :: Arrow a => a () Int
810 expr = proc (y,z) -> do
814 Here the 'proc (y,z)' binding scopes over the arrow tails but not the
815 arrow body (e.g 'term'). As things stand (bogusly) all the
816 constraints from the proc body are gathered together, so constraints
817 from 'term' will be seen by the tcPat for (y,z). But we must *not*
818 bind constraints from 'term' here, becuase the desugarer will not make
819 these bindings scope over 'term'.
821 The Right Thing is not to confuse these constraints together. But for
822 now the Easy Thing is to ensure that we do not have existential or
823 GADT constraints in a 'proc', and to short-cut the constraint
824 simplification for such vanilla patterns so that it binds no
825 constraints. Hence the 'fast path' in tcConPat; but it's also a good
826 plan for ordinary vanilla patterns to bypass the constraint
830 %************************************************************************
834 %************************************************************************
836 In tcOverloadedLit we convert directly to an Int or Integer if we
837 know that's what we want. This may save some time, by not
838 temporarily generating overloaded literals, but it won't catch all
839 cases (the rest are caught in lookupInst).
842 tcOverloadedLit :: InstOrigin
845 -> TcM (HsOverLit TcId)
846 tcOverloadedLit orig lit@(HsIntegral i fi _) res_ty
847 | not (fi `isHsVar` fromIntegerName) -- Do not generate a LitInst for rebindable syntax.
848 -- Reason: If we do, tcSimplify will call lookupInst, which
849 -- will call tcSyntaxName, which does unification,
850 -- which tcSimplify doesn't like
851 -- ToDo: noLoc sadness
852 = do { integer_ty <- tcMetaTy integerTyConName
853 ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
854 ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty))) res_ty) }
856 | Just expr <- shortCutIntLit i res_ty
857 = return (HsIntegral i expr res_ty)
860 = do { expr <- newLitInst orig lit res_ty
861 ; return (HsIntegral i expr res_ty) }
863 tcOverloadedLit orig lit@(HsFractional r fr _) res_ty
864 | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case
865 = do { rat_ty <- tcMetaTy rationalTyConName
866 ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
867 -- Overloaded literals must have liftedTypeKind, because
868 -- we're instantiating an overloaded function here,
869 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
870 -- However this'll be picked up by tcSyntaxOp if necessary
871 ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty))) res_ty) }
873 | Just expr <- shortCutFracLit r res_ty
874 = return (HsFractional r expr res_ty)
877 = do { expr <- newLitInst orig lit res_ty
878 ; return (HsFractional r expr res_ty) }
880 tcOverloadedLit orig lit@(HsIsString s fr _) res_ty
881 | not (fr `isHsVar` fromStringName) -- c.f. HsIntegral case
882 = do { str_ty <- tcMetaTy stringTyConName
883 ; fr' <- tcSyntaxOp orig fr (mkFunTy str_ty res_ty)
884 ; return (HsIsString s (HsApp (noLoc fr') (nlHsLit (HsString s))) res_ty) }
886 | Just expr <- shortCutStringLit s res_ty
887 = return (HsIsString s expr res_ty)
890 = do { expr <- newLitInst orig lit res_ty
891 ; return (HsIsString s expr res_ty) }
893 newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
894 newLitInst orig lit res_ty -- Make a LitInst
895 = do { loc <- getInstLoc orig
896 ; res_tau <- zapToMonotype res_ty
897 ; new_uniq <- newUnique
898 ; let lit_nm = mkSystemVarName new_uniq FSLIT("lit")
899 lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit,
900 tci_ty = res_tau, tci_loc = loc}
902 ; return (HsVar (instToId lit_inst)) }
906 %************************************************************************
908 Note [Pattern coercions]
910 %************************************************************************
912 In principle, these program would be reasonable:
914 f :: (forall a. a->a) -> Int
915 f (x :: Int->Int) = x 3
917 g :: (forall a. [a]) -> Bool
920 In both cases, the function type signature restricts what arguments can be passed
921 in a call (to polymorphic ones). The pattern type signature then instantiates this
922 type. For example, in the first case, (forall a. a->a) <= Int -> Int, and we
923 generate the translated term
924 f = \x' :: (forall a. a->a). let x = x' Int in x 3
926 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
927 And it requires a significant amount of code to implement, becuase we need to decorate
928 the translated pattern with coercion functions (generated from the subsumption check
931 So for now I'm just insisting on type *equality* in patterns. No subsumption.
933 Old notes about desugaring, at a time when pattern coercions were handled:
935 A SigPat is a type coercion and must be handled one at at time. We can't
936 combine them unless the type of the pattern inside is identical, and we don't
937 bother to check for that. For example:
939 data T = T1 Int | T2 Bool
940 f :: (forall a. a -> a) -> T -> t
941 f (g::Int->Int) (T1 i) = T1 (g i)
942 f (g::Bool->Bool) (T2 b) = T2 (g b)
944 We desugar this as follows:
946 f = \ g::(forall a. a->a) t::T ->
948 in case t of { T1 i -> T1 (gi i)
951 in case t of { T2 b -> T2 (gb b)
954 Note that we do not treat the first column of patterns as a
955 column of variables, because the coerced variables (gi, gb)
956 would be of different types. So we get rather grotty code.
957 But I don't think this is a common case, and if it was we could
958 doubtless improve it.
960 Meanwhile, the strategy is:
961 * treat each SigPat coercion (always non-identity coercions)
963 * deal with the stuff inside, and then wrap a binding round
964 the result to bind the new variable (gi, gb, etc)
967 %************************************************************************
969 \subsection{Errors and contexts}
971 %************************************************************************
974 patCtxt :: Pat Name -> Maybe Message -- Not all patterns are worth pushing a context
975 patCtxt (VarPat _) = Nothing
976 patCtxt (ParPat _) = Nothing
977 patCtxt (AsPat _ _) = Nothing
978 patCtxt pat = Just (hang (ptext SLIT("In the pattern:"))
981 -----------------------------------------------
983 existentialExplode pat
984 = hang (vcat [text "My brain just exploded.",
985 text "I can't handle pattern bindings for existentially-quantified constructors.",
986 text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
987 text "In the binding group for"])
990 sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env
991 = do { pat_tys' <- mapM zonkTcType pat_tys
992 ; body_ty' <- zonkTcType body_ty
993 ; let (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
994 (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
995 (env3, tidy_body_ty) = tidyOpenType env2 body_ty'
997 sep [ptext SLIT("When checking an existential match that binds"),
998 nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
999 ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
1000 ptext SLIT("The body has type:") <+> ppr tidy_body_ty
1003 bound_ids = collectPatsBinders pats
1004 show_ids = filter is_interesting bound_ids
1005 is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
1007 ppr_id id ty = ppr id <+> dcolon <+> ppr ty
1008 -- Don't zonk the types so we get the separate, un-unified versions
1010 badFieldCon :: DataCon -> Name -> SDoc
1011 badFieldCon con field
1012 = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
1013 ptext SLIT("does not have field"), quotes (ppr field)]
1015 polyPatSig :: TcType -> SDoc
1017 = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
1020 badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
1022 existentialProcPat :: DataCon -> SDoc
1023 existentialProcPat con
1024 = hang (ptext SLIT("Illegal constructor") <+> quotes (ppr con) <+> ptext SLIT("in a 'proc' pattern"))
1025 2 (ptext SLIT("Proc patterns cannot use existentials or GADTs"))
1029 hang (ptext SLIT("A lazy (~) pattern cannot bind existential type variables"))
1030 2 (vcat (map pprSkolTvBinding tvs))
1033 = hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
1034 2 (ptext SLIT("Solution: add a type signature"))
1036 nonRigidResult res_ty
1037 = hang (ptext SLIT("GADT pattern match with non-rigid result type") <+> quotes (ppr res_ty))
1038 2 (ptext SLIT("Solution: add a type signature"))
1041 = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg