ghc/compiler/types/Unify.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section{Unify}
   5
   6 This module contains a unifier and a matcher, both of which
   7 use an explicit substitution
   8
   9 \begin{code}
  10 module Unify ( unifyTysX, unifyTyListsX, allDistinctTyVars,
  11                match, matchTy, matchTys,
  12   ) where
  13
  14 #include "HsVersions.h"
  15
  16 import TypeRep  ( Type(..) )     -- friend
  17 import Type     ( typeKind, tyVarsOfType, splitAppTy_maybe, getTyVar_maybe,
  18                   splitUTy, isUTy, deNoteType
  19                 )
  20
  21 import PprType  ()      -- Instances
  22                         -- This import isn't strictly necessary, but it makes sure that
  23                         -- PprType is below Unify in the hierarchy, which in turn makes
  24                         -- fewer modules boot-import PprType
  25
  26 import Var      ( tyVarKind )
  27 import VarSet
  28 import VarEnv   ( TyVarSubstEnv, emptySubstEnv, lookupSubstEnv, extendSubstEnv,
  29                   SubstResult(..)
  30                 )
  31
  32 import Outputable
  33 \end{code}
  34
  35 %************************************************************************
  36 %*                                                                      *
  37 \subsection{Unification with an explicit substitution}
  38 %*                                                                      *
  39 %************************************************************************
  40
  41 (allDistinctTyVars tys tvs) = True
  42         iff
  43 all the types tys are type variables,
  44 distinct from each other and from tvs.
  45
  46 This is useful when checking that unification hasn't unified signature
  47 type variables.  For example, if the type sig is
  48         f :: forall a b. a -> b -> b
  49 we want to check that 'a' and 'b' havn't
  50         (a) been unified with a non-tyvar type
  51         (b) been unified with each other (all distinct)
  52         (c) been unified with a variable free in the environment
  53
  54 \begin{code}
  55 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
  56
  57 allDistinctTyVars []       acc
  58   = True
  59 allDistinctTyVars (ty:tys) acc
  60   = case getTyVar_maybe ty of
  61         Nothing                       -> False  -- (a)
  62         Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
  63                 | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
  64 \end{code}
  65
  66 %************************************************************************
  67 %*                                                                      *
  68 \subsection{Unification with an explicit substitution}
  69 %*                                                                      *
  70 %************************************************************************
  71
  72 Unify types with an explicit substitution and no monad.
  73 Ignore usage annotations.
  74
  75 \begin{code}
  76 type MySubst
  77    = (TyVarSet,         -- Set of template tyvars
  78       TyVarSubstEnv)    -- Not necessarily idempotent
  79
  80 unifyTysX :: TyVarSet           -- Template tyvars
  81           -> Type
  82           -> Type
  83           -> Maybe TyVarSubstEnv
  84 unifyTysX tmpl_tyvars ty1 ty2
  85   = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
  86
  87 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
  88               -> Maybe TyVarSubstEnv
  89 unifyTyListsX tmpl_tyvars tys1 tys2
  90   = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
  91
  92
  93 uTysX :: Type
  94       -> Type
  95       -> (MySubst -> Maybe result)
  96       -> MySubst
  97       -> Maybe result
  98
  99 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
 100 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
 101
 102         -- Variables; go for uVar
 103 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
 104   | tyvar1 == tyvar2
 105   = k subst
 106 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
 107   | tyvar1 `elemVarSet` tmpls
 108   = uVarX tyvar1 ty2 k subst
 109 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
 110   | tyvar2 `elemVarSet` tmpls
 111   = uVarX tyvar2 ty1 k subst
 112
 113         -- Functions; just check the two parts
 114 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
 115   = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
 116
 117         -- Type constructors must match
 118 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
 119   | (con1 == con2 && length tys1 == length tys2)
 120   = uTyListsX tys1 tys2 k subst
 121
 122         -- Applications need a bit of care!
 123         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 124         -- NB: we've already dealt with type variables and Notes,
 125         -- so if one type is an App the other one jolly well better be too
 126 uTysX (AppTy s1 t1) ty2 k subst
 127   = case splitAppTy_maybe ty2 of
 128       Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
 129       Nothing       -> Nothing    -- Fail
 130
 131 uTysX ty1 (AppTy s2 t2) k subst
 132   = case splitAppTy_maybe ty1 of
 133       Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
 134       Nothing       -> Nothing    -- Fail
 135
 136         -- Not expecting for-alls in unification
 137 #ifdef DEBUG
 138 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
 139 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
 140 #endif
 141
 142         -- Ignore usages
 143 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
 144 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
 145
 146         -- Anything else fails
 147 uTysX ty1 ty2 k subst = Nothing
 148
 149
 150 uTyListsX []         []         k subst = k subst
 151 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
 152 uTyListsX tys1       tys2       k subst = Nothing   -- Fail if the lists are different lengths
 153 \end{code}
 154
 155 \begin{code}
 156 -- Invariant: tv1 is a unifiable variable
 157 uVarX tv1 ty2 k subst@(tmpls, env)
 158   = case lookupSubstEnv env tv1 of
 159       Just (DoneTy ty1) ->    -- Already bound
 160                      uTysX ty1 ty2 k subst
 161
 162       Nothing        -- Not already bound
 163                |  typeKind ty2 == tyVarKind tv1
 164                && occur_check_ok ty2
 165                ->     -- No kind mismatch nor occur check
 166                   UASSERT( not (isUTy ty2) )
 167                   k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
 168
 169                | otherwise -> Nothing   -- Fail if kind mis-match or occur check
 170   where
 171     occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
 172     occur_check_ok_tv tv | tv1 == tv = False
 173                          | otherwise = case lookupSubstEnv env tv of
 174                                          Nothing           -> True
 175                                          Just (DoneTy ty)  -> occur_check_ok ty
 176 \end{code}
 177
 178
 179
 180 %************************************************************************
 181 %*                                                                      *
 182 \subsection{Matching on types}
 183 %*                                                                      *
 184 %************************************************************************
 185
 186 Matching is a {\em unidirectional} process, matching a type against a
 187 template (which is just a type with type variables in it).  The
 188 matcher assumes that there are no repeated type variables in the
 189 template, so that it simply returns a mapping of type variables to
 190 types.  It also fails on nested foralls.
 191
 192 @matchTys@ matches corresponding elements of a list of templates and
 193 types.  It and @matchTy@ both ignore usage annotations, unlike the
 194 main function @match@.
 195
 196 \begin{code}
 197 matchTy :: TyVarSet                     -- Template tyvars
 198         -> Type                         -- Template
 199         -> Type                         -- Proposed instance of template
 200         -> Maybe TyVarSubstEnv          -- Matching substitution
 201
 202
 203 matchTys :: TyVarSet                    -- Template tyvars
 204          -> [Type]                      -- Templates
 205          -> [Type]                      -- Proposed instance of template
 206          -> Maybe (TyVarSubstEnv,               -- Matching substitution
 207                    [Type])              -- Left over instance types
 208
 209 matchTy tmpls ty1 ty2 = match False ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
 210
 211 matchTys tmpls tys1 tys2 = match_list False tys1 tys2 tmpls
 212                                       (\ (senv,tys) -> Just (senv,tys))
 213                                       emptySubstEnv
 214 \end{code}
 215
 216 @match@ is the main function.  It takes a flag indicating whether
 217 usage annotations are to be respected.
 218
 219 \begin{code}
 220 match :: Bool                                   -- Respect usages?
 221       -> Type -> Type                           -- Current match pair
 222       -> TyVarSet                               -- Template vars
 223       -> (TyVarSubstEnv -> Maybe result)        -- Continuation
 224       -> TyVarSubstEnv                          -- Current subst
 225       -> Maybe result
 226
 227 -- When matching against a type variable, see if the variable
 228 -- has already been bound.  If so, check that what it's bound to
 229 -- is the same as ty; if not, bind it and carry on.
 230
 231 match uflag (TyVarTy v) ty tmpls k senv
 232   | v `elemVarSet` tmpls
 233   =     -- v is a template variable
 234     case lookupSubstEnv senv v of
 235         Nothing -> UASSERT( not (isUTy ty) )
 236                    k (extendSubstEnv senv v (DoneTy ty))
 237         Just (DoneTy ty')  | ty' == ty         -> k senv   -- Succeeds
 238                            | otherwise         -> Nothing  -- Fails
 239
 240   | otherwise
 241   =     -- v is not a template variable; ty had better match
 242         -- Can't use (==) because types differ
 243     case deNoteType ty of
 244         TyVarTy v' | v == v' -> k senv    -- Success
 245         other                -> Nothing   -- Failure
 246     -- This deNoteType is *required* and cost me much pain.  I guess
 247     -- the reason the Note-stripping case is *last* rather than first
 248     -- is to preserve type synonyms etc., so I'm not moving it to the
 249     -- top; but this means that (without the deNotetype) a type
 250     -- variable may not match the pattern (TyVarTy v') as one would
 251     -- expect, due to an intervening Note.  KSW 2000-06.
 252
 253 match uflag (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
 254   = match uflag arg1 arg2 tmpls (match uflag res1 res2 tmpls k) senv
 255
 256 match uflag (AppTy fun1 arg1) ty2 tmpls k senv
 257   = case splitAppTy_maybe ty2 of
 258         Just (fun2,arg2) -> match uflag fun1 fun2 tmpls (match uflag arg1 arg2 tmpls k) senv
 259         Nothing          -> Nothing     -- Fail
 260
 261 match uflag (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
 262   | tc1 == tc2
 263   = match_list uflag tys1 tys2 tmpls k' senv
 264   where
 265     k' (senv', tys2') | null tys2' = k senv'    -- Succeed
 266                       | otherwise  = Nothing    -- Fail
 267
 268 match False (UsageTy _ ty1) ty2 tmpls k senv = match False ty1 ty2 tmpls k senv
 269 match False ty1 (UsageTy _ ty2) tmpls k senv = match False ty1 ty2 tmpls k senv
 270
 271 match True (UsageTy u1 ty1) (UsageTy u2 ty2) tmpls k senv
 272   = match True u1 u2 tmpls (match True ty1 ty2 tmpls k) senv
 273 match True ty1@(UsageTy _ _) ty2 tmpls k senv
 274   = case splitUTy ty2 of { (u,ty2') -> match True ty1 ty2' tmpls k senv }
 275 match True ty1 ty2@(UsageTy _ _) tmpls k senv
 276   = case splitUTy ty1 of { (u,ty1') -> match True ty1' ty2 tmpls k senv }
 277
 278         -- With type synonyms, we have to be careful for the exact
 279         -- same reasons as in the unifier.  Please see the
 280         -- considerable commentary there before changing anything
 281         -- here! (WDP 95/05)
 282 match uflag (NoteTy _ ty1) ty2      tmpls k senv = match uflag ty1 ty2 tmpls k senv
 283 match uflag ty1      (NoteTy _ ty2) tmpls k senv = match uflag ty1 ty2 tmpls k senv
 284
 285 -- Catch-all fails
 286 match _ _ _ _ _ _ = Nothing
 287
 288 match_list uflag []         tys2       tmpls k senv = k (senv, tys2)
 289 match_list uflag (ty1:tys1) []         tmpls k senv = Nothing   -- Not enough arg tys => failure
 290 match_list uflag (ty1:tys1) (ty2:tys2) tmpls k senv
 291   = match uflag ty1 ty2 tmpls (match_list uflag tys1 tys2 tmpls k) senv
 292 \end{code}
 293
 294