TcPat.lhs 35.5 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, tcLamPat, tcLamPats, tcOverloadedLit,
10
	       addDataConStupidTheta, badFieldCon, polyPatSig ) where
11

12
#include "HsVersions.h"
13

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

import HsSyn
import TcHsSyn
18
import TcRnMonad
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
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
import StaticFlags
import TyCon
import DataCon
37
import DynFlags
38
39
40
41
42
43
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
\end{code}
47

48
49
50

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

\begin{code}
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
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, 
				pat_reft = emptyRefinement }
	; (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)
76
77
78
79
80
81
82
83
84

-- 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
85
--   3. Apply the refinement to the environment and result type
86
87
88
--   4. Check the body
--   5. Check that no existentials escape

89
90
91
92
93
94
95
96
97
98
99
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) }
100

101
102
103
104
105
106
107
108
109
-----------------
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 
  =  do	{ let init_state = PS { pat_ctxt = LamPat, pat_reft = reft }

	; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
110
				  refineEnvironment (pat_reft pstate') $
111
	     			  thing_inside (pat_reft pstate', res_ty)
112

113
114
	; let tys = map snd pat_ty_prs
	; tcCheckExistentialPat pats' ex_tvs tys res_ty
115
116
117
118
119

	; returnM (pats', res) }


-----------------
120
tcCheckExistentialPat :: [LPat TcId]		-- Patterns (just for error message)
121
122
123
124
125
126
127
128
129
130
131
		      -> [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).

132
tcCheckExistentialPat pats [] pat_tys body_ty
133
134
  = return ()	-- Short cut for case when there are no existentials

135
tcCheckExistentialPat pats ex_tvs pat_tys body_ty
136
  = addErrCtxtM (sigPatCtxt pats ex_tvs pat_tys body_ty)	$
137
138
139
140
    checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs

data PatState = PS {
	pat_ctxt :: PatCtxt,
141
	pat_reft :: Refinement	-- Binds rigid TcTyVars to their refinements
142
143
144
145
146
147
148
149
150
  }

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

patSigCtxt :: PatState -> UserTypeCtxt
patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
patSigCtxt other			= LamPatSigCtxt
151
152
153
\end{code}


154

155
156
%************************************************************************
%*									*
157
		Binders
158
159
160
%*									*
%************************************************************************

161
\begin{code}
162
163
tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
164
  = do	{ pat_ty' <- unBoxPatBndrType pat_ty bndr_name
165
166
167
168
		-- 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:
169
170
171
172
		-- 	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
173
	; return (Id.mkLocalId bndr_name pat_ty') }
174

175
176
177
178
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
179
	; return (Id.mkLocalId mono_name mono_ty) }
180
181

  | otherwise
182
  = do	{ pat_ty' <- unBoxPatBndrType pat_ty bndr_name
183
	; mono_name <- newLocalName bndr_name
184
	; return (Id.mkLocalId mono_name pat_ty') }
185
186
187
188
189
190
191
192
193
194
195


-------------------
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) }
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212

-------------------
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
213
	  else if isSubArgTypeKind (typeKind ty') then
214
215
216
217
218
219
220
		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")
221
222
\end{code}

223

224
225
%************************************************************************
%*									*
226
		The main worker functions
227
228
229
%*									*
%************************************************************************

230
231
Note [Nesting]
~~~~~~~~~~~~~~
lennart@augustsson.net's avatar
lennart@augustsson.net committed
232
tcPat takes a "thing inside" over which the pattern scopes.  This is partly
233
234
235
236
237
238
239
240
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.

241
\begin{code}
242
--------------------
243
244
245
246
247
248
249
250
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
251
  = do	{ err_ctxt <- getErrCtxt
252
	; let loop pstate []
253
254
255
		= do { res <- thing_inside pstate
		     ; return ([], [], res) }

256
	      loop pstate (arg:args)
257
		= do { (p', p_tvs, (ps', ps_tvs, res)) 
258
				<- tc_pat arg pstate $ \ pstate' ->
259
				   setErrCtxt err_ctxt $
260
				   loop pstate' args
261
262
263
264
265
		-- setErrCtxt: restore context before doing the next pattern
		-- See note [Nesting] above
				
		     ; return (p':ps', p_tvs ++ ps_tvs, res) }

266
	; loop pstate args }
267
268

--------------------
269
270
271
272
273
274
275
276
277
278
279
280
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
281
282
  = setSrcSpan span		  $
    maybeAddErrCtxt (patCtxt pat) $
283
284
285
    do	{ let mb_reft = refineType (pat_reft pstate) pat_ty
	      pat_ty' = case mb_reft of { Just (_, ty') -> ty'; Nothing -> pat_ty }

286
		-- Make sure the result type reflects the current refinement
287
288
289
290
291
292
		-- 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.
293

294
	; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
295
296
297
298
	; let final_pat = case mb_reft of
				Nothing     -> pat'
				Just (co,_) -> CoPat (WpCo co) pat' pat_ty
	; return (L span final_pat, tvs, res) }
299
300
301
302
303

--------------------
tc_pat	:: PatState
	-> Pat Name -> BoxySigmaType	-- Fully refined result type
	-> (PatState -> TcM a)	-- Thing inside
304
	-> TcM (Pat TcId, 	-- Translated pattern
305
306
307
		[TcTyVar], 	-- Existential binders
		a)		-- Result of thing inside

308
309
tc_pat pstate (VarPat name) pat_ty thing_inside
  = do	{ id <- tcPatBndr pstate name pat_ty
310
311
312
	; (res, binds) <- bindInstsOfPatId id $
			  tcExtendIdEnv1 name id $
			  (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
313
			   >> thing_inside pstate)
314
315
316
317
	; let pat' | isEmptyLHsBinds binds = VarPat id
		   | otherwise		   = VarPatOut id binds
	; return (pat', [], res) }

318
tc_pat pstate (ParPat pat) pat_ty thing_inside
319
  = do	{ (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
320
321
	; return (ParPat pat', tvs, res) }

simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
322
tc_pat pstate (BangPat pat) pat_ty thing_inside
323
  = do	{ (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
324
325
	; return (BangPat pat', tvs, res) }

326
-- There's a wrinkle with irrefutable patterns, namely that we
327
328
329
330
331
332
333
334
335
-- 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
336
337
338
339
340
341
342
343
344
345
346
347
--
-- 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.

348
tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
349
350
351
352
353
354
355
  = 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]

356
	-- Check no existentials
357
358
	; if (null pat_tvs) then return ()
	  else lazyPatErr lpat pat_tvs
359
360
361
362
363

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

364
365
	; return (LazyPat pat', [], res) }

366
tc_pat pstate (WildPat _) pat_ty thing_inside
367
  = do	{ pat_ty' <- unBoxWildCardType pat_ty	-- Make sure it's filled in with monotypes
368
	; res <- thing_inside pstate
369
370
	; return (WildPat pat_ty', [], res) }

371
372
tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
  = do	{ bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
373
	; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
374
			      tc_lpat pat (idType bndr_id) pstate thing_inside
375
376
377
378
379
380
381
382
383
	    -- 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) }

384
385
386
387
388
-- 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 $
389
			      tc_lpat pat inner_ty pstate thing_inside
390
	; return (SigPatOut pat' inner_ty, tvs, res) }
391

392
tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
393
  = failWithTc (badTypePat pat)
394

395
396
------------------------
-- Lists, tuples, arrays
397
398
tc_pat pstate (ListPat pats _) pat_ty thing_inside
  = do	{ elt_ty <- boxySplitListTy pat_ty
399
400
	; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
					 	pats pstate thing_inside
401
402
403
404
 	; return (ListPat pats' elt_ty, pats_tvs, res) }

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

410
tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
411
  = do	{ arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
412
413
	; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
					       pstate thing_inside
414
415
416
417
418

	-- 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.
419
	; let unmangled_result = TuplePat pats' boxity pat_ty
420
421
422
423
	      possibly_mangled_result
	        | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
	        | otherwise			          = unmangled_result

424
 	; ASSERT( length arg_tys == length pats )	-- Syntactically enforced
425
426
427
428
	  return (possibly_mangled_result, pats_tvs, res) }

------------------------
-- Data constructors
429
tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
430
431
  = do	{ data_con <- tcLookupDataCon con_name
	; let tycon = dataConTyCon data_con
432
	; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
433
434
435

------------------------
-- Literal patterns
436
437
438
tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
  = do	{ boxyUnify (hsLitType simple_lit) pat_ty
	; res <- thing_inside pstate
439
440
441
442
	; returnM (LitPat simple_lit, [], res) }

------------------------
-- Overloaded patterns: n, and n+k
443
444
445
446
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)
447
448
	; mb_neg' <- case mb_neg of
			Nothing  -> return Nothing	-- Positive literal
449
450
			Just neg -> 	-- Negative literal
					-- The 'negate' is re-mappable syntax
451
 			    do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
452
			       ; return (Just neg') }
453
454
	; res <- thing_inside pstate
	; returnM (NPat lit' mb_neg' eq' pat_ty, [], res) }
455

456
457
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)
458
 	; let pat_ty' = idType bndr_id
459
460
	      orig    = LiteralOrigin lit
	; lit' <- tcOverloadedLit orig lit pat_ty'
461

462
463
464
	-- 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')
465

466
467
	-- The Report says that n+k patterns must be in Integral
	-- We may not want this when using re-mappable syntax, though (ToDo?)
468
	; icls <- tcLookupClass integralClassName
469
	; instStupidTheta orig [mkClassPred icls [pat_ty']]	
470
    
471
	; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
472
	; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
473

474
tc_pat _ _other_pat _ _ = panic "tc_pat" 	-- ConPatOut, SigPatOut, VarPatOut
475
\end{code}
476

477

478
479
%************************************************************************
%*									*
480
481
	Most of the work for constructors is here
	(the rest is in the ConPatIn case of tc_pat)
482
483
%*									*
%************************************************************************
484

485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
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
[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.

540
\begin{code}
541
542
543
544
--	Running example:
-- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
-- 	 with scrutinee of type (T ty)

545
546
tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon 
	 -> BoxySigmaType	-- Type of the pattern
547
	 -> HsConPatDetails Name -> (PatState -> TcM a)
548
	 -> TcM (Pat TcId, [TcTyVar], a)
549
tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
550
  = do	{ let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _) = dataConFullSig data_con
551
	      skol_info = PatSkol data_con
552
	      origin    = SigOrigin skol_info
553
554

	  -- Instantiate the constructor type variables [a->ty]
555
	; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty
556
557
	; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs	-- Get location from monad,
							-- not from ex_tvs
558
	; let tenv     = zipTopTvSubst (univ_tvs ++ ex_tvs)
559
				       (ctxt_res_tys ++ mkTyVarTys ex_tvs')
560
561
562
563
564
	      eq_spec' = substEqSpec tenv eq_spec
	      theta'   = substTheta  tenv theta
	      arg_tys' = substTys    tenv arg_tys

	; co_vars <- newCoVars eq_spec'	-- Make coercion variables
565
	; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty
566
567

	; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
568
		tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
569

570
571
	; loc <- getInstLoc origin
	; dicts <- newDictBndrs loc theta'
572
573
	; dict_binds <- tcSimplifyCheckPat loc co_vars (pat_reft pstate') 
					   ex_tvs' dicts lie_req
574

575
	; addDataConStupidTheta data_con ctxt_res_tys
576

577
578
579
580
581
582
583
584
	; return
	    (unwrapFamInstScrutinee tycon ctxt_res_tys $
	       ConPatOut { pat_con = L con_span data_con, 
			   pat_tvs = ex_tvs' ++ co_vars,
			   pat_dicts = map instToId dicts, 
			   pat_binds = dict_binds,
			   pat_args = arg_pats', pat_ty = pat_ty },
	     ex_tvs' ++ inner_tvs, res)
585
	}
586
  where
587
    -- Split against the family tycon if the pattern constructor 
588
    -- belongs to a family instance tycon.
589
    boxySplitTyConAppWithFamily tycon pat_ty =
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
590
      traceTc traceMsg >>
591
592
593
594
595
596
597
598
      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
599
600
601
602
603
604
      where
        traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
		         ppr tycon <+> ppr pat_ty
		       , text "  family instance:" <+> 
			 ppr (tyConFamInst_maybe tycon)
                       ]
605
606
607
608
609
610
611

    -- 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
612
613
--      , not (isNewTyCon tycon)       -- newtypes are explicitly unwrapped by
				     -- the desugarer
614
615
616
          -- 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.
617
      = CoPat (WpCo $ mkTyConApp co_con args)       -- co fam ty to repr ty
618
619
620
621
622
623
	      (pat {pat_ty = mkTyConApp tycon args})    -- representation type
	      pat_ty					-- family inst type
      | otherwise
      = pat


624
tcConArgs :: DataCon -> [TcSigmaType]
625
	  -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
626

627
tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
628
629
  = do	{ checkTc (con_arity == no_of_args)	-- Check correct arity
		  (arityErr "Constructor" data_con con_arity no_of_args)
630
631
632
	; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
	; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
					      pstate thing_inside 
633
	; return (PrefixCon arg_pats', tvs, res) }
634
635
636
  where
    con_arity  = dataConSourceArity data_con
    no_of_args = length arg_pats
637

638
tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside
639
640
  = do	{ checkTc (con_arity == 2)	-- Check correct arity
	 	  (arityErr "Constructor" data_con con_arity 2)
641
642
	; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
					      pstate thing_inside
643
	; return (InfixCon p1' p2', tvs, res) }
644
645
646
  where
    con_arity  = dataConSourceArity data_con

647
648
649
tcConArgs data_con other_args (InfixCon p1 p2) pstate thing_inside
  = pprPanic "tcConArgs" (ppr data_con)	-- InfixCon always has two arguments

650
tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
651
  = do	{ (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
652
	; return (RecCon (HsRecFields rpats' dd), tvs, res) }
653
  where
654
    tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
655
    tc_field (HsRecField field_lbl pat pun) pstate thing_inside
656
      = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
657
	   ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
658
	   ; return (HsRecField sel_id pat' pun, tvs, res) }
659

660
    find_field_ty :: FieldLabel -> TcM (Id, TcType)
661
662
    find_field_ty field_lbl
	= case [ty | (f,ty) <- field_tys, f == field_lbl] of
663
664
665
666
667
668
669
670
671

		-- 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".
672
	   [] -> do { addErrTc (badFieldCon data_con field_lbl)
673
		    ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
674
		    ; return (error "Bogus selector Id", bogus_ty) }
675
676
677
678

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

682
    field_tys :: [(FieldLabel, TcType)]
683
684
685
686
    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).
687
688
689
690
691
692
693

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
694
695
\end{code}

696
\begin{code}
697
addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
698
699
-- Instantiate the "stupid theta" of the data con, and throw 
-- the constraints into the constraint set
700
addDataConStupidTheta data_con inst_tys
701
702
703
  | null stupid_theta = return ()
  | otherwise	      = instStupidTheta origin inst_theta
  where
704
705
706
    origin = OccurrenceOf (dataConName data_con)
	-- The origin should always report "occurrence of C"
	-- even when C occurs in a pattern
707
708
709
710
711
    stupid_theta = dataConStupidTheta data_con
    tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
    inst_theta = substTheta tenv stupid_theta
\end{code}

712

713
714
%************************************************************************
%*									*
715
		Type refinement
716
717
718
719
%*									*
%************************************************************************

\begin{code}
720
721
722
723
724
725
726
727
728
729
730
refineAlt :: DataCon		-- For tracing only
	  -> PatState 
	  -> [TcTyVar]		-- Existentials
	  -> [CoVar]		-- Equational constraints
	  -> BoxySigmaType	-- Pattern type
	  -> TcM PatState

refineAlt con pstate ex_tvs [] pat_ty
  = return pstate	-- Common case: no equational constraints

refineAlt con pstate ex_tvs co_vars pat_ty
731
732
733
734
735
  = 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)
736
737
738
739
740
741
742
743
744
745
746
747
748
749
	-- 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

750
751
		-- In the rigid case, we perform type refinement
	; case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
752
753
754
755
756
757
758
	    Failed msg     -> failWithTc (inaccessibleAlt msg) ;
	    Succeeded reft -> do { traceTc trace_msg
			  	 ; return (pstate { pat_reft = reft }) }
	 	    -- DO NOT refine the envt right away, because we 
		    -- might be inside a lazy pattern.  Instead, refine pstate
	        where
		    
759
760
761
762
		    trace_msg = text "refineAlt:match" <+> 
				vcat [ ppr con <+> ppr ex_tvs,
				       ppr [(v, tyVarKind v) | v <- co_vars],
				       ppr reft]
763
	} } }
764
765
\end{code}

766
767
768
769
770
771
772
773
774
775
776

%************************************************************************
%*									*
		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).
777
778

\begin{code}
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
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) }

817
818
819
820
821
822
823
824
825
826
827
828
829
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) }

830
831
832
833
834
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
835
	; let	lit_nm   = mkSystemVarName new_uniq FSLIT("lit")
836
837
		lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit, 
				    tci_ty = res_tau, tci_loc = loc}
838
839
	; extendLIE lit_inst
	; return (HsVar (instToId lit_inst)) }
840
841
\end{code}

842

843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
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
%************************************************************************
%*									*
		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)

903

904
905
906
907
908
909
%************************************************************************
%*									*
\subsection{Errors and contexts}
%*									*
%************************************************************************

910
\begin{code}
911
912
913
914
patCtxt :: Pat Name -> Maybe Message	-- Not all patterns are worth pushing a context
patCtxt (VarPat _)  = Nothing
patCtxt (ParPat _)  = Nothing
patCtxt (AsPat _ _) = Nothing
915
patCtxt pat 	    = Just (hang (ptext SLIT("In the pattern:")) 
916
			       4 (ppr pat))
917

918
919
-----------------------------------------------

920
existentialExplode pat
921
922
  = hang (vcat [text "My brain just exploded.",
	        text "I can't handle pattern bindings for existentially-quantified constructors.",
923
	        text "Instead, use a case-expression to unpack the constructor.",
924
		text "In the binding group for"])
925
	4 (ppr pat)
926

927
sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env 
928
929
930
931
932
933
  = 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,
934
935
936
		 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),
937
		      ptext SLIT("The body has type:") <+> ppr tidy_body_ty
938
		]) }
939
  where
940
    bound_ids = collectPatsBinders pats
941
    show_ids = filter is_interesting bound_ids
942
    is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
943
944
945
946

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

947
badFieldCon :: DataCon -> Name -> SDoc
948
badFieldCon con field
949
  = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
950
	  ptext SLIT("does not have field"), quotes (ppr field)]
951
952
953

polyPatSig :: TcType -> SDoc
polyPatSig sig_ty
954
  = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
955
	 4 (ppr sig_ty)
956
957

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

959
960
lazyPatErr pat tvs
  = failWithTc $
961
    hang (ptext SLIT("A lazy (~) pattern cannot bind existential type variables"))
962
       2 (vcat (map pprSkolTvBinding tvs))
963

964
965
966
967
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"))

968
969
970
inaccessibleAlt msg
  = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
\end{code}