[project @ 2002-03-12 15:55:26 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index 5db0ad7..8286f64 100644 (file)
@@ -46,6 +46,7 @@ module TcType (
   isDoubleTy, isFloatTy, isIntTy,
   isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy, 
   isTauTy, tcIsTyVarTy, tcIsForAllTy,
+  allDistinctTyVars,
 
   ---------------------------------
   -- Misc type manipulators
@@ -59,7 +60,7 @@ module TcType (
   isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
   mkDictTy, tcSplitPredTy_maybe, predTyUnique,
   isDictTy, tcSplitDFunTy, predTyUnique, 
-  mkClassPred, inheritablePred, isIPPred, mkPredName, 
+  mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
 
   ---------------------------------
   -- Foreign import and export
@@ -74,7 +75,6 @@ module TcType (
   ---------------------------------
   -- Unifier and matcher  
   unifyTysX, unifyTyListsX, unifyExtendTysX,
-  allDistinctTyVars,
   matchTy, matchTys, match,
 
   --------------------------------
@@ -82,12 +82,12 @@ module TcType (
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 
   superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
-  isTypeKind,
+  isTypeKind, isAnyTypeKind,
 
   Type, SourceType(..), PredType, ThetaType, 
   mkForAllTy, mkForAllTys, 
   mkFunTy, mkFunTys, zipFunTys, 
-  mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+  mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys, 
 
   isUnLiftedType,      -- Source types are always lifted
@@ -113,9 +113,9 @@ import Type         (       -- Re-exports
                          tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
                          Kind, Type, SourceType(..), PredType, ThetaType, 
                          unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
-                         mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
+                         mkForAllTy, mkForAllTys, defaultKind, isTypeKind, isAnyTypeKind,
                          mkFunTy, mkFunTys, zipFunTys, 
-                         mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+                         mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
                          mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
                          isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
                          splitNewType_maybe, splitTyConApp_maybe,
@@ -137,7 +137,7 @@ import OccName              ( OccName, mkDictOcc )
 import NameSet
 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
 import TysWiredIn      ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
-import BasicTypes      ( ipNameName )
+import BasicTypes      ( IPName(..), ipNameName )
 import Unique          ( Unique, Uniquable(..) )
 import SrcLoc          ( SrcLoc )
 import Util            ( cmpList, thenCmp, equalLength )
@@ -250,7 +250,9 @@ isUserTyVar tv = case mutTyVarDetails tv of
 
 isSkolemTyVar :: TcTyVar -> Bool
 isSkolemTyVar tv = case mutTyVarDetails tv of
-                     SigTv -> True
+                     SigTv  -> True
+                     ClsTv  -> True
+                     InstTv -> True
                      oteher -> False
 
 isHoleTyVar :: TcTyVar -> Bool
@@ -371,11 +373,11 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
                        Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 
 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
--- Newtypes are opaque, so they may be split
 tcSplitTyConApp_maybe (TyConApp tc tys)        = Just (tc, tys)
 tcSplitTyConApp_maybe (FunTy arg res)          = Just (funTyCon, [arg,res])
 tcSplitTyConApp_maybe (NoteTy n ty)            = tcSplitTyConApp_maybe ty
 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
+       -- Newtypes are opaque, so they may be split
        -- However, predicates are not treated
        -- as tycon applications by the type checker
 tcSplitTyConApp_maybe other                    = Nothing
@@ -453,6 +455,31 @@ tcSplitDFunTy ty
     (tvs, theta, clas, tys) }}
 \end{code}
 
+(allDistinctTyVars tys tvs) = True 
+       iff 
+all the types tys are type variables, 
+distinct from each other and from tvs.
+
+This is useful when checking that unification hasn't unified signature
+type variables.  For example, if the type sig is
+       f :: forall a b. a -> b -> b
+we want to check that 'a' and 'b' havn't 
+       (a) been unified with a non-tyvar type
+       (b) been unified with each other (all distinct)
+       (c) been unified with a variable free in the environment
+
+\begin{code}
+allDistinctTyVars :: [Type] -> TyVarSet -> Bool
+
+allDistinctTyVars []       acc
+  = True
+allDistinctTyVars (ty:tys) acc 
+  = case tcGetTyVar_maybe ty of
+       Nothing                       -> False  -- (a)
+       Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
+               | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
+\end{code}    
+
 
 %************************************************************************
 %*                                                                     *
@@ -530,7 +557,7 @@ isIPPred :: SourceType -> Bool
 isIPPred (IParam _ _) = True
 isIPPred other       = False
 
-inheritablePred :: PredType -> Bool
+isInheritablePred :: PredType -> Bool
 -- Can be inherited by a context.  For example, consider
 --     f x = let g y = (?v, y+x)
 --           in (g 3 with ?v = 8, 
@@ -539,8 +566,12 @@ inheritablePred :: PredType -> Bool
 --     g :: (?v :: a) => a -> a
 -- but it doesn't need to be quantified over the Num a dictionary
 -- which can be free in g's rhs, and shared by both calls to g
-inheritablePred (ClassP _ _) = True
-inheritablePred other       = False
+isInheritablePred (ClassP _ _) = True
+isInheritablePred other             = False
+
+isLinearPred :: TcPredType -> Bool
+isLinearPred (IParam (Linear n) _) = True
+isLinearPred other                = False
 \end{code}
 
 
@@ -882,38 +913,6 @@ boxedMarshalableTyCon tc
 %*                                                                     *
 %************************************************************************
 
-(allDistinctTyVars tys tvs) = True 
-       iff 
-all the types tys are type variables, 
-distinct from each other and from tvs.
-
-This is useful when checking that unification hasn't unified signature
-type variables.  For example, if the type sig is
-       f :: forall a b. a -> b -> b
-we want to check that 'a' and 'b' havn't 
-       (a) been unified with a non-tyvar type
-       (b) been unified with each other (all distinct)
-       (c) been unified with a variable free in the environment
-
-\begin{code}
-allDistinctTyVars :: [Type] -> TyVarSet -> Bool
-
-allDistinctTyVars []       acc
-  = True
-allDistinctTyVars (ty:tys) acc 
-  = case tcGetTyVar_maybe ty of
-       Nothing                       -> False  -- (a)
-       Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
-               | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
-\end{code}    
-
-
-%************************************************************************
-%*                                                                     *
-\subsection{Unification with an explicit substitution}
-%*                                                                     *
-%************************************************************************
-
 Unify types with an explicit substitution and no monad.
 Ignore usage annotations.
 
@@ -1087,7 +1086,15 @@ match (TyVarTy v) ty tmpls k senv
   | v `elemVarSet` tmpls
   =     -- v is a template variable
     case lookupSubstEnv senv v of
-       Nothing -> k (extendSubstEnv senv v (DoneTy ty))
+       Nothing | typeKind ty `eqKind` tyVarKind v      
+                       -- We do a kind check, just as in the uVarX above
+                       -- The kind check is needed to avoid bogus matches
+                       -- of   (a b) with (c d), where the kinds don't match
+                       -- An occur check isn't needed when matching.
+               -> k (extendSubstEnv senv v (DoneTy ty))
+
+               | otherwise  -> Nothing -- Fails
+
        Just (DoneTy ty')  | ty' `tcEqType` ty   -> k senv   -- Succeeds
                           | otherwise           -> Nothing  -- Fails