1{- 2(c) The University of Glasgow 2006 3(c) The GRASP/AQUA Project, Glasgow University, 1992-1998 4 5 6TcPat: Typechecking patterns 7-} 8 9{-# LANGUAGE CPP, RankNTypes, TupleSections #-} 10{-# LANGUAGE FlexibleContexts #-} 11{-# LANGUAGE TypeFamilies #-} 12{-# LANGUAGE ViewPatterns #-} 13 14module TcPat ( tcLetPat, newLetBndr, LetBndrSpec(..) 15 , tcPat, tcPat_O, tcPats 16 , addDataConStupidTheta, badFieldCon, polyPatSig ) where 17 18#include "HsVersions.h" 19 20import GhcPrelude 21 22import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcSyntaxOpGen, tcInferSigma ) 23 24import GHC.Hs 25import TcHsSyn 26import TcSigs( TcPragEnv, lookupPragEnv, addInlinePrags ) 27import TcRnMonad 28import Inst 29import Id 30import Var 31import Name 32import RdrName 33import TcEnv 34import TcMType 35import TcValidity( arityErr ) 36import TyCoPpr ( pprTyVars ) 37import TcType 38import TcUnify 39import TcHsType 40import TysWiredIn 41import TcEvidence 42import TcOrigin 43import TyCon 44import DataCon 45import PatSyn 46import ConLike 47import PrelNames 48import BasicTypes hiding (SuccessFlag(..)) 49import DynFlags 50import SrcLoc 51import VarSet 52import Util 53import Outputable 54import qualified GHC.LanguageExtensions as LangExt 55import Control.Arrow ( second ) 56import ListSetOps ( getNth ) 57 58{- 59************************************************************************ 60* * 61 External interface 62* * 63************************************************************************ 64-} 65 66tcLetPat :: (Name -> Maybe TcId) 67 -> LetBndrSpec 68 -> LPat GhcRn -> ExpSigmaType 69 -> TcM a 70 -> TcM (LPat GhcTcId, a) 71tcLetPat sig_fn no_gen pat pat_ty thing_inside 72 = do { bind_lvl <- getTcLevel 73 ; let ctxt = LetPat { pc_lvl = bind_lvl 74 , pc_sig_fn = sig_fn 75 , pc_new = no_gen } 76 penv = PE { pe_lazy = True 77 , pe_ctxt = ctxt 78 , pe_orig = PatOrigin } 79 80 ; tc_lpat pat pat_ty penv thing_inside } 81 82----------------- 83tcPats :: HsMatchContext Name 84 -> [LPat GhcRn] -- Patterns, 85 -> [ExpSigmaType] -- and their types 86 -> TcM a -- and the checker for the body 87 -> TcM ([LPat GhcTcId], a) 88 89-- This is the externally-callable wrapper function 90-- Typecheck the patterns, extend the environment to bind the variables, 91-- do the thing inside, use any existentially-bound dictionaries to 92-- discharge parts of the returning LIE, and deal with pattern type 93-- signatures 94 95-- 1. Initialise the PatState 96-- 2. Check the patterns 97-- 3. Check the body 98-- 4. Check that no existentials escape 99 100tcPats ctxt pats pat_tys thing_inside 101 = tc_lpats penv pats pat_tys thing_inside 102 where 103 penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin } 104 105tcPat :: HsMatchContext Name 106 -> LPat GhcRn -> ExpSigmaType 107 -> TcM a -- Checker for body 108 -> TcM (LPat GhcTcId, a) 109tcPat ctxt = tcPat_O ctxt PatOrigin 110 111-- | A variant of 'tcPat' that takes a custom origin 112tcPat_O :: HsMatchContext Name 113 -> CtOrigin -- ^ origin to use if the type needs inst'ing 114 -> LPat GhcRn -> ExpSigmaType 115 -> TcM a -- Checker for body 116 -> TcM (LPat GhcTcId, a) 117tcPat_O ctxt orig pat pat_ty thing_inside 118 = tc_lpat pat pat_ty penv thing_inside 119 where 120 penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig } 121 122 123{- 124************************************************************************ 125* * 126 PatEnv, PatCtxt, LetBndrSpec 127* * 128************************************************************************ 129-} 130 131data PatEnv 132 = PE { pe_lazy :: Bool -- True <=> lazy context, so no existentials allowed 133 , pe_ctxt :: PatCtxt -- Context in which the whole pattern appears 134 , pe_orig :: CtOrigin -- origin to use if the pat_ty needs inst'ing 135 } 136 137data PatCtxt 138 = LamPat -- Used for lambdas, case etc 139 (HsMatchContext Name) 140 141 | LetPat -- Used only for let(rec) pattern bindings 142 -- See Note [Typing patterns in pattern bindings] 143 { pc_lvl :: TcLevel 144 -- Level of the binding group 145 146 , pc_sig_fn :: Name -> Maybe TcId 147 -- Tells the expected type 148 -- for binders with a signature 149 150 , pc_new :: LetBndrSpec 151 -- How to make a new binder 152 } -- for binders without signatures 153 154data LetBndrSpec 155 = LetLclBndr -- We are going to generalise, and wrap in an AbsBinds 156 -- so clone a fresh binder for the local monomorphic Id 157 158 | LetGblBndr TcPragEnv -- Generalisation plan is NoGen, so there isn't going 159 -- to be an AbsBinds; So we must bind the global version 160 -- of the binder right away. 161 -- And here is the inline-pragma information 162 163instance Outputable LetBndrSpec where 164 ppr LetLclBndr = text "LetLclBndr" 165 ppr (LetGblBndr {}) = text "LetGblBndr" 166 167makeLazy :: PatEnv -> PatEnv 168makeLazy penv = penv { pe_lazy = True } 169 170inPatBind :: PatEnv -> Bool 171inPatBind (PE { pe_ctxt = LetPat {} }) = True 172inPatBind (PE { pe_ctxt = LamPat {} }) = False 173 174{- ********************************************************************* 175* * 176 Binders 177* * 178********************************************************************* -} 179 180tcPatBndr :: PatEnv -> Name -> ExpSigmaType -> TcM (HsWrapper, TcId) 181-- (coi, xp) = tcPatBndr penv x pat_ty 182-- Then coi : pat_ty ~ typeof(xp) 183-- 184tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl = bind_lvl 185 , pc_sig_fn = sig_fn 186 , pc_new = no_gen } }) 187 bndr_name exp_pat_ty 188 -- For the LetPat cases, see 189 -- Note [Typechecking pattern bindings] in TcBinds 190 191 | Just bndr_id <- sig_fn bndr_name -- There is a signature 192 = do { wrap <- tcSubTypePat penv exp_pat_ty (idType bndr_id) 193 -- See Note [Subsumption check at pattern variables] 194 ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty) 195 ; return (wrap, bndr_id) } 196 197 | otherwise -- No signature 198 = do { (co, bndr_ty) <- case exp_pat_ty of 199 Check pat_ty -> promoteTcType bind_lvl pat_ty 200 Infer infer_res -> ASSERT( bind_lvl == ir_lvl infer_res ) 201 -- If we were under a constructor that bumped 202 -- the level, we'd be in checking mode 203 do { bndr_ty <- inferResultToType infer_res 204 ; return (mkTcNomReflCo bndr_ty, bndr_ty) } 205 ; bndr_id <- newLetBndr no_gen bndr_name bndr_ty 206 ; traceTc "tcPatBndr(nosig)" (vcat [ ppr bind_lvl 207 , ppr exp_pat_ty, ppr bndr_ty, ppr co 208 , ppr bndr_id ]) 209 ; return (mkWpCastN co, bndr_id) } 210 211tcPatBndr _ bndr_name pat_ty 212 = do { pat_ty <- expTypeToType pat_ty 213 ; traceTc "tcPatBndr(not let)" (ppr bndr_name $$ ppr pat_ty) 214 ; return (idHsWrapper, mkLocalId bndr_name pat_ty) } 215 -- Whether or not there is a sig is irrelevant, 216 -- as this is local 217 218newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId 219-- Make up a suitable Id for the pattern-binder. 220-- See Note [Typechecking pattern bindings], item (4) in TcBinds 221-- 222-- In the polymorphic case when we are going to generalise 223-- (plan InferGen, no_gen = LetLclBndr), generate a "monomorphic version" 224-- of the Id; the original name will be bound to the polymorphic version 225-- by the AbsBinds 226-- In the monomorphic case when we are not going to generalise 227-- (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds, 228-- and we use the original name directly 229newLetBndr LetLclBndr name ty 230 = do { mono_name <- cloneLocalName name 231 ; return (mkLocalId mono_name ty) } 232newLetBndr (LetGblBndr prags) name ty 233 = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name) 234 235tcSubTypePat :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper 236-- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt 237-- Used when typechecking patterns 238tcSubTypePat penv t1 t2 = tcSubTypeET (pe_orig penv) GenSigCtxt t1 t2 239 240{- Note [Subsumption check at pattern variables] 241~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 242When we come across a variable with a type signature, we need to do a 243subsumption, not equality, check against the context type. e.g. 244 245 data T = MkT (forall a. a->a) 246 f :: forall b. [b]->[b] 247 MkT f = blah 248 249Since 'blah' returns a value of type T, its payload is a polymorphic 250function of type (forall a. a->a). And that's enough to bind the 251less-polymorphic function 'f', but we need some impedance matching 252to witness the instantiation. 253 254 255************************************************************************ 256* * 257 The main worker functions 258* * 259************************************************************************ 260 261Note [Nesting] 262~~~~~~~~~~~~~~ 263tcPat takes a "thing inside" over which the pattern scopes. This is partly 264so that tcPat can extend the environment for the thing_inside, but also 265so that constraints arising in the thing_inside can be discharged by the 266pattern. 267 268This does not work so well for the ErrCtxt carried by the monad: we don't 269want the error-context for the pattern to scope over the RHS. 270Hence the getErrCtxt/setErrCtxt stuff in tcMultiple 271-} 272 273-------------------- 274type Checker inp out = forall r. 275 inp 276 -> PatEnv 277 -> TcM r 278 -> TcM (out, r) 279 280tcMultiple :: Checker inp out -> Checker [inp] [out] 281tcMultiple tc_pat args penv thing_inside 282 = do { err_ctxt <- getErrCtxt 283 ; let loop _ [] 284 = do { res <- thing_inside 285 ; return ([], res) } 286 287 loop penv (arg:args) 288 = do { (p', (ps', res)) 289 <- tc_pat arg penv $ 290 setErrCtxt err_ctxt $ 291 loop penv args 292 -- setErrCtxt: restore context before doing the next pattern 293 -- See note [Nesting] above 294 295 ; return (p':ps', res) } 296 297 ; loop penv args } 298 299-------------------- 300tc_lpat :: LPat GhcRn 301 -> ExpSigmaType 302 -> PatEnv 303 -> TcM a 304 -> TcM (LPat GhcTcId, a) 305tc_lpat (dL->L span pat) pat_ty penv thing_inside 306 = setSrcSpan span $ 307 do { (pat', res) <- maybeWrapPatCtxt pat (tc_pat penv pat pat_ty) 308 thing_inside 309 ; return (cL span pat', res) } 310 311tc_lpats :: PatEnv 312 -> [LPat GhcRn] -> [ExpSigmaType] 313 -> TcM a 314 -> TcM ([LPat GhcTcId], a) 315tc_lpats penv pats tys thing_inside 316 = ASSERT2( equalLength pats tys, ppr pats $$ ppr tys ) 317 tcMultiple (\(p,t) -> tc_lpat p t) 318 (zipEqual "tc_lpats" pats tys) 319 penv thing_inside 320 321-------------------- 322tc_pat :: PatEnv 323 -> Pat GhcRn 324 -> ExpSigmaType -- Fully refined result type 325 -> TcM a -- Thing inside 326 -> TcM (Pat GhcTcId, -- Translated pattern 327 a) -- Result of thing inside 328 329tc_pat penv (VarPat x (dL->L l name)) pat_ty thing_inside 330 = do { (wrap, id) <- tcPatBndr penv name pat_ty 331 ; res <- tcExtendIdEnv1 name id thing_inside 332 ; pat_ty <- readExpType pat_ty 333 ; return (mkHsWrapPat wrap (VarPat x (cL l id)) pat_ty, res) } 334 335tc_pat penv (ParPat x pat) pat_ty thing_inside 336 = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside 337 ; return (ParPat x pat', res) } 338 339tc_pat penv (BangPat x pat) pat_ty thing_inside 340 = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside 341 ; return (BangPat x pat', res) } 342 343tc_pat penv (LazyPat x pat) pat_ty thing_inside 344 = do { (pat', (res, pat_ct)) 345 <- tc_lpat pat pat_ty (makeLazy penv) $ 346 captureConstraints thing_inside 347 -- Ignore refined penv', revert to penv 348 349 ; emitConstraints pat_ct 350 -- captureConstraints/extendConstraints: 351 -- see Note [Hopping the LIE in lazy patterns] 352 353 -- Check that the expected pattern type is itself lifted 354 ; pat_ty <- readExpType pat_ty 355 ; _ <- unifyType Nothing (tcTypeKind pat_ty) liftedTypeKind 356 357 ; return (LazyPat x pat', res) } 358 359tc_pat _ (WildPat _) pat_ty thing_inside 360 = do { res <- thing_inside 361 ; pat_ty <- expTypeToType pat_ty 362 ; return (WildPat pat_ty, res) } 363 364tc_pat penv (AsPat x (dL->L nm_loc name) pat) pat_ty thing_inside 365 = do { (wrap, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty) 366 ; (pat', res) <- tcExtendIdEnv1 name bndr_id $ 367 tc_lpat pat (mkCheckExpType $ idType bndr_id) 368 penv thing_inside 369 -- NB: if we do inference on: 370 -- \ (y@(x::forall a. a->a)) = e 371 -- we'll fail. The as-pattern infers a monotype for 'y', which then 372 -- fails to unify with the polymorphic type for 'x'. This could 373 -- perhaps be fixed, but only with a bit more work. 374 -- 375 -- If you fix it, don't forget the bindInstsOfPatIds! 376 ; pat_ty <- readExpType pat_ty 377 ; return (mkHsWrapPat wrap (AsPat x (cL nm_loc bndr_id) pat') pat_ty, 378 res) } 379 380tc_pat penv (ViewPat _ expr pat) overall_pat_ty thing_inside 381 = do { 382 -- Expr must have type `forall a1...aN. OPT' -> B` 383 -- where overall_pat_ty is an instance of OPT'. 384 ; (expr',expr'_inferred) <- tcInferSigma expr 385 386 -- expression must be a function 387 ; let expr_orig = lexprCtOrigin expr 388 herald = text "A view pattern expression expects" 389 ; (expr_wrap1, [inf_arg_ty], inf_res_ty) 390 <- matchActualFunTys herald expr_orig (Just (unLoc expr)) 1 expr'_inferred 391 -- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty) 392 393 -- check that overall pattern is more polymorphic than arg type 394 ; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty 395 -- expr_wrap2 :: overall_pat_ty "->" inf_arg_ty 396 397 -- pattern must have inf_res_ty 398 ; (pat', res) <- tc_lpat pat (mkCheckExpType inf_res_ty) penv thing_inside 399 400 ; overall_pat_ty <- readExpType overall_pat_ty 401 ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper 402 overall_pat_ty inf_res_ty doc 403 -- expr_wrap2' :: (inf_arg_ty -> inf_res_ty) "->" 404 -- (overall_pat_ty -> inf_res_ty) 405 expr_wrap = expr_wrap2' <.> expr_wrap1 406 doc = text "When checking the view pattern function:" <+> (ppr expr) 407 ; return (ViewPat overall_pat_ty (mkLHsWrap expr_wrap expr') pat', res)} 408 409-- Type signatures in patterns 410-- See Note [Pattern coercions] below 411tc_pat penv (SigPat _ pat sig_ty) pat_ty thing_inside 412 = do { (inner_ty, tv_binds, wcs, wrap) <- tcPatSig (inPatBind penv) 413 sig_ty pat_ty 414 -- Using tcExtendNameTyVarEnv is appropriate here 415 -- because we're not really bringing fresh tyvars into scope. 416 -- We're *naming* existing tyvars. Note that it is OK for a tyvar 417 -- from an outer scope to mention one of these tyvars in its kind. 418 ; (pat', res) <- tcExtendNameTyVarEnv wcs $ 419 tcExtendNameTyVarEnv tv_binds $ 420 tc_lpat pat (mkCheckExpType inner_ty) penv thing_inside 421 ; pat_ty <- readExpType pat_ty 422 ; return (mkHsWrapPat wrap (SigPat inner_ty pat' sig_ty) pat_ty, res) } 423 424------------------------ 425-- Lists, tuples, arrays 426tc_pat penv (ListPat Nothing pats) pat_ty thing_inside 427 = do { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv pat_ty 428 ; (pats', res) <- tcMultiple (\p -> tc_lpat p (mkCheckExpType elt_ty)) 429 pats penv thing_inside 430 ; pat_ty <- readExpType pat_ty 431 ; return (mkHsWrapPat coi 432 (ListPat (ListPatTc elt_ty Nothing) pats') pat_ty, res) 433} 434 435tc_pat penv (ListPat (Just e) pats) pat_ty thing_inside 436 = do { tau_pat_ty <- expTypeToType pat_ty 437 ; ((pats', res, elt_ty), e') 438 <- tcSyntaxOpGen ListOrigin e [SynType (mkCheckExpType tau_pat_ty)] 439 SynList $ 440 \ [elt_ty] -> 441 do { (pats', res) <- tcMultiple (\p -> tc_lpat p (mkCheckExpType elt_ty)) 442 pats penv thing_inside 443 ; return (pats', res, elt_ty) } 444 ; return (ListPat (ListPatTc elt_ty (Just (tau_pat_ty,e'))) pats', res) 445} 446 447tc_pat penv (TuplePat _ pats boxity) pat_ty thing_inside 448 = do { let arity = length pats 449 tc = tupleTyCon boxity arity 450 -- NB: tupleTyCon does not flatten 1-tuples 451 -- See Note [Don't flatten tuples from HsSyn] in MkCore 452 ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) 453 penv pat_ty 454 -- Unboxed tuples have RuntimeRep vars, which we discard: 455 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon 456 ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys 457 Boxed -> arg_tys 458 ; (pats', res) <- tc_lpats penv pats (map mkCheckExpType con_arg_tys) 459 thing_inside 460 461 ; dflags <- getDynFlags 462 463 -- Under flag control turn a pattern (x,y,z) into ~(x,y,z) 464 -- so that we can experiment with lazy tuple-matching. 465 -- This is a pretty odd place to make the switch, but 466 -- it was easy to do. 467 ; let 468 unmangled_result = TuplePat con_arg_tys pats' boxity 469 -- pat_ty /= pat_ty iff coi /= IdCo 470 possibly_mangled_result 471 | gopt Opt_IrrefutableTuples dflags && 472 isBoxed boxity = LazyPat noExtField (noLoc unmangled_result) 473 | otherwise = unmangled_result 474 475 ; pat_ty <- readExpType pat_ty 476 ; ASSERT( con_arg_tys `equalLength` pats ) -- Syntactically enforced 477 return (mkHsWrapPat coi possibly_mangled_result pat_ty, res) 478 } 479 480tc_pat penv (SumPat _ pat alt arity ) pat_ty thing_inside 481 = do { let tc = sumTyCon arity 482 ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) 483 penv pat_ty 484 ; -- Drop levity vars, we don't care about them here 485 let con_arg_tys = drop arity arg_tys 486 ; (pat', res) <- tc_lpat pat (mkCheckExpType (con_arg_tys `getNth` (alt - 1))) 487 penv thing_inside 488 ; pat_ty <- readExpType pat_ty 489 ; return (mkHsWrapPat coi (SumPat con_arg_tys pat' alt arity) pat_ty 490 , res) 491 } 492 493------------------------ 494-- Data constructors 495tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside 496 = tcConPat penv con pat_ty arg_pats thing_inside 497 498------------------------ 499-- Literal patterns 500tc_pat penv (LitPat x simple_lit) pat_ty thing_inside 501 = do { let lit_ty = hsLitType simple_lit 502 ; wrap <- tcSubTypePat penv pat_ty lit_ty 503 ; res <- thing_inside 504 ; pat_ty <- readExpType pat_ty 505 ; return ( mkHsWrapPat wrap (LitPat x (convertLit simple_lit)) pat_ty 506 , res) } 507 508------------------------ 509-- Overloaded patterns: n, and n+k 510 511-- In the case of a negative literal (the more complicated case), 512-- we get 513-- 514-- case v of (-5) -> blah 515-- 516-- becoming 517-- 518-- if v == (negate (fromInteger 5)) then blah else ... 519-- 520-- There are two bits of rebindable syntax: 521-- (==) :: pat_ty -> neg_lit_ty -> Bool 522-- negate :: lit_ty -> neg_lit_ty 523-- where lit_ty is the type of the overloaded literal 5. 524-- 525-- When there is no negation, neg_lit_ty and lit_ty are the same 526tc_pat _ (NPat _ (dL->L l over_lit) mb_neg eq) pat_ty thing_inside 527 = do { let orig = LiteralOrigin over_lit 528 ; ((lit', mb_neg'), eq') 529 <- tcSyntaxOp orig eq [SynType pat_ty, SynAny] 530 (mkCheckExpType boolTy) $ 531 \ [neg_lit_ty] -> 532 let new_over_lit lit_ty = newOverloadedLit over_lit 533 (mkCheckExpType lit_ty) 534 in case mb_neg of 535 Nothing -> (, Nothing) <$> new_over_lit neg_lit_ty 536 Just neg -> -- Negative literal 537 -- The 'negate' is re-mappable syntax 538 second Just <$> 539 (tcSyntaxOp orig neg [SynRho] (mkCheckExpType neg_lit_ty) $ 540 \ [lit_ty] -> new_over_lit lit_ty) 541 542 ; res <- thing_inside 543 ; pat_ty <- readExpType pat_ty 544 ; return (NPat pat_ty (cL l lit') mb_neg' eq', res) } 545 546{- 547Note [NPlusK patterns] 548~~~~~~~~~~~~~~~~~~~~~~ 549From 550 551 case v of x + 5 -> blah 552 553we get 554 555 if v >= 5 then (\x -> blah) (v - 5) else ... 556 557There are two bits of rebindable syntax: 558 (>=) :: pat_ty -> lit1_ty -> Bool 559 (-) :: pat_ty -> lit2_ty -> var_ty 560 561lit1_ty and lit2_ty could conceivably be different. 562var_ty is the type inferred for x, the variable in the pattern. 563 564If the pushed-down pattern type isn't a tau-type, the two pat_ty's above 565could conceivably be different specializations. But this is very much 566like the situation in Note [Case branches must be taus] in TcMatches. 567So we tauify the pat_ty before proceeding. 568 569Note that we need to type-check the literal twice, because it is used 570twice, and may be used at different types. The second HsOverLit stored in the 571AST is used for the subtraction operation. 572-} 573 574-- See Note [NPlusK patterns] 575tc_pat penv (NPlusKPat _ (dL->L nm_loc name) 576 (dL->L loc lit) _ ge minus) pat_ty 577 thing_inside 578 = do { pat_ty <- expTypeToType pat_ty 579 ; let orig = LiteralOrigin lit 580 ; (lit1', ge') 581 <- tcSyntaxOp orig ge [synKnownType pat_ty, SynRho] 582 (mkCheckExpType boolTy) $ 583 \ [lit1_ty] -> 584 newOverloadedLit lit (mkCheckExpType lit1_ty) 585 ; ((lit2', minus_wrap, bndr_id), minus') 586 <- tcSyntaxOpGen orig minus [synKnownType pat_ty, SynRho] SynAny $ 587 \ [lit2_ty, var_ty] -> 588 do { lit2' <- newOverloadedLit lit (mkCheckExpType lit2_ty) 589 ; (wrap, bndr_id) <- setSrcSpan nm_loc $ 590 tcPatBndr penv name (mkCheckExpType var_ty) 591 -- co :: var_ty ~ idType bndr_id 592 593 -- minus_wrap is applicable to minus' 594 ; return (lit2', wrap, bndr_id) } 595 596 -- The Report says that n+k patterns must be in Integral 597 -- but it's silly to insist on this in the RebindableSyntax case 598 ; unlessM (xoptM LangExt.RebindableSyntax) $ 599 do { icls <- tcLookupClass integralClassName 600 ; instStupidTheta orig [mkClassPred icls [pat_ty]] } 601 602 ; res <- tcExtendIdEnv1 name bndr_id thing_inside 603 604 ; let minus'' = minus' { syn_res_wrap = 605 minus_wrap <.> syn_res_wrap minus' } 606 pat' = NPlusKPat pat_ty (cL nm_loc bndr_id) (cL loc lit1') lit2' 607 ge' minus'' 608 ; return (pat', res) } 609 610-- HsSpliced is an annotation produced by 'RnSplice.rnSplicePat'. 611-- Here we get rid of it and add the finalizers to the global environment. 612-- 613-- See Note [Delaying modFinalizers in untyped splices] in RnSplice. 614tc_pat penv (SplicePat _ (HsSpliced _ mod_finalizers (HsSplicedPat pat))) 615 pat_ty thing_inside 616 = do addModFinalizersWithLclEnv mod_finalizers 617 tc_pat penv pat pat_ty thing_inside 618 619tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut 620 621 622{- 623Note [Hopping the LIE in lazy patterns] 624~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 625In a lazy pattern, we must *not* discharge constraints from the RHS 626from dictionaries bound in the pattern. E.g. 627 f ~(C x) = 3 628We can't discharge the Num constraint from dictionaries bound by 629the pattern C! 630 631So we have to make the constraints from thing_inside "hop around" 632the pattern. Hence the captureConstraints and emitConstraints. 633 634The same thing ensures that equality constraints in a lazy match 635are not made available in the RHS of the match. For example 636 data T a where { T1 :: Int -> T Int; ... } 637 f :: T a -> Int -> a 638 f ~(T1 i) y = y 639It's obviously not sound to refine a to Int in the right 640hand side, because the argument might not match T1 at all! 641 642Finally, a lazy pattern should not bind any existential type variables 643because they won't be in scope when we do the desugaring 644 645 646************************************************************************ 647* * 648 Most of the work for constructors is here 649 (the rest is in the ConPatIn case of tc_pat) 650* * 651************************************************************************ 652 653[Pattern matching indexed data types] 654~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 655Consider the following declarations: 656 657 data family Map k :: * -> * 658 data instance Map (a, b) v = MapPair (Map a (Pair b v)) 659 660and a case expression 661 662 case x :: Map (Int, c) w of MapPair m -> ... 663 664As explained by [Wrappers for data instance tycons] in MkIds.hs, the 665worker/wrapper types for MapPair are 666 667 $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v 668 $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v 669 670So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is 671:R123Map, which means the straight use of boxySplitTyConApp would give a type 672error. Hence, the smart wrapper function boxySplitTyConAppWithFamily calls 673boxySplitTyConApp with the family tycon Map instead, which gives us the family 674type list {(Int, c), w}. To get the correct split for :R123Map, we need to 675unify the family type list {(Int, c), w} with the instance types {(a, b), v} 676(provided by tyConFamInst_maybe together with the family tycon). This 677unification yields the substitution [a -> Int, b -> c, v -> w], which gives us 678the split arguments for the representation tycon :R123Map as {Int, c, w} 679 680In other words, boxySplitTyConAppWithFamily implicitly takes the coercion 681 682 Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v} 683 684moving between representation and family type into account. To produce type 685correct Core, this coercion needs to be used to case the type of the scrutinee 686from the family to the representation type. This is achieved by 687unwrapFamInstScrutinee using a CoPat around the result pattern. 688 689Now it might appear seem as if we could have used the previous GADT type 690refinement infrastructure of refineAlt and friends instead of the explicit 691unification and CoPat generation. However, that would be wrong. Why? The 692whole point of GADT refinement is that the refinement is local to the case 693alternative. In contrast, the substitution generated by the unification of 694the family type list and instance types needs to be propagated to the outside. 695Imagine that in the above example, the type of the scrutinee would have been 696(Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the 697substitution [x -> (a, b), v -> w]. In contrast to GADT matching, the 698instantiation of x with (a, b) must be global; ie, it must be valid in *all* 699alternatives of the case expression, whereas in the GADT case it might vary 700between alternatives. 701 702RIP GADT refinement: refinements have been replaced by the use of explicit 703equality constraints that are used in conjunction with implication constraints 704to express the local scope of GADT refinements. 705-} 706 707-- Running example: 708-- MkT :: forall a b c. (a~[b]) => b -> c -> T a 709-- with scrutinee of type (T ty) 710 711tcConPat :: PatEnv -> Located Name 712 -> ExpSigmaType -- Type of the pattern 713 -> HsConPatDetails GhcRn -> TcM a 714 -> TcM (Pat GhcTcId, a) 715tcConPat penv con_lname@(dL->L _ con_name) pat_ty arg_pats thing_inside 716 = do { con_like <- tcLookupConLike con_name 717 ; case con_like of 718 RealDataCon data_con -> tcDataConPat penv con_lname data_con 719 pat_ty arg_pats thing_inside 720 PatSynCon pat_syn -> tcPatSynPat penv con_lname pat_syn 721 pat_ty arg_pats thing_inside 722 } 723 724tcDataConPat :: PatEnv -> Located Name -> DataCon 725 -> ExpSigmaType -- Type of the pattern 726 -> HsConPatDetails GhcRn -> TcM a 727 -> TcM (Pat GhcTcId, a) 728tcDataConPat penv (dL->L con_span con_name) data_con pat_ty 729 arg_pats thing_inside 730 = do { let tycon = dataConTyCon data_con 731 -- For data families this is the representation tycon 732 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _) 733 = dataConFullSig data_con 734 header = cL con_span (RealDataCon data_con) 735 736 -- Instantiate the constructor type variables [a->ty] 737 -- This may involve doing a family-instance coercion, 738 -- and building a wrapper 739 ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty 740 ; pat_ty <- readExpType pat_ty 741 742 -- Add the stupid theta 743 ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys 744 745 ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys 746 ; checkExistentials ex_tvs all_arg_tys penv 747 748 ; tenv <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys 749 -- NB: Do not use zipTvSubst! See #14154 750 -- We want to create a well-kinded substitution, so 751 -- that the instantiated type is well-kinded 752 753 ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv ex_tvs 754 -- Get location from monad, not from ex_tvs 755 756 ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys 757 -- pat_ty' is type of the actual constructor application 758 -- pat_ty' /= pat_ty iff coi /= IdCo 759 760 arg_tys' = substTys tenv arg_tys 761 762 ; traceTc "tcConPat" (vcat [ ppr con_name 763 , pprTyVars univ_tvs 764 , pprTyVars ex_tvs 765 , ppr eq_spec 766 , ppr theta 767 , pprTyVars ex_tvs' 768 , ppr ctxt_res_tys 769 , ppr arg_tys' 770 , ppr arg_pats ]) 771 ; if null ex_tvs && null eq_spec && null theta 772 then do { -- The common case; no class bindings etc 773 -- (see Note [Arrows and patterns]) 774 (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys' 775 arg_pats penv thing_inside 776 ; let res_pat = ConPatOut { pat_con = header, 777 pat_tvs = [], pat_dicts = [], 778 pat_binds = emptyTcEvBinds, 779 pat_args = arg_pats', 780 pat_arg_tys = ctxt_res_tys, 781 pat_wrap = idHsWrapper } 782 783 ; return (mkHsWrapPat wrap res_pat pat_ty, res) } 784 785 else do -- The general case, with existential, 786 -- and local equality constraints 787 { let theta' = substTheta tenv (eqSpecPreds eq_spec ++ theta) 788 -- order is *important* as we generate the list of 789 -- dictionary binders from theta' 790 no_equalities = null eq_spec && not (any isEqPred theta) 791 skol_info = PatSkol (RealDataCon data_con) mc 792 mc = case pe_ctxt penv of 793 LamPat mc -> mc 794 LetPat {} -> PatBindRhs 795 796 ; gadts_on <- xoptM LangExt.GADTs 797 ; families_on <- xoptM LangExt.TypeFamilies 798 ; checkTc (no_equalities || gadts_on || families_on) 799 (text "A pattern match on a GADT requires the" <+> 800 text "GADTs or TypeFamilies language extension") 801 -- #2905 decided that a *pattern-match* of a GADT 802 -- should require the GADT language flag. 803 -- Re TypeFamilies see also #7156 804 805 ; given <- newEvVars theta' 806 ; (ev_binds, (arg_pats', res)) 807 <- checkConstraints skol_info ex_tvs' given $ 808 tcConArgs (RealDataCon data_con) arg_tys' arg_pats penv thing_inside 809 810 ; let res_pat = ConPatOut { pat_con = header, 811 pat_tvs = ex_tvs', 812 pat_dicts = given, 813 pat_binds = ev_binds, 814 pat_args = arg_pats', 815 pat_arg_tys = ctxt_res_tys, 816 pat_wrap = idHsWrapper } 817 ; return (mkHsWrapPat wrap res_pat pat_ty, res) 818 } } 819 820tcPatSynPat :: PatEnv -> Located Name -> PatSyn 821 -> ExpSigmaType -- Type of the pattern 822 -> HsConPatDetails GhcRn -> TcM a 823 -> TcM (Pat GhcTcId, a) 824tcPatSynPat penv (dL->L con_span _) pat_syn pat_ty arg_pats thing_inside 825 = do { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn 826 827 ; (subst, univ_tvs') <- newMetaTyVars univ_tvs 828 829 ; let all_arg_tys = ty : prov_theta ++ arg_tys 830 ; checkExistentials ex_tvs all_arg_tys penv 831 ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs 832 ; let ty' = substTy tenv ty 833 arg_tys' = substTys tenv arg_tys 834 prov_theta' = substTheta tenv prov_theta 835 req_theta' = substTheta tenv req_theta 836 837 ; wrap <- tcSubTypePat penv pat_ty ty' 838 ; traceTc "tcPatSynPat" (ppr pat_syn $$ 839 ppr pat_ty $$ 840 ppr ty' $$ 841 ppr ex_tvs' $$ 842 ppr prov_theta' $$ 843 ppr req_theta' $$ 844 ppr arg_tys') 845 846 ; prov_dicts' <- newEvVars prov_theta' 847 848 ; let skol_info = case pe_ctxt penv of 849 LamPat mc -> PatSkol (PatSynCon pat_syn) mc 850 LetPat {} -> UnkSkol -- Doesn't matter 851 852 ; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta' 853 ; traceTc "instCall" (ppr req_wrap) 854 855 ; traceTc "checkConstraints {" Outputable.empty 856 ; (ev_binds, (arg_pats', res)) 857 <- checkConstraints skol_info ex_tvs' prov_dicts' $ 858 tcConArgs (PatSynCon pat_syn) arg_tys' arg_pats penv thing_inside 859 860 ; traceTc "checkConstraints }" (ppr ev_binds) 861 ; let res_pat = ConPatOut { pat_con = cL con_span $ PatSynCon pat_syn, 862 pat_tvs = ex_tvs', 863 pat_dicts = prov_dicts', 864 pat_binds = ev_binds, 865 pat_args = arg_pats', 866 pat_arg_tys = mkTyVarTys univ_tvs', 867 pat_wrap = req_wrap } 868 ; pat_ty <- readExpType pat_ty 869 ; return (mkHsWrapPat wrap res_pat pat_ty, res) } 870 871---------------------------- 872-- | Convenient wrapper for calling a matchExpectedXXX function 873matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a)) 874 -> PatEnv -> ExpSigmaType -> TcM (HsWrapper, a) 875-- See Note [Matching polytyped patterns] 876-- Returns a wrapper : pat_ty ~R inner_ty 877matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty 878 = do { pat_ty <- expTypeToType pat_ty 879 ; (wrap, pat_rho) <- topInstantiate orig pat_ty 880 ; (co, res) <- inner_match pat_rho 881 ; traceTc "matchExpectedPatTy" (ppr pat_ty $$ ppr wrap) 882 ; return (mkWpCastN (mkTcSymCo co) <.> wrap, res) } 883 884---------------------------- 885matchExpectedConTy :: PatEnv 886 -> TyCon -- The TyCon that this data 887 -- constructor actually returns 888 -- In the case of a data family this is 889 -- the /representation/ TyCon 890 -> ExpSigmaType -- The type of the pattern; in the case 891 -- of a data family this would mention 892 -- the /family/ TyCon 893 -> TcM (HsWrapper, [TcSigmaType]) 894-- See Note [Matching constructor patterns] 895-- Returns a wrapper : pat_ty "->" T ty1 ... tyn 896matchExpectedConTy (PE { pe_orig = orig }) data_tc exp_pat_ty 897 | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc 898 -- Comments refer to Note [Matching constructor patterns] 899 -- co_tc :: forall a. T [a] ~ T7 a 900 = do { pat_ty <- expTypeToType exp_pat_ty 901 ; (wrap, pat_rho) <- topInstantiate orig pat_ty 902 903 ; (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc) 904 -- tys = [ty1,ty2] 905 906 ; traceTc "matchExpectedConTy" (vcat [ppr data_tc, 907 ppr (tyConTyVars data_tc), 908 ppr fam_tc, ppr fam_args, 909 ppr exp_pat_ty, 910 ppr pat_ty, 911 ppr pat_rho, ppr wrap]) 912 ; co1 <- unifyType Nothing (mkTyConApp fam_tc (substTys subst fam_args)) pat_rho 913 -- co1 : T (ty1,ty2) ~N pat_rho 914 -- could use tcSubType here... but it's the wrong way round 915 -- for actual vs. expected in error messages. 916 917 ; let tys' = mkTyVarTys tvs' 918 co2 = mkTcUnbranchedAxInstCo co_tc tys' [] 919 -- co2 : T (ty1,ty2) ~R T7 ty1 ty2 920 921 full_co = mkTcSubCo (mkTcSymCo co1) `mkTcTransCo` co2 922 -- full_co :: pat_rho ~R T7 ty1 ty2 923 924 ; return ( mkWpCastR full_co <.> wrap, tys') } 925 926 | otherwise 927 = do { pat_ty <- expTypeToType exp_pat_ty 928 ; (wrap, pat_rho) <- topInstantiate orig pat_ty 929 ; (coi, tys) <- matchExpectedTyConApp data_tc pat_rho 930 ; return (mkWpCastN (mkTcSymCo coi) <.> wrap, tys) } 931 932{- 933Note [Matching constructor patterns] 934~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 935Suppose (coi, tys) = matchExpectedConType data_tc pat_ty 936 937 * In the simple case, pat_ty = tc tys 938 939 * If pat_ty is a polytype, we want to instantiate it 940 This is like part of a subsumption check. Eg 941 f :: (forall a. [a]) -> blah 942 f [] = blah 943 944 * In a type family case, suppose we have 945 data family T a 946 data instance T (p,q) = A p | B q 947 Then we'll have internally generated 948 data T7 p q = A p | B q 949 axiom coT7 p q :: T (p,q) ~ T7 p q 950 951 So if pat_ty = T (ty1,ty2), we return (coi, [ty1,ty2]) such that 952 coi = coi2 . coi1 : T7 t ~ pat_ty 953 coi1 : T (ty1,ty2) ~ pat_ty 954 coi2 : T7 ty1 ty2 ~ T (ty1,ty2) 955 956 For families we do all this matching here, not in the unifier, 957 because we never want a whisper of the data_tycon to appear in 958 error messages; it's a purely internal thing 959-} 960 961tcConArgs :: ConLike -> [TcSigmaType] 962 -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc) 963 964tcConArgs con_like arg_tys (PrefixCon arg_pats) penv thing_inside 965 = do { checkTc (con_arity == no_of_args) -- Check correct arity 966 (arityErr (text "constructor") con_like con_arity no_of_args) 967 ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys 968 ; (arg_pats', res) <- tcMultiple tcConArg pats_w_tys 969 penv thing_inside 970 ; return (PrefixCon arg_pats', res) } 971 where 972 con_arity = conLikeArity con_like 973 no_of_args = length arg_pats 974 975tcConArgs con_like arg_tys (InfixCon p1 p2) penv thing_inside 976 = do { checkTc (con_arity == 2) -- Check correct arity 977 (arityErr (text "constructor") con_like con_arity 2) 978 ; let [arg_ty1,arg_ty2] = arg_tys -- This can't fail after the arity check 979 ; ([p1',p2'], res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)] 980 penv thing_inside 981 ; return (InfixCon p1' p2', res) } 982 where 983 con_arity = conLikeArity con_like 984 985tcConArgs con_like arg_tys (RecCon (HsRecFields rpats dd)) penv thing_inside 986 = do { (rpats', res) <- tcMultiple tc_field rpats penv thing_inside 987 ; return (RecCon (HsRecFields rpats' dd), res) } 988 where 989 tc_field :: Checker (LHsRecField GhcRn (LPat GhcRn)) 990 (LHsRecField GhcTcId (LPat GhcTcId)) 991 tc_field (dL->L l (HsRecField (dL->L loc 992 (FieldOcc sel (dL->L lr rdr))) pat pun)) 993 penv thing_inside 994 = do { sel' <- tcLookupId sel 995 ; pat_ty <- setSrcSpan loc $ find_field_ty sel 996 (occNameFS $ rdrNameOcc rdr) 997 ; (pat', res) <- tcConArg (pat, pat_ty) penv thing_inside 998 ; return (cL l (HsRecField (cL loc (FieldOcc sel' (cL lr rdr))) pat' 999 pun), res) } 1000 tc_field (dL->L _ (HsRecField (dL->L _ (XFieldOcc _)) _ _)) _ _ 1001 = panic "tcConArgs" 1002 tc_field _ _ _ = panic "tc_field: Impossible Match" 1003 -- due to #15884 1004 1005 1006 find_field_ty :: Name -> FieldLabelString -> TcM TcType 1007 find_field_ty sel lbl 1008 = case [ty | (fl, ty) <- field_tys, flSelector fl == sel] of 1009 1010 -- No matching field; chances are this field label comes from some 1011 -- other record type (or maybe none). If this happens, just fail, 1012 -- otherwise we get crashes later (#8570), and similar: 1013 -- f (R { foo = (a,b) }) = a+b 1014 -- If foo isn't one of R's fields, we don't want to crash when 1015 -- typechecking the "a+b". 1016 [] -> failWith (badFieldCon con_like lbl) 1017 1018 -- The normal case, when the field comes from the right constructor 1019 (pat_ty : extras) -> do 1020 traceTc "find_field" (ppr pat_ty <+> ppr extras) 1021 ASSERT( null extras ) (return pat_ty) 1022 1023 field_tys :: [(FieldLabel, TcType)] 1024 field_tys = zip (conLikeFieldLabels con_like) arg_tys 1025 -- Don't use zipEqual! If the constructor isn't really a record, then 1026 -- dataConFieldLabels will be empty (and each field in the pattern 1027 -- will generate an error below). 1028 1029tcConArg :: Checker (LPat GhcRn, TcSigmaType) (LPat GhcTc) 1030tcConArg (arg_pat, arg_ty) penv thing_inside 1031 = tc_lpat arg_pat (mkCheckExpType arg_ty) penv thing_inside 1032 1033addDataConStupidTheta :: DataCon -> [TcType] -> TcM () 1034-- Instantiate the "stupid theta" of the data con, and throw 1035-- the constraints into the constraint set 1036addDataConStupidTheta data_con inst_tys 1037 | null stupid_theta = return () 1038 | otherwise = instStupidTheta origin inst_theta 1039 where 1040 origin = OccurrenceOf (dataConName data_con) 1041 -- The origin should always report "occurrence of C" 1042 -- even when C occurs in a pattern 1043 stupid_theta = dataConStupidTheta data_con 1044 univ_tvs = dataConUnivTyVars data_con 1045 tenv = zipTvSubst univ_tvs (takeList univ_tvs inst_tys) 1046 -- NB: inst_tys can be longer than the univ tyvars 1047 -- because the constructor might have existentials 1048 inst_theta = substTheta tenv stupid_theta 1049 1050{- 1051Note [Arrows and patterns] 1052~~~~~~~~~~~~~~~~~~~~~~~~~~ 1053(Oct 07) Arrow notation has the odd property that it involves 1054"holes in the scope". For example: 1055 expr :: Arrow a => a () Int 1056 expr = proc (y,z) -> do 1057 x <- term -< y 1058 expr' -< x 1059 1060Here the 'proc (y,z)' binding scopes over the arrow tails but not the 1061arrow body (e.g 'term'). As things stand (bogusly) all the 1062constraints from the proc body are gathered together, so constraints 1063from 'term' will be seen by the tcPat for (y,z). But we must *not* 1064bind constraints from 'term' here, because the desugarer will not make 1065these bindings scope over 'term'. 1066 1067The Right Thing is not to confuse these constraints together. But for 1068now the Easy Thing is to ensure that we do not have existential or 1069GADT constraints in a 'proc', and to short-cut the constraint 1070simplification for such vanilla patterns so that it binds no 1071constraints. Hence the 'fast path' in tcConPat; but it's also a good 1072plan for ordinary vanilla patterns to bypass the constraint 1073simplification step. 1074 1075************************************************************************ 1076* * 1077 Note [Pattern coercions] 1078* * 1079************************************************************************ 1080 1081In principle, these program would be reasonable: 1082 1083 f :: (forall a. a->a) -> Int 1084 f (x :: Int->Int) = x 3 1085 1086 g :: (forall a. [a]) -> Bool 1087 g [] = True 1088 1089In both cases, the function type signature restricts what arguments can be passed 1090in a call (to polymorphic ones). The pattern type signature then instantiates this 1091type. For example, in the first case, (forall a. a->a) <= Int -> Int, and we 1092generate the translated term 1093 f = \x' :: (forall a. a->a). let x = x' Int in x 3 1094 1095From a type-system point of view, this is perfectly fine, but it's *very* seldom useful. 1096And it requires a significant amount of code to implement, because we need to decorate 1097the translated pattern with coercion functions (generated from the subsumption check 1098by tcSub). 1099 1100So for now I'm just insisting on type *equality* in patterns. No subsumption. 1101 1102Old notes about desugaring, at a time when pattern coercions were handled: 1103 1104A SigPat is a type coercion and must be handled one at at time. We can't 1105combine them unless the type of the pattern inside is identical, and we don't 1106bother to check for that. For example: 1107 1108 data T = T1 Int | T2 Bool 1109 f :: (forall a. a -> a) -> T -> t 1110 f (g::Int->Int) (T1 i) = T1 (g i) 1111 f (g::Bool->Bool) (T2 b) = T2 (g b) 1112 1113We desugar this as follows: 1114 1115 f = \ g::(forall a. a->a) t::T -> 1116 let gi = g Int 1117 in case t of { T1 i -> T1 (gi i) 1118 other -> 1119 let gb = g Bool 1120 in case t of { T2 b -> T2 (gb b) 1121 other -> fail }} 1122 1123Note that we do not treat the first column of patterns as a 1124column of variables, because the coerced variables (gi, gb) 1125would be of different types. So we get rather grotty code. 1126But I don't think this is a common case, and if it was we could 1127doubtless improve it. 1128 1129Meanwhile, the strategy is: 1130 * treat each SigPat coercion (always non-identity coercions) 1131 as a separate block 1132 * deal with the stuff inside, and then wrap a binding round 1133 the result to bind the new variable (gi, gb, etc) 1134 1135 1136************************************************************************ 1137* * 1138\subsection{Errors and contexts} 1139* * 1140************************************************************************ 1141 1142Note [Existential check] 1143~~~~~~~~~~~~~~~~~~~~~~~~ 1144Lazy patterns can't bind existentials. They arise in two ways: 1145 * Let bindings let { C a b = e } in b 1146 * Twiddle patterns f ~(C a b) = e 1147The pe_lazy field of PatEnv says whether we are inside a lazy 1148pattern (perhaps deeply) 1149 1150See also Note [Typechecking pattern bindings] in TcBinds 1151-} 1152 1153maybeWrapPatCtxt :: Pat GhcRn -> (TcM a -> TcM b) -> TcM a -> TcM b 1154-- Not all patterns are worth pushing a context 1155maybeWrapPatCtxt pat tcm thing_inside 1156 | not (worth_wrapping pat) = tcm thing_inside 1157 | otherwise = addErrCtxt msg $ tcm $ popErrCtxt thing_inside 1158 -- Remember to pop before doing thing_inside 1159 where 1160 worth_wrapping (VarPat {}) = False 1161 worth_wrapping (ParPat {}) = False 1162 worth_wrapping (AsPat {}) = False 1163 worth_wrapping _ = True 1164 msg = hang (text "In the pattern:") 2 (ppr pat) 1165 1166----------------------------------------------- 1167checkExistentials :: [TyVar] -- existentials 1168 -> [Type] -- argument types 1169 -> PatEnv -> TcM () 1170 -- See Note [Existential check]] 1171 -- See Note [Arrows and patterns] 1172checkExistentials ex_tvs tys _ 1173 | all (not . (`elemVarSet` tyCoVarsOfTypes tys)) ex_tvs = return () 1174checkExistentials _ _ (PE { pe_ctxt = LetPat {}}) = return () 1175checkExistentials _ _ (PE { pe_ctxt = LamPat ProcExpr }) = failWithTc existentialProcPat 1176checkExistentials _ _ (PE { pe_lazy = True }) = failWithTc existentialLazyPat 1177checkExistentials _ _ _ = return () 1178 1179existentialLazyPat :: SDoc 1180existentialLazyPat 1181 = hang (text "An existential or GADT data constructor cannot be used") 1182 2 (text "inside a lazy (~) pattern") 1183 1184existentialProcPat :: SDoc 1185existentialProcPat 1186 = text "Proc patterns cannot use existential or GADT data constructors" 1187 1188badFieldCon :: ConLike -> FieldLabelString -> SDoc 1189badFieldCon con field 1190 = hsep [text "Constructor" <+> quotes (ppr con), 1191 text "does not have field", quotes (ppr field)] 1192 1193polyPatSig :: TcType -> SDoc 1194polyPatSig sig_ty 1195 = hang (text "Illegal polymorphic type signature in pattern:") 1196 2 (ppr sig_ty) 1197