[project @ 2005-02-07 13:51:26 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
index 45ab32e..4db7ae3 100644 (file)
@@ -21,7 +21,8 @@ module TcMType (
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstType, 
-  tcSkolTyVar, tcSkolTyVars, tcSkolType,
+  tcSkolType, tcSkolTyVars,
+  tcSkolSigType, tcSkolSigTyVars,
 
   --------------------------------
   -- Checking type validity
@@ -80,6 +81,7 @@ import Name           ( Name, setNameUnique, mkSysTvName )
 import VarSet
 import VarEnv
 import CmdLineOpts     ( dopt, DynFlag(..) )
+import UniqSupply      ( uniqsFromSupply )
 import Util            ( nOfThem, isSingleton, equalLength, notNull )
 import ListSetOps      ( removeDups )
 import SrcLoc          ( unLoc )
@@ -185,49 +187,57 @@ tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- tcInstType instantiates the outer-level for-alls of a TcType with
 -- fresh (mutable) type variables, splits off the dictionary part, 
 -- and returns the pieces.
-tcInstType ty
-  = case tcSplitForAllTys ty of
-       ([],     rho) ->        -- There may be overloading despite no type variables;
-                               --      (?x :: Int) => Int -> Int
-                        let
-                          (theta, tau) = tcSplitPhiTy rho
-                        in
-                        returnM ([], theta, tau)
+tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
 
-       (tyvars, rho) -> tcInstTyVars tyvars            `thenM` \ (tyvars', _, tenv) ->
-                        let
-                          (theta, tau) = tcSplitPhiTy (substTy tenv rho)
-                        in
-                        returnM (tyvars', theta, tau)
 
 ---------------------------------------------
--- Similar functions but for skolem constants
+tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh skolem constants
+tcSkolType info ty = tc_inst_type (tcSkolTyVars info) ty
 
 tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-tcSkolTyVars info tyvars = mappM (tcSkolTyVar info) tyvars
-  
-tcSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-tcSkolTyVar info tyvar
-  = do { uniq <- newUnique
-       ; let name = setNameUnique (tyVarName tyvar) uniq
-               -- See Note [TyVarName]
-       ; return (mkTcTyVar name (tyVarKind tyvar) 
-                           (SkolemTv info)) }
+tcSkolTyVars info tyvars
+  = do { us <- newUniqueSupply
+       ; return (zipWith skol_tv tyvars (uniqsFromSupply us)) }
+  where
+    skol_tv tv uniq = mkTcTyVar (setNameUnique (tyVarName tv) uniq)
+                               (tyVarKind tv) (SkolemTv info)
+       -- See Note [TyVarName]
+                           
 
-tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-tcSkolType info ty
+---------------------------------------------
+tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type signature with skolem constants, but 
+-- do *not* give them fresh names, because we want the name to
+-- be in the type environment -- it is lexically scoped.
+tcSkolSigType info ty
+  = tc_inst_type (\tvs -> return (tcSkolSigTyVars info tvs)) ty
+
+tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
+tcSkolSigTyVars info tyvars = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info) 
+                             | tv <- tyvars ]
+
+-----------------------
+tc_inst_type :: ([TyVar] -> TcM [TcTyVar])             -- How to instantiate the type variables
+            -> TcType                                  -- Type to instantiate
+            -> TcM ([TcTyVar], TcThetaType, TcType)    -- Result
+tc_inst_type inst_tyvars ty
   = case tcSplitForAllTys ty of
-       ([],     rho) -> let
+       ([],     rho) -> let    -- There may be overloading despite no type variables;
+                               --      (?x :: Int) => Int -> Int
                           (theta, tau) = tcSplitPhiTy rho
                         in
-                        returnM ([], theta, tau)
+                        return ([], theta, tau)
 
-       (tyvars, rho) -> tcSkolTyVars info tyvars       `thenM` \ tyvars' ->
-                        let
-                          tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
-                          (theta, tau) = tcSplitPhiTy (substTy tenv rho)
-                        in
-                        returnM (tyvars', theta, tau)
+       (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
+
+                           ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
+                               -- Either the tyvars are freshly made, by inst_tyvars,
+                               -- or (in the call from tcSkolSigType) any nested foralls
+                               -- have different binders.  Either way, zipTopTvSubst is ok
+
+                           ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+                           ; return (tyvars', theta, tau) }
 \end{code}
 
 
@@ -394,7 +404,7 @@ zonkTcPredType (IParam n t)
 \begin{code}
 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
--- It might be a meta TyVar, in which case we freeze it inot ano ordinary TyVar.
+-- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
 -- The meta tyvar is updated to point to the new regular TyVar.  Now any 
 -- bound occurences of the original type variable will get zonked to 
@@ -486,9 +496,6 @@ zonkType unbound_var_fn rflag ty
     go (TyConApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
                                    returnM (TyConApp tycon tys')
 
-    go (NewTcApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
-                                   returnM (NewTcApp tycon tys')
-
     go (NoteTy (SynNote ty1) ty2) = go ty1             `thenM` \ ty1' ->
                                    go ty2              `thenM` \ ty2' ->
                                    returnM (NoteTy (SynNote ty1') ty2')
@@ -525,9 +532,8 @@ zonkTyVar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variabl
           -> Bool                               -- Consult the type refinement?
          -> TcTyVar -> TcM TcType
 zonkTyVar unbound_var_fn rflag tyvar 
-  | not (isTcTyVar tyvar)      -- This can happen when
-                               -- zonking a forall type, when the bound type variable
-                               -- needn't be mutable
+  | not (isTcTyVar tyvar)      -- When zonking (forall a.  ...a...), the occurrences of 
+                               -- the quantified variable a are TyVars not TcTyVars
   = returnM (TyVarTy tyvar)
 
   | otherwise
@@ -765,9 +771,17 @@ check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 -- Rank is allowed rank for function args
 -- No foralls otherwise
 
-check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup (PredTy sty)    = getDOpts         `thenM` \ dflags ->
-                                               check_source_ty dflags TypeCtxt sty
+check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
+check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
+       -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
+
+-- Naked PredTys don't usually show up, but they can as a result of
+--     {-# SPECIALISE instance Ord Char #-}
+-- The Right Thing would be to fix the way that SPECIALISE instance pragmas
+-- are handled, but the quick thing is just to permit PredTys here.
+check_tau_type rank ubx_tup (PredTy sty) = getDOpts            `thenM` \ dflags ->
+                                          check_source_ty dflags TypeCtxt sty
+
 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
   = check_poly_type rank UT_NotOk arg_ty       `thenM_`
@@ -802,9 +816,6 @@ check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
 check_tau_type rank ubx_tup (NoteTy other_note ty)
   = check_tau_type rank ubx_tup ty
 
-check_tau_type rank ubx_tup (NewTcApp tc tys)
-  = mappM_ check_arg_type tys
-
 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   | isSynTyCon tc      
   =    -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
@@ -838,7 +849,7 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
     ubx_tup_msg = ubxArgTyErr ty
 
 ----------------------------------------
-forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
+forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind