[project @ 2005-02-25 13:06:31 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index 379b370..ce31dd5 100644 (file)
@@ -22,14 +22,14 @@ module TcType (
 
   --------------------------------
   -- MetaDetails
-  TcTyVarDetails(..),
+  Expected(..), TcRef, TcTyVarDetails(..),
   MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar,
   isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef,
   isFlexi, isIndirect,
 
   --------------------------------
   -- Builders
-  mkPhiTy, mkSigmaTy, 
+  mkPhiTy, mkSigmaTy, hoistForAllTys,
 
   --------------------------------
   -- Splitters  
@@ -38,12 +38,12 @@ module TcType (
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
-  tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
+  tcGetTyVar_maybe, tcGetTyVar,
 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
-  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
+  tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
   isSigmaTy, isOverloadedTy, 
   isDoubleTy, isFloatTy, isIntTy,
   isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
@@ -60,7 +60,7 @@ module TcType (
   getClassPredTys_maybe, getClassPredTys, 
   isClassPred, isTyVarClassPred, 
   mkDictTy, tcSplitPredTy_maybe, 
-  isPredTy, isDictTy, tcSplitDFunTy, predTyUnique, 
+  isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, 
   mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
 
   ---------------------------------
@@ -94,17 +94,17 @@ module TcType (
   -- Type substitutions
   TvSubst(..),         -- Representation visible to a few friends
   TvSubstEnv, emptyTvSubst,
-  mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
+  mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
   getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
   extendTvSubst, extendTvSubstList, isInScope,
-  substTy, substTys, substTyWith, substTheta, substTyVar, 
+  substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
 
   isUnLiftedType,      -- Source types are always lifted
   isUnboxedTupleType,  -- Ditto
   isPrimitiveType, 
 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
-  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
+  tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
   typeKind, 
 
   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
@@ -122,11 +122,10 @@ import TypeRep            ( Type(..), TyNote(..), funTyCon )  -- friend
 
 import Type            (       -- Re-exports
                          tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
-                         tyVarsOfTheta, Kind, Type, PredType(..),
+                         tyVarsOfTheta, Kind, PredType(..),
                          ThetaType, unliftedTypeKind, 
                          liftedTypeKind, openTypeKind, mkArrowKind,
                          isLiftedTypeKind, isUnliftedTypeKind, 
-                         isOpenTypeKind, 
                          mkArrowKinds, mkForAllTy, mkForAllTys,
                          defaultKind, isArgTypeKind, isOpenTypeKind,
                          mkFunTy, mkFunTys, zipFunTys, 
@@ -140,13 +139,17 @@ import Type               (       -- Re-exports
                          tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
                          tidyTyVarBndr, tidyOpenTyVar,
                          tidyOpenTyVars, 
-                         isSubKind, 
+                         isSubKind, deShadowTy,
+
+                         tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
+                         tcEqPred, tcCmpPred, tcEqTypeX, 
+
                          TvSubst(..),
                          TvSubstEnv, emptyTvSubst,
-                         mkTvSubst, zipTvSubst, zipTopTvSubst, mkTopTvSubst,
+                         mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
                          getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
                          extendTvSubst, extendTvSubstList, isInScope,
-                         substTy, substTys, substTyWith, substTheta, substTyVar, 
+                         substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
 
                          typeKind, repType,
                          pprKind, pprParendKind,
@@ -156,22 +159,21 @@ import Type               (       -- Re-exports
 import TyCon           ( TyCon, isUnLiftedTyCon, tyConUnique )
 import DataCon         ( DataCon )
 import Class           ( Class )
-import Var             ( TyVar, Id, isTcTyVar, tcTyVarDetails )
+import Var             ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
 import ForeignCall     ( Safety, playSafe, DNType(..) )
-import VarEnv
 import VarSet
 
 -- others:
 import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
 import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )
 import NameSet
+import VarEnv          ( TidyEnv )
 import OccName         ( OccName, mkDictOcc )
 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
 import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
 import BasicTypes      ( IPName(..), ipNameName )
-import Unique          ( Unique, Uniquable(..) )
 import SrcLoc          ( SrcLoc, SrcSpan )
-import Util            ( cmpList, thenCmp, snocView )
+import Util            ( snocView )
 import Maybes          ( maybeToBool, expectJust )
 import Outputable
 import DATA_IOREF
@@ -227,6 +229,10 @@ type TcRhoType      = TcType
 type TcTauType      = TcType
 type TcKind         = Kind
 type TcTyVarSet     = TyVarSet
+
+type TcRef a    = IORef a
+data Expected ty = Infer (TcRef ty)    -- The hole to fill in for type inference
+                | Check ty             -- The type to check during type checking
 \end{code}
 
 
@@ -261,7 +267,8 @@ data SkolemInfo
                        -- variable for 'a'.  
   | ArrowSkol SrcSpan  -- An arrow form (see TcArrows)
 
-  | GenSkol TcType     -- Bound when doing a subsumption check for this type
+  | GenSkol [TcTyVar]  -- Bound when doing a subsumption check for 
+           TcType      --      (forall tvs. ty)
            SrcSpan
 
 data MetaDetails
@@ -271,6 +278,19 @@ data MetaDetails
   | Indirect TcType  -- Type indirections, treated as wobbly 
                      -- for the purpose of GADT unification.
 
+tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
+-- Tidy the type inside a GenSkol, preparatory to printing it
+tidySkolemTyVar env tv
+  = ASSERT( isSkolemTyVar tv )
+    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info1))
+  where
+    (env1, info1) = case skolemTvInfo tv of
+                     GenSkol tvs ty loc -> (env2, GenSkol tvs1 ty1 loc)
+                           where
+                             (env1, tvs1) = tidyOpenTyVars env tvs
+                             (env2, ty1)  = tidyOpenType env1 ty
+                     info -> (env, info)
+                    
 pprSkolemTyVar :: TcTyVar -> SDoc
 pprSkolemTyVar tv
   = ASSERT( isSkolemTyVar tv )
@@ -283,8 +303,9 @@ instance Outputable SkolemInfo where
   ppr (ArrowSkol loc)  = ptext SLIT("the arrow form at") <+> ppr loc
   ppr (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
                            nest 2 (ptext SLIT("at") <+> ppr loc)]
-  ppr (GenSkol ty loc) = sep [ptext SLIT("the polymorphic type") <+> quotes (ppr ty),
-                           nest 2 (ptext SLIT("at") <+> ppr loc)]
+  ppr (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type") 
+                                 <+> quotes (ppr (mkForAllTys tvs ty)),
+                                 nest 2 (ptext SLIT("at") <+> ppr loc)]
 
 instance Outputable MetaDetails where
   ppr Flexi        = ptext SLIT("Flexi")
@@ -480,31 +501,18 @@ tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
 
 tcIsTyVarTy :: Type -> Bool
 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
-\end{code}
-
-The type of a method for class C is always of the form:
-       Forall a1..an. C a1..an => sig_ty
-where sig_ty is the type given by the method's signature, and thus in general
-is a ForallTy.  At the point that splitMethodTy is called, it is expected
-that the outer Forall has already been stripped off.  splitMethodTy then
-returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes stripped off.
-
-\begin{code}
-tcSplitMethodTy :: Type -> (PredType, Type)
-tcSplitMethodTy ty = split ty
- where
-  split (FunTy arg res) = case tcSplitPredTy_maybe arg of
-                           Just p  -> (p, res)
-                           Nothing -> panic "splitMethodTy"
-  split (NoteTy n ty)  = split ty
-  split _               = panic "splitMethodTy"
 
 tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type])
 -- Split the type of a dictionary function
 tcSplitDFunTy ty 
-  = case tcSplitSigmaTy ty       of { (tvs, theta, tau) ->
-    case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) -> 
+  = case tcSplitSigmaTy ty   of { (tvs, theta, tau) ->
+    case tcSplitDFunHead tau of { (clas, tys) -> 
     (tvs, theta, clas, tys) }}
+
+tcSplitDFunHead :: Type -> (Class, [Type])
+tcSplitDFunHead tau  
+  = case tcSplitPredTy_maybe tau of 
+       Just (ClassP clas tys) -> (clas, tys)
 \end{code}
 
 
@@ -587,95 +595,6 @@ isLinearPred other            = False
 
 %************************************************************************
 %*                                                                     *
-\subsection{Comparison}
-%*                                                                     *
-%************************************************************************
-
-Comparison, taking note of newtypes, predicates, etc,
-
-\begin{code}
-tcEqType :: Type -> Type -> Bool
-tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
-
-tcEqTypes :: [Type] -> [Type] -> Bool
-tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
-
-tcEqPred :: PredType -> PredType -> Bool
-tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
-
--------------
-tcCmpType :: Type -> Type -> Ordering
-tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
-
-tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
-
-tcCmpPred p1 p2 = cmpPredTy emptyVarEnv p1 p2
--------------
-cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
-
--------------
-cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
-  -- The "env" maps type variables in ty1 to type variables in ty2
-  -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
-  -- we in effect substitute tv2 for tv1 in t1 before continuing
-
-    -- Look through NoteTy
-cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
-cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
-
-    -- Deal with equal constructors
-cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
-                                         Just tv1a -> tv1a `compare` tv2
-                                         Nothing   -> tv1  `compare` tv2
-
-cmpTy env (PredTy p1) (PredTy p2) = cmpPredTy env p1 p2
-cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
-cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
-cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
-cmpTy env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTy (extendVarEnv env tv1 tv2) t1 t2
-    
-    -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < PredTy
-cmpTy env (AppTy _ _) (TyVarTy _) = GT
-    
-cmpTy env (FunTy _ _) (TyVarTy _) = GT
-cmpTy env (FunTy _ _) (AppTy _ _) = GT
-    
-cmpTy env (TyConApp _ _) (TyVarTy _) = GT
-cmpTy env (TyConApp _ _) (AppTy _ _) = GT
-cmpTy env (TyConApp _ _) (FunTy _ _) = GT
-    
-cmpTy env (ForAllTy _ _) (TyVarTy _)    = GT
-cmpTy env (ForAllTy _ _) (AppTy _ _)    = GT
-cmpTy env (ForAllTy _ _) (FunTy _ _)    = GT
-cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
-
-cmpTy env (PredTy _)   t2              = GT
-
-cmpTy env _ _ = LT
-\end{code}
-
-\begin{code}
-cmpPredTy :: TyVarEnv TyVar -> PredType -> PredType -> Ordering
-cmpPredTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
-       -- Compare types as well as names for implicit parameters
-       -- This comparison is used exclusively (I think) for the
-       -- finite map built in TcSimplify
-cmpPredTy env (IParam _ _)     (ClassP _ _)      = LT
-cmpPredTy env (ClassP _ _)     (IParam _ _)     = GT
-cmpPredTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
-\end{code}
-
-PredTypes are used as a FM key in TcSimplify, 
-so we take the easy path and make them an instance of Ord
-
-\begin{code}
-instance Eq  PredType where { (==)    = tcEqPred }
-instance Ord PredType where { compare = tcCmpPred }
-\end{code}
-
-
-%************************************************************************
-%*                                                                     *
 \subsection{Predicates}
 %*                                                                     *
 %************************************************************************
@@ -721,6 +640,79 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 \end{code}
 
 
+
+
+%************************************************************************
+%*                                                                     *
+               Hoisting for-alls
+%*                                                                     *
+%************************************************************************
+
+hoistForAllTys is used for user-written type signatures only
+We want to 'look through' type synonyms when doing this
+so it's better done on the Type than the HsType
+
+It moves all the foralls and constraints to the top
+e.g.   T -> forall a. a        ==>   forall a. T -> a
+       T -> (?x::Int) -> Int   ==>   (?x::Int) -> T -> Int
+
+Also: it eliminates duplicate constraints.  These can show up
+when hoisting constraints, notably implicit parameters.
+
+It tries hard to retain type synonyms if hoisting does not break one
+up.  Not only does this improve error messages, but there's a tricky
+interaction with Haskell 98.  H98 requires no unsaturated type
+synonyms, which is checked by checkValidType.  This runs after
+hoisting, so we don't want hoisting to remove the SynNotes!  (We can't
+run validity checking before hoisting because in mutually-recursive
+type definitions we postpone validity checking until after the knot is
+tied.)
+
+\begin{code}
+hoistForAllTys :: Type -> Type
+hoistForAllTys ty
+  = go (deShadowTy ty)
+       -- Running over ty with an empty substitution gives it the
+       -- no-shadowing property.  This is important.  For example:
+       --      type Foo r = forall a. a -> r
+       --      foo :: Foo (Foo ())
+       -- Here the hoisting should give
+       --      foo :: forall a a1. a -> a1 -> ()
+       --
+       -- What about type vars that are lexically in scope in the envt?
+       -- We simply rely on them having a different unique to any
+       -- binder in 'ty'.  Otherwise we'd have to slurp the in-scope-tyvars
+       -- out of the envt, which is boring and (I think) not necessary.
+
+  where
+    go (TyVarTy tv)               = TyVarTy tv
+    go (TyConApp tc tys)          = TyConApp tc (map go tys)
+    go (PredTy pred)              = PredTy pred    -- No nested foralls 
+    go (NoteTy (SynNote ty1) ty2)  = NoteTy (SynNote (go ty1)) (go ty2)
+    go (NoteTy (FTVNote _) ty2)    = go ty2        -- Discard the free tyvar note
+    go (FunTy arg res)            = mk_fun_ty (go arg) (go res)
+    go (AppTy fun arg)            = AppTy (go fun) (go arg)
+    go (ForAllTy tv ty)                   = ForAllTy tv (go ty)
+
+       -- mk_fun_ty does all the work.  
+       -- It's building t1 -> t2: 
+       --      if t2 is a for-all type, push t1 inside it
+       --      if t2 is (pred -> t3), check for duplicates
+    mk_fun_ty ty1 ty2
+       | not (isSigmaTy ty2)           -- No forall's, or context => 
+       = FunTy ty1 ty2         
+       | PredTy p1 <- ty1              -- ty1 is a predicate
+       = if p1 `elem` theta then       -- so check for duplicates
+               ty2
+         else
+               mkSigmaTy tvs (p1:theta) tau
+       | otherwise     
+       = mkSigmaTy tvs theta (FunTy ty1 tau)
+       where
+         (tvs, theta, tau) = tcSplitSigmaTy ty2
+\end{code}
+
+
 %************************************************************************
 %*                                                                     *
 \subsection{Misc}