FIX Trac #1901: check no existential context in H98 mode
[ghc-hetmet.git] / compiler / typecheck / TcTyClsDecls.lhs
index 8af4e85..3880f1f 100644 (file)
@@ -6,6 +6,13 @@
 TcTyClsDecls: Typecheck type and class declarations
 
 \begin{code}
+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
 module TcTyClsDecls (
        tcTyAndClassDecls, tcFamInstDecl
     ) where
@@ -133,8 +140,12 @@ indeed type families).  I think.
 tcTyAndClassDecls :: ModDetails -> [LTyClDecl Name]
                   -> TcM TcGblEnv      -- Input env extended by types and classes 
                                        -- and their implicit Ids,DataCons
+-- Fails if there are any errors
+
 tcTyAndClassDecls boot_details allDecls
-  = do {       -- Omit instances of type families; they are handled together
+  = checkNoErrs $      -- The code recovers internally, but if anything gave rise to
+                       -- an error we'd better stop now, to avoid a cascade
+    do {       -- Omit instances of type families; they are handled together
                -- with the *heads* of class instances
         ; let decls = filter (not . isFamInstDecl . unLoc) allDecls
 
@@ -240,7 +251,7 @@ tcFamInstDecl (L loc decl)
     recoverM (returnM Nothing)                 $
     setSrcSpan loc                             $
     tcAddDeclCtxt decl                         $
-    do { -- type families require -ftype-families and can't be in an
+    do { -- type families require -XTypeFamilies and can't be in an
         -- hs-boot file
        ; type_families <- doptM Opt_TypeFamilies
        ; is_boot  <- tcIsHsBoot          -- Are we compiling an hs-boot file?
@@ -263,19 +274,20 @@ tcFamInstDecl1 (decl@TySynonym {tcdLName = L loc tc_name})
        ; -- (1) kind check the right-hand side of the type equation
        ; k_rhs <- kcCheckHsType (tcdSynRhs decl) resKind
 
+         -- we need the exact same number of type parameters as the family
+         -- declaration 
+       ; let famArity = tyConArity family
+       ; checkTc (length k_typats == famArity) $ 
+           wrongNumberOfParmsErr famArity
+
          -- (2) type check type equation
        ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
        ; t_typats <- mappM tcHsKindedType k_typats
        ; t_rhs    <- tcHsKindedType k_rhs
 
          -- (3) check that 
-         --     - left-hand side contains no type family applications
-         --       (vanilla synonyms are fine, though)
-       ; mappM_ checkTyFamFreeness t_typats
-
-         --     - the right-hand side is a tau type
-       ; unless (isTauTy t_rhs) $ 
-          addErr (polyTyErr t_rhs)
+         --     - check the well-formedness of the instance
+       ; checkValidTypeInst t_typats t_rhs
 
          -- (4) construct representation tycon
        ; rep_tc_name <- newFamInstTyConName tc_name loc
@@ -299,7 +311,7 @@ tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
             k_cons = tcdCons k_decl
 
          -- result kind must be '*' (otherwise, we have too few patterns)
-       ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr tc_name
+       ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr (tyConArity family)
 
          -- (2) type check indexed data type declaration
        ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
@@ -311,7 +323,8 @@ tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
 
          -- (3) Check that
          --     - left-hand side contains no type family applications
-         --       (vanilla synonyms are fine, though)
+         --       (vanilla synonyms are fine, though, and we checked for
+         --       foralls earlier)
        ; mappM_ checkTyFamFreeness t_typats
 
         --     - we don't use GADT syntax for indexed types
@@ -323,13 +336,14 @@ tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
 
          -- (4) construct representation tycon
        ; rep_tc_name <- newFamInstTyConName tc_name loc
+       ; let ex_ok = True      -- Existentials ok for type families!
        ; tycon <- fixM (\ tycon -> do 
-            { data_cons <- mappM (addLocM (tcConDecl unbox_strict tycon t_tvs))
+            { data_cons <- mappM (addLocM (tcConDecl unbox_strict ex_ok tycon t_tvs))
                                  k_cons
             ; tc_rhs <-
                 case new_or_data of
                   DataType -> return (mkDataTyConRhs data_cons)
-                  NewType  -> ASSERT( isSingleton data_cons )
+                  NewType  -> ASSERT( not (null data_cons) )
                               mkNewTyConRhs rep_tc_name tycon (head data_cons)
             ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
                             False h98_syntax (Just (family, t_typats))
@@ -348,27 +362,6 @@ tcFamInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
                        L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
                        other -> True
 
--- Check that a type index does not contain any type family applications
---
--- * Earlier phases have already checked that there are no foralls in the
---   type; we also cannot have PredTys and NoteTys are being skipped by using
---   the core view. 
---
-checkTyFamFreeness :: Type -> TcM ()
-checkTyFamFreeness ty | Just (tycon, tys) <- splitTyConApp_maybe ty
-                      = if isSynTyCon tycon 
-                        then addErr $ tyFamAppInIndexErr ty
-                        else mappM_ checkTyFamFreeness tys
-                          -- splitTyConApp_maybe uses the core view; hence,
-                          -- any synonym tycon must be a family tycon
-
-                      | Just (ty1, ty2) <- splitAppTy_maybe ty
-                      = checkTyFamFreeness ty1 >> checkTyFamFreeness ty2
-
-                      | otherwise          -- only vars remaining
-                      = return ()
-
-
 -- Kind checking of indexed types
 -- -
 
@@ -678,14 +671,14 @@ tcTyClDecl1 _calc_isrec
   { traceTc (text "type family: " <+> ppr tc_name) 
   ; idx_tys <- doptM Opt_TypeFamilies
 
-       -- Check that we don't use families without -ftype-families
+       -- Check that we don't use families without -XTypeFamilies
   ; checkTc idx_tys $ badFamInstDecl tc_name
 
   ; tycon <- buildSynTyCon tc_name tvs' (OpenSynTyCon kind Nothing) Nothing
   ; return [ATyCon tycon]
   }
 
-  -- "newtype family" or "data family" declaration
+  -- "data family" declaration
 tcTyClDecl1 _calc_isrec 
   (TyFamily {tcdFlavour = DataFamily, 
             tcdLName = L _ tc_name, tcdTyVars = tvs, tcdKind = mb_kind})
@@ -696,7 +689,7 @@ tcTyClDecl1 _calc_isrec
 
   ; idx_tys <- doptM Opt_TypeFamilies
 
-       -- Check that we don't use families without -ftype-families
+       -- Check that we don't use families without -XTypeFamilies
   ; checkTc idx_tys $ badFamInstDecl tc_name
 
   ; tycon <- buildAlgTyCon tc_name final_tvs [] 
@@ -705,6 +698,7 @@ tcTyClDecl1 _calc_isrec
   }
 
   -- "newtype" and "data"
+  -- NB: not used for newtype/data instances (whether associated or not)
 tcTyClDecl1 calc_isrec
   (TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
           tcdLName = L _ tc_name, tcdKindSig = mb_ksig, tcdCons = cons})
@@ -716,8 +710,10 @@ tcTyClDecl1 calc_isrec
   ; unbox_strict <- doptM Opt_UnboxStrictFields
   ; empty_data_decls <- doptM Opt_EmptyDataDecls
   ; kind_signatures <- doptM Opt_KindSignatures
+  ; existential_ok <- doptM Opt_ExistentialQuantification
   ; gadt_ok      <- doptM Opt_GADTs
   ; is_boot     <- tcIsHsBoot  -- Are we compiling an hs-boot file?
+  ; let ex_ok = existential_ok || gadt_ok      -- Data cons can have existential context
 
        -- Check that we don't use GADT syntax in H98 world
   ; checkTc (gadt_ok || h98_syntax) (badGadtDecl tc_name)
@@ -738,7 +734,7 @@ tcTyClDecl1 calc_isrec
            (newtypeConError tc_name (length cons))
 
   ; tycon <- fixM (\ tycon -> do 
-       { data_cons <- mappM (addLocM (tcConDecl unbox_strict tycon final_tvs)) 
+       { data_cons <- mappM (addLocM (tcConDecl unbox_strict ex_ok tycon final_tvs)) 
                             cons
        ; tc_rhs <-
            if null cons && is_boot     -- In a hs-boot file, empty cons means
@@ -746,7 +742,7 @@ tcTyClDecl1 calc_isrec
            else case new_or_data of
                   DataType -> return (mkDataTyConRhs data_cons)
                   NewType  -> 
-                       ASSERT( isSingleton data_cons )
+                       ASSERT( not (null data_cons) )
                        mkNewTyConRhs tc_name tycon (head data_cons)
        ; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
            (want_generic && canDoGenerics data_cons) h98_syntax Nothing
@@ -767,6 +763,8 @@ tcTyClDecl1 calc_isrec
   { ctxt' <- tcHsKindedContext ctxt
   ; fds' <- mappM (addLocM tc_fundep) fundeps
   ; atss <- mappM (addLocM (tcTyClDecl1 (const Recursive))) ats
+            -- NB: 'ats' only contains "type family" and "data family"
+            --     declarations as well as type family defaults
   ; let ats' = zipWith setTyThingPoss atss (map (tcdTyVars . unLoc) ats)
   ; sig_stuff <- tcClassSigs class_name sigs meths
   ; clas <- fixM (\ clas ->
@@ -807,14 +805,17 @@ tcTyClDecl1 calc_isrec
 
 -----------------------------------
 tcConDecl :: Bool              -- True <=> -funbox-strict_fields
+         -> Bool               -- True <=> -XExistentialQuantificaton or -XGADTs
          -> TyCon -> [TyVar] 
          -> ConDecl Name 
          -> TcM DataCon
 
-tcConDecl unbox_strict tycon tc_tvs    -- Data types
+tcConDecl unbox_strict existential_ok tycon tc_tvs     -- Data types
          (ConDecl name _ tvs ctxt details res_ty _)
   = tcTyVarBndrs tvs           $ \ tvs' -> do 
     { ctxt' <- tcHsKindedContext ctxt
+    ; checkTc (existential_ok || (null tvs && null (unLoc ctxt)))
+             (badExistential name)
     ; (univ_tvs, ex_tvs, eq_preds, data_tc) <- tcResultType tycon tc_tvs tvs' res_ty
     ; let 
        -- Tiresome: tidy the tyvar binders, since tc_tvs and tvs' may have the same OccNames
@@ -1066,14 +1067,14 @@ checkNewDataCon con
                -- One argument
        ; checkTc (null eq_spec) (newtypePredError con)
                -- Return type is (T a b c)
-       ; checkTc (null ex_tvs && null theta) (newtypeExError con)
+       ; checkTc (null ex_tvs && null eq_theta && null dict_theta) (newtypeExError con)
                -- No existentials
        ; checkTc (not (any isMarkedStrict (dataConStrictMarks con))) 
                  (newtypeStrictError con)
                -- No strictness
     }
   where
-    (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig con
+    (_univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _res_ty) = dataConFullSig con
 
 -------------------------------
 checkValidClass :: Class -> TcM ()
@@ -1109,6 +1110,7 @@ checkValidClass cls
                -- The 'tail' removes the initial (C a) from the
                -- class itself, leaving just the method type
 
+       ; traceTc (text "class op type" <+> ppr op_ty <+> ppr tau)
        ; checkValidType (FunSigCtxt op_name) tau
 
                -- Check that the type mentions at least one of
@@ -1210,6 +1212,11 @@ badGadtDecl tc_name
   = vcat [ ptext SLIT("Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
         , nest 2 (parens $ ptext SLIT("Use -XGADTs to allow GADTs")) ]
 
+badExistential con_name
+  = hang (ptext SLIT("Data constructor") <+> quotes (ppr con_name) <+>
+               ptext SLIT("has existential type variables, or a context, or both"))
+       2 (parens $ ptext SLIT("Use -XExistentialQuantification or -XGADTs to allow this"))
+
 badStupidTheta tc_name
   = ptext SLIT("A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
 
@@ -1252,9 +1259,13 @@ tooManyParmsErr tc_name
   = ptext SLIT("Family instance has too many parameters:") <+> 
     quotes (ppr tc_name)
 
-tooFewParmsErr tc_name
-  = ptext SLIT("Family instance has too few parameters:") <+> 
-    quotes (ppr tc_name)
+tooFewParmsErr arity
+  = ptext SLIT("Family instance has too few parameters; expected") <+> 
+    ppr arity
+
+wrongNumberOfParmsErr exp_arity
+  = ptext SLIT("Number of parameters must match family declaration; expected")
+    <+> ppr exp_arity
 
 badBootFamInstDeclErr = 
   ptext SLIT("Illegal family instance in hs-boot file")
@@ -1267,15 +1278,6 @@ wrongKindOfFamily family =
                 | isAlgTyCon family = ptext SLIT("data type")
                 | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
 
-polyTyErr ty 
-  = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $
-      ppr ty
-
-tyFamAppInIndexErr ty
-  = hang (ptext SLIT("Illegal type family application in type instance") <> 
-         colon) 4 $
-      ppr ty
-
 emptyConDeclsErr tycon
   = sep [quotes (ppr tycon) <+> ptext SLIT("has no constructors"),
         nest 2 $ ptext SLIT("(-XEmptyDataDecls permits this)")]