X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FUnify.lhs;h=8ffee8910c6965d6b75ac88f9e20086d1e40e3cb;hb=6a05ec5ef5373f61b7f9f5bdc344483417fa801b;hp=9d94a63961e5f9a67e9515144c5915f711198a10;hpb=ab22f4e6456820c1b5169d75f5975a94e61f54ce;p=ghc-hetmet.git

diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 9d94a63..8ffee89 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -3,11 +3,21 @@
 %
 
 \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
 	--	respects newtypes (rather than looking through them)
-	tcMatchTys, tcMatchTyX, ruleMatchTyX, tcMatchPreds, MatchEnv(..)
+	tcMatchTy, tcMatchTys, tcMatchTyX, 
+	ruleMatchTyX, tcMatchPreds, MatchEnv(..),
+	
+	dataConCannotMatch
    ) where
 
 #include "HsVersions.h"
@@ -16,8 +26,12 @@ import Var
 import VarEnv
 import VarSet
 import Type
+import Coercion
+import TyCon
+import DataCon
 import TypeRep
 import Outputable
+import Util
 import Maybes
 \end{code}
 
@@ -57,10 +71,26 @@ data MatchEnv
  	, me_env   :: RnEnv2	-- Renaming envt for nested foralls
 	}			--   In-scope set includes template tyvars
 
+tcMatchTy :: TyVarSet		-- Template tyvars
+	  -> Type		-- Template
+	  -> Type		-- Target
+	  -> Maybe TvSubst	-- One-shot; in principle the template
+				-- variables could be free in the target
+
+tcMatchTy tmpls ty1 ty2
+  = case match menv emptyTvSubstEnv ty1 ty2 of
+	Just subst_env -> Just (TvSubst in_scope subst_env)
+	Nothing	       -> Nothing
+  where
+    menv     = ME { me_tmpls = tmpls, me_env = mkRnEnv2 in_scope }
+    in_scope = mkInScopeSet (tmpls `unionVarSet` tyVarsOfType ty2)
+	-- We're assuming that all the interesting 
+	-- tyvars in tys1 are in tmpls
+
 tcMatchTys :: TyVarSet		-- Template tyvars
-	 -> [Type]		-- Template
-	 -> [Type]		-- Target
-	 -> Maybe TvSubst	-- One-shot; in principle the template
+	   -> [Type]		-- Template
+	   -> [Type]		-- Target
+	   -> Maybe TvSubst	-- One-shot; in principle the template
 				-- variables could be free in the target
 
 tcMatchTys tmpls tys1 tys2
@@ -120,24 +150,25 @@ match :: MatchEnv	-- For the most part this is pushed downwards
 -- it respects NewTypes and PredType
 
 match menv subst ty1 ty2 | Just ty1' <- tcView ty1 = match menv subst ty1' ty2
-match menv subst ty1 ty2 | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
+			 | Just ty2' <- tcView ty2 = match menv subst ty1 ty2'
 
 match menv subst (TyVarTy tv1) ty2
-  | tv1 `elemVarSet` me_tmpls menv
+  | tv1' `elemVarSet` me_tmpls menv
   = case lookupVarEnv subst tv1' of
-	Nothing | 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)
-
-	Just ty1' | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
+	Nothing 	-- No existing binding
+	    | any (inRnEnvR rn_env) (varSetElems (tyVarsOfType ty2))
+	    -> Nothing	-- Occurs check
+	    | otherwise	
+	    -> do { subst1 <- match_kind menv subst tv1 ty2
+		  ; return (extendVarEnv subst tv1' ty2) }
+
+	Just ty1' 	-- There is an existing binding; check whether ty2 matches it
+	    | tcEqTypeX (nukeRnEnvL rn_env) ty1' ty2
 		-- ty1 has no locally-bound variables, hence nukeRnEnvL
 		-- Note tcEqType...we are doing source-type matching here
-		  -> Just subst
-
-	other -> Nothing
+	    -> Just subst
+	    | otherwise	-> Nothing	-- ty2 doesn't match
+	    
 
    | otherwise	-- tv1 is not a template tyvar
    = case ty2 of
@@ -161,6 +192,7 @@ match menv subst (FunTy ty1a ty1b) (FunTy ty2a ty2b)
        ; match menv subst' ty1b ty2b }
 match menv subst (AppTy ty1a ty1b) ty2
   | Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
+	-- 'repSplit' used because the tcView stuff is done above
   = do { subst' <- match menv subst ty1a ty2a
        ; match menv subst' ty1b ty2b }
 
@@ -168,6 +200,33 @@ match menv subst ty1 ty2
   = 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 menv subst tys1 tys2 = match_list (match menv) subst tys1 tys2
 
 --------------
@@ -187,3 +246,125 @@ match_pred menv subst p1 p2 = Nothing
 \end{code}
 
 
+%************************************************************************
+%*									*
+		GADTs
+%*									*
+%************************************************************************
+
+Note [Pruning dead case alternatives]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider	data T a where
+		   T1 :: T Int
+		   T2 :: T a
+
+		newtype X = MkX Int
+		newtype Y = MkY Char
+
+		type family F a
+		type instance F Bool = Int
+
+Now consider	case x of { T1 -> e1; T2 -> e2 }
+
+The question before the house is this: if I know something about the type
+of x, can I prune away the T1 alternative?
+
+Suppose x::T Char.  It's impossible to construct a (T Char) using T1, 
+	Answer = YES (clearly)
+
+Suppose x::T (F a), where 'a' is in scope.  Then 'a' might be instantiated
+to 'Bool', in which case x::T Int, so
+	ANSWER = NO (clearly)
+
+Suppose x::T X.  Then *in Haskell* it's impossible to construct a (non-bottom) 
+value of type (T X) using T1.  But *in FC* it's quite possible.  The newtype
+gives a coercion
+	CoX :: X ~ Int
+So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
+of type (T X) constructed with T1.  Hence
+	ANSWER = NO (surprisingly)
+
+Furthermore, this can even happen; see Trac #1251.  GHC's newtype-deriving
+mechanism uses a cast, just as above, to move from one dictionary to another,
+in effect giving the programmer access to CoX.
+
+Finally, suppose x::T Y.  Then *even in FC* we can't construct a
+non-bottom value of type (T Y) using T1.  That's because we can get
+from Y to Char, but not to Int.
+
+
+Here's a related question.  	data Eq a b where EQ :: Eq a a
+Consider
+	case x of { EQ -> ... }
+
+Suppose x::Eq Int Char.  Is the alternative dead?  Clearly yes.
+
+What about x::Eq Int a, in a context where we have evidence that a~Char.
+Then again the alternative is dead.   
+
+
+			Summary
+
+We are really doing a test for unsatisfiability of the type
+constraints implied by the match. And that is clearly, in general, a
+hard thing to do.  
+
+However, since we are simply dropping dead code, a conservative test
+suffices.  There is a continuum of tests, ranging from easy to hard, that
+drop more and more dead code.
+
+For now we implement a very simple test: type variables match
+anything, type functions (incl newtypes) match anything, and only
+distinct data types fail to match.  We can elaborate later.
+
+\begin{code}
+dataConCannotMatch :: [Type] -> DataCon -> Bool
+-- Returns True iff the data con *definitely cannot* match a 
+--		    scrutinee of type (T tys)
+--		    where T is the type constructor for the data con
+--
+dataConCannotMatch tys con
+  | null eq_spec      = False	-- Common
+  | all isTyVarTy tys = False	-- Also common
+  | otherwise
+  = cant_match_s (map (substTyVar subst . fst) eq_spec)
+	         (map snd eq_spec)
+  where
+    dc_tvs  = dataConUnivTyVars con
+    eq_spec = dataConEqSpec con
+    subst   = zipTopTvSubst dc_tvs tys
+
+    cant_match_s :: [Type] -> [Type] -> Bool
+    cant_match_s tys1 tys2 = ASSERT( equalLength tys1 tys2 )
+			     or (zipWith cant_match tys1 tys2)
+
+    cant_match :: Type -> Type -> Bool
+    cant_match t1 t2
+	| Just t1' <- coreView t1 = cant_match t1' t2
+	| Just t2' <- coreView t2 = cant_match t1 t2'
+
+    cant_match (FunTy a1 r1) (FunTy a2 r2)
+	= cant_match a1 a2 || cant_match r1 r2
+
+    cant_match (TyConApp tc1 tys1) (TyConApp tc2 tys2)
+	| isDataTyCon tc1 && isDataTyCon tc2
+	= tc1 /= tc2 || cant_match_s tys1 tys2
+
+    cant_match (FunTy {}) (TyConApp tc _) = isDataTyCon tc
+    cant_match (TyConApp tc _) (FunTy {}) = isDataTyCon tc
+	-- tc can't be FunTyCon by invariant
+
+    cant_match (AppTy f1 a1) ty2
+	| Just (f2, a2) <- repSplitAppTy_maybe ty2
+	= cant_match f1 f2 || cant_match a1 a2
+    cant_match ty1 (AppTy f2 a2)
+	| Just (f1, a1) <- repSplitAppTy_maybe ty1
+	= cant_match f1 f2 || cant_match a1 a2
+
+    cant_match ty1 ty2 = False	-- Safe!
+
+-- Things we could add;
+--	foralls
+--	look through newtypes
+--	take account of tyvar bindings (EQ example above)
+\end{code}
\ No newline at end of file