[project @ 2000-10-03 08:43:00 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index 95a5bdd..6a4680f 100644 (file)
@@ -12,9 +12,6 @@ module TcType (
   newTyVarTy,          -- Kind -> NF_TcM s TcType
   newTyVarTys,         -- Int -> Kind -> NF_TcM s [TcType]
 
-  newTyVarTy_OpenKind, -- NF_TcM s TcType
-  newOpenTypeKind,     -- NF_TcM s TcKind
-
   -----------------------------------------
   TcType, TcTauType, TcThetaType, TcRhoType,
 
@@ -29,21 +26,15 @@ module TcType (
   tcInstSigVar,
   tcInstTcType,
 
-  typeToTcType,
-
-  tcTypeKind,          -- :: TcType -> NF_TcM s TcKind
   --------------------------------
   TcKind,
-  newKindVar, newKindVars,
-  kindToTcKind,
-  zonkTcKind,
+  newKindVar, newKindVars, newBoxityVar,
 
   --------------------------------
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarBndr,
-  zonkTcType, zonkTcTypes, zonkTcThetaType,
+  zonkTcTyVar, zonkTcTyVars, zonkTcSigTyVars,
+  zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
 
-  zonkTcTypeToType, zonkTcTyVarToTyVar,
-  zonkTcKindToKind
+  zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv
 
   ) where
 
@@ -51,27 +42,25 @@ module TcType (
 
 
 -- friends:
-import PprType         ( pprType )
-import TypeRep         ( Type(..), Kind, TyNote(..), 
-                         typeCon, openTypeKind, boxedTypeKind, boxedKind, superKind, superBoxity
-                       )  -- friend
-import Type            ( ThetaType,
-                         mkAppTy, mkTyConApp,
-                         splitDictTy_maybe, splitForAllTys, isNotUsgTy,
+import TypeRep         ( Type(..), Kind, TyNote(..) )  -- friend
+import Type            ( ThetaType, PredType(..),
+                         getTyVar, mkAppTy, mkTyConApp, mkPredTy,
+                         splitPredTy_maybe, splitForAllTys, isNotUsgTy,
                          isTyVarTy, mkTyVarTy, mkTyVarTys, 
+                         openTypeKind, boxedTypeKind, 
+                         superKind, superBoxity, 
+                         defaultKind, boxedBoxity
                        )
 import Subst           ( Subst, mkTopTyVarSubst, substTy )
 import TyCon           ( tyConKind, mkPrimTyCon )
 import PrimRep         ( PrimRep(VoidRep) )
-import VarEnv
-import VarSet          ( emptyVarSet )
 import Var             ( TyVar, tyVarKind, tyVarName, isTyVar, isMutTyVar, mkTyVar )
 
 -- others:
-import TcMonad
+import TcMonad          -- TcType, amongst others
 import TysWiredIn      ( voidTy )
 
-import Name            ( NamedThing(..), setNameUnique, mkSysLocalName,
+import Name            ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
                          mkDerivedName, mkDerivedTyConOcc
                        )
 import Unique          ( Unique, Uniquable(..) )
@@ -80,19 +69,6 @@ import Outputable
 \end{code}
 
 
-
-Coercions
-~~~~~~~~~~
-Type definitions are in TcMonad.lhs
-
-\begin{code}
-typeToTcType :: Type -> TcType
-typeToTcType ty =  ty
-
-kindToTcKind :: Kind -> TcKind
-kindToTcKind kind = kind
-\end{code}
-
 Utility functions
 ~~~~~~~~~~~~~~~~~
 These tcSplit functions are like their non-Tc analogues, but they
@@ -108,7 +84,7 @@ tcSplitRhoTy t
  where
        -- A type variable is never instantiated to a dictionary type,
        -- so we don't need to do a tcReadVar on the "arg".
-    go syn_t (FunTy arg res) ts = case splitDictTy_maybe arg of
+    go syn_t (FunTy arg res) ts = case splitPredTy_maybe arg of
                                        Just pair -> go res res (pair:ts)
                                        Nothing   -> returnNF_Tc (reverse ts, syn_t)
     go syn_t (NoteTy _ t)    ts = go syn_t t ts
@@ -149,16 +125,11 @@ newKindVar
 newKindVars :: Int -> NF_TcM s [TcKind]
 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 
--- Returns a type variable of kind (Type bv) where bv is a new boxity var
--- Used when you need a type variable that's definitely a , but you don't know
--- what kind of type (boxed or unboxed).
-newTyVarTy_OpenKind :: NF_TcM s TcType
-newTyVarTy_OpenKind = newOpenTypeKind  `thenNF_Tc` \ kind -> 
-                     newTyVarTy kind
-
-newOpenTypeKind :: NF_TcM s TcKind
-newOpenTypeKind = newTyVarTy superBoxity       `thenNF_Tc` \ bv ->
-                 returnNF_Tc (mkTyConApp typeCon [bv])
+newBoxityVar :: NF_TcM s TcKind
+newBoxityVar
+  = tcGetUnique                                                `thenNF_Tc` \ uniq ->
+    tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
+    returnNF_Tc (TyVarTy kv)
 \end{code}
 
 
@@ -194,26 +165,8 @@ tcInstTyVar tyvar
        -- in an error message.  -dppr-debug will show up the difference
        -- Better watch out for this.  If worst comes to worst, just
        -- use mkSysLocalName.
-
-       kind = tyVarKind tyvar
     in
-
-       -- Hack alert!  Certain system functions (like error) are quantified
-       -- over type variables with an 'open' kind (a :: ?).  When we instantiate
-       -- these tyvars we want to make a type variable whose kind is (Type bv)
-       -- where bv is a boxity variable.  This makes sure it's a type, but 
-       -- is open about its boxity.  We *don't* want to give the thing the
-       -- kind '?' (= Type AnyBox).  
-       --
-       -- This is all a hack to avoid giving error it's "proper" type:
-       --       error :: forall bv. forall a::Type bv. String -> a
-
-    (if kind == openTypeKind then
-       newOpenTypeKind 
-     else
-       returnNF_Tc kind)       `thenNF_Tc` \ kind' ->
-
-    tcNewMutTyVar name kind'
+    tcNewMutTyVar name (tyVarKind tyvar)
 
 tcInstSigVar tyvar     -- Very similar to tcInstTyVar
   = tcGetUnique        `thenNF_Tc` \ uniq ->
@@ -310,13 +263,16 @@ short_out other_ty = returnNF_Tc other_ty
 zonkTcTyVars :: [TcTyVar] -> NF_TcM s [TcType]
 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 
-zonkTcTyVarBndr :: TcTyVar -> NF_TcM s TcTyVar
-zonkTcTyVarBndr tyvar
-  = zonkTcTyVar tyvar  `thenNF_Tc` \ (TyVarTy tyvar') ->
-    returnNF_Tc tyvar'
-       
 zonkTcTyVar :: TcTyVar -> NF_TcM s TcType
 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
+
+zonkTcSigTyVars :: [TcTyVar] -> NF_TcM s [TcTyVar]
+-- This guy is to zonk the tyvars we're about to feed into tcSimplify
+-- Usually this job is done by checkSigTyVars, but in a couple of places
+-- that is overkill, so we use this simpler chap
+zonkTcSigTyVars tyvars
+  = zonkTcTyVars tyvars        `thenNF_Tc` \ tys ->
+    returnNF_Tc (map (getTyVar "zonkTcSigTyVars") tys)
 \end{code}
 
 -----------------  Types
@@ -328,47 +284,55 @@ zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 zonkTcTypes :: [TcType] -> NF_TcM s [TcType]
 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 
-zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
-zonkTcThetaType theta = mapNF_Tc zonk theta
-                   where
-                       zonk (c,ts) = zonkTcTypes ts    `thenNF_Tc` \ new_ts ->
-                                     returnNF_Tc (c, new_ts)
+zonkTcClassConstraints cts = mapNF_Tc zonk cts
+    where zonk (clas, tys)
+           = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
+             returnNF_Tc (clas, new_tys)
 
-zonkTcKind :: TcKind -> NF_TcM s TcKind
-zonkTcKind = zonkTcType
+zonkTcThetaType :: TcThetaType -> NF_TcM s TcThetaType
+zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
+
+zonkTcPredType :: TcPredType -> NF_TcM s TcPredType
+zonkTcPredType (Class c ts) =
+    zonkTcTypes ts     `thenNF_Tc` \ new_ts ->
+    returnNF_Tc (Class c new_ts)
+zonkTcPredType (IParam n t) =
+    zonkTcType t       `thenNF_Tc` \ new_t ->
+    returnNF_Tc (IParam n new_t)
 \end{code}
 
 -------------------  These ...ToType, ...ToKind versions
                     are used at the end of type checking
 
 \begin{code}
-zonkTcKindToKind :: TcKind -> NF_TcM s Kind
-zonkTcKindToKind kind = zonkType zonk_unbound_kind_var kind
-  where
-       -- Zonk a mutable but unbound kind variable to
-       --      (Type Boxed)    if it has kind superKind
-       --      Boxed           if it has kind superBoxity
-    zonk_unbound_kind_var kv
-       | super_kind == superKind = tcPutTyVar kv boxedTypeKind
-       | otherwise               = ASSERT( super_kind == superBoxity )
-                                   tcPutTyVar kv boxedKind
-       where
-         super_kind = tyVarKind kv
+zonkKindEnv :: [(Name, TcKind)] -> NF_TcM s [(Name, Kind)]
+zonkKindEnv pairs 
+  = mapNF_Tc zonk_it pairs
+ where
+    zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
+                             returnNF_Tc (name, kind)
+
+       -- 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 == superKind   = tcPutTyVar kv boxedTypeKind
+                            | tyVarKind kv == superBoxity = tcPutTyVar kv boxedBoxity
+                            | otherwise                   = pprPanic "zonkKindEnv" (ppr kv)
                        
-
 zonkTcTypeToType :: TcType -> NF_TcM s Type
 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
   where
        -- Zonk a mutable but unbound type variable to
-       --      Void            if it has kind (Type Boxed)
-       --      Voidxxx         otherwise
+       --      Void            if it has kind Boxed
+       --      :Void           otherwise
     zonk_unbound_tyvar tv
-       = zonkTcKindToKind (tyVarKind tv)       `thenNF_Tc` \ kind ->
-         if kind == boxedTypeKind then
-               tcPutTyVar tv voidTy    -- Just to avoid creating a new tycon in
-                                       -- this vastly common case
-         else
-               tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
+       | kind == boxedTypeKind
+       = tcPutTyVar tv voidTy  -- Just to avoid creating a new tycon in
+                               -- this vastly common case
+       | otherwise
+       = tcPutTyVar tv (TyConApp (mk_void_tycon tv kind) [])
+       where
+         kind = tyVarKind tv
 
     mk_void_tycon tv kind      -- Make a new TyCon with the same kind as the 
                                -- type variable tv.  Same name too, apart from
@@ -378,18 +342,19 @@ zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
          tc_name = mkDerivedName mkDerivedTyConOcc (getName tv) (getUnique tv)
 
 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence 
--- of a type variable, at the *end* of type checking.
--- It zonks the type variable, to get a mutable, but unbound, tyvar, tv;
--- zonks its kind, and then makes an immutable version of tv and binds tv to it.
+-- 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 -> NF_TcM s TyVar
 zonkTcTyVarToTyVar tv
-  = zonkTcKindToKind (tyVarKind tv)    `thenNF_Tc` \ kind ->
-    let
-               -- Make an immutable version
-       immut_tv    = mkTyVar (tyVarName tv) kind
+  = let
+               -- Make an immutable version, defaulting 
+               -- the kind to boxed if necessary
+       immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
        immut_tv_ty = mkTyVarTy immut_tv
 
         zap tv = tcPutTyVar tv immut_tv_ty
@@ -398,7 +363,8 @@ zonkTcTyVarToTyVar tv
        -- 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           `thenNF_Tc` \ ty2 ->
-    ASSERT2( immut_tv_ty == ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
+
+    WARN( immut_tv_ty /= ty2, ppr tv $$ ppr immut_tv $$ ppr ty2 )
 
     returnNF_Tc immut_tv
 \end{code}
@@ -441,6 +407,9 @@ zonkType unbound_var_fn ty
     go (NoteTy (UsgForAll uv) ty2)= go ty2             `thenNF_Tc` \ ty2' ->
                                    returnNF_Tc (NoteTy (UsgForAll uv) ty2')
 
+    go (PredTy p)                = go_pred p           `thenNF_Tc` \ p' ->
+                                   returnNF_Tc (PredTy p')
+
     go (FunTy arg res)           = go arg              `thenNF_Tc` \ arg' ->
                                    go res              `thenNF_Tc` \ res' ->
                                    returnNF_Tc (FunTy arg' res')
@@ -450,13 +419,16 @@ zonkType unbound_var_fn ty
                                    returnNF_Tc (mkAppTy fun' arg')
 
        -- The two interesting cases!
-    go (TyVarTy tyvar)           = zonkTyVar unbound_var_fn tyvar
+    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 
-    go (ForAllTy tyvar ty)
-       = zonkTcTyVarToTyVar tyvar      `thenNF_Tc` \ tyvar' ->
-         go ty                         `thenNF_Tc` \ ty' ->
-         returnNF_Tc (ForAllTy tyvar' ty')
+    go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar  `thenNF_Tc` \ tyvar' ->
+                            go ty                      `thenNF_Tc` \ ty' ->
+                            returnNF_Tc (ForAllTy tyvar' ty')
 
+    go_pred (Class c tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
+                           returnNF_Tc (Class c tys')
+    go_pred (IParam n ty) = go ty              `thenNF_Tc` \ ty' ->
+                           returnNF_Tc (IParam n ty')
 
 zonkTyVar :: (TcTyVar -> NF_TcM s Type)                -- What to do for an unbound mutable variable
          -> TcTyVar -> NF_TcM s TcType
@@ -475,49 +447,3 @@ zonkTyVar unbound_var_fn tyvar
                            zonkType unbound_var_fn other_ty    -- Bound
 \end{code}
 
-%************************************************************************
-%*                                                                     *
-\subsection{tcTypeKind}
-%*                                                                     *
-%************************************************************************
-
-Sadly, we need a Tc version of typeKind, that looks though mutable
-kind variables.  See the notes with Type.typeKind for the typeKindF nonsense
-
-This is pretty gruesome.
-
-\begin{code}
-tcTypeKind :: TcType -> NF_TcM s TcKind
-
-tcTypeKind (TyVarTy tyvar)     = returnNF_Tc (tyVarKind tyvar)
-tcTypeKind (TyConApp tycon tys)        = foldlTc (\k _ -> tcFunResultTy k) (tyConKind tycon) tys
-tcTypeKind (NoteTy _ ty)       = tcTypeKind ty
-tcTypeKind (AppTy fun arg)     = tcTypeKind fun        `thenNF_Tc` \ fun_kind ->
-                                 tcFunResultTy fun_kind
-tcTypeKind (FunTy fun arg)     = tcTypeKindF arg
-tcTypeKind (ForAllTy _ ty)     = tcTypeKindF ty
-
-tcTypeKindF :: TcType -> NF_TcM s TcKind
-tcTypeKindF (NoteTy _ ty)   = tcTypeKindF ty
-tcTypeKindF (FunTy _ ty)    = tcTypeKindF ty
-tcTypeKindF (ForAllTy _ ty) = tcTypeKindF ty
-tcTypeKindF other          = tcTypeKind other  `thenNF_Tc` \ kind ->
-                             fix_up kind
-  where
-    fix_up (TyConApp kc _) | kc == typeCon = returnNF_Tc boxedTypeKind
-               -- Functions at the type level are always boxed
-    fix_up (NoteTy _ kind)   = fix_up kind
-    fix_up kind@(TyVarTy tv) = tcGetTyVar tv   `thenNF_Tc` \ maybe_ty ->
-                              case maybe_ty of
-                                 Just kind' -> fix_up kind'
-                                 Nothing  -> returnNF_Tc kind
-    fix_up kind              = returnNF_Tc kind
-
-tcFunResultTy (NoteTy _ ty)   = tcFunResultTy ty
-tcFunResultTy (FunTy arg res) = returnNF_Tc res
-tcFunResultTy (TyVarTy tv)    = tcGetTyVar tv  `thenNF_Tc` \ maybe_ty ->
-                               case maybe_ty of
-                                 Just ty' -> tcFunResultTy ty'
-       -- The Nothing case, and the other cases for tcFunResultTy
-       -- should never happen... pattern match failure
-\end{code}