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