[project @ 2002-09-09 12:55:52 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
index 38d44c2..d4d506a 100644 (file)
@@ -51,7 +51,7 @@ import TcType         ( TcType, TcThetaType, TcTauType, TcPredType,
                          tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcSplitTyConApp_maybe, tcSplitForAllTys,
                          tcIsTyVarTy, tcSplitSigmaTy, 
-                         isUnLiftedType, isIPPred, isHoleTyVar,
+                         isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
 
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
@@ -82,8 +82,9 @@ import PrelNames      ( cCallableClassKey, cReturnableClassKey, hasKey )
 import ForeignCall     ( Safety(..) )
 import FunDeps         ( grow )
 import PprType         ( pprPred, pprSourceType, pprTheta, pprClassPred )
-import Name            ( Name, NamedThing(..), setNameUnique, mkSystemName,
-                         mkInternalName, mkDerivedTyConOcc
+import Name            ( Name, NamedThing(..), setNameUnique, 
+                         mkInternalName, mkDerivedTyConOcc, 
+                         mkSystemTvNameEncoded,
                        )
 import VarSet
 import BasicTypes      ( Boxity(Boxed) )
@@ -106,7 +107,7 @@ import Outputable
 newTyVar :: Kind -> NF_TcM TcTyVar
 newTyVar kind
   = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSystemName uniq FSLIT("t")) kind VanillaTv
+    tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
 
 newTyVarTy  :: Kind -> NF_TcM TcType
 newTyVarTy kind
@@ -119,7 +120,7 @@ newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 newKindVar :: NF_TcM TcKind
 newKindVar
   = tcGetUnique                                                        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSystemName uniq FSLIT("k")) superKind VanillaTv   `thenNF_Tc` \ kv ->
+    tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv  `thenNF_Tc` \ kv ->
     returnNF_Tc (TyVarTy kv)
 
 newKindVars :: Int -> NF_TcM [TcKind]
@@ -128,7 +129,7 @@ newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 newBoxityVar :: NF_TcM TcKind
 newBoxityVar
   = tcGetUnique                                                          `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSystemName uniq FSLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
+    tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
     returnNF_Tc (TyVarTy kv)
 \end{code}
 
@@ -142,7 +143,7 @@ newBoxityVar
 \begin{code}
 newHoleTyVarTy :: NF_TcM TcType
   = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSystemName uniq FSLIT("h")) openTypeKind HoleTv   `thenNF_Tc` \ tv ->
+    tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv  `thenNF_Tc` \ tv ->
     returnNF_Tc (TyVarTy tv)
 
 readHoleResult :: TcType -> NF_TcM TcType
@@ -414,7 +415,7 @@ mkArbitraryType tv
          = tupleTyCon Boxed (length args)      -- *-> ... ->*->*
 
          | otherwise
-         = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
+         = pprTrace "Urk! Inventing strangely-kinded void TyCon:" (ppr tc_name $$ ppr kind) $
            mkPrimTyCon tc_name kind 0 [] VoidRep
                -- Same name as the tyvar, apart from making it start with a colon (sigh)
                -- I dread to think what will happen if this gets out into an 
@@ -445,11 +446,45 @@ zonkTcTyVarToTyVar tv
        -- so that all other occurrences of the tyvar will get zapped too
     zonkTyVar zap tv           `thenNF_Tc` \ ty2 ->
 
+       -- This warning shows up if the allegedly-unbound tyvar is
+       -- already bound to something.  It can actually happen, and 
+       -- in a harmless way (see [Silly Type Synonyms] below) so
+       -- it's only a warning
     WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
 
     returnNF_Tc immut_tv
 \end{code}
 
+[Silly Type Synonyms]
+
+Consider this:
+       type C u a = u  -- Note 'a' unused
+
+       foo :: (forall a. C u a -> C u a) -> u
+       foo x = ...
+
+       bar :: Num u => u
+       bar = foo (\t -> t + t)
+
+* From the (\t -> t+t) we get type  {Num d} =>  d -> d
+  where d is fresh.
+
+* Now unify with type of foo's arg, and we get:
+       {Num (C d a)} =>  C d a -> C d a
+  where a is fresh.
+
+* Now abstract over the 'a', but float out the Num (C d a) constraint
+  because it does not 'really' mention a.  (see Type.tyVarsOfType)
+  The arg to foo becomes
+       /\a -> \t -> t+t
+
+* So we get a dict binding for Num (C d a), which is zonked to give
+       a = ()
+
+* Then the /\a abstraction has a zonked 'a' in it.
+
+All very silly.   I think its harmless to ignore the problem.
+
 
 %************************************************************************
 %*                                                                     *
@@ -901,6 +936,10 @@ check_valid_theta ctxt []
 check_valid_theta ctxt theta
   = getDOptsTc                                 `thenNF_Tc` \ dflags ->
     warnTc (notNull dups) (dupPredWarn dups)   `thenNF_Tc_`
+       -- Actually, in instance decls and type signatures, 
+       -- duplicate constraints are eliminated by TcMonoType.hoistForAllTys,
+       -- so this error can only fire for the context of a class or
+       -- data type decl.
     mapTc_ (check_source_ty dflags ctxt) theta
   where
     (_,dups) = removeDups tcCmpPred theta
@@ -910,7 +949,7 @@ check_source_ty dflags ctxt pred@(ClassP cls tys)
   =    -- Class predicates are valid in all contexts
     mapTc_ check_arg_type tys          `thenTc_`
     checkTc (arity == n_tys) arity_err         `thenTc_`
-    checkTc (all tyvar_head tys || arby_preds_ok)
+    checkTc (check_class_pred_tys dflags ctxt tys)
            (predTyVarErr pred $$ how_to_allow)
 
   where
@@ -919,12 +958,6 @@ check_source_ty dflags ctxt pred@(ClassP cls tys)
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
 
-    arby_preds_ok = case ctxt of
-                       InstHeadCtxt  -> True   -- We check for instance-head formation
-                                               -- in checkValidInstHead
-                       InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
-                       other         -> dopt Opt_GlasgowExts               dflags
-
     how_to_allow = case ctxt of
                     InstHeadCtxt  -> empty     -- Should not happen
                     InstThetaCtxt -> parens undecidableMsg
@@ -946,6 +979,17 @@ check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 
 -------------------------
+check_class_pred_tys dflags ctxt tys 
+  = case ctxt of
+       InstHeadCtxt  -> True   -- We check for instance-head 
+                               -- formation in checkValidInstHead
+       InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
+       other         -> gla_exts       || all tyvar_head tys
+  where
+    undecidable_ok = dopt Opt_AllowUndecidableInstances dflags 
+    gla_exts      = dopt Opt_GlasgowExts dflags
+
+-------------------------
 tyvar_head ty                  -- Haskell 98 allows predicates of form 
   | tcIsTyVarTy ty = True      --      C (a ty1 .. tyn)
   | otherwise                  -- where a is a type variable