[project @ 2000-06-27 09:08:32 by lewie]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index 2745f78..2e6a570 100644 (file)
@@ -13,8 +13,8 @@ module TcMonoType ( tcHsType, tcHsSigType, tcHsTypeKind, tcHsTopType, tcHsTopBox
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsType(..), HsTyVar(..), MonoUsageAnn(..),
-                          Sig(..), HsPred(..), pprHsPred, pprParendHsType )
+import HsSyn           ( HsType(..), HsTyVarBndr(..), HsUsageAnn(..),
+                          Sig(..), HsPred(..), pprParendHsType, HsTupCon(..) )
 import RnHsSyn         ( RenamedHsType, RenamedContext, RenamedSig )
 import TcHsSyn         ( TcId )
 
@@ -28,19 +28,21 @@ import TcType               ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
                          newKindVar, tcInstSigVar,
                          zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType, zonkTcTyVar
                        )
-import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
+import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr,
+                         instFunDeps, instFunDepsOfTheta )
+import FunDeps         ( tyVarFunDep, oclose )
 import TcUnify         ( unifyKind, unifyKinds, unifyTypeKind )
 import Type            ( Type, PredType(..), ThetaType, UsageAnn(..),
                          mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
                           mkUsForAllTy, zipFunTys, hoistForAllTys,
                          mkSigmaTy, mkDictTy, mkPredTy, mkTyConApp,
                          mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
-                         boxedTypeKind, unboxedTypeKind, tyVarsOfType,
+                         boxedTypeKind, unboxedTypeKind, 
                          mkArrowKinds, getTyVar_maybe, getTyVar,
                          tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
-                         tyVarsOfType, tyVarsOfTypes, mkForAllTys
+                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, mkForAllTys
                        )
-import PprType         ( pprConstraint, pprType )
+import PprType         ( pprConstraint, pprType, pprPred )
 import Subst           ( mkTopTyVarSubst, substTy )
 import Id              ( mkVanillaId, idName, idType, idFreeTyVars )
 import Var             ( TyVar, mkTyVar, mkNamedUVar, varName )
@@ -48,14 +50,14 @@ import VarEnv
 import VarSet
 import Bag             ( bagToList )
 import ErrUtils                ( Message )
-import PrelInfo                ( cCallishClassKeys )
 import TyCon           ( TyCon )
 import Name            ( Name, OccName, isLocallyDefined )
-import TysWiredIn      ( mkListTy, mkTupleTy, mkUnboxedTupleTy )
+import TysWiredIn      ( mkListTy, mkTupleTy )
 import UniqFM          ( elemUFM, foldUFM )
+import BasicTypes      ( Boxity(..) )
 import SrcLoc          ( SrcLoc )
 import Unique          ( Unique, Uniquable(..) )
-import Util            ( mapAccumL, isSingleton )
+import Util            ( mapAccumL, isSingleton, removeDups )
 import Outputable
 \end{code}
 
@@ -153,49 +155,45 @@ tc_type ty
     returnTc tc_ty
 
 tc_type_kind :: RenamedHsType -> TcM s (TcKind, Type)
-tc_type_kind ty@(MonoTyVar name)
+tc_type_kind ty@(HsTyVar name)
   = tc_app ty []
 
-tc_type_kind (MonoListTy ty)
+tc_type_kind (HsListTy ty)
   = tc_boxed_type ty           `thenTc` \ tau_ty ->
     returnTc (boxedTypeKind, mkListTy tau_ty)
 
-tc_type_kind (MonoTupleTy tys True {-boxed-})
+tc_type_kind (HsTupleTy (HsTupCon _ Boxed) tys)
   = mapTc tc_boxed_type tys    `thenTc` \ tau_tys ->
-    returnTc (boxedTypeKind, mkTupleTy (length tys) tau_tys)
+    returnTc (boxedTypeKind, mkTupleTy Boxed (length tys) tau_tys)
 
-tc_type_kind (MonoTupleTy tys False {-unboxed-})
+tc_type_kind (HsTupleTy (HsTupCon _ Unboxed) tys)
   = mapTc tc_type tys                  `thenTc` \ tau_tys ->
-    returnTc (unboxedTypeKind, mkUnboxedTupleTy (length tys) tau_tys)
+    returnTc (unboxedTypeKind, mkTupleTy Unboxed (length tys) tau_tys)
 
-tc_type_kind (MonoFunTy ty1 ty2)
+tc_type_kind (HsFunTy ty1 ty2)
   = tc_type ty1        `thenTc` \ tau_ty1 ->
     tc_type ty2        `thenTc` \ tau_ty2 ->
     returnTc (boxedTypeKind, mkFunTy tau_ty1 tau_ty2)
 
-tc_type_kind (MonoTyApp ty1 ty2)
+tc_type_kind (HsAppTy ty1 ty2)
   = tc_app ty1 [ty2]
 
-tc_type_kind (MonoIParamTy n ty)
-  = tc_type ty `thenTc` \ tau ->
-    returnTc (boxedTypeKind, mkPredTy (IParam n tau))
+tc_type_kind (HsPredTy pred)
+  = tcClassAssertion True pred `thenTc` \ pred' ->
+    returnTc (boxedTypeKind, mkPredTy pred')
 
-tc_type_kind (MonoDictTy class_name tys)
-  = tcClassAssertion (HsPClass class_name tys) `thenTc` \ (Class clas arg_tys) ->
-    returnTc (boxedTypeKind, mkDictTy clas arg_tys)
-
-tc_type_kind (MonoUsgTy usg ty)
+tc_type_kind (HsUsgTy usg ty)
   = newUsg usg                          `thenTc` \ usg' ->
     tc_type_kind ty                     `thenTc` \ (kind, tc_ty) ->
     returnTc (kind, mkUsgTy usg' tc_ty)
   where
     newUsg usg = case usg of
-                   MonoUsOnce        -> returnTc UsOnce
-                   MonoUsMany        -> returnTc UsMany
-                   MonoUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
+                   HsUsOnce        -> returnTc UsOnce
+                   HsUsMany        -> returnTc UsMany
+                   HsUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
                                         returnTc (UsVar uv)
 
-tc_type_kind (MonoUsgForAllTy uv_name ty)
+tc_type_kind (HsUsgForAllTy uv_name ty)
   = let
         uv = mkNamedUVar uv_name
     in
@@ -204,10 +202,9 @@ tc_type_kind (MonoUsgForAllTy uv_name ty)
       returnTc (kind, mkUsForAllTy uv tc_ty)
 
 tc_type_kind (HsForAllTy (Just tv_names) context ty)
-  = tcExtendTyVarScope tv_names                $ \ tyvars ->
+  = tcExtendTyVarScope tv_names                $ \ forall_tyvars ->
     tcContext context                  `thenTc` \ theta ->
     tc_type_kind ty                    `thenTc` \ (kind, tau) ->
-    tcGetInScopeTyVars                 `thenTc` \ in_scope_vars ->
     let
        body_kind | null theta = kind
                  | otherwise  = boxedTypeKind
@@ -216,24 +213,67 @@ tc_type_kind (HsForAllTy (Just tv_names) context ty)
                -- give overloaded functions like
                --      f :: forall a. Num a => (# a->a, a->a #)
                -- And we want these to get through the type checker
-        check ct@(Class c tys) | ambiguous = failWithTc (ambigErr (c,tys) tau)
-         where ct_vars = tyVarsOfTypes tys
-               forall_tyvars = map varName in_scope_vars
-               tau_vars = tyVarsOfType tau
-               ambig ct_var = (varName ct_var `elem` forall_tyvars) &&
-                              not (ct_var `elemUFM` tau_vars)
-               ambiguous = foldUFM ((||) . ambig) False ct_vars
-       check _ = returnTc ()
+
+       -- Check for ambiguity
+       --   forall V. P => tau
+       -- is ambiguous if P contains generic variables
+       -- (i.e. one of the Vs) that are not mentioned in tau
+       --
+       -- However, we need to take account of functional dependencies
+       -- when we speak of 'mentioned in tau'.  Example:
+       --      class C a b | a -> b where ...
+       -- Then the type
+       --      forall x y. (C x y) => x
+       -- is not ambiguous because x is mentioned and x determines y
+       --
+       -- NOTE: In addition, GHC insists that at least one type variable
+       -- in each constraint is in V.  So we disallow a type like
+       --      forall a. Eq b => b -> b
+       -- even in a scope where b is in scope.
+       -- This is the is_free test below.
+
+       tau_vars            = tyVarsOfType tau
+       fds                 = instFunDepsOfTheta theta
+       tvFundep            = tyVarFunDep fds
+       extended_tau_vars   = oclose tvFundep tau_vars
+       is_ambig ct_var     = (ct_var `elem` forall_tyvars) &&
+                             not (ct_var `elemUFM` extended_tau_vars)
+       is_free ct_var      = not (ct_var `elem` forall_tyvars)
+
+       check_pred pred = checkTc (not any_ambig) (ambigErr pred ty) `thenTc_`
+                         checkTc (not all_free)  (freeErr  pred ty)
+             where 
+               ct_vars   = varSetElems (tyVarsOfPred pred)
+               any_ambig = is_source_polytype && any is_ambig ct_vars
+               all_free  = all is_free  ct_vars
+
+       -- Check ambiguity only for source-program types, not
+       -- for types coming from inteface files.  The latter can
+       -- legitimately have ambiguous types. Example
+       --    class S a where s :: a -> (Int,Int)
+       --    instance S Char where s _ = (1,1)
+       --    f:: S a => [a] -> Int -> (Int,Int)
+       --    f (_::[a]) x = (a*x,b)
+       --      where (a,b) = s (undefined::a)
+       -- Here the worker for f gets the type
+       --      fw :: forall a. S a => Int -> (# Int, Int #)
+       --
+       -- If the list of tv_names is empty, we have a monotype,
+       -- and then we don't need to check for ambiguity either,
+       -- because the test can't fail (see is_ambig).
+       is_source_polytype = case tv_names of
+                               (UserTyVar _ : _) -> True
+                               other             -> False
     in
-    mapTc check theta                  `thenTc_`
-    returnTc (body_kind, mkSigmaTy tyvars theta tau)
+    mapTc check_pred theta             `thenTc_`
+    returnTc (body_kind, mkSigmaTy forall_tyvars theta tau)
 \end{code}
 
 Help functions for type applications
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 \begin{code}
-tc_app (MonoTyApp ty1 ty2) tys
+tc_app (HsAppTy ty1 ty2) tys
   = tc_app ty1 (ty2:tys)
 
 tc_app ty tys
@@ -257,16 +297,16 @@ tc_app ty tys
 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 --     hence the rather strange functionality.
 
-tc_fun_type (MonoTyVar name) arg_tys
-  = tcLookupTy name                    `thenTc` \ (tycon_kind, maybe_arity, thing) ->
+tc_fun_type (HsTyVar name) arg_tys
+  = tcLookupTy name                    `thenTc` \ (tycon_kind, thing) ->
     case thing of
-       ATyVar tv   -> returnTc (tycon_kind, mkAppTys (mkTyVarTy tv) arg_tys)
-       AClass clas -> failWithTc (classAsTyConErr name)
-       ATyCon tc   -> case maybe_arity of
-                        Nothing ->     -- Data or newtype
-                                       returnTc (tycon_kind, mkTyConApp tc arg_tys)
+       ATyVar tv     -> returnTc (tycon_kind, mkAppTys (mkTyVarTy tv) arg_tys)
+       AClass clas _ -> failWithTc (classAsTyConErr name)
+
+       ADataTyCon tc ->  -- Data or newtype
+                         returnTc (tycon_kind, mkTyConApp tc arg_tys)
 
-                        Just arity ->  -- Type synonym
+       ASynTyCon tc arity ->   -- Type synonym
                                  checkTc (arity <= n_args) err_msg     `thenTc_`
                                  returnTc (tycon_kind, result_ty)
                           where
@@ -290,35 +330,14 @@ Contexts
 \begin{code}
 
 tcContext :: RenamedContext -> TcM s ThetaType
-tcContext context
-  =    --Someone discovered that @CCallable@ and @CReturnable@
-       -- could be used in contexts such as:
-       --      foo :: CCallable a => a -> PrimIO Int
-       -- Doing this utterly wrecks the whole point of introducing these
-       -- classes so we specifically check that this isn't being done.
-       --
-       -- We *don't* do this check in tcClassAssertion, because that's
-       -- called when checking a HsDictTy, and we don't want to reject
-       --      instance CCallable Int 
-       -- etc. Ugh!
-    mapTc check_naughty context `thenTc_`
-
-    mapTc tcClassAssertion context
-
- where
-   check_naughty (HsPClass class_name _) 
-     = checkTc (not (getUnique class_name `elem` cCallishClassKeys))
-              (naughtyCCallContextErr class_name)
-   check_naughty (HsPIParam _ _) = returnTc ()
-
-tcClassAssertion assn@(HsPClass class_name tys)
-  = tcAddErrCtxt (appKindCtxt (pprHsPred assn))        $
-    mapAndUnzipTc tc_type_kind tys     `thenTc` \ (arg_kinds, arg_tys) ->
-    tcLookupTy class_name              `thenTc` \ (kind, ~(Just arity), thing) ->
+tcContext context = mapTc (tcClassAssertion False) context
+
+tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
+  = tcAddErrCtxt (appKindCtxt (ppr assn))      $
+    mapAndUnzipTc tc_type_kind tys             `thenTc` \ (arg_kinds, arg_tys) ->
+    tcLookupTy class_name                      `thenTc` \ (kind, thing) ->
     case thing of
-       ATyVar  _   -> failWithTc (tyVarAsClassErr class_name)
-       ATyCon  _   -> failWithTc (tyConAsClassErr class_name)
-       AClass clas ->
+       AClass clas arity ->
                        -- Check with kind mis-match
                checkTc (arity == n_tys) err                            `thenTc_`
                unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)   `thenTc_`
@@ -326,8 +345,10 @@ tcClassAssertion assn@(HsPClass class_name tys)
            where
                n_tys = length tys
                err   = arityErr "Class" class_name arity n_tys
-tcClassAssertion assn@(HsPIParam name ty)
-  = tcAddErrCtxt (appKindCtxt (pprHsPred assn))        $
+       other -> failWithTc (tyVarAsClassErr class_name)
+
+tcClassAssertion ccall_ok assn@(HsPIParam name ty)
+  = tcAddErrCtxt (appKindCtxt (ppr assn))      $
     tc_type_kind ty    `thenTc` \ (arg_kind, arg_ty) ->
     returnTc (IParam name arg_ty)
 \end{code}
@@ -340,7 +361,7 @@ tcClassAssertion assn@(HsPIParam name ty)
 %************************************************************************
 
 \begin{code}
-tcExtendTopTyVarScope :: TcKind -> [HsTyVar Name]
+tcExtendTopTyVarScope :: TcKind -> [HsTyVarBndr Name]
                      -> ([TcTyVar] -> TcKind -> TcM s a)
                      -> TcM s a
 tcExtendTopTyVarScope kind tyvar_names thing_inside
@@ -354,14 +375,14 @@ tcExtendTopTyVarScope kind tyvar_names thing_inside
     mk_tv (IfaceTyVar name _, kind) = mkTyVar name kind
        -- NB: immutable tyvars, but perhaps with mutable kinds
 
-tcExtendTyVarScope :: [HsTyVar Name] 
+tcExtendTyVarScope :: [HsTyVarBndr Name] 
                   -> ([TcTyVar] -> TcM s a) -> TcM s a
 tcExtendTyVarScope tv_names thing_inside
   = mapNF_Tc tcHsTyVar tv_names        `thenNF_Tc` \ tyvars ->
     tcExtendTyVarEnv tyvars            $
     thing_inside tyvars
     
-tcHsTyVar :: HsTyVar Name -> NF_TcM s TcTyVar
+tcHsTyVar :: HsTyVarBndr Name -> NF_TcM s TcTyVar
 tcHsTyVar (UserTyVar name)       = newKindVar          `thenNF_Tc` \ kind ->
                                   tcNewMutTyVar name kind
        -- NB: mutable kind => mutable tyvar, so that zonking can bind
@@ -369,7 +390,7 @@ tcHsTyVar (UserTyVar name)       = newKindVar               `thenNF_Tc` \ kind ->
 
 tcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (mkTyVar name (kindToTcKind kind))
 
-kcHsTyVar :: HsTyVar name -> NF_TcM s TcKind
+kcHsTyVar :: HsTyVarBndr name -> NF_TcM s TcKind
 kcHsTyVar (UserTyVar name)       = newKindVar
 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (kindToTcKind kind)
 \end{code}
@@ -406,7 +427,7 @@ data TcSigInfo
                                -- Does *not* have name = N
                                -- Has type tau
 
-       Inst                    -- Empty if theta is null, or 
+       [Inst]                  -- Empty if theta is null, or
                                -- (method mono_id) otherwise
 
        SrcLoc                  -- Of the signature
@@ -428,7 +449,8 @@ maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 tcTySig :: RenamedSig -> TcM s TcSigInfo
 
 tcTySig (Sig v ty src_loc)
- = tcAddSrcLoc 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 -> 
    returnTc sig
@@ -461,8 +483,9 @@ mkTcSig poly_id src_loc
                tyvar_tys'
                theta' tau'                     `thenNF_Tc` \ inst ->
        -- We make a Method even if it's not overloaded; no harm
+   instFunDeps SignatureOrigin theta'          `thenNF_Tc` \ fds ->
        
-   returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) inst src_loc)
+   returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
   where
     name = idName poly_id
 \end{code}
@@ -716,9 +739,7 @@ sigPatCtxt bound_tvs bound_ids tidy_env
 %************************************************************************
 
 \begin{code}
-naughtyCCallContextErr clas_name
-  = sep [ptext SLIT("Can't use class") <+> quotes (ppr clas_name), 
-        ptext SLIT("in a context")]
+tcsigCtxt v   = ptext SLIT("In a type signature for") <+> quotes (ppr v)
 
 typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
 
@@ -739,8 +760,14 @@ tyConAsClassErr name
 tyVarAsClassErr name
   = ptext SLIT("Type variable used as a class:") <+> ppr name
 
-ambigErr (c, ts) ty
-  = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprConstraint c ts),
+ambigErr pred ty
+  = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
         nest 4 (ptext SLIT("for the type:") <+> ppr ty),
-        nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>."))]
+        nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear 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))
+    ]
 \end{code}