Unify.lhs 6.09 KB
Newer Older
1
2
3
4
%
% (c) The University of Glasgow 2006
%

5
6
\begin{code}
module Unify ( 
7
8
9
10
	-- Matching of types: 
	--	the "tc" prefix indicates that matching always
	--	respects newtypes (rather than looking through them)
	tcMatchTys, tcMatchTyX, ruleMatchTyX, tcMatchPreds, MatchEnv(..)
11
12
13
14
   ) where

#include "HsVersions.h"

15
import Var
16
17
import VarEnv
import VarSet
18
19
import Type
import TypeRep
20
21
22
23
24
25
26
import Outputable
import Maybes
\end{code}


%************************************************************************
%*									*
27
28
29
30
31
32
33
34
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
		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

60
tcMatchTys :: TyVarSet		-- Template tyvars
61
62
	 -> [Type]		-- Template
	 -> [Type]		-- Target
63
	 -> Maybe TvSubst	-- One-shot; in principle the template
64
65
				-- variables could be free in the target

66
tcMatchTys tmpls tys1 tys2
67
68
69
  = case match_tys menv emptyTvSubstEnv tys1 tys2 of
	Just subst_env -> Just (TvSubst in_scope subst_env)
	Nothing	       -> Nothing
70
  where
71
72
    menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
    in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
73
74
75
	-- We're assuming that all the interesting 
	-- tyvars in tys1 are in tmpls

76
77
78
79
80
81
82
83
84
85
86
87
88
-- This is similar, but extends a substitution
tcMatchTyX :: TyVarSet 		-- Template tyvars
	   -> TvSubst		-- Substitution to extend
	   -> Type		-- Template
	   -> Type		-- Target
	   -> Maybe TvSubst
tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
  = case match menv subst_env ty1 ty2 of
	Just subst_env -> Just (TvSubst in_scope subst_env)
	Nothing	       -> Nothing
  where
    menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}

89
90
91
92
93
94
95
96
97
98
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)

99
-- This one is called from the expression matcher, which already has a MatchEnv in hand
100
ruleMatchTyX :: MatchEnv 
101
102
103
104
105
	 -> TvSubstEnv		-- Substitution to extend
	 -> Type		-- Template
	 -> Type		-- Target
	 -> Maybe TvSubstEnv

106
ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2	-- Rename for export
107
108
109
110
111
\end{code}

Now the internals of matching

\begin{code}
112
match :: MatchEnv	-- For the most part this is pushed downwards
113
114
115
116
117
118
119
120
121
      -> 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

122
match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2
123
			  | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
124
125

match menv subst (TyVarTy tv1) ty2
126
  | tv1' `elemVarSet` me_tmpls menv
127
  = case lookupVarEnv subst tv1' of
128
129
130
131
132
133
	Nothing 	-- No existing binding
	    | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
	    -> Nothing	-- Occurs check
	    | not (typeKind ty2 `isSubKind` tyVarKind tv1)
	    -> Nothing	-- Kind mis-match
	    | otherwise
134
	    -> Just (extendVarEnv subst tv1' ty2)
135
136
137

	Just ty1' 	-- There is an existing binding; check whether ty2 matches it
	    | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
138
139
		-- ty1 has no locally-bound variables, hence nukeRnEnvL
		-- Note tcEqType...we are doing source-type matching here
140
141
142
	    -> Just subst
	    | otherwise	-> Nothing	-- ty2 doesn't match
	    
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165

   | 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
166
	-- 'repSplit' used because the tcView stuff is done above
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
  = 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}