+\subsection{Type checking instances of indexed types}
+%* *
+%************************************************************************
+
+Instances of indexed types are somewhat of a hybrid. They are processed
+together with class instance heads, but can contain data constructors and hence
+they share a lot of kinding and type checking code with ordinary algebraic
+data types (and GADTs).
+
+\begin{code}
+tcIdxTyInstDecl :: LTyClDecl Name -> TcM (Maybe TyThing) -- Nothing if error
+tcIdxTyInstDecl (L loc decl)
+ = -- Prime error recovery, set source location
+ recoverM (returnM Nothing) $
+ setSrcSpan loc $
+ tcAddDeclCtxt decl $
+ do { -- indexed data types require -findexed-types and can't be in an
+ -- hs-boot file
+ ; gla_exts <- doptM Opt_IndexedTypes
+ ; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file?
+ ; checkTc gla_exts $ badIdxTyDecl (tcdLName decl)
+ ; checkTc (not is_boot) $ badBootTyIdxDeclErr
+
+ -- perform kind and type checking
+ ; tcIdxTyInstDecl1 decl
+ }
+
+tcIdxTyInstDecl1 :: TyClDecl Name -> TcM (Maybe TyThing) -- Nothing if error
+
+tcIdxTyInstDecl1 (decl@TySynonym {})
+ = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
+ do { -- check that the family declaration is for a synonym
+ unless (isSynTyCon family) $
+ addErr (wrongKindOfFamily family)
+
+ ; -- (1) kind check the right hand side of the type equation
+ ; k_rhs <- kcCheckHsType (tcdSynRhs decl) resKind
+
+ -- (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
+
+ -- !!!of the form: forall t_tvs. (tcdLName decl) t_typats = t_rhs
+ ; return Nothing -- !!!TODO: need TyThing for indexed synonym
+ }}
+
+tcIdxTyInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
+ tcdCons = cons})
+ = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
+ do { -- check that the family declaration is for the right kind
+ unless (new_or_data == NewType && isNewTyCon family ||
+ new_or_data == DataType && isDataTyCon family) $
+ addErr (wrongKindOfFamily family)
+
+ ; -- (1) kind check the data declaration as usual
+ ; k_decl <- kcDataDecl decl k_tvs
+ ; let k_ctxt = tcdCtxt k_decl
+ k_cons = tcdCons k_decl
+
+ -- result kind must be '*' (otherwise, we have too few patterns)
+ ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr tc_name
+
+ -- (2) type check indexed data type declaration
+ ; tcTyVarBndrs k_tvs $ \t_tvs -> do { -- turn kinded into proper tyvars
+ ; unbox_strict <- doptM Opt_UnboxStrictFields
+
+ -- Check that we don't use GADT syntax for indexed types
+ ; checkTc h98_syntax (badGadtIdxTyDecl tc_name)
+
+ -- Check that a newtype has exactly one constructor
+ ; checkTc (new_or_data == DataType || isSingleton k_cons) $
+ newtypeConError tc_name (length k_cons)
+
+ ; t_typats <- mappM tcHsKindedType k_typats
+ ; stupid_theta <- tcHsKindedContext k_ctxt
+
+ ; rep_tc_name <- newFamInstTyConName tc_name (srcSpanStart loc)
+ ; tycon <- fixM (\ tycon -> do
+ { data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data
+ tycon t_tvs))
+ k_cons
+ ; tc_rhs <-
+ case new_or_data of
+ DataType -> return (mkDataTyConRhs data_cons)
+ NewType -> ASSERT( isSingleton data_cons )
+ mkNewTyConRhs tc_name tycon (head data_cons)
+ ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
+ False h98_syntax (Just (family, t_typats))
+ -- We always assume that indexed types are recursive. Why?
+ -- (1) Due to their open nature, we can never be sure that a
+ -- further instance might not introduce a new recursive
+ -- dependency. (2) They are always valid loop breakers as
+ -- they involve a coercion.
+ })
+
+ -- construct result
+ ; return $ Just (ATyCon tycon)
+ }}
+ where
+ h98_syntax = case cons of -- All constructors have same shape
+ L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
+ other -> True
+
+-- Kind checking of indexed types
+-- -
+
+-- 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 functions.
+--
+kcIdxTyPats :: TyClDecl Name
+ -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TyCon -> TcM a)
+ -- ^^kinded tvs ^^kinded ty pats ^^res kind
+ -> TcM a
+kcIdxTyPats decl thing_inside
+ = kcHsTyVars (tcdTyVars decl) $ \tvs ->
+ do { family <- tcLookupLocatedTyCon (tcdLName decl)
+ ; let { (kinds, resKind) = splitKindFunTys (tyConKind family)
+ ; 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 <- TcRnMonad.zipWithM kcCheckHsType hs_typats kinds
+ ; thing_inside tvs typats resultKind family
+ }
+ where
+\end{code}
+
+
+%************************************************************************
+%* *