TcGadt.lhs 17.8 KB
Newer Older
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
1
%
2
% (c) The University of Glasgow 2006
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
3
4
5
6
7
8
9
10
11
12
13
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%

%************************************************************************
%*									*
		Type refinement for GADTs
%*									*
%************************************************************************

\begin{code}
module TcGadt (
14
15
16
	Refinement, emptyRefinement, isEmptyRefinement, 
	gadtRefine, 
	refineType, refinePred, refineResType,
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
17
18
19
	tcUnifyTys, BindFlag(..)
  ) where

20
21
22
23
#include "HsVersions.h"

import HsSyn
import Coercion
24
import Type
25

26
27
28
import TypeRep
import DataCon
import Var
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
29
30
import VarEnv
import VarSet
31
32
33
import ErrUtils
import Maybes
import Control.Monad
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
34
import Outputable
35
import TcType
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
36

37
38
39
40
#ifdef DEBUG
import Unique
import UniqFM
#endif
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
41
42
43
44
45
46
47
48
49
50
\end{code}


%************************************************************************
%*									*
		What a refinement is
%*									*
%************************************************************************

\begin{code}
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
51
data Refinement = Reft InScopeSet InternalReft 
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
52
53

type InternalReft = TyVarEnv (Coercion, Type)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
54
55
-- INVARIANT:   a->(co,ty)   then   co :: (a:=:ty)
-- Not necessarily idemopotent
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
56
57

instance Outputable Refinement where
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
58
59
60
  ppr (Reft in_scope env)
    = ptext SLIT("Refinement") <+>
        braces (ppr env)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
61
62

emptyRefinement :: Refinement
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
63
emptyRefinement = (Reft emptyInScopeSet emptyVarEnv)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
64

65
66
isEmptyRefinement :: Refinement -> Bool
isEmptyRefinement (Reft _ env) = isEmptyVarEnv env
67

68
refineType :: Refinement -> Type -> Maybe (Coercion, Type)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
69
70
71
-- Apply the refinement to the type.
-- If (refineType r ty) = (co, ty')
-- Then co :: ty:=:ty'
72
-- Nothing => the refinement does nothing to this type
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
73
74
75
refineType (Reft in_scope env) ty
  | not (isEmptyVarEnv env),		-- Common case
    any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty))
76
  = Just (substTy co_subst ty, substTy tv_subst ty)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
77
  | otherwise
78
  = Nothing	-- The type doesn't mention any refined type variables
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
79
  where
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
80
    tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
81
82
83
84
85
86
87
88
89
90
91
    co_subst = mkTvSubst in_scope (mapVarEnv fst env)
 
refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType)
refinePred (Reft in_scope env) pred
  | not (isEmptyVarEnv env),		-- Common case
    any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred))
  = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred)
  | otherwise
  = Nothing	-- The type doesn't mention any refined type variables
  where
    tv_subst = mkTvSubst in_scope (mapVarEnv snd env)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
92
    co_subst = mkTvSubst in_scope (mapVarEnv fst env)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
93
 
94
refineResType :: Refinement -> Type -> (HsWrapper, Type)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
95
96
97
-- Like refineType, but returns the 'sym' coercion
-- If (refineResType r ty) = (co, ty')
-- Then co :: ty':=:ty
98
-- It's convenient to return a HsWrapper here
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
99
100
refineResType reft ty
  = case refineType reft ty of
101
102
	Just (co, ty1) -> (WpCo (mkSymCoercion co), ty1)
	Nothing	       -> (idHsWrapper, 	    ty)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
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
\end{code}


%************************************************************************
%*									*
		Generating a type refinement
%*									*
%************************************************************************

\begin{code}
gadtRefine :: Refinement
	   -> [TyVar] 	-- Bind these by preference
	   -> [CoVar]
	   -> MaybeErr Message Refinement
\end{code}

(gadtRefine cvs) takes a list of coercion variables, and returns a
list of coercions, obtained by unifying the types equated by the
incoming coercions.  The returned coercions all have kinds of form
(a:=:ty), where a is a rigid type variable.

Example:
  gadtRefine [c :: (a,Int):=:(Bool,b)]
  = [ right (left c) :: a:=:Bool,	
      sym (right c)  :: b:=:Int ]

That is, given evidence 'c' that (a,Int)=(Bool,b), it returns derived
evidence in easy-to-use form.  In particular, given any e::ty, we know 
that:
	e `cast` ty[right (left c)/a, sym (right c)/b]
	:: ty [Bool/a, Int/b]
      
Two refinements:

- It can fail, if the coercion is unsatisfiable.

- It's biased, by being given a set of type variables to bind
  when there is a choice. Example:
	MkT :: forall a. a -> T [a]
	f :: forall b. T [b] -> b
	f x = let v = case x of { MkT y -> y }
	      in ...
  Here we want to bind [a->b], not the other way round, because
  in this example the return type is wobbly, and we want the
  program to typecheck


-- E.g. (a, Bool, right (left c))
-- INVARIANT: in the triple (tv, ty, co), we have (co :: tv:=:ty)
-- The result is idempotent: the 

\begin{code}
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
155
gadtRefine (Reft in_scope env1) 
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
156
	   ex_tvs co_vars
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
157
-- Precondition: fvs( co_vars ) # env1
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
158
-- That is, the kinds of the co_vars are a
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
159
-- fixed point of the incoming refinement
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
160

161
162
163
  = ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars),
	     ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) )
    initUM (tryToBind tv_set) $
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
164
165
166
167
168
    do	{ 	-- Run the unifier, starting with an empty env
	; env2 <- foldM do_one emptyInternalReft co_vars

		-- Find the fixed point of the resulting 
		-- non-idempotent substitution
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
169
170
	; let tmp_env = env1 `plusVarEnv` env2
              out_env = fixTvCoEnv in_scope' tmp_env
171
172
173
	; WARN( not (null (badReftElts tmp_env)), ppr (badReftElts tmp_env) $$ ppr tmp_env )
	  WARN( not (null (badReftElts out_env)), ppr (badReftElts out_env) $$ ppr out_env )
	  return (Reft in_scope' out_env) }
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
174
175
176
  where
    tv_set = mkVarSet ex_tvs
    in_scope' = foldr extend in_scope co_vars
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
177
178

	-- For each co_var, add it *and* the tyvars it mentions, to in_scope
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
179
    extend co_var in_scope
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
180
181
	= extendInScopeSetSet in_scope $
	  extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
182
183
184
185
	
    do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2
	where
	   (ty1,ty2) = splitCoercionKind (tyVarKind co_var)
186
\end{code}
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
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

%************************************************************************
%*									*
		Unification
%*									*
%************************************************************************

\begin{code}
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
--
-- We implement tcUnifyTys using the evidence-generating 'unify' function
-- in this module, even though we don't need to generate any evidence.
-- This is simply to avoid replicating all all the code for unify
tcUnifyTys bind_fn tys1 tys2
  = maybeErrToMaybe $ initUM bind_fn $
    do { reft <- unifyList emptyInternalReft cos tys1 tys2

	-- Find the fixed point of the resulting non-idempotent substitution
	; let in_scope = mkInScopeSet (tvs1 `unionVarSet` tvs2)
	      tv_env   = fixTvSubstEnv in_scope (mapVarEnv snd reft)

	; return (mkTvSubst in_scope tv_env) }
  where
    tvs1 = tyVarsOfTypes tys1
    tvs2 = tyVarsOfTypes tys2
    cos  = zipWith mkUnsafeCoercion tys1 tys2


----------------------------
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
220
221
fixTvCoEnv :: InScopeSet -> InternalReft -> InternalReft
	-- Find the fixed point of a Refinement
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
222
	-- (assuming it has no loops!)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
223
224
225
226
227
fixTvCoEnv in_scope env
  = fixpt
  where
    fixpt         = mapVarEnv step env

228
229
230
    step (co, ty) = case refineType (Reft in_scope fixpt) ty of
			Nothing 	-> (co, 		    ty)
			Just (co', ty') -> (mkTransCoercion co co', ty')
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
231
232
233
234
235
236
237
      -- Apply fixpt one step:
      -- Use refineType to get a substituted type, ty', and a coercion, co_fn,
      -- which justifies the substitution.  If the coercion is not the identity
      -- then use transitivity with the original coercion

-----------------------------
fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
238
239
240
241
242
243
244
245
246
fixTvSubstEnv in_scope env
  = fixpt 
  where
    fixpt = mapVarEnv (substTy (mkTvSubst in_scope fixpt)) env

----------------------------
tryToBind :: TyVarSet -> TyVar -> BindFlag
tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe
		    | otherwise	             = AvoidMe
247

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
248
249
250
251
252
253
254
255
256
257
\end{code}


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

\begin{code}
258
#ifdef DEBUG
259
260
261
262
263
264
265
266
267
268
269
270
badReftElts :: InternalReft -> [(Unique, (Coercion,Type))]
-- Return the BAD elements of the refinement
-- Should be empty; used in asserions only
badReftElts env
  = filter (not . ok) (ufmToList env)
  where
    ok :: (Unique, (Coercion, Type)) -> Bool
    ok (u, (co, ty)) | Just tv <- tcGetTyVar_maybe ty1
		     = varUnique tv == u && ty `tcEqType` ty2 
		     | otherwise = False
	where
	  (ty1,ty2) = coercionKind co
271
#endif
272

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
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
emptyInternalReft :: InternalReft
emptyInternalReft = emptyVarEnv

unify :: InternalReft		-- An existing substitution to extend
      -> Coercion 	-- Witness of their equality 
      -> Type -> Type 	-- Types to be unified, and witness of their equality
      -> UM InternalReft		-- 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.

-- PRE-CONDITION: in the call (unify r co ty1 ty2), we know that
--			co :: (ty1:=:ty2)

-- Respects newtypes, PredTypes

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

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

unify_ subst co ty1 ty2 | Just ty1' <- tcView ty1 = unify subst co ty1' ty2
unify_ subst co ty1 ty2 | Just ty2' <- tcView ty2 = unify subst co ty1 ty2'

unify_ subst co (PredTy p1) (PredTy p2) = unify_pred subst co p1 p2

unify_ subst co t1@(TyConApp tyc1 tys1) t2@(TyConApp tyc2 tys2) 
  | tyc1 == tyc2 = unify_tys subst co tys1 tys2

unify_ subst co (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
  = do	{ let [co1,co2] = decomposeCo 2 co
	; subst' <- unify subst co1 ty1a ty2a
	; unify subst' co2 ty1b ty2b }

	-- 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
unify_ subst co (AppTy ty1a ty1b) ty2
  | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
  = do	{ subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
        ; unify subst' (mkRightCoercion co) ty1b ty2b }

unify_ subst co ty1 (AppTy ty2a ty2b)
  | Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
  = do	{ subst' <- unify subst (mkLeftCoercion co) ty1a ty2a
        ; unify subst' (mkRightCoercion co) ty1b ty2b }

unify_ subst co ty1 ty2 = failWith (misMatch ty1 ty2)
	-- ForAlls??


------------------------------
unify_pred subst co (ClassP c1 tys1) (ClassP c2 tys2)
  | c1 == c2 = unify_tys subst co tys1 tys2
unify_pred subst co (IParam n1 t1) (IParam n2 t2)
  | n1 == n2 = unify subst co t1 t2
unify_pred subst co p1 p2 = failWith (misMatch (PredTy p1) (PredTy p2))
 
------------------------------
unify_tys :: InternalReft -> Coercion -> [Type] -> [Type] -> UM InternalReft
unify_tys subst co xs ys
  = unifyList subst (decomposeCo (length xs) co) xs ys

unifyList :: InternalReft -> [Coercion] -> [Type] -> [Type] -> UM InternalReft
unifyList subst orig_cos orig_xs orig_ys
  = go subst orig_cos orig_xs orig_ys
  where
    go subst _	      []     []     = return subst
    go subst (co:cos) (x:xs) (y:ys) = do { subst' <- unify subst co x y
				         ; go subst' cos xs ys }
    go subst _ _ _ = failWith (lengthMisMatch orig_xs orig_ys)

---------------------------------
uVar :: Bool            -- Swapped
     -> InternalReft	-- An existing substitution to extend
     -> Coercion
     -> TyVar           -- Type variable to be unified
     -> Type            -- with this type
     -> UM InternalReft

-- PRE-CONDITION: in the call (uVar swap r co tv1 ty), we know that
--	if swap=False	co :: (tv1:=:ty)
--	if swap=True	co :: (ty:=:tv1)

uVar swap subst co tv1 ty
 = -- Check to see whether tv1 is refined by the substitution
   case (lookupVarEnv subst tv1) of

     -- Yes, call back into unify'
     Just (co',ty')	-- co' :: (tv1:=:ty')
	| swap      	-- co :: (ty:=:tv1)
	-> unify subst (mkTransCoercion co co') ty ty' 
        | otherwise 	-- co :: (tv1:=:ty)
	-> unify subst (mkTransCoercion (mkSymCoercion co') co) ty' ty

     -- No, continue
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
373
     Nothing -> uUnrefined swap subst co
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
374
375
376
			   tv1 ty ty


chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
377
378
uUnrefined :: Bool                -- Whether the input is swapped
           -> InternalReft        -- An existing substitution to extend
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
379
380
381
382
383
384
385
	   -> Coercion
           -> TyVar               -- Type variable to be unified
           -> Type                -- with this type
           -> Type                -- (de-noted version)
           -> UM InternalReft

-- We know that tv1 isn't refined
386
387
388
389
-- PRE-CONDITION: in the call (uUnrefined False r co tv1 ty2 ty2'), we know that
--	co :: tv1:=:ty2
-- and if the first argument is True instead, we know
--      co :: ty2:=:tv1
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
390

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
391
uUnrefined swap subst co tv1 ty2 ty2'
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
392
  | Just ty2'' <- tcView ty2'
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
393
  = uUnrefined swap subst co tv1 ty2 ty2''	-- Unwrap synonyms
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
394
395
396
397
		-- This is essential, in case we have
		--	type Foo a = a
		-- and then unify a :=: Foo a

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
398
uUnrefined swap subst co tv1 ty2 (TyVarTy tv2)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
399
400
401
402
  | tv1 == tv2		-- Same type variable
  = return subst

    -- Check to see whether tv2 is refined
403
  | Just (co',ty') <- lookupVarEnv subst tv2	-- co' :: tv2:=:ty'
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
404
  = uUnrefined False subst (mkTransCoercion (doSwap swap co) co') tv1 ty' ty'
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
405
406
407
408
409
410

  -- So both are unrefined; next, see if the kinds force the direction
  | eqKind k1 k2	-- Can update either; so check the bind-flags
  = do	{ b1 <- tvBindFlag tv1
	; b2 <- tvBindFlag tv2
	; case (b1,b2) of
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
411
	    (BindMe, _) 	 -> bind swap tv1 ty2
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
412

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
413
414
	    (AvoidMe, BindMe)	 -> bind (not swap) tv2 ty1
	    (AvoidMe, _)	 -> bind swap tv1 ty2
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
415
416
417

	    (WildCard, WildCard) -> return subst
	    (WildCard, Skolem)   -> return subst
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
418
	    (WildCard, _)	 -> bind (not swap) tv2 ty1
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
419
420
421

	    (Skolem, WildCard)	 -> return subst
	    (Skolem, Skolem)	 -> failWith (misMatch ty1 ty2)
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
422
	    (Skolem, _)		 -> bind (not swap) tv2 ty1
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
423
424
	}

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
425
426
  | k1 `isSubKind` k2 = bindTv (not swap) subst co tv2 ty1  -- Must update tv2
  | k2 `isSubKind` k1 = bindTv swap subst co tv1 ty2	    -- Must update tv1
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
427
428
429
430
431
432

  | otherwise = failWith (kindMisMatch tv1 ty2)
  where
    ty1 = TyVarTy tv1
    k1 = tyVarKind tv1
    k2 = tyVarKind tv2
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
433
    bind swap tv ty = extendReft swap subst tv co ty
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
434

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
435
uUnrefined swap subst co tv1 ty2 ty2'	-- ty2 is not a type variable
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
436
437
438
439
440
  | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2')
  = failWith (occursCheck tv1 ty2)	-- Occurs check
  | not (k2 `isSubKind` k1)
  = failWith (kindMisMatch tv1 ty2)	-- Kind check
  | otherwise
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
441
  = bindTv swap subst co tv1 ty2		-- Bind tyvar to the synonym if poss
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
442
443
444
445
446
447
448
449
450
451
452
453
454
455
  where
    k1 = tyVarKind tv1
    k2 = typeKind ty2'

substTvSet :: InternalReft -> 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)

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
456
457
bindTv swap subst co tv ty	-- ty is not a type variable
  = do  { b <- tvBindFlag tv
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
458
459
460
	; case b of
	    Skolem   -> failWith (misMatch (TyVarTy tv) ty)
	    WildCard -> return subst
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
461
	    other    -> extendReft swap subst tv co ty
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
462
	}
chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479

doSwap :: Bool -> Coercion -> Coercion
doSwap swap co = if swap then mkSymCoercion co else co

extendReft :: Bool 
           -> InternalReft 
           -> TyVar 
           -> Coercion 
           -> Type 
           -> UM InternalReft
extendReft swap subst tv  co ty
  = ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty), 
          (text "Refinement invariant failure: co = " <+> ppr co1  <+> ppr (coercionKindPredTy co1) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)) )
    return (extendVarEnv subst tv (co1, ty))
  where
    co1 = doSwap swap co

chak@cse.unsw.edu.au.'s avatar
chak@cse.unsw.edu.au. committed
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
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
549
550
\end{code}

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

\begin{code}
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

newtype UM a = UM { unUM :: (TyVar -> BindFlag)
		         -> MaybeErr Message a }

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)

initUM :: (TyVar -> BindFlag) -> UM a -> MaybeErr Message a
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)

maybeErrToMaybe :: MaybeErr fail succ -> Maybe succ
maybeErrToMaybe (Succeeded a) = Just a
maybeErrToMaybe (Failed m)    = Nothing
\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)
551
\end{code}