Comments and layout only
[ghc.git] / compiler / types / Unify.lhs
1 %
2 % (c) The University of Glasgow 2006
3 %
4
5 \begin{code}
6 module Unify ( 
7         -- Matching of types: 
8         --      the "tc" prefix indicates that matching always
9         --      respects newtypes (rather than looking through them)
10         tcMatchTys, tcMatchTyX, ruleMatchTyX, tcMatchPreds, MatchEnv(..)
11    ) where
12
13 #include "HsVersions.h"
14
15 import Var
16 import VarEnv
17 import VarSet
18 import Type
19 import TypeRep
20 import Outputable
21 import Maybes
22 \end{code}
23
24
25 %************************************************************************
26 %*                                                                      *
27                 Matching
28 %*                                                                      *
29 %************************************************************************
30
31
32 Matching is much tricker than you might think.
33
34 1. The substitution we generate binds the *template type variables*
35    which are given to us explicitly.
36
37 2. We want to match in the presence of foralls; 
38         e.g     (forall a. t1) ~ (forall b. t2)
39
40    That is what the RnEnv2 is for; it does the alpha-renaming
41    that makes it as if a and b were the same variable.
42    Initialising the RnEnv2, so that it can generate a fresh
43    binder when necessary, entails knowing the free variables of
44    both types.
45
46 3. We must be careful not to bind a template type variable to a
47    locally bound variable.  E.g.
48         (forall a. x) ~ (forall b. b)
49    where x is the template type variable.  Then we do not want to
50    bind x to a/b!  This is a kind of occurs check.
51    The necessary locals accumulate in the RnEnv2.
52
53
54 \begin{code}
55 data MatchEnv
56   = ME  { me_tmpls :: VarSet    -- Template tyvars
57         , me_env   :: RnEnv2    -- Renaming envt for nested foralls
58         }                       --   In-scope set includes template tyvars
59
60 tcMatchTys :: TyVarSet          -- Template tyvars
61          -> [Type]              -- Template
62          -> [Type]              -- Target
63          -> Maybe TvSubst       -- One-shot; in principle the template
64                                 -- variables could be free in the target
65
66 tcMatchTys tmpls tys1 tys2
67   = case match_tys menv emptyTvSubstEnv tys1 tys2 of
68         Just subst_env -> Just (TvSubst in_scope subst_env)
69         Nothing        -> Nothing
70   where
71     menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
72     in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfTypes tys2)
73         -- We're assuming that all the interesting 
74         -- tyvars in tys1 are in tmpls
75
76 -- This is similar, but extends a substitution
77 tcMatchTyX :: TyVarSet          -- Template tyvars
78            -> TvSubst           -- Substitution to extend
79            -> Type              -- Template
80            -> Type              -- Target
81            -> Maybe TvSubst
82 tcMatchTyX tmpls (TvSubst in_scope subst_env) ty1 ty2
83   = case match menv subst_env ty1 ty2 of
84         Just subst_env -> Just (TvSubst in_scope subst_env)
85         Nothing        -> Nothing
86   where
87     menv = ME {me_tmpls = tmpls, me_env = mkRnEnv2 in_scope}
88
89 tcMatchPreds
90         :: [TyVar]                      -- Bind these
91         -> [PredType] -> [PredType]
92         -> Maybe TvSubstEnv
93 tcMatchPreds tmpls ps1 ps2
94   = match_list (match_pred menv) emptyTvSubstEnv ps1 ps2
95   where
96     menv = ME { me_tmpls = mkVarSet tmpls, me_env = mkRnEnv2 in_scope_tyvars }
97     in_scope_tyvars = mkInScopeSet (tyVarsOfTheta ps1 `unionVarSet` tyVarsOfTheta ps2)
98
99 -- This one is called from the expression matcher, which already has a MatchEnv in hand
100 ruleMatchTyX :: MatchEnv 
101          -> TvSubstEnv          -- Substitution to extend
102          -> Type                -- Template
103          -> Type                -- Target
104          -> Maybe TvSubstEnv
105
106 ruleMatchTyX menv subst ty1 ty2 = match menv subst ty1 ty2      -- Rename for export
107 \end{code}
108
109 Now the internals of matching
110
111 \begin{code}
112 match :: MatchEnv       -- For the most part this is pushed downwards
113       -> TvSubstEnv     -- Substitution so far:
114                         --   Domain is subset of template tyvars
115                         --   Free vars of range is subset of 
116                         --      in-scope set of the RnEnv2
117       -> Type -> Type   -- Template and target respectively
118       -> Maybe TvSubstEnv
119 -- This matcher works on source types; that is, 
120 -- it respects NewTypes and PredType
121
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         Nothing         -- No existing binding
129             | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
130             -> Nothing  -- Occurs check
131             | not (typeKind ty2 `isSubKind` tyVarKind tv1)
132             -> Nothing  -- Kind mis-match
133             | otherwise
134             -> Just (extendVarEnv subst tv1 ty2)
135
136         Just ty1'       -- There is an existing binding; check whether ty2 matches it
137             | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
138                 -- ty1 has no locally-bound variables, hence nukeRnEnvL
139                 -- Note tcEqType...we are doing source-type matching here
140             -> Just subst
141             | otherwise -> Nothing      -- ty2 doesn't match
142             
143
144    | otherwise  -- tv1 is not a template tyvar
145    = case ty2 of
146         TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
147         other                                   -> Nothing
148   where
149     rn_env = me_env menv
150     tv1' = rnOccL rn_env tv1
151
152 match menv subst (ForAllTy tv1 ty1) (ForAllTy tv2 ty2) 
153   = match menv' subst ty1 ty2
154   where         -- Use the magic of rnBndr2 to go under the binders
155     menv' = menv { me_env = rnBndr2 (me_env menv) tv1 tv2 }
156
157 match menv subst (PredTy p1) (PredTy p2) 
158   = match_pred menv subst p1 p2
159 match menv subst (TyConApp tc1 tys1) (TyConApp tc2 tys2) 
160   | tc1 == tc2 = match_tys menv subst tys1 tys2
161 match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b) 
162   = do { subst' <- match menv subst ty1a ty2a
163        ; match menv subst' ty1b ty2b }
164 match menv subst (AppTy ty1a ty1b) ty2
165   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
166         -- 'repSplit' used because the tcView stuff is done above
167   = do { subst' <- match menv subst ty1a ty2a
168        ; match menv subst' ty1b ty2b }
169
170 match menv subst ty1 ty2
171   = Nothing
172
173 --------------
174 match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
175
176 --------------
177 match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
178            -> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
179 match_list fn subst []         []         = Just subst
180 match_list fn subst (ty1:tys1) (ty2:tys2) = do  { subst' <- fn subst ty1 ty2
181                                                 ; match_list fn subst' tys1 tys2 }
182 match_list fn subst tys1       tys2       = Nothing     
183
184 --------------
185 match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
186   | c1 == c2 = match_tys menv subst tys1 tys2
187 match_pred menv subst (IParam n1 t1) (IParam n2 t2)
188   | n1 == n2 = match menv subst t1 t2
189 match_pred menv subst p1 p2 = Nothing
190 \end{code}
191
192