Add HsCoreTy to HsType
[ghc-hetmet.git] / compiler / typecheck / TcHsType.lhs
index b7cbc1e..fcf329b 100644 (file)
@@ -6,7 +6,7 @@
 
 \begin{code}
 module TcHsType (
-       tcHsSigType, tcHsDeriv, 
+       tcHsSigType, tcHsSigTypeNC, tcHsDeriv, 
        tcHsInstHead, tcHsQuantifiedType,
        UserTypeCtxt(..), 
 
@@ -16,7 +16,7 @@ module TcHsType (
        
                -- Typechecking kinded types
        tcHsKindedContext, tcHsKindedType, tcHsBangType,
-       tcTyVarBndrs, dsHsType, tcLHsConResTy,
+       tcTyVarBndrs, dsHsType, 
        tcDataKindSig, ExpKind(..), EkCtxt(..),
 
                -- Pattern type signatures
@@ -25,6 +25,10 @@ module TcHsType (
 
 #include "HsVersions.h"
 
+#ifdef GHCI    /* Only if bootstrapped */
+import {-# SOURCE #-}  TcSplice( kcSpliceType )
+#endif
+
 import HsSyn
 import RnHsSyn
 import TcRnMonad
@@ -35,21 +39,20 @@ import TcIface
 import TcType
 import {- Kind parts of -} Type
 import Var
+import VarSet
 import Coercion
 import TyCon
 import Class
 import Name
-import OccName
 import NameSet
 import PrelNames
 import TysWiredIn
 import BasicTypes
 import SrcLoc
+import Util
 import UniqSupply
 import Outputable
 import FastString
-
-import Control.Monad
 \end{code}
 
 
@@ -136,14 +139,19 @@ the TyCon being defined.
 %************************************************************************
 
 \begin{code}
-tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
+tcHsSigType, tcHsSigTypeNC :: UserTypeCtxt -> LHsType Name -> TcM Type
   -- Do kind checking, and hoist for-alls to the top
   -- NB: it's important that the foralls that come from the top-level
   --    HsForAllTy in hs_ty occur *first* in the returned type.
   --     See Note [Scoped] with TcSigInfo
 tcHsSigType ctxt hs_ty 
   = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
-    do { kinded_ty <- kcTypeType hs_ty
+    tcHsSigTypeNC ctxt hs_ty
+
+tcHsSigTypeNC ctxt hs_ty
+  = do { (kinded_ty, _kind) <- kc_lhs_type hs_ty
+         -- The kind is checked by checkValidType, and isn't necessarily
+         -- of kind * in a Template Haskell quote eg [t| Maybe |]
        ; ty <- tcHsKindedType kinded_ty
        ; checkValidType ctxt ty        
        ; return ty }
@@ -151,10 +159,26 @@ tcHsSigType ctxt hs_ty
 tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Type)
 -- Typecheck an instance head.  We can't use 
 -- tcHsSigType, because it's not a valid user type.
-tcHsInstHead hs_ty
-  = do { kinded_ty <- kcHsSigType hs_ty
-       ; poly_ty   <- tcHsKindedType kinded_ty
-       ; return (tcSplitSigmaTy poly_ty) }
+tcHsInstHead (L loc ty)
+  = setSrcSpan loc   $ -- No need for an "In the type..." context
+    tc_inst_head ty     -- because that comes from the caller
+  where
+    -- tc_inst_head expects HsPredTy, which isn't usually even allowed
+    tc_inst_head (HsPredTy pred)
+      = do { pred'  <- kcHsPred pred
+          ; pred'' <- dsHsPred pred'
+           ; return ([], [], mkPredTy pred'') }
+
+    tc_inst_head (HsForAllTy _ tvs ctxt (L _ (HsPredTy pred)))
+      = kcHsTyVars tvs    $ \ tvs' ->
+       do { ctxt' <- kcHsContext ctxt
+          ; pred' <- kcHsPred    pred
+          ; tcTyVarBndrs tvs'  $ \ tvs'' ->
+       do { ctxt'' <- mapM dsHsLPred (unLoc ctxt')
+          ; pred'' <- dsHsPred pred'
+          ; return (tvs'', ctxt'', mkPredTy pred'') } }
+
+    tc_inst_head _ = failWithTc (ptext (sLit "Malformed instance type"))
 
 tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
 -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
@@ -275,11 +299,6 @@ kc_check_hs_type ty@(HsAppTy ty1 ty2) exp_kind
        ; arg_tys' <- kcCheckApps fun_ty fun_kind arg_tys ty exp_kind
        ; return (mkHsAppTys fun_ty' arg_tys') }
 
-kc_check_hs_type ty@(HsPredTy (HsClassP cls tys)) exp_kind
-  = do { cls_kind <- kcClass cls
-       ; tys' <- kcCheckApps cls cls_kind tys ty exp_kind
-       ; return (HsPredTy (HsClassP cls tys')) }
-
 -- This is the general case: infer the kind and compare
 kc_check_hs_type ty exp_kind
   = do { (ty', act_kind) <- kc_hs_type ty
@@ -298,7 +317,6 @@ kc_check_hs_type ty exp_kind
     strip (HsBangTy _ (L _ ty))       = strip ty
     strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
     strip ty                         = ty
-
 \end{code}
 
        Here comes the main function
@@ -373,12 +391,11 @@ kc_hs_type (HsAppTy ty1 ty2) = do
   where
     (fun_ty, arg_tys) = splitHsAppTys ty1 ty2
 
-kc_hs_type (HsPredTy (HsEqualP _ _))
-  = wrongEqualityErr
+kc_hs_type (HsPredTy pred)
+  = wrongPredErr pred
 
-kc_hs_type (HsPredTy pred) = do
-    pred' <- kcHsPred pred
-    return (HsPredTy pred', liftedTypeKind)
+kc_hs_type (HsCoreTy ty)
+  = return (HsCoreTy ty, typeKind ty)
 
 kc_hs_type (HsForAllTy exp tv_names context ty)
   = kcHsTyVars tv_names         $ \ tv_names' ->
@@ -395,12 +412,22 @@ kc_hs_type (HsForAllTy exp tv_names context ty)
 
        ; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }
 
-kc_hs_type (HsBangTy b ty) = do
-    (ty', kind) <- kc_lhs_type ty
-    return (HsBangTy b ty', kind)
+kc_hs_type (HsBangTy b ty)
+  = do { (ty', kind) <- kc_lhs_type ty
+       ; return (HsBangTy b ty', kind) }
+
+kc_hs_type ty@(HsRecTy _)
+  = failWithTc (ptext (sLit "Unexpected record type") <+> ppr ty)
+      -- Record types (which only show up temporarily in constructor signatures) 
+      -- should have been removed by now
 
-kc_hs_type ty@(HsSpliceTy _)
-  = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
+#ifdef GHCI    /* Only if bootstrapped */
+kc_hs_type (HsSpliceTy sp fvs _) = kcSpliceType sp fvs
+#else
+kc_hs_type ty@(HsSpliceTy {}) = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
+#endif
+
+kc_hs_type (HsQuasiQuoteTy {}) = panic "kc_hs_type"    -- Eliminated by renamer
 
 -- remove the doc nodes here, no need to worry about the location since
 -- its the same for a doc node and it's child type node
@@ -542,9 +569,12 @@ ds_type ty@(HsTyVar _)
 ds_type (HsParTy ty)           -- Remove the parentheses markers
   = dsHsType ty
 
-ds_type ty@(HsBangTy _ _)      -- No bangs should be here
+ds_type ty@(HsBangTy {})    -- No bangs should be here
   = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
 
+ds_type ty@(HsRecTy {})            -- No bangs should be here
+  = failWithTc (ptext (sLit "Unexpected record type:") <+> ppr ty)
+
 ds_type (HsKindSig ty _)
   = dsHsType ty        -- Kind checking done already
 
@@ -593,11 +623,16 @@ ds_type (HsForAllTy _ tv_names ctxt ty)
     tau <- dsHsType ty
     return (mkSigmaTy tyvars theta tau)
 
-ds_type (HsSpliceTy {}) = panic "ds_type: HsSpliceTy"
-
 ds_type (HsDocTy ty _)  -- Remove the doc comment
   = dsHsType ty
 
+ds_type (HsSpliceTy _ _ kind) 
+  = do { kind' <- zonkTcKindToKind kind
+       ; newFlexiTyVarTy kind' }
+
+ds_type (HsQuasiQuoteTy {}) = panic "ds_type"  -- Eliminated by renamer
+ds_type (HsCoreTy ty)       = return ty
+
 dsHsTypes :: [LHsType Name] -> TcM [Type]
 dsHsTypes arg_tys = mapM dsHsType arg_tys
 \end{code}
@@ -651,35 +686,7 @@ dsHsPred (HsIParam name ty)
        }
 \end{code}
 
-GADT constructor signatures
-
 \begin{code}
-tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
-tcLHsConResTy (L span res_ty)
-  = setSrcSpan span $
-    case get_args res_ty [] of
-          (HsTyVar tc_name, args) 
-             -> do { args' <- mapM dsHsType args
-                   ; thing <- tcLookup tc_name
-                   ; case thing of
-                       AGlobal (ATyCon tc) -> return (tc, args')
-                       _ -> failWithTc (badGadtDecl res_ty) }
-          _ -> failWithTc (badGadtDecl res_ty)
-  where
-       -- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe
-       -- because that causes a black hole, and for good reason.  Building
-       -- the type means expanding type synonyms, and we can't do that
-       -- inside the "knot".  So we have to work by steam.
-    get_args (HsAppTy (L _ fun) arg)   args = get_args fun (arg:args)
-    get_args (HsParTy (L _ ty))        args = get_args ty  args
-    get_args (HsOpTy ty1 (L _ tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
-    get_args ty                        args = (ty, args)
-
-badGadtDecl :: HsType Name -> SDoc
-badGadtDecl ty
-  = hang (ptext (sLit "Malformed constructor result type:"))
-       2 (ppr ty)
-
 addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
        -- Wrap a context around only if we want to show that contexts.  
 addKcTypeCtxt (L _ (HsPredTy _)) thing = thing
@@ -702,14 +709,14 @@ kcHsTyVars :: [LHsTyVarBndr Name]
           -> ([LHsTyVarBndr Name] -> TcM r)    -- These binders are kind-annotated
                                                -- They scope over the thing inside
           -> TcM r
-kcHsTyVars tvs thing_inside  = do
-    bndrs <- mapM (wrapLocM kcHsTyVar) tvs
-    tcExtendKindEnvTvs bndrs (thing_inside bndrs)
+kcHsTyVars tvs thing_inside
+  = do { kinded_tvs <- mapM (wrapLocM kcHsTyVar) tvs
+       ; tcExtendKindEnvTvs kinded_tvs thing_inside }
 
 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
        -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it      
-kcHsTyVar (UserTyVar name)        = KindedTyVar name <$> newKindVar
-kcHsTyVar (KindedTyVar name kind) = return (KindedTyVar name kind)
+kcHsTyVar (UserTyVar name _)  = UserTyVar name <$> newKindVar
+kcHsTyVar tv@(KindedTyVar {}) = return tv
 
 ------------------
 tcTyVarBndrs :: [LHsTyVarBndr Name]    -- Kind-annotated binders, which need kind-zonking
@@ -721,10 +728,9 @@ tcTyVarBndrs bndrs thing_inside = do
     tyvars <- mapM (zonk . unLoc) bndrs
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
   where
-    zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
-                                     ; return (mkTyVar name kind') }
-    zonk (UserTyVar name) = WARN( True, ptext (sLit "Un-kinded tyvar") <+> ppr name )
-                           return (mkTyVar name liftedTypeKind)
+    zonk (UserTyVar name kind) = do { kind' <- zonkTcKindToKind kind
+                                   ; return (mkTyVar name kind') }
+    zonk (KindedTyVar name kind) = return (mkTyVar name kind)
 
 -----------------------------------
 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
@@ -834,9 +840,9 @@ tcHsPatSigType ctxt hs_ty
                -- should be bound by the pattern signature
          in_scope <- getInLocalScope
        ; let span = getLoc hs_ty
-             sig_tvs = [ L span (UserTyVar n) 
-                       | n <- nameSetToList (extractHsTyVars hs_ty),
-                         not (in_scope n) ]
+             sig_tvs = userHsTyVarBndrs $ map (L span) $ 
+                       filterOut in_scope $
+                        nameSetToList (extractHsTyVars hs_ty)
 
        ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
        ; checkValidType ctxt sig_ty 
@@ -874,6 +880,16 @@ tcPatSig ctxt sig res_ty
                -- Check that pat_ty is rigid
        ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)
 
+               -- Check that all newly-in-scope tyvars are in fact
+               -- constrained by the pattern.  This catches tiresome
+               -- cases like   
+               --      type T a = Int
+               --      f :: Int -> Int
+               --      f (x :: T a) = ...
+               -- Here 'a' doesn't get a binding.  Sigh
+       ; let bad_tvs = filterOut (`elemVarSet` exactTyVarsOfType sig_ty) sig_tvs
+       ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
+
                -- Now match the pattern signature against res_ty
                -- For convenience, and uniform-looking error messages
                -- we do the matching by allocating meta type variables, 
@@ -1008,7 +1024,7 @@ checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
 
 \begin{code}
 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
-pprHsSigCtxt ctxt hs_ty = vcat [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon, 
+pprHsSigCtxt ctxt hs_ty = sep [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon, 
                                 nest 2 (pp_sig ctxt) ]
   where
     pp_sig (FunSigCtxt n)  = pp_n_colon n
@@ -1024,6 +1040,15 @@ wobblyPatSig sig_tvs
                <+> pprQuotedList sig_tvs)
        2 (ptext (sLit "unless the pattern has a rigid type context"))
                
+badPatSigTvs :: TcType -> [TyVar] -> SDoc
+badPatSigTvs sig_ty bad_tvs
+  = vcat [ fsep [ptext (sLit "The type variable") <> plural bad_tvs, 
+                 quotes (pprWithCommas ppr bad_tvs), 
+                ptext (sLit "should be bound by the pattern signature") <+> quotes (ppr sig_ty),
+                ptext (sLit "but are actually discarded by a type synonym") ]
+         , ptext (sLit "To fix this, expand the type synonym") 
+         , ptext (sLit "[Note: I hope to lift this restriction in due course]") ]
+
 scopedNonVar :: Name -> Type -> SDoc
 scopedNonVar n ty
   = vcat [sep [ptext (sLit "The scoped type variable") <+> quotes (ppr n),
@@ -1036,8 +1061,7 @@ dupInScope n n' _
        2 (vcat [ptext (sLit "are bound to the same type (variable)"),
                ptext (sLit "Distinct scoped type variables must be distinct")])
 
-wrongEqualityErr :: TcM (HsType Name, TcKind)
-wrongEqualityErr
-  = failWithTc (text "Equality predicate used as a type")
+wrongPredErr :: HsPred Name -> TcM (HsType Name, TcKind)
+wrongPredErr pred = failWithTc (text "Predicate used as a type:" <+> ppr pred)
 \end{code}