TcPat.lhs 40.7 KB
Newer Older
1
%
2
% (c) The University of Glasgow 2006
3
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
%
5
6

TcPat: Typechecking patterns
7
8

\begin{code}
9
module TcPat ( tcLetPat, tcPat, tcPats, tcOverloadedLit,
10
	       addDataConStupidTheta, badFieldCon, polyPatSig ) where
11

12
#include "HsVersions.h"
13

14
import {-# SOURCE #-}	TcExpr( tcSyntaxOp, tcInferRho)
15
16
17

import HsSyn
import TcHsSyn
18
import TcRnMonad
19
20
21
22
23
24
25
26
27
import Inst
import Id
import Var
import CoreFVs
import Name
import TcSimplify
import TcEnv
import TcMType
import TcType
Ian Lynagh's avatar
Ian Lynagh committed
28
import VarEnv
29
30
31
32
33
import VarSet
import TcUnify
import TcHsType
import TysWiredIn
import Type
34
import Coercion
35
36
37
38
39
40
41
42
43
import StaticFlags
import TyCon
import DataCon
import PrelNames
import BasicTypes hiding (SuccessFlag(..))
import SrcLoc
import ErrUtils
import Util
import Maybes
sof's avatar
sof committed
44
import Outputable
45
import FastString
46
import Monad
47
\end{code}
48

49
50
51

%************************************************************************
%*									*
52
		External interface
53
54
55
56
%*									*
%************************************************************************

\begin{code}
57
58
tcLetPat :: (Name -> Maybe TcRhoType)
      	 -> LPat Name -> BoxySigmaType 
59
     	 -> TcM a
60
61
      	 -> TcM (LPat TcId, a)
tcLetPat sig_fn pat pat_ty thing_inside
62
  = do	{ let init_state = PS { pat_ctxt = LetPat sig_fn,
63
				pat_eqs  = False }
64
65
	; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state 
                                   (\ _ -> thing_inside)
66
67
68
69
70
71
72

	-- Don't know how to deal with pattern-bound existentials yet
	; checkTc (null ex_tvs) (existentialExplode pat)

	; return (pat', res) }

-----------------
73
74
75
76
77
78
tcPats :: HsMatchContext Name
       -> [LPat Name]		 -- Patterns,
       -> [BoxySigmaType]	 --   and their types
       -> BoxyRhoType 		 -- Result type,
       -> (BoxyRhoType -> TcM a) --   and the checker for the body
       -> TcM ([LPat TcId], a)
79
80
81
82
83
84
85
86
87

-- This is the externally-callable wrapper function
-- Typecheck the patterns, extend the environment to bind the variables,
-- do the thing inside, use any existentially-bound dictionaries to 
-- discharge parts of the returning LIE, and deal with pattern type
-- signatures

--   1. Initialise the PatState
--   2. Check the patterns
88
89
--   3. Check the body
--   4. Check that no existentials escape
90

91
92
tcPats ctxt pats tys res_ty thing_inside
  = tc_lam_pats (APat ctxt) (zipEqual "tcLamPats" pats tys)
93
	        res_ty thing_inside
94

95
96
97
98
99
100
101
tcPat :: HsMatchContext Name
      -> LPat Name -> BoxySigmaType 
      -> BoxyRhoType             -- Result type
      -> (BoxyRhoType -> TcM a)  -- Checker for body, given
                                 -- its result type
      -> TcM (LPat TcId, a)
tcPat ctxt = tc_lam_pat (APat ctxt)
102

Ian Lynagh's avatar
Ian Lynagh committed
103
104
tc_lam_pat :: PatCtxt -> LPat Name -> BoxySigmaType -> BoxyRhoType
           -> (BoxyRhoType -> TcM a) -> TcM (LPat TcId, a)
105
106
tc_lam_pat ctxt pat pat_ty res_ty thing_inside
  = do	{ ([pat'],thing) <- tc_lam_pats ctxt [(pat, pat_ty)] res_ty thing_inside
107
	; return (pat', thing) }
108

109
-----------------
110
111
tc_lam_pats :: PatCtxt
	    -> [(LPat Name,BoxySigmaType)]
112
113
       	    -> BoxyRhoType            -- Result type
       	    -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
114
       	    -> TcM ([LPat TcId], a)
115
116
tc_lam_pats ctxt pat_ty_prs res_ty thing_inside 
  =  do	{ let init_state = PS { pat_ctxt = ctxt, pat_eqs = False }
117

118
119
120
	; (pats', ex_tvs, res) <- do { traceTc (text "tc_lam_pats" <+> (ppr pat_ty_prs $$ ppr res_ty)) 
				  ; tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
				    if (pat_eqs pstate' && (not $ isRigidTy res_ty))
121
				     then nonRigidResult ctxt res_ty
122
	     			     else thing_inside res_ty }
123

124
125
	; let tys = map snd pat_ty_prs
	; tcCheckExistentialPat pats' ex_tvs tys res_ty
126

127
	; return (pats', res) }
128
129
130


-----------------
131
tcCheckExistentialPat :: [LPat TcId]		-- Patterns (just for error message)
132
133
134
135
136
137
138
139
140
141
142
		      -> [TcTyVar]		-- Existentially quantified tyvars bound by pattern
		      -> [BoxySigmaType]	-- Types of the patterns
		      -> BoxyRhoType		-- Type of the body of the match
		      				-- Tyvars in either of these must not escape
		      -> TcM ()
-- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat
-- For example, we must reject this program:
--	data C = forall a. C (a -> Int) 
-- 	f (C g) x = g x
-- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).

Ian Lynagh's avatar
Ian Lynagh committed
143
tcCheckExistentialPat _ [] _ _
144
145
  = return ()	-- Short cut for case when there are no existentials

146
tcCheckExistentialPat pats ex_tvs pat_tys body_ty
147
  = addErrCtxtM (sigPatCtxt pats ex_tvs pat_tys body_ty)	$
148
149
150
151
    checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs

data PatState = PS {
	pat_ctxt :: PatCtxt,
152
153
154
	pat_eqs  :: Bool        -- <=> there are any equational constraints 
				-- Used at the end to say whether the result
				-- type must be rigid
155
156
157
  }

data PatCtxt 
158
  = APat (HsMatchContext Name)
159
160
  | LetPat (Name -> Maybe TcRhoType)	-- Used for let(rec) bindings

161
162
163
164
notProcPat :: PatCtxt -> Bool
notProcPat (APat ProcExpr) = False
notProcPat _	  	   = True

165
166
patSigCtxt :: PatState -> UserTypeCtxt
patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
Ian Lynagh's avatar
Ian Lynagh committed
167
patSigCtxt _                            = LamPatSigCtxt
168
169
170
\end{code}


171

172
173
%************************************************************************
%*									*
174
		Binders
175
176
177
%*									*
%************************************************************************

178
\begin{code}
179
180
181
182
183
tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
  | Just mono_ty <- lookup_sig bndr_name
  = do	{ mono_name <- newLocalName bndr_name
	; boxyUnify mono_ty pat_ty
184
	; return (Id.mkLocalId mono_name mono_ty) }
185
186

  | otherwise
187
  = do	{ pat_ty' <- unBoxPatBndrType pat_ty bndr_name
188
	; mono_name <- newLocalName bndr_name
189
	; return (Id.mkLocalId mono_name pat_ty') }
190

191
192
193
194
195
196
197
198
199
200
201
202
tcPatBndr (PS { pat_ctxt = _lam_or_proc }) bndr_name pat_ty
  = do	{ pat_ty' <- unBoxPatBndrType pat_ty bndr_name
		-- We have an undecorated binder, so we do rule ABS1,
		-- by unboxing the boxy type, forcing any un-filled-in
		-- boxes to become monotypes
		-- NB that pat_ty' can still be a polytype:
		-- 	data T = MkT (forall a. a->a)
		-- 	f t = case t of { MkT g -> ... }
		-- Here, the 'g' must get type (forall a. a->a) from the
		-- MkT context
	; return (Id.mkLocalId bndr_name pat_ty') }

203
204
205
206
207
208
209
210
211
212

-------------------
bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
bindInstsOfPatId id thing_inside
  | not (isOverloadedTy (idType id))
  = do { res <- thing_inside; return (res, emptyLHsBinds) }
  | otherwise
  = do	{ (res, lie) <- getLIE thing_inside
	; binds <- bindInstsOfLocalFuns lie [id]
	; return (res, binds) }
213
214

-------------------
Ian Lynagh's avatar
Ian Lynagh committed
215
unBoxPatBndrType :: BoxyType -> Name -> TcM TcType
216
unBoxPatBndrType  ty name = unBoxArgType ty (ptext (sLit "The variable") <+> quotes (ppr name))
Ian Lynagh's avatar
Ian Lynagh committed
217
218

unBoxWildCardType :: BoxyType -> TcM TcType
219
unBoxWildCardType ty      = unBoxArgType ty (ptext (sLit "A wild-card pattern"))
Ian Lynagh's avatar
Ian Lynagh committed
220
221

unBoxViewPatType :: BoxyType -> Pat Name -> TcM TcType
222
unBoxViewPatType  ty pat  = unBoxArgType ty (ptext (sLit "The view pattern") <+> ppr pat)
223
224
225
226
227
228
229
230
231
232
233
234
235

unBoxArgType :: BoxyType -> SDoc -> TcM TcType
-- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind; 
-- that is, it can't be an unboxed tuple.  For example, 
--	case (f x) of r -> ...
-- should fail if 'f' returns an unboxed tuple.
unBoxArgType ty pp_this
  = do	{ ty' <- unBox ty	-- Returns a zonked type

	-- Neither conditional is strictly necesssary (the unify alone will do)
	-- but they improve error messages, and allocate fewer tyvars
	; if isUnboxedTupleType ty' then
		failWithTc msg
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
236
	  else if isSubArgTypeKind (typeKind ty') then
237
238
239
240
241
242
		return ty'
	  else do 	-- OpenTypeKind, so constrain it
	{ ty2 <- newFlexiTyVarTy argTypeKind
	; unifyType ty' ty2
	; return ty' }}
  where
243
    msg = pp_this <+> ptext (sLit "cannot be bound to an unboxed tuple")
244
245
\end{code}

246

247
248
%************************************************************************
%*									*
249
		The main worker functions
250
251
252
%*									*
%************************************************************************

253
254
Note [Nesting]
~~~~~~~~~~~~~~
lennart@augustsson.net's avatar
lennart@augustsson.net committed
255
tcPat takes a "thing inside" over which the pattern scopes.  This is partly
256
257
258
259
260
261
262
263
so that tcPat can extend the environment for the thing_inside, but also 
so that constraints arising in the thing_inside can be discharged by the
pattern.

This does not work so well for the ErrCtxt carried by the monad: we don't
want the error-context for the pattern to scope over the RHS. 
Hence the getErrCtxt/setErrCtxt stuff in tc_lpats.

264
\begin{code}
265
--------------------
266
267
268
269
270
271
272
273
type Checker inp out =  forall r.
			  inp
		       -> PatState
		       -> (PatState -> TcM r)
		       -> TcM (out, [TcTyVar], r)

tcMultiple :: Checker inp out -> Checker [inp] [out]
tcMultiple tc_pat args pstate thing_inside
274
  = do	{ err_ctxt <- getErrCtxt
275
	; let loop pstate []
276
277
278
		= do { res <- thing_inside pstate
		     ; return ([], [], res) }

279
	      loop pstate (arg:args)
280
		= do { (p', p_tvs, (ps', ps_tvs, res)) 
281
				<- tc_pat arg pstate $ \ pstate' ->
282
				   setErrCtxt err_ctxt $
283
				   loop pstate' args
284
285
286
287
288
		-- setErrCtxt: restore context before doing the next pattern
		-- See note [Nesting] above
				
		     ; return (p':ps', p_tvs ++ ps_tvs, res) }

289
	; loop pstate args }
290
291

--------------------
292
293
294
295
296
297
298
299
300
301
302
303
tc_lpat_pr :: (LPat Name, BoxySigmaType)
	   -> PatState
	   -> (PatState -> TcM a)
	   -> TcM (LPat TcId, [TcTyVar], a)
tc_lpat_pr (pat, ty) = tc_lpat pat ty

tc_lpat :: LPat Name 
	-> BoxySigmaType
	-> PatState
	-> (PatState -> TcM a)
	-> TcM (LPat TcId, [TcTyVar], a)
tc_lpat (L span pat) pat_ty pstate thing_inside
304
305
  = setSrcSpan span		  $
    maybeAddErrCtxt (patCtxt pat) $
306
307
    do	{ (pat', tvs, res) <- tc_pat pstate pat pat_ty thing_inside
	; return (L span pat', tvs, res) }
308
309
310

--------------------
tc_pat	:: PatState
311
312
313
314
315
316
        -> Pat Name 
        -> BoxySigmaType	-- Fully refined result type
        -> (PatState -> TcM a)	-- Thing inside
        -> TcM (Pat TcId, 	-- Translated pattern
                [TcTyVar], 	-- Existential binders
                a)		-- Result of thing inside
317

318
319
tc_pat pstate (VarPat name) pat_ty thing_inside
  = do	{ id <- tcPatBndr pstate name pat_ty
320
321
322
	; (res, binds) <- bindInstsOfPatId id $
			  tcExtendIdEnv1 name id $
			  (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
323
			   >> thing_inside pstate)
324
325
326
327
	; let pat' | isEmptyLHsBinds binds = VarPat id
		   | otherwise		   = VarPatOut id binds
	; return (pat', [], res) }

328
tc_pat pstate (ParPat pat) pat_ty thing_inside
329
  = do	{ (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
330
331
	; return (ParPat pat', tvs, res) }

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
332
tc_pat pstate (BangPat pat) pat_ty thing_inside
333
  = do	{ (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
334
335
	; return (BangPat pat', tvs, res) }

336
-- There's a wrinkle with irrefutable patterns, namely that we
337
338
339
340
341
342
343
344
345
-- must not propagate type refinement from them.  For example
--	data T a where { T1 :: Int -> T Int; ... }
--	f :: T a -> Int -> a
--	f ~(T1 i) y = y
-- It's obviously not sound to refine a to Int in the right
-- hand side, because the arugment might not match T1 at all!
--
-- Nor should a lazy pattern bind any existential type variables
-- because they won't be in scope when we do the desugaring
346
347
348
349
350
351
352
353
354
355
356
357
--
-- Note [Hopping the LIE in lazy patterns]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- In a lazy pattern, we must *not* discharge constraints from the RHS
-- from dictionaries bound in the pattern.  E.g.
--	f ~(C x) = 3
-- We can't discharge the Num constraint from dictionaries bound by
-- the pattern C!  
--
-- So we have to make the constraints from thing_inside "hop around" 
-- the pattern.  Hence the getLLE and extendLIEs later.

358
tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
359
360
361
362
363
364
365
  = do	{ (pat', pat_tvs, (res,lie)) 
		<- tc_lpat pat pat_ty pstate $ \ _ ->
		   getLIE (thing_inside pstate)
		-- Ignore refined pstate', revert to pstate
	; extendLIEs lie
	-- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns]

366
	-- Check no existentials
367
368
	; if (null pat_tvs) then return ()
	  else lazyPatErr lpat pat_tvs
369
370
371
372
373

	-- Check that the pattern has a lifted type
	; pat_tv <- newBoxyTyVar liftedTypeKind
	; boxyUnify pat_ty (mkTyVarTy pat_tv)

374
375
	; return (LazyPat pat', [], res) }

376
377
378
tc_pat _ p@(QuasiQuotePat _) _ _
  = pprPanic "Should never see QuasiQuotePat in type checker" (ppr p)

379
tc_pat pstate (WildPat _) pat_ty thing_inside
380
  = do	{ pat_ty' <- unBoxWildCardType pat_ty	-- Make sure it's filled in with monotypes
381
	; res <- thing_inside pstate
382
383
	; return (WildPat pat_ty', [], res) }

384
385
tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
  = do	{ bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
386
	; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
387
			      tc_lpat pat (idType bndr_id) pstate thing_inside
388
389
390
391
392
393
394
395
396
	    -- NB: if we do inference on:
	    --		\ (y@(x::forall a. a->a)) = e
	    -- we'll fail.  The as-pattern infers a monotype for 'y', which then
	    -- fails to unify with the polymorphic type for 'x'.  This could 
	    -- perhaps be fixed, but only with a bit more work.
	    --
	    -- If you fix it, don't forget the bindInstsOfPatIds!
	; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }

397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
tc_pat pstate (orig@(ViewPat expr pat _)) overall_pat_ty thing_inside 
  = do	{ -- morally, expr must have type
         -- `forall a1...aN. OPT' -> B` 
         -- where overall_pat_ty is an instance of OPT'.
         -- Here, we infer a rho type for it,
         -- which replaces the leading foralls and constraints
         -- with fresh unification variables.
         (expr',expr'_inferred) <- tcInferRho expr
         -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty`
       ; let expr'_expected = \ pat_ty -> (mkFunTy overall_pat_ty pat_ty)
         -- tcSubExp: expected first, offered second
         -- returns coercion
         -- 
         -- NOTE: this forces pat_ty to be a monotype (because we use a unification 
         -- variable to find it).  this means that in an example like
         -- (view -> f)    where view :: _ -> forall b. b
         -- we will only be able to use view at one instantation in the
         -- rest of the view
415
416
417
	; (expr_coerc, pat_ty) <- tcInfer $ \ pat_ty -> 
		tcSubExp ViewPatOrigin (expr'_expected pat_ty) expr'_inferred

418
419
420
421
422
423
424
         -- pattern must have pat_ty
       ; (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
         -- this should get zonked later on, but we unBox it here
         -- so that we do the same checks as above
	; annotation_ty <- unBoxViewPatType overall_pat_ty orig        
	; return (ViewPat (mkLHsWrap expr_coerc expr') pat' annotation_ty, tvs, res) }

425
426
427
-- Type signatures in patterns
-- See Note [Pattern coercions] below
tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
428
429
430
431
  = do	{ (inner_ty, tv_binds, coi) <- tcPatSig (patSigCtxt pstate) sig_ty 
                                                                    pat_ty
        ; unless (isIdentityCoercion coi) $ 
            failWithTc (badSigPat pat_ty)
432
	; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
433
			      tc_lpat pat inner_ty pstate thing_inside
434
	; return (SigPatOut pat' inner_ty, tvs, res) }
435

Ian Lynagh's avatar
Ian Lynagh committed
436
tc_pat _ pat@(TypePat _) _ _
437
  = failWithTc (badTypePat pat)
438

439
440
------------------------
-- Lists, tuples, arrays
441
tc_pat pstate (ListPat pats _) pat_ty thing_inside
442
  = do	{ (elt_ty, coi) <- boxySplitListTy pat_ty
443
        ; let scoi = mkSymCoI coi
444
445
	; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
					 	pats pstate thing_inside
446
447
 	; return (mkCoPatCoI scoi (ListPat pats' elt_ty) pat_ty, pats_tvs, res) 
        }
448
449

tc_pat pstate (PArrPat pats _) pat_ty thing_inside
450
  = do	{ (elt_ty, coi) <- boxySplitPArrTy pat_ty
451
        ; let scoi = mkSymCoI coi
452
453
	; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
						pats pstate thing_inside 
454
	; when (null pats) (zapToMonotype pat_ty >> return ())  -- c.f. ExplicitPArr in TcExpr
455
456
	; return (mkCoPatCoI scoi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res)
        }
457

458
tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
459
460
  = do	{ let tc = tupleTyCon boxity (length pats)
        ; (arg_tys, coi) <- boxySplitTyConApp tc pat_ty
461
        ; let scoi = mkSymCoI coi
462
463
	; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
					       pstate thing_inside
464
465
466
467
468

	-- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
	-- so that we can experiment with lazy tuple-matching.
	-- This is a pretty odd place to make the switch, but
	-- it was easy to do.
469
470
471
	; let pat_ty'          = mkTyConApp tc arg_tys
                                     -- pat_ty /= pat_ty iff coi /= IdCo
              unmangled_result = TuplePat pats' boxity pat_ty'
472
	      possibly_mangled_result
473
474
475
	        | opt_IrrefutableTuples && 
                  isBoxed boxity            = LazyPat (noLoc unmangled_result)
	        | otherwise		    = unmangled_result
476

477
 	; ASSERT( length arg_tys == length pats )      -- Syntactically enforced
478
	  return (mkCoPatCoI scoi possibly_mangled_result pat_ty, pats_tvs, res)
479
        }
480
481
482

------------------------
-- Data constructors
Ian Lynagh's avatar
Ian Lynagh committed
483
tc_pat pstate (ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
484
485
  = do	{ data_con <- tcLookupDataCon con_name
	; let tycon = dataConTyCon data_con
486
	; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
487
488
489

------------------------
-- Literal patterns
490
tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
491
492
493
  = do	{ let lit_ty = hsLitType simple_lit
	; coi <- boxyUnify lit_ty pat_ty
			-- coi is of kind: lit_ty ~ pat_ty
494
	; res <- thing_inside pstate
495
496
497
			-- pattern coercions have to
			-- be of kind: pat_ty ~ lit_ty
			-- hence, sym coi
498
	; return (mkCoPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, 
499
                   [], res) }
500
501
502

------------------------
-- Overloaded patterns: n, and n+k
Ian Lynagh's avatar
Ian Lynagh committed
503
tc_pat pstate (NPat over_lit mb_neg eq) pat_ty thing_inside
504
505
506
  = do	{ let orig = LiteralOrigin over_lit
	; lit'    <- tcOverloadedLit orig over_lit pat_ty
	; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
507
508
	; mb_neg' <- case mb_neg of
			Nothing  -> return Nothing	-- Positive literal
509
510
			Just neg -> 	-- Negative literal
					-- The 'negate' is re-mappable syntax
511
 			    do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
512
			       ; return (Just neg') }
513
	; res <- thing_inside pstate
514
	; return (NPat lit' mb_neg' eq', [], res) }
515

Ian Lynagh's avatar
Ian Lynagh committed
516
tc_pat pstate (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
517
  = do	{ bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
518
 	; let pat_ty' = idType bndr_id
519
520
	      orig    = LiteralOrigin lit
	; lit' <- tcOverloadedLit orig lit pat_ty'
521

522
523
524
	-- The '>=' and '-' parts are re-mappable syntax
	; ge'    <- tcSyntaxOp orig ge    (mkFunTys [pat_ty', pat_ty'] boolTy)
	; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
525

526
527
	-- The Report says that n+k patterns must be in Integral
	-- We may not want this when using re-mappable syntax, though (ToDo?)
528
	; icls <- tcLookupClass integralClassName
529
	; instStupidTheta orig [mkClassPred icls [pat_ty']]	
530
    
531
	; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
532
	; return (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
533

534
tc_pat _ _other_pat _ _ = panic "tc_pat" 	-- ConPatOut, SigPatOut, VarPatOut
535
\end{code}
536

537

538
539
%************************************************************************
%*									*
540
541
	Most of the work for constructors is here
	(the rest is in the ConPatIn case of tc_pat)
542
543
%*									*
%************************************************************************
544

545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
[Pattern matching indexed data types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following declarations:

  data family Map k :: * -> *
  data instance Map (a, b) v = MapPair (Map a (Pair b v))

and a case expression

  case x :: Map (Int, c) w of MapPair m -> ...

As explained by [Wrappers for data instance tycons] in MkIds.lhs, the
worker/wrapper types for MapPair are

  $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
  $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v

So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
:R123Map, which means the straight use of boxySplitTyConApp would give a type
error.  Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
boxySplitTyConApp with the family tycon Map instead, which gives us the family
type list {(Int, c), w}.  To get the correct split for :R123Map, we need to
unify the family type list {(Int, c), w} with the instance types {(a, b), v}
(provided by tyConFamInst_maybe together with the family tycon).  This
unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
the split arguments for the representation tycon :R123Map as {Int, c, w}

In other words, boxySplitTyConAppWithFamily implicitly takes the coercion 

574
  Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
575
576
577
578
579
580

moving between representation and family type into account.  To produce type
correct Core, this coercion needs to be used to case the type of the scrutinee
from the family to the representation type.  This is achieved by
unwrapFamInstScrutinee using a CoPat around the result pattern.

581
Now it might appear seem as if we could have used the previous GADT type
582
583
584
585
586
587
588
589
590
591
592
593
refinement infrastructure of refineAlt and friends instead of the explicit
unification and CoPat generation.  However, that would be wrong.  Why?  The
whole point of GADT refinement is that the refinement is local to the case
alternative.  In contrast, the substitution generated by the unification of
the family type list and instance types needs to be propagated to the outside.
Imagine that in the above example, the type of the scrutinee would have been
(Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
substitution [x -> (a, b), v -> w].  In contrast to GADT matching, the
instantiation of x with (a, b) must be global; ie, it must be valid in *all*
alternatives of the case expression, whereas in the GADT case it might vary
between alternatives.

594
595
596
RIP GADT refinement: refinements have been replaced by the use of explicit
equality constraints that are used in conjunction with implication constraints
to express the local scope of GADT refinements.
597

598
\begin{code}
599
--	Running example:
600
-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
601
602
-- 	 with scrutinee of type (T ty)

603
604
tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon 
	 -> BoxySigmaType	-- Type of the pattern
605
	 -> HsConPatDetails Name -> (PatState -> TcM a)
606
	 -> TcM (Pat TcId, [TcTyVar], a)
607
tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
608
609
  = do	{ let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _)
                = dataConFullSig data_con
610
611
612
	      skol_info  = PatSkol data_con
	      origin     = SigOrigin skol_info
	      full_theta = eq_theta ++ dict_theta
613
614

	  -- Instantiate the constructor type variables [a->ty]
615
616
	  -- This may involve doing a family-instance coercion, and building a
	  -- wrapper 
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
617
618
	; (ctxt_res_tys, coi, unwrap_ty) <- boxySplitTyConAppWithFamily tycon 
                                                                        pat_ty
619
620
621
622
623
624
        ; let sym_coi = mkSymCoI coi  -- boxy split coercion oriented wrongly
	      pat_ty' = mkTyConApp tycon ctxt_res_tys
                                      -- pat_ty' /= pat_ty iff coi /= IdCo
              
              wrap_res_pat res_pat = mkCoPatCoI sym_coi uwScrut pat_ty
                where
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
625
626
                  uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys
                                                   unwrap_ty res_pat
627

628
629
630
	  -- Add the stupid theta
	; addDataConStupidTheta data_con ctxt_res_tys

631
632
633
	; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs	
                     -- Get location from monad, not from ex_tvs

634
	; let tenv     = zipTopTvSubst (univ_tvs ++ ex_tvs)
635
				       (ctxt_res_tys ++ mkTyVarTys ex_tvs')
636
637
638
	      arg_tys' = substTys tenv arg_tys

	; if null ex_tvs && null eq_spec && null full_theta
639
640
	  then do { -- The common case; no class bindings etc 
                    -- (see Note [Arrows and patterns])
641
		    (arg_pats', inner_tvs, res) <- tcConArgs data_con arg_tys' 
642
						    arg_pats pstate thing_inside
643
		  ; let res_pat = ConPatOut { pat_con = L con_span data_con, 
644
645
646
647
			            	      pat_tvs = [], pat_dicts = [], 
                                              pat_binds = emptyLHsBinds,
					      pat_args = arg_pats', 
                                              pat_ty = pat_ty' }
648

649
650
		    ; return (wrap_res_pat res_pat, inner_tvs, res) }

651
652
	  else do   -- The general case, with existential, and local equality 
                    -- constraints
653
	{ checkTc (notProcPat (pat_ctxt pstate))
654
		  (existentialProcPat data_con)
655
		  -- See Note [Arrows and patterns]
656
657
658
659
660
661
662

          -- Need to test for rigidity if *any* constraints in theta as class
          -- constraints may have superclass equality constraints.  However,
          -- we don't want to check for rigidity if we got here only because
          -- ex_tvs was non-null.
--        ; unless (null theta') $
          -- FIXME: AT THE MOMENT WE CHEAT!  We only perform the rigidity test
663
          --   if we explicitly or implicitly (by a GADT def) have equality 
664
          --   constraints.
665
666
667
668
669
670
671
672
        ; let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
	      theta'   = substTheta tenv (eq_preds ++ full_theta)
                           -- order is *important* as we generate the list of
                           -- dictionary binders from theta'
	      no_equalities = not (any isEqPred theta')
	      pstate' | no_equalities = pstate
		      | otherwise     = pstate { pat_eqs = True }

673
674
	; unless no_equalities $ checkTc (isRigidTy pat_ty) $
                                 nonRigidMatch (pat_ctxt pstate) data_con
675

676
	; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
677
		tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
678

679
680
	; loc <- getInstLoc origin
	; dicts <- newDictBndrs loc theta'
681
	; dict_binds <- tcSimplifyCheckPat loc ex_tvs' dicts lie_req
682

683
        ; let res_pat = ConPatOut { pat_con = L con_span data_con, 
684
			            pat_tvs = ex_tvs',
685
686
687
			            pat_dicts = map instToVar dicts, 
			            pat_binds = dict_binds,
			            pat_args = arg_pats', pat_ty = pat_ty' }
688
689
	; return (wrap_res_pat res_pat, ex_tvs' ++ inner_tvs, res)
	} }
690
  where
691
    -- Split against the family tycon if the pattern constructor 
692
    -- belongs to a family instance tycon.
693
    boxySplitTyConAppWithFamily tycon pat_ty =
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
694
      traceTc traceMsg >>
695
      case tyConFamInst_maybe tycon of
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
696
697
698
699
        Nothing                   -> 
          do { (scrutinee_arg_tys, coi1) <- boxySplitTyConApp tycon pat_ty
             ; return (scrutinee_arg_tys, coi1, pat_ty)
             }
700
	Just (fam_tycon, instTys) -> 
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
701
	  do { (scrutinee_arg_tys, coi1) <- boxySplitTyConApp fam_tycon pat_ty
702
	     ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
703
704
705
706
707
708
709
710
711
712
713
714
715
             ; let instTys' = substTys subst instTys
	     ; cois <- boxyUnifyList instTys' scrutinee_arg_tys
             ; let coi = if isIdentityCoercion coi1
                         then  -- pat_ty was splittable
                               -- => boxyUnifyList had real work to do
                           mkTyConAppCoI fam_tycon instTys' cois
                         else  -- pat_ty was not splittable
                               -- => scrutinee_arg_tys are fresh tvs and
                               --    boxyUnifyList just instantiated those
                           coi1
	     ; return (freshTvs, coi, mkTyConApp fam_tycon instTys')
                                      -- this is /= pat_ty 
                                      -- iff cois is non-trivial
716
	     }
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
717
718
719
720
721
722
      where
        traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
		         ppr tycon <+> ppr pat_ty
		       , text "  family instance:" <+> 
			 ppr (tyConFamInst_maybe tycon)
                       ]
723
724
725
726

    -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
    -- pattern if the tycon is an instance of a family.
    --
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
727
728
    unwrapFamInstScrutinee :: TyCon -> [Type] -> Type -> Pat Id -> Pat Id
    unwrapFamInstScrutinee tycon args unwrap_ty pat
729
      | Just co_con <- tyConFamilyCoercion_maybe tycon 
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
730
731
--      , not (isNewTyCon tycon)       -- newtypes are explicitly unwrapped by
				     -- the desugarer
732
733
734
          -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
          --	 coercion is not the identity; mkCoPat is inconvenient as it
          --	 wants a located pattern.
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
735
      = CoPat (WpCast $ mkTyConApp co_con args)       -- co fam ty to repr ty
736
	      (pat {pat_ty = mkTyConApp tycon args})    -- representation type
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
737
	      unwrap_ty					-- family inst type
738
739
740
      | otherwise
      = pat

741
tcConArgs :: DataCon -> [TcSigmaType]
742
	  -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
743

744
tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
745
746
  = do	{ checkTc (con_arity == no_of_args)	-- Check correct arity
		  (arityErr "Constructor" data_con con_arity no_of_args)
747
748
749
	; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
	; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
					      pstate thing_inside 
750
	; return (PrefixCon arg_pats', tvs, res) }
751
752
753
  where
    con_arity  = dataConSourceArity data_con
    no_of_args = length arg_pats
754

755
tcConArgs data_con arg_tys (InfixCon p1 p2) pstate thing_inside
756
757
  = do	{ checkTc (con_arity == 2)	-- Check correct arity
	 	  (arityErr "Constructor" data_con con_arity 2)
758
	; let [arg_ty1,arg_ty2] = arg_tys	-- This can't fail after the arity check
759
760
	; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
					      pstate thing_inside
761
	; return (InfixCon p1' p2', tvs, res) }
762
763
764
  where
    con_arity  = dataConSourceArity data_con

765
tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
766
  = do	{ (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
767
	; return (RecCon (HsRecFields rpats' dd), tvs, res) }
768
  where
769
    tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
770
    tc_field (HsRecField field_lbl pat pun) pstate thing_inside
771
      = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
772
	   ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
773
	   ; return (HsRecField sel_id pat' pun, tvs, res) }
774

775
    find_field_ty :: FieldLabel -> TcM (Id, TcType)
776
777
    find_field_ty field_lbl
	= case [ty | (f,ty) <- field_tys, f == field_lbl] of
778
779
780
781
782
783
784
785
786

		-- No matching field; chances are this field label comes from some
		-- other record type (or maybe none).  As well as reporting an
		-- error we still want to typecheck the pattern, principally to
		-- make sure that all the variables it binds are put into the
		-- environment, else the type checker crashes later:
		--	f (R { foo = (a,b) }) = a+b
		-- If foo isn't one of R's fields, we don't want to crash when
		-- typechecking the "a+b".
787
	   [] -> do { addErrTc (badFieldCon data_con field_lbl)
788
		    ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
789
		    ; return (error "Bogus selector Id", bogus_ty) }
790
791
792
793

		-- The normal case, when the field comes from the right constructor
	   (pat_ty : extras) -> 
		ASSERT( null extras )
794
		do { sel_id <- tcLookupField field_lbl
795
		   ; return (sel_id, pat_ty) }
796

797
    field_tys :: [(FieldLabel, TcType)]
798
799
800
801
    field_tys = zip (dataConFieldLabels data_con) arg_tys
	-- Don't use zipEqual! If the constructor isn't really a record, then
	-- dataConFieldLabels will be empty (and each field in the pattern
	-- will generate an error below).
802
803
804
805

tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
tcConArg (arg_pat, arg_ty) pstate thing_inside
  = tc_lpat arg_pat arg_ty pstate thing_inside
806
807
\end{code}

808
\begin{code}
809
addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
810
811
-- Instantiate the "stupid theta" of the data con, and throw 
-- the constraints into the constraint set
812
addDataConStupidTheta data_con inst_tys
813
814
815
  | null stupid_theta = return ()
  | otherwise	      = instStupidTheta origin inst_theta
  where
816
817
818
    origin = OccurrenceOf (dataConName data_con)
	-- The origin should always report "occurrence of C"
	-- even when C occurs in a pattern
819
    stupid_theta = dataConStupidTheta data_con
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
820
821
822
    tenv = mkTopTvSubst (dataConUnivTyVars data_con `zip` inst_tys)
    	 -- NB: inst_tys can be longer than the univ tyvars
	 --     because the constructor might have existentials
823
824
825
    inst_theta = substTheta tenv stupid_theta
\end{code}

826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
Note [Arrows and patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~
(Oct 07) Arrow noation has the odd property that it involves "holes in the scope". 
For example:
  expr :: Arrow a => a () Int
  expr = proc (y,z) -> do
          x <- term -< y
          expr' -< x

Here the 'proc (y,z)' binding scopes over the arrow tails but not the
arrow body (e.g 'term').  As things stand (bogusly) all the
constraints from the proc body are gathered together, so constraints
from 'term' will be seen by the tcPat for (y,z).  But we must *not*
bind constraints from 'term' here, becuase the desugarer will not make
these bindings scope over 'term'.

The Right Thing is not to confuse these constraints together. But for
now the Easy Thing is to ensure that we do not have existential or
GADT constraints in a 'proc', and to short-cut the constraint
simplification for such vanilla patterns so that it binds no
constraints. Hence the 'fast path' in tcConPat; but it's also a good
plan for ordinary vanilla patterns to bypass the constraint
simplification step.

850

851
852
853
854
855
856
857
858
859
860
%************************************************************************
%*									*
		Overloaded literals
%*									*
%************************************************************************

In tcOverloadedLit we convert directly to an Int or Integer if we
know that's what we want.  This may save some time, by not
temporarily generating overloaded literals, but it won't catch all
cases (the rest are caught in lookupInst).
861
862

\begin{code}
863
864
865
866
tcOverloadedLit :: InstOrigin
		 -> HsOverLit Name
		 -> BoxyRhoType
		 -> TcM (HsOverLit TcId)
867
868
869
870
tcOverloadedLit orig lit@(OverLit { ol_val = val, ol_rebindable = rebindable
				  , ol_witness = meth_name }) res_ty
  | rebindable
	-- Do not generate a LitInst for rebindable syntax.  
871
872
873
874
	-- Reason: If we do, tcSimplify will call lookupInst, which
	--	   will call tcSyntaxName, which does unification, 
	--	   which tcSimplify doesn't like
	-- ToDo: noLoc sadness
875
876
877
  = do	{ hs_lit <- mkOverLit val
	; let lit_ty = hsLitType hs_lit
	; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
878
879
880
881
	 	-- Overloaded literals must have liftedTypeKind, because
	 	-- we're instantiating an overloaded function here,
	 	-- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
		-- However this'll be picked up by tcSyntaxOp if necessary
882
883
	; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
	; return (lit { ol_witness = witness, ol_type = res_ty }) }
884

885
886
  | Just expr <- shortCutLit val res_ty 
  = return (lit { ol_witness = expr, ol_type = res_ty })
887
888
889
890
891

  | otherwise
  = do 	{ loc <- getInstLoc orig
	; res_tau <- zapToMonotype res_ty
	; new_uniq <- newUnique
892
	; let	lit_nm   = mkSystemVarName new_uniq (fsLit "lit")
893
894
		lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit, 
				    tci_ty = res_tau, tci_loc = loc}
895
		witness = HsVar (instToId lit_inst)
896
	; extendLIE lit_inst
897
	; return (lit { ol_witness = witness, ol_type = res_ty }) }
898
899
\end{code}

900

901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
%************************************************************************
%*									*
		Note [Pattern coercions]
%*									*
%************************************************************************

In principle, these program would be reasonable:
	
	f :: (forall a. a->a) -> Int
	f (x :: Int->Int) = x 3

	g :: (forall a. [a]) -> Bool
	g [] = True

In both cases, the function type signature restricts what arguments can be passed
in a call (to polymorphic ones).  The pattern type signature then instantiates this
type.  For example, in the first case,  (forall a. a->a) <= Int -> Int, and we
generate the translated term
	f = \x' :: (forall a. a->a).  let x = x' Int in x 3

From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
And it requires a significant amount of code to implement, becuase we need to decorate
the translated pattern with coercion functions (generated from the subsumption check 
by tcSub).  

So for now I'm just insisting on type *equality* in patterns.  No subsumption. 

Old notes about desugaring, at a time when pattern coercions were handled:

A SigPat is a type coercion and must be handled one at at time.  We can't
combine them unless the type of the pattern inside is identical, and we don't
bother to check for that.  For example:

	data T = T1 Int | T2 Bool
	f :: (forall a. a -> a) -> T -> t
	f (g::Int->Int)   (T1 i) = T1 (g i)
	f (g::Bool->Bool) (T2 b) = T2 (g b)

We desugar this as follows:

	f = \ g::(forall a. a->a) t::T ->
	    let gi = g Int
	    in case t of { T1 i -> T1 (gi i)
			   other ->
	    let	gb = g Bool
	    in case t of { T2 b -> T2 (gb b)
			   other -> fail }}

Note that we do not treat the first column of patterns as a
column of variables, because the coerced variables (gi, gb)
would be of different types.  So we get rather grotty code.
But I don't think this is a common case, and if it was we could
doubtless improve it.

Meanwhile, the strategy is:
	* treat each SigPat coercion (always non-identity coercions)
		as a separate block
	* deal with the stuff inside, and then wrap a binding round
		the result to bind the new variable (gi, gb, etc)

961

962
963
964
965
966
967
%************************************************************************
%*									*
\subsection{Errors and contexts}
%*									*
%************************************************************************

968
\begin{code}
969
970
971
972
patCtxt :: Pat Name -> Maybe Message	-- Not all patterns are worth pushing a context
patCtxt (VarPat _)  = Nothing
patCtxt (ParPat _)  = Nothing
patCtxt (AsPat _ _) = Nothing
973
patCtxt pat 	    = Just (hang (ptext (sLit "In the pattern:")) 
974
			       4 (ppr pat))
975

976
977
-----------------------------------------------

Ian Lynagh's avatar
Ian Lynagh committed
978
existentialExplode :: LPat Name -> SDoc
979
existentialExplode pat
980
981
  = hang (vcat [text "My brain just exploded.",
	        text "I can't handle pattern bindings for existentially-quantified constructors.",
982
	        text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
983
		text "In the binding group for"])
984
	4 (ppr pat)
985

Ian Lynagh's avatar
Ian Lynagh committed
986
987
sigPatCtxt :: [LPat Var] -> [Var] -> [TcType] -> TcType -> TidyEnv
           -> TcM (TidyEnv, SDoc)
988
sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env 
989
990
991
992
993
994
  = do	{ pat_tys' <- mapM zonkTcType pat_tys
	; body_ty' <- zonkTcType body_ty
	; let (env1,  tidy_tys)    = tidyOpenTypes tidy_env (map idType show_ids)
	      (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
	      (env3, tidy_body_ty) = tidyOpenType  env2 body_ty'
	; return (env3,
995
		 sep [ptext (sLit "When checking an existential match that binds"),
996
		      nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
997
998
		      ptext (sLit "The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
		      ptext (sLit "The body has type:") <+> ppr tidy_body_ty
999
		]) }
1000
  where
1001
    bound_ids = collectPatsBinders pats
1002
    show_ids = filter is_interesting bound_ids
1003
    is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
1004
1005
1006
1007

    ppr_id id ty = ppr id <+> dcolon <+> ppr ty
	-- Don't zonk the types so we get the separate, un-unified versions

1008
badFieldCon :: DataCon -> Name -> SDoc
1009
badFieldCon con field
1010
1011
  = hsep [ptext (sLit "Constructor") <+> quotes (ppr con),
	  ptext (sLit "does not have field"), quotes (ppr field)]
1012
1013
1014

polyPatSig :: TcType -> SDoc
polyPatSig sig_ty
1015
  = hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
1016
       2 (ppr sig_ty)
1017

1018
1019
1020
1021
badSigPat :: TcType -> SDoc
badSigPat pat_ty = ptext (sLit "Pattern signature must exactly match:") <+> 
                   ppr pat_ty

Ian Lynagh's avatar
Ian Lynagh committed
1022
badTypePat :: Pat Name -> SDoc
1023
badTypePat pat = ptext (sLit "Illegal type pattern") <+> ppr pat
1024

1025
1026
existentialProcPat :: DataCon -> SDoc
existentialProcPat con
1027
1028
  = hang (ptext (sLit "Illegal constructor") <+> quotes (ppr con) <+> ptext (sLit "in a 'proc' pattern"))
       2 (ptext (sLit "Proc patterns cannot use existentials or GADTs"))
1029

Ian Lynagh's avatar
Ian Lynagh committed
1030
1031
lazyPatErr :: Pat name -> [TcTyVar] -> TcM ()
lazyPatErr _ tvs
1032
  = failWithTc $
1033
    hang (ptext (sLit "A lazy (~) pattern cannot bind existential type variables"))
1034
       2 (vcat (map pprSkolTvBinding tvs))
1035

1036
1037
nonRigidMatch :: PatCtxt -> DataCon -> SDoc
nonRigidMatch ctxt con
1038
  =  hang (ptext (sLit "GADT pattern match in non-rigid context for") <+> quotes (ppr con))
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
	2 (ptext (sLit "Probable solution: add a type signature for") <+> what ctxt)
  where
     what (APat (FunRhs f _)) = quotes (ppr f)
     what (APat CaseAlt)      = ptext (sLit "the scrutinee of the case expression")
     what (APat LambdaExpr )  = ptext (sLit "the lambda expression")
     what (APat (StmtCtxt _)) = ptext (sLit "the right hand side of a do/comprehension binding")
     what _other	      = ptext (sLit "something")

nonRigidResult :: PatCtxt -> Type -> TcM a
nonRigidResult ctxt res_ty
1049
1050
  = do	{ env0 <- tcInitTidyEnv
	; let (env1, res_ty') = tidyOpenType env0 res_ty
1051
	      msg = hang (ptext (sLit "GADT pattern match with non-rigid result type")
1052
				<+> quotes (ppr res_ty'))
1053
1054
		  	 2 (ptext (sLit "Solution: add a type signature for")
			   	  <+> what ctxt )
1055
	; failWithTcM (env1, msg) }
1056
1057
1058
1059
1060
1061
  where
     what (APat (FunRhs f _)) = quotes (ppr f)
     what (APat CaseAlt)      = ptext (sLit "the entire case expression")
     what (APat LambdaExpr)   = ptext (sLit "the lambda exression")
     what (APat (StmtCtxt _)) = ptext (sLit "the entire do/comprehension expression")
     what _other              = ptext (sLit "something")
1062
\end{code}