compiler/typecheck/TcPat.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[TcPat]{Typechecking patterns}
   5
   6 \begin{code}
   7 module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit,
   8                addDataConStupidTheta, badFieldCon, polyPatSig ) where
   9
  10 #include "HsVersions.h"
  11
  12 import {-# SOURCE #-}   TcExpr( tcSyntaxOp )
  13 import HsSyn            ( Pat(..), LPat, HsConDetails(..), HsLit(..),
  14                           HsOverLit(..), HsExpr(..), OutPat, ExprCoFn(..),
  15                           mkCoPat, idCoercion,
  16                           LHsBinds, emptyLHsBinds, isEmptyLHsBinds,
  17                           collectPatsBinders, nlHsLit )
  18 import TcHsSyn          ( TcId, hsLitType )
  19 import TcRnMonad
  20 import Inst             ( InstOrigin(..), shortCutFracLit, shortCutIntLit,
  21                           newDictBndrs, instToId, instStupidTheta, isHsVar
  22                         )
  23 import Id               ( Id, idType, mkLocalId )
  24 import CoreFVs          ( idFreeTyVars )
  25 import Name             ( Name, mkSystemVarName )
  26 import TcSimplify       ( tcSimplifyCheck, bindInstsOfLocalFuns )
  27 import TcEnv            ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
  28                           tcLookupClass, tcLookupDataCon, refineEnvironment,
  29                           tcLookupField, tcMetaTy )
  30 import TcMType          ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars,
  31                           newCoVars, zonkTcType, tcInstTyVars )
  32 import TcType           ( TcType, TcTyVar, TcSigmaType, TcRhoType, BoxyType,
  33                           SkolemInfo(PatSkol),
  34                           BoxySigmaType, BoxyRhoType, argTypeKind, typeKind,
  35                           pprSkolTvBinding, isRigidTy, tcTyVarsOfTypes,
  36                           zipTopTvSubst, isArgTypeKind, isUnboxedTupleType,
  37                           mkTyVarTys, mkClassPred, isOverloadedTy, substEqSpec,
  38                           mkFunTy, mkFunTys, tidyOpenType, tidyOpenTypes )
  39 import VarSet           ( elemVarSet )
  40 import {- Kind parts of -}
  41        Type             ( liftedTypeKind )
  42 import TcUnify          ( boxySplitTyConApp, boxySplitListTy, unBox,
  43                           zapToMonotype, boxyUnify, boxyUnifyList,
  44                           checkSigTyVarsWrt, unifyType )
  45 import TcHsType         ( UserTypeCtxt(..), tcPatSig )
  46 import TysWiredIn       ( boolTy, parrTyCon, tupleTyCon )
  47 import Type             ( Type, mkTyConApp, substTys, substTheta )
  48 import StaticFlags      ( opt_IrrefutableTuples )
  49 import TyCon            ( TyCon, FieldLabel, tyConFamInst_maybe,
  50                           tyConFamilyCoercion_maybe, tyConTyVars, isNewTyCon )
  51 import DataCon          ( DataCon, dataConTyCon, dataConFullSig, dataConName,
  52                           dataConFieldLabels, dataConSourceArity,
  53                           dataConStupidTheta, dataConUnivTyVars )
  54 import PrelNames        ( integralClassName, fromIntegerName, integerTyConName,
  55                           fromRationalName, rationalTyConName )
  56 import BasicTypes       ( isBoxed )
  57 import SrcLoc           ( Located(..), SrcSpan, noLoc )
  58 import ErrUtils         ( Message )
  59 import Util             ( zipEqual )
  60 import Maybes           ( MaybeErr(..) )
  61 import Outputable
  62 import FastString
  63 \end{code}
  64
  65
  66 %************************************************************************
  67 %*                                                                      *
  68                 External interface
  69 %*                                                                      *
  70 %************************************************************************
  71
  72 \begin{code}
  73 tcLetPat :: (Name -> Maybe TcRhoType)
  74          -> LPat Name -> BoxySigmaType
  75          -> TcM a
  76          -> TcM (LPat TcId, a)
  77 tcLetPat sig_fn pat pat_ty thing_inside
  78   = do  { let init_state = PS { pat_ctxt = LetPat sig_fn,
  79                                 pat_reft = emptyRefinement }
  80         ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)
  81
  82         -- Don't know how to deal with pattern-bound existentials yet
  83         ; checkTc (null ex_tvs) (existentialExplode pat)
  84
  85         ; return (pat', res) }
  86
  87 -----------------
  88 tcLamPats :: [LPat Name]                                -- Patterns,
  89           -> [BoxySigmaType]                            --   and their types
  90           -> BoxyRhoType                                -- Result type,
  91           -> ((Refinement, BoxyRhoType) -> TcM a)       --   and the checker for the body
  92           -> TcM ([LPat TcId], a)
  93
  94 -- This is the externally-callable wrapper function
  95 -- Typecheck the patterns, extend the environment to bind the variables,
  96 -- do the thing inside, use any existentially-bound dictionaries to
  97 -- discharge parts of the returning LIE, and deal with pattern type
  98 -- signatures
  99
 100 --   1. Initialise the PatState
 101 --   2. Check the patterns
 102 --   3. Apply the refinement to the environment and result type
 103 --   4. Check the body
 104 --   5. Check that no existentials escape
 105
 106 tcLamPats pats tys res_ty thing_inside
 107   = tc_lam_pats (zipEqual "tcLamPats" pats tys)
 108                 (emptyRefinement, res_ty) thing_inside
 109
 110 tcLamPat :: LPat Name -> BoxySigmaType
 111          -> (Refinement,BoxyRhoType)            -- Result type
 112          -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
 113          -> TcM (LPat TcId, a)
 114 tcLamPat pat pat_ty res_ty thing_inside
 115   = do  { ([pat'],thing) <- tc_lam_pats [(pat, pat_ty)] res_ty thing_inside
 116         ; return (pat', thing) }
 117
 118 -----------------
 119 tc_lam_pats :: [(LPat Name,BoxySigmaType)]
 120             -> (Refinement,BoxyRhoType)                 -- Result type
 121             -> ((Refinement,BoxyRhoType) -> TcM a)      -- Checker for body, given its result type
 122             -> TcM ([LPat TcId], a)
 123 tc_lam_pats pat_ty_prs (reft, res_ty) thing_inside
 124   =  do { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft }
 125
 126         ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
 127                                   refineEnvironment (pat_reft pstate') $
 128                                   thing_inside (pat_reft pstate', res_ty)
 129
 130         ; let tys = map snd pat_ty_prs
 131         ; tcCheckExistentialPat pats' ex_tvs tys res_ty
 132
 133         ; returnM (pats', res) }
 134
 135
 136 -----------------
 137 tcCheckExistentialPat :: [LPat TcId]            -- Patterns (just for error message)
 138                       -> [TcTyVar]              -- Existentially quantified tyvars bound by pattern
 139                       -> [BoxySigmaType]        -- Types of the patterns
 140                       -> BoxyRhoType            -- Type of the body of the match
 141                                                 -- Tyvars in either of these must not escape
 142                       -> TcM ()
 143 -- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat
 144 -- For example, we must reject this program:
 145 --      data C = forall a. C (a -> Int)
 146 --      f (C g) x = g x
 147 -- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
 148
 149 tcCheckExistentialPat pats [] pat_tys body_ty
 150   = return ()   -- Short cut for case when there are no existentials
 151
 152 tcCheckExistentialPat pats ex_tvs pat_tys body_ty
 153   = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys body_ty)   $
 154     checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
 155
 156 data PatState = PS {
 157         pat_ctxt :: PatCtxt,
 158         pat_reft :: Refinement  -- Binds rigid TcTyVars to their refinements
 159   }
 160
 161 data PatCtxt
 162   = LamPat
 163   | LetPat (Name -> Maybe TcRhoType)    -- Used for let(rec) bindings
 164
 165 patSigCtxt :: PatState -> UserTypeCtxt
 166 patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
 167 patSigCtxt other                        = LamPatSigCtxt
 168 \end{code}
 169
 170
 171
 172 %************************************************************************
 173 %*                                                                      *
 174                 Binders
 175 %*                                                                      *
 176 %************************************************************************
 177
 178 \begin{code}
 179 tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
 180 tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
 181   = do  { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
 182                 -- We have an undecorated binder, so we do rule ABS1,
 183                 -- by unboxing the boxy type, forcing any un-filled-in
 184                 -- boxes to become monotypes
 185                 -- NB that pat_ty' can still be a polytype:
 186                 --      data T = MkT (forall a. a->a)
 187                 --      f t = case t of { MkT g -> ... }
 188                 -- Here, the 'g' must get type (forall a. a->a) from the
 189                 -- MkT context
 190         ; return (mkLocalId bndr_name pat_ty') }
 191
 192 tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
 193   | Just mono_ty <- lookup_sig bndr_name
 194   = do  { mono_name <- newLocalName bndr_name
 195         ; boxyUnify mono_ty pat_ty
 196         ; return (mkLocalId mono_name mono_ty) }
 197
 198   | otherwise
 199   = do  { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
 200         ; mono_name <- newLocalName bndr_name
 201         ; return (mkLocalId mono_name pat_ty') }
 202
 203
 204 -------------------
 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) }
 209   | otherwise
 210   = do  { (res, lie) <- getLIE thing_inside
 211         ; binds <- bindInstsOfLocalFuns lie [id]
 212         ; return (res, binds) }
 213
 214 -------------------
 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
 218 unBoxArgType :: BoxyType -> SDoc -> TcM TcType
 219 -- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind;
 220 -- that is, it can't be an unboxed tuple.  For example,
 221 --      case (f x) of r -> ...
 222 -- should fail if 'f' returns an unboxed tuple.
 223 unBoxArgType ty pp_this
 224   = do  { ty' <- unBox ty       -- Returns a zonked type
 225
 226         -- Neither conditional is strictly necesssary (the unify alone will do)
 227         -- but they improve error messages, and allocate fewer tyvars
 228         ; if isUnboxedTupleType ty' then
 229                 failWithTc msg
 230           else if isArgTypeKind (typeKind ty') then
 231                 return ty'
 232           else do       -- OpenTypeKind, so constrain it
 233         { ty2 <- newFlexiTyVarTy argTypeKind
 234         ; unifyType ty' ty2
 235         ; return ty' }}
 236   where
 237     msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple")
 238 \end{code}
 239
 240
 241 %************************************************************************
 242 %*                                                                      *
 243                 The main worker functions
 244 %*                                                                      *
 245 %************************************************************************
 246
 247 Note [Nesting]
 248 ~~~~~~~~~~~~~~
 249 tcPat takes a "thing inside" over which the patter scopes.  This is partly
 250 so that tcPat can extend the environment for the thing_inside, but also
 251 so that constraints arising in the thing_inside can be discharged by the
 252 pattern.
 253
 254 This does not work so well for the ErrCtxt carried by the monad: we don't
 255 want the error-context for the pattern to scope over the RHS.
 256 Hence the getErrCtxt/setErrCtxt stuff in tc_lpats.
 257
 258 \begin{code}
 259 --------------------
 260 type Checker inp out =  forall r.
 261                           inp
 262                        -> PatState
 263                        -> (PatState -> TcM r)
 264                        -> TcM (out, [TcTyVar], r)
 265
 266 tcMultiple :: Checker inp out -> Checker [inp] [out]
 267 tcMultiple tc_pat args pstate thing_inside
 268   = do  { err_ctxt <- getErrCtxt
 269         ; let loop pstate []
 270                 = do { res <- thing_inside pstate
 271                      ; return ([], [], res) }
 272
 273               loop pstate (arg:args)
 274                 = do { (p', p_tvs, (ps', ps_tvs, res))
 275                                 <- tc_pat arg pstate $ \ pstate' ->
 276                                    setErrCtxt err_ctxt $
 277                                    loop pstate' args
 278                 -- setErrCtxt: restore context before doing the next pattern
 279                 -- See note [Nesting] above
 280
 281                      ; return (p':ps', p_tvs ++ ps_tvs, res) }
 282
 283         ; loop pstate args }
 284
 285 --------------------
 286 tc_lpat_pr :: (LPat Name, BoxySigmaType)
 287            -> PatState
 288            -> (PatState -> TcM a)
 289            -> TcM (LPat TcId, [TcTyVar], a)
 290 tc_lpat_pr (pat, ty) = tc_lpat pat ty
 291
 292 tc_lpat :: LPat Name
 293         -> BoxySigmaType
 294         -> PatState
 295         -> (PatState -> TcM a)
 296         -> TcM (LPat TcId, [TcTyVar], a)
 297 tc_lpat (L span pat) pat_ty pstate thing_inside
 298   = setSrcSpan span               $
 299     maybeAddErrCtxt (patCtxt pat) $
 300     do  { let (coercion, pat_ty') = refineType (pat_reft pstate) pat_ty
 301                 -- Make sure the result type reflects the current refinement
 302                 -- We must do this here, so that it correctly ``sees'' all
 303                 -- the refinements to the left.  Example:
 304                 -- Suppose C :: forall a. T a -> a -> Foo
 305                 -- Pattern      C a p1 True
 306                 -- So p1 might refine 'a' to True, and the True
 307                 -- pattern had better see it.
 308
 309         ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
 310         ; return (mkCoPat coercion (L span pat') pat_ty, tvs, res) }
 311
 312 --------------------
 313 tc_pat  :: PatState
 314         -> Pat Name -> BoxySigmaType    -- Fully refined result type
 315         -> (PatState -> TcM a)  -- Thing inside
 316         -> TcM (Pat TcId,       -- Translated pattern
 317                 [TcTyVar],      -- Existential binders
 318                 a)              -- Result of thing inside
 319
 320 tc_pat pstate (VarPat name) pat_ty thing_inside
 321   = do  { id <- tcPatBndr pstate name pat_ty
 322         ; (res, binds) <- bindInstsOfPatId id $
 323                           tcExtendIdEnv1 name id $
 324                           (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
 325                            >> thing_inside pstate)
 326         ; let pat' | isEmptyLHsBinds binds = VarPat id
 327                    | otherwise             = VarPatOut id binds
 328         ; return (pat', [], res) }
 329
 330 tc_pat pstate (ParPat pat) pat_ty thing_inside
 331   = do  { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
 332         ; return (ParPat pat', tvs, res) }
 333
 334 tc_pat pstate (BangPat pat) pat_ty thing_inside
 335   = do  { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
 336         ; return (BangPat pat', tvs, res) }
 337
 338 -- There's a wrinkle with irrefutable patterns, namely that we
 339 -- must not propagate type refinement from them.  For example
 340 --      data T a where { T1 :: Int -> T Int; ... }
 341 --      f :: T a -> Int -> a
 342 --      f ~(T1 i) y = y
 343 -- It's obviously not sound to refine a to Int in the right
 344 -- hand side, because the arugment might not match T1 at all!
 345 --
 346 -- Nor should a lazy pattern bind any existential type variables
 347 -- because they won't be in scope when we do the desugaring
 348 tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
 349   = do  { (pat', pat_tvs, res) <- tc_lpat pat pat_ty pstate $ \ _ ->
 350                                   thing_inside pstate
 351                                         -- Ignore refined pstate',
 352                                         -- revert to pstate
 353         -- Check no existentials
 354         ; if (null pat_tvs) then return ()
 355           else lazyPatErr lpat pat_tvs
 356
 357         -- Check that the pattern has a lifted type
 358         ; pat_tv <- newBoxyTyVar liftedTypeKind
 359         ; boxyUnify pat_ty (mkTyVarTy pat_tv)
 360
 361         ; return (LazyPat pat', [], res) }
 362
 363 tc_pat pstate (WildPat _) pat_ty thing_inside
 364   = do  { pat_ty' <- unBoxWildCardType pat_ty   -- Make sure it's filled in with monotypes
 365         ; res <- thing_inside pstate
 366         ; return (WildPat pat_ty', [], res) }
 367
 368 tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
 369   = do  { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
 370         ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
 371                               tc_lpat pat (idType bndr_id) pstate thing_inside
 372             -- NB: if we do inference on:
 373             --          \ (y@(x::forall a. a->a)) = e
 374             -- we'll fail.  The as-pattern infers a monotype for 'y', which then
 375             -- fails to unify with the polymorphic type for 'x'.  This could
 376             -- perhaps be fixed, but only with a bit more work.
 377             --
 378             -- If you fix it, don't forget the bindInstsOfPatIds!
 379         ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
 380
 381 -- Type signatures in patterns
 382 -- See Note [Pattern coercions] below
 383 tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
 384   = do  { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
 385         ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
 386                               tc_lpat pat inner_ty pstate thing_inside
 387         ; return (SigPatOut pat' inner_ty, tvs, res) }
 388
 389 tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
 390   = failWithTc (badTypePat pat)
 391
 392 ------------------------
 393 -- Lists, tuples, arrays
 394 tc_pat pstate (ListPat pats _) pat_ty thing_inside
 395   = do  { elt_ty <- boxySplitListTy pat_ty
 396         ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
 397                                                 pats pstate thing_inside
 398         ; return (ListPat pats' elt_ty, pats_tvs, res) }
 399
 400 tc_pat pstate (PArrPat pats _) pat_ty thing_inside
 401   = do  { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty
 402         ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
 403                                                 pats pstate thing_inside
 404         ; ifM (null pats) (zapToMonotype pat_ty)        -- c.f. ExplicitPArr in TcExpr
 405         ; return (PArrPat pats' elt_ty, pats_tvs, res) }
 406
 407 tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
 408   = do  { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
 409         ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
 410                                                pstate thing_inside
 411
 412         -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
 413         -- so that we can experiment with lazy tuple-matching.
 414         -- This is a pretty odd place to make the switch, but
 415         -- it was easy to do.
 416         ; let unmangled_result = TuplePat pats' boxity pat_ty
 417               possibly_mangled_result
 418                 | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
 419                 | otherwise                               = unmangled_result
 420
 421         ; ASSERT( length arg_tys == length pats )       -- Syntactically enforced
 422           return (possibly_mangled_result, pats_tvs, res) }
 423
 424 ------------------------
 425 -- Data constructors
 426 tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
 427   = do  { data_con <- tcLookupDataCon con_name
 428         ; let tycon = dataConTyCon data_con
 429         ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
 430
 431 ------------------------
 432 -- Literal patterns
 433 tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
 434   = do  { boxyUnify (hsLitType simple_lit) pat_ty
 435         ; res <- thing_inside pstate
 436         ; returnM (LitPat simple_lit, [], res) }
 437
 438 ------------------------
 439 -- Overloaded patterns: n, and n+k
 440 tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside
 441   = do  { let orig = LiteralOrigin over_lit
 442         ; lit'    <- tcOverloadedLit orig over_lit pat_ty
 443         ; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
 444         ; mb_neg' <- case mb_neg of
 445                         Nothing  -> return Nothing      -- Positive literal
 446                         Just neg ->     -- Negative literal
 447                                         -- The 'negate' is re-mappable syntax
 448                             do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
 449                                ; return (Just neg') }
 450         ; res <- thing_inside pstate
 451         ; returnM (NPat lit' mb_neg' eq' pat_ty, [], res) }
 452
 453 tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
 454   = do  { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
 455         ; let pat_ty' = idType bndr_id
 456               orig    = LiteralOrigin lit
 457         ; lit' <- tcOverloadedLit orig lit pat_ty'
 458
 459         -- The '>=' and '-' parts are re-mappable syntax
 460         ; ge'    <- tcSyntaxOp orig ge    (mkFunTys [pat_ty', pat_ty'] boolTy)
 461         ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
 462
 463         -- The Report says that n+k patterns must be in Integral
 464         -- We may not want this when using re-mappable syntax, though (ToDo?)
 465         ; icls <- tcLookupClass integralClassName
 466         ; instStupidTheta orig [mkClassPred icls [pat_ty']]
 467
 468         ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
 469         ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
 470
 471 tc_pat _ _other_pat _ _ = panic "tc_pat"        -- DictPat, ConPatOut, SigPatOut, VarPatOut
 472 \end{code}
 473
 474
 475 %************************************************************************
 476 %*                                                                      *
 477         Most of the work for constructors is here
 478         (the rest is in the ConPatIn case of tc_pat)
 479 %*                                                                      *
 480 %************************************************************************
 481
 482 [Pattern matching indexed data types]
 483 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 484 Consider the following declarations:
 485
 486   data family Map k :: * -> *
 487   data instance Map (a, b) v = MapPair (Map a (Pair b v))
 488
 489 and a case expression
 490
 491   case x :: Map (Int, c) w of MapPair m -> ...
 492
 493 As explained by [Wrappers for data instance tycons] in MkIds.lhs, the
 494 worker/wrapper types for MapPair are
 495
 496   $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
 497   $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
 498
 499 So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
 500 :R123Map, which means the straight use of boxySplitTyConApp would give a type
 501 error.  Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
 502 boxySplitTyConApp with the family tycon Map instead, which gives us the family
 503 type list {(Int, c), w}.  To get the correct split for :R123Map, we need to
 504 unify the family type list {(Int, c), w} with the instance types {(a, b), v}
 505 (provided by tyConFamInst_maybe together with the family tycon).  This
 506 unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
 507 the split arguments for the representation tycon :R123Map as {Int, c, w}
 508
 509 In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
 510
 511   Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
 512
 513 moving between representation and family type into account.  To produce type
 514 correct Core, this coercion needs to be used to case the type of the scrutinee
 515 from the family to the representation type.  This is achieved by
 516 unwrapFamInstScrutinee using a CoPat around the result pattern.
 517
 518 Now it might appear seem as if we could have used the existing GADT type
 519 refinement infrastructure of refineAlt and friends instead of the explicit
 520 unification and CoPat generation.  However, that would be wrong.  Why?  The
 521 whole point of GADT refinement is that the refinement is local to the case
 522 alternative.  In contrast, the substitution generated by the unification of
 523 the family type list and instance types needs to be propagated to the outside.
 524 Imagine that in the above example, the type of the scrutinee would have been
 525 (Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
 526 substitution [x -> (a, b), v -> w].  In contrast to GADT matching, the
 527 instantiation of x with (a, b) must be global; ie, it must be valid in *all*
 528 alternatives of the case expression, whereas in the GADT case it might vary
 529 between alternatives.
 530
 531 In fact, if we have a data instance declaration defining a GADT, eq_spec will
 532 be non-empty and we will get a mixture of global instantiations and local
 533 refinement from a single match.  This neatly reflects that, as soon as we
 534 have constrained the type of the scrutinee to the required type index, all
 535 further type refinement is local to the alternative.
 536
 537 \begin{code}
 538 --      Running example:
 539 -- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
 540 --       with scrutinee of type (T ty)
 541
 542 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
 543          -> BoxySigmaType       -- Type of the pattern
 544          -> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
 545          -> TcM (Pat TcId, [TcTyVar], a)
 546 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 547   = do  { span <- getSrcSpanM   -- Span for the whole pattern
 548         ; let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys) = dataConFullSig data_con
 549               skol_info = PatSkol data_con span
 550               origin    = SigOrigin skol_info
 551
 552           -- Instantiate the constructor type variables [a->ty]
 553         ; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty
 554         ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
 555         ; let tenv     = zipTopTvSubst (univ_tvs ++ ex_tvs)
 556                                       (ctxt_res_tys ++ mkTyVarTys ex_tvs')
 557               eq_spec' = substEqSpec tenv eq_spec
 558               theta'   = substTheta  tenv theta
 559               arg_tys' = substTys    tenv arg_tys
 560
 561         ; co_vars <- newCoVars eq_spec' -- Make coercion variables
 562         ; pstate' <- refineAlt data_con pstate ex_tvs co_vars pat_ty
 563
 564         ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
 565                 tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
 566
 567         ; loc <- getInstLoc origin
 568         ; dicts <- newDictBndrs loc theta'
 569         ; dict_binds <- tcSimplifyCheck doc ex_tvs' dicts lie_req
 570
 571         ; addDataConStupidTheta origin data_con ctxt_res_tys
 572
 573         ; return
 574             (unwrapFamInstScrutinee tycon ctxt_res_tys $
 575                ConPatOut { pat_con = L con_span data_con,
 576                            pat_tvs = ex_tvs' ++ co_vars,
 577                            pat_dicts = map instToId dicts,
 578                            pat_binds = dict_binds,
 579                            pat_args = arg_pats', pat_ty = pat_ty },
 580              ex_tvs' ++ inner_tvs, res)
 581         }
 582   where
 583     doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
 584
 585     -- Split against the family tycon if the pattern constructor belongs to a
 586     -- representation tycon.
 587     --
 588     boxySplitTyConAppWithFamily tycon pat_ty =
 589       traceTc traceMsg >>
 590       case tyConFamInst_maybe tycon of
 591         Nothing                   -> boxySplitTyConApp tycon pat_ty
 592         Just (fam_tycon, instTys) ->
 593           do { scrutinee_arg_tys <- boxySplitTyConApp fam_tycon pat_ty
 594              ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
 595              ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
 596              ; return freshTvs
 597              }
 598       where
 599         traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
 600                          ppr tycon <+> ppr pat_ty
 601                        , text "  family instance:" <+>
 602                          ppr (tyConFamInst_maybe tycon)
 603                        ]
 604
 605     -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
 606     -- pattern if the tycon is an instance of a family.
 607     --
 608     unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id
 609     unwrapFamInstScrutinee tycon args pat
 610       | Just co_con <- tyConFamilyCoercion_maybe tycon
 611 --      , not (isNewTyCon tycon)       -- newtypes are explicitly unwrapped by
 612                                      -- the desugarer
 613           -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
 614           --     coercion is not the identity; mkCoPat is inconvenient as it
 615           --     wants a located pattern.
 616       = CoPat (ExprCoFn $ mkTyConApp co_con args)       -- co fam ty to repr ty
 617               (pat {pat_ty = mkTyConApp tycon args})    -- representation type
 618               pat_ty                                    -- family inst type
 619       | otherwise
 620       = pat
 621
 622
 623 tcConArgs :: DataCon -> [TcSigmaType]
 624           -> Checker (HsConDetails Name (LPat Name))
 625                      (HsConDetails Id (LPat Id))
 626
 627 tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
 628   = do  { checkTc (con_arity == no_of_args)     -- Check correct arity
 629                   (arityErr "Constructor" data_con con_arity no_of_args)
 630         ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
 631         ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
 632                                               pstate thing_inside
 633         ; return (PrefixCon arg_pats', tvs, res) }
 634   where
 635     con_arity  = dataConSourceArity data_con
 636     no_of_args = length arg_pats
 637
 638 tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside
 639   = do  { checkTc (con_arity == 2)      -- Check correct arity
 640                   (arityErr "Constructor" data_con con_arity 2)
 641         ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
 642                                               pstate thing_inside
 643         ; return (InfixCon p1' p2', tvs, res) }
 644   where
 645     con_arity  = dataConSourceArity data_con
 646
 647 tcConArgs data_con arg_tys (RecCon rpats) pstate thing_inside
 648   = do  { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
 649         ; return (RecCon rpats', tvs, res) }
 650   where
 651     tc_field :: Checker (Located Name, LPat Name) (Located TcId, LPat TcId)
 652     tc_field (field_lbl, pat) pstate thing_inside
 653       = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
 654            ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
 655            ; return ((sel_id, pat'), tvs, res) }
 656
 657     find_field_ty :: FieldLabel -> TcM (Id, TcType)
 658     find_field_ty field_lbl
 659         = case [ty | (f,ty) <- field_tys, f == field_lbl] of
 660
 661                 -- No matching field; chances are this field label comes from some
 662                 -- other record type (or maybe none).  As well as reporting an
 663                 -- error we still want to typecheck the pattern, principally to
 664                 -- make sure that all the variables it binds are put into the
 665                 -- environment, else the type checker crashes later:
 666                 --      f (R { foo = (a,b) }) = a+b
 667                 -- If foo isn't one of R's fields, we don't want to crash when
 668                 -- typechecking the "a+b".
 669            [] -> do { addErrTc (badFieldCon data_con field_lbl)
 670                     ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
 671                     ; return (error "Bogus selector Id", bogus_ty) }
 672
 673                 -- The normal case, when the field comes from the right constructor
 674            (pat_ty : extras) ->
 675                 ASSERT( null extras )
 676                 do { sel_id <- tcLookupField field_lbl
 677                    ; return (sel_id, pat_ty) }
 678
 679     field_tys :: [(FieldLabel, TcType)]
 680     field_tys = zip (dataConFieldLabels data_con) arg_tys
 681         -- Don't use zipEqual! If the constructor isn't really a record, then
 682         -- dataConFieldLabels will be empty (and each field in the pattern
 683         -- will generate an error below).
 684
 685 tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
 686 tcConArg (arg_pat, arg_ty) pstate thing_inside
 687   = tc_lpat arg_pat arg_ty pstate thing_inside
 688         -- NB: the tc_lpat will refine pat_ty if necessary
 689         --     based on the current pstate, which may include
 690         --     refinements from peer argument patterns to the left
 691 \end{code}
 692
 693 \begin{code}
 694 addDataConStupidTheta :: InstOrigin -> DataCon -> [TcType] -> TcM ()
 695 -- Instantiate the "stupid theta" of the data con, and throw
 696 -- the constraints into the constraint set
 697 addDataConStupidTheta origin data_con inst_tys
 698   | null stupid_theta = return ()
 699   | otherwise         = instStupidTheta origin inst_theta
 700   where
 701     stupid_theta = dataConStupidTheta data_con
 702     tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
 703     inst_theta = substTheta tenv stupid_theta
 704 \end{code}
 705
 706
 707 %************************************************************************
 708 %*                                                                      *
 709                 Type refinement
 710 %*                                                                      *
 711 %************************************************************************
 712
 713 \begin{code}
 714 refineAlt :: DataCon            -- For tracing only
 715           -> PatState
 716           -> [TcTyVar]          -- Existentials
 717           -> [CoVar]            -- Equational constraints
 718           -> BoxySigmaType      -- Pattern type
 719           -> TcM PatState
 720
 721 refineAlt con pstate ex_tvs [] pat_ty
 722   = return pstate       -- Common case: no equational constraints
 723
 724 refineAlt con pstate ex_tvs co_vars pat_ty
 725   | not (isRigidTy pat_ty)
 726   = failWithTc (nonRigidMatch con)
 727         -- We are matching against a GADT constructor with non-trivial
 728         -- constraints, but pattern type is wobbly.  For now we fail.
 729         -- We can make sense of this, however:
 730         -- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a
 731         --      (\x -> case x of { MkT v -> v })
 732         -- We can infer that x must have type T [c], for some wobbly 'c'
 733         -- and translate to
 734         --      (\(x::T [c]) -> case x of
 735         --                        MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g
 736         -- To implement this, we'd first instantiate the equational
 737         -- constraints with *wobbly* type variables for the existentials;
 738         -- then unify these constraints to make pat_ty the right shape;
 739         -- then proceed exactly as in the rigid case
 740
 741   | otherwise   -- In the rigid case, we perform type refinement
 742   = case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
 743             Failed msg     -> failWithTc (inaccessibleAlt msg) ;
 744             Succeeded reft -> do { traceTc trace_msg
 745                                  ; return (pstate { pat_reft = reft }) }
 746                     -- DO NOT refine the envt right away, because we
 747                     -- might be inside a lazy pattern.  Instead, refine pstate
 748                 where
 749
 750                     trace_msg = text "refineAlt:match" <+> ppr con <+> ppr reft
 751         }
 752 \end{code}
 753
 754
 755 %************************************************************************
 756 %*                                                                      *
 757                 Overloaded literals
 758 %*                                                                      *
 759 %************************************************************************
 760
 761 In tcOverloadedLit we convert directly to an Int or Integer if we
 762 know that's what we want.  This may save some time, by not
 763 temporarily generating overloaded literals, but it won't catch all
 764 cases (the rest are caught in lookupInst).
 765
 766 \begin{code}
 767 tcOverloadedLit :: InstOrigin
 768                  -> HsOverLit Name
 769                  -> BoxyRhoType
 770                  -> TcM (HsOverLit TcId)
 771 tcOverloadedLit orig lit@(HsIntegral i fi) res_ty
 772   | not (fi `isHsVar` fromIntegerName)  -- Do not generate a LitInst for rebindable syntax.
 773         -- Reason: If we do, tcSimplify will call lookupInst, which
 774         --         will call tcSyntaxName, which does unification,
 775         --         which tcSimplify doesn't like
 776         -- ToDo: noLoc sadness
 777   = do  { integer_ty <- tcMetaTy integerTyConName
 778         ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
 779         ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) }
 780
 781   | Just expr <- shortCutIntLit i res_ty
 782   = return (HsIntegral i expr)
 783
 784   | otherwise
 785   = do  { expr <- newLitInst orig lit res_ty
 786         ; return (HsIntegral i expr) }
 787
 788 tcOverloadedLit orig lit@(HsFractional r fr) res_ty
 789   | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case
 790   = do  { rat_ty <- tcMetaTy rationalTyConName
 791         ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
 792                 -- Overloaded literals must have liftedTypeKind, because
 793                 -- we're instantiating an overloaded function here,
 794                 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
 795                 -- However this'll be picked up by tcSyntaxOp if necessary
 796         ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty)))) }
 797
 798   | Just expr <- shortCutFracLit r res_ty
 799   = return (HsFractional r expr)
 800
 801   | otherwise
 802   = do  { expr <- newLitInst orig lit res_ty
 803         ; return (HsFractional r expr) }
 804
 805 newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
 806 newLitInst orig lit res_ty      -- Make a LitInst
 807   = do  { loc <- getInstLoc orig
 808         ; res_tau <- zapToMonotype res_ty
 809         ; new_uniq <- newUnique
 810         ; let   lit_nm   = mkSystemVarName new_uniq FSLIT("lit")
 811                 lit_inst = LitInst lit_nm lit res_tau loc
 812         ; extendLIE lit_inst
 813         ; return (HsVar (instToId lit_inst)) }
 814 \end{code}
 815
 816
 817 %************************************************************************
 818 %*                                                                      *
 819                 Note [Pattern coercions]
 820 %*                                                                      *
 821 %************************************************************************
 822
 823 In principle, these program would be reasonable:
 824
 825         f :: (forall a. a->a) -> Int
 826         f (x :: Int->Int) = x 3
 827
 828         g :: (forall a. [a]) -> Bool
 829         g [] = True
 830
 831 In both cases, the function type signature restricts what arguments can be passed
 832 in a call (to polymorphic ones).  The pattern type signature then instantiates this
 833 type.  For example, in the first case,  (forall a. a->a) <= Int -> Int, and we
 834 generate the translated term
 835         f = \x' :: (forall a. a->a).  let x = x' Int in x 3
 836
 837 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
 838 And it requires a significant amount of code to implement, becuase we need to decorate
 839 the translated pattern with coercion functions (generated from the subsumption check
 840 by tcSub).
 841
 842 So for now I'm just insisting on type *equality* in patterns.  No subsumption.
 843
 844 Old notes about desugaring, at a time when pattern coercions were handled:
 845
 846 A SigPat is a type coercion and must be handled one at at time.  We can't
 847 combine them unless the type of the pattern inside is identical, and we don't
 848 bother to check for that.  For example:
 849
 850         data T = T1 Int | T2 Bool
 851         f :: (forall a. a -> a) -> T -> t
 852         f (g::Int->Int)   (T1 i) = T1 (g i)
 853         f (g::Bool->Bool) (T2 b) = T2 (g b)
 854
 855 We desugar this as follows:
 856
 857         f = \ g::(forall a. a->a) t::T ->
 858             let gi = g Int
 859             in case t of { T1 i -> T1 (gi i)
 860                            other ->
 861             let gb = g Bool
 862             in case t of { T2 b -> T2 (gb b)
 863                            other -> fail }}
 864
 865 Note that we do not treat the first column of patterns as a
 866 column of variables, because the coerced variables (gi, gb)
 867 would be of different types.  So we get rather grotty code.
 868 But I don't think this is a common case, and if it was we could
 869 doubtless improve it.
 870
 871 Meanwhile, the strategy is:
 872         * treat each SigPat coercion (always non-identity coercions)
 873                 as a separate block
 874         * deal with the stuff inside, and then wrap a binding round
 875                 the result to bind the new variable (gi, gb, etc)
 876
 877
 878 %************************************************************************
 879 %*                                                                      *
 880 \subsection{Errors and contexts}
 881 %*                                                                      *
 882 %************************************************************************
 883
 884 \begin{code}
 885 patCtxt :: Pat Name -> Maybe Message    -- Not all patterns are worth pushing a context
 886 patCtxt (VarPat _)  = Nothing
 887 patCtxt (ParPat _)  = Nothing
 888 patCtxt (AsPat _ _) = Nothing
 889 patCtxt pat         = Just (hang (ptext SLIT("In the pattern:"))
 890                                4 (ppr pat))
 891
 892 -----------------------------------------------
 893
 894 existentialExplode pat
 895   = hang (vcat [text "My brain just exploded.",
 896                 text "I can't handle pattern bindings for existentially-quantified constructors.",
 897                 text "In the binding group for"])
 898         4 (ppr pat)
 899
 900 sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env
 901   = do  { pat_tys' <- mapM zonkTcType pat_tys
 902         ; body_ty' <- zonkTcType body_ty
 903         ; let (env1,  tidy_tys)    = tidyOpenTypes tidy_env (map idType show_ids)
 904               (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
 905               (env3, tidy_body_ty) = tidyOpenType  env2 body_ty'
 906         ; return (env3,
 907                  sep [ptext SLIT("When checking an existential match that binds"),
 908                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
 909                       ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
 910                       ptext SLIT("The body has type:") <+> ppr tidy_body_ty
 911                 ]) }
 912   where
 913     show_ids = filter is_interesting bound_ids
 914     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
 915
 916     ppr_id id ty = ppr id <+> dcolon <+> ppr ty
 917         -- Don't zonk the types so we get the separate, un-unified versions
 918
 919 badFieldCon :: DataCon -> Name -> SDoc
 920 badFieldCon con field
 921   = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
 922           ptext SLIT("does not have field"), quotes (ppr field)]
 923
 924 polyPatSig :: TcType -> SDoc
 925 polyPatSig sig_ty
 926   = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
 927          4 (ppr sig_ty)
 928
 929 badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
 930
 931 lazyPatErr pat tvs
 932   = failWithTc $
 933     hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
 934        2 (vcat (map pprSkolTvBinding tvs))
 935
 936 nonRigidMatch con
 937   =  hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
 938         2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
 939
 940 inaccessibleAlt msg
 941   = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
 942 \end{code}