Unify.lhs 16.6 KB
Newer Older
1
2
3
\begin{code}
module Unify ( 
	-- Matching and unification
4
	tcMatchTys, tcMatchTyX, tcMatchPreds, MatchEnv(..), 
5

6
	tcUnifyTys, 
7

8
9
	gadtRefineTys, BindFlag(..),

10
	coreRefineTys, TypeRefinement,
11
12
13
14
15
16
17
18
19
20
21

	-- Re-export
	MaybeErr(..)
   ) where

#include "HsVersions.h"

import Var		( Var, TyVar, tyVarKind )
import VarEnv
import VarSet
import Kind		( isSubKind )
22
import Type		( typeKind, tyVarsOfType, tyVarsOfTypes, tyVarsOfTheta, mkTyVarTys,
23
			  TvSubstEnv, emptyTvSubstEnv, TvSubst(..), substTy, tcEqTypeX )
24
import TypeRep          ( Type(..), PredType(..), funTyCon )
25
import DataCon 		( DataCon, dataConResTy )
26
27
28
29
30
31
32
33
34
import Util		( snocView )
import ErrUtils		( Message )
import Outputable
import Maybes
\end{code}


%************************************************************************
%*									*
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
		Matching
%*									*
%************************************************************************


Matching is much tricker than you might think.

1. The substitution we generate binds the *template type variables*
   which are given to us explicitly.

2. We want to match in the presence of foralls; 
	e.g 	(forall a. t1) ~ (forall b. t2)

   That is what the RnEnv2 is for; it does the alpha-renaming
   that makes it as if a and b were the same variable.
   Initialising the RnEnv2, so that it can generate a fresh
   binder when necessary, entails knowing the free variables of
   both types.

3. We must be careful not to bind a template type variable to a
   locally bound variable.  E.g.
	(forall a. x) ~ (forall b. b)
   where x is the template type variable.  Then we do not want to
   bind x to a/b!  This is a kind of occurs check.
   The necessary locals accumulate in the RnEnv2.


\begin{code}
data MatchEnv
  = ME	{ me_tmpls :: VarSet	-- Template tyvars
 	, me_env   :: RnEnv2	-- Renaming envt for nested foralls
	}			--   In-scope set includes template tyvars

68
tcMatchTys :: TyVarSet		-- Template tyvars
69
70
	 -> [Type]		-- Template
	 -> [Type]		-- Target
71
	 -> Maybe TvSubst	-- One-shot; in principle the template
72
73
				-- variables could be free in the target

74
tcMatchTys tmpls tys1 tys2
75
76
77
  = case match_tys menv emptyTvSubstEnv tys1 tys2 of
	Just subst_env -> Just (TvSubst in_scope subst_env)
	Nothing	       -> Nothing
78
  where
79
80
    menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
    in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
81
82
83
84
85
86
87
88
89
90
91
92
93
	-- We're assuming that all the interesting 
	-- tyvars in tys1 are in tmpls

tcMatchPreds
	:: [TyVar]			-- Bind these
	-> [PredType] -> [PredType]
   	-> Maybe TvSubstEnv
tcMatchPreds tmpls ps1 ps2
  = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
  where
    menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
    in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)

94
-- This one is called from the expression matcher, which already has a MatchEnv in hand
95
tcMatchTyX :: MatchEnv 
96
97
98
99
100
	 -> TvSubstEnv		-- Substitution to extend
	 -> Type		-- Template
	 -> Type		-- Target
	 -> Maybe TvSubstEnv

101
tcMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2	-- Rename for export
102
103
104
105
106
\end{code}

Now the internals of matching

\begin{code}
107
match :: MatchEnv	-- For the most part this is pushed downwards
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
      -> TvSubstEnv 	-- Substitution so far:
			--   Domain is subset of template tyvars
			--   Free vars of range is subset of 
			--	in-scope set of the RnEnv2
      -> Type -> Type	-- Template and target respectively
      -> Maybe TvSubstEnv
-- This matcher works on source types; that is, 
-- it respects NewTypes and PredType

match menv subst (NoteTy _ ty1) ty2 = match menv subst ty1 ty2
match menv subst ty1 (NoteTy _ ty2) = match menv subst ty1 ty2

match menv subst (TyVarTy tv1) ty2
  | tv1 `elemVarSet` me_tmpls menv
  = case lookupVarEnv subst tv1' of
	Nothing | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
		-> Nothing	-- Occurs check
125
126
		| not (typeKind ty2 `isSubKind` tyVarKind tv1)
		-> Nothing	-- Kind mis-match
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
		| otherwise
		-> Just (extendVarEnv subst tv1 ty2)

	Just ty1' | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
		-- ty1 has no locally-bound variables, hence nukeRnEnvL
		-- Note tcEqType...we are doing source-type matching here
		  -> Just subst

	other -> Nothing

   | otherwise	-- tv1 is not a template tyvar
   = case ty2 of
	TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
	other					-> Nothing
  where
    rn_env = me_env menv
    tv1' = rnOccL rn_env tv1

match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2) 
  = match menv' subst ty1 ty2
  where		-- Use the magic of rnBndr2 to go under the binders
    menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }

match menv subst (PredTy p1) (PredTy p2) 
  = match_pred menv subst p1 p2
match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
  | tc1 == tc2 = match_tys menv subst tys1 tys2
match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
  = do { subst' <- match menv subst ty1a ty2a
       ; match menv subst' ty1b ty2b }
match menv subst (AppTy ty1a ty1b) ty2
  | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
  = do { subst' <- match menv subst ty1a ty2a
       ; match menv subst' ty1b ty2b }

match menv subst ty1 ty2
  = Nothing

--------------
match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2

--------------
match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
	   -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
match_list fn subst []         []	  = Just subst
match_list fn subst (ty1:tys1) (ty2:tys2) = do	{ subst' <- fn subst ty1 ty2
						; match_list fn subst' tys1 tys2 }
match_list fn subst tys1       tys2 	  = Nothing	

--------------
match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
  | c1 == c2 = match_tys menv subst tys1 tys2
match_pred menv subst (IParam n1 t1) (IParam n2 t2)
  | n1 == n2 = match menv subst t1 t2
match_pred menv subst p1 p2 = Nothing
\end{code}


%************************************************************************
%*									*
187
		Unification
188
189
190
191
%*									*
%************************************************************************

\begin{code}
192
193
194
195
196
197
198
199
tcUnifyTys :: (TyVar -> BindFlag)
	   -> [Type] -> [Type]
	   -> Maybe TvSubst	-- A regular one-shot substitution
-- The two types may have common type variables, and indeed do so in the
-- second call to tcUnifyTys in FunDeps.checkClsFD
tcUnifyTys bind_fn tys1 tys2
  = maybeErrToMaybe $ initUM bind_fn $
    do { subst_env <- unify_tys emptyTvSubstEnv tys1 tys2
200

201
202
203
204
205
206
207
208
	-- Find the fixed point of the resulting non-idempotent substitution
	; let in_scope	      = mkInScopeSet (tvs1 `unionVarSet` tvs2)
	      subst  	      = TvSubst in_scope subst_env_fixpt
	      subst_env_fixpt = mapVarEnv (substTy subst) subst_env
	; return subst }
  where
    tvs1 = tyVarsOfTypes tys1
    tvs2 = tyVarsOfTypes tys2
209
210

----------------------------
211
212
213
214
215
216
217
218
219
220
221
222
223
224
coreRefineTys :: InScopeSet		-- Superset of free vars of either type
	      -> DataCon -> [TyVar]	-- Case pattern (con tv1 .. tvn ...)
	      -> Type			-- Type of scrutinee
	      -> Maybe TypeRefinement

type TypeRefinement = (TvSubstEnv, Bool)
	-- The Bool is True iff all the bindings in the 
	-- env are for the pattern type variables
	-- In this case, there is no type refinement 
	-- for already-in-scope type variables

-- Used by Core Lint and the simplifier.
coreRefineTys in_scope con tvs scrut_ty
  = maybeErrToMaybe $ initUM (tryToBind tv_set) $
225
    do	{ 	-- Run the unifier, starting with an empty env
226
	; subst_env <- unify emptyTvSubstEnv pat_res_ty scrut_ty
227
228
229
230

	-- Find the fixed point of the resulting non-idempotent substitution
	; let subst  	      = TvSubst in_scope subst_env_fixpt
	      subst_env_fixpt = mapVarEnv (substTy subst) subst_env
231
232
233
234
235
236
237
238
239
240
		
	; return (subst_env_fixpt, all_bound_here subst_env) }
  where
    pat_res_ty = dataConResTy con (mkTyVarTys tvs)

	-- 'tvs' are the tyvars bound by the pattern
    tv_set 	       = mkVarSet tvs
    all_bound_here env = all bound_here (varEnvKeys env)
    bound_here uniq    = elemVarSetByKey uniq tv_set
    
241
242

----------------------------
243
244
245
246
247
248
249
250
251
gadtRefineTys
	:: (TyVar -> BindFlag)		-- Try to unify these
	-> TvSubstEnv			-- Not idempotent
	-> [Type] -> [Type]
   	-> MaybeErr Message TvSubstEnv	-- Not idempotent
-- This one is used by the type checker.  Neither the input nor result
-- substitition is idempotent
gadtRefineTys bind_fn subst tys1 tys2
  = initUM bind_fn (unify_tys subst tys1 tys2)
252
253

----------------------------
254
tryToBind :: TyVarSet -> TyVar -> BindFlag
255
256
257
258
259
260
261
262
263
264
265
266
tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
		    | otherwise	             = AvoidMe
\end{code}


%************************************************************************
%*									*
		The workhorse
%*									*
%************************************************************************

\begin{code}
267
unify :: TvSubstEnv		-- An existing substitution to extend
268
269
270
271
272
273
274
      -> Type -> Type           -- Types to be unified
      -> UM TvSubstEnv		-- Just the extended substitution, 
				-- Nothing if unification failed
-- We do not require the incoming substitution to be idempotent,
-- nor guarantee that the outgoing one is.  That's fixed up by
-- the wrappers.

275
276
-- Respects newtypes, PredTypes

277
unify subst ty1 ty2 = -- pprTrace "unify" (ppr subst <+> pprParendType ty1 <+> pprParendType ty2) $
278
		      unify_ subst ty1 ty2
279

280
-- in unify_, any NewTcApps/Preds should be taken at face value
281
282
unify_ subst (TyVarTy tv1) ty2  = uVar False subst tv1 ty2
unify_ subst ty1 (TyVarTy tv2)  = uVar True  subst tv2 ty1
283

284
285
286
unify_ subst (NoteTy _ ty1) ty2  = unify subst ty1 ty2
unify_ subst ty1 (NoteTy _ ty2)  = unify subst ty1 ty2

287
unify_ subst (PredTy p1) (PredTy p2) = unify_pred subst p1 p2
288

289
290
unify_ subst t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2) 
  | tyc1 == tyc2 = unify_tys subst tys1 tys2
291

292
293
294
unify_ subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
  = do { subst' <- unify subst ty1a ty2a
       ; unify subst' ty1b ty2b }
295
296
297
298
299

	-- 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
300
301
302
303
unify_ subst (AppTy ty1a ty1b) ty2
  | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
  = do	{ subst' <- unify subst ty1a ty2a
        ; unify subst' ty1b ty2b }
304

305
306
307
308
unify_ subst ty1 (AppTy ty2a ty2b)
  | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
  = do	{ subst' <- unify subst ty1a ty2a
        ; unify subst' ty1b ty2b }
309

310
unify_ subst ty1 ty2 = failWith (misMatch ty1 ty2)
311
312

------------------------------
313
314
315
316
317
unify_pred subst (ClassP c1 tys1) (ClassP c2 tys2)
  | c1 == c2 = unify_tys subst tys1 tys2
unify_pred subst (IParam n1 t1) (IParam n2 t2)
  | n1 == n2 = unify subst t1 t2
unify_pred subst p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
318
319
 
------------------------------
320
unify_tys = unifyList unify
321
322
323
324
325
326
327
328
329
330
331
332
333

unifyList :: Outputable a 
	  => (TvSubstEnv -> a -> a -> UM TvSubstEnv)
	  -> TvSubstEnv -> [a] -> [a] -> UM TvSubstEnv
unifyList unifier subst orig_xs orig_ys
  = go subst orig_xs orig_ys
  where
    go subst []     []     = return subst
    go subst (x:xs) (y:ys) = do { subst' <- unifier subst x y
			        ; go subst' xs ys }
    go subst _      _      = failWith (lengthMisMatch orig_xs orig_ys)

------------------------------
334
uVar :: Bool            -- Swapped
335
336
337
338
339
     -> TvSubstEnv	-- An existing substitution to extend
     -> TyVar           -- Type variable to be unified
     -> Type            -- with this type
     -> UM TvSubstEnv

340
uVar swap subst tv1 ty
341
 = -- Check to see whether tv1 is refined by the substitution
342
   case (lookupVarEnv subst tv1) of
343
     -- Yes, call back into unify'
344
345
     Just ty' | swap      -> unify subst ty ty' 
              | otherwise -> unify subst ty' ty
346
     -- No, continue
347
     Nothing          -> uUnrefined subst tv1 ty ty
348
349
350
351
352


uUnrefined :: TvSubstEnv          -- An existing substitution to extend
           -> TyVar               -- Type variable to be unified
           -> Type                -- with this type
353
           -> Type                -- (de-noted version)
354
355
356
           -> UM TvSubstEnv

-- We know that tv1 isn't refined
357
358
359
360
361
362
363
364
365

uUnrefined subst tv1 ty2 (NoteTy _ ty2')
  = uUnrefined subst tv1 ty2 ty2'	-- Unwrap synonyms
		-- This is essential, in case we have
		--	type Foo a = a
		-- and then unify a :=: Foo a

uUnrefined subst tv1 ty2 (TyVarTy tv2)
  | tv1 == tv2		-- Same type variable
366
367
368
369
  = return subst

    -- Check to see whether tv2 is refined
  | Just ty' <- lookupVarEnv subst tv2
370
  = uUnrefined subst tv1 ty' ty'
371
372
373
374
375
376

  -- So both are unrefined; next, see if the kinds force the direction
  | k1 == k2	-- Can update either; so check the bind-flags
  = do	{ b1 <- tvBindFlag tv1
	; b2 <- tvBindFlag tv2
	; case (b1,b2) of
377
	    (BindMe, _) 	 -> bind tv1 ty2
378

379
380
	    (AvoidMe, BindMe)	 -> bind tv2 ty1
	    (AvoidMe, _)	 -> bind tv1 ty2
381

382
383
384
385
386
387
388
	    (WildCard, WildCard) -> return subst
	    (WildCard, Skolem)   -> return subst
	    (WildCard, _)	 -> bind tv2 ty1

	    (Skolem, WildCard)	 -> return subst
	    (Skolem, Skolem)	 -> failWith (misMatch ty1 ty2)
	    (Skolem, _)		 -> bind tv2 ty1
389
390
	}

391
392
393
  | k1 `isSubKind` k2 = bindTv subst tv2 ty1	-- Must update tv2
  | k2 `isSubKind` k1 = bindTv subst tv1 ty2	-- Must update tv1

394
395
396
397
398
  | otherwise = failWith (kindMisMatch tv1 ty2)
  where
    ty1 = TyVarTy tv1
    k1 = tyVarKind tv1
    k2 = tyVarKind tv2
399
    bind tv ty = return (extendVarEnv subst tv ty)
400

401
402
uUnrefined subst tv1 ty2 ty2'	-- ty2 is not a type variable
  | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
403
404
405
  = failWith (occursCheck tv1 ty2)	-- Occurs check
  | not (k2 `isSubKind` k1)
  = failWith (kindMisMatch tv1 ty2)	-- Kind check
406
  | otherwise
407
  = bindTv subst tv1 ty2		-- Bind tyvar to the synonym if poss
408
409
  where
    k1 = tyVarKind tv1
410
    k2 = typeKind ty2'
411
412
413
414
415
416
417
418
419
420
421

substTvSet :: TvSubstEnv -> TyVarSet -> TyVarSet
-- Apply the non-idempotent substitution to a set of type variables,
-- remembering that the substitution isn't necessarily idempotent
substTvSet subst tvs
  = foldVarSet (unionVarSet . get) emptyVarSet tvs
  where
    get tv = case lookupVarEnv subst tv of
		Nothing -> unitVarSet tv
		Just ty -> substTvSet subst (tyVarsOfType ty)

422
423
424
425
426
427
428
bindTv subst tv ty	-- ty is not a type variable
  = do	{ b <- tvBindFlag tv
	; case b of
	    Skolem   -> failWith (misMatch (TyVarTy tv) ty)
	    WildCard -> return subst
	    other    -> return (extendVarEnv subst tv ty)
	}
429
430
431
432
433
434
435
436
437
\end{code}

%************************************************************************
%*									*
		Unification monad
%*									*
%************************************************************************

\begin{code}
438
439
440
441
442
443
444
445
446
data BindFlag 
  = BindMe	-- A regular type variable
  | AvoidMe	-- Like BindMe but, given the choice, avoid binding it

  | Skolem	-- This type variable is a skolem constant
		-- Don't bind it; it only matches itself

  | WildCard 	-- This type variable matches anything,
		-- and does not affect the substitution
447
448

newtype UM a = UM { unUM :: (TyVar -> BindFlag)
449
		         -> MaybeErr Message a }
450
451
452
453
454
455
456
457

instance Monad UM where
  return a = UM (\tvs -> Succeeded a)
  fail s   = UM (\tvs -> Failed (text s))
  m >>= k  = UM (\tvs -> case unUM m tvs of
			   Failed err -> Failed err
			   Succeeded v  -> unUM (k v) tvs)

458
initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
459
460
461
462
463
464
465
466
initUM badtvs um = unUM um badtvs

tvBindFlag :: TyVar -> UM BindFlag
tvBindFlag tv = UM (\tv_fn -> Succeeded (tv_fn tv))

failWith :: Message -> UM a
failWith msg = UM (\tv_fn -> Failed msg)

467
maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
468
469
maybeErrToMaybe (Succeeded a) = Just a
maybeErrToMaybe (Failed m)    = Nothing
470
471
472
473
474
475
476
477
478
479

------------------------------
repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
-- Like Type.splitAppTy_maybe, but any coreView stuff is already done
repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
repSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
						Just (tys', ty') -> Just (TyConApp tc tys', ty')
						Nothing		 -> Nothing
repSplitAppTy_maybe other = Nothing
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
\end{code}


%************************************************************************
%*									*
		Error reporting
	We go to a lot more trouble to tidy the types
	in TcUnify.  Maybe we'll end up having to do that
	here too, but I'll leave it for now.
%*									*
%************************************************************************

\begin{code}
misMatch t1 t2
  = ptext SLIT("Can't match types") <+> quotes (ppr t1) <+> 
    ptext SLIT("and") <+> quotes (ppr t2)

lengthMisMatch tys1 tys2
  = sep [ptext SLIT("Can't match unequal length lists"), 
	 nest 2 (ppr tys1), nest 2 (ppr tys2) ]

kindMisMatch tv1 t2
  = vcat [ptext SLIT("Can't match kinds") <+> quotes (ppr (tyVarKind tv1)) <+> 
	    ptext SLIT("and") <+> quotes (ppr (typeKind t2)),
	  ptext SLIT("when matching") <+> quotes (ppr tv1) <+> 
		ptext SLIT("with") <+> quotes (ppr t2)]

occursCheck tv ty
  = hang (ptext SLIT("Can't construct the infinite type"))
       2 (ppr tv <+> equals <+> ppr ty)
\end{code}