[project @ 2004-04-02 12:38:33 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index ffcf392..0e430f4 100644 (file)
@@ -22,7 +22,7 @@ module TcType (
 
   --------------------------------
   -- TyVarDetails
-  TyVarDetails(..), isUserTyVar, isSkolemTyVar, 
+  TyVarDetails(..), isUserTyVar, isSkolemTyVar, isExistentialTyVar,
   tyVarBindingInfo,
 
   --------------------------------
@@ -73,6 +73,7 @@ module TcType (
   isFFILabelTy,        -- :: Type -> Bool
   isFFIDotnetTy,       -- :: DynFlags -> Type -> Bool
   isFFIDotnetObjTy,    -- :: Type -> Bool
+  isFFITy,            -- :: Type -> Bool
   
   toDNType,            -- :: Type -> DNType
 
@@ -86,8 +87,7 @@ module TcType (
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, 
   isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, 
-  isSubKind, defaultKind, 
-  isArgTypeKind, isOpenTypeKind, 
+  isArgTypeKind, isSubKind, defaultKind, 
 
   Type, PredType(..), ThetaType, 
   mkForAllTy, mkForAllTys, 
@@ -248,6 +248,14 @@ data TyVarDetails
    | PatSigTv  -- Scoped type variable, introduced by a pattern
                -- type signature       \ x::a -> e
 
+   | ExistTv   -- An existential type variable bound by a pattern for
+               -- a data constructor with an existential type. E.g.
+               --      data T = forall a. Eq a => MkT a
+               --      f (MkT x) = ...
+               -- The pattern MkT x will allocate an existential type
+               -- variable for 'a'.  We distinguish these from all others
+               -- on one place, namely InstEnv.lookupInstEnv.
+
    | VanillaTv -- Everything else
 
 isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
@@ -257,10 +265,16 @@ isUserTyVar tv = case tcTyVarDetails tv of
 
 isSkolemTyVar :: TcTyVar -> Bool
 isSkolemTyVar tv = case tcTyVarDetails tv of
-                     SigTv  -> True
-                     ClsTv  -> True
-                     InstTv -> True
-                     oteher -> False
+                     SigTv   -> True
+                     ClsTv   -> True
+                     InstTv  -> True
+                     ExistTv -> True
+                     other   -> False
+
+isExistentialTyVar :: TcTyVar -> Bool
+isExistentialTyVar tv = case tcTyVarDetails tv of
+                             ExistTv -> True
+                             other   -> False
 
 tyVarBindingInfo :: TcTyVar -> SDoc    -- Used in checkSigTyVars
 tyVarBindingInfo tv
@@ -271,6 +285,7 @@ tyVarBindingInfo tv
     details ClsTv     = ptext SLIT("class declaration")
     details InstTv    = ptext SLIT("instance declaration")
     details PatSigTv  = ptext SLIT("pattern type signature")
+    details ExistTv   = ptext SLIT("existential constructor")
     details VanillaTv = ptext SLIT("//vanilla//")      -- Ditto
 \end{code}
 
@@ -771,6 +786,10 @@ restricted set of types as arguments and results (the restricting factor
 being the )
 
 \begin{code}
+isFFITy :: Type -> Bool
+-- True for any TyCon that can possibly be an arg or result of an FFI call
+isFFITy ty = checkRepTyCon legalFFITyCon ty
+
 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
 -- Checks for valid argument type for a 'foreign import'
 isFFIArgumentTy dflags safety ty 
@@ -862,7 +881,9 @@ toDNType ty
 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
        -- Look through newtypes
        -- Non-recursive ones are transparent to splitTyConApp,
-       -- but recursive ones aren't
+       -- but recursive ones aren't.  Manuel had:
+       --      newtype T = MkT (Ptr T)
+       -- and wanted it to work...
 checkRepTyCon check_tc ty 
   | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc
   | otherwise                                      = False
@@ -910,6 +931,11 @@ legalOutgoingTyCon dflags safety tc
   | otherwise
   = marshalableTyCon dflags tc
 
+legalFFITyCon :: TyCon -> Bool
+-- True for any TyCon that can possibly be an arg or result of an FFI call
+legalFFITyCon tc
+  = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
+
 marshalableTyCon dflags tc
   =  (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
   || boxedMarshalableTyCon tc
@@ -1112,7 +1138,7 @@ match (TyVarTy v) ty tmpls k senv
   | v `elemVarSet` tmpls
   =     -- v is a template variable
     case lookupSubstEnv senv v of
-       Nothing | typeKind ty == tyVarKind v    
+       Nothing | typeKind ty `isSubKind` 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
@@ -1147,12 +1173,14 @@ match (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) tmpls k senv
 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
   = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
 
+       -- If the template is an application, try to make the 
+       -- thing we are matching look like an application
 match (AppTy fun1 arg1) ty2 tmpls k senv 
   = case tcSplitAppTy_maybe ty2 of
        Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
        Nothing          -> Nothing     -- Fail
 
--- Newtypes are opaque; predicate types should not happen
+       -- Newtypes are opaque; predicate types should not happen
 match (NewTcApp tc1 tys1) (NewTcApp tc2 tys2) tmpls k senv
   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv