[project @ 2004-11-11 08:58:23 by simonpj]

[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs

diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index b2c86cc..09bbc26 100644 (file)
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -11,31 +11,33 @@ module TcMType (
 
   --------------------------------
   -- Creating new mutable type variables
 
   --------------------------------
   -- Creating new mutable type variables

-  newTyVar, newSigTyVar,
-  newTyVarTy,          -- Kind -> TcM TcType
-  newTyVarTys,         -- Int -> Kind -> TcM [TcType]
-  newKindVar, newKindVars, newOpenTypeKind,
-  putTcTyVar, getTcTyVar,
-  newMutTyVar, readMutTyVar, writeMutTyVar, 
+  newFlexiTyVar,
+  newTyFlexiVarTy,             -- Kind -> TcM TcType
+  newTyFlexiVarTys,            -- Int -> Kind -> TcM [TcType]
+  newKindVar, newKindVars, 
+  lookupTcTyVar, condLookupTcTyVar, LookupTyVarResult(..),
+  newMetaTyVar, readMetaTyVar, writeMetaTyVar, putMetaTyVar, 

 
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstType, 
 
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstType, 

+  tcSkolTyVar, tcSkolTyVars, tcSkolType,

 
   --------------------------------
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
   checkValidInstHead, instTypeErr, checkAmbiguity,
 
   --------------------------------
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
   checkValidInstHead, instTypeErr, checkAmbiguity,

-  arityErr, 
+  arityErr, isRigidType,

 
   --------------------------------
   -- Zonking
 
   --------------------------------
   -- Zonking

-  zonkType,
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
+  zonkType, zonkTcPredType, 
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,

   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,

-  zonkTcPredType, zonkTcTyVarToTyVar, 
-  zonkTcKindToKind
+  zonkTcKindToKind, zonkTcKind,
+
+  readKindVar, writeKindVar

 
   ) where
 
 
   ) where
 

@@ -43,43 +45,44 @@ module TcMType (
 
 
 -- friends:
 
 
 -- friends:

-import HsSyn           ( HsType )
+import HsSyn           ( LHsType )

 import TypeRep         ( Type(..), PredType(..), TyNote(..),    -- Friend; can see representation
                          Kind, ThetaType
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
 import TypeRep         ( Type(..), PredType(..), TyNote(..),    -- Friend; can see representation
                          Kind, ThetaType
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,

-                         TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
-                         tcEqType, tcCmpPred, isClassPred, mkTyConApp, typeCon,
+                         TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
+                         MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
+                         tcCmpPred, isClassPred, 

                          tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcSplitTyConApp_maybe, tcSplitForAllTys,
                          tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
                          tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcSplitTyConApp_maybe, tcSplitForAllTys,
                          tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,

-                         isUnLiftedType, isIPPred, 
-
+                         isUnLiftedType, isIPPred, isImmutableTyVar,
+                         typeKind, isFlexi, isSkolemTyVar,

                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,

-
-                         liftedTypeKind, defaultKind, superKind,
-                         superBoxity, liftedBoxity, typeKind,

                          tyVarsOfType, tyVarsOfTypes, 
                          tyVarsOfType, tyVarsOfTypes, 

-                         eqKind, isTypeKind, 
+                         pprPred, pprTheta, pprClassPred )
+import Kind            ( Kind(..), KindVar(..), mkKindVar, isSubKind,
+                         isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
+                         liftedTypeKind, defaultKind

                        )
                        )

-import PprType         ( pprThetaArrow )
-import Subst           ( Subst, mkTopTyVarSubst, substTy )
+import Type            ( TvSubst, zipTopTvSubst, substTy )

 import Class           ( Class, classArity, className )
 import TyCon           ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
                          tyConArity, tyConName )
 import Class           ( Class, classArity, className )
 import TyCon           ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
                          tyConArity, tyConName )

-import Var             ( TyVar, tyVarKind, tyVarName, isTyVar, 
-                         mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
+import Var             ( TyVar, tyVarKind, tyVarName, 
+                         mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar )

 
 -- others:
 import TcRnMonad          -- TcType, amongst others
 import FunDeps         ( grow )
 
 -- others:
 import TcRnMonad          -- TcType, amongst others
 import FunDeps         ( grow )

-import PprType         ( pprPred, pprTheta, pprClassPred )
-import Name            ( Name, setNameUnique, mkSystemTvNameEncoded )
+import Name            ( Name, setNameUnique, mkSysTvName )

 import VarSet
 import VarSet

+import VarEnv

 import CmdLineOpts     ( dopt, DynFlag(..) )
 import Util            ( nOfThem, isSingleton, equalLength, notNull )
 import ListSetOps      ( removeDups )
 import CmdLineOpts     ( dopt, DynFlag(..) )
 import Util            ( nOfThem, isSingleton, equalLength, notNull )
 import ListSetOps      ( removeDups )

+import SrcLoc          ( unLoc )

 import Outputable
 \end{code}
 
 import Outputable
 \end{code}
 

@@ -91,53 +94,55 @@ import Outputable
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

-newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
-newMutTyVar name kind details
-  = do { ref <- newMutVar Nothing ;
-        return (mkMutTyVar name kind details ref) }
-
-readMutTyVar :: TyVar -> TcM (Maybe Type)
-readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
+newMetaTyVar :: Name -> Kind -> MetaDetails -> TcM TyVar
+newMetaTyVar name kind details
+  = do { ref <- newMutVar details ;
+        return (mkTcTyVar name kind (MetaTv ref)) }

 
 

-writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
-writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
+readMetaTyVar :: TyVar -> TcM MetaDetails
+readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
+                     readMutVar (metaTvRef tyvar)

 
 

-newTyVar :: Kind -> TcM TcTyVar
-newTyVar kind
-  = newUnique  `thenM` \ uniq ->
-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
+writeMetaTyVar :: TyVar -> MetaDetails -> TcM ()
+writeMetaTyVar tyvar val = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) 
+                          writeMutVar (metaTvRef tyvar) val

 
 

-newSigTyVar :: Kind -> TcM TcTyVar
-newSigTyVar kind
+newFlexiTyVar :: Kind -> TcM TcTyVar
+newFlexiTyVar kind

   = newUnique  `thenM` \ uniq ->
   = newUnique  `thenM` \ uniq ->

-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("s")) kind SigTv
+    newMetaTyVar (mkSysTvName uniq FSLIT("t")) kind Flexi

 
 

-newTyVarTy  :: Kind -> TcM TcType
-newTyVarTy kind
-  = newTyVar kind      `thenM` \ tc_tyvar ->
+newTyFlexiVarTy  :: Kind -> TcM TcType
+newTyFlexiVarTy kind
+  = newFlexiTyVar kind `thenM` \ tc_tyvar ->

     returnM (TyVarTy tc_tyvar)
 
     returnM (TyVarTy tc_tyvar)
 

-newTyVarTys :: Int -> Kind -> TcM [TcType]
-newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
+newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
+newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
+
+isRigidType :: TcType -> TcM Bool
+-- Check that the type is rigid, *taking the type refinement into account*
+-- In other words if a rigid type variable tv is refined to a wobbly type,
+-- the answer should be False
+-- ToDo: can this happen?
+isRigidType ty
+  = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty))
+       ; return (and rigids) }
+  where
+    is_rigid tv = do { details <- lookupTcTyVar tv
+                    ; case details of
+                       RigidTv            -> return True
+                       IndirectTv True ty -> isRigidType ty
+                       other              -> return False
+                    }

 
 newKindVar :: TcM TcKind
 
 newKindVar :: TcM TcKind

-newKindVar
-  = newUnique                                                  `thenM` \ uniq ->
-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv    `thenM` \ kv ->
-    returnM (TyVarTy kv)
+newKindVar = do        { uniq <- newUnique
+               ; ref <- newMutVar Nothing
+               ; return (KindVar (mkKindVar uniq ref)) }

 
 newKindVars :: Int -> TcM [TcKind]
 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 
 newKindVars :: Int -> TcM [TcKind]
 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())

-
-newBoxityVar :: TcM TcKind     -- Really TcBoxity
-  = newUnique                                            `thenM` \ uniq ->
-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) 
-               superBoxity VanillaTv                     `thenM` \ kv ->
-    returnM (TyVarTy kv)
-
-newOpenTypeKind :: TcM TcKind
-newOpenTypeKind = newBoxityVar `thenM` \ bx_var ->
-                 returnM (mkTyConApp typeCon [bx_var])

 \end{code}
 
 
 \end{code}
 
 

@@ -149,38 +154,38 @@ newOpenTypeKind = newBoxityVar    `thenM` \ bx_var ->
 
 Instantiating a bunch of type variables
 
 
 Instantiating a bunch of type variables
 

-\begin{code}
-tcInstTyVars :: TyVarDetails -> [TyVar] 
-            -> TcM ([TcTyVar], [TcType], Subst)
+Note [TyVarName]
+~~~~~~~~~~~~~~~~
+Note that we don't change the print-name
+This won't confuse the type checker but there's a chance
+that two different tyvars will print the same way 
+in an error message.  -dppr-debug will show up the difference
+Better watch out for this.  If worst comes to worst, just
+use mkSystemName.

 
 

-tcInstTyVars tv_details tyvars
-  = mappM (tcInstTyVar tv_details) tyvars      `thenM` \ tc_tyvars ->
-    let
-       tys = mkTyVarTys tc_tyvars
-    in
-    returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
+
+\begin{code}
+-----------------------
+tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
+tcInstTyVars tyvars
+  = do { tc_tvs <- mappM tcInstTyVar tyvars
+       ; let tys = mkTyVarTys tc_tvs
+       ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }

                -- Since the tyvars are freshly made,
                -- they cannot possibly be captured by
                -- Since the tyvars are freshly made,
                -- they cannot possibly be captured by

-               -- any existing for-alls.  Hence mkTopTyVarSubst
-
-tcInstTyVar tv_details tyvar
-  = newUnique          `thenM` \ uniq ->
-    let
-       name = setNameUnique (tyVarName tyvar) uniq
-       -- Note that we don't change the print-name
-       -- This won't confuse the type checker but there's a chance
-       -- that two different tyvars will print the same way 
-       -- in an error message.  -dppr-debug will show up the difference
-       -- Better watch out for this.  If worst comes to worst, just
-       -- use mkSystemName.
-    in
-    newMutTyVar name (tyVarKind tyvar) tv_details
+               -- any existing for-alls.  Hence zipTopTvSubst
+
+tcInstTyVar tyvar
+  = do { uniq <- newUnique
+       ; let name = setNameUnique (tyVarName tyvar) uniq
+               -- See Note [TyVarName]
+       ; newMetaTyVar name (tyVarKind tyvar) Flexi }

 
 

-tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+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 instantiates the outer-level for-alls of a TcType with
 -- fresh (mutable) type variables, splits off the dictionary part, 
 -- and returns the pieces.

-tcInstType tv_details ty
+tcInstType ty

   = case tcSplitForAllTys ty of
        ([],     rho) ->        -- There may be overloading despite no type variables;
                                --      (?x :: Int) => Int -> Int
   = case tcSplitForAllTys ty of
        ([],     rho) ->        -- There may be overloading despite no type variables;
                                --      (?x :: Int) => Int -> Int

@@ -189,11 +194,40 @@ tcInstType tv_details ty
                         in
                         returnM ([], theta, tau)
 
                         in
                         returnM ([], theta, tau)
 

-       (tyvars, rho) -> tcInstTyVars tv_details tyvars         `thenM` \ (tyvars', _, tenv) ->
+       (tyvars, rho) -> tcInstTyVars tyvars            `thenM` \ (tyvars', _, tenv) ->

                         let
                           (theta, tau) = tcSplitPhiTy (substTy tenv rho)
                         in
                         returnM (tyvars', theta, tau)
                         let
                           (theta, tau) = tcSplitPhiTy (substTy tenv rho)
                         in
                         returnM (tyvars', theta, tau)

+
+---------------------------------------------
+-- Similar functions but for skolem constants
+
+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)) }
+
+tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+tcSkolType info ty
+  = case tcSplitForAllTys ty of
+       ([],     rho) -> let
+                          (theta, tau) = tcSplitPhiTy rho
+                        in
+                        returnM ([], 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)

 \end{code}
 
 
 \end{code}
 
 

@@ -204,30 +238,26 @@ tcInstType tv_details ty
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

-putTcTyVar :: TcTyVar -> TcType -> TcM TcType
-getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
-\end{code}
-
-Putting is easy:
-
-\begin{code}
-putTcTyVar tyvar ty 
-  | not (isMutTyVar tyvar)
+putMetaTyVar :: TcTyVar -> TcType -> TcM ()
+#ifndef DEBUG
+putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty)
+#else
+putMetaTyVar tyvar ty
+  | not (isMetaTyVar tyvar)

   = pprTrace "putTcTyVar" (ppr tyvar) $
   = pprTrace "putTcTyVar" (ppr tyvar) $

-    returnM ty
+    returnM ()

 
   | otherwise
 
   | otherwise

-  = ASSERT( isMutTyVar tyvar )
-    writeMutTyVar tyvar (Just ty)      `thenM_`
-    returnM ty
+  = ASSERT( isMetaTyVar tyvar )
+    ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
+    do { ASSERTM( do { details <- readMetaTyVar tyvar; return (isFlexi details) } )
+       ; writeMetaTyVar tyvar (Indirect ty) }
+  where
+    k1 = tyVarKind tyvar
+    k2 = typeKind ty
+#endif

 \end{code}
 
 \end{code}
 

-Getting is more interesting.  The easy thing to do is just to read, thus:
-
-\begin{verbatim}
-getTcTyVar tyvar = readMutTyVar tyvar
-\end{verbatim}
-

 But it's more fun to short out indirections on the way: If this
 version returns a TyVar, then that TyVar is unbound.  If it returns
 any other type, then there might be bound TyVars embedded inside it.
 But it's more fun to short out indirections on the way: If this
 version returns a TyVar, then that TyVar is unbound.  If it returns
 any other type, then there might be bound TyVars embedded inside it.

@@ -235,36 +265,80 @@ any other type, then there might be bound TyVars embedded inside it.
 We return Nothing iff the original box was unbound.
 
 \begin{code}
 We return Nothing iff the original box was unbound.
 
 \begin{code}

+data LookupTyVarResult -- The result of a lookupTcTyVar call
+  = FlexiTv
+  | RigidTv
+  | IndirectTv Bool TcType
+       --      True  => This is a non-wobbly type refinement, 
+       --               gotten from GADT match unification
+       --      False => This is a wobbly type, 
+       --               gotten from inference unification
+
+lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
+-- This function is the ONLY PLACE that we consult the 
+-- type refinement carried by the monad
+--
+-- The boolean returned with Indirect
+lookupTcTyVar tyvar 
+  = case tcTyVarDetails tyvar of
+      SkolemTv _ -> do { type_reft <- getTypeRefinement
+                       ; case lookupVarEnv type_reft tyvar of
+                           Just ty -> return (IndirectTv True ty)
+                           Nothing -> return RigidTv
+                       }
+      MetaTv ref -> do         { details <- readMutVar ref
+                       ; case details of
+                           Indirect ty -> return (IndirectTv False ty)
+                           Flexi       -> return FlexiTv
+                       }
+
+-- Look up a meta type variable, conditionally consulting 
+-- the current type refinement
+condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
+condLookupTcTyVar use_refinement tyvar 
+  | use_refinement = lookupTcTyVar tyvar
+  | otherwise
+  = case tcTyVarDetails tyvar of
+      SkolemTv _ -> return RigidTv
+      MetaTv ref -> do { details <- readMutVar ref
+                       ; case details of
+                           Indirect ty -> return (IndirectTv False ty)
+                           Flexi       -> return FlexiTv
+                       }
+
+{- 
+-- gaw 2004 We aren't shorting anything out anymore, at least for now

 getTcTyVar tyvar
 getTcTyVar tyvar

-  | not (isMutTyVar tyvar)
+  | not (isTcTyVar tyvar)

   = pprTrace "getTcTyVar" (ppr tyvar) $
     returnM (Just (mkTyVarTy tyvar))
 
   | otherwise
   = pprTrace "getTcTyVar" (ppr tyvar) $
     returnM (Just (mkTyVarTy tyvar))
 
   | otherwise

-  = ASSERT2( isMutTyVar tyvar, ppr tyvar )
-    readMutTyVar tyvar                         `thenM` \ maybe_ty ->
+  = ASSERT2( isTcTyVar tyvar, ppr tyvar )
+    readMetaTyVar tyvar                                `thenM` \ maybe_ty ->

     case maybe_ty of
        Just ty -> short_out ty                         `thenM` \ ty' ->
     case maybe_ty of
        Just ty -> short_out ty                         `thenM` \ ty' ->

-                  writeMutTyVar tyvar (Just ty')       `thenM_`
+                  writeMetaTyVar tyvar (Just ty')      `thenM_`

                   returnM (Just ty')
 
        Nothing    -> returnM Nothing
 
 short_out :: TcType -> TcM TcType
 short_out ty@(TyVarTy tyvar)
                   returnM (Just ty')
 
        Nothing    -> returnM Nothing
 
 short_out :: TcType -> TcM TcType
 short_out ty@(TyVarTy tyvar)

-  | not (isMutTyVar tyvar)
+  | not (isTcTyVar tyvar)

   = returnM ty
 
   | otherwise
   = returnM ty
 
   | otherwise

-  = readMutTyVar tyvar `thenM` \ maybe_ty ->
+  = readMetaTyVar tyvar        `thenM` \ maybe_ty ->

     case maybe_ty of
        Just ty' -> short_out ty'                       `thenM` \ ty' ->
     case maybe_ty of
        Just ty' -> short_out ty'                       `thenM` \ ty' ->

-                   writeMutTyVar tyvar (Just ty')      `thenM_`
+                   writeMetaTyVar tyvar (Just ty')     `thenM_`

                    returnM ty'
 
        other    -> returnM ty
 
 short_out other_ty = returnM other_ty
                    returnM ty'
 
        other    -> returnM ty
 
 short_out other_ty = returnM other_ty

+-}

 \end{code}
 
 
 \end{code}
 
 

@@ -285,14 +359,14 @@ zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars       `thenM` \ tys ->
                           returnM (tyVarsOfTypes tys)
 
 zonkTcTyVar :: TcTyVar -> TcM TcType
                           returnM (tyVarsOfTypes tys)
 
 zonkTcTyVar :: TcTyVar -> TcM TcType

-zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
+zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar

 \end{code}
 
 -----------------  Types
 
 \begin{code}
 zonkTcType :: TcType -> TcM TcType
 \end{code}
 
 -----------------  Types
 
 \begin{code}
 zonkTcType :: TcType -> TcM TcType

-zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
+zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty

 
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mappM zonkTcType tys
 
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mappM zonkTcType tys

@@ -318,48 +392,38 @@ zonkTcPredType (IParam n t)
                     are used at the end of type checking
 
 \begin{code}
                     are used at the end of type checking
 
 \begin{code}

-zonkTcKindToKind :: TcKind -> TcM Kind
-zonkTcKindToKind tc_kind 
-  = zonkType zonk_unbound_kind_var tc_kind
-  where
-       -- When zonking a kind, we want to
-       --      zonk a *kind* variable to (Type *)
-       --      zonk a *boxity* variable to *
-    zonk_unbound_kind_var kv 
-       | tyVarKind kv `eqKind` superKind   = putTcTyVar kv liftedTypeKind
-       | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
-       | otherwise                         = pprPanic "zonkKindEnv" (ppr kv)
-                       
--- zonkTcTyVarToTyVar is applied to the *binding* occurrence 
--- of a type variable, at the *end* of type checking.  It changes
--- the *mutable* type variable into an *immutable* one.
--- 
--- It does this by making an immutable version of tv and binds tv to it.
--- Now any bound occurences of the original type variable will get 
--- zonked to the immutable version.
-
-zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
-zonkTcTyVarToTyVar tv
-  = let
-               -- Make an immutable version, defaulting 
-               -- the kind to lifted if necessary
-       immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
-       immut_tv_ty = mkTyVarTy immut_tv
-
-        zap tv = putTcTyVar tv immut_tv_ty
-               -- Bind the mutable version to the immutable one
-    in 
-       -- If the type variable is mutable, then bind it to immut_tv_ty
-       -- so that all other occurrences of the tyvar will get zapped too
-    zonkTyVar zap tv           `thenM` \ ty2 ->
-
-       -- This warning shows up if the allegedly-unbound tyvar is
-       -- already bound to something.  It can actually happen, and 
-       -- in a harmless way (see [Silly Type Synonyms] below) so
-       -- it's only a warning
-    WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
-
-    returnM immut_tv
+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 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 
+-- the immutable version.
+--
+-- We leave skolem TyVars alone; they are imutable.
+zonkQuantifiedTyVar tv
+  | isSkolemTyVar tv = return tv
+       -- It might be a skolem type variable, 
+       -- for example from a user type signature
+
+  | otherwise  -- It's a meta-type-variable
+  = do { details <- readMetaTyVar tv
+
+       -- Create the new, frozen, regular type variable
+       ; let final_kind = defaultKind (tyVarKind tv)
+             final_tv   = mkTyVar (tyVarName tv) final_kind
+
+       -- Bind the meta tyvar to the new tyvar
+       ; case details of
+           Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
+                          return ()
+               -- [Sept 04] I don't think this should happen
+               -- See note [Silly Type Synonym]
+
+           other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv))
+
+       -- Return the new tyvar
+       ; return final_tv }

 \end{code}
 
 [Silly Type Synonyms]
 \end{code}
 
 [Silly Type Synonyms]

@@ -387,10 +451,15 @@ Consider this:
 
 * So we get a dict binding for Num (C d a), which is zonked to give
        a = ()
 
 * So we get a dict binding for Num (C d a), which is zonked to give
        a = ()

+  [Note Sept 04: now that we are zonking quantified type variables
+  on construction, the 'a' will be frozen as a regular tyvar on
+  quantification, so the floated dict will still have type (C d a).
+  Which renders this whole note moot; happily!]

 
 * Then the /\a abstraction has a zonked 'a' in it.
 
 
 * Then the /\a abstraction has a zonked 'a' in it.
 

-All very silly.   I think its harmless to ignore the problem.
+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 ()

 
 
 %************************************************************************
 
 
 %************************************************************************

@@ -402,25 +471,21 @@ All very silly.   I think its harmless to ignore the problem.
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

--- zonkType is used for Kinds as well
-

 -- For unbound, mutable tyvars, zonkType uses the function given to it
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --     type variable and zonks the kind too
 
 zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
                                        -- see zonkTcType, and zonkTcTypeToType
 -- For unbound, mutable tyvars, zonkType uses the function given to it
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --     type variable and zonks the kind too
 
 zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
                                        -- see zonkTcType, and zonkTcTypeToType

-        -> TcType
+        -> Bool                        -- Should we consult the current type refinement?
+         -> TcType

         -> TcM Type
         -> TcM Type

-zonkType unbound_var_fn ty
+zonkType unbound_var_fn rflag ty

   = go ty
   where
     go (TyConApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
                                    returnM (TyConApp tycon tys')
 
   = go ty
   where
     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')
     go (NoteTy (SynNote ty1) ty2) = go ty1             `thenM` \ ty1' ->
                                    go ty2              `thenM` \ ty2' ->
                                    returnM (NoteTy (SynNote ty1') ty2')

@@ -442,11 +507,11 @@ zonkType unbound_var_fn ty
                -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
                -- to pull the TyConApp to the top.
 
        -- The two interesting cases!

-    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
+    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn rflag tyvar

 
 

-    go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar  `thenM` \ tyvar' ->
-                            go ty                      `thenM` \ ty' ->
-                            returnM (ForAllTy tyvar' ty')
+    go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
+                            go ty              `thenM` \ ty' ->
+                            returnM (ForAllTy tyvar ty')

 
     go_pred (ClassP c tys) = mappM go tys      `thenM` \ tys' ->
                             returnM (ClassP c tys')
 
     go_pred (ClassP c tys) = mappM go tys      `thenM` \ tys' ->
                             returnM (ClassP c tys')

@@ -454,25 +519,66 @@ zonkType unbound_var_fn ty
                             returnM (IParam n ty')
 
 zonkTyVar :: (TcTyVar -> TcM Type)             -- What to do for an unbound mutable variable
                             returnM (IParam n ty')
 
 zonkTyVar :: (TcTyVar -> TcM Type)             -- What to do for an unbound mutable variable

-         -> TcTyVar -> TcM TcType
-zonkTyVar unbound_var_fn tyvar 
-  | not (isMutTyVar tyvar)     -- Not a mutable tyvar.  This can happen when
-                               -- zonking a forall type, when the bound type variable
-                               -- needn't be mutable
-  = ASSERT( isTyVar tyvar )            -- Should not be any immutable kind vars
-    returnM (TyVarTy tyvar)
+          -> Bool                               -- Consult the type refinement?
+         -> TcTyVar -> TcM TcType
+zonkTyVar unbound_var_fn rflag tyvar 
+  | not (isTcTyVar tyvar)      -- When zonking (forall a.  ...a...), the occurrences of 
+                               -- the quantified variable a are TyVars not TcTyVars
+  = returnM (TyVarTy tyvar)

 
   | otherwise
 
   | otherwise

-  =  getTcTyVar tyvar  `thenM` \ maybe_ty ->
-     case maybe_ty of
-         Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
-         Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
+  =  condLookupTcTyVar rflag tyvar  `thenM` \ details ->
+     case details of
+          -- If b is true, the variable was refined, and therefore it is okay
+          -- to continue refining inside.  Otherwise it was wobbly and we should
+          -- not refine further inside.
+         IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
+          FlexiTv         -> unbound_var_fn tyvar         -- Unbound flexi
+          RigidTv         -> return (TyVarTy tyvar)       -- Rigid, no zonking necessary

 \end{code}
 
 
 
 %************************************************************************
 %*                                                                     *
 \end{code}
 
 
 
 %************************************************************************
 %*                                                                     *

+                       Zonking kinds
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+readKindVar  :: KindVar -> TcM (Maybe TcKind)
+writeKindVar :: KindVar -> TcKind -> TcM ()
+readKindVar  (KVar _ ref)     = readMutVar ref
+writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
+
+-------------
+zonkTcKind :: TcKind -> TcM TcKind
+zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
+                               ; k2' <- zonkTcKind k2
+                               ; returnM (FunKind k1' k2') }
+zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv 
+                              ; case mb_kind of
+                                   Nothing -> returnM k
+                                   Just k  -> zonkTcKind k }
+zonkTcKind other_kind = returnM other_kind
+
+-------------
+zonkTcKindToKind :: TcKind -> TcM Kind
+zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
+                                     ; k2' <- zonkTcKindToKind k2
+                                     ; returnM (FunKind k1' k2') }
+
+zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv 
+                                  ; case mb_kind of
+                                      Nothing -> return liftedTypeKind
+                                      Just k  -> zonkTcKindToKind k }
+
+zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
+zonkTcKindToKind other_kind   = returnM other_kind
+\end{code}
+                       
+%************************************************************************
+%*                                                                     *

 \subsection{Checking a user type}
 %*                                                                     *
 %************************************************************************
 \subsection{Checking a user type}
 %*                                                                     *
 %************************************************************************

@@ -532,8 +638,8 @@ data UserTypeCtxt
 -- With gla-exts that's right, but for H98 we should complain. 
 
 
 -- With gla-exts that's right, but for H98 we should complain. 
 
 

-pprHsSigCtxt :: UserTypeCtxt -> HsType Name -> SDoc
-pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt hs_ty ctxt
+pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
+pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt

 
 pprUserTypeCtxt ty (FunSigCtxt n)  = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
 pprUserTypeCtxt ty ExprSigCtxt     = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
 
 pprUserTypeCtxt ty (FunSigCtxt n)  = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
 pprUserTypeCtxt ty ExprSigCtxt     = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]

@@ -574,17 +680,18 @@ checkValidType ctxt ty
 
        actual_kind = typeKind ty
 
 
        actual_kind = typeKind ty
 

-       actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
-

        kind_ok = case ctxt of
                        TySynCtxt _  -> True    -- Any kind will do
        kind_ok = case ctxt of
                        TySynCtxt _  -> True    -- Any kind will do

-                       GenPatCtxt   -> actual_kind_is_lifted
-                       ForSigCtxt _ -> actual_kind_is_lifted
-                       other        -> isTypeKind actual_kind
+                       ResSigCtxt   -> isOpenTypeKind   actual_kind
+                       ExprSigCtxt  -> isOpenTypeKind   actual_kind
+                       GenPatCtxt   -> isLiftedTypeKind actual_kind
+                       ForSigCtxt _ -> isLiftedTypeKind actual_kind
+                       other        -> isArgTypeKind       actual_kind

        
        ubx_tup | not gla_exts = UT_NotOk
                | otherwise    = case ctxt of
                                   TySynCtxt _ -> UT_Ok
        
        ubx_tup | not gla_exts = UT_NotOk
                | otherwise    = case ctxt of
                                   TySynCtxt _ -> UT_Ok

+                                  ExprSigCtxt -> UT_Ok

                                   other       -> UT_NotOk
                -- Unboxed tuples ok in function results,
                -- but for type synonyms we allow them even at
                                   other       -> UT_NotOk
                -- Unboxed tuples ok in function results,
                -- but for type synonyms we allow them even at

@@ -654,9 +761,17 @@ check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 -- Rank is allowed rank for function args
 -- No foralls otherwise
 
 -- 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_`
 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_`

@@ -691,9 +806,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 (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
 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   | isSynTyCon tc      
   =    -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated

@@ -706,8 +818,8 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg  `thenM_`
     mappM_ (check_tau_type (Rank 0) UT_Ok) tys 
   = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
     checkTc (ubx_tup_ok gla_exts) ubx_tup_msg  `thenM_`
     mappM_ (check_tau_type (Rank 0) UT_Ok) tys 

-                       -- Args are allowed to be unlifted, or
-                       -- more unboxed tuples, so can't use check_arg_ty
+               -- Args are allowed to be unlifted, or
+               -- more unboxed tuples, so can't use check_arg_ty

 
   | otherwise
   = mappM_ check_arg_type tys
 
   | otherwise
   = mappM_ check_arg_type tys

@@ -727,7 +839,7 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
     ubx_tup_msg = ubxArgTyErr ty
 
 ----------------------------------------
     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
 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