X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcBinds.lhs;h=c4e1b92f6c981640dce050094c6cfaeafa1b4d51;hb=ff818166a0a06e77becad9e28ed116f3b7f5cc8b;hp=a16cddcc0caf56c150181e25e5971110ff4e196e;hpb=8e67f5502e2e316245806ee3735a2f41a844b611;p=ghc-hetmet.git

diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs
index a16cddc..c4e1b92 100644
--- a/ghc/compiler/typecheck/TcBinds.lhs
+++ b/ghc/compiler/typecheck/TcBinds.lhs
@@ -39,7 +39,7 @@ import TcMType		( newTyFlexiVarTy, zonkQuantifiedTyVar,
 import TcType		( TcTyVar, SkolemInfo(SigSkol), 
 			  TcTauType, TcSigmaType, 
 			  mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType, 
-			  mkForAllTy, isUnLiftedType, tcGetTyVar_maybe, 
+			  mkForAllTy, isUnLiftedType, tcGetTyVar, 
 			  mkTyVarTys, tidyOpenTyVar, tidyOpenType )
 import Kind		( argTypeKind )
 import VarEnv		( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv, emptyTidyEnv ) 
@@ -561,26 +561,7 @@ getMonoBindInfo tc_binds
 %*									*
 %************************************************************************
 
-Type signatures are tricky.  Consider
-
-  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.
-
-Current solution: don't use skolems at all.  Instead, instantiate the type
-signatures with ordinary meta type variables, and check at the end that
-each group has remained distinct.
-
+Type signatures are tricky.  See Note [Signature skolems] in TcType
 
 \begin{code}
 tcTySigs :: [LSig Name] -> TcM [TcSigInfo]
@@ -612,8 +593,10 @@ tcTySig :: LSig Name -> TcM TcSigInfo
 tcTySig (L span (Sig (L _ name) ty))
   = setSrcSpan span		$
     do	{ sigma_ty <- tcHsSigType (FunSigCtxt name) ty
-	; let rigid_info = SigSkol name
-	      poly_id    = mkLocalId name sigma_ty
+	; (tvs, theta, tau) <- tcInstSigType name sigma_ty
+	; loc <- getInstLoc (SigOrigin (SigSkol name))
+
+	; let poly_id = mkLocalId name sigma_ty
 
 		-- The scoped names are the ones explicitly mentioned
 		-- in the HsForAll.  (There may be more in sigma_ty, because
@@ -622,8 +605,6 @@ tcTySig (L span (Sig (L _ name) ty))
 				L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs
 				other 		    	   -> []
 
-	; (tvs, theta, tau) <- tcInstSigType sigma_ty
-	; loc <- getInstLoc (SigOrigin rigid_info)
 	; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names,
 			      sig_tvs = tvs, sig_theta = theta, sig_tau = tau, 
 			      sig_loc = loc }) }
@@ -721,26 +702,26 @@ checkDistinctTyVars sig_tvs
 	; return zonked_tvs }
   where
     zonk_one sig_tv = do { ty <- zonkTcTyVar sig_tv
-		         ; case tcGetTyVar_maybe ty of
-			     Just tv' -> return tv'
-			     Nothing  -> bomb_out sig_tv "a type" ty }
+		         ; return (tcGetTyVar "checkDistinctTyVars" ty) }
+	-- 'ty' is bound to be a type variable, because SigSkolTvs
+	-- can only be unified with type variables
 
     check_dup :: TyVarEnv TcTyVar -> (TcTyVar, TcTyVar) -> TcM (TyVarEnv TcTyVar)
 	-- The TyVarEnv maps each zonked type variable back to its
 	-- corresponding user-written signature type variable
     check_dup acc (sig_tv, zonked_tv)
 	= case lookupVarEnv acc zonked_tv of
-		Just sig_tv' -> bomb_out sig_tv "another quantified type variable" 
-						(mkTyVarTy sig_tv')
+		Just sig_tv' -> bomb_out sig_tv sig_tv'
 
 		Nothing -> return (extendVarEnv acc zonked_tv sig_tv)
 
-    bomb_out sig_tv doc ty 
-       = failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv) 
-		     <+> ptext SLIT("is unified with") <+> text doc <+> ppr tidy_ty)
+    bomb_out sig_tv1 sig_tv2
+       = failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv1) 
+		     <+> ptext SLIT("is unified with another quantified type variable") 
+		     <+> ppr tidy_tv2)
        where
-	 (env1,  tidy_tv) = tidyOpenTyVar emptyTidyEnv sig_tv
-	 (_env2, tidy_ty) = tidyOpenType  env1	       ty
+	 (env1,  tidy_tv1) = tidyOpenTyVar emptyTidyEnv sig_tv1
+	 (_env2, tidy_tv2) = tidyOpenTyVar env1	        sig_tv2
 \end{code}