[project @ 2003-02-14 14:19:15 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcUnify.lhs
index 4446534..e4116e2 100644 (file)
@@ -7,12 +7,12 @@
 module TcUnify (
        -- Full-blown subsumption
   tcSubOff, tcSubExp, tcGen, subFunTy, TcHoleType,
-  checkSigTyVars, checkSigTyVarsWrt, sigCtxt, 
+  checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals,
 
        -- Various unifications
   unifyTauTy, unifyTauTyList, unifyTauTyLists, 
   unifyFunTy, unifyListTy, unifyPArrTy, unifyTupleTy,
-  unifyKind, unifyKinds, unifyOpenTypeKind,
+  unifyKind, unifyKinds, unifyOpenTypeKind, unifyFunKind,
 
        -- Coercions
   Coercion, ExprCoFn, PatCoFn, 
@@ -26,8 +26,7 @@ module TcUnify (
 
 import HsSyn           ( HsExpr(..) )
 import TcHsSyn         ( TypecheckedHsExpr, TcPat, mkHsLet )
-import TypeRep         ( Type(..), SourceType(..), TyNote(..),
-                         openKindCon, typeCon )
+import TypeRep         ( Type(..), SourceType(..), TyNote(..), openKindCon )
 
 import TcRnMonad         -- TcType, amongst others
 import TcType          ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
@@ -39,22 +38,22 @@ import TcType               ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
                          typeKind, tcSplitFunTy_maybe, mkForAllTys,
                          isHoleTyVar, isSkolemTyVar, isUserTyVar, 
                          tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
-                         eqKind, openTypeKind, liftedTypeKind, isTypeKind,
-                         hasMoreBoxityInfo, tyVarBindingInfo, allDistinctTyVars
+                         eqKind, openTypeKind, liftedTypeKind, isTypeKind, mkArrowKind,
+                         hasMoreBoxityInfo, allDistinctTyVars
                        )
 import qualified Type  ( getTyVar_maybe )
 import Inst            ( newDicts, instToId, tcInstCall )
-import TcMType         ( getTcTyVar, putTcTyVar, tcInstType, readHoleResult,
-                         newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy,
+import TcMType         ( getTcTyVar, putTcTyVar, tcInstType, readHoleResult, newKindVar,
+                         newTyVarTy, newTyVarTys, newOpenTypeKind, newHoleTyVarTy, 
                          zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcTyVar )
 import TcSimplify      ( tcSimplifyCheck )
 import TysWiredIn      ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
-import TcEnv           ( TcTyThing(..), tcGetGlobalTyVars, getLclEnvElts )
+import TcEnv           ( TcTyThing(..), tcGetGlobalTyVars, findGlobals )
 import TyCon           ( tyConArity, isTupleTyCon, tupleTyConBoxity )
 import PprType         ( pprType )
 import Id              ( Id, mkSysLocal, idType )
 import Var             ( Var, varName, tyVarKind )
-import VarSet          ( emptyVarSet, unionVarSet, elemVarSet, varSetElems )
+import VarSet          ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
 import VarEnv
 import Name            ( isSystemName, getSrcLoc )
 import ErrUtils                ( Message )
@@ -101,7 +100,8 @@ These two check for holes
 
 \begin{code}
 tcSubExp expected_ty offered_ty
-  = checkHole expected_ty offered_ty tcSub
+  = traceTc (text "tcSubExp" <+> (ppr expected_ty $$ ppr offered_ty))  `thenM_`
+    checkHole expected_ty offered_ty tcSub
 
 tcSubOff expected_ty offered_ty
   = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
@@ -117,7 +117,8 @@ checkHole (TyVarTy tv) other_ty thing_inside
   = getTcTyVar tv      `thenM` \ maybe_ty ->
     case maybe_ty of
        Just ty -> thing_inside ty other_ty
-       Nothing -> putTcTyVar tv other_ty       `thenM_`
+       Nothing -> traceTc (text "checkHole" <+> ppr tv)        `thenM_`
+                  putTcTyVar tv other_ty       `thenM_`
                   returnM idCoercion
 
 checkHole ty other_ty thing_inside 
@@ -130,7 +131,7 @@ No holes expected now.  Add some error-check context info.
 tcSub expected_ty actual_ty
   = traceTc (text "tcSub" <+> details)         `thenM_`
     addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
-                 (tc_sub expected_ty expected_ty actual_ty actual_ty)
+               (tc_sub expected_ty expected_ty actual_ty actual_ty)
   where
     details = vcat [text "Expected:" <+> ppr expected_ty,
                    text "Actual:  " <+> ppr actual_ty]
@@ -200,7 +201,19 @@ tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
 --      when the arg/res is not a tau-type?
 -- NO!  e.g.   f :: ((forall a. a->a) -> Int) -> Int
 --     then   x = (f,f)
---     is perfectly fine!
+--     is perfectly fine, because we can instantiat f's type to a monotype
+--
+-- However, we get can get jolly unhelpful error messages.  
+--     e.g.    foo = id runST
+--
+--    Inferred type is less polymorphic than expected
+--     Quantified type variable `s' escapes
+--     Expected type: ST s a -> t
+--     Inferred type: (forall s1. ST s1 a) -> a
+--    In the first argument of `id', namely `runST'
+--    In a right-hand side of function `foo': id runST
+--
+-- I'm not quite sure what to do about this!
 
 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
   = ASSERT( not (isHoleTyVar tv) )
@@ -333,7 +346,7 @@ tcGen expected_ty extra_tvs thing_inside    -- We expect expected_ty to be a forall
     returnM (mkCoercion co_fn, result)
   where
     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
-    sig_msg  = ptext SLIT("type of an expression")
+    sig_msg  = ptext SLIT("expected type of an expression")
 \end{code}    
 
     
@@ -879,9 +892,7 @@ unify_tuple_ty_help boxity arity ty
 unifyKind :: TcKind                -- Expected
          -> TcKind                 -- Actual
          -> TcM ()
-unifyKind k1 k2 
-  = addErrCtxtM (unifyCtxt "kind" k1 k2) $
-    uTys k1 k1 k2 k2
+unifyKind k1 k2 = uTys k1 k1 k2 k2
 
 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
 unifyKinds []       []       = returnM ()
@@ -906,10 +917,27 @@ unifyOpenTypeKind ty
   | otherwise     = unify_open_kind_help ty
 
 unify_open_kind_help ty        -- Revert to ordinary unification
-  = newBoxityVar       `thenM` \ boxity ->
-    unifyKind ty (mkTyConApp typeCon [boxity])
+  = newOpenTypeKind    `thenM` \ open_kind ->
+    unifyKind ty open_kind
 \end{code}
 
+\begin{code}
+unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
+-- Like unifyFunTy, but does not fail; instead just returns Nothing
+
+unifyFunKind (TyVarTy tyvar)
+  = getTcTyVar tyvar   `thenM` \ maybe_ty ->
+    case maybe_ty of
+       Just fun_kind -> unifyFunKind fun_kind
+       Nothing       -> newKindVar     `thenM` \ arg_kind ->
+                        newKindVar     `thenM` \ res_kind ->
+                        putTcTyVar tyvar (mkArrowKind arg_kind res_kind)       `thenM_`
+                        returnM (Just (arg_kind,res_kind))
+    
+unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
+unifyFunKind (NoteTy _ ty)            = unifyFunKind ty
+unifyFunKind other                    = returnM Nothing
+\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -1117,8 +1145,7 @@ check_sig_tyvars extra_tvs sig_tvs
                        -- Game plan: 
                        --       get the local TcIds and TyVars from the environment,
                        --       and pass them to find_globals (they might have tv free)
-           then   getLclEnvElts                        `thenM` \ ve ->
-                  find_globals tv tidy_env ve          `thenM` \ (tidy_env1, globs) ->
+           then   findGlobals (unitVarSet tv) tidy_env         `thenM` \ (tidy_env1, globs) ->
                   returnM (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
 
            else        -- All OK
@@ -1129,59 +1156,6 @@ check_sig_tyvars extra_tvs sig_tvs
 
 \begin{code}
 -----------------------
--- find_globals looks at the value environment and finds values
--- whose types mention the offending type variable.  It has to be 
--- careful to zonk the Id's type first, so it has to be in the monad.
--- We must be careful to pass it a zonked type variable, too.
-
-find_globals :: Var 
-             -> TidyEnv 
-             -> [TcTyThing] 
-             -> TcM (TidyEnv, [SDoc])
-
-find_globals tv tidy_env things
-  = go tidy_env [] things
-  where
-    go tidy_env acc [] = returnM (tidy_env, acc)
-    go tidy_env acc (thing : things)
-      = find_thing ignore_it tidy_env thing    `thenM` \ (tidy_env1, maybe_doc) ->
-       case maybe_doc of
-         Just d  -> go tidy_env1 (d:acc) things
-         Nothing -> go tidy_env1 acc     things
-
-    ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
-
------------------------
-find_thing ignore_it tidy_env (ATcId id _)
-  = zonkTcType  (idType id)    `thenM` \ id_ty ->
-    if ignore_it id_ty then
-       returnM (tidy_env, Nothing)
-    else let
-       (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
-       msg = sep [ppr id <+> dcolon <+> ppr tidy_ty, 
-                  nest 2 (parens (ptext SLIT("bound at") <+>
-                                  ppr (getSrcLoc id)))]
-    in
-    returnM (tidy_env', Just msg)
-
-find_thing ignore_it tidy_env (ATyVar tv)
-  = zonkTcTyVar tv             `thenM` \ tv_ty ->
-    if ignore_it tv_ty then
-       returnM (tidy_env, Nothing)
-    else let
-       (tidy_env1, tv1)     = tidyOpenTyVar tidy_env  tv
-       (tidy_env2, tidy_ty) = tidyOpenType  tidy_env1 tv_ty
-       msg = sep [ppr tv1 <+> eq_stuff, nest 2 bound_at]
-
-       eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
-                | otherwise                                        = equals <+> ppr tv_ty
-               -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
-       
-       bound_at = tyVarBindingInfo tv
-    in
-    returnM (tidy_env2, Just msg)
-
------------------------
 escape_msg sig_tv tv globs
   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
     if notNull globs then