X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcType.lhs;h=af03b7aa56ec9c0e41325139ce735036a0e26be5;hb=25ef3ade4257614cd966e29d0ed595c9db5587a7;hp=753ad4ffdf9ef74455a1a92299b3733c96fca8cb;hpb=49ac6c398f2915de9eadff3cd2631bc31f806ec8;p=ghc-hetmet.git

diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index 753ad4f..af03b7a 100644
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -22,7 +22,7 @@ module TcType (
 
   --------------------------------
   -- TyVarDetails
-  TyVarDetails(..), isUserTyVar, isSkolemTyVar, 
+  TyVarDetails(..), isUserTyVar, isSkolemTyVar, isExistentialTyVar,
   tyVarBindingInfo,
 
   --------------------------------
@@ -248,6 +248,14 @@ data TyVarDetails
    | PatSigTv	-- Scoped type variable, introduced by a pattern
 		-- type signature	\ x::a -> e
 
+   | ExistTv	-- An existential type variable bound by a pattern for
+		-- a data constructor with an existential type. E.g.
+		--	data T = forall a. Eq a => MkT a
+		-- 	f (MkT x) = ...
+		-- The pattern MkT x will allocate an existential type
+		-- variable for 'a'.  We distinguish these from all others
+		-- on one place, namely InstEnv.lookupInstEnv.
+
    | VanillaTv	-- Everything else
 
 isUserTyVar :: TcTyVar -> Bool	-- Avoid unifying these if possible
@@ -257,10 +265,16 @@ isUserTyVar tv = case tcTyVarDetails tv of
 
 isSkolemTyVar :: TcTyVar -> Bool
 isSkolemTyVar tv = case tcTyVarDetails tv of
-		      SigTv  -> True
-		      ClsTv  -> True
-		      InstTv -> True
-		      oteher -> False
+		      SigTv   -> True
+		      ClsTv   -> True
+		      InstTv  -> True
+		      ExistTv -> True
+		      other   -> False
+
+isExistentialTyVar :: TcTyVar -> Bool
+isExistentialTyVar tv = case tcTyVarDetails tv of
+			      ExistTv -> True
+			      other   -> False
 
 tyVarBindingInfo :: TcTyVar -> SDoc	-- Used in checkSigTyVars
 tyVarBindingInfo tv
@@ -271,6 +285,7 @@ tyVarBindingInfo tv
     details ClsTv     = ptext SLIT("class declaration")
     details InstTv    = ptext SLIT("instance declaration")
     details PatSigTv  = ptext SLIT("pattern type signature")
+    details ExistTv   = ptext SLIT("existential constructor")
     details VanillaTv = ptext SLIT("//vanilla//")	-- Ditto
 \end{code}
 
@@ -493,7 +508,7 @@ allDistinctTyVars (ty:tys) acc
 tcSplitPredTy_maybe :: Type -> Maybe PredType
    -- Returns Just for predicates only
 tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
-tcSplitPredTy_maybe (PredTy p)  = Just p
+tcSplitPredTy_maybe (PredTy p)    = Just p
 tcSplitPredTy_maybe other	  = Nothing
 	
 predTyUnique :: PredType -> Unique
@@ -866,7 +881,9 @@ toDNType ty
 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
 	-- Look through newtypes
 	-- Non-recursive ones are transparent to splitTyConApp,
-	-- but recursive ones aren't
+	-- but recursive ones aren't.  Manuel had:
+	--	newtype T = MkT (Ptr T)
+	-- and wanted it to work...
 checkRepTyCon check_tc ty 
   | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
   | otherwise				  	    = False
@@ -1121,7 +1138,7 @@ match (TyVarTy v) ty tmpls k senv
   | v `elemVarSet` tmpls
   =     -- v is a template variable
     case lookupSubstEnv senv v of
-	Nothing | typeKind ty == tyVarKind v	
+	Nothing | typeKind ty `isSubKind` tyVarKind v	
 			-- We do a kind check, just as in the uVarX above
 			-- The kind check is needed to avoid bogus matches
 			-- of (a b) with (c d), where the kinds don't match
@@ -1156,12 +1173,14 @@ match (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) tmpls k senv
 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
   = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
 
+	-- If the template is an application, try to make the 
+	-- thing we are matching look like an application
 match (AppTy fun1 arg1) ty2 tmpls k senv 
   = case tcSplitAppTy_maybe ty2 of
 	Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
 	Nothing 	 -> Nothing	-- Fail
 
--- Newtypes are opaque; predicate types should not happen
+	-- Newtypes are opaque; predicate types should not happen
 match (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) tmpls k senv
   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv