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

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

diff --git a/ghc/compiler/basicTypes/Var.lhs b/ghc/compiler/basicTypes/Var.lhs
index e5c820d..0d20b98 100644 (file)
--- a/ghc/compiler/basicTypes/Var.lhs
+++ b/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}
 
 

diff --git a/ghc/compiler/typecheck/TcForeign.lhs b/ghc/compiler/typecheck/TcForeign.lhs
index 3b70db5..a6dee24 100644 (file)
--- a/ghc/compiler/typecheck/TcForeign.lhs
+++ b/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 )

diff --git a/ghc/compiler/typecheck/TcMonad.lhs b/ghc/compiler/typecheck/TcMonad.lhs
index 0e81a32..b2d0497 100644 (file)
--- a/ghc/compiler/typecheck/TcMonad.lhs
+++ b/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
 

diff --git a/ghc/compiler/typecheck/TcMonoType.lhs b/ghc/compiler/typecheck/TcMonoType.lhs
index 93fb0a5..a20c460 100644 (file)
--- a/ghc/compiler/typecheck/TcMonoType.lhs
+++ b/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}

diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index 7305d51..ff0a61e 100644 (file)
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/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

diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs
index f7a78e5..ec1189c 100644 (file)
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/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]))