[project @ 2001-05-22 13:43:14 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index c86db59..bc42127 100644 (file)
@@ -6,12 +6,13 @@
 \begin{code}
 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
@@ -30,7 +31,7 @@ import TcEnv          ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
                          TyThing(..), TcTyThing(..), tcExtendKindEnv
                        )
 import TcType          ( TcKind, TcTyVar, TcThetaType, TcTauType,
-                         newKindVar, tcInstSigVar,
+                         newKindVar, tcInstSigVars,
                          zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar
                        )
 import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
@@ -46,9 +47,9 @@ import Type           ( Type, Kind, PredType(..), ThetaType, SigmaType, TauType,
                          mkArrowKinds, getTyVar_maybe, getTyVar, splitFunTy_maybe,
                          tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
                          tyVarsOfType, tyVarsOfPred, mkForAllTys,
-                         classesOfPreds, isUnboxedTupleType, isForAllTy
+                         isUnboxedTupleType, isForAllTy, isIPPred
                        )
-import PprType         ( pprType, pprPred )
+import PprType         ( pprType, pprTheta, pprPred )
 import Subst           ( mkTopTyVarSubst, substTy )
 import CoreFVs         ( idFreeTyVars )
 import Id              ( mkLocalId, idName, idType )
@@ -57,7 +58,7 @@ 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
 
 ---------------------------
@@ -241,11 +253,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 ->
@@ -371,7 +383,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)
@@ -397,7 +412,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
@@ -433,9 +448,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 (isForAllTy 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
@@ -492,22 +507,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
@@ -515,7 +525,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)
@@ -570,18 +580,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}
 
 %************************************************************************
@@ -675,7 +694,7 @@ mkTcSig poly_id src_loc
    let
        (tyvars, rho) = splitForAllTys (idType poly_id)
    in
-   mapNF_Tc tcInstSigVar tyvars                `thenNF_Tc` \ tyvars' ->
+   tcInstSigVars tyvars                        `thenNF_Tc` \ tyvars' ->
        -- Make *signature* type variables
 
    let
@@ -817,15 +836,17 @@ checkSigTyVars sig_tyvars free_tyvars
                -- acc maps a zonked type variable back to a signature type variable
          = case getTyVar_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
@@ -909,7 +930,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}
 
@@ -972,16 +993,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