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