Merge branch 'no-pred-ty'
[ghc.git] / compiler / typecheck / TcTyClsDecls.lhs
index 0cc8835..b8a376b 100644 (file)
@@ -7,8 +7,13 @@ TcTyClsDecls: Typecheck type and class declarations
 
 \begin{code}
 module TcTyClsDecls (
-       tcTyAndClassDecls, kcDataDecl, tcConDecls, mkRecSelBinds,
-        checkValidTyCon, dataDeclChecks
+       tcTyAndClassDecls, mkRecSelBinds,
+
+       -- Functions used by TcInstDcls to check 
+       -- data/type family instance declarations
+        kcDataDecl, tcConDecls, dataDeclChecks, checkValidTyCon,
+        tcSynFamInstDecl, kcFamTyPats, 
+        wrongKindOfFamily, badATErr, wrongATArgErr
     ) where
 
 #include "HsVersions.h"
@@ -35,6 +40,7 @@ import IdInfo
 import Var
 import VarSet
 import Name
+import NameSet
 import NameEnv
 import Outputable
 import Maybes
@@ -406,8 +412,10 @@ kcFamilyDecl classTvs decl@(TyFamily {tcdKind = kind})
       | otherwise = return ()
     classTyKinds = [hsTyVarNameKind tv | L _ tv <- classTvs]
 
-kcFamilyDecl _ (TySynonym {})              -- type family defaults
-  = panic "TcTyClsDecls.kcFamilyDecl: not implemented yet"
+kcFamilyDecl _ decl@(TySynonym {})
+  = return decl
+   -- We don't have to do anything here for type family defaults:
+   -- tcClassATs will use tcAssocDecl to check them
 kcFamilyDecl _ d = pprPanic "kcFamilyDecl" (ppr d)
 \end{code}
 
@@ -508,19 +516,25 @@ tcTyClDecl1 _parent calc_isrec
 tcTyClDecl1 _parent calc_isrec 
   (ClassDecl {tcdLName = L _ class_tycon_name, tcdTyVars = tvs, 
              tcdCtxt = ctxt, tcdMeths = meths,
-             tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats} )
+             tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats, tcdATDefs = at_defs} )
   = ASSERT( isNoParent _parent )
     tcTyVarBndrs tvs           $ \ tvs' -> do 
   { ctxt' <- tcHsKindedContext ctxt
   ; fds' <- mapM (addLocM tc_fundep) fundeps
   ; (sig_stuff, gen_dm_env) <- tcClassSigs class_tycon_name sigs meths
   ; clas <- fixM $ \ clas -> do
-           { let tc_isrec = calc_isrec class_tycon_name
-           ; atss' <- mapM (addLocM $ tcTyClDecl1 (AssocFamilyTyCon clas) (const Recursive)) ats
-            -- NB: 'ats' only contains "type family" and "data family"
-            --     declarations as well as type family defaults
+           { let       -- This little knot is just so we can get
+                       -- hold of the name of the class TyCon, which we
+                       -- need to look up its recursiveness
+                   tycon_name = tyConName (classTyCon clas)
+                   tc_isrec = calc_isrec tycon_name
+            
+            ; at_stuff <- tcClassATs clas tvs' ats at_defs
+            -- NB: 'ats' only contains "type family" and "data family" declarations
+            -- and 'at_defs' only contains associated-type defaults
+            
             ; buildClass False {- Must include unfoldings for selectors -}
-                        class_tycon_name tvs' ctxt' fds' (concat atss')
+                        class_tycon_name tvs' ctxt' fds' at_stuff
                         sig_stuff tc_isrec }
 
   ; let gen_dm_ids = [ AnId (mkExportedLocalId gen_dm_name gen_dm_ty)
@@ -547,7 +561,175 @@ tcTyClDecl1 _ _
   = return [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0)]
 
 tcTyClDecl1 _ _ d = pprPanic "tcTyClDecl1" (ppr d)
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+               Typechecking associated types (in class decls)
+              (including the associated-type defaults)
+%*                                                                     *
+%************************************************************************
+
+Example:     class C a where
+               data D a 
+
+               type F a b :: *
+               type F a Z = [a]        -- Default
+               type F a (S n) = F a n  -- Default
+
+We can get default defns only for type families, not data families
+       
+\begin{code}
+tcClassATs :: Class            -- The class
+           -> [TyVar]          -- Class type variables (can't look them up in class b/c its knot-tied)
+           -> [LTyClDecl Name] -- Associated types. All FamTyCon
+           -> [LTyClDecl Name] -- Associated type defaults. All SynTyCon
+           -> TcM [ClassATItem]
+tcClassATs clas clas_tvs ats at_defs
+  = do {  -- Complain about associated type defaults for non associated-types
+         sequence_ [ failWithTc (badATErr clas n)
+                   | n <- map (tcdName . unLoc) at_defs
+                   , not (n `elemNameSet` at_names) ]
+       ; mapM tc_at ats }
+  where
+    at_names = mkNameSet (map (tcdName . unLoc) ats)
+
+    at_defs_map :: NameEnv [LTyClDecl Name]
+    -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
+    at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv (tcdName (unLoc at_def)) [at_def]) 
+                        emptyNameEnv at_defs
+
+    tc_at at = do { [ATyCon fam_tc] <- addLocM (tcTyClDecl1 (AssocFamilyTyCon clas) (const Recursive)) at
+                  ; atd <- mapM (tcDefaultAssocDecl fam_tc clas_tvs)
+                                (lookupNameEnv at_defs_map (tyConName fam_tc) `orElse` []) 
+                  ; return (fam_tc, atd) }
+
+
+-------------------------
+tcDefaultAssocDecl :: TyCon              -- ^ Family TyCon
+                   -> [TyVar]            -- ^ TyVars of associated type's class
+                   -> LTyClDecl Name     -- ^ RHS
+                   -> TcM ATDefault      -- ^ Type checked RHS and free TyVars
+tcDefaultAssocDecl fam_tc clas_tvs (L loc decl)
+  = setSrcSpan loc      $
+    tcAddDeclCtxt decl  $
+    do { (at_tvs, at_tys, at_rhs) <- tcSynFamInstDecl fam_tc decl
+       
+       -- See Note [Checking consistent instantiation]
+       -- We only want to check this on the *class* TyVars,
+       -- not the *family* TyVars (there may be more of these)
+       ; zipWithM_ check_arg clas_tvs at_tys
+
+       ; return (ATD at_tvs at_tys at_rhs) }
+  where
+    check_arg fam_tc_tv at_ty
+      = checkTc (mkTyVarTy fam_tc_tv `eqType` at_ty) 
+                (wrongATArgErr at_ty (mkTyVarTy fam_tc_tv))
+
+-------------------------
+tcSynFamInstDecl :: TyCon -> TyClDecl Name -> TcM ([TyVar], [Type], Type)
+tcSynFamInstDecl fam_tc (decl@TySynonym {})
+  = kcFamTyPats fam_tc decl $ \k_tvs k_typats resKind ->
+    do { -- check that the family declaration is for a synonym
+         checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
+
+       ; -- (1) kind check the right-hand side of the type equation
+       ; k_rhs <- kcCheckLHsType (tcdSynRhs decl) (EK resKind EkUnk)
+                  -- ToDo: the ExpKind could be better
+
+         -- we need the exact same number of type parameters as the family
+         -- declaration
+       ; let famArity = tyConArity fam_tc
+       ; 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 <- mapM tcHsKindedType k_typats
+       ; t_rhs    <- tcHsKindedType k_rhs
+
+        -- NB: we don't check well-formedness of the instance here because we call
+        -- this function from within the TcTyClsDecls fixpoint. The callers must do
+        -- the check.
 
+       ; return (t_tvs, t_typats, t_rhs) }}
+
+tcSynFamInstDecl _ decl = pprPanic "tcSynFamInstDecl" (ppr decl)
+
+-------------------------
+-- Kind check type patterns and kind annotate the embedded type variables.
+--
+-- * Here we check that a type instance matches its kind signature, but we do
+--   not check whether there is a pattern for each type index; the latter
+--   check is only required for type synonym instances.
+
+kcFamTyPats :: TyCon
+            -> TyClDecl Name
+            -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TcM a)
+               -- ^^kinded tvs         ^^kinded ty pats  ^^res kind
+            -> TcM a
+kcFamTyPats fam_tc decl thing_inside
+  = kcHsTyVars (tcdTyVars decl) $ \tvs ->
+    do { let { (kinds, resKind) = splitKindFunTys (tyConKind fam_tc)
+             ; hs_typats        = fromJust $ tcdTyPats decl }
+
+         -- We may not have more parameters than the kind indicates
+       ; checkTc (length kinds >= length hs_typats) $
+                 tooManyParmsErr (tcdLName decl)
+
+         -- Type functions can have a higher-kinded result
+       ; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind
+       ; typats <- zipWithM kcCheckLHsType hs_typats
+                            [ EK kind (EkArg (ppr fam_tc) n)
+                            | (kind,n) <- kinds `zip` [1..]]
+       ; thing_inside tvs typats resultKind 
+       }
+\end{code}
+
+Note [Associated type instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We allow this:
+  class C a where
+    type T x a
+  instance C Int where
+    type T (S y) Int = y
+    type T Z     Int = Char
+
+Note that 
+  a) The variable 'x' is not bound by the class decl
+  b) 'x' is instantiated to a non-type-variable in the instance
+  c) There are several type instance decls for T in the instance
+
+All this is fine.  Of course, you can't give any *more* instances
+for (T ty Int) elsewhere, becuase it's an *associated* type.
+
+Note [Checking consistent instantiation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  class C a b where
+    type T a x b
+
+  instance C [p] Int
+    type T [p] y Int = (p,y,y)  -- Induces the family instance TyCon
+                                --    type TR p y = (p,y,y)
+
+So we 
+  * Form the mini-envt from the class type variables a,b
+    to the instance decl types [p],Int:   [a->[p], b->Int]
+
+  * Look at the tyvars a,x,b of the type family constructor T
+    (it shares tyvars with the class C)
+
+  * Apply the mini-evnt to them, and check that the result is
+    consistent with the instance types [p] y Int
+
+
+%************************************************************************
+%*                                                                      *
+               Data types
+%*                                                                      *
+%************************************************************************
+
+\begin{code}
 dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl Name] -> TcM ()
 dataDeclChecks tc_name new_or_data stupid_theta cons
   = do {   -- Check that we don't use GADT syntax in H98 world
@@ -966,13 +1148,16 @@ checkValidClass cls
        -- Check the class operations
        ; mapM_ (check_op constrained_class_methods) op_stuff
 
+        -- Check the associated type defaults are well-formed
+        ; mapM_ check_at at_stuff
+
        -- Check that if the class has generic methods, then the
        -- class has only one parameter.  We can't do generic
        -- multi-parameter type classes!
        ; checkTc (unary || no_generics) (genericMultiParamErr cls)
        }
   where
-    (tyvars, fundeps, theta, _, _, op_stuff) = classExtraBigSig cls
+    (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
     unary      = isSingleton tyvars
     no_generics = null [() | (_, (GenDefMeth _)) <- op_stuff]
 
@@ -1014,6 +1199,9 @@ checkValidClass cls
                -- in the context of a for-all must mention at least one quantified
                -- type variable.  What a mess!
 
+    check_at (_fam_tc, defs)
+      = mapM_ (\(ATD _tvs pats rhs) -> checkValidFamInst pats rhs) defs
+
 checkFamFlag :: Name -> TcM ()
 -- Check that we don't use families without -XTypeFamilies
 -- The parser won't even parse them, but I suppose a GHC API
@@ -1307,6 +1495,11 @@ badDataConTyCon data_con res_ty_tmpl actual_res_ty
                ptext (sLit "returns type") <+> quotes (ppr actual_res_ty))
        2 (ptext (sLit "instead of an instance of its parent type") <+> quotes (ppr res_ty_tmpl))
 
+badATErr :: Outputable a => a -> Name -> SDoc
+badATErr clas op
+  = hsep [ptext (sLit "Class"), quotes (ppr clas), 
+          ptext (sLit "does not have an associated type"), quotes (ppr op)]
+
 badGadtDecl :: Name -> SDoc
 badGadtDecl tc_name
   = vcat [ ptext (sLit "Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
@@ -1357,4 +1550,30 @@ emptyConDeclsErr :: Name -> SDoc
 emptyConDeclsErr tycon
   = sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
         nest 2 $ ptext (sLit "(-XEmptyDataDecls permits this)")]
+
+wrongATArgErr :: Type -> Type -> SDoc
+wrongATArgErr ty instTy =
+  sep [ ptext (sLit "Type indexes must match class instance head")
+      , ptext (sLit "Found") <+> quotes (ppr ty)
+        <+> ptext (sLit "but expected") <+> quotes (ppr instTy)
+      ]
+
+tooManyParmsErr :: Located Name -> SDoc
+tooManyParmsErr tc_name
+  = ptext (sLit "Family instance has too many parameters:") <+>
+    quotes (ppr tc_name)
+
+wrongNumberOfParmsErr :: Arity -> SDoc
+wrongNumberOfParmsErr exp_arity
+  = ptext (sLit "Number of parameters must match family declaration; expected")
+    <+> ppr exp_arity
+
+wrongKindOfFamily :: TyCon -> SDoc
+wrongKindOfFamily family
+  = ptext (sLit "Wrong category of family instance; declaration was for a")
+    <+> kindOfFamily
+  where
+    kindOfFamily | isSynTyCon family = ptext (sLit "type synonym")
+                 | isAlgTyCon family = ptext (sLit "data type")
+                 | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
 \end{code}