[project @ 2005-10-14 11:22:41 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcType.lhs
index ce31dd5..08d122c 100644 (file)
@@ -23,9 +23,9 @@ module TcType (
   --------------------------------
   -- MetaDetails
   Expected(..), TcRef, TcTyVarDetails(..),
-  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar,
-  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef,
-  isFlexi, isIndirect,
+  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
+  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
+  isFlexi, isIndirect, 
 
   --------------------------------
   -- Builders
@@ -38,14 +38,14 @@ module TcType (
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy,
-  tcGetTyVar_maybe, tcGetTyVar,
+  tcValidInstHeadTy, tcGetTyVar_maybe, tcGetTyVar,
 
   ---------------------------------
   -- Predicates. 
   -- Again, newtypes are opaque
   tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
   isSigmaTy, isOverloadedTy, 
-  isDoubleTy, isFloatTy, isIntTy,
+  isDoubleTy, isFloatTy, isIntTy, isStringTy,
   isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
   isTauTy, tcIsTyVarTy, tcIsForAllTy,
 
@@ -62,6 +62,7 @@ module TcType (
   mkDictTy, tcSplitPredTy_maybe, 
   isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, 
   mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
+  dataConsStupidTheta, 
 
   ---------------------------------
   -- Foreign import and export
@@ -105,7 +106,7 @@ module TcType (
 
   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
   tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar,
-  typeKind, 
+  typeKind, tidyKind,
 
   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
 
@@ -138,7 +139,7 @@ import Type         (       -- Re-exports
                          tidyTopType, tidyType, tidyPred, tidyTypes,
                          tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
                          tidyTyVarBndr, tidyOpenTyVar,
-                         tidyOpenTyVars, 
+                         tidyOpenTyVars, tidyKind,
                          isSubKind, deShadowTy,
 
                          tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
@@ -149,22 +150,24 @@ import Type               (       -- Re-exports
                          mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
                          getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
                          extendTvSubst, extendTvSubstList, isInScope,
-                         substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr,
+                         substTy, substTys, substTyWith, substTheta, 
+                         substTyVar, substTyVarBndr, substPred,
 
                          typeKind, repType,
                          pprKind, pprParendKind,
                          pprType, pprParendType, pprTyThingCategory,
                          pprPred, pprTheta, pprThetaArrow, pprClassPred
                        )
-import TyCon           ( TyCon, isUnLiftedTyCon, tyConUnique )
-import DataCon         ( DataCon )
+import TyCon           ( TyCon, isUnLiftedTyCon, isSynTyCon, tyConUnique )
+import DataCon         ( DataCon, dataConStupidTheta, dataConResTys )
 import Class           ( Class )
 import Var             ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
 import ForeignCall     ( Safety, playSafe, DNType(..) )
+import Unify           ( tcMatchTys )
 import VarSet
 
 -- others:
-import CmdLineOpts     ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
+import DynFlags                ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
 import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )
 import NameSet
 import VarEnv          ( TidyEnv )
@@ -173,8 +176,10 @@ import PrelNames   -- Lots (e.g. in isFFIArgumentTy)
 import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
 import BasicTypes      ( IPName(..), ipNameName )
 import SrcLoc          ( SrcLoc, SrcSpan )
-import Util            ( snocView )
-import Maybes          ( maybeToBool, expectJust )
+import Util            ( snocView, equalLength )
+import Maybes          ( maybeToBool, expectJust, mapCatMaybes )
+import ListSetOps      ( hasNoDups )
+import List            ( nubBy )
 import Outputable
 import DATA_IOREF
 \end{code}
@@ -247,13 +252,45 @@ checking.  It's attached to mutable type variables only.
 It's knot-tied back to Var.lhs.  There is no reason in principle
 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 
+Note [Signature skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+
+  x :: [a]
+  y :: b
+  (x,y,z) = ([y,z], z, head x)
+
+Here, x and y have type sigs, which go into the environment.  We used to
+instantiate their types with skolem constants, and push those types into
+the RHS, so we'd typecheck the RHS with type
+       ( [a*], b*, c )
+where a*, b* are skolem constants, and c is an ordinary meta type varible.
+
+The trouble is that the occurrences of z in the RHS force a* and b* to 
+be the *same*, so we can't make them into skolem constants that don't unify
+with each other.  Alas.
+
+On the other hand, we *must* use skolems for signature type variables, 
+becuase GADT type refinement refines skolems only.  
+
+One solution woudl be insist that in the above defn the programmer uses
+the same type variable in both type signatures.  But that takes explanation.
+
+The alternative (currently implemented) is to have a special kind of skolem
+constant, SigSkokTv, which can unify with other SigSkolTvs.  
+
+
 \begin{code}
 type TcTyVar = TyVar   -- Used only during type inference
 
 -- A TyVarDetails is inside a TyVar
 data TcTyVarDetails
-  = SkolemTv SkolemInfo                -- A skolem constant
-  | MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
+  = MetaTv (IORef MetaDetails)         -- A meta type variable stands for a tau-type
+  | SkolemTv SkolemInfo                        -- A skolem constant
+  | SigSkolTv Name (IORef MetaDetails) -- Ditto, but from a type signature;
+                                       --      see Note [Signature skolems]
+                                       --      The MetaDetails, if filled in, will 
+                                       --      always be another SigSkolTv
 
 data SkolemInfo
   = SigSkol Name       -- Bound at a type signature
@@ -282,30 +319,34 @@ 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))
+    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
   where
-    (env1, info1) = case skolemTvInfo tv of
-                     GenSkol tvs ty loc -> (env2, GenSkol tvs1 ty1 loc)
+    (env1, info1) = case tcTyVarDetails tv of
+                     SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (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 )
-    quotes (ppr tv) <+> ptext SLIT("is bound by") <+> ppr (skolemTvInfo tv)
-
-instance Outputable SkolemInfo where
-  ppr (SigSkol id)  = ptext SLIT("the type signature for") <+> quotes (ppr id)
-  ppr (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
-  ppr (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
-  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 tvs ty loc) = sep [ptext SLIT("the polymorphic type") 
-                                 <+> quotes (ppr (mkForAllTys tvs ty)),
-                                 nest 2 (ptext SLIT("at") <+> ppr loc)]
+pprTcTyVar :: TcTyVar -> SDoc
+-- Print tyvar with info about its binding
+pprTcTyVar tv
+  = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
+  where
+    ppr_details (MetaTv _)      = ptext SLIT("is a meta type variable")
+    ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id)
+    ppr_details (SkolemTv info)  = ptext SLIT("is bound by") <+> pprSkolInfo info
+pprSkolInfo :: SkolemInfo -> SDoc
+pprSkolInfo (SigSkol id)     = ptext SLIT("the type signature for") <+> quotes (ppr id)
+pprSkolInfo (ClsSkol cls)    = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo (InstSkol df)    = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
+pprSkolInfo (ArrowSkol loc)  = ptext SLIT("the arrow form at") <+> ppr loc
+pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
+                                   nest 2 (ptext SLIT("at") <+> ppr loc)]
+pprSkolInfo (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")
@@ -319,8 +360,9 @@ isImmutableTyVar tv
 isSkolemTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-       SkolemTv _ -> True
-       MetaTv _   -> False
+       SkolemTv _    -> True
+       SigSkolTv _ _ -> True
+       MetaTv _      -> False
 
 isExistentialTyVar tv  -- Existential type variable, bound by a pattern
   = ASSERT( isTcTyVar tv )
@@ -331,20 +373,15 @@ isExistentialTyVar tv     -- Existential type variable, bound by a pattern
 isMetaTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-       SkolemTv _ -> False
        MetaTv _   -> True
-
-skolemTvInfo :: TyVar -> SkolemInfo
-skolemTvInfo tv 
-  = ASSERT( isTcTyVar tv )
-    case tcTyVarDetails tv of
-       SkolemTv info -> info
+       other      -> False
 
 metaTvRef :: TyVar -> IORef MetaDetails
 metaTvRef tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
-        MetaTv ref -> ref
+       MetaTv ref -> ref
+       other      -> pprPanic "metaTvRef" (ppr tv)
 
 isFlexi, isIndirect :: MetaDetails -> Bool
 isFlexi Flexi = True
@@ -454,6 +491,30 @@ tcSplitTyConApp_maybe (NoteTy n ty)     = tcSplitTyConApp_maybe ty
        -- as tycon applications by the type checker
 tcSplitTyConApp_maybe other                    = Nothing
 
+tcValidInstHeadTy :: Type -> Bool
+-- Used in Haskell-98 mode, for the argument types of an instance head
+-- These must not be type synonyms, but everywhere else type synonyms
+-- are transparent, so we need a special function here
+tcValidInstHeadTy ty 
+  = case ty of
+       TyConApp tc tys -> ASSERT( not (isSynTyCon tc) ) ok tys
+                          -- A synonym would be a NoteTy
+       FunTy arg res        -> ok [arg, res]
+       NoteTy (SynNote _) _ -> False
+       NoteTy other_note ty -> tcValidInstHeadTy ty
+       other                -> False
+  where
+       -- Check that all the types are type variables,
+       -- and that each is distinct
+    ok tys = equalLength tvs tys && hasNoDups tvs
+          where
+            tvs = mapCatMaybes get_tv tys
+
+    get_tv (TyVarTy tv)          = Just tv       -- Again, do not look
+    get_tv (NoteTy (SynNote _) _) = Nothing    -- through synonyms
+    get_tv (NoteTy other_note ty) = get_tv ty
+    get_tv other                 = Nothing
+
 tcSplitFunTys :: Type -> ([Type], Type)
 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
                        Nothing        -> ([], ty)
@@ -592,6 +653,27 @@ isLinearPred (IParam (Linear n) _) = True
 isLinearPred other                = False
 \end{code}
 
+--------------------- The stupid theta (sigh) ---------------------------------
+
+\begin{code}
+dataConsStupidTheta :: [DataCon] -> ThetaType
+-- Union the stupid thetas from all the specified constructors (non-empty)
+-- All the constructors should have the same result type, modulo alpha conversion
+-- The resulting ThetaType uses type variables from the *first* constructor in the list
+--
+-- It's here because it's used in MkId.mkRecordSelId, and in TcExpr
+dataConsStupidTheta (con1:cons)
+  = nubBy tcEqPred all_preds
+  where
+    all_preds    = dataConStupidTheta con1 ++ other_stupids
+    res_tys1     = dataConResTys con1
+    tvs1         = tyVarsOfTypes res_tys1
+    other_stupids = [ substPred subst pred
+                   | con <- cons
+                   , let Just subst = tcMatchTys tvs1 res_tys1 (dataConResTys con)
+                   , pred <- dataConStupidTheta con ]
+\end{code}
+
 
 %************************************************************************
 %*                                                                     *
@@ -721,18 +803,9 @@ hoistForAllTys ty
 
 \begin{code}
 deNoteType :: Type -> Type
-       -- Remove synonyms, but not predicate types
-deNoteType ty@(TyVarTy tyvar)  = ty
-deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
-deNoteType (PredTy p)          = PredTy (deNotePredType p)
-deNoteType (NoteTy _ ty)       = deNoteType ty
-deNoteType (AppTy fun arg)     = AppTy (deNoteType fun) (deNoteType arg)
-deNoteType (FunTy fun arg)     = FunTy (deNoteType fun) (deNoteType arg)
-deNoteType (ForAllTy tv ty)    = ForAllTy tv (deNoteType ty)
-
-deNotePredType :: PredType -> PredType
-deNotePredType (ClassP c tys)   = ClassP c (map deNoteType tys)
-deNotePredType (IParam n ty)    = IParam n (deNoteType ty)
+-- Remove *outermost* type synonyms and other notes
+deNoteType (NoteTy _ ty) = deNoteType ty
+deNoteType ty           = ty
 \end{code}
 
 Find the free tycons and classes of a type.  This is used in the front
@@ -744,8 +817,8 @@ tyClsNamesOfType (TyVarTy tv)                   = emptyNameSet
 tyClsNamesOfType (TyConApp tycon tys)      = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
 tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
 tyClsNamesOfType (NoteTy other_note    ty2) = tyClsNamesOfType ty2
-tyClsNamesOfType (PredTy (IParam n ty))   = tyClsNamesOfType ty
-tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (PredTy (IParam n ty))     = tyClsNamesOfType ty
+tyClsNamesOfType (PredTy (ClassP cl tys))   = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
 tyClsNamesOfType (FunTy arg res)           = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
 tyClsNamesOfType (AppTy fun arg)           = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
 tyClsNamesOfType (ForAllTy tyvar ty)       = tyClsNamesOfType ty