%
\begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
--- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
module Unify (
-- Matching of types:
-- the "tc" prefix indicates that matching always
dataConCannotMatch
) where
+-- XXX This define is a bit of a hack, and should be done more nicely
+#define FAST_STRING_NOT_NEEDED 1
#include "HsVersions.h"
import Var
import VarEnv
import VarSet
import Type
+import Coercion
import TyCon
import DataCon
import TypeRep
-- in-scope set of the RnEnv2
-> Type -> Type -- Template and target respectively
-> Maybe TvSubstEnv
--- This matcher works on source types; that is,
--- it respects NewTypes and PredType
+-- This matcher works on core types; that is, it ignores PredTypes
+-- Watch out if newtypes become transparent agin!
+-- this matcher must respect newtypes
-match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2
- | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
+match menv subst ty1 ty2 | Just ty1' <- coreView ty1 = match menv subst ty1' ty2
+ | Just ty2' <- coreView ty2 = match menv subst ty1 ty2'
match menv subst (TyVarTy tv1) ty2
| tv1' `elemVarSet` me_tmpls menv
Nothing -- No existing binding
| any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
-> Nothing -- Occurs check
- | not (typeKind ty2 `isSubKind` tyVarKind tv1)
- -> Nothing -- Kind mis-match
- | otherwise
- -> Just (extendVarEnv subst tv1' ty2)
+ | otherwise
+ -> do { subst1 <- match_kind menv subst tv1 ty2
+ ; return (extendVarEnv subst1 tv1' ty2) }
+ -- Note [Matching kinds]
Just ty1' -- There is an existing binding; check whether ty2 matches it
| tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
| otherwise -- tv1 is not a template tyvar
= case ty2 of
TyVarTy tv2 | tv1' == rnOccR rn_env tv2 -> Just subst
- other -> Nothing
+ _ -> Nothing
where
rn_env = me_env menv
tv1' = rnOccL rn_env tv1
= do { subst' <- match menv subst ty1a ty2a
; match menv subst' ty1b ty2b }
-match menv subst ty1 ty2
+match _ _ _ _
= Nothing
--------------
+match_kind :: MatchEnv -> TvSubstEnv -> TyVar -> Type -> Maybe TvSubstEnv
+-- Match the kind of the template tyvar with the kind of Type
+-- Note [Matching kinds]
+match_kind menv subst tv ty
+ | isCoVar tv = do { let (ty1,ty2) = splitCoercionKind (tyVarKind tv)
+ (ty3,ty4) = coercionKind ty
+ ; subst1 <- match menv subst ty1 ty3
+ ; match menv subst1 ty2 ty4 }
+ | otherwise = if typeKind ty `isSubKind` tyVarKind tv
+ then Just subst
+ else Nothing
+
+-- Note [Matching kinds]
+-- ~~~~~~~~~~~~~~~~~~~~~
+-- For ordinary type variables, we don't want (m a) to match (n b)
+-- if say (a::*) and (b::*->*). This is just a yes/no issue.
+--
+-- For coercion kinds matters are more complicated. If we have a
+-- coercion template variable co::a~[b], where a,b are presumably also
+-- template type variables, then we must match co's kind against the
+-- kind of the actual argument, so as to give bindings to a,b.
+--
+-- In fact I have no example in mind that *requires* this kind-matching
+-- to instantiate template type variables, but it seems like the right
+-- thing to do. C.f. Note [Matching variable types] in Rules.lhs
+
+--------------
+match_tys :: MatchEnv -> TvSubstEnv -> [Type] -> [Type] -> Maybe TvSubstEnv
match_tys menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
--------------
match_list :: (TvSubstEnv -> a -> a -> Maybe TvSubstEnv)
-> TvSubstEnv -> [a] -> [a] -> Maybe TvSubstEnv
-match_list fn subst [] [] = Just subst
+match_list _ subst [] [] = Just subst
match_list fn subst (ty1:tys1) (ty2:tys2) = do { subst' <- fn subst ty1 ty2
; match_list fn subst' tys1 tys2 }
-match_list fn subst tys1 tys2 = Nothing
+match_list _ _ _ _ = Nothing
--------------
+match_pred :: MatchEnv -> TvSubstEnv -> PredType -> PredType -> Maybe TvSubstEnv
match_pred menv subst (ClassP c1 tys1) (ClassP c2 tys2)
| c1 == c2 = match_tys menv subst tys1 tys2
match_pred menv subst (IParam n1 t1) (IParam n2 t2)
| n1 == n2 = match menv subst t1 t2
-match_pred menv subst p1 p2 = Nothing
+match_pred _ _ _ _ = Nothing
\end{code}
| Just (f1, a1) <- repSplitAppTy_maybe ty1
= cant_match f1 f2 || cant_match a1 a2
- cant_match ty1 ty2 = False -- Safe!
+ cant_match _ _ = False -- Safe!
-- Things we could add;
-- foralls