X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=63c64f07a1f7dc07f258d679bb5e84856fc8ca5e;hb=2e3b6bd7e00fa3faaa07ea0badee7f020a7c8306;hp=edec800d7bb0200daf4c4f201a44959399e6aa62;hpb=7fc749a43b4b6b85d234fa95d4928648259584f4;p=ghc-hetmet.git

diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index edec800..63c64f0 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -3,13 +3,6 @@
 %
 
 \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
@@ -20,12 +13,15 @@ module Unify (
 	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
@@ -145,11 +141,12 @@ match :: MatchEnv	-- For the most part this is pushed downwards
 			--	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
@@ -157,10 +154,10 @@ match menv subst (TyVarTy tv1) ty2
 	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
@@ -173,7 +170,7 @@ match menv subst (TyVarTy tv1) 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
@@ -196,26 +193,55 @@ match menv subst (AppTy ty1a ty1b) ty2
   = 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}
 
 
@@ -334,7 +360,7 @@ dataConCannotMatch tys con
 	| 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