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 ( Subst,
  11                unifyTysX, unifyTyListsX,
  12                matchTy, matchTys
  13   ) where
  14
  15 import Var      ( GenTyVar, TyVar, tyVarKind )
  16 import VarEnv
  17 import VarSet   ( varSetElems )
  18 import Type     ( GenType(..), funTyCon, typeKind, tyVarsOfType, hasMoreBoxityInfo,
  19                   splitAppTy_maybe
  20                 )
  21 import Unique   ( Uniquable(..) )
  22 import Outputable( panic )
  23 import Util     ( snocView )
  24 \end{code}
  25
  26 %************************************************************************
  27 %*                                                                      *
  28 \subsection{Unification wih a explicit substitution}
  29 %*                                                                      *
  30 %************************************************************************
  31
  32 Unify types with an explicit substitution and no monad.
  33
  34 \begin{code}
  35 type Subst flexi_tmpl flexi_result
  36    = ([GenTyVar flexi_tmpl],            -- Set of template tyvars
  37       TyVarEnv (GenType flexi_result))  -- Not necessarily idempotent
  38
  39 unifyTysX :: [GenTyVar flexi]           -- Template tyvars
  40           -> GenType flexi
  41           -> GenType flexi
  42           -> Maybe (TyVarEnv (GenType flexi))
  43 unifyTysX tmpl_tyvars ty1 ty2
  44   = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptyVarEnv)
  45
  46 unifyTyListsX :: [GenTyVar flexi] -> [GenType flexi] -> [GenType flexi]
  47               -> Maybe (TyVarEnv (GenType flexi))
  48 unifyTyListsX tmpl_tyvars tys1 tys2
  49   = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptyVarEnv)
  50
  51
  52 uTysX :: GenType flexi
  53       -> GenType flexi
  54       -> (Subst flexi flexi -> Maybe result)
  55       -> Subst flexi flexi
  56       -> Maybe result
  57
  58 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
  59 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
  60
  61         -- Variables; go for uVar
  62 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
  63   | tyvar1 == tyvar2
  64   = k subst
  65 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
  66   | tyvar1 `elem` tmpls
  67   = uVarX tyvar1 ty2 k subst
  68 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
  69   | tyvar2 `elem` tmpls
  70   = uVarX tyvar2 ty1 k subst
  71
  72         -- Functions; just check the two parts
  73 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
  74   = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
  75
  76         -- Type constructors must match
  77 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
  78   | (con1 == con2 && length tys1 == length tys2)
  79   = uTyListsX tys1 tys2 k subst
  80
  81         -- Applications need a bit of care!
  82         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
  83         -- NB: we've already dealt with type variables and Notes,
  84         -- so if one type is an App the other one jolly well better be too
  85 uTysX (AppTy s1 t1) ty2 k subst
  86   = case splitAppTy_maybe ty2 of
  87       Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
  88       Nothing       -> Nothing    -- Fail
  89
  90 uTysX ty1 (AppTy s2 t2) k subst
  91   = case splitAppTy_maybe ty1 of
  92       Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
  93       Nothing       -> Nothing    -- Fail
  94
  95         -- Not expecting for-alls in unification
  96 #ifdef DEBUG
  97 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
  98 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
  99 #endif
 100
 101         -- Anything else fails
 102 uTysX ty1 ty2 k subst = Nothing
 103
 104
 105 uTyListsX []         []         k subst = k subst
 106 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
 107 uTyListsX tys1       tys2       k subst = Nothing   -- Fail if the lists are different lengths
 108 \end{code}
 109
 110 \begin{code}
 111 -- Invariant: tv1 is a unifiable variable
 112 uVarX tv1 ty2 k subst@(tmpls, env)
 113   = case lookupVarEnv env tv1 of
 114       Just ty1 ->    -- Already bound
 115                      uTysX ty1 ty2 k subst
 116
 117       Nothing        -- Not already bound
 118                |  typeKind ty2 `hasMoreBoxityInfo` tyVarKind tv1
 119                && occur_check_ok ty2
 120                ->     -- No kind mismatch nor occur check
 121                   k (tmpls, extendVarEnv env tv1 ty2)
 122
 123                | otherwise -> Nothing   -- Fail if kind mis-match or occur check
 124   where
 125     occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
 126     occur_check_ok_tv tv | tv1 == tv = False
 127                          | otherwise = case lookupVarEnv env tv of
 128                                          Nothing -> True
 129                                          Just ty -> occur_check_ok ty
 130 \end{code}
 131
 132
 133
 134 %************************************************************************
 135 %*                                                                      *
 136 \subsection{Matching on types}
 137 %*                                                                      *
 138 %************************************************************************
 139
 140 Matching is a {\em unidirectional} process, matching a type against a
 141 template (which is just a type with type variables in it).  The
 142 matcher assumes that there are no repeated type variables in the
 143 template, so that it simply returns a mapping of type variables to
 144 types.  It also fails on nested foralls.
 145
 146 @matchTys@ matches corresponding elements of a list of templates and
 147 types.
 148
 149 \begin{code}
 150 matchTy :: [GenTyVar flexi_tmpl]                        -- Template tyvars
 151         -> GenType flexi_tmpl                           -- Template
 152         -> GenType flexi_result                         -- Proposed instance of template
 153         -> Maybe (TyVarEnv (GenType flexi_result))      -- Matching substitution
 154
 155
 156 matchTys :: [GenTyVar flexi_tmpl]                       -- Template tyvars
 157          -> [GenType flexi_tmpl]                        -- Templates
 158          -> [GenType flexi_result]                      -- Proposed instance of template
 159          -> Maybe (TyVarEnv (GenType flexi_result),     -- Matching substitution
 160                    [GenType flexi_result])              -- Left over instance types
 161
 162 matchTy  tmpls ty1  ty2  = match      ty1  ty2  (\(_,env)       -> Just env)
 163                                                 (tmpls, emptyVarEnv)
 164
 165 matchTys tmpls tys1 tys2 = match_list tys1 tys2 (\((_,env),tys) -> Just (env,tys))
 166                                                 (tmpls, emptyVarEnv)
 167 \end{code}
 168
 169 @match@ is the main function.
 170
 171 \begin{code}
 172 match :: GenType flexi_tmpl -> GenType flexi_result         -- Current match pair
 173       -> (Subst flexi_tmpl flexi_result -> Maybe result)    -- Continuation
 174       -> Subst flexi_tmpl flexi_result                      -- Current substitution
 175       -> Maybe result
 176
 177 -- When matching against a type variable, see if the variable
 178 -- has already been bound.  If so, check that what it's bound to
 179 -- is the same as ty; if not, bind it and carry on.
 180
 181 match (TyVarTy v) ty k = \  s@(tmpls,env) ->
 182                          if v `elem` tmpls then
 183                                -- v is a template variable
 184                                case lookupVarEnv env v of
 185                                   Nothing  -> k (tmpls, extendVarEnv env v ty)
 186                                   Just ty' | ty' == ty -> k s      -- Succeeds
 187                                            | otherwise -> Nothing  -- Fails
 188                          else
 189                                      -- v is not a template variable; ty had better match
 190                                      -- Can't use (==) because types differ
 191                                case ty of
 192                                   TyVarTy v' | getUnique v == getUnique v'
 193                                              -> k s       -- Success
 194                                   other      -> Nothing   -- Failure
 195
 196 match (FunTy arg1 res1)   (FunTy arg2 res2)   k = match arg1 arg2 (match res1 res2 k)
 197 match (AppTy fun1 arg1)   ty2                 k = case splitAppTy_maybe ty2 of
 198                                                         Just (fun2,arg2) -> match fun1 fun2 (match arg1 arg2 k)
 199                                                         Nothing          -> \ _ -> Nothing      -- Fail
 200 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) k | tc1 == tc2
 201                                                 = match_list tys1 tys2 ( \(s,tys2') ->
 202                                                   if null tys2' then
 203                                                         k s     -- Succeed
 204                                                   else
 205                                                         Nothing -- Fail
 206                                                   )
 207
 208         -- With type synonyms, we have to be careful for the exact
 209         -- same reasons as in the unifier.  Please see the
 210         -- considerable commentary there before changing anything
 211         -- here! (WDP 95/05)
 212 match (NoteTy _ ty1) ty2           k = match ty1 ty2 k
 213 match ty1           (NoteTy _ ty2) k = match ty1 ty2 k
 214
 215 -- Catch-all fails
 216 match _ _ _ = \s -> Nothing
 217
 218 match_list []         tys2       k = \s -> k (s, tys2)
 219 match_list (ty1:tys1) []         k = \s -> Nothing      -- Not enough arg tys => failure
 220 match_list (ty1:tys1) (ty2:tys2) k = match ty1 ty2 (match_list tys1 tys2 k)
 221 \end{code}
 222