X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=3357004df441aedb86d08f6ae57b5aa1faf7fde9;hb=85e16365444e938b4adff9d241d56df4c1fbca91;hp=dc811cb959e842d1873b3882c5d0bc52759d33f1;hpb=29897cfe9c9cf1363b89f4eb177c85329a8ca1e5;p=ghc-hetmet.git

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index dc811cb..3357004 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -26,7 +26,8 @@ module TcMType (
   newFlexiTyVarTys,		-- Int -> Kind -> TcM [TcType]
   newKindVar, newKindVars, 
   lookupTcTyVar, LookupTyVarResult(..),
-  newMetaTyVar, readMetaTyVar, writeMetaTyVar, 
+
+  newMetaTyVar, readMetaTyVar, writeMetaTyVar, isFilledMetaTyVar,
 
   --------------------------------
   -- Boxy type variables
@@ -39,7 +40,7 @@ module TcMType (
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
-  tcInstSigTyVars, zonkSigTyVar,
+  tcInstSigTyVars,
   tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, 
   tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
 
@@ -55,7 +56,7 @@ module TcMType (
   --------------------------------
   -- Zonking
   zonkType, zonkTcPredType, 
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
@@ -496,6 +497,15 @@ readMetaTyVar :: TyVar -> TcM MetaDetails
 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
 		      readMutVar (metaTvRef tyvar)
 
+isFilledMetaTyVar :: TyVar -> TcM Bool
+-- True of a filled-in (Indirect) meta type variable
+isFilledMetaTyVar tv
+  | not (isTcTyVar tv) = return False
+  | MetaTv _ ref <- tcTyVarDetails tv
+  = do 	{ details <- readMutVar ref
+	; return (isIndirect details) }
+  | otherwise = return False
+
 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
 #ifndef DEBUG
 writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
@@ -756,17 +766,17 @@ zonkTopTyVar tv
     k = tyVarKind tv
     default_k = defaultKind k
 
-zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar]
+zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
 zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar
 
-zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
+zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 --
 -- The quantified type variables often include meta type variables
 -- we want to freeze them into ordinary type variables, and
 -- default their kind (e.g. from OpenTypeKind to TypeKind)
 -- 			-- see notes with Kind.defaultKind
--- The meta tyvar is updated to point to the new regular TyVar.  Now any 
+-- The meta tyvar is updated to point to the new skolem TyVar.  Now any 
 -- bound occurences of the original type variable will get zonked to 
 -- the immutable version.
 --
@@ -780,9 +790,11 @@ zonkQuantifiedTyVar tv
   | otherwise	-- It's a meta-type-variable
   = do	{ details <- readMetaTyVar tv
 
-	-- Create the new, frozen, regular type variable
+	-- Create the new, frozen, skolem type variable
+        -- We zonk to a skolem, not to a regular TcVar
+        -- See Note [Zonking to Skolem]
 	; let final_kind = defaultKind (tyVarKind tv)
-	      final_tv   = mkTyVar (tyVarName tv) final_kind
+	      final_tv   = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
 
 	-- Bind the meta tyvar to the new tyvar
 	; case details of
@@ -797,8 +809,8 @@ zonkQuantifiedTyVar tv
 	; return final_tv }
 \end{code}
 
-[Silly Type Synonyms]
-
+Note [Silly Type Synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this:
 	type C u a = u	-- Note 'a' unused
 
@@ -832,6 +844,37 @@ Consider this:
 All very silly.   I think its harmless to ignore the problem.  We'll end up with
 a /\a in the final result but all the occurrences of a will be zonked to ()
 
+Note [Zonking to Skolem]
+~~~~~~~~~~~~~~~~~~~~~~~~
+We used to zonk quantified type variables to regular TyVars.  However, this
+leads to problems.  Consider this program from the regression test suite:
+
+  eval :: Int -> String -> String -> String
+  eval 0 root actual = evalRHS 0 root actual
+
+  evalRHS :: Int -> a
+  evalRHS 0 root actual = eval 0 root actual
+
+It leads to the deferral of an equality
+
+  (String -> String -> String) ~ a
+
+which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
+In the meantime `a' is zonked and quantified to form `evalRHS's signature.
+This has the *side effect* of also zonking the `a' in the deferred equality
+(which at this point is being handed around wrapped in an implication
+constraint).
+
+Finally, the equality (with the zonked `a') will be handed back to the
+simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
+If we zonk `a' with a regular type variable, we will have this regular type
+variable now floating around in the simplifier, which in many places assumes to
+only see proper TcTyVars.
+
+We can avoid this problem by zonking with a skolem.  The skolem is rigid
+(which we requirefor a quantified variable), but is still a TcTyVar that the
+simplifier knows how to deal with.
+
 
 %************************************************************************
 %*									*
@@ -1097,7 +1140,7 @@ check_tau_type rank ubx_tup (NoteTy other_note ty)
 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   | isSynTyCon tc
   = do	{ 	-- Check that the synonym has enough args
-		-- This applies eqaually to open and closed synonyms
+		-- This applies equally to open and closed synonyms
 	 	-- It's OK to have an *over-applied* type synonym
 		--	data Tree a b = ...
 		--	type Foo a = Tree [a]
@@ -1106,14 +1149,14 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
 
 	-- See Note [Liberal type synonyms]
 	; liberal <- doptM Opt_LiberalTypeSynonyms
-	; if not liberal then
-		-- For H98, do check the type args
+	; if not liberal || isOpenSynTyCon tc then
+		-- For H98 and synonym families, do check the type args
 		mappM_ check_arg_type tys
 
-	  else	-- In the liberal case, expand then check
+	  else	-- In the liberal case (only for closed syns), expand then check
 	  case tcView ty of   
 	     Just ty' -> check_tau_type rank ubx_tup ty' 
-	     Nothing -> pprPanic "check_tau_type" (ppr ty)
+	     Nothing  -> pprPanic "check_tau_type" (ppr ty)
     }
     
   | isUnboxedTupleTyCon tc