[project @ 2001-07-10 11:32:28 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index 52aec0e..4ceae2b 100644 (file)
@@ -4,14 +4,15 @@
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
-module TcMonoType ( tcHsType, tcHsRecType, 
+module TcMonoType ( tcHsType, tcHsRecType, tcIfaceType,
                    tcHsSigType, tcHsLiftedSigType, 
-                   tcRecClassContext, checkAmbiguity,
+                   tcRecTheta, checkAmbiguity,
 
                        -- Kind checking
                    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
-                   kcHsType, kcHsSigType, kcHsLiftedSigType, kcHsContext,
-                   tcTyVars, tcHsTyVars, mkImmutTyVars,
+                   kcHsType, kcHsSigType, kcHsSigTypes, 
+                   kcHsLiftedSigType, kcHsContext,
+                   tcScopedTyVars, tcHsTyVars, mkImmutTyVars,
 
                    TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
                    checkSigTyVars, sigCtxt, sigPatCtxt
@@ -29,35 +30,35 @@ import TcEnv                ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
                          tcGetGlobalTyVars, tcEnvTcIds, tcEnvTyVars,
                          TyThing(..), TcTyThing(..), tcExtendKindEnv
                        )
-import TcType          ( TcKind, TcTyVar, TcThetaType, TcTauType,
-                         newKindVar, tcInstSigVar,
-                         zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar
+import TcMType         ( newKindVar, tcInstSigVars, 
+                         zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar,
+                         unifyKind, unifyOpenTypeKind
                        )
-import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
-import FunDeps         ( grow )
-import TcUnify         ( unifyKind, unifyOpenTypeKind )
-import Unify           ( allDistinctTyVars )
-import Type            ( Type, Kind, PredType(..), ThetaType, SigmaType, TauType,
+import TcType          ( Type, Kind, SourceType(..), ThetaType, SigmaType, TauType,
                          mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
-                          zipFunTys, hoistForAllTys,
+                         tcSplitForAllTys, tcSplitRhoTy,
+                         hoistForAllTys, allDistinctTyVars,
+                          zipFunTys, 
                          mkSigmaTy, mkPredTy, mkTyConApp,
-                         mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
+                         mkAppTys, mkRhoTy,
                          liftedTypeKind, unliftedTypeKind, mkArrowKind,
-                         mkArrowKinds, getTyVar_maybe, getTyVar, splitFunTy_maybe,
+                         mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe,
                          tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
                          tyVarsOfType, tyVarsOfPred, mkForAllTys,
-                         classesOfPreds, isUnboxedTupleType, isForAllTy
+                         isUnboxedTupleType, tcIsForAllTy, isIPPred
                        )
-import PprType         ( pprType, pprPred )
+import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
+import FunDeps         ( grow )
+import PprType         ( pprType, pprTheta, pprPred )
 import Subst           ( mkTopTyVarSubst, substTy )
 import CoreFVs         ( idFreeTyVars )
-import Id              ( mkVanillaId, idName, idType )
+import Id              ( mkLocalId, idName, idType )
 import Var             ( Id, Var, TyVar, mkTyVar, tyVarKind )
 import VarEnv
 import VarSet
 import ErrUtils                ( Message )
 import TyCon           ( TyCon, isSynTyCon, tyConArity, tyConKind )
-import Class           ( ClassContext, classArity, classTyCon )
+import Class           ( classArity, classTyCon )
 import Name            ( Name )
 import TysWiredIn      ( mkListTy, mkTupleTy, genUnitTyCon )
 import BasicTypes      ( Boxity(..), RecFlag(..), isRec )
@@ -117,6 +118,10 @@ But equally valid would be
                                a::(*->*)-> *, b::*->*
 
 \begin{code}
+-- tcHsTyVars is used for type variables in type signatures
+--     e.g. forall a. a->a
+-- They are immutable, because they scope only over the signature
+-- They may or may not be explicitly-kinded
 tcHsTyVars :: [HsTyVarBndr Name] 
           -> TcM a                             -- The kind checker
           -> ([TyVar] -> TcM b)
@@ -134,16 +139,22 @@ tcHsTyVars tv_names kind_check thing_inside
     in
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 
-tcTyVars :: [Name] 
-            -> TcM a                           -- The kind checker
-            -> TcM [TyVar]
-tcTyVars [] kind_check = returnTc []
-
-tcTyVars tv_names kind_check
+-- tcScopedTyVars is used for scoped type variables
+--     e.g.  \ (x::a) (y::a) -> x+y
+-- They never have explicit kinds (because this is source-code only)
+-- They are mutable (because they can get bound to a more specific type)
+tcScopedTyVars :: [Name] 
+              -> TcM a                         -- The kind checker
+              -> TcM b
+              -> TcM b
+tcScopedTyVars [] kind_check thing_inside = thing_inside
+
+tcScopedTyVars tv_names kind_check thing_inside
   = mapNF_Tc newNamedKindVar tv_names          `thenTc` \ kind_env ->
     tcExtendKindEnv kind_env kind_check                `thenTc_`
     zonkKindEnv kind_env                       `thenNF_Tc` \ tvs_w_kinds ->
-    listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- tvs_w_kinds]
+    listTc [tcNewMutTyVar name kind | (name, kind) <- tvs_w_kinds]     `thenNF_Tc` \ tyvars ->
+    tcExtendTyVarEnv tyvars thing_inside
 \end{code}
     
 
@@ -178,7 +189,8 @@ kcTypeType ty
 ---------------------------
 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
        -- Used for type signatures
-kcHsSigType     = kcTypeType
+kcHsSigType      = kcTypeType
+kcHsSigTypes tys  = mapTc_ kcHsSigType tys
 kcHsLiftedSigType = kcLiftedType
 
 ---------------------------
@@ -200,6 +212,9 @@ kcHsType (HsFunTy ty1 ty2)
     kcTypeType ty2     `thenTc_`
     returnTc liftedTypeKind
 
+kcHsType (HsNumTy _)           -- The unit type for generics
+  = returnTc liftedTypeKind
+
 kcHsType ty@(HsOpTy ty1 op ty2)
   = kcTyVar op                         `thenTc` \ op_kind ->
     kcHsType ty1                       `thenTc` \ ty1_kind ->
@@ -227,7 +242,7 @@ kcHsType (HsForAllTy (Just tv_names) context ty)
 
 ---------------------------
 kcAppKind fun_kind arg_kind
-  = case splitFunTy_maybe fun_kind of 
+  = case tcSplitFunTy_maybe fun_kind of 
        Just (arg_kind', res_kind)
                -> unifyKind arg_kind arg_kind' `thenTc_`
                   returnTc res_kind
@@ -241,11 +256,11 @@ kcAppKind fun_kind arg_kind
 kcHsContext ctxt = mapTc_ kcHsPred ctxt
 
 kcHsPred :: RenamedHsPred -> TcM ()
-kcHsPred pred@(HsPIParam name ty)
+kcHsPred pred@(HsIParam name ty)
   = tcAddErrCtxt (appKindCtxt (ppr pred))      $
     kcLiftedType ty
 
-kcHsPred pred@(HsPClass cls tys)
+kcHsPred pred@(HsClassP cls tys)
   = tcAddErrCtxt (appKindCtxt (ppr pred))      $
     kcClass cls                                        `thenTc` \ kind ->
     mapTc kcHsType tys                         `thenTc` \ arg_kinds ->
@@ -290,14 +305,25 @@ tcHsSigType and tcHsLiftedSigType are used for type signatures written by the pr
 \begin{code}
 tcHsSigType, tcHsLiftedSigType :: RenamedHsType -> TcM Type
   -- Do kind checking, and hoist for-alls to the top
-tcHsSigType      ty = kcTypeType ty  `thenTc_`  tcHsType ty    
-tcHsLiftedSigType ty = kcLiftedType ty `thenTc_`  tcHsType ty
+tcHsSigType       ty = kcTypeType   ty `thenTc_` tcHsType ty
+tcHsLiftedSigType ty = kcLiftedType ty `thenTc_` tcHsType ty
 
 tcHsType    ::            RenamedHsType -> TcM Type
 tcHsRecType :: RecFlag -> RenamedHsType -> TcM Type
   -- Don't do kind checking, but do hoist for-alls to the top
+  -- These are used in type and class decls, where kinding is
+  -- done in advance
 tcHsType             ty = tc_type NonRecursive ty  `thenTc` \ ty' ->  returnTc (hoistForAllTys ty')
 tcHsRecType wimp_out ty = tc_type wimp_out     ty  `thenTc` \ ty' ->  returnTc (hoistForAllTys ty')
+
+-- In interface files the type is already kinded,
+-- and we definitely don't want to hoist for-alls.
+-- Otherwise we'll change
+--     dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
+-- into 
+--     dmfail :: forall m:(*->*) a:* Monad m => String -> m a
+-- which definitely isn't right!
+tcIfaceType ty = tc_type NonRecursive ty
 \end{code}
 
 
@@ -360,7 +386,10 @@ tc_type wimp_out (HsFunTy ty1 ty2)
   = tc_type wimp_out ty1                       `thenTc` \ tau_ty1 ->
        -- Function argument can be polymorphic, but
        -- must not be an unboxed tuple
-    checkTc (not (isUnboxedTupleType tau_ty1))
+       --
+       -- In a recursive loop we can't ask whether the thing is
+       -- unboxed -- might be a synonym inside a synonym inside a group
+    checkTc (isRec wimp_out || not (isUnboxedTupleType tau_ty1))
            (ubxArgTyErr ty1)                   `thenTc_`
     tc_type wimp_out ty2                       `thenTc` \ tau_ty2 ->
     returnTc (mkFunTy tau_ty1 tau_ty2)
@@ -386,7 +415,7 @@ tc_type wimp_out full_ty@(HsForAllTy (Just tv_names) ctxt ty)
        kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
     in
     tcHsTyVars tv_names kind_check                     $ \ tyvars ->
-    tc_context wimp_out ctxt                           `thenTc` \ theta ->
+    tcRecTheta wimp_out ctxt                           `thenTc` \ theta ->
 
        -- Context behaves like a function type
        -- This matters.  Return-unboxed-tuple analysis can
@@ -422,9 +451,9 @@ tc_arg_type wimp_out arg_ty
   = tc_type wimp_out arg_ty
 
   | otherwise
-  = tc_type wimp_out arg_ty                                            `thenTc` \ arg_ty' ->
-    checkTc (not (isForAllTy arg_ty'))        (polyArgTyErr arg_ty)    `thenTc_`
-    checkTc (not (isUnboxedTupleType arg_ty')) (ubxArgTyErr arg_ty)    `thenTc_`
+  = tc_type wimp_out arg_ty                                                            `thenTc` \ arg_ty' ->
+    checkTc (isRec wimp_out || not (tcIsForAllTy arg_ty'))      (polyArgTyErr arg_ty)  `thenTc_`
+    checkTc (isRec wimp_out || not (isUnboxedTupleType arg_ty')) (ubxArgTyErr arg_ty)  `thenTc_`
     returnTc arg_ty'
 
 tc_arg_types wimp_out arg_tys = mapTc (tc_arg_type wimp_out) arg_tys
@@ -481,22 +510,17 @@ tc_fun_type name arg_tys
 Contexts
 ~~~~~~~~
 \begin{code}
-tcRecClassContext :: RecFlag -> RenamedContext -> TcM ClassContext
+tcRecTheta :: RecFlag -> RenamedContext -> TcM ThetaType
        -- Used when we are expecting a ClassContext (i.e. no implicit params)
-tcRecClassContext wimp_out context
-  = tc_context wimp_out context        `thenTc` \ theta ->
-    returnTc (classesOfPreds theta)
-
-tc_context :: RecFlag -> RenamedContext -> TcM ThetaType
-tc_context wimp_out context = mapTc (tc_pred wimp_out) context
+tcRecTheta wimp_out context = mapTc (tc_pred wimp_out) context
 
-tc_pred wimp_out assn@(HsPClass class_name tys)
+tc_pred wimp_out assn@(HsClassP class_name tys)
   = tcAddErrCtxt (appKindCtxt (ppr assn))      $
     tc_arg_types wimp_out tys                  `thenTc` \ arg_tys ->
     tcLookupGlobal class_name                  `thenTc` \ thing ->
     case thing of
        AClass clas -> checkTc (arity == n_tys) err     `thenTc_`
-                      returnTc (Class clas arg_tys)
+                      returnTc (ClassP clas arg_tys)
            where
                arity = classArity clas
                n_tys = length tys
@@ -504,7 +528,7 @@ tc_pred wimp_out assn@(HsPClass class_name tys)
 
        other -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
 
-tc_pred wimp_out assn@(HsPIParam name ty)
+tc_pred wimp_out assn@(HsIParam name ty)
   = tcAddErrCtxt (appKindCtxt (ppr assn))      $
     tc_arg_type wimp_out ty                    `thenTc` \ arg_ty ->
     returnTc (IParam name arg_ty)
@@ -559,18 +583,27 @@ checkAmbiguity wimp_out is_source_polytype forall_tyvars theta tau
     tau_vars         = tyVarsOfType tau
     extended_tau_vars = grow theta tau_vars
 
+       -- Hack alert.  If there are no tyvars, (ppr sigma_ty) will print
+       -- something strange like {Eq k} -> k -> k, because there is no
+       -- ForAll at the top of the type.  Since this is going to the user
+       -- we want it to look like a proper Haskell type even then; hence the hack
+       -- 
+       -- This shows up in the complaint about
+       --      case C a where
+       --        op :: Eq a => a -> a
+    ppr_sigma        | null forall_tyvars = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
+                     | otherwise          = ppr sigma_ty 
+
     is_ambig ct_var   = (ct_var `elem` forall_tyvars) &&
                        not (ct_var `elemVarSet` extended_tau_vars)
     is_free ct_var    = not (ct_var `elem` forall_tyvars)
     
-    check_pred pred = checkTc (not any_ambig)              (ambigErr pred sigma_ty) `thenTc_`
-                     checkTc (is_ip pred || not all_free) (freeErr  pred sigma_ty)
+    check_pred pred = checkTc (not any_ambig)                 (ambigErr pred ppr_sigma) `thenTc_`
+                     checkTc (isIPPred pred || not all_free) (freeErr  pred ppr_sigma)
              where 
                ct_vars   = varSetElems (tyVarsOfPred pred)
                all_free  = all is_free ct_vars
                any_ambig = is_source_polytype && any is_ambig ct_vars
-               is_ip (IParam _ _) = True
-               is_ip _            = False
 \end{code}
 
 %************************************************************************
@@ -649,7 +682,7 @@ tcTySig (Sig v ty src_loc)
  = tcAddSrcLoc src_loc                         $ 
    tcAddErrCtxt (tcsigCtxt v)                  $
    tcHsSigType ty                              `thenTc` \ sigma_tc_ty ->
-   mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig -> 
+   mkTcSig (mkLocalId v sigma_tc_ty) src_loc   `thenNF_Tc` \ sig -> 
    returnTc sig
 
 mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
@@ -662,16 +695,17 @@ mkTcSig poly_id src_loc
        -- typechecking the rest of the program with the function bound
        -- to a pristine type, namely sigma_tc_ty
    let
-       (tyvars, rho) = splitForAllTys (idType poly_id)
+       (tyvars, rho) = tcSplitForAllTys (idType poly_id)
    in
-   mapNF_Tc tcInstSigVar tyvars                `thenNF_Tc` \ tyvars' ->
+   tcInstSigVars tyvars                        `thenNF_Tc` \ tyvars' ->
        -- Make *signature* type variables
 
    let
      tyvar_tys' = mkTyVarTys tyvars'
      rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
        -- mkTopTyVarSubst because the tyvars' are fresh
-     (theta', tau') = splitRhoTy rho'
+
+     (theta', tau') = tcSplitRhoTy rho'
        -- This splitRhoTy tries hard to make sure that tau' is a type synonym
        -- wherever possible, which can improve interface files.
    in
@@ -766,7 +800,7 @@ checkSigTyVars sig_tyvars free_tyvars
     checkTcM (allDistinctTyVars sig_tys globals)
             (complain sig_tys globals) `thenTc_`
 
-    returnTc (map (getTyVar "checkSigTyVars") sig_tys)
+    returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
 
   where
     complain sig_tys globals
@@ -782,7 +816,7 @@ checkSigTyVars sig_tyvars free_tyvars
        let
            in_scope_assoc = [ (zonked_tv, in_scope_tv) 
                             | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
-                              Just zonked_tv <- [getTyVar_maybe z_ty]
+                              Just zonked_tv <- [tcGetTyVar_maybe z_ty]
                             ]
            in_scope_env = mkVarEnv in_scope_assoc
        in
@@ -804,17 +838,19 @@ checkSigTyVars sig_tyvars free_tyvars
                -- ty is what you get if you zonk sig_tyvar and then tidy it
                --
                -- acc maps a zonked type variable back to a signature type variable
-         = case getTyVar_maybe ty of {
+         = case tcGetTyVar_maybe ty of {
              Nothing ->                        -- Error (a)!
-                       returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
+                       returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
 
              Just tv ->
 
            case lookupVarEnv acc tv of {
                Just sig_tyvar' ->      -- Error (b) or (d)!
-                       returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
+                       returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
+                   where
+                       thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
 
-               Nothing ->
+             ; Nothing ->
 
            if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
                                        -- The least comprehensible, so put it last
@@ -898,7 +934,7 @@ escape_msg sig_tv tv globs frees
     vcat_first 0 (x:xs) = text "...others omitted..."
     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
 
-unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
+unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 \end{code}
 
@@ -961,16 +997,17 @@ wrongThingErr expected thing name
     pp_thing (ATcId _)           = ptext SLIT("Local identifier")
     pp_thing (AThing _)          = ptext SLIT("Utterly bogus")
 
-ambigErr pred ty
+ambigErr pred ppr_ty
   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
-        nest 4 (ptext SLIT("for the type:") <+> ppr ty),
+        nest 4 (ptext SLIT("for the type:") <+> ppr_ty),
         nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
                 ptext SLIT("must be reachable from the type after the =>"))]
 
-freeErr pred ty
-  = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
-                  ptext SLIT("does not mention any of the universally quantified type variables"),
-        nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
+freeErr pred ppr_ty
+  = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
+                  ptext SLIT("are already in scope"),
+        nest 4 (ptext SLIT("At least one must be universally quantified here")),
+        ptext SLIT("In the type") <+> quotes ppr_ty
     ]
 
 polyArgTyErr ty = ptext SLIT("Illegal polymorphic type as argument:")   <+> ppr ty