TcPat.lhs 36.8 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
{-# OPTIONS -w #-}
10
11
12
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and fix
-- any warnings in the module. See
Ian Lynagh's avatar
Ian Lynagh committed
13
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
14
15
-- for details

16
module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit,
17
	       addDataConStupidTheta, badFieldCon, polyPatSig ) where
18

19
#include "HsVersions.h"
20

21
import {-# SOURCE #-}	TcExpr( tcSyntaxOp )
22
23
24

import HsSyn
import TcHsSyn
25
import TcRnMonad
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
import Inst
import Id
import Var
import CoreFVs
import Name
import TcSimplify
import TcEnv
import TcMType
import TcType
import VarSet
import TcUnify
import TcHsType
import TysWiredIn
import TcGadt
import Type
41
import Coercion
42
43
44
import StaticFlags
import TyCon
import DataCon
45
import DynFlags
46
47
48
49
50
51
import PrelNames
import BasicTypes hiding (SuccessFlag(..))
import SrcLoc
import ErrUtils
import Util
import Maybes
sof's avatar
sof committed
52
import Outputable
53
import FastString
54
\end{code}
55

56
57
58

%************************************************************************
%*									*
59
		External interface
60
61
62
63
%*									*
%************************************************************************

\begin{code}
64
65
66
67
68
69
tcLetPat :: (Name -> Maybe TcRhoType)
      	 -> LPat Name -> BoxySigmaType 
      	 -> TcM a
      	 -> TcM (LPat TcId, a)
tcLetPat sig_fn pat pat_ty thing_inside
  = do	{ let init_state = PS { pat_ctxt = LetPat sig_fn, 
70
71
				pat_reft = emptyRefinement,
				pat_eqs  = False }
72
73
74
75
76
77
78
79
80
81
82
83
84
	; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)

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

	; return (pat', res) }

-----------------
tcLamPats :: [LPat Name]				-- Patterns,
	  -> [BoxySigmaType]				--   and their types
	  -> BoxyRhoType 				-- Result type,
	  -> ((Refinement, BoxyRhoType) -> TcM a)	--   and the checker for the body
	  -> TcM ([LPat TcId], a)
85
86
87
88
89
90
91
92
93

-- 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
94
--   3. Apply the refinement to the environment and result type
95
96
97
--   4. Check the body
--   5. Check that no existentials escape

98
99
100
101
102
103
104
105
106
107
108
tcLamPats pats tys res_ty thing_inside
  = tc_lam_pats (zipEqual "tcLamPats" pats tys)
	        (emptyRefinement, res_ty) thing_inside

tcLamPat :: LPat Name -> BoxySigmaType 
      	 -> (Refinement,BoxyRhoType)		-- Result type
      	 -> ((Refinement,BoxyRhoType) -> TcM a)	-- Checker for body, given its result type
      	 -> TcM (LPat TcId, a)
tcLamPat pat pat_ty res_ty thing_inside
  = do	{ ([pat'],thing) <- tc_lam_pats [(pat, pat_ty)] res_ty thing_inside
	; return (pat', thing) }
109

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

	; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
119
120
121
122
				  refineEnvironment (pat_reft pstate') (pat_eqs pstate') $
				  if (pat_eqs pstate' && (not $ isRigidTy res_ty))
				     then failWithTc (nonRigidResult res_ty)
	     			     else thing_inside (pat_reft pstate', res_ty)
123

124
125
	; let tys = map snd pat_ty_prs
	; tcCheckExistentialPat pats' ex_tvs tys res_ty
126
127
128
129
130

	; returnM (pats', res) }


-----------------
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).

143
tcCheckExistentialPat pats [] pat_tys body_ty
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_reft :: Refinement,	-- Binds rigid TcTyVars to their refinements
	pat_eqs  :: Bool        -- <=> there are GADT equational constraints 
				--     for refinement 
155
156
157
158
159
160
161
162
163
  }

data PatCtxt 
  = LamPat 
  | LetPat (Name -> Maybe TcRhoType)	-- Used for let(rec) bindings

patSigCtxt :: PatState -> UserTypeCtxt
patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
patSigCtxt other			= LamPatSigCtxt
164
165
166
\end{code}


167

168
169
%************************************************************************
%*									*
170
		Binders
171
172
173
%*									*
%************************************************************************

174
\begin{code}
175
176
tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
177
  = do	{ pat_ty' <- unBoxPatBndrType pat_ty bndr_name
178
179
180
181
		-- 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:
182
183
184
185
		-- 	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
186
	; return (Id.mkLocalId bndr_name pat_ty') }
187

188
189
190
191
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
192
	; return (Id.mkLocalId mono_name mono_ty) }
193
194

  | otherwise
195
  = do	{ pat_ty' <- unBoxPatBndrType pat_ty bndr_name
196
	; mono_name <- newLocalName bndr_name
197
	; return (Id.mkLocalId mono_name pat_ty') }
198
199
200
201
202
203
204
205
206
207
208


-------------------
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) }
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225

-------------------
unBoxPatBndrType  ty name = unBoxArgType ty (ptext SLIT("The variable") <+> quotes (ppr name))
unBoxWildCardType ty      = unBoxArgType ty (ptext SLIT("A wild-card pattern"))

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
226
	  else if isSubArgTypeKind (typeKind ty') then
227
228
229
230
231
232
233
		return ty'
	  else do 	-- OpenTypeKind, so constrain it
	{ ty2 <- newFlexiTyVarTy argTypeKind
	; unifyType ty' ty2
	; return ty' }}
  where
    msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple")
234
235
\end{code}

236

237
238
%************************************************************************
%*									*
239
		The main worker functions
240
241
242
%*									*
%************************************************************************

243
244
Note [Nesting]
~~~~~~~~~~~~~~
lennart@augustsson.net's avatar
lennart@augustsson.net committed
245
tcPat takes a "thing inside" over which the pattern scopes.  This is partly
246
247
248
249
250
251
252
253
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.

254
\begin{code}
255
--------------------
256
257
258
259
260
261
262
263
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
264
  = do	{ err_ctxt <- getErrCtxt
265
	; let loop pstate []
266
267
268
		= do { res <- thing_inside pstate
		     ; return ([], [], res) }

269
	      loop pstate (arg:args)
270
		= do { (p', p_tvs, (ps', ps_tvs, res)) 
271
				<- tc_pat arg pstate $ \ pstate' ->
272
				   setErrCtxt err_ctxt $
273
				   loop pstate' args
274
275
276
277
278
		-- setErrCtxt: restore context before doing the next pattern
		-- See note [Nesting] above
				
		     ; return (p':ps', p_tvs ++ ps_tvs, res) }

279
	; loop pstate args }
280
281

--------------------
282
283
284
285
286
287
288
289
290
291
292
293
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
294
295
  = setSrcSpan span		  $
    maybeAddErrCtxt (patCtxt pat) $
296
297
298
    do	{ let mb_reft = refineType (pat_reft pstate) pat_ty
	      pat_ty' = case mb_reft of { Just (_, ty') -> ty'; Nothing -> pat_ty }

299
		-- Make sure the result type reflects the current refinement
300
301
302
303
304
305
		-- We must do this here, so that it correctly ``sees'' all
		-- the refinements to the left.  Example:
		-- Suppose C :: forall a. T a -> a -> Foo
		-- Pattern	C a p1 True
		-- So p1 might refine 'a' to True, and the True 
		-- pattern had better see it.
306

307
	; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
308
309
310
311
	; let final_pat = case mb_reft of
				Nothing     -> pat'
				Just (co,_) -> CoPat (WpCo co) pat' pat_ty
	; return (L span final_pat, tvs, res) }
312
313
314
315
316

--------------------
tc_pat	:: PatState
	-> Pat Name -> BoxySigmaType	-- Fully refined result type
	-> (PatState -> TcM a)	-- Thing inside
317
	-> TcM (Pat TcId, 	-- Translated pattern
318
319
320
		[TcTyVar], 	-- Existential binders
		a)		-- Result of thing inside

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

331
tc_pat pstate (ParPat pat) pat_ty thing_inside
332
  = do	{ (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
333
334
	; return (ParPat pat', tvs, res) }

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

339
-- There's a wrinkle with irrefutable patterns, namely that we
340
341
342
343
344
345
346
347
348
-- 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
349
350
351
352
353
354
355
356
357
358
359
360
--
-- 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.

361
tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
362
363
364
365
366
367
368
  = 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]

369
	-- Check no existentials
370
371
	; if (null pat_tvs) then return ()
	  else lazyPatErr lpat pat_tvs
372
373
374
375
376

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

377
378
	; return (LazyPat pat', [], res) }

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
-- Type signatures in patterns
-- See Note [Pattern coercions] below
tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
  = do	{ (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
	; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
402
			      tc_lpat pat inner_ty pstate thing_inside
403
	; return (SigPatOut pat' inner_ty, tvs, res) }
404

405
tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
406
  = failWithTc (badTypePat pat)
407

408
409
------------------------
-- Lists, tuples, arrays
410
411
tc_pat pstate (ListPat pats _) pat_ty thing_inside
  = do	{ elt_ty <- boxySplitListTy pat_ty
412
413
	; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
					 	pats pstate thing_inside
414
415
416
417
 	; return (ListPat pats' elt_ty, pats_tvs, res) }

tc_pat pstate (PArrPat pats _) pat_ty thing_inside
  = do	{ [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty
418
419
	; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
						pats pstate thing_inside 
420
421
422
	; ifM (null pats) (zapToMonotype pat_ty)	-- c.f. ExplicitPArr in TcExpr
	; return (PArrPat pats' elt_ty, pats_tvs, res) }

423
tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
424
  = do	{ arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
425
426
	; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
					       pstate thing_inside
427
428
429
430
431

	-- 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.
432
	; let unmangled_result = TuplePat pats' boxity pat_ty
433
434
435
436
	      possibly_mangled_result
	        | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
	        | otherwise			          = unmangled_result

437
 	; ASSERT( length arg_tys == length pats )	-- Syntactically enforced
438
439
440
441
	  return (possibly_mangled_result, pats_tvs, res) }

------------------------
-- Data constructors
442
tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
443
444
  = do	{ data_con <- tcLookupDataCon con_name
	; let tycon = dataConTyCon data_con
445
	; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
446
447
448

------------------------
-- Literal patterns
449
tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
450
451
452
  = do	{ let lit_ty = hsLitType simple_lit
	; coi <- boxyUnify lit_ty pat_ty
			-- coi is of kind: lit_ty ~ pat_ty
453
	; res <- thing_inside pstate
454
455
456
457
458
	; span <- getSrcSpanM
			-- pattern coercions have to
			-- be of kind: pat_ty ~ lit_ty
			-- hence, sym coi
	; returnM (wrapPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, [], res) }
459
460
461

------------------------
-- Overloaded patterns: n, and n+k
462
463
464
465
tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside
  = do	{ let orig = LiteralOrigin over_lit
	; lit'    <- tcOverloadedLit orig over_lit pat_ty
	; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
466
467
	; mb_neg' <- case mb_neg of
			Nothing  -> return Nothing	-- Positive literal
468
469
			Just neg -> 	-- Negative literal
					-- The 'negate' is re-mappable syntax
470
 			    do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
471
			       ; return (Just neg') }
472
473
	; res <- thing_inside pstate
	; returnM (NPat lit' mb_neg' eq' pat_ty, [], res) }
474

475
476
tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
  = do	{ bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
477
 	; let pat_ty' = idType bndr_id
478
479
	      orig    = LiteralOrigin lit
	; lit' <- tcOverloadedLit orig lit pat_ty'
480

481
482
483
	-- 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')
484

485
486
	-- The Report says that n+k patterns must be in Integral
	-- We may not want this when using re-mappable syntax, though (ToDo?)
487
	; icls <- tcLookupClass integralClassName
488
	; instStupidTheta orig [mkClassPred icls [pat_ty']]	
489
    
490
	; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
491
	; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
492

493
tc_pat _ _other_pat _ _ = panic "tc_pat" 	-- ConPatOut, SigPatOut, VarPatOut
494
\end{code}
495

496

497
498
%************************************************************************
%*									*
499
500
	Most of the work for constructors is here
	(the rest is in the ConPatIn case of tc_pat)
501
502
%*									*
%************************************************************************
503

504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
[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 

  Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}

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.

Now it might appear seem as if we could have used the existing GADT type
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.

In fact, if we have a data instance declaration defining a GADT, eq_spec will
be non-empty and we will get a mixture of global instantiations and local
refinement from a single match.  This neatly reflects that, as soon as we
have constrained the type of the scrutinee to the required type index, all
further type refinement is local to the alternative.

559
\begin{code}
560
561
562
563
--	Running example:
-- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
-- 	 with scrutinee of type (T ty)

564
565
tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon 
	 -> BoxySigmaType	-- Type of the pattern
566
	 -> HsConPatDetails Name -> (PatState -> TcM a)
567
	 -> TcM (Pat TcId, [TcTyVar], a)
568
tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
569
  = do	{ let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _) = dataConFullSig data_con
570
	      skol_info = PatSkol data_con
571
	      origin    = SigOrigin skol_info
572
573

	  -- Instantiate the constructor type variables [a->ty]
574
	; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty
575
576
	; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs	-- Get location from monad,
							-- not from ex_tvs
577
	; let tenv     = zipTopTvSubst (univ_tvs ++ ex_tvs)
578
				       (ctxt_res_tys ++ mkTyVarTys ex_tvs')
579
	      eq_spec' = substEqSpec tenv eq_spec
580
	      theta'   = substTheta  tenv (eq_theta ++ dict_theta)
581
582
583
	      arg_tys' = substTys    tenv arg_tys

	; co_vars <- newCoVars eq_spec'	-- Make coercion variables
584
	; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty
585
	
586
	; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
587
		tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
588

589
590
	; loc <- getInstLoc origin
	; dicts <- newDictBndrs loc theta'
591
592
	; dict_binds <- tcSimplifyCheckPat loc co_vars (pat_reft pstate') 
					   ex_tvs' dicts lie_req
593

594
	; addDataConStupidTheta data_con ctxt_res_tys
595

596
597
598
599
	; return
	    (unwrapFamInstScrutinee tycon ctxt_res_tys $
	       ConPatOut { pat_con = L con_span data_con, 
			   pat_tvs = ex_tvs' ++ co_vars,
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
600
			   pat_dicts = map instToVar dicts, 
601
602
603
			   pat_binds = dict_binds,
			   pat_args = arg_pats', pat_ty = pat_ty },
	     ex_tvs' ++ inner_tvs, res)
604
	}
605
  where
606
    -- Split against the family tycon if the pattern constructor 
607
    -- belongs to a family instance tycon.
608
    boxySplitTyConAppWithFamily tycon pat_ty =
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
609
      traceTc traceMsg >>
610
611
612
613
614
615
616
617
      case tyConFamInst_maybe tycon of
        Nothing                   -> boxySplitTyConApp tycon pat_ty
	Just (fam_tycon, instTys) -> 
	  do { scrutinee_arg_tys <- boxySplitTyConApp fam_tycon pat_ty
	     ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
	     ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
	     ; return freshTvs
	     }
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
618
619
620
621
622
623
      where
        traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
		         ppr tycon <+> ppr pat_ty
		       , text "  family instance:" <+> 
			 ppr (tyConFamInst_maybe tycon)
                       ]
624
625
626
627
628
629
630

    -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
    -- pattern if the tycon is an instance of a family.
    --
    unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id
    unwrapFamInstScrutinee tycon args pat
      | Just co_con <- tyConFamilyCoercion_maybe tycon 
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
631
632
--      , not (isNewTyCon tycon)       -- newtypes are explicitly unwrapped by
				     -- the desugarer
633
634
635
          -- 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.
636
      = CoPat (WpCo $ mkTyConApp co_con args)       -- co fam ty to repr ty
637
638
639
640
641
642
	      (pat {pat_ty = mkTyConApp tycon args})    -- representation type
	      pat_ty					-- family inst type
      | otherwise
      = pat


643
tcConArgs :: DataCon -> [TcSigmaType]
644
	  -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
645

646
tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
647
648
  = do	{ checkTc (con_arity == no_of_args)	-- Check correct arity
		  (arityErr "Constructor" data_con con_arity no_of_args)
649
650
651
	; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
	; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
					      pstate thing_inside 
652
	; return (PrefixCon arg_pats', tvs, res) }
653
654
655
  where
    con_arity  = dataConSourceArity data_con
    no_of_args = length arg_pats
656

657
tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside
658
659
  = do	{ checkTc (con_arity == 2)	-- Check correct arity
	 	  (arityErr "Constructor" data_con con_arity 2)
660
661
	; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
					      pstate thing_inside
662
	; return (InfixCon p1' p2', tvs, res) }
663
664
665
  where
    con_arity  = dataConSourceArity data_con

666
667
668
tcConArgs data_con other_args (InfixCon p1 p2) pstate thing_inside
  = pprPanic "tcConArgs" (ppr data_con)	-- InfixCon always has two arguments

669
tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
670
  = do	{ (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
671
	; return (RecCon (HsRecFields rpats' dd), tvs, res) }
672
  where
673
    tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
674
    tc_field (HsRecField field_lbl pat pun) pstate thing_inside
675
      = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
676
	   ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
677
	   ; return (HsRecField sel_id pat' pun, tvs, res) }
678

679
    find_field_ty :: FieldLabel -> TcM (Id, TcType)
680
681
    find_field_ty field_lbl
	= case [ty | (f,ty) <- field_tys, f == field_lbl] of
682
683
684
685
686
687
688
689
690

		-- 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".
691
	   [] -> do { addErrTc (badFieldCon data_con field_lbl)
692
		    ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
693
		    ; return (error "Bogus selector Id", bogus_ty) }
694
695
696
697

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

701
    field_tys :: [(FieldLabel, TcType)]
702
703
704
705
    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).
706
707
708
709
710
711
712

tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
tcConArg (arg_pat, arg_ty) pstate thing_inside
  = tc_lpat arg_pat arg_ty pstate thing_inside
	-- NB: the tc_lpat will refine pat_ty if necessary
	--     based on the current pstate, which may include
	--     refinements from peer argument patterns to the left
713
714
\end{code}

715
\begin{code}
716
addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
717
718
-- Instantiate the "stupid theta" of the data con, and throw 
-- the constraints into the constraint set
719
addDataConStupidTheta data_con inst_tys
720
721
722
  | null stupid_theta = return ()
  | otherwise	      = instStupidTheta origin inst_theta
  where
723
724
725
    origin = OccurrenceOf (dataConName data_con)
	-- The origin should always report "occurrence of C"
	-- even when C occurs in a pattern
726
727
728
729
730
    stupid_theta = dataConStupidTheta data_con
    tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
    inst_theta = substTheta tenv stupid_theta
\end{code}

731

732
733
%************************************************************************
%*									*
734
		Type refinement
735
736
737
738
%*									*
%************************************************************************

\begin{code}
739
740
741
742
743
744
745
746
refineAlt :: DataCon		-- For tracing only
	  -> PatState 
	  -> [TcTyVar]		-- Existentials
	  -> [CoVar]		-- Equational constraints
	  -> BoxySigmaType	-- Pattern type
	  -> TcM PatState

refineAlt con pstate ex_tvs [] pat_ty
747
  | null $ dataConEqTheta con
748
749
750
  = return pstate	-- Common case: no equational constraints

refineAlt con pstate ex_tvs co_vars pat_ty
751
752
753
754
755
  = do	{ opt_gadt <- doptM Opt_GADTs	-- No type-refinement unless GADTs are on
	; if (not opt_gadt) then return pstate
	  else do 

	{ checkTc (isRigidTy pat_ty) (nonRigidMatch con)
756
757
758
759
760
761
762
763
764
765
766
767
768
769
	-- We are matching against a GADT constructor with non-trivial
	-- constraints, but pattern type is wobbly.  For now we fail.
	-- We can make sense of this, however:
	-- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a
	--	(\x -> case x of { MkT v -> v })
	-- We can infer that x must have type T [c], for some wobbly 'c'
	-- and translate to
	--	(\(x::T [c]) -> case x of
	--			  MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g
	-- To implement this, we'd first instantiate the equational
	-- constraints with *wobbly* type variables for the existentials;
	-- then unify these constraints to make pat_ty the right shape;
	-- then proceed exactly as in the rigid case

770
771
		-- In the rigid case, we perform type refinement
	; case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
772
773
	    Failed msg     -> failWithTc (inaccessibleAlt msg) ;
	    Succeeded reft -> do { traceTc trace_msg
774
			  	 ; return (pstate { pat_reft = reft, pat_eqs = (pat_eqs pstate || not (null $ dataConEqTheta con)) }) }
775
776
777
778
	 	    -- DO NOT refine the envt right away, because we 
		    -- might be inside a lazy pattern.  Instead, refine pstate
	        where
		    
779
780
781
782
		    trace_msg = text "refineAlt:match" <+> 
				vcat [ ppr con <+> ppr ex_tvs,
				       ppr [(v, tyVarKind v) | v <- co_vars],
				       ppr reft]
783
	} } }
784
785
\end{code}

786
787
788
789
790
791
792
793
794
795
796

%************************************************************************
%*									*
		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).
797
798

\begin{code}
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
tcOverloadedLit :: InstOrigin
		 -> HsOverLit Name
		 -> BoxyRhoType
		 -> TcM (HsOverLit TcId)
tcOverloadedLit orig lit@(HsIntegral i fi) res_ty
  | not (fi `isHsVar` fromIntegerName)	-- Do not generate a LitInst for rebindable syntax.  
	-- Reason: If we do, tcSimplify will call lookupInst, which
	--	   will call tcSyntaxName, which does unification, 
	--	   which tcSimplify doesn't like
	-- ToDo: noLoc sadness
  = do	{ integer_ty <- tcMetaTy integerTyConName
	; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
	; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) }

  | Just expr <- shortCutIntLit i res_ty 
  = return (HsIntegral i expr)

  | otherwise
  = do 	{ expr <- newLitInst orig lit res_ty
	; return (HsIntegral i expr) }

tcOverloadedLit orig lit@(HsFractional r fr) res_ty
  | not (fr `isHsVar` fromRationalName)	-- c.f. HsIntegral case
  = do	{ rat_ty <- tcMetaTy rationalTyConName
	; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
	 	-- 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
	; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty)))) }

  | Just expr <- shortCutFracLit r res_ty 
  = return (HsFractional r expr)

  | otherwise
  = do 	{ expr <- newLitInst orig lit res_ty
	; return (HsFractional r expr) }

837
838
839
840
841
842
843
844
845
846
847
848
849
tcOverloadedLit orig lit@(HsIsString s fr) res_ty
  | not (fr `isHsVar` fromStringName)	-- c.f. HsIntegral case
  = do	{ str_ty <- tcMetaTy stringTyConName
	; fr' <- tcSyntaxOp orig fr (mkFunTy str_ty res_ty)
	; return (HsIsString s (HsApp (noLoc fr') (nlHsLit (HsString s)))) }

  | Just expr <- shortCutStringLit s res_ty 
  = return (HsIsString s expr)

  | otherwise
  = do 	{ expr <- newLitInst orig lit res_ty
	; return (HsIsString s expr) }

850
851
852
853
854
newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
newLitInst orig lit res_ty	-- Make a LitInst
  = do 	{ loc <- getInstLoc orig
	; res_tau <- zapToMonotype res_ty
	; new_uniq <- newUnique
855
	; let	lit_nm   = mkSystemVarName new_uniq FSLIT("lit")
856
857
		lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit, 
				    tci_ty = res_tau, tci_loc = loc}
858
859
	; extendLIE lit_inst
	; return (HsVar (instToId lit_inst)) }
860
861
\end{code}

862

863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
%************************************************************************
%*									*
		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)

923

924
925
926
927
928
929
%************************************************************************
%*									*
\subsection{Errors and contexts}
%*									*
%************************************************************************

930
\begin{code}
931
932
933
934
patCtxt :: Pat Name -> Maybe Message	-- Not all patterns are worth pushing a context
patCtxt (VarPat _)  = Nothing
patCtxt (ParPat _)  = Nothing
patCtxt (AsPat _ _) = Nothing
935
patCtxt pat 	    = Just (hang (ptext SLIT("In the pattern:")) 
936
			       4 (ppr pat))
937

938
939
-----------------------------------------------

940
existentialExplode pat
941
942
  = hang (vcat [text "My brain just exploded.",
	        text "I can't handle pattern bindings for existentially-quantified constructors.",
943
	        text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
944
		text "In the binding group for"])
945
	4 (ppr pat)
946

947
sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env 
948
949
950
951
952
953
  = 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,
954
955
956
		 sep [ptext SLIT("When checking an existential match that binds"),
		      nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
		      ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
957
		      ptext SLIT("The body has type:") <+> ppr tidy_body_ty
958
		]) }
959
  where
960
    bound_ids = collectPatsBinders pats
961
    show_ids = filter is_interesting bound_ids
962
    is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
963
964
965
966

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

967
badFieldCon :: DataCon -> Name -> SDoc
968
badFieldCon con field
969
  = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
970
	  ptext SLIT("does not have field"), quotes (ppr field)]
971
972
973

polyPatSig :: TcType -> SDoc
polyPatSig sig_ty
974
  = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
975
	 4 (ppr sig_ty)
976
977

badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
978

979
980
lazyPatErr pat tvs
  = failWithTc $
981
    hang (ptext SLIT("A lazy (~) pattern cannot bind existential type variables"))
982
       2 (vcat (map pprSkolTvBinding tvs))
983

984
985
986
987
nonRigidMatch con
  =  hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
	2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))

988
989
990
991
nonRigidResult res_ty
  =  hang (ptext SLIT("GADT pattern match with non-rigid result type") <+> quotes (ppr res_ty))
	2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))

992
993
994
inaccessibleAlt msg
  = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
\end{code}
995
996
997
998
999
1000

\begin{code}
wrapPatCoI :: CoercionI -> Pat a -> TcType -> Pat a
wrapPatCoI IdCo     pat ty = pat
wrapPatCoI (ACo co) pat ty = CoPat (WpCo co) pat ty
\end{code}