TcMType.lhs 45.7 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
%
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
\section{Monadic type operations}

This module contains monadic operations over types that contain mutable type variables

\begin{code}
module TcMType (
  TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcRhoType, TcTyVarSet,

  --------------------------------
  -- Creating new mutable type variables
  newTyVar,
  newTyVarTy,		-- Kind -> NF_TcM TcType
  newTyVarTys,		-- Int -> Kind -> NF_TcM [TcType]
  newKindVar, newKindVars, newBoxityVar,

  --------------------------------
  -- Instantiation
  tcInstTyVar, tcInstTyVars,
  tcInstSigVars, tcInstType,
  tcSplitRhoTyM,

25
26
27
28
29
  --------------------------------
  -- Checking type validity
  Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
  SourceTyCtxt(..), checkValidTheta,

30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
  --------------------------------
  -- Unification
  unifyTauTy, unifyTauTyList, unifyTauTyLists, 
  unifyFunTy, unifyListTy, unifyTupleTy,
  unifyKind, unifyKinds, unifyOpenTypeKind,

  --------------------------------
  -- Zonking
  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
  zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
  zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,

  ) where

#include "HsVersions.h"


-- friends:
48
49
import TypeRep		( Type(..), SourceType(..), TyNote(..),	 -- Friend; can see representation
			  Kind, TauType, ThetaType, 
50
51
			  openKindCon, typeCon
			) 
52
import TcType		( tcEqType, tcCmpPred,
53
			  tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
54
			  tcSplitTyConApp_maybe, tcSplitFunTy_maybe, tcSplitForAllTys,
55
			  tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, isUnLiftedType, isIPPred,
56
57

			  mkAppTy, mkTyVarTy, mkTyVarTys, mkFunTy, mkTyConApp,
58
			  tyVarsOfPred,
59
60
61
62

			  liftedTypeKind, unliftedTypeKind, openTypeKind, defaultKind, superKind,
			  superBoxity, liftedBoxity, hasMoreBoxityInfo, typeKind,
			  tyVarsOfType, tyVarsOfTypes, tidyOpenType, tidyOpenTypes, tidyTyVar,
63
			  eqKind, isTypeKind
64
65
			)
import Subst		( Subst, mkTopTyVarSubst, substTy )
66
67
68
import Class		( classArity, className )
import TyCon		( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon, 
			  isTupleTyCon, tyConArity, tupleTyConBoxity, tyConName )
69
70
71
72
73
74
75
import PrimRep		( PrimRep(VoidRep) )
import Var		( TyVar, varName, tyVarKind, tyVarName, isTyVar, mkTyVar,
			  isMutTyVar, isSigTyVar )

-- others:
import TcMonad          -- TcType, amongst others
import TysWiredIn	( voidTy, listTyCon, mkListTy, mkTupleTy )
76
77
import FunDeps		( grow )
import PprType		( pprPred, pprSourceType, pprTheta )
78
79
80
81
82
import Name		( Name, NamedThing(..), setNameUnique, mkSysLocalName,
			  mkLocalName, mkDerivedTyConOcc, isSystemName
			)
import VarSet
import BasicTypes	( Boxity, Arity, isBoxed )
83
import CmdLineOpts	( dopt, DynFlag(..) )
84
import Unique		( Uniquable(..) )
85
86
import SrcLoc		( noSrcLoc )
import Util		( nOfThem )
87
import ListSetOps	( removeDups )
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
import Outputable
\end{code}


%************************************************************************
%*									*
\subsection{New type variables}
%*									*
%************************************************************************

\begin{code}
newTyVar :: Kind -> NF_TcM TcTyVar
newTyVar kind
  = tcGetUnique 	`thenNF_Tc` \ uniq ->
    tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind

newTyVarTy  :: Kind -> NF_TcM TcType
newTyVarTy kind
  = newTyVar kind	`thenNF_Tc` \ tc_tyvar ->
    returnNF_Tc (TyVarTy tc_tyvar)

newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)

newKindVar :: NF_TcM TcKind
newKindVar
  = tcGetUnique 						`thenNF_Tc` \ uniq ->
    tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind	`thenNF_Tc` \ kv ->
    returnNF_Tc (TyVarTy kv)

newKindVars :: Int -> NF_TcM [TcKind]
newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())

newBoxityVar :: NF_TcM TcKind
newBoxityVar
  = tcGetUnique 						`thenNF_Tc` \ uniq ->
    tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity	`thenNF_Tc` \ kv ->
    returnNF_Tc (TyVarTy kv)
\end{code}


%************************************************************************
%*									*
\subsection{Type instantiation}
%*									*
%************************************************************************

I don't understand why this is needed
An old comments says "No need for tcSplitForAllTyM because a type 
	variable can't be instantiated to a for-all type"
But the same is true of rho types!

\begin{code}
tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
tcSplitRhoTyM t
  = go t t []
 where
	-- A type variable is never instantiated to a dictionary type,
	-- so we don't need to do a tcReadVar on the "arg".
    go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
					Just pair -> go res res (pair:ts)
					Nothing   -> returnNF_Tc (reverse ts, syn_t)
    go syn_t (NoteTy n t)    ts = go syn_t t ts
151
    go syn_t (TyVarTy tv)    ts = getTcTyVar tv		`thenNF_Tc` \ maybe_ty ->
152
				  case maybe_ty of
153
154
				    Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
				    other			   -> returnNF_Tc (reverse ts, syn_t)
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
    go syn_t (UsageTy _ t)   ts = go syn_t t ts
    go syn_t t		     ts = returnNF_Tc (reverse ts, syn_t)
\end{code}


%************************************************************************
%*									*
\subsection{Type instantiation}
%*									*
%************************************************************************

Instantiating a bunch of type variables

\begin{code}
tcInstTyVars :: [TyVar] 
	     -> NF_TcM ([TcTyVar], [TcType], Subst)

tcInstTyVars tyvars
  = mapNF_Tc tcInstTyVar tyvars	`thenNF_Tc` \ tc_tyvars ->
    let
	tys = mkTyVarTys tc_tyvars
    in
    returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
		-- Since the tyvars are freshly made,
		-- they cannot possibly be captured by
		-- any existing for-alls.  Hence mkTopTyVarSubst

tcInstTyVar tyvar
  = tcGetUnique 		`thenNF_Tc` \ uniq ->
    let
	name = setNameUnique (tyVarName tyvar) uniq
	-- Note that we don't change the print-name
	-- This won't confuse the type checker but there's a chance
	-- that two different tyvars will print the same way 
	-- in an error message.  -dppr-debug will show up the difference
	-- Better watch out for this.  If worst comes to worst, just
	-- use mkSysLocalName.
    in
    tcNewMutTyVar name (tyVarKind tyvar)

tcInstSigVars tyvars	-- Very similar to tcInstTyVar
  = tcGetUniques 	`thenNF_Tc` \ uniqs ->
    listTc [ ASSERT( not (kind `eqKind` openTypeKind) )	-- Shouldn't happen
	     tcNewSigTyVar name kind 
	   | (tyvar, uniq) <- tyvars `zip` uniqs,
	     let name = setNameUnique (tyVarName tyvar) uniq, 
	     let kind = tyVarKind tyvar
	   ]
\end{code}

@tcInstType@ instantiates the outer-level for-alls of a TcType with
fresh type variables, splits off the dictionary part, and returns the results.

\begin{code}
tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
tcInstType ty
211
  = case tcSplitForAllTys ty of
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
	([],     rho) -> 	-- There may be overloading but no type variables;
				-- 	(?x :: Int) => Int -> Int
			 let
			   (theta, tau) = tcSplitRhoTy rho	-- Used to be tcSplitRhoTyM
			 in
			 returnNF_Tc ([], theta, tau)

	(tyvars, rho) -> tcInstTyVars tyvars			`thenNF_Tc` \ (tyvars', _, tenv)  ->
			 let
			   (theta, tau) = tcSplitRhoTy (substTy tenv rho)	-- Used to be tcSplitRhoTyM
			 in
			 returnNF_Tc (tyvars', theta, tau)
\end{code}



%************************************************************************
%*									*
\subsection{Putting and getting  mutable type variables}
%*									*
%************************************************************************

\begin{code}
235
236
putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
237
238
239
240
241
\end{code}

Putting is easy:

\begin{code}
242
putTcTyVar tyvar ty 
243
  | not (isMutTyVar tyvar)
244
  = pprTrace "putTcTyVar" (ppr tyvar) $
245
246
247
248
249
250
251
252
253
254
255
256
    returnNF_Tc ty

  | otherwise
  = ASSERT( isMutTyVar tyvar )
    UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
    tcWriteMutTyVar tyvar (Just ty)	`thenNF_Tc_`
    returnNF_Tc ty
\end{code}

Getting is more interesting.  The easy thing to do is just to read, thus:

\begin{verbatim}
257
getTcTyVar tyvar = tcReadMutTyVar tyvar
258
259
260
261
262
263
264
265
266
\end{verbatim}

But it's more fun to short out indirections on the way: If this
version returns a TyVar, then that TyVar is unbound.  If it returns
any other type, then there might be bound TyVars embedded inside it.

We return Nothing iff the original box was unbound.

\begin{code}
267
getTcTyVar tyvar
268
  | not (isMutTyVar tyvar)
269
  = pprTrace "getTcTyVar" (ppr tyvar) $
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
    returnNF_Tc (Just (mkTyVarTy tyvar))

  | otherwise
  = ASSERT2( isMutTyVar tyvar, ppr tyvar )
    tcReadMutTyVar tyvar				`thenNF_Tc` \ maybe_ty ->
    case maybe_ty of
	Just ty -> short_out ty				`thenNF_Tc` \ ty' ->
		   tcWriteMutTyVar tyvar (Just ty')	`thenNF_Tc_`
		   returnNF_Tc (Just ty')

	Nothing	   -> returnNF_Tc Nothing

short_out :: TcType -> NF_TcM TcType
short_out ty@(TyVarTy tyvar)
  | not (isMutTyVar tyvar)
  = returnNF_Tc ty

  | otherwise
  = tcReadMutTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
    case maybe_ty of
	Just ty' -> short_out ty' 			`thenNF_Tc` \ ty' ->
		    tcWriteMutTyVar tyvar (Just ty')	`thenNF_Tc_`
		    returnNF_Tc ty'

	other    -> returnNF_Tc ty

short_out other_ty = returnNF_Tc other_ty
\end{code}


%************************************************************************
%*									*
\subsection{Zonking -- the exernal interfaces}
%*									*
%************************************************************************

-----------------  Type variables

\begin{code}
zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars

zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars	`thenNF_Tc` \ tys ->
			   returnNF_Tc (tyVarsOfTypes tys)

zonkTcTyVar :: TcTyVar -> NF_TcM TcType
zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar

zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
-- This guy is to zonk the tyvars we're about to feed into tcSimplify
-- Usually this job is done by checkSigTyVars, but in a couple of places
-- that is overkill, so we use this simpler chap
zonkTcSigTyVars tyvars
  = zonkTcTyVars tyvars	`thenNF_Tc` \ tys ->
325
    returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
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
\end{code}

-----------------  Types

\begin{code}
zonkTcType :: TcType -> NF_TcM TcType
zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty

zonkTcTypes :: [TcType] -> NF_TcM [TcType]
zonkTcTypes tys = mapNF_Tc zonkTcType tys

zonkTcClassConstraints cts = mapNF_Tc zonk cts
    where zonk (clas, tys)
	    = zonkTcTypes tys	`thenNF_Tc` \ new_tys ->
	      returnNF_Tc (clas, new_tys)

zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta

zonkTcPredType :: TcPredType -> NF_TcM TcPredType
zonkTcPredType (ClassP c ts) =
    zonkTcTypes ts	`thenNF_Tc` \ new_ts ->
    returnNF_Tc (ClassP c new_ts)
zonkTcPredType (IParam n t) =
    zonkTcType t	`thenNF_Tc` \ new_t ->
    returnNF_Tc (IParam n new_t)
\end{code}

-------------------  These ...ToType, ...ToKind versions
		     are used at the end of type checking

\begin{code}
zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
zonkKindEnv pairs 
  = mapNF_Tc zonk_it pairs
 where
    zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
			      returnNF_Tc (name, kind)

	-- When zonking a kind, we want to
	--	zonk a *kind* variable to (Type *)
	--	zonk a *boxity* variable to *
368
369
    zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind   = putTcTyVar kv liftedTypeKind
			     | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
370
371
372
373
374
375
376
377
			     | otherwise		 	 = pprPanic "zonkKindEnv" (ppr kv)
			
zonkTcTypeToType :: TcType -> NF_TcM Type
zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
  where
	-- Zonk a mutable but unbound type variable to
	--	Void		if it has kind Lifted
	--	:Void		otherwise
378
379
380
381
382
	-- We know it's unbound even though we don't carry an environment,
	-- because at the binding site for a type variable we bind the
	-- mutable tyvar to a fresh immutable one.  So the mutable store
	-- plays the role of an environment.  If we come across a mutable
	-- type variable that isn't so bound, it must be completely free.
383
384
    zonk_unbound_tyvar tv
	| kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
385
	= putTcTyVar tv voidTy	-- Just to avoid creating a new tycon in
386
387
				-- this vastly common case
	| otherwise
388
	= putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
	where
	  kind = tyVarKind tv

    mk_void_tycon tv kind	-- Make a new TyCon with the same kind as the 
				-- type variable tv.  Same name too, apart from
				-- making it start with a colon (sigh)
		-- I dread to think what will happen if this gets out into an 
		-- interface file.  Catastrophe likely.  Major sigh.
	= pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
	  mkPrimTyCon tc_name kind 0 [] VoidRep
	where
	  tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc

-- zonkTcTyVarToTyVar is applied to the *binding* occurrence 
-- of a type variable, at the *end* of type checking.  It changes
-- the *mutable* type variable into an *immutable* one.
-- 
-- It does this by making an immutable version of tv and binds tv to it.
-- Now any bound occurences of the original type variable will get 
-- zonked to the immutable version.

zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
zonkTcTyVarToTyVar tv
  = let
		-- Make an immutable version, defaulting 
		-- the kind to lifted if necessary
	immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
	immut_tv_ty = mkTyVarTy immut_tv

418
        zap tv = putTcTyVar tv immut_tv_ty
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
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
466
467
468
469
470
471
472
473
474
		-- Bind the mutable version to the immutable one
    in 
	-- If the type variable is mutable, then bind it to immut_tv_ty
	-- so that all other occurrences of the tyvar will get zapped too
    zonkTyVar zap tv		`thenNF_Tc` \ ty2 ->

    WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )

    returnNF_Tc immut_tv
\end{code}


%************************************************************************
%*									*
\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
%*									*
%*		For internal use only!					*
%*									*
%************************************************************************

\begin{code}
-- zonkType is used for Kinds as well

-- For unbound, mutable tyvars, zonkType uses the function given to it
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
--	type variable and zonks the kind too

zonkType :: (TcTyVar -> NF_TcM Type) 	-- What to do with unbound mutable type variables
					-- see zonkTcType, and zonkTcTypeToType
	 -> TcType
	 -> NF_TcM Type
zonkType unbound_var_fn ty
  = go ty
  where
    go (TyConApp tycon tys)	  = mapNF_Tc go tys	`thenNF_Tc` \ tys' ->
				    returnNF_Tc (TyConApp tycon tys')

    go (NoteTy (SynNote ty1) ty2) = go ty1		`thenNF_Tc` \ ty1' ->
				    go ty2		`thenNF_Tc` \ ty2' ->
				    returnNF_Tc (NoteTy (SynNote ty1') ty2')

    go (NoteTy (FTVNote _) ty2)   = go ty2	-- Discard free-tyvar annotations

    go (SourceTy p)		  = go_pred p		`thenNF_Tc` \ p' ->
				    returnNF_Tc (SourceTy p')

    go (FunTy arg res)      	  = go arg		`thenNF_Tc` \ arg' ->
				    go res		`thenNF_Tc` \ res' ->
				    returnNF_Tc (FunTy arg' res')
 
    go (AppTy fun arg)	 	  = go fun		`thenNF_Tc` \ fun' ->
				    go arg		`thenNF_Tc` \ arg' ->
				    returnNF_Tc (mkAppTy fun' arg')

    go (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
                                    go ty               `thenNF_Tc` \ ty' ->
475
                                    returnNF_Tc (UsageTy u' ty')
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500

	-- The two interesting cases!
    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar

    go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar	`thenNF_Tc` \ tyvar' ->
			     go ty			`thenNF_Tc` \ ty' ->
			     returnNF_Tc (ForAllTy tyvar' ty')

    go_pred (ClassP c tys) = mapNF_Tc go tys	`thenNF_Tc` \ tys' ->
			     returnNF_Tc (ClassP c tys')
    go_pred (NType tc tys) = mapNF_Tc go tys	`thenNF_Tc` \ tys' ->
			     returnNF_Tc (NType tc tys')
    go_pred (IParam n ty) = go ty		`thenNF_Tc` \ ty' ->
			    returnNF_Tc (IParam n ty')

zonkTyVar :: (TcTyVar -> NF_TcM Type)		-- What to do for an unbound mutable variable
	  -> TcTyVar -> NF_TcM TcType
zonkTyVar unbound_var_fn tyvar 
  | not (isMutTyVar tyvar)	-- Not a mutable tyvar.  This can happen when
				-- zonking a forall type, when the bound type variable
				-- needn't be mutable
  = ASSERT( isTyVar tyvar )		-- Should not be any immutable kind vars
    returnNF_Tc (TyVarTy tyvar)

  | otherwise
501
  =  getTcTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
502
503
504
505
506
507
508
509
510
     case maybe_ty of
	  Nothing	-> unbound_var_fn tyvar			-- Mutable and unbound
	  Just other_ty	-> zonkType unbound_var_fn other_ty	-- Bound
\end{code}



%************************************************************************
%*									*
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
\subsection{Checking a user type}
%*									*
%************************************************************************

When dealing with a user-written type, we first translate it from an HsType
to a Type, performing kind checking, and then check various things that should 
be true about it.  We don't want to perform these checks at the same time
as the initial translation because (a) they are unnecessary for interface-file
types and (b) when checking a mutually recursive group of type and class decls,
we can't "look" at the tycons/classes yet.

One thing we check for is 'rank'.  

	Rank 0: 	monotypes (no foralls)
	Rank 1:		foralls at the front only, Rank 0 inside
	Rank 2:		foralls at the front, Rank 1 on left of fn arrow,

	basic ::= tyvar | T basic ... basic

	r2  ::= forall tvs. cxt => r2a
	r2a ::= r1 -> r2a | basic
	r1  ::= forall tvs. cxt => r0
	r0  ::= r0 -> r0 | basic
	

\begin{code}
data UserTypeCtxt 
  = FunSigCtxt Name	-- Function type signature
  | ExprSigCtxt		-- Expression type signature
  | ConArgCtxt Name	-- Data constructor argument
  | TySynCtxt Name	-- RHS of a type synonym decl
  | GenPatCtxt		-- Pattern in generic decl
			-- 	f{| a+b |} (Inl x) = ...
  | PatSigCtxt		-- Type sig in pattern
			-- 	f (x::t) = ...
  | ResSigCtxt		-- Result type sig
			-- 	f x :: t = ....
  | ForSigCtxt Name	-- Foreign inport or export signature
549
550
551
552
553
554
555
556
557
558
559
  | RuleSigCtxt Name 	-- Signature on a forall'd variable in a RULE

pprUserTypeCtxt (FunSigCtxt n) 	= ptext SLIT("the type signature for") <+> quotes (ppr n)
pprUserTypeCtxt ExprSigCtxt    	= ptext SLIT("an expression type signature")
pprUserTypeCtxt (ConArgCtxt c) 	= ptext SLIT("the type of constructor") <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c)  	= ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
pprUserTypeCtxt GenPatCtxt     	= ptext SLIT("the type pattern of a generic definition")
pprUserTypeCtxt PatSigCtxt     	= ptext SLIT("a pattern type signature")
pprUserTypeCtxt ResSigCtxt     	= ptext SLIT("a result type signature")
pprUserTypeCtxt (ForSigCtxt n) 	= ptext SLIT("the foreign signature for") <+> quotes (ppr n)
pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
\end{code}

\begin{code}
checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context
checkValidType ctxt ty
  = doptsTc Opt_GlasgowExts	`thenNF_Tc` \ gla_exts ->
    let 
	rank = case ctxt of
		 GenPatCtxt		  -> 0
		 PatSigCtxt		  -> 0
		 ResSigCtxt		  -> 0
		 ExprSigCtxt 	          -> 1
		 FunSigCtxt _ | gla_exts  -> 2
			      | otherwise -> 1
		 ConArgCtxt _ | gla_exts  -> 2	-- We are given the type of the entire
			      | otherwise -> 1	-- constructor; hence rank 1 is ok
		 TySynCtxt _  | gla_exts  -> 1
			      | otherwise -> 0
		 ForSigCtxt _		  -> 1
580
		 RuleSigCtxt _		  -> 1
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671

	actual_kind = typeKind ty

	actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind

	kind_ok = case ctxt of
			TySynCtxt _  -> True	-- Any kind will do
			GenPatCtxt   -> actual_kind_is_lifted
			ForSigCtxt _ -> actual_kind_is_lifted
			other	     -> isTypeKind actual_kind
    in
    tcAddErrCtxt (checkTypeCtxt ctxt ty)	$

	-- Check that the thing has kind Type, and is lifted if necessary
    checkTc kind_ok (kindErr actual_kind)	`thenTc_`

	-- Check the internal validity of the type itself
    check_poly_type rank ty

-- Notes re TySynCtxt
-- We allow type synonyms that aren't types; e.g.  type List = []
--
-- If the RHS mentions tyvars that aren't in scope, we'll 
-- quantify over them:
--	e.g. 	type T = a->a
-- will become	type T = forall a. a->a
--
-- With gla-exts that's right, but for H98 we should complain. 


----------------------------------------
type Rank = Int
check_poly_type :: Rank -> Type -> TcM ()
check_poly_type rank ty 
  | rank == 0 
  = check_tau_type 0 False ty
  | otherwise	-- rank > 0
  = let
	(tvs, theta, tau) = tcSplitSigmaTy ty
    in
    check_valid_theta SigmaCtxt theta	`thenTc_`
    check_tau_type (rank-1) False tau	`thenTc_`
    checkAmbiguity tvs theta tau

----------------------------------------
check_arg_type :: Type -> TcM ()
-- The sort of type that can instantiate a type variable,
-- or be the argument of a type constructor.
-- Not an unboxed tuple, not a forall.
-- Other unboxed types are very occasionally allowed as type
-- arguments depending on the kind of the type constructor
-- 
-- For example, we want to reject things like:
--
--	instance Ord a => Ord (forall s. T s a)
-- and
--	g :: T s (forall b.b)
--
-- NB: unboxed tuples can have polymorphic or unboxed args.
--     This happens in the workers for functions returning
--     product types with polymorphic components.
--     But not in user code
-- 
-- Question: what about nested unboxed tuples?
-- 	     Currently rejected.
check_arg_type ty 
  = check_tau_type 0 False ty	`thenTc_` 
    checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)

----------------------------------------
check_tau_type :: Rank -> Bool -> Type -> TcM ()
-- Rank is allowed rank for function args
-- No foralls otherwise
-- Bool is True iff unboxed tuple are allowed here

check_tau_type rank ubx_tup_ok ty@(UsageTy _ _)  = addErrTc (usageTyErr ty)
check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = addErrTc (forAllTyErr ty)
check_tau_type rank ubx_tup_ok (SourceTy sty)    = getDOptsTc		`thenNF_Tc` \ dflags ->
						   check_source_ty dflags TypeCtxt sty
check_tau_type rank ubx_tup_ok (TyVarTy _)       = returnTc ()
check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
  = check_poly_type rank      arg_ty	`thenTc_`
    check_tau_type  rank True res_ty

check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
  = check_arg_type ty1 `thenTc_` check_arg_type ty2

check_tau_type rank ubx_tup_ok (NoteTy note ty)
  = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty

check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
672
673
674
675
676
677
678
679
680
681
682
683
  | isSynTyCon tc
  = checkTc syn_arity_ok arity_msg	`thenTc_`
    mapTc_ check_arg_type tys
    
  | isUnboxedTupleTyCon tc
  = checkTc ubx_tup_ok ubx_tup_msg	`thenTc_`
    mapTc_ (check_tau_type 0 True) tys		-- Args are allowed to be unlifted, or
						-- more unboxed tuples, so can't use check_arg_ty

  | otherwise
  = mapTc_ check_arg_type tys

684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
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
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
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
  where
    syn_arity_ok = tc_arity <= n_args
		-- It's OK to have an *over-applied* type synonym
		--	data Tree a b = ...
		--	type Foo a = Tree [a]
		--	f :: Foo a b -> ...
    n_args    = length tys
    tc_arity  = tyConArity tc

    arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
    ubx_tup_msg = ubxArgTyErr ty

----------------------------------------
check_note (FTVNote _)  = returnTc ()
check_note (SynNote ty) = check_tau_type 0 False ty
\end{code}


\begin{code}
data SourceTyCtxt
  = ClassSCCtxt Name	-- Superclasses of clas
  | SigmaCtxt		-- Context of a normal for-all type
  | DataTyCtxt Name	-- Context of a data decl
  | TypeCtxt 		-- Source type in an ordinary type
  | InstDeclCtxt	-- Context of an instance decl
		
pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
pprSourceTyCtxt InstDeclCtxt    = ptext SLIT("the context of an instance declaration")
pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
\end{code}

\begin{code}
checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
checkValidTheta ctxt theta 
  = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)

-------------------------
check_valid_theta ctxt []
  = returnTc ()
check_valid_theta ctxt theta
  = getDOptsTc					`thenNF_Tc` \ dflags ->
    warnTc (not (null dups)) (dupPredWarn dups)	`thenNF_Tc_`
    mapTc_ (check_source_ty dflags ctxt) theta
  where
    (_,dups) = removeDups tcCmpPred theta

-------------------------
check_source_ty dflags ctxt pred@(ClassP cls tys)
  = 	-- Class predicates are valid in all contexts
    mapTc_ check_arg_type tys			`thenTc_`
    checkTc (arity == n_tys) arity_err		`thenTc_`
    checkTc (all tyvar_head tys || arby_preds_ok) (predTyVarErr pred)

  where
    class_name = className cls
    arity      = classArity cls
    n_tys      = length tys
    arity_err  = arityErr "Class" class_name arity n_tys

    arby_preds_ok = case ctxt of
			InstDeclCtxt -> dopt Opt_AllowUndecidableInstances dflags
			other	     -> dopt Opt_GlasgowExts               dflags

check_source_ty dflags SigmaCtxt (IParam name ty) = check_arg_type ty
check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys

-- Catch-all
check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)

-------------------------
tyvar_head ty			-- Haskell 98 allows predicates of form 
  | tcIsTyVarTy ty = True	-- 	C (a ty1 .. tyn)
  | otherwise			-- where a is a type variable
  = case tcSplitAppTy_maybe ty of
	Just (ty, _) -> tyvar_head ty
	Nothing	     -> False
\end{code}

Check for ambiguity
~~~~~~~~~~~~~~~~~~~
	  forall V. P => tau
is ambiguous if P contains generic variables
(i.e. one of the Vs) that are not mentioned in tau

However, we need to take account of functional dependencies
when we speak of 'mentioned in tau'.  Example:
	class C a b | a -> b where ...
Then the type
	forall x y. (C x y) => x
is not ambiguous because x is mentioned and x determines y

NOTE: In addition, GHC insists that at least one type variable
in each constraint is in V.  So we disallow a type like
	forall a. Eq b => b -> b
even in a scope where b is in scope.
This is the is_free test below.

NB; the ambiguity check is only used for *user* types, not for types
coming from inteface files.  The latter can legitimately have
ambiguous types. Example

   class S a where s :: a -> (Int,Int)
   instance S Char where s _ = (1,1)
   f:: S a => [a] -> Int -> (Int,Int)
   f (_::[a]) x = (a*x,b)
	where (a,b) = s (undefined::a)

Here the worker for f gets the type
	fw :: forall a. S a => Int -> (# Int, Int #)

If the list of tv_names is empty, we have a monotype, and then we
don't need to check for ambiguity either, because the test can't fail
(see is_ambig).

\begin{code}
checkAmbiguity :: [TyVar] -> ThetaType -> TauType -> TcM ()
checkAmbiguity forall_tyvars theta tau
  = mapTc_ check_pred theta	`thenTc_`
    returnTc ()
  where
    tau_vars	      = tyVarsOfType tau
    extended_tau_vars = grow theta tau_vars

    is_ambig ct_var   = (ct_var `elem` forall_tyvars) &&
		        not (ct_var `elemVarSet` extended_tau_vars)
    is_free ct_var    = not (ct_var `elem` forall_tyvars)
    
    check_pred pred = checkTc (not any_ambig)                 (ambigErr pred) `thenTc_`
	    	      checkTc (isIPPred pred || not all_free) (freeErr  pred)
             where 
	    	ct_vars	  = varSetElems (tyVarsOfPred pred)
	    	all_free  = all is_free ct_vars
	    	any_ambig = any is_ambig ct_vars
\end{code}


\begin{code}
ambigErr pred
  = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
	 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
		 ptext SLIT("must be reachable from the type after the =>"))]

freeErr pred
  = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
		   ptext SLIT("are already in scope"),
	 nest 4 (ptext SLIT("At least one must be universally quantified here"))
    ]

forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
usageTyErr      ty = ptext SLIT("Illegal usage type:") <+> ppr ty
unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)

checkTypeCtxt ctxt ty
  = vcat [ptext SLIT("In the type:") <+> ppr_ty,
	  ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
  where  
	-- Hack alert.  If there are no tyvars, (ppr sigma_ty) will print
	-- something strange like {Eq k} -> k -> k, because there is no
	-- ForAll at the top of the type.  Since this is going to the user
	-- we want it to look like a proper Haskell type even then; hence the hack
	-- 
	-- This shows up in the complaint about
	--	case C a where
	--	  op :: Eq a => a -> a
    ppr_ty | null forall_tyvars = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
	   | otherwise	 	= ppr ty
    (forall_tyvars, theta, tau) = tcSplitSigmaTy ty

checkThetaCtxt ctxt theta
  = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
	  ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
\end{code}


%************************************************************************
%*									*
\subsection{Kind unification}
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
%*									*
%************************************************************************

\begin{code}
unifyKind :: TcKind		    -- Expected
	  -> TcKind		    -- Actual
	  -> TcM ()
unifyKind k1 k2 
  = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
    uTys k1 k1 k2 k2

unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
unifyKinds []       []       = returnTc ()
unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 	`thenTc_`
			       unifyKinds ks1 ks2
unifyKinds _ _ = panic "unifyKinds: length mis-match"
\end{code}

\begin{code}
unifyOpenTypeKind :: TcKind -> TcM ()	
-- Ensures that the argument kind is of the form (Type bx)
-- for some boxity bx

unifyOpenTypeKind ty@(TyVarTy tyvar)
892
  = getTcTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
893
894
895
896
897
    case maybe_ty of
	Just ty' -> unifyOpenTypeKind ty'
	other	 -> unify_open_kind_help ty

unifyOpenTypeKind ty
898
899
  | isTypeKind ty = returnTc ()
  | otherwise     = unify_open_kind_help ty
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
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
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104

unify_open_kind_help ty	-- Revert to ordinary unification
  = newBoxityVar 	`thenNF_Tc` \ boxity ->
    unifyKind ty (mkTyConApp typeCon [boxity])
\end{code}


%************************************************************************
%*									*
\subsection[Unify-exported]{Exported unification functions}
%*									*
%************************************************************************

The exported functions are all defined as versions of some
non-exported generic functions.

Unify two @TauType@s.  Dead straightforward.

\begin{code}
unifyTauTy :: TcTauType -> TcTauType -> TcM ()
unifyTauTy ty1 ty2 	-- ty1 expected, ty2 inferred
  = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
    uTys ty1 ty1 ty2 ty2
\end{code}

@unifyTauTyList@ unifies corresponding elements of two lists of
@TauType@s.  It uses @uTys@ to do the real work.  The lists should be
of equal length.  We charge down the list explicitly so that we can
complain if their lengths differ.

\begin{code}
unifyTauTyLists :: [TcTauType] -> [TcTauType] ->  TcM ()
unifyTauTyLists [] 	     []	        = returnTc ()
unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2   `thenTc_`
					unifyTauTyLists tys1 tys2
unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
\end{code}

@unifyTauTyList@ takes a single list of @TauType@s and unifies them
all together.  It is used, for example, when typechecking explicit
lists, when all the elts should be of the same type.

\begin{code}
unifyTauTyList :: [TcTauType] -> TcM ()
unifyTauTyList []		 = returnTc ()
unifyTauTyList [ty]		 = returnTc ()
unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2	`thenTc_`
				   unifyTauTyList tys
\end{code}

%************************************************************************
%*									*
\subsection[Unify-uTys]{@uTys@: getting down to business}
%*									*
%************************************************************************

@uTys@ is the heart of the unifier.  Each arg happens twice, because
we want to report errors in terms of synomyms if poss.  The first of
the pair is used in error messages only; it is always the same as the
second, except that if the first is a synonym then the second may be a
de-synonym'd version.  This way we get better error messages.

We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.

\begin{code}
uTys :: TcTauType -> TcTauType	-- Error reporting ty1 and real ty1
				-- ty1 is the *expected* type

     -> TcTauType -> TcTauType	-- Error reporting ty2 and real ty2
				-- ty2 is the *actual* type
     -> TcM ()

	-- Always expand synonyms (see notes at end)
        -- (this also throws away FTVs)
uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2

	-- Ignore usage annotations inside typechecker
uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2

	-- Variables; go for uVar
uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True  tyvar2 ps_ty1 ty1
					-- "True" means args swapped

	-- Predicates
uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
  | n1 == n2 = uTys t1 t1 t2 t2
uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
  | c1 == c2 = unifyTauTyLists tys1 tys2
uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
  | tc1 == tc2 = unifyTauTyLists tys1 tys2

	-- Functions; just check the two parts
uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
  = uTys fun1 fun1 fun2 fun2	`thenTc_`    uTys arg1 arg1 arg2 arg2

	-- Type constructors must match
uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
  | con1 == con2 && length tys1 == length tys2
  = unifyTauTyLists tys1 tys2

  | con1 == openKindCon
	-- When we are doing kind checking, we might match a kind '?' 
	-- against a kind '*' or '#'.  Notably, CCallable :: ? -> *, and
	-- (CCallable Int) and (CCallable Int#) are both OK
  = unifyOpenTypeKind ps_ty2

	-- Applications need a bit of care!
	-- They can match FunTy and TyConApp, so use splitAppTy_maybe
	-- NB: we've already dealt with type variables and Notes,
	-- so if one type is an App the other one jolly well better be too
uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
  = case tcSplitAppTy_maybe ty2 of
	Just (s2,t2) -> uTys s1 s1 s2 s2	`thenTc_`    uTys t1 t1 t2 t2
	Nothing      -> unifyMisMatch ps_ty1 ps_ty2

	-- Now the same, but the other way round
	-- Don't swap the types, because the error messages get worse
uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
  = case tcSplitAppTy_maybe ty1 of
	Just (s1,t1) -> uTys s1 s1 s2 s2	`thenTc_`    uTys t1 t1 t2 t2
	Nothing      -> unifyMisMatch ps_ty1 ps_ty2

	-- Not expecting for-alls in unification
	-- ... but the error message from the unifyMisMatch more informative
	-- than a panic message!

	-- Anything else fails
uTys ps_ty1 ty1 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
\end{code}


Notes on synonyms
~~~~~~~~~~~~~~~~~
If you are tempted to make a short cut on synonyms, as in this
pseudocode...

\begin{verbatim}
-- NO	uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
-- NO     = if (con1 == con2) then
-- NO	-- Good news!  Same synonym constructors, so we can shortcut
-- NO	-- by unifying their arguments and ignoring their expansions.
-- NO	unifyTauTypeLists args1 args2
-- NO    else
-- NO	-- Never mind.  Just expand them and try again
-- NO	uTys ty1 ty2
\end{verbatim}

then THINK AGAIN.  Here is the whole story, as detected and reported
by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
\begin{quotation}
Here's a test program that should detect the problem:

\begin{verbatim}
	type Bogus a = Int
	x = (1 :: Bogus Char) :: Bogus Bool
\end{verbatim}

The problem with [the attempted shortcut code] is that
\begin{verbatim}
	con1 == con2
\end{verbatim}
is not a sufficient condition to be able to use the shortcut!
You also need to know that the type synonym actually USES all
its arguments.  For example, consider the following type synonym
which does not use all its arguments.
\begin{verbatim}
	type Bogus a = Int
\end{verbatim}

If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
would fail, even though the expanded forms (both \tr{Int}) should
match.

Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
unnecessarily bind \tr{t} to \tr{Char}.

... You could explicitly test for the problem synonyms and mark them
somehow as needing expansion, perhaps also issuing a warning to the
user.
\end{quotation}


%************************************************************************
%*									*
\subsection[Unify-uVar]{@uVar@: unifying with a type variable}
%*									*
%************************************************************************

@uVar@ is called when at least one of the types being unified is a
variable.  It does {\em not} assume that the variable is a fixed point
of the substitution; rather, notice that @uVar@ (defined below) nips
back into @uTys@ if it turns out that the variable is already bound.

\begin{code}
uVar :: Bool		-- False => tyvar is the "expected"
			-- True  => ty    is the "expected" thing
     -> TcTyVar
     -> TcTauType -> TcTauType	-- printing and real versions
     -> TcM ()

uVar swapped tv1 ps_ty2 ty2
1105
  = getTcTyVar tv1	`thenNF_Tc` \ maybe_ty1 ->
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
    case maybe_ty1 of
	Just ty1 | swapped   -> uTys ps_ty2 ty2 ty1 ty1	-- Swap back
		 | otherwise -> uTys ty1 ty1 ps_ty2 ty2	-- Same order
	other       -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2

	-- Expand synonyms; ignore FTVs
uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
  = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2


	-- The both-type-variable case
uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)

	-- Same type variable => no-op
  | tv1 == tv2
  = returnTc ()

	-- Distinct type variables
	-- ASSERT maybe_ty1 /= Just
  | otherwise
1126
  = getTcTyVar tv2	`thenNF_Tc` \ maybe_ty2 ->
1127
1128
1129
1130
1131
1132
    case maybe_ty2 of
	Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'

	Nothing | update_tv2

		-> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
1133
		   putTcTyVar tv2 (TyVarTy tv1)		`thenNF_Tc_`
1134
1135
1136
1137
		   returnTc ()
		|  otherwise

		-> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
1138
                   (putTcTyVar tv1 ps_ty2		`thenNF_Tc_`
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
	  	    returnTc ())
  where
    k1 = tyVarKind tv1
    k2 = tyVarKind tv2
    update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
			-- Try to get rid of open type variables as soon as poss

    nicer_to_update_tv2 =  isSigTyVar tv1 
				-- Don't unify a signature type variable if poss
			|| isSystemName (varName tv2)
				-- Try to update sys-y type variables in preference to sig-y ones

	-- Second one isn't a type variable
uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
  = 	-- Check that the kinds match
    checkKinds swapped tv1 non_var_ty2			`thenTc_`

	-- Check that tv1 isn't a type-signature type variable
    checkTcM (not (isSigTyVar tv1))
	     (failWithTcM (unifyWithSigErr tv1 ps_ty2))	`thenTc_`

	-- Check that we aren't losing boxity info (shouldn't happen)
    warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
	   ((ppr tv1 <+> ppr (tyVarKind tv1)) $$ 
	     (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2)))		`thenNF_Tc_` 

	-- Occurs check
	-- Basically we want to update     tv1 := ps_ty2
	-- because ps_ty2 has type-synonym info, which improves later error messages
	-- 
	-- But consider 
	--	type A a = ()
	--
	--	f :: (A a -> a -> ()) -> ()
	--	f = \ _ -> ()
	--
	-- 	x :: ()
	-- 	x = f (\ x p -> p x)
	--
	-- In the application (p x), we try to match "t" with "A t".  If we go
	-- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into 
	-- an infinite loop later.
 	-- But we should not reject the program, because A t = ().
	-- Rather, we should bind t to () (= non_var_ty2).
	-- 
	-- That's why we have this two-state occurs-check
    zonkTcType ps_ty2					`thenNF_Tc` \ ps_ty2' ->
    if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
1187
	putTcTyVar tv1 ps_ty2'				`thenNF_Tc_`
1188
1189
1190
1191
1192
1193
	returnTc ()
    else
    zonkTcType non_var_ty2				`thenNF_Tc` \ non_var_ty2' ->
    if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
	-- This branch rarely succeeds, except in strange cases
	-- like that in the example above
1194
	putTcTyVar tv1 non_var_ty2'			`thenNF_Tc_`
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
	returnTc ()
    else
    failWithTcM (unifyOccurCheck tv1 ps_ty2')


checkKinds swapped tv1 ty2
-- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
-- We need to check that we don't unify a lifted type variable with an
-- unlifted type: e.g.  (id 3#) is illegal
  | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
  = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)	$
    unifyMisMatch k1 k2
  | otherwise
  = returnTc ()
  where
    (k1,k2) | swapped   = (tk2,tk1)
	    | otherwise = (tk1,tk2)
    tk1 = tyVarKind tv1
    tk2 = typeKind ty2
\end{code}


%************************************************************************
%*									*
\subsection[Unify-fun]{@unifyFunTy@}
%*									*
%************************************************************************

@unifyFunTy@ is used to avoid the fruitless creation of type variables.

\begin{code}
unifyFunTy :: TcType	 			-- Fail if ty isn't a function type
	   -> TcM (TcType, TcType)	-- otherwise return arg and result types

unifyFunTy ty@(TyVarTy tyvar)
1230
  = getTcTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
    case maybe_ty of
	Just ty' -> unifyFunTy ty'
	other	    -> unify_fun_ty_help ty

unifyFunTy ty
  = case tcSplitFunTy_maybe ty of
	Just arg_and_res -> returnTc arg_and_res
	Nothing 	 -> unify_fun_ty_help ty

unify_fun_ty_help ty	-- Special cases failed, so revert to ordinary unification
  = newTyVarTy openTypeKind	`thenNF_Tc` \ arg ->
    newTyVarTy openTypeKind	`thenNF_Tc` \ res ->
    unifyTauTy ty (mkFunTy arg res)	`thenTc_`
    returnTc (arg,res)
\end{code}

\begin{code}
unifyListTy :: TcType              -- expected list type
	    -> TcM TcType      -- list element type

unifyListTy ty@(TyVarTy tyvar)
1252
  = getTcTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
    case maybe_ty of
	Just ty' -> unifyListTy ty'
	other	 -> unify_list_ty_help ty

unifyListTy ty
  = case tcSplitTyConApp_maybe ty of
	Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
	other					    -> unify_list_ty_help ty

unify_list_ty_help ty	-- Revert to ordinary unification
  = newTyVarTy liftedTypeKind		`thenNF_Tc` \ elt_ty ->
    unifyTauTy ty (mkListTy elt_ty)	`thenTc_`
    returnTc elt_ty
\end{code}

\begin{code}
unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
unifyTupleTy boxity arity ty@(TyVarTy tyvar)
1271
  = getTcTyVar tyvar	`thenNF_Tc` \ maybe_ty ->
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
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
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
    case maybe_ty of
	Just ty' -> unifyTupleTy boxity arity ty'
	other	 -> unify_tuple_ty_help boxity arity ty

unifyTupleTy boxity arity ty
  = case tcSplitTyConApp_maybe ty of
	Just (tycon, arg_tys)
		|  isTupleTyCon tycon 
		&& tyConArity tycon == arity
		&& tupleTyConBoxity tycon == boxity
		-> returnTc arg_tys
	other -> unify_tuple_ty_help boxity arity ty

unify_tuple_ty_help boxity arity ty
  = newTyVarTys arity kind				`thenNF_Tc` \ arg_tys ->
    unifyTauTy ty (mkTupleTy boxity arity arg_tys)	`thenTc_`
    returnTc arg_tys
  where
    kind | isBoxed boxity = liftedTypeKind
	 | otherwise      = openTypeKind
\end{code}


%************************************************************************
%*									*
\subsection[Unify-context]{Errors and contexts}
%*									*
%************************************************************************

Errors
~~~~~~

\begin{code}
unifyCtxt s ty1 ty2 tidy_env	-- ty1 expected, ty2 inferred
  = zonkTcType ty1	`thenNF_Tc` \ ty1' ->
    zonkTcType ty2	`thenNF_Tc` \ ty2' ->
    returnNF_Tc (err ty1' ty2')
  where
    err ty1 ty2 = (env1, 
		   nest 4 
			(vcat [
			   text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
			   text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
		        ]))
		  where
		    (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]

unifyKindCtxt swapped tv1 ty2 tidy_env	-- not swapped => tv1 expected, ty2 inferred
	-- tv1 is zonked already
  = zonkTcType ty2	`thenNF_Tc` \ ty2' ->
    returnNF_Tc (err ty2')
  where
    err ty2 = (env2, ptext SLIT("When matching types") <+> 
		     sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
	    where
	      (pp_expected, pp_actual) | swapped   = (pp2, pp1)
				       | otherwise = (pp1, pp2)
	      (env1, tv1') = tidyTyVar tidy_env tv1
	      (env2, ty2') = tidyOpenType  env1 ty2
	      pp1 = ppr tv1'
	      pp2 = ppr ty2'

unifyMisMatch ty1 ty2
  = zonkTcType ty1	`thenNF_Tc` \ ty1' ->
    zonkTcType ty2	`thenNF_Tc` \ ty2' ->
    let
    	(env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
	msg = hang (ptext SLIT("Couldn't match"))
		   4 (sep [quotes (ppr tidy_ty1), 
			   ptext SLIT("against"), 
			   quotes (ppr tidy_ty2)])
    in
    failWithTcM (env, msg)

unifyWithSigErr tyvar ty
  = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
	      4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
  where
    (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
    (env2, tidy_ty)    = tidyOpenType  env1     ty

unifyOccurCheck tyvar ty
  = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
	      4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
  where
    (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
    (env2, tidy_ty)    = tidyOpenType  env1     ty
\end{code}