TcPat.lhs 17.5 KB
Newer Older
1
%
2
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
3
4
5
6
%
\section[TcPat]{Typechecking patterns}

\begin{code}
7
8
9
module TcPat ( tcPat, tcMonoPatBndr, tcSubPat,
	       badFieldCon, polyPatSig
  ) where
10

11
#include "HsVersions.h"
12

13
import HsSyn		( InPat(..), OutPat(..), HsLit(..), HsOverLit(..), HsExpr(..) )
14
import RnHsSyn		( RenamedPat )
15
import TcHsSyn		( TcPat, TcId, simpleHsLitTy )
16

17
import TcMonad
18
import Inst		( InstOrigin(..),
19
			  emptyLIE, plusLIE, LIE, mkLIE, unitLIE, instToId, isEmptyLIE,
20
			  newMethod, newOverloadedLit, newDicts
21
			)
22
import Id		( mkLocalId, mkSysLocal )
23
import Name		( Name )
24
import FieldLabel	( fieldLabelName )
25
import TcEnv		( tcLookupClass, tcLookupDataCon, tcLookupGlobalId, tcLookupId )
26
27
28
29
import TcMType 		( tcInstTyVars, newTyVarTy, getTcTyVar, putTcTyVar )
import TcType		( TcType, TcTyVar, TcSigmaType,
			  mkTyConApp, mkClassPred, liftedTypeKind, tcGetTyVar_maybe,
			  isHoleTyVar, openTypeKind )
chak's avatar
chak committed
30
31
32
import TcUnify		( tcSub, unifyTauTy, unifyListTy, unifyPArrTy,
			  unifyTupleTy,  mkCoercion, idCoercion, isIdCoercion,
			  (<$>), PatCoFn )
33
import TcMonoType	( tcHsSigType, UserTypeCtxt(..) )
34

35
import TysWiredIn	( stringTy )
36
import CmdLineOpts	( opt_IrrefutableTuples )
37
import DataCon		( dataConSig, dataConFieldLabels, 
38
39
			  dataConSourceArity
			)
40
import Subst		( substTy, substTheta )
41
import PrelNames	( eqStringName, eqName, geName, cCallableClassName )
42
import BasicTypes	( isBoxed )
43
import Bag
sof's avatar
sof committed
44
import Outputable
45
\end{code}
46

47
48
49
50
51
52
53
54

%************************************************************************
%*									*
\subsection{Variable patterns}
%*									*
%************************************************************************

\begin{code}
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
type BinderChecker = Name -> TcSigmaType -> TcM (PatCoFn, LIE, TcId)
			-- How to construct a suitable (monomorphic)
			-- Id for variables found in the pattern
			-- The TcSigmaType is the expected type 
			-- from the pattern context

-- The Id may have a sigma type (e.g. f (x::forall a. a->a))
-- so we want to *create* it during pattern type checking.
-- We don't want to make Ids first with a type-variable type
-- and then unify... becuase we can't unify a sigma type with a type variable.

tcMonoPatBndr :: BinderChecker
  -- This is the right function to pass to tcPat when 
  -- we're looking at a lambda-bound pattern, 
  -- so there's no polymorphic guy to worry about

tcMonoPatBndr binder_name pat_ty 
  | Just tv <- tcGetTyVar_maybe pat_ty,
    isHoleTyVar tv
	-- If there are *no constraints* on the pattern type, we
	-- revert to good old H-M typechecking, making
	-- the type of the binder into an *ordinary* 
	-- type variable.  We find out if there are no constraints
	-- by seeing if we are given an "open hole" as our info.
	-- What we are trying to avoid here is giving a binder
	-- a type that is a 'hole'.  The only place holes should
	-- appear is as an argument to tcPat and tcExpr/tcMonoExpr.
  = getTcTyVar tv	`thenNF_Tc` \ maybe_ty ->
    case maybe_ty of
	Just ty -> tcMonoPatBndr binder_name ty
	Nothing -> newTyVarTy openTypeKind	`thenNF_Tc` \ ty ->
		   putTcTyVar tv ty		`thenNF_Tc_`
		   returnTc (idCoercion, emptyLIE, mkLocalId binder_name ty)
  | otherwise
  = returnTc (idCoercion, emptyLIE, mkLocalId binder_name pat_ty)
90
91
92
93
94
95
96
97
98
\end{code}


%************************************************************************
%*									*
\subsection{Typechecking patterns}
%*									*
%************************************************************************

99
\begin{code}
100
tcPat :: BinderChecker
101
      -> RenamedPat
102

103
      -> TcSigmaType	-- Expected type derived from the context
104
105
106
			--	In the case of a function with a rank-2 signature,
			--	this type might be a forall type.

107
      -> TcM (TcPat, 
108
109
110
111
112
113
		LIE,			-- Required by n+k and literal pats
		Bag TcTyVar,	-- TyVars bound by the pattern
					-- 	These are just the existentially-bound ones.
					--	Any tyvars bound by *type signatures* in the
					-- 	patterns are brought into scope before we begin.
		Bag (Name, TcId),	-- Ids bound by the pattern, along with the Name under
114
115
116
					--	which it occurs in the pattern
					-- 	The two aren't the same because we conjure up a new
					-- 	local name for each variable.
117
118
		LIE)			-- Dicts or methods [see below] bound by the pattern
					-- 	from existential constructor patterns
119
120
\end{code}

121

122
123
124
125
126
127
128
%************************************************************************
%*									*
\subsection{Variables, wildcards, lazy pats, as-pats}
%*									*
%************************************************************************

\begin{code}
129
130
131
tcPat tc_bndr pat@(TypePatIn ty) pat_ty
  = failWithTc (badTypePat pat)

132
tcPat tc_bndr (VarPatIn name) pat_ty
133
134
135
  = tc_bndr name pat_ty				`thenTc` \ (co_fn, lie_req, bndr_id) ->
    returnTc (co_fn <$> VarPat bndr_id, lie_req,
	      emptyBag, unitBag (name, bndr_id), emptyLIE)
136

137
138
tcPat tc_bndr (LazyPatIn pat) pat_ty
  = tcPat tc_bndr pat pat_ty		`thenTc` \ (pat', lie_req, tvs, ids, lie_avail) ->
139
    returnTc (LazyPat pat', lie_req, tvs, ids, lie_avail)
140

141
tcPat tc_bndr pat_in@(AsPatIn name pat) pat_ty
142
143
  = tc_bndr name pat_ty			`thenTc` \ (co_fn, lie_req1, bndr_id) ->
    tcPat tc_bndr pat pat_ty		`thenTc` \ (pat', lie_req2, tvs, ids, lie_avail) ->
144
    returnTc (co_fn <$> (AsPat bndr_id pat'), lie_req1 `plusLIE` lie_req2, 
145
	      tvs, (name, bndr_id) `consBag` ids, lie_avail)
146

147
tcPat tc_bndr WildPatIn pat_ty
148
  = returnTc (WildPat pat_ty, emptyLIE, emptyBag, emptyBag, emptyLIE)
149

150
151
tcPat tc_bndr (ParPatIn parend_pat) pat_ty
  = tcPat tc_bndr parend_pat pat_ty
152

153
tcPat tc_bndr (SigPatIn pat sig) pat_ty
154
155
156
157
  = tcHsSigType PatSigCtxt sig		`thenTc` \ sig_ty ->
    tcSubPat sig_ty pat_ty		`thenTc` \ (co_fn, lie_sig) ->
    tcPat tc_bndr pat sig_ty		`thenTc` \ (pat', lie_req, tvs, ids, lie_avail) ->
    returnTc (co_fn <$> pat', lie_req `plusLIE` lie_sig, tvs, ids, lie_avail)
158
159
\end{code}

160

161
162
%************************************************************************
%*									*
chak's avatar
chak committed
163
\subsection{Explicit lists, parallel arrays, and tuples}
164
165
166
167
%*									*
%************************************************************************

\begin{code}
168
tcPat tc_bndr pat_in@(ListPatIn pats) pat_ty
169
170
  = tcAddErrCtxt (patCtxt pat_in)		$
    unifyListTy pat_ty				`thenTc` \ elem_ty ->
171
    tcPats tc_bndr pats (repeat elem_ty)	`thenTc` \ (pats', lie_req, tvs, ids, lie_avail) ->
172
    returnTc (ListPat elem_ty pats', lie_req, tvs, ids, lie_avail)
chak's avatar
chak committed
173
174
175
176
177
178

tcPat tc_bndr pat_in@(PArrPatIn pats) pat_ty
  = tcAddErrCtxt (patCtxt pat_in)		$
    unifyPArrTy pat_ty				`thenTc` \ elem_ty ->
    tcPats tc_bndr pats (repeat elem_ty)	`thenTc` \ (pats', lie_req, tvs, ids, lie_avail) ->
    returnTc (PArrPat elem_ty pats', lie_req, tvs, ids, lie_avail)
179

180
tcPat tc_bndr pat_in@(TuplePatIn pats boxity) pat_ty
181
  = tcAddErrCtxt (patCtxt pat_in)	$
182

183
184
    unifyTupleTy boxity arity pat_ty		`thenTc` \ arg_tys ->
    tcPats tc_bndr pats arg_tys 		`thenTc` \ (pats', lie_req, tvs, ids, lie_avail) ->
185
186
187

	-- possibly do the "make all tuple-pats irrefutable" test:
    let
188
	unmangled_result = TuplePat pats' boxity
189
190
191
192
193

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

195
	possibly_mangled_result
196
197
	  | opt_IrrefutableTuples && isBoxed boxity = LazyPat unmangled_result
	  | otherwise			   	    = unmangled_result
198
    in
199
200
201
    returnTc (possibly_mangled_result, lie_req, tvs, ids, lie_avail)
  where
    arity = length pats
202
203
\end{code}

204

205
206
207
208
209
%************************************************************************
%*									*
\subsection{Other constructors}
%*									*

210
%************************************************************************
211
212

\begin{code}
213
214
tcPat tc_bndr pat@(ConPatIn name arg_pats) pat_ty
  = tcConPat tc_bndr pat name arg_pats pat_ty
215

216
217
tcPat tc_bndr pat@(ConOpPatIn pat1 op _ pat2) pat_ty
  = tcConPat tc_bndr pat op [pat1, pat2] pat_ty
218
219
\end{code}

220

221
222
223
224
225
226
227
%************************************************************************
%*									*
\subsection{Records}
%*									*
%************************************************************************

\begin{code}
228
tcPat tc_bndr pat@(RecPatIn name rpats) pat_ty
229
  = tcAddErrCtxt (patCtxt pat)	$
230

231
 	-- Check the constructor itself
232
233
234
235
    tcConstructor pat name 		`thenTc` \ (data_con, ex_tvs, dicts, lie_avail1, arg_tys, con_res_ty) ->

	-- Check overall type matches (c.f. tcConPat)
    tcSubPat con_res_ty pat_ty 		`thenTc` \ (co_fn, lie_req1) ->
236
    let
237
	-- Don't use zipEqual! If the constructor isn't really a record, then
238
239
240
241
	-- dataConFieldLabels will be empty (and each field in the pattern
	-- will generate an error below).
	field_tys = zip (map fieldLabelName (dataConFieldLabels data_con))
			arg_tys
242
243
    in

244
	-- Check the fields
245
    tc_fields field_tys rpats		`thenTc` \ (rpats', lie_req2, tvs, ids, lie_avail2) ->
246

247
    returnTc (RecPat data_con pat_ty ex_tvs dicts rpats',
248
	      lie_req1 `plusLIE` lie_req2,
249
250
251
	      listToBag ex_tvs `unionBags` tvs,
	      ids,
	      lie_avail1 `plusLIE` lie_avail2)
252
253

  where
254
255
256
257
    tc_fields field_tys []
      = returnTc ([], emptyLIE, emptyBag, emptyBag, emptyLIE)

    tc_fields field_tys ((field_label, rhs_pat, pun_flag) : rpats)
258
259
260
261
262
263
264
265
266
267
268
269
270
      =	tc_fields field_tys rpats	`thenTc` \ (rpats', lie_req1, tvs1, ids1, lie_avail1) ->

	(case [ty | (f,ty) <- field_tys, f == field_label] of

		-- 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".
	   [] -> addErrTc (badFieldCon name field_label)	`thenNF_Tc_` 
271
		 newTyVarTy liftedTypeKind			`thenNF_Tc_` 
272
273
274
275
276
		 returnTc (error "Bogus selector Id", pat_ty)

		-- The normal case, when the field comes from the right constructor
	   (pat_ty : extras) -> 
		ASSERT( null extras )
277
		tcLookupGlobalId field_label			`thenNF_Tc` \ sel_id ->
278
279
280
281
		returnTc (sel_id, pat_ty)
	)							`thenTc` \ (sel_id, pat_ty) ->

	tcPat tc_bndr rhs_pat pat_ty	`thenTc` \ (rhs_pat', lie_req2, tvs2, ids2, lie_avail2) ->
282
283
284
285
286
287

	returnTc ((sel_id, rhs_pat', pun_flag) : rpats',
		  lie_req1 `plusLIE` lie_req2,
		  tvs1 `unionBags` tvs2,
		  ids1 `unionBags` ids2,
		  lie_avail1 `plusLIE` lie_avail2)
288
289
\end{code}

290
291
%************************************************************************
%*									*
292
\subsection{Literals}
293
294
295
296
%*									*
%************************************************************************

\begin{code}
297
tcPat tc_bndr (LitPatIn lit@(HsLitLit s _)) pat_ty 
298
	-- cf tcExpr on LitLits
299
  = tcLookupClass cCallableClassName		`thenNF_Tc` \ cCallableClass ->
300
    newDicts (LitLitOrigin (_UNPK_ s))
301
302
	     [mkClassPred cCallableClass [pat_ty]]	`thenNF_Tc` \ dicts ->
    returnTc (LitPat (HsLitLit s pat_ty) pat_ty, mkLIE dicts, emptyBag, emptyBag, emptyLIE)
303
304
305

tcPat tc_bndr pat@(LitPatIn lit@(HsString _)) pat_ty
  = unifyTauTy pat_ty stringTy			`thenTc_` 
306
    tcLookupGlobalId eqStringName		`thenNF_Tc` \ eq_id ->
307
308
309
310
311
312
313
314
315
    returnTc (NPat lit stringTy (HsVar eq_id `HsApp` HsLit lit), 
	      emptyLIE, emptyBag, emptyBag, emptyLIE)

tcPat tc_bndr (LitPatIn simple_lit) pat_ty
  = unifyTauTy pat_ty (simpleHsLitTy simple_lit)		`thenTc_` 
    returnTc (LitPat simple_lit pat_ty, emptyLIE, emptyBag, emptyBag, emptyLIE)

tcPat tc_bndr pat@(NPatIn over_lit) pat_ty
  = newOverloadedLit (PatOrigin pat) over_lit pat_ty	`thenNF_Tc` \ (over_lit_expr, lie1) ->
316
    tcLookupGlobalId eqName				`thenNF_Tc` \ eq_sel_id ->
317
    newMethod origin eq_sel_id [pat_ty]			`thenNF_Tc` \ eq ->
318

319
320
    returnTc (NPat lit' pat_ty (HsApp (HsVar (instToId eq)) over_lit_expr),
	      lie1 `plusLIE` unitLIE eq,
321
322
323
324
	      emptyBag, emptyBag, emptyLIE)
  where
    origin = PatOrigin pat
    lit' = case over_lit of
325
326
		HsIntegral i _   -> HsInteger i
		HsFractional f _ -> HsRat f pat_ty
327
328
329
330
\end{code}

%************************************************************************
%*									*
331
\subsection{n+k patterns}
332
333
334
335
%*									*
%************************************************************************

\begin{code}
336
tcPat tc_bndr pat@(NPlusKPatIn name lit@(HsIntegral i _) minus_name) pat_ty
337
  = tc_bndr name pat_ty				`thenTc` \ (co_fn, lie1, bndr_id) ->
338
	-- The '-' part is re-mappable syntax
339
    tcLookupId minus_name			`thenNF_Tc` \ minus_sel_id ->
340
    tcLookupGlobalId geName			`thenNF_Tc` \ ge_sel_id ->
341
    newOverloadedLit origin lit pat_ty		`thenNF_Tc` \ (over_lit_expr, lie2) ->
342
343
    newMethod origin ge_sel_id    [pat_ty]	`thenNF_Tc` \ ge ->
    newMethod origin minus_sel_id [pat_ty]	`thenNF_Tc` \ minus ->
344

345
    returnTc (NPlusKPat bndr_id i pat_ty
346
347
			(SectionR (HsVar (instToId ge)) over_lit_expr)
			(SectionR (HsVar (instToId minus)) over_lit_expr),
348
	      lie1 `plusLIE` lie2 `plusLIE` mkLIE [ge,minus],
349
	      emptyBag, unitBag (name, bndr_id), emptyLIE)
350
  where
351
    origin = PatOrigin pat
352
353
354
355
356
357
358
359
\end{code}

%************************************************************************
%*									*
\subsection{Lists of patterns}
%*									*
%************************************************************************

360
361
Helper functions

362
\begin{code}
363
tcPats :: BinderChecker				-- How to deal with variables
364
       -> [RenamedPat] -> [TcType]		-- Excess 'expected types' discarded
365
       -> TcM ([TcPat], 
366
367
368
369
		 LIE,				-- Required by n+k and literal pats
		 Bag TcTyVar,
		 Bag (Name, TcId),	-- Ids bound by the pattern
		 LIE)				-- Dicts bound by the pattern
370

371
tcPats tc_bndr [] tys = returnTc ([], emptyLIE, emptyBag, emptyBag, emptyLIE)
372

373
374
375
tcPats tc_bndr (ty:tys) (pat:pats)
  = tcPat tc_bndr ty pat		`thenTc` \ (pat',  lie_req1, tvs1, ids1, lie_avail1) ->
    tcPats tc_bndr tys pats	`thenTc` \ (pats', lie_req2, tvs2, ids2, lie_avail2) ->
376
377
378
379
380

    returnTc (pat':pats', lie_req1 `plusLIE` lie_req2,
	      tvs1 `unionBags` tvs2, ids1 `unionBags` ids2, 
	      lie_avail1 `plusLIE` lie_avail2)
\end{code}
381

382
------------------------------------------------------
383
\begin{code}
384
tcConstructor pat con_name
385
  = 	-- Check that it's a constructor
386
    tcLookupDataCon con_name		`thenNF_Tc` \ data_con ->
387
388
389

	-- Instantiate it
    let 
390
	(tvs, _, ex_tvs, ex_theta, arg_tys, tycon) = dataConSig data_con
391
	     -- Ignore the theta; overloaded constructors only
392
393
	     -- behave differently when called, not when used for
	     -- matching.
394
395
396
    in
    tcInstTyVars (ex_tvs ++ tvs)	`thenNF_Tc` \ (all_tvs', ty_args', tenv) ->
    let
397
	ex_theta' = substTheta tenv ex_theta
398
	arg_tys'  = map (substTy tenv) arg_tys
399
400
401
402
403

	n_ex_tvs  = length ex_tvs
	ex_tvs'   = take n_ex_tvs all_tvs'
	result_ty = mkTyConApp tycon (drop n_ex_tvs ty_args')
    in
404
    newDicts (PatOrigin pat) ex_theta'	`thenNF_Tc` \ dicts ->
405

406
    returnTc (data_con, ex_tvs', map instToId dicts, mkLIE dicts, arg_tys', result_ty)
407
408
409
410
\end{code}	      

------------------------------------------------------
\begin{code}
411
tcConPat tc_bndr pat con_name arg_pats pat_ty
412
413
414
  = tcAddErrCtxt (patCtxt pat)	$

	-- Check the constructor itself
415
416
417
418
419
420
    tcConstructor pat con_name 	`thenTc` \ (data_con, ex_tvs, dicts, lie_avail1, arg_tys, con_res_ty) ->

	-- Check overall type matches.
	-- The pat_ty might be a for-all type, in which
	-- case we must instantiate to match
    tcSubPat con_res_ty pat_ty 	`thenTc` \ (co_fn, lie_req1) ->
421
422

	-- Check correct arity
423
    let
424
425
	con_arity  = dataConSourceArity data_con
	no_of_args = length arg_pats
426
    in
427
    checkTc (con_arity == no_of_args)
428
429
430
	    (arityErr "Constructor" data_con con_arity no_of_args)	`thenTc_`

	-- Check arguments
431
    tcPats tc_bndr arg_pats arg_tys	`thenTc` \ (arg_pats', lie_req2, tvs, ids, lie_avail2) ->
432

433
434
435
    returnTc (co_fn <$> ConPat data_con pat_ty ex_tvs dicts arg_pats',
	      lie_req1 `plusLIE` lie_req2,
	      listToBag ex_tvs `unionBags` tvs,
436
437
	      ids,
	      lie_avail1 `plusLIE` lie_avail2)
438
439
440
\end{code}


441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
%************************************************************************
%*									*
\subsection{Subsumption}
%*									*
%************************************************************************

Example:  
	f :: (forall a. a->a) -> Int -> Int
	f (g::Int->Int) y = g y
This is ok: the type signature allows fewer callers than
the (more general) signature f :: (Int->Int) -> Int -> Int
I.e.    (forall a. a->a) <= Int -> Int
We end up translating this to:
	f = \g' :: (forall a. a->a).  let g = g' Int in g' y

tcSubPat does the work
 	sig_ty is the signature on the pattern itself 
		(Int->Int in the example)
	expected_ty is the type passed inwards from the context
		(forall a. a->a in the example)

\begin{code}
tcSubPat :: TcSigmaType -> TcSigmaType -> TcM (PatCoFn, LIE)

tcSubPat sig_ty exp_ty
466
 = tcSub sig_ty exp_ty			`thenTc` \ (co_fn, lie) ->
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
	-- co_fn is a coercion on *expressions*, and we
	-- need to make a coercion on *patterns*
   if isIdCoercion co_fn then
	ASSERT( isEmptyLIE lie )
	returnNF_Tc (idCoercion, emptyLIE)
   else
   tcGetUnique				`thenNF_Tc` \ uniq ->
   let
	arg_id  = mkSysLocal SLIT("sub") uniq exp_ty
	the_fn  = DictLam [arg_id] (co_fn <$> HsVar arg_id)
	pat_co_fn p = SigPat p exp_ty the_fn
   in
   returnNF_Tc (mkCoercion pat_co_fn, lie)
\end{code}


483
484
485
486
487
488
%************************************************************************
%*									*
\subsection{Errors and contexts}
%*									*
%************************************************************************

489
\begin{code}
490
491
patCtxt pat = hang (ptext SLIT("In the pattern:")) 
		 4 (ppr pat)
492

493
494
badFieldCon :: Name -> Name -> SDoc
badFieldCon con field
495
  = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
496
	  ptext SLIT("does not have field"), quotes (ppr field)]
497
498
499

polyPatSig :: TcType -> SDoc
polyPatSig sig_ty
500
  = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
501
	 4 (ppr sig_ty)
502
503

badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
504
\end{code}
505