X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcType.lhs;h=b9ff393b608e5a6a9eb9ea9c5fbc94e02665d2bb;hb=ff818166a0a06e77becad9e28ed116f3b7f5cc8b;hp=c1199384f9ed9fe9c77cd99371913d6bcc97a3ab;hpb=8254dcf1884fde961c477d5784024ec8ab1d84d2;p=ghc-hetmet.git

diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index c119938..b9ff393 100644
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -22,10 +22,10 @@ module TcType (
 
   --------------------------------
   -- MetaDetails
-  TcTyVarDetails(..),
-  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar,
-  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef,
-  isFlexi, isIndirect,
+  Expected(..), TcRef, TcTyVarDetails(..),
+  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
+  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
+  isFlexi, isIndirect, 
 
   --------------------------------
   -- Builders
@@ -94,7 +94,7 @@ module TcType (
   -- Type substitutions
   TvSubst(..), 	-- Representation visible to a few friends
   TvSubstEnv, emptyTvSubst,
-  mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
+  mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
   getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
   extendTvSubst, extendTvSubstList, isInScope,
   substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
@@ -104,7 +104,7 @@ module TcType (
   isPrimitiveType, 
 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
-  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
+  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
   typeKind, 
 
   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
@@ -146,7 +146,7 @@ import Type		(	-- Re-exports
 
 			  TvSubst(..),
 			  TvSubstEnv, emptyTvSubst,
-			  mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
+			  mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
 			  getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
 			  extendTvSubst, extendTvSubstList, isInScope,
 		  	  substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
@@ -159,7 +159,7 @@ import Type		(	-- Re-exports
 import TyCon		( TyCon, isUnLiftedTyCon, tyConUnique )
 import DataCon		( DataCon )
 import Class		( Class )
-import Var		( TyVar, Id, isTcTyVar, tcTyVarDetails )
+import Var		( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
 import ForeignCall	( Safety, playSafe, DNType(..) )
 import VarSet
 
@@ -167,6 +167,7 @@ import VarSet
 import CmdLineOpts	( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
 import Name		( Name, NamedThing(..), mkInternalName, getSrcLoc )
 import NameSet
+import VarEnv		( TidyEnv )
 import OccName		( OccName, mkDictOcc )
 import PrelNames	-- Lots (e.g. in isFFIArgumentTy)
 import TysWiredIn	( unitTyCon, charTyCon, listTyCon )
@@ -228,6 +229,10 @@ type TcRhoType      = TcType
 type TcTauType      = TcType
 type TcKind         = Kind
 type TcTyVarSet     = TyVarSet
+
+type TcRef a 	 = IORef a
+data Expected ty = Infer (TcRef ty)	-- The hole to fill in for type inference
+		 | Check ty		-- The type to check during type checking
 \end{code}
 
 
@@ -242,13 +247,45 @@ checking.  It's attached to mutable type variables only.
 It's knot-tied back to Var.lhs.  There is no reason in principle
 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 
+Note [Signature skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+
+  x :: [a]
+  y :: b
+  (x,y,z) = ([y,z], z, head x)
+
+Here, x and y have type sigs, which go into the environment.  We used to
+instantiate their types with skolem constants, and push those types into
+the RHS, so we'd typecheck the RHS with type
+	( [a*], b*, c )
+where a*, b* are skolem constants, and c is an ordinary meta type varible.
+
+The trouble is that the occurrences of z in the RHS force a* and b* to 
+be the *same*, so we can't make them into skolem constants that don't unify
+with each other.  Alas.
+
+On the other hand, we *must* use skolems for signature type variables, 
+becuase GADT type refinement refines skolems only.  
+
+One solution woudl be insist that in the above defn the programmer uses
+the same type variable in both type signatures.  But that takes explanation.
+
+The alternative (currently implemented) is to have a special kind of skolem
+constant, SigSkokTv, which can unify with other SigSkolTvs.  
+
+
 \begin{code}
 type TcTyVar = TyVar  	-- Used only during type inference
 
 -- A TyVarDetails is inside a TyVar
 data TcTyVarDetails
-  = SkolemTv SkolemInfo		-- A skolem constant
-  | MetaTv (IORef MetaDetails)	-- A meta type variable stands for a tau-type
+  = MetaTv (IORef MetaDetails)		-- A meta type variable stands for a tau-type
+  | SkolemTv SkolemInfo			-- A skolem constant
+  | SigSkolTv Name (IORef MetaDetails)	-- Ditto, but from a type signature;
+					-- 	see Note [Signature skolems]
+					--	The MetaDetails, if filled in, will 
+					-- 	always be another SigSkolTv
 
 data SkolemInfo
   = SigSkol Name	-- Bound at a type signature
@@ -262,7 +299,8 @@ data SkolemInfo
 			-- variable for 'a'.  
   | ArrowSkol SrcSpan	-- An arrow form (see TcArrows)
 
-  | GenSkol TcType	-- Bound when doing a subsumption check for this type
+  | GenSkol [TcTyVar]	-- Bound when doing a subsumption check for 
+	    TcType	-- 	(forall tvs. ty)
 	    SrcSpan
 
 data MetaDetails
@@ -272,20 +310,38 @@ data MetaDetails
   | Indirect TcType  -- Type indirections, treated as wobbly 
                      -- for the purpose of GADT unification.
 
-pprSkolemTyVar :: TcTyVar -> SDoc
-pprSkolemTyVar tv
+tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
+-- Tidy the type inside a GenSkol, preparatory to printing it
+tidySkolemTyVar env tv
   = ASSERT( isSkolemTyVar tv )
-    quotes (ppr tv) <+> ptext SLIT("is bound by") <+> ppr (skolemTvInfo tv)
-
-instance Outputable SkolemInfo where
-  ppr (SigSkol id)  = ptext SLIT("the type signature for") <+> quotes (ppr id)
-  ppr (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
-  ppr (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
-  ppr (ArrowSkol loc)  = ptext SLIT("the arrow form at") <+> ppr loc
-  ppr (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
-	       		    nest 2 (ptext SLIT("at") <+> ppr loc)]
-  ppr (GenSkol ty loc) = sep [ptext SLIT("the polymorphic type") <+> quotes (ppr ty),
-			    nest 2 (ptext SLIT("at") <+> ppr loc)]
+    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
+  where
+    (env1, info1) = case tcTyVarDetails tv of
+		      SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))
+			    where
+			      (env1, tvs1) = tidyOpenTyVars env tvs
+			      (env2, ty1)  = tidyOpenType env1 ty
+		      info -> (env, info)
+		     
+pprTcTyVar :: TcTyVar -> SDoc
+-- Print tyvar with info about its binding
+pprTcTyVar tv
+  = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
+  where
+    ppr_details (MetaTv _)	 = ptext SLIT("is a meta type variable")
+    ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id)
+    ppr_details (SkolemTv info)  = ptext SLIT("is bound by") <+> pprSkolInfo info
+ 
+pprSkolInfo :: SkolemInfo -> SDoc
+pprSkolInfo (SigSkol id)     = ptext SLIT("the type signature for") <+> quotes (ppr id)
+pprSkolInfo (ClsSkol cls)    = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo (InstSkol df)    = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
+pprSkolInfo (ArrowSkol loc)  = ptext SLIT("the arrow form at") <+> ppr loc
+pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
+           		            nest 2 (ptext SLIT("at") <+> ppr loc)]
+pprSkolInfo (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type") 
+				   	<+> quotes (ppr (mkForAllTys tvs ty)),
+				        nest 2 (ptext SLIT("at") <+> ppr loc)]
 
 instance Outputable MetaDetails where
   ppr Flexi 	    = ptext SLIT("Flexi")
@@ -299,8 +355,9 @@ isImmutableTyVar tv
 isSkolemTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-	SkolemTv _ -> True
-	MetaTv _   -> False
+	SkolemTv _    -> True
+	SigSkolTv _ _ -> True
+	MetaTv _      -> False
 
 isExistentialTyVar tv 	-- Existential type variable, bound by a pattern
   = ASSERT( isTcTyVar tv )
@@ -311,20 +368,15 @@ isExistentialTyVar tv 	-- Existential type variable, bound by a pattern
 isMetaTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-	SkolemTv _ -> False
 	MetaTv _   -> True
-
-skolemTvInfo :: TyVar -> SkolemInfo
-skolemTvInfo tv 
-  = ASSERT( isTcTyVar tv )
-    case tcTyVarDetails tv of
-	SkolemTv info -> info
+	other      -> False
 
 metaTvRef :: TyVar -> IORef MetaDetails
 metaTvRef tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-	 MetaTv ref -> ref
+	MetaTv ref -> ref
+	other	   -> pprPanic "metaTvRef" (ppr tv)
 
 isFlexi, isIndirect :: MetaDetails -> Bool
 isFlexi Flexi = True
@@ -679,7 +731,7 @@ hoistForAllTys ty
 	--	if t2 is a for-all type, push t1 inside it
 	--	if t2 is (pred -> t3), check for duplicates
     mk_fun_ty ty1 ty2
-	| not (isOverloadedTy ty2) 	-- No forall's, or context => 
+	| not (isSigmaTy ty2)	 	-- No forall's, or context => 
 	= FunTy ty1 ty2 	
 	| PredTy p1 <- ty1		-- ty1 is a predicate
 	= if p1 `elem` theta then 	-- so check for duplicates