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

6
7
8


\begin{code}
9
module TcSimplify (
10
11
12
13
	tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck, 
	tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop, 
	tcSimplifyThetas, tcSimplifyCheckThetas,
	bindInstsOfLocalFuns
14
15
    ) where

16
#include "HsVersions.h"
17

18
import HsSyn		( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
19
import TcHsSyn		( TcExpr, TcId, 
20
21
			  TcMonoBinds, TcDictBinds
			)
22

23
import TcMonad
24
import Inst		( lookupInst, lookupSimpleInst, LookupInstResult(..),
25
26
			  tyVarsOfInst, predsOfInsts, 
			  isDict, isClassDict, 
27
			  isStdClassTyVarDict, isMethodFor,
28
29
30
			  instToId, tyVarsOfInsts,
			  instBindingRequired, instCanBeGeneralised,
			  newDictsFromOld, instMentionsIPs,
31
			  getDictClassTys, getIPs, isTyVarDict,
32
			  instLoc, pprInst, zonkInst, tidyInst, tidyInsts,
33
			  Inst, LIE, pprInsts, pprInstsInFull,
34
			  mkLIE, lieToList 
sof's avatar
sof committed
35
			)
36
import TcEnv		( tcGetGlobalTyVars, tcGetInstEnv )
37
import InstEnv		( lookupInstEnv, classInstEnv, InstLookupResult(..) )
38

39
import TcType		( zonkTcTyVarsAndFV, tcInstTyVars )
40
41
import TcUnify		( unifyTauTy )
import Id		( idType )
42
43
import Name		( Name )
import NameSet		( mkNameSet )
44
import Class		( Class, classBigSig )
45
import FunDeps		( oclose, grow, improve )
sof's avatar
sof committed
46
import PrelInfo		( isNumericClass, isCreturnableClass, isCcallishClass )
47

48
import Type		( Type, ClassContext,
49
			  mkTyVarTy, getTyVar, 
50
			  isTyVarTy, splitSigmaTy, tyVarsOfTypes
51
			)
52
import Subst		( mkTopTyVarSubst, substClasses, substTy )
53
import PprType		( pprClassPred )
54
import TysWiredIn	( unitTy )
55
import VarSet
56
57
import FiniteMap
import Outputable
58
59
import ListSetOps	( equivClasses )
import Util		( zipEqual, mapAccumL )
60
import List		( partition )
61
import CmdLineOpts
62
63
64
65
66
\end{code}


%************************************************************************
%*									*
67
\subsection{NOTES}
68
69
70
%*									*
%************************************************************************

71
72
73
74
75
76
77
78
79
	--------------------------------------	
		Notes on quantification
	--------------------------------------	

Suppose we are about to do a generalisation step.
We have in our hand

	G	the environment
	T	the type of the RHS
80
	C	the constraints from that RHS
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243

The game is to figure out

	Q	the set of type variables over which to quantify
	Ct	the constraints we will *not* quantify over
	Cq	the constraints we will quantify over

So we're going to infer the type

	forall Q. Cq => T

and float the constraints Ct further outwards.  

Here are the things that *must* be true:

 (A)	Q intersect fv(G) = EMPTY			limits how big Q can be
 (B)	Q superset fv(Cq union T) \ oclose(fv(G),C)	limits how small Q can be

(A) says we can't quantify over a variable that's free in the
environment.  (B) says we must quantify over all the truly free
variables in T, else we won't get a sufficiently general type.  We do
not *need* to quantify over any variable that is fixed by the free
vars of the environment G.

	BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!

Example:	class H x y | x->y where ...

	fv(G) = {a}	C = {H a b, H c d}
			T = c -> b

	(A)  Q intersect {a} is empty
	(B)  Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}

	So Q can be {c,d}, {b,c,d}

Other things being equal, however, we'd like to quantify over as few
variables as possible: smaller types, fewer type applications, more
constraints can get into Ct instead of Cq.


-----------------------------------------
We will make use of

  fv(T)	 	the free type vars of T

  oclose(vs,C)	The result of extending the set of tyvars vs
		using the functional dependencies from C

  grow(vs,C)	The result of extend the set of tyvars vs
		using all conceivable links from C.  

		E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
		Then grow(vs,C) = {a,b,c}

		Note that grow(vs,C) `superset` grow(vs,simplify(C))
		That is, simplfication can only shrink the result of grow.

Notice that 
   oclose is conservative one way:      v `elem` oclose(vs,C) => v is definitely fixed by vs
   grow is conservative the other way:  if v might be fixed by vs => v `elem` grow(vs,C)


-----------------------------------------

Choosing Q
~~~~~~~~~~
Here's a good way to choose Q:

	Q = grow( fv(T), C ) \ oclose( fv(G), C )

That is, quantify over all variable that that MIGHT be fixed by the
call site (which influences T), but which aren't DEFINITELY fixed by
G.  This choice definitely quantifies over enough type variables,
albeit perhaps too many.

Why grow( fv(T), C ) rather than fv(T)?  Consider

	class H x y | x->y where ...
	
	T = c->c
	C = (H c d)

  If we used fv(T) = {c} we'd get the type

	forall c. H c d => c -> b

  And then if the fn was called at several different c's, each of 
  which fixed d differently, we'd get a unification error, because
  d isn't quantified.  Solution: quantify d.  So we must quantify
  everything that might be influenced by c.

Why not oclose( fv(T), C )?  Because we might not be able to see
all the functional dependencies yet:

	class H x y | x->y where ...
	instance H x y => Eq (T x y) where ...

	T = c->c
	C = (Eq (T c d))

  Now oclose(fv(T),C) = {c}, because the functional dependency isn't
  apparent yet, and that's wrong.  We must really quantify over d too.


There really isn't any point in quantifying over any more than
grow( fv(T), C ), because the call sites can't possibly influence
any other type variables.



	--------------------------------------	
		Notes on ambiguity  
	--------------------------------------	

It's very hard to be certain when a type is ambiguous.  Consider

	class K x
	class H x y | x -> y
	instance H x y => K (x,y)

Is this type ambiguous?
	forall a b. (K (a,b), Eq b) => a -> a

Looks like it!  But if we simplify (K (a,b)) we get (H a b) and
now we see that a fixes b.  So we can't tell about ambiguity for sure
without doing a full simplification.  And even that isn't possible if
the context has some free vars that may get unified.  Urgle!

Here's another example: is this ambiguous?
	forall a b. Eq (T b) => a -> a
Not if there's an insance decl (with no context)
	instance Eq (T b) where ...

You may say of this example that we should use the instance decl right
away, but you can't always do that:

	class J a b where ...
	instance J Int b where ...

	f :: forall a b. J a b => a -> a

(Notice: no functional dependency in J's class decl.)
Here f's type is perfectly fine, provided f is only called at Int.
It's premature to complain when meeting f's signature, or even
when inferring a type for f.



However, we don't *need* to report ambiguity right away.  It'll always
show up at the call site.... and eventually at main, which needs special
treatment.  Nevertheless, reporting ambiguity promptly is an excellent thing.

So heres the plan.  We WARN about probable ambiguity if

	fv(Cq) is not a subset of  oclose(fv(T) union fv(G), C)

(all tested before quantification).
That is, all the type variables in Cq must be fixed by the the variables
in the environment, or by the variables in the type.  

Notice that we union before calling oclose.  Here's an example:

244
	class J a b c | a b -> c
245
246
247
	fv(G) = {a}

Is this ambiguous?
248
	forall b c. (J a b c) => b -> b
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376

Only if we union {a} from G with {b} from T before using oclose,
do we see that c is fixed.  

It's a bit vague exactly which C we should use for this oclose call.  If we 
don't fix enough variables we might complain when we shouldn't (see
the above nasty example).  Nothing will be perfect.  That's why we can
only issue a warning.


Can we ever be *certain* about ambiguity?  Yes: if there's a constraint

	c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY

then c is a "bubble"; there's no way it can ever improve, and it's 
certainly ambiguous.  UNLESS it is a constant (sigh).  And what about
the nasty example?

	class K x
	class H x y | x -> y
	instance H x y => K (x,y)

Is this type ambiguous?
	forall a b. (K (a,b), Eq b) => a -> a

Urk.  The (Eq b) looks "definitely ambiguous" but it isn't.  What we are after
is a "bubble" that's a set of constraints

	Cq = Ca union Cq'  st  fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY

Hence another idea.  To decide Q start with fv(T) and grow it
by transitive closure in Cq (no functional dependencies involved).
Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
The definitely-ambigous can then float out, and get smashed at top level
(which squashes out the constants, like Eq (T a) above)


	--------------------------------------	
		Notes on implicit parameters
	--------------------------------------	

Consider

	f x = ...?y...

Then we get an LIE like (?y::Int).  Doesn't constrain a type variable,
but we must nevertheless infer a type like

	f :: (?y::Int) => Int -> Int

so that f is passed the value of y at the call site.  Is this legal?
	
	f :: Int -> Int
	f x = x + ?y

Should f be overloaded on "?y" ?  Or does the type signature say that it
shouldn't be?  Our position is that it should be illegal.  Otherwise
you can change the *dynamic* semantics by adding a type signature:

	(let f x = x + ?y	-- f :: (?y::Int) => Int -> Int
 	 in (f 3, f 3 with ?y=5))  with ?y = 6

		returns (3+6, 3+5)
vs
	(let f :: Int -> Int 
	    f x = x + ?y
	 in (f 3, f 3 with ?y=5))  with ?y = 6

		returns (3+6, 3+6)

URK!  Let's not do this. So this is illegal:

	f :: Int -> Int
	f x = x + ?y

BOTTOM LINE: you *must* quantify over implicit parameters.


	--------------------------------------	
		Notes on principal types
	--------------------------------------	

    class C a where
      op :: a -> a
    
    f x = let g y = op (y::Int) in True

Here the principal type of f is (forall a. a->a)
but we'll produce the non-principal type
    f :: forall a. C Int => a -> a

	
%************************************************************************
%*									*
\subsection{tcSimplifyInfer}
%*									*
%************************************************************************

tcSimplify is called when we *inferring* a type.  Here's the overall game plan:

    1. Compute Q = grow( fvs(T), C )
    
    2. Partition C based on Q into Ct and Cq.  Notice that ambiguous 
       predicates will end up in Ct; we deal with them at the top level
    
    3. Try improvement, using functional dependencies
    
    4. If Step 3 did any unification, repeat from step 1
       (Unification can change the result of 'grow'.)

Note: we don't reduce dictionaries in step 2.  For example, if we have
Eq (a,b), we don't simplify to (Eq a, Eq b).  So Q won't be different 
after step 2.  However note that we may therefore quantify over more
type variables than we absolutely have to.

For the guts, we need a loop, that alternates context reduction and
improvement with unification.  E.g. Suppose we have

	class C x y | x->y where ...
    
and tcSimplify is called with:
	(C Int a, C Int b)
Then improvement unifies a with b, giving
	(C Int a, C Int a)

If we need to unify anything, we rattle round the whole thing all over
again. 

377
378

\begin{code}
379
tcSimplifyInfer
380
	:: SDoc 
381
382
383
384
385
386
387
	-> [TcTyVar]		-- fv(T); type vars 
	-> LIE			-- Wanted
	-> TcM ([TcTyVar],	-- Tyvars to quantify (zonked)
		LIE,		-- Free
		TcDictBinds,	-- Bindings
		[TcId])		-- Dict Ids that must be bound here (zonked)
\end{code}
388

389
390
391
392

\begin{code}
tcSimplifyInfer doc tau_tvs wanted_lie
  = inferLoop doc tau_tvs (lieToList wanted_lie)	`thenTc` \ (qtvs, frees, binds, irreds) ->
393
394

	-- Check for non-generalisable insts
395
396
    mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds)	`thenTc_`

397
    returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
398
399
400
401
402
403

inferLoop doc tau_tvs wanteds
  =   	-- Step 1
    zonkTcTyVarsAndFV tau_tvs		`thenNF_Tc` \ tau_tvs' ->
    mapNF_Tc zonkInst wanteds		`thenNF_Tc` \ wanteds' ->
    tcGetGlobalTyVars			`thenNF_Tc` \ gbl_tvs ->
404
    let
405
406
407
408
409
410
411
 	preds = predsOfInsts wanteds'
	qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
	
	try_me inst 	
	  | isFree qtvs inst  = Free
	  | isClassDict inst  = DontReduceUnlessConstant	-- Dicts
	  | otherwise	      = ReduceMe AddToIrreds		-- Lits and Methods
412
    in
413
414
415
416
417
		-- Step 2
    reduceContext doc try_me [] wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
	
		-- Step 3
    if no_improvement then
418
	returnTc (varSetElems qtvs, frees, binds, irreds)
419
    else
420
421
422
423
424
425
426
427
428
429
430
431
432
433
	-- If improvement did some unification, we go round again.  There
	-- are two subtleties:
	--   a) We start again with irreds, not wanteds
	-- 	Using an instance decl might have introduced a fresh type variable
	--	which might have been unified, so we'd get an infinite loop
	--	if we started again with wanteds!  See example [LOOP]
	--
	--   b) It's also essential to re-process frees, because unification
	--      might mean that a type variable that looked free isn't now.
	--
	-- Hence the (irreds ++ frees)

	inferLoop doc tau_tvs (irreds ++ frees)	`thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
	returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
434
\end{code}	
435

436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
Example [LOOP]

	class If b t e r | b t e -> r
	instance If T t e t
	instance If F t e e
	class Lte a b c | a b -> c where lte :: a -> b -> c
	instance Lte Z b T
	instance (Lte a b l,If l b a c) => Max a b c

Wanted:	Max Z (S x) y

Then we'll reduce using the Max instance to:
	(Lte Z (S x) l, If l (S x) Z y)
and improve by binding l->T, after which we can do some reduction 
on both the Lte and If constraints.  What we *can't* do is start again
with (Max Z (S x) y)!

453
454
455
456
457
458
\begin{code}
isFree qtvs inst
  =  not (tyVarsOfInst inst `intersectsVarSet` qtvs)	-- Constrains no quantified vars
  && null (getIPs inst)					-- And no implicit parameter involved
							-- (see "Notes on implicit parameters")
\end{code}
459

460

461
462
463
464
465
%************************************************************************
%*									*
\subsection{tcSimplifyCheck}
%*									*
%************************************************************************
466

467
@tcSimplifyCheck@ is used when we know exactly the set of variables
468
we are going to quantify over.  For example, a class or instance declaration.
469
470

\begin{code}
471
tcSimplifyCheck
472
	 :: SDoc 
473
474
	 -> [TcTyVar]		-- Quantify over these
	 -> [Inst]		-- Given
475
	 -> LIE			-- Wanted
476
	 -> TcM (LIE,		-- Free
477
		 TcDictBinds)	-- Bindings
478

479
480
tcSimplifyCheck doc qtvs givens wanted_lie
  = checkLoop doc qtvs givens (lieToList wanted_lie)	`thenTc` \ (frees, binds, irreds) ->
481

482
	-- Complain about any irreducible ones
483
    complainCheck doc givens irreds		`thenNF_Tc_`
484

485
	-- Done
486
    returnTc (mkLIE frees, binds)
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503

checkLoop doc qtvs givens wanteds
  =   	-- Step 1
    zonkTcTyVarsAndFV qtvs		`thenNF_Tc` \ qtvs' ->
    mapNF_Tc zonkInst givens		`thenNF_Tc` \ givens' ->
    mapNF_Tc zonkInst wanteds		`thenNF_Tc` \ wanteds' ->
    let
	      -- When checking against a given signature we always reduce
	      -- until we find a match against something given, or can't reduce
	try_me inst | isFree qtvs' inst  = Free
		    | otherwise          = ReduceMe AddToIrreds
    in
		-- Step 2
    reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
	
		-- Step 3
    if no_improvement then
504
	returnTc (frees, binds, irreds)
505
    else
506
507
	checkLoop doc qtvs givens' (irreds ++ frees)	`thenTc` \ (frees1, binds1, irreds1) ->
	returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
508
509
510
511
512

complainCheck doc givens irreds
  = mapNF_Tc zonkInst given_dicts			`thenNF_Tc` \ givens' ->
    mapNF_Tc (addNoInstanceErr doc given_dicts) irreds	`thenNF_Tc_`
    returnTc ()
513
  where
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
    given_dicts = filter isDict givens
	-- Filter out methods, which are only added to 
	-- the given set as an optimisation
\end{code}



%************************************************************************
%*									*
\subsection{tcSimplifyAndCheck}
%*									*
%************************************************************************

@tcSimplifyInferCheck@ is used when we know the consraints we are to simplify
against, but we don't know the type variables over which we are going to quantify.
529
530
This happens when we have a type signature for a mutually recursive
group.
531
532
533
534
535
536
537
538
539
540
541
542
543

\begin{code}
tcSimplifyInferCheck
	 :: SDoc 
	 -> [TcTyVar]		-- fv(T)
	 -> [Inst]		-- Given
	 -> LIE			-- Wanted
	 -> TcM ([TcTyVar],	-- Variables over which to quantify
		 LIE,		-- Free
		 TcDictBinds)	-- Bindings

tcSimplifyInferCheck doc tau_tvs givens wanted
  = inferCheckLoop doc tau_tvs givens (lieToList wanted)	`thenTc` \ (qtvs, frees, binds, irreds) ->
544

545
546
547
548
	-- Complain about any irreducible ones
    complainCheck doc givens irreds		`thenNF_Tc_`

	-- Done
549
    returnTc (qtvs, mkLIE frees, binds)
550

551
552
553
554
555
556
inferCheckLoop doc tau_tvs givens wanteds
  =   	-- Step 1
    zonkTcTyVarsAndFV tau_tvs		`thenNF_Tc` \ tau_tvs' ->
    mapNF_Tc zonkInst givens		`thenNF_Tc` \ givens' ->
    mapNF_Tc zonkInst wanteds		`thenNF_Tc` \ wanteds' ->
    tcGetGlobalTyVars			`thenNF_Tc` \ gbl_tvs ->
557

558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
    let
  	-- Figure out what we are going to generalise over
	-- You might think it should just be the signature tyvars,
	-- but in bizarre cases you can get extra ones
	-- 	f :: forall a. Num a => a -> a
	--	f x = fst (g (x, head [])) + 1
	--	g a b = (b,a)
	-- Here we infer g :: forall a b. a -> b -> (b,a)
	-- We don't want g to be monomorphic in b just because
	-- f isn't quantified over b.
	qtvs    = (tau_tvs' `unionVarSet` tyVarsOfInsts givens') `minusVarSet` gbl_tvs
			-- We could close gbl_tvs, but its not necessary for
			-- soundness, and it'll only affect which tyvars, not which 
			-- dictionaries, we quantify over

	      -- When checking against a given signature we always reduce
	      -- until we find a match against something given, or can't reduce
	try_me inst | isFree qtvs inst  = Free
		    | otherwise         = ReduceMe AddToIrreds
    in
		-- Step 2
    reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
	
		-- Step 3
    if no_improvement then
583
	returnTc (varSetElems qtvs, frees, binds, irreds)
584
    else
585
586
	inferCheckLoop doc tau_tvs givens' (irreds ++ frees)	`thenTc` \ (qtvs1, frees1, binds1, irreds1) ->
	returnTc (qtvs1, frees1, binds `AndMonoBinds` binds1, irreds1)
587
588
\end{code}

589
590
591
592
593
594
595

%************************************************************************
%*									*
\subsection{tcSimplifyToDicts}
%*									*
%************************************************************************

596
597
598
599
On the LHS of transformation rules we only simplify methods and constants,
getting dictionaries.  We want to keep all of them unsimplified, to serve
as the available stuff for the RHS of the rule.

600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
The same thing is used for specialise pragmas. Consider
	
	f :: Num a => a -> a
	{-# SPECIALISE f :: Int -> Int #-}
	f = ...

The type checker generates a binding like:

	f_spec = (f :: Int -> Int)

and we want to end up with

	f_spec = _inline_me_ (f Int dNumInt)

But that means that we must simplify the Method for f to (f Int dNumInt)! 
So tcSimplifyToDicts squeezes out all Methods.

617
\begin{code}
618
tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
619
tcSimplifyToDicts wanted_lie
620
621
622
  = simpleReduceLoop doc try_me wanteds		`thenTc` \ (frees, binds, irreds) ->
	-- Since try_me doesn't look at types, we don't need to 
	-- do any zonking, so it's safe to call reduceContext directly
623
    ASSERT( null frees )
624
625
    returnTc (irreds, binds)

626
  where
627
    doc = text "tcSimplifyToDicts"
628
    wanteds = lieToList wanted_lie
629
630
631
632
633
634

	-- Reduce methods and lits only; stop as soon as we get a dictionary
    try_me inst	| isDict inst = DontReduce
		| otherwise   = ReduceMe AddToIrreds
\end{code}

635

636
637
638
639
640
641
642
643
644
645
646
%************************************************************************
%*									*
\subsection{Filtering at a dynamic binding}
%*									*
%************************************************************************

When we have
	let ?x = R in B

we must discharge all the ?x constraints from B.  We also do an improvement
step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.  No need to iterate, though.
647
648

\begin{code}
649
650
651
652
653
654
655
656
tcSimplifyIPs :: [Name]		-- The implicit parameters bound here
	      -> LIE
	      -> TcM (LIE, TcDictBinds)
tcSimplifyIPs ip_names wanted_lie
  = simpleReduceLoop doc try_me wanteds	`thenTc` \ (frees, binds, irreds) ->
	-- The irreducible ones should be a subset of the implicit
	-- parameters we provided
    ASSERT( all here_ip irreds )
657
    returnTc (mkLIE frees, binds)
658
659
660
661
662
663
    
  where
    doc	    = text "tcSimplifyIPs" <+> ppr ip_names
    wanteds = lieToList wanted_lie
    ip_set  = mkNameSet ip_names
    here_ip ip = isDict ip && ip `instMentionsIPs` ip_set
664

665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
	-- Simplify any methods that mention the implicit parameter
    try_me inst | inst `instMentionsIPs` ip_set = ReduceMe AddToIrreds
		| otherwise		        = Free
\end{code}


%************************************************************************
%*									*
\subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
%*									*
%************************************************************************

When doing a binding group, we may have @Insts@ of local functions.
For example, we might have...
\begin{verbatim}
let f x = x + 1	    -- orig local function (overloaded)
    f.1 = f Int	    -- two instances of f
    f.2 = f Float
 in
    (f.1 5, f.2 6.7)
\end{verbatim}
The point is: we must drop the bindings for @f.1@ and @f.2@ here,
where @f@ is in scope; those @Insts@ must certainly not be passed
upwards towards the top-level.	If the @Insts@ were binding-ified up
there, they would have unresolvable references to @f@.

We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
For each method @Inst@ in the @init_lie@ that mentions one of the
@Ids@, we create a binding.  We return the remaining @Insts@ (in an
@LIE@), as well as the @HsBinds@ generated.

\begin{code}
bindInstsOfLocalFuns ::	LIE -> [TcId] -> TcM (LIE, TcMonoBinds)

bindInstsOfLocalFuns init_lie local_ids
  | null overloaded_ids 
	-- Common case
  = returnTc (init_lie, EmptyMonoBinds)

  | otherwise
  = simpleReduceLoop doc try_me wanteds		`thenTc` \ (frees, binds, irreds) -> 
    ASSERT( null irreds )
707
    returnTc (mkLIE frees, binds)
708
709
710
711
712
713
714
715
716
717
718
719
720
  where
    doc		     = text "bindInsts" <+> ppr local_ids
    wanteds	     = lieToList init_lie
    overloaded_ids   = filter is_overloaded local_ids
    is_overloaded id = case splitSigmaTy (idType id) of
			  (_, theta, _) -> not (null theta)

    overloaded_set = mkVarSet overloaded_ids	-- There can occasionally be a lot of them
						-- so it's worth building a set, so that 
						-- lookup (in isMethodFor) is faster

    try_me inst | isMethodFor overloaded_set inst = ReduceMe AddToIrreds
		| otherwise		          = Free
721
\end{code}
722

723

724
725
%************************************************************************
%*									*
726
\subsection{Data types for the reduction mechanism}
727
728
729
%*									*
%************************************************************************

730
731
The main control over context reduction is here

732
\begin{code}
733
data WhatToDo 
734
 = ReduceMe		  -- Try to reduce this
735
	NoInstanceAction  -- What to do if there's no such instance
736

737
738
739
740
 | DontReduce		  	-- Return as irreducible 

 | DontReduceUnlessConstant	-- Return as irreducible unless it can
				-- be reduced to a constant in one step
741

742
 | Free			  -- Return as free
743

744
data NoInstanceAction
745
746
  = Stop		-- Fail; no error message
			-- (Only used when tautology checking.)
747
748
749

  | AddToIrreds		-- Just add the inst to the irreductible ones; don't 
			-- produce an error message of any kind.
750
			-- It might be quite legitimate such as (Eq a)!
751
\end{code}
752
753
754
755



\begin{code}
756
757
type RedState = (Avails,	-- What's available
		 [Inst])	-- Insts for which try_me returned Free
758

759
type Avails = FiniteMap Inst Avail
760

761
data Avail
762
763
764
765
766
767
768
  = Irred		-- Used for irreducible dictionaries,
			-- which are going to be lambda bound

  | BoundTo TcId	-- Used for dictionaries for which we have a binding
			-- e.g. those "given" in a signature

  | NoRhs 		-- Used for Insts like (CCallable f)
769
770
771
			-- where no witness is required.

  | Rhs 		-- Used when there is a RHS 
772
773
	TcExpr	 	-- The RHS
	[Inst]		-- Insts free in the RHS; we need these too
774

775
776
pprAvails avails = vcat [ppr inst <+> equals <+> pprAvail avail
			| (inst,avail) <- fmToList avails ]
777
778
779
780

instance Outputable Avail where
    ppr = pprAvail

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
817
818
819
820
821
822
823
824
825
826
827
828
pprAvail NoRhs	      = text "<no rhs>"
pprAvail Irred	      = text "Irred"
pprAvail (BoundTo x)  = text "Bound to" <+> ppr x
pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
\end{code}

Extracting the bindings from a bunch of Avails.
The bindings do *not* come back sorted in dependency order.
We assume that they'll be wrapped in a big Rec, so that the
dependency analyser can sort them out later

The loop startes
\begin{code}
bindsAndIrreds :: Avails
	       -> [Inst]		-- Wanted
	       -> (TcDictBinds, 	-- Bindings
		   [Inst])		-- Irreducible ones

bindsAndIrreds avails wanteds
  = go avails EmptyMonoBinds [] wanteds
  where
    go avails binds irreds [] = (binds, irreds)

    go avails binds irreds (w:ws)
      = case lookupFM avails w of
	  Nothing    -> -- Free guys come out here
			-- (If we didn't do addFree we could use this as the
			--  criterion for free-ness, and pick up the free ones here too)
			go avails binds irreds ws

	  Just NoRhs -> go avails binds irreds ws

	  Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws

	  Just (BoundTo id) -> go avails new_binds irreds ws
			    where
				-- For implicit parameters, all occurrences share the same
				-- Id, so there is no need for synonym bindings
			       new_binds | new_id == id = binds
					 | otherwise	= binds `AndMonoBinds` new_bind
			       new_bind = VarMonoBind new_id (HsVar id)
			       new_id   = instToId w

	  Just (Rhs rhs ws') -> go avails' (binds `AndMonoBinds` new_bind) irreds (ws' ++ ws)
			     where
				id	 = instToId w
				avails'  = addToFM avails w (BoundTo id)
				new_bind = VarMonoBind id rhs
829
830
831
832
833
\end{code}


%************************************************************************
%*									*
834
\subsection[reduce]{@reduce@}
835
%*									*
836
837
%************************************************************************

838
839
840
841
842
When the "what to do" predicate doesn't depend on the quantified type variables,
matters are easier.  We don't need to do any zonking, unless the improvement step
does something, in which case we zonk before iterating.

The "given" set is always empty.
843

844
\begin{code}
845
846
847
simpleReduceLoop :: SDoc
	 	 -> (Inst -> WhatToDo)		-- What to do, *not* based on the quantified type variables
		 -> [Inst]			-- Wanted
848
		 -> TcM ([Inst],		-- Free
849
850
851
852
853
854
855
856
857
			 TcDictBinds,
			 [Inst])		-- Irreducible

simpleReduceLoop doc try_me wanteds
  = mapNF_Tc zonkInst wanteds			`thenNF_Tc` \ wanteds' ->
    reduceContext doc try_me [] wanteds'	`thenTc` \ (no_improvement, frees, binds, irreds) ->
    if no_improvement then
	returnTc (frees, binds, irreds)
    else
858
859
	simpleReduceLoop doc try_me (irreds ++ frees)	`thenTc` \ (frees1, binds1, irreds1) ->
	returnTc (frees1, binds `AndMonoBinds` binds1, irreds1)
860
\end{code}	
861

862
863
864
865
866
867
868
869


\begin{code}
reduceContext :: SDoc
	      -> (Inst -> WhatToDo)
	      -> [Inst]			-- Given
	      -> [Inst]			-- Wanted
	      -> NF_TcM (Bool, 		-- True <=> improve step did no unification
870
			 [Inst],	-- Free
871
872
873
874
875
			 TcDictBinds,	-- Dictionary bindings
			 [Inst])	-- Irreducible

reduceContext doc try_me givens wanteds
  =
876
    traceTc (text "reduceContext" <+> (vcat [
877
	     text "----------------------",
878
	     doc,
879
880
881
	     text "given" <+> ppr givens,
	     text "wanted" <+> ppr wanteds,
	     text "----------------------"
882
883
	     ]))					`thenNF_Tc_`

884
        -- Build the Avail mapping from "givens"
885
    foldlNF_Tc addGiven (emptyFM, []) givens		`thenNF_Tc` \ init_state ->
886
887

        -- Do the real work
888
889
890
891
892
    reduceList (0,[]) try_me wanteds init_state		`thenNF_Tc` \ state@(avails, frees) ->

	-- Do improvement, using everything in avails
	-- In particular, avails includes all superclasses of everything
    tcImprove avails					`thenTc` \ no_improvement ->
893

894
    traceTc (text "reduceContext end" <+> (vcat [
895
	     text "----------------------",
896
	     doc,
897
898
899
	     text "given" <+> ppr givens,
	     text "wanted" <+> ppr wanteds,
	     text "----", 
900
	     text "avails" <+> pprAvails avails,
901
	     text "frees" <+> ppr frees,
902
	     text "no_improvement =" <+> ppr no_improvement,
903
	     text "----------------------"
904
905
906
907
	     ])) 					`thenNF_Tc_`
     let
	(binds, irreds) = bindsAndIrreds avails wanteds
     in
908
     returnTc (no_improvement, frees, binds, irreds)
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923

tcImprove avails
 =  tcGetInstEnv 				`thenTc` \ inst_env ->
    let
	preds = predsOfInsts (keysFM avails)
		-- Avails has all the superclasses etc (good)
		-- It also has all the intermediates of the deduction (good)
		-- It does not have duplicates (good)
		-- NB that (?x::t1) and (?x::t2) will be held separately in avails
		--    so that improve will see them separate
	eqns  = improve (classInstEnv inst_env) preds
     in
     if null eqns then
	returnTc True
     else
924
925
	traceTc (ptext SLIT("Improve:") <+> vcat (map ppr_eqn eqns))	`thenNF_Tc_`
        mapTc_ unify eqns	`thenTc_`
926
	returnTc False
927
928
929
930
931
  where
    unify (qtvs, t1, t2) = tcInstTyVars (varSetElems qtvs)	`thenNF_Tc` \ (_, _, tenv) ->
			   unifyTauTy (substTy tenv t1) (substTy tenv t2)
    ppr_eqn (qtvs, t1, t2) = ptext SLIT("forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)) <+>
			     ppr t1 <+> equals <+> ppr t2
932
\end{code}
933

934
935
936
The main context-reduction function is @reduce@.  Here's its game plan.

\begin{code}
937
938
939
940
reduceList :: (Int,[Inst])		-- Stack (for err msgs)
					-- along with its depth
       	   -> (Inst -> WhatToDo)
       	   -> [Inst]
941
942
       	   -> RedState
       	   -> TcM RedState
943
944
945
946
947
948
949
950
951
952
953
\end{code}

@reduce@ is passed
     try_me:	given an inst, this function returns
		  Reduce       reduce this
		  DontReduce   return this in "irreds"
		  Free	       return this in "frees"

     wanteds:	The list of insts to reduce
     state:	An accumulating parameter of type RedState 
		that contains the state of the algorithm
954
 
955
956
  It returns a RedState.

957
958
959
960
The (n,stack) pair is just used for error reporting.  
n is always the depth of the stack.
The stack is the stack of Insts being reduced: to produce X
I had to produce Y, to produce Y I had to produce Z, and so on.
961
962

\begin{code}
963
964
965
reduceList (n,stack) try_me wanteds state
  | n > opt_MaxContextReductionDepth
  = failWithTc (reduceDepthErr n stack)
966

967
968
969
  | otherwise
  =
#ifdef DEBUG
970
   (if n > 8 then
971
972
973
974
975
976
977
978
979
980
	pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
    else (\x->x))
#endif
    go wanteds state
  where
    go []     state = returnTc state
    go (w:ws) state = reduce (n+1, w:stack) try_me w state	`thenTc` \ state' ->
		      go ws state'

    -- Base case: we're done!
981
reduce stack try_me wanted state
982
    -- It's the same as an existing inst, or a superclass thereof
983
984
  | isAvailable state wanted
  = returnTc state
985

986
987
988
  | otherwise
  = case try_me wanted of {

989
      DontReduce -> addIrred state wanted
990

991
992
993
    ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
  				     -- First, see if the inst can be reduced to a constant in one step
	try_simple addIrred
994

995
996
997
    ; Free ->	-- It's free so just chuck it upstairs
  		-- First, see if the inst can be reduced to a constant in one step
	try_simple addFree
998

999
1000
1001
1002
1003
1004
    ; ReduceMe no_instance_action ->	-- It should be reduced
	lookupInst wanted	      `thenNF_Tc` \ lookup_result ->
	case lookup_result of
	    GenInst wanteds' rhs -> reduceList stack try_me wanteds' state	`thenTc` \ state' -> 
				    addWanted state' wanted rhs wanteds'
	    SimpleInst rhs       -> addWanted state wanted rhs []
1005

1006
1007
1008
1009
	    NoInstance ->    -- No such instance! 
		    case no_instance_action of
			Stop        -> failTc		
			AddToIrreds -> addIrred state wanted
1010

1011
1012
1013
1014
1015
1016
1017
1018
    }
  where
    try_simple do_this_otherwise
      = lookupInst wanted	  `thenNF_Tc` \ lookup_result ->
	case lookup_result of
	    SimpleInst rhs -> addWanted state wanted rhs []
	    other	   -> do_this_otherwise state wanted
\end{code}
1019
1020
1021


\begin{code}
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
isAvailable :: RedState -> Inst -> Bool
isAvailable (avails, _) wanted = wanted `elemFM` avails
	-- NB: the Ord instance of Inst compares by the class/type info
	-- *not* by unique.  So 
	--	d1::C Int ==  d2::C Int

-------------------------
addFree :: RedState -> Inst -> NF_TcM RedState
	-- When an Inst is tossed upstairs as 'free' we nevertheless add it
	-- to avails, so that any other equal Insts will be commoned up right
	-- here rather than also being tossed upstairs.  This is really just
	-- an optimisation, and perhaps it is more trouble that it is worth,
	-- as the following comments show!
	--
	-- NB1: do *not* add superclasses.  If we have
	--	df::Floating a
	--	dn::Num a
	-- but a is not bound here, then we *don't* want to derive 
	-- dn from df here lest we lose sharing.
	--
	-- NB2: do *not* add the Inst to avails at all if it's a method.
	-- The following situation shows why this is bad:
	--	truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
	-- From an application (truncate f i) we get
	--	t1 = truncate at f 
	--	t2 = t1 at i
	-- If we have also have a second occurrence of truncate, we get
	--	t3 = truncate at f
	--	t4 = t3 at i
	-- When simplifying with i,f free, we might still notice that
	--   t1=t3; but alas, the binding for t2 (which mentions t1)
	--   will continue to float out!
	-- Solution: never put methods in avail till they are captured
	-- in which case addFree isn't used
	--
	-- NB3: make sure that CCallable/CReturnable use NoRhs rather
	--	than BoundTo, else we end up with bogus bindings.
	--	c.f. instBindingRequired in addWanted
addFree (avails, frees) free
  | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
  | otherwise   = returnNF_Tc (avails,			  free:frees)
  where
    avail | instBindingRequired free = BoundTo (instToId free)
	  | otherwise		     = NoRhs

addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
addWanted state@(avails, frees) wanted rhs_expr wanteds
-- Do *not* add superclasses as well.  Here's an example of why not
-- 	class Eq a => Foo a b 
--	instance Eq a => Foo [a] a
-- If we are reducing
--	(Foo [t] t)
-- we'll first deduce that it holds (via the instance decl).  We  
-- must not then overwrite the Eq t constraint with a superclass selection!
-- 	ToDo: this isn't entirely unsatisfactory, because
--	      we may also lose some entirely-legitimate sharing this way

1079
  = ASSERT( not (isAvailable state wanted) )
1080
    returnNF_Tc (addToFM avails wanted avail, frees)
1081
1082
1083
1084
  where 
    avail | instBindingRequired wanted = Rhs rhs_expr wanteds
	  | otherwise		       = ASSERT( null wanteds ) NoRhs

1085
1086
1087
1088
1089
1090
addGiven :: RedState -> Inst -> NF_TcM RedState
addGiven state given = add_avail state given (BoundTo (instToId given))

addIrred :: RedState -> Inst -> NF_TcM RedState
addIrred state irred = add_avail state irred Irred

1091
1092
1093
1094
1095
1096
1097
1098
1099
add_avail :: RedState -> Inst -> Avail -> NF_TcM RedState
add_avail (avails, frees) wanted avail
  = addAvail avails wanted avail	`thenNF_Tc` \ avails' ->
    returnNF_Tc (avails', frees)

---------------------
addAvail :: Avails -> Inst -> Avail -> NF_TcM Avails
addAvail avails wanted avail
  = addSuperClasses (addToFM avails wanted avail) wanted
1100

1101
1102
1103
addSuperClasses :: Avails -> Inst -> NF_TcM Avails
	-- Add all the superclasses of the Inst to Avails
	-- Invariant: the Inst is already in Avails.
1104

1105
1106
1107
addSuperClasses avails dict
  | not (isClassDict dict)
  = returnNF_Tc avails
1108

1109
1110
1111
1112
1113
1114
1115
  | otherwise	-- It is a dictionary
  = newDictsFromOld dict sc_theta'	`thenNF_Tc` \ sc_dicts ->
    foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_dicts sc_sels)
  where
    (clas, tys) = getDictClassTys dict
    (tyvars, sc_theta, sc_sels, _) = classBigSig clas
    sc_theta' = substClasses (mkTopTyVarSubst tyvars tys) sc_theta
1116

1117
1118
1119
1120
1121
1122
1123
    add_sc avails (sc_dict, sc_sel)	-- Add it, and its superclasses
      = case lookupFM avails sc_dict of
	  Just (BoundTo _) -> returnNF_Tc avails	-- See Note [SUPER] below
	  other		   -> addAvail avails sc_dict avail
      where
	sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
	avail      = Rhs sc_sel_rhs [dict]
1124
\end{code}
1125

1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
Note [SUPER].  We have to be careful here.  If we are *given* d1:Ord a,
and want to deduce (d2:C [a]) where

	class Ord a => C a where
	instance Ord a => C [a] where ...

Then we'll use the instance decl to deduce C [a] and then add the 
superclasses of C [a] to avails.  But we must not overwrite the binding
for d1:Ord a (which is given) with a superclass selection or we'll just
build a loop!  Hence looking for BoundTo.  Crudely, BoundTo is cheaper
than a selection.

1138
1139
1140

%************************************************************************
%*									*
1141
\section{tcSimplifyTop: defaulting}
1142
1143
1144
1145
1146
%*									*
%************************************************************************


If a dictionary constrains a type variable which is
1147
1148
	* not mentioned in the environment
	* and not mentioned in the type of the expression
1149
1150
1151
1152
1153
1154
1155
then it is ambiguous. No further information will arise to instantiate
the type variable; nor will it be generalised and turned into an extra
parameter to a function.

It is an error for this to occur, except that Haskell provided for
certain rules to be applied in the special case of numeric types.
Specifically, if
1156
1157
	* at least one of its classes is a numeric class, and
	* all of its classes are numeric or standard
1158
1159
1160
1161
1162
1163
1164
1165
then the type variable can be defaulted to the first type in the
default-type list which is an instance of all the offending classes.

So here is the function which does the work.  It takes the ambiguous
dictionaries and either resolves them (producing bindings) or
complains.  It works by splitting the dictionary list by type
variable, and using @disambigOne@ to do the real business.

1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
@tcSimplifyTop@ is called once per module to simplify all the constant
and ambiguous Insts.

We need to be careful of one case.  Suppose we have

	instance Num a => Num (Foo a b) where ...

and @tcSimplifyTop@ is given a constraint (Num (Foo x y)).  Then it'll simplify
to (Num x), and default x to Int.  But what about y??  

It's OK: the final zonking stage should zap y to (), which is fine.
1177

1178
1179

\begin{code}
1180
tcSimplifyTop :: LIE -> TcM TcDictBinds
1181
tcSimplifyTop wanted_lie
1182
  = simpleReduceLoop (text "tcSimplTop") try_me wanteds	`thenTc` \ (frees, binds, irreds) ->
1183
    ASSERT( null frees )
1184

1185
1186
1187
1188
1189
1190
1191
1192
1193
    let
		-- All the non-std ones are definite errors
	(stds, non_stds) = partition isStdClassTyVarDict irreds
	
		-- Group by type variable
	std_groups = equivClasses cmp_by_tyvar stds

		-- Pick the ones which its worth trying to disambiguate
	(std_oks, std_bads) = partition worth_a_try std_groups
1194

1195
1196
1197
		-- Have a try at disambiguation 
		-- if the type variable isn't bound
		-- up with one of the non-standard classes
1198
	worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
1199
	non_std_tyvars		= unionVarSets (map tyVarsOfInst non_stds)
1200
1201
1202
1203
1204
1205

		-- Collect together all the bad guys
	bad_guys = non_stds ++ concat std_bads
    in
	-- Disambiguate the ones that look feasible
    mapTc disambigGroup std_oks		`thenTc` \ binds_ambig ->
1206

1207
	-- And complain about the ones that don't
1208
    addTopAmbigErrs bad_guys		`thenNF_Tc_`
1209

1210
    returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
1211
  where
1212
    wanteds	= lieToList wanted_lie
1213
    try_me inst	= ReduceMe AddToIrreds
1214
1215

    d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
1216

1217
1218
1219
1220
get_tv d   = case getDictClassTys d of
		   (clas, [ty]) -> getTyVar "tcSimplifyTop" ty
get_clas d = case getDictClassTys d of
		   (clas, [ty]) -> clas
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
\end{code}

@disambigOne@ assumes that its arguments dictionaries constrain all
the same type variable.

ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
@()@ instead of @Int@.  I reckon this is the Right Thing to do since
the most common use of defaulting is code like:
\begin{verbatim}
	_ccall_ foo	`seqPrimIO` bar
\end{verbatim}
Since we're not using the result of @foo@, the result if (presumably)
@void@.

\begin{code}
1236
disambigGroup :: [Inst]	-- All standard classes of form (C a)
1237
	      -> TcM TcDictBinds
1238

1239
disambigGroup dicts
sof's avatar
sof committed
1240
1241
1242
1243
1244
  |   any isNumericClass classes 	-- Guaranteed all standard classes
	  -- see comment at the end of function for reasons as to 
	  -- why the defaulting mechanism doesn't apply to groups that
	  -- include CCallable or CReturnable dicts.
   && not (any isCcallishClass classes)
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
  = 	-- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
	-- SO, TRY DEFAULT TYPES IN ORDER

	-- Failure here is caused by there being no type in the
	-- default list which can satisfy all the ambiguous classes.
	-- For example, if Real a is reqd, but the only type in the
	-- default list is Int.
    tcGetDefaultTys			`thenNF_Tc` \ default_tys ->
    let
      try_default [] 	-- No defaults work, so fail
1255
	= failTc
1256
1257

      try_default (default_ty : default_tys)
1258
	= tryTc_ (try_default default_tys) $	-- If default_ty fails, we try
1259
						-- default_tys instead
1260
	  tcSimplifyCheckThetas [] thetas	`thenTc` \ _ ->
1261
1262
	  returnTc default_ty
        where
1263
	  thetas = classes `zip` repeat [default_ty]
1264
1265
    in
	-- See if any default works, and if so bind the type variable to it
1266
	-- If not, add an AmbigErr
1267
    recoverTc (addAmbigErrs dicts `thenNF_Tc_` returnTc EmptyMonoBinds)	$
1268
1269
1270
1271

    try_default default_tys		 	`thenTc` \ chosen_default_ty ->

	-- Bind the type variable and reduce the context, for real this time
1272
    unifyTauTy chosen_default_ty (mkTyVarTy tyvar)	`thenTc_`
1273
1274
    simpleReduceLoop (text "disambig" <+> ppr dicts)
		     try_me dicts			`thenTc` \ (frees, binds, ambigs) ->
1275
    WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
1276
    warnDefault dicts chosen_default_ty			`thenTc_`
1277
    returnTc binds
1278

sof's avatar
sof committed
1279
  | all isCreturnableClass classes
1280
  = 	-- Default CCall stuff to (); we don't even both to check that () is an 
sof's avatar
sof committed
1281
	-- instance of CReturnable, because we know it is.
1282
1283
    unifyTauTy (mkTyVarTy tyvar) unitTy    `thenTc_`
    returnTc EmptyMonoBinds
1284
1285
    
  | otherwise -- No defaults
1286
  = addAmbigErrs dicts	`thenNF_Tc_`
1287
    returnTc EmptyMonoBinds
1288

1289
  where
1290
    try_me inst = ReduceMe AddToIrreds		-- This reduce should not fail
1291
1292
    tyvar       = get_tv (head dicts)		-- Should be non-empty
    classes     = map get_clas dicts
1293
1294
\end{code}

sof's avatar
sof committed
1295
1296
[Aside - why the defaulting mechanism is turned off when
 dealing with arguments and results to ccalls.
1297

sof's avatar
sof committed
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
When typechecking _ccall_s, TcExpr ensures that the external
function is only passed arguments (and in the other direction,
results) of a restricted set of 'native' types. This is
implemented via the help of the pseudo-type classes,
@CReturnable@ (CR) and @CCallable@ (CC.)
 
The interaction between the defaulting mechanism for numeric
values and CC & CR can be a bit puzzling to the user at times.
For example,

    x <- _ccall_ f
    if (x /= 0) then
       _ccall_ g x
     else
       return ()

What type has 'x' got here? That depends on the default list
in operation, if it is equal to Haskell 98's default-default
of (Integer, Double), 'x' has type Double, since Integer
is not an instance of CR. If the default list is equal to
Haskell 1.4's default-default of (Int, Double), 'x' has type
Int. 

To try to minimise the potential for surprises here, the
defaulting mechanism is turned off in the presence of
CCallable and CReturnable.

]
1326

1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459

%************************************************************************
%*									*
\subsection[simple]{@Simple@ versions}
%*									*
%************************************************************************

Much simpler versions when there are no bindings to make!

@tcSimplifyThetas@ simplifies class-type constraints formed by
@deriving@ declarations and when specialising instances.  We are
only interested in the simplified bunch of class/type constraints.

It simplifies to constraints of the form (C a b c) where
a,b,c are type variables.  This is required for the context of
instance declarations.

\begin{code}
tcSimplifyThetas :: ClassContext		-- Wanted
	       	 -> TcM ClassContext		-- Needed

tcSimplifyThetas wanteds
  = doptsTc Opt_GlasgowExts 		`thenNF_Tc` \ glaExts ->
    reduceSimple [] wanteds		`thenNF_Tc` \ irreds ->
    let
	-- For multi-param Haskell, check that the returned dictionaries
 	-- don't have any of the form (C Int Bool) for which
	-- we expect an instance here
	-- For Haskell 98, check that all the constraints are of the form C a,
	-- where a is a type variable
    	bad_guys | glaExts   = [ct | ct@(clas,tys) <- irreds, 
				     isEmptyVarSet (tyVarsOfTypes tys)]
		 | otherwise = [ct | ct@(clas,tys) <- irreds, 
				     not (all isTyVarTy tys)]
    in
    if null bad_guys then
	returnTc irreds
    else
       mapNF_Tc addNoInstErr bad_guys		`thenNF_Tc_`
       failTc
\end{code}

@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
used with \tr{default} declarations.  We are only interested in
whether it worked or not.

\begin{code}
tcSimplifyCheckThetas :: ClassContext	-- Given
		      -> ClassContext	-- Wanted
		      -> TcM ()

tcSimplifyCheckThetas givens wanteds
  = reduceSimple givens wanteds    `thenNF_Tc`	\ irreds ->
    if null irreds then
       returnTc ()
    else
       mapNF_Tc addNoInstErr irreds		`thenNF_Tc_`
       failTc
\end{code}


\begin{code}
type AvailsSimple = FiniteMap (Class,[Type]) Bool
		    -- True  => irreducible 
		    -- False => given, or can be derived from a given or from an irreducible

reduceSimple :: ClassContext			-- Given
	     -> ClassContext			-- Wanted
	     -> NF_TcM ClassContext		-- Irreducible

reduceSimple givens wanteds
  = reduce_simple (0,[]) givens_fm wanteds	`thenNF_Tc` \ givens_fm' ->
    returnNF_Tc [ct | (ct,True) <- fmToList givens_fm']
  where
    givens_fm     = foldl addNonIrred emptyFM givens

reduce_simple :: (Int,ClassContext)		-- Stack
	      -> AvailsSimple
	      -> ClassContext
	      -> NF_TcM AvailsSimple

reduce_simple (n,stack) avails wanteds
  = go avails wanteds
  where
    go avails []     = returnNF_Tc avails
    go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w	`thenNF_Tc` \ avails' ->
		       go avails' ws

reduce_simple_help stack givens wanted@(clas,tys)
  | wanted `elemFM` givens
  = returnNF_Tc givens

  | otherwise
  = lookupSimpleInst clas tys	`thenNF_Tc` \ maybe_theta ->

    case maybe_theta of
      Nothing ->    returnNF_Tc (addSimpleIrred givens wanted)
      Just theta -> reduce_simple stack (addNonIrred givens wanted) theta

addSimpleIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
addSimpleIrred givens ct@(clas,tys)
  = addSCs (addToFM givens ct True) ct

addNonIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
addNonIrred givens ct@(clas,tys)
  = addSCs (addToFM givens ct False) ct

addSCs givens ct@(clas,tys)
 = foldl add givens sc_theta
 where
   (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
   sc_theta = substClasses (mkTopTyVarSubst tyvars tys) sc_theta_tmpl

   add givens ct@(clas, tys)
     = case lookupFM givens ct of
       Nothing    -> -- Add it and its superclasses
		     addSCs (addToFM givens ct False) ct

       Just True  -> -- Set its flag to False; superclasses already done
		     addToFM givens ct False

       Just False -> -- Already done
		     givens
			   
\end{code}


%************************************************************************
%*									*
\section{Errors and contexts}
%*									*
%************************************************************************

1460
1461
1462
1463
1464
ToDo: for these error messages, should we note the location as coming
from the insts, or just whatever seems to be around in the monad just
now?

\begin{code}
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
addTopAmbigErrs dicts
  = mapNF_Tc complain tidy_dicts
  where
    fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
    (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
    complain d | not (null (getIPs d))		      = addTopIPErr tidy_env d
	       | tyVarsOfInst d `subVarSet` fixed_tvs = addTopInstanceErr tidy_env d
	       | otherwise			      = addAmbigErr tidy_env d

addTopIPErr tidy_env tidy_dict
  = addInstErrTcM (instLoc tidy_dict) 
	(tidy_env, 
	 ptext SLIT("Unbound implicit parameter") <+> quotes (pprInst tidy_dict))

-- Used for top-level irreducibles
addTopInstanceErr tidy_env tidy_dict
  = addInstErrTcM (instLoc tidy_dict) 
	(tidy_env, 
	 ptext SLIT("No instance for") <+> quotes (pprInst tidy_dict))
1484

1485
1486
1487
1488
addAmbigErrs dicts
  = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
  where
    (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
1489

1490
1491
addAmbigErr tidy_env tidy_dict
  = addInstErrTcM (instLoc tidy_dict)
1492
	(tidy_env,
1493
	 sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
1494
	      nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
1495
  where
1496
    ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
1497

1498
warnDefault dicts default_ty
1499
1500
1501
1502
  = doptsTc Opt_WarnTypeDefaults  `thenTc` \ warn_flag ->
    if warn_flag 
	then mapNF_Tc warn groups  `thenNF_Tc_`  returnNF_Tc ()
	else returnNF_Tc ()
1503
1504

  where
1505
	-- Tidy them first
1506
1507
    (_, tidy_dicts) = mapAccumL tidyInst emptyTidyEnv dicts

1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
	-- Group the dictionaries by source location
    groups      = equivClasses cmp tidy_dicts
    i1 `cmp` i2 = get_loc i1 `compare` get_loc i2
    get_loc i   = case instLoc i of { (_,loc,_) -> loc }

    warn [dict] = tcAddSrcLoc (get_loc dict) $
		  warnTc True (ptext SLIT("Defaulting") <+> quotes (pprInst dict) <+> 
			       ptext SLIT("to type") <+> quotes (ppr default_ty))

    warn dicts  = tcAddSrcLoc (get_loc (head dicts)) $
		  warnTc True (vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+> quotes (ppr default_ty),
				     pprInstsInFull dicts])

1521
1522
1523
1524
1525
-- The error message when we don't find a suitable instance
-- is complicated by the fact that sometimes this is because
-- there is no instance, and sometimes it's because there are
-- too many instances (overlap).  See the comments in TcEnv.lhs
-- with the InstEnv stuff.
1526
addNoInstanceErr what_doc givens dict
1527
1528
  = tcGetInstEnv	`thenNF_Tc` \ inst_env ->
    let
1529
1530
    	doc = vcat [sep [herald <+> quotes (pprInst tidy_dict),
			 nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
		    ambig_doc,
		    ptext SLIT("Probable fix:"),
		    nest 4 fix1,
		    nest 4 fix2]
    
    	herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
    	unambig_doc | ambig_overlap = ptext SLIT("unambiguously")	
		    | otherwise     = empty
    
    	ambig_doc 
	    | not ambig_overlap = empty
	    | otherwise 	    
	    = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
		    nest 4 (ptext SLIT("depends on the instantiation of") <+> 
			    quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst tidy_dict))))]
    
    	fix1 = sep [ptext SLIT("Add") <+> quotes (pprInst tidy_dict),
1548
		    ptext SLIT("to the") <+> what_doc]
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
    
    	fix2 | isTyVarDict dict || ambig_overlap
	     = empty
	     | otherwise
	     = ptext SLIT("Or add an instance declaration for") <+> quotes (pprInst tidy_dict)
    
    	(tidy_env, tidy_dict:tidy_givens) = tidyInsts emptyTidyEnv (dict:givens)
    
	    -- Checks for the ambiguous case when we have overlapping instances
    	ambig_overlap | isClassDict dict
		      = case lookupInstEnv inst_env clas tys of
			    NoMatch ambig -> ambig
			    other 	  -> False
		      | otherwise = False
		      where
    			(clas,tys) = getDictClassTys dict
    in
    addInstErrTcM (instLoc dict) (tidy_env, doc)
1567

1568
1569
-- Used for the ...Thetas variants; all top level
addNoInstErr (c,ts)
1570
  = addErrTc (ptext SLIT("No instance for") <+> quotes (pprClassPred c ts))
1571
1572
1573
1574
1575
1576
1577

reduceDepthErr n stack
  = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
	  ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
	  nest 4 (pprInstsInFull stack)]

reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
1578
1579
1580
1581
1582

-----------------------------------------------
addCantGenErr inst
  = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"), 
		   nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])
1583
\end{code}