[project @ 1999-04-20 12:59:51 by simonpj]

Better typechecker error message when a type-signature variable is unified with a type

ghc/compiler/basicTypes/Var.lhs

@@ -15,8 +15,9 @@ module Var (
 	TyVar,
 	tyVarName, tyVarKind,
 	setTyVarName, setTyVarUnique,
-	mkTyVar, mkSysTyVar, isTyVar,
-	newMutTyVar, readMutTyVar, writeMutTyVar, isMutTyVar, makeTyVarImmutable,
+	mkTyVar, mkSysTyVar, isTyVar, isSigTyVar,
+	newMutTyVar, newSigTyVar,
+	readMutTyVar, writeMutTyVar, isMutTyVar, makeTyVarImmutable,
 
 	-- Ids
 	Id, DictId,
@@ -76,7 +77,9 @@ data VarDetails
   | ConstantId Con			-- The Id for a constant (data constructor or primop)
   | RecordSelId FieldLabel		-- The Id for a record selector
   | TyVar
-  | MutTyVar (IORef (Maybe Type))	-- Used during unification
+  | MutTyVar (IORef (Maybe Type)) 	-- Used during unification;
+	     Bool			-- True <=> this is a type signature variable, which
+					--	    should not be unified with a non-tyvar type
 
 -- For a long time I tried to keep mutable Vars statically type-distinct
 -- from immutable Vars, but I've finally given up.   It's just too painful.
@@ -177,13 +180,21 @@ newMutTyVar name kind =
      return (Var { varName = name, 
 		   realUnique = getKey (nameUnique name),
 		   varType = kind, 
-		   varDetails = MutTyVar loc })
+		   varDetails = MutTyVar loc False})
+
+newSigTyVar :: Name -> Kind -> IO TyVar
+newSigTyVar name kind = 
+  do loc <- newIORef Nothing
+     return (Var { varName = name, 
+		   realUnique = getKey (nameUnique name),
+		   varType = kind, 
+		   varDetails = MutTyVar loc True})
 
 readMutTyVar :: TyVar -> IO (Maybe Type)
-readMutTyVar (Var {varDetails = MutTyVar loc}) = readIORef loc
+readMutTyVar (Var {varDetails = MutTyVar loc _}) = readIORef loc
 
 writeMutTyVar :: TyVar -> Maybe Type -> IO ()
-writeMutTyVar (Var {varDetails = MutTyVar loc}) val = writeIORef loc val
+writeMutTyVar (Var {varDetails = MutTyVar loc _}) val = writeIORef loc val
 
 makeTyVarImmutable :: TyVar -> TyVar
 makeTyVarImmutable tyvar = tyvar { varDetails = TyVar}
@@ -192,13 +203,17 @@ makeTyVarImmutable tyvar = tyvar { varDetails = TyVar}
 \begin{code}
 isTyVar :: Var -> Bool
 isTyVar (Var {varDetails = details}) = case details of
-					TyVar      -> True
-					MutTyVar _ -> True
-					other	   -> False
+					TyVar        -> True
+					MutTyVar _ _ -> True
+					other	     -> False
 
 isMutTyVar :: Var -> Bool
-isMutTyVar (Var {varDetails = MutTyVar _}) = True
-isMutTyVar other			       = False
+isMutTyVar (Var {varDetails = MutTyVar _ _}) = True
+isMutTyVar other			     = False
+
+isSigTyVar :: Var -> Bool
+isSigTyVar (Var {varDetails = MutTyVar _ is_sig}) = is_sig
+isSigTyVar other			          = False
 \end{code}
 
 

ghc/compiler/typecheck/TcForeign.lhs

@@ -27,7 +27,7 @@ import RnHsSyn		( RenamedHsDecl, RenamedForeignDecl )
 
 import TcMonad
 import TcEnv		( newLocalId )
-import TcType		( tcInstTcType, typeToTcType, tcSplitRhoTy, zonkTcTypeToType )
+import TcType		( typeToTcType, tcSplitRhoTy, zonkTcTypeToType )
 import TcMonoType	( tcHsTopBoxedType )
 import TcHsSyn		( TcMonoBinds, TypecheckedForeignDecl,
 			  TcForeignExportDecl )

ghc/compiler/typecheck/TcMonad.lhs

@@ -32,7 +32,7 @@ module TcMonad(
 	tcAddErrCtxtM, tcSetErrCtxtM,
 	tcAddErrCtxt, tcSetErrCtxt,
 
-	tcNewMutVar, tcReadMutVar, tcWriteMutVar, TcRef,
+	tcNewMutVar, tcNewSigTyVar, tcReadMutVar, tcWriteMutVar, TcRef,
 	tcNewMutTyVar, tcReadMutTyVar, tcWriteMutTyVar,
 
 	TcError, TcWarning, TidyEnv, emptyTidyEnv,
@@ -52,7 +52,7 @@ import Bag		( Bag, emptyBag, isEmptyBag,
 			  foldBag, unitBag, unionBags, snocBag )
 import Class		( Class )
 import Name		( Name )
-import Var		( TyVar, newMutTyVar, readMutTyVar, writeMutTyVar )
+import Var		( TyVar, newMutTyVar, newSigTyVar, readMutTyVar, writeMutTyVar )
 import VarEnv		( TyVarEnv, emptyVarEnv, TidyEnv, emptyTidyEnv )
 import VarSet		( TyVarSet )
 import UniqSupply	( UniqSupply, uniqFromSupply, uniqsFromSupply, splitUniqSupply,
@@ -430,6 +430,9 @@ tcReadMutVar var down env = readIORef var
 tcNewMutTyVar :: Name -> Kind -> NF_TcM s TyVar
 tcNewMutTyVar name kind down env = newMutTyVar name kind
 
+tcNewSigTyVar :: Name -> Kind -> NF_TcM s TyVar
+tcNewSigTyVar name kind down env = newSigTyVar name kind
+
 tcReadMutTyVar :: TyVar -> NF_TcM s (Maybe Type)
 tcReadMutTyVar tyvar down env = readMutTyVar tyvar
 

ghc/compiler/typecheck/TcMonoType.lhs

@@ -22,18 +22,18 @@ import TcEnv		( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
 			  tcGetGlobalTyVars, TcTyThing(..)
 			)
 import TcType		( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
-			  typeToTcType, tcInstTcType, kindToTcKind,
-			  newKindVar,
+			  typeToTcType, kindToTcKind,
+			  newKindVar, tcInstSigVar,
 			  zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType
 			)
 import Inst		( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
 import TcUnify		( unifyKind, unifyKinds, unifyTypeKind )
 import Type		( Type, ThetaType, 
 			  mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, zipFunTys,
-			  mkSigmaTy, mkDictTy, mkTyConApp, mkAppTys, splitRhoTy,
+			  mkSigmaTy, mkDictTy, mkTyConApp, mkAppTys, splitForAllTys, splitRhoTy,
 			  boxedTypeKind, unboxedTypeKind, tyVarsOfType,
 			  mkArrowKinds, getTyVar_maybe, getTyVar,
-		  	  tidyOpenType, tidyOpenTypes, tidyTyVar
+		  	  tidyOpenType, tidyOpenTypes, tidyTyVar, fullSubstTy
 			)
 import Id		( mkUserId, idName, idType, idFreeTyVars )
 import Var		( TyVar, mkTyVar )
@@ -379,19 +379,26 @@ mkTcSig poly_id src_loc
 	-- the tyvars *do* get unified with something, we want to carry on
 	-- typechecking the rest of the program with the function bound
 	-- to a pristine type, namely sigma_tc_ty
-   tcInstTcType (idType poly_id)		`thenNF_Tc` \ (tyvars, rho) ->
    let
-     (theta, tau) = splitRhoTy rho
-	-- This splitSigmaTy tries hard to make sure that tau' is a type synonym
+	(tyvars, rho) = splitForAllTys (idType poly_id)
+   in
+   mapNF_Tc tcInstSigVar tyvars		`thenNF_Tc` \ tyvars' ->
+	-- Make *signature* type variables
+
+   let
+     tyvar_tys' = mkTyVarTys tyvars'
+     rho' = fullSubstTy (zipVarEnv tyvars tyvar_tys') emptyVarSet rho
+     (theta', tau') = splitRhoTy rho'
+	-- This splitRhoTy tries hard to make sure that tau' is a type synonym
 	-- wherever possible, which can improve interface files.
    in
    newMethodWithGivenTy SignatureOrigin 
 		poly_id
-		(mkTyVarTys tyvars) 
-		theta tau			`thenNF_Tc` \ inst ->
+		tyvar_tys'
+		theta' tau'			`thenNF_Tc` \ inst ->
 	-- We make a Method even if it's not overloaded; no harm
 	
-   returnNF_Tc (TySigInfo name poly_id tyvars theta tau (instToIdBndr inst) inst src_loc)
+   returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) inst src_loc)
   where
     name = idName poly_id
 \end{code}

ghc/compiler/typecheck/TcType.lhs

@@ -26,6 +26,7 @@ module TcType (
   tcSplitRhoTy,
 
   tcInstTyVars,
+  tcInstSigVar,
   tcInstTcType,
 
   typeToTcType,
@@ -172,13 +173,13 @@ tcInstTyVars :: [TyVar]
 	     -> NF_TcM s ([TcTyVar], [TcType], TyVarEnv TcType)
 
 tcInstTyVars tyvars
-  = mapNF_Tc inst_tyvar tyvars	`thenNF_Tc` \ tc_tyvars ->
+  = mapNF_Tc tcInstTyVar tyvars	`thenNF_Tc` \ tc_tyvars ->
     let
 	tys = mkTyVarTys tc_tyvars
     in
     returnNF_Tc (tc_tyvars, tys, zipVarEnv tyvars tys)
 
-inst_tyvar tyvar	-- Could use the name from the tyvar?
+tcInstTyVar tyvar
   = tcGetUnique 		`thenNF_Tc` \ uniq ->
     let
 	name = setNameUnique (tyVarName tyvar) uniq
@@ -208,6 +209,15 @@ inst_tyvar tyvar	-- Could use the name from the tyvar?
 	returnNF_Tc kind)	`thenNF_Tc` \ kind' ->
 
     tcNewMutTyVar name kind'
+
+tcInstSigVar tyvar	-- Very similar to tcInstTyVar
+  = tcGetUnique 	`thenNF_Tc` \ uniq ->
+    let 
+	name = setNameUnique (tyVarName tyvar) uniq
+	kind = tyVarKind tyvar
+    in
+    ASSERT( not (kind == openTypeKind) )	-- Shouldn't happen
+    tcNewSigTyVar name kind
 \end{code}
 
 @tcInstTcType@ instantiates the outer-level for-alls of a TcType with

ghc/compiler/typecheck/TcUnify.lhs

@@ -25,7 +25,7 @@ import Type	( Type(..), tyVarsOfType, funTyCon,
 import TyCon	( TyCon, isTupleTyCon, isUnboxedTupleTyCon, 
 		  tyConArity )
 import Name	( hasBetterProv )
-import Var	( TyVar, tyVarKind, varName )
+import Var	( TyVar, tyVarKind, varName, isSigTyVar )
 import VarEnv	
 import VarSet	( varSetElems )
 import TcType	( TcType, TcTauType, TcTyVar, TcKind, 
@@ -271,13 +271,17 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
 
 	Nothing -> checkKinds swapped tv1 ty2			`thenTc_`
 
-			-- Try to update sys-y type variables in preference to sig-y ones
-		   if varName tv1 `hasBetterProv` varName tv2 then
-			tcPutTyVar tv2 (TyVarTy tv1)				`thenNF_Tc_`
+		   if tv1 `dominates` tv2 then
+			tcPutTyVar tv2 (TyVarTy tv1)		`thenNF_Tc_`
 			returnTc ()
 		   else
-			tcPutTyVar tv1 ps_ty2					`thenNF_Tc_`
+			tcPutTyVar tv1 ps_ty2			`thenNF_Tc_`
 			returnTc ()
+  where
+    tv1 `dominates` tv2 =  isSigTyVar tv1 
+				-- Don't unify a signature type variable if poss
+			|| varName tv1 `hasBetterProv` varName tv2 
+				-- Try to update sys-y type variables in preference to sig-y ones
 
 	-- Second one isn't a type variable
 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
@@ -286,9 +290,11 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
   = returnTc ()
 
   | otherwise
-  = checkKinds swapped tv1 non_var_ty2		`thenTc_`
-    occur_check non_var_ty2			`thenTc_`
-    tcPutTyVar tv1 ps_ty2			`thenNF_Tc_`
+  = checkKinds swapped tv1 non_var_ty2			`thenTc_`
+    occur_check non_var_ty2				`thenTc_`
+    checkTcM (not (isSigTyVar tv1))
+	     (failWithTcM (unifyWithSigErr tv1 ps_ty2))	`thenTc_`
+    tcPutTyVar tv1 ps_ty2				`thenNF_Tc_`
     returnTc ()
   where
     occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty))	`thenTc_`
@@ -482,6 +488,13 @@ unifyMisMatch ty1 ty2
     in
     failWithTcM (env, msg)
 
+unifyWithSigErr tyvar ty
+  = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
+	      4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
+  where
+    (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
+    (env2, tidy_ty)    = tidyOpenType  env1     ty
+
 unifyOccurCheck tyvar ty
   = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
 	      4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))