Fix #10815 by kind-checking type patterns against known kinds.
authorRichard Eisenberg <eir@cis.upenn.edu>
Mon, 31 Aug 2015 17:46:01 +0000 (10:46 -0700)
committerRichard Eisenberg <eir@cis.upenn.edu>
Sat, 19 Sep 2015 16:09:16 +0000 (12:09 -0400)
tcFamTyPats now must take information about the instantiation of any
class variables, when checking the instance of an associated type.

Getting this to work out required some unexpected refactoring in
TcDeriv. TcDeriv needs to look at class instances because of the
possibility of associated datatypes with `deriving` specs. TcDeriv
worked over the user-specified instances. But any data family instances
were already processed, and TcDeriv had no way of finding the rep
tycons. Indeed, TcDeriv *re-type-checked* any data family instances
in an attempt to rediscover what GHC already knew. So, this commit
introduces better tracking of compiled data families between TcInstDcls
and TcDeriv to streamline all of this.

compiler/typecheck/TcDeriv.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcValidity.hs
compiler/types/TyCon.hs
testsuite/tests/ghci/scripts/T6018ghcifail.stderr
testsuite/tests/indexed-types/should_compile/T10815.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T
testsuite/tests/indexed-types/should_fail/T9160.stderr
testsuite/tests/typecheck/should_fail/T6018fail.stderr

index 0a20155..a8a83f5 100644 (file)
@@ -8,7 +8,7 @@ Handles @deriving@ clauses on @data@ declarations.
 
 {-# LANGUAGE CPP #-}
 
-module TcDeriv ( tcDeriving ) where
+module TcDeriv ( tcDeriving, DerivInfo(..), mkDerivInfos ) where
 
 #include "HsVersions.h"
 
@@ -19,9 +19,8 @@ import TcRnMonad
 import FamInst
 import TcErrors( reportAllUnsolved )
 import TcValidity( validDerivPred )
+import TcClassDcl( tcMkDeclCtxt )
 import TcEnv
-import TcTyClsDecls( tcFamTyPats, famTyConShape, tcAddDataFamInstCtxt, kcDataDefn )
-import TcClassDcl( tcAddDeclCtxt )      -- Small helper
 import TcGenDeriv                       -- Deriv stuff
 import TcGenGenerics
 import InstEnv
@@ -331,6 +330,33 @@ See Trac #3221.  Consider
 Are T1 and T2 unused?  Well, no: the deriving clause expands to mention
 both of them.  So we gather defs/uses from deriving just like anything else.
 
+-}
+
+-- | Stuff needed to process a `deriving` clause
+data DerivInfo = DerivInfo { di_rep_tc :: TyCon
+                             -- ^ The data tycon for normal datatypes,
+                             -- or the *representation* tycon for data families
+                           , di_preds  :: [LHsType Name]
+                           , di_ctxt   :: SDoc -- ^ error context
+                           }
+
+-- | Extract `deriving` clauses of proper data type (skips data families)
+mkDerivInfos :: [TyClGroup Name] -> TcM [DerivInfo]
+mkDerivInfos tycls = concatMapM mk_derivs tycls
+  where
+    mk_derivs (TyClGroup { group_tyclds = decls })
+      = concatMapM (mk_deriv . unLoc) decls
+
+    mk_deriv decl@(DataDecl { tcdLName = L _ data_name
+                            , tcdDataDefn =
+                                HsDataDefn { dd_derivs = Just (L _ preds) } })
+      = do { tycon <- tcLookupTyCon data_name
+           ; return [DerivInfo { di_rep_tc = tycon, di_preds = preds
+                               , di_ctxt = tcMkDeclCtxt decl }] }
+    mk_deriv _ = return []
+
+{-
+
 ************************************************************************
 *                                                                      *
 \subsection[TcDeriv-driver]{Top-level function for \tr{derivings}}
@@ -338,11 +364,10 @@ both of them.  So we gather defs/uses from deriving just like anything else.
 ************************************************************************
 -}
 
-tcDeriving  :: [LTyClDecl Name]  -- All type constructors
-            -> [LInstDecl Name]  -- All instance declarations
+tcDeriving  :: [DerivInfo]       -- All `deriving` clauses
             -> [LDerivDecl Name] -- All stand-alone deriving declarations
             -> TcM (TcGblEnv, Bag (InstInfo Name), HsValBinds Name)
-tcDeriving tycl_decls inst_decls deriv_decls
+tcDeriving deriv_infos deriv_decls
   = recoverM (do { g <- getGblEnv
                  ; return (g, emptyBag, emptyValBindsOut)}) $
     do  {       -- Fish the "deriving"-related information out of the TcEnv
@@ -350,7 +375,7 @@ tcDeriving tycl_decls inst_decls deriv_decls
           is_boot <- tcIsHsBootOrSig
         ; traceTc "tcDeriving" (ppr is_boot)
 
-        ; early_specs <- makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
+        ; early_specs <- makeDerivSpecs is_boot deriv_infos deriv_decls
         ; traceTc "tcDeriving 1" (ppr early_specs)
 
         -- for each type, determine the auxliary declarations that are common
@@ -501,6 +526,20 @@ So we want to signal a user of the data constructor 'MkP'.
 This is the reason behind the (Maybe Name) part of the return type
 of genInst.
 
+Note [Why we don't pass rep_tc into deriveTyData]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Down in the bowels of mkEqnHelp, we need to convert the fam_tc back into
+the rep_tc by means of a lookup. And yet we have the rep_tc right here!
+Why look it up again? Answer: it's just easier this way.
+We drop some number of arguments from the end of the datatype definition
+in deriveTyData. The arguments are dropped from the fam_tc.
+This action may drop a *different* number of arguments
+passed to the rep_tc, depending on how many free variables, etc., the
+dropped patterns have.
+
+Also, this technique carries over the kind substitution from deriveTyData
+nicely.
+
 ************************************************************************
 *                                                                      *
                 From HsSyn to DerivSpec
@@ -511,15 +550,13 @@ of genInst.
 -}
 
 makeDerivSpecs :: Bool
-               -> [LTyClDecl Name]
-               -> [LInstDecl Name]
+               -> [DerivInfo]
                -> [LDerivDecl Name]
                -> TcM [EarlyDerivSpec]
-makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
-  = do  { eqns1 <- concatMapM (recoverM (return []) . deriveTyDecl)     tycl_decls
-        ; eqns2 <- concatMapM (recoverM (return []) . deriveInstDecl)   inst_decls
-        ; eqns3 <- concatMapM (recoverM (return []) . deriveStandalone) deriv_decls
-        ; let eqns = eqns1 ++ eqns2 ++ eqns3
+makeDerivSpecs is_boot deriv_infos deriv_decls
+  = do  { eqns1 <- concatMapM (recoverM (return []) . deriveDerivInfo)  deriv_infos
+        ; eqns2 <- concatMapM (recoverM (return []) . deriveStandalone) deriv_decls
+        ; let eqns = eqns1 ++ eqns2
 
         ; if is_boot then   -- No 'deriving' at all in hs-boot files
               do { unless (null eqns) (add_deriv_err (head eqns))
@@ -532,63 +569,21 @@ makeDerivSpecs is_boot tycl_decls inst_decls deriv_decls
                     2 (ptext (sLit "Use an instance declaration instead")))
 
 ------------------------------------------------------------------
-deriveTyDecl :: LTyClDecl Name -> TcM [EarlyDerivSpec]
-deriveTyDecl (L _ decl@(DataDecl { tcdLName = L _ tc_name
-                                 , tcdDataDefn = HsDataDefn { dd_derivs = preds } }))
-  = tcAddDeclCtxt decl $
-    do { tc <- tcLookupTyCon tc_name
-       ; let tvs  = tyConTyVars tc
-             tys  = mkTyVarTys tvs
-
-       ; case preds of
-          Just (L _ preds') -> concatMapM (deriveTyData tvs tc tys) preds'
-          Nothing           -> return [] }
-
-deriveTyDecl _ = return []
-
-------------------------------------------------------------------
-deriveInstDecl :: LInstDecl Name -> TcM [EarlyDerivSpec]
-deriveInstDecl (L _ (TyFamInstD {})) = return []
-deriveInstDecl (L _ (DataFamInstD { dfid_inst = fam_inst }))
-  = deriveFamInst fam_inst
-deriveInstDecl (L _ (ClsInstD { cid_inst = ClsInstDecl { cid_datafam_insts = fam_insts } }))
-  = concatMapM (deriveFamInst . unLoc) fam_insts
-
-------------------------------------------------------------------
-deriveFamInst :: DataFamInstDecl Name -> TcM [EarlyDerivSpec]
-deriveFamInst decl@(DataFamInstDecl
-                       { dfid_tycon = L _ tc_name, dfid_pats = pats
-                       , dfid_defn
-                         = defn@(HsDataDefn { dd_derivs = Just (L _ preds) }) })
-  = tcAddDataFamInstCtxt decl $
-    do { fam_tc <- tcLookupTyCon tc_name
-       ; tcFamTyPats (famTyConShape fam_tc) pats (kcDataDefn defn) $
-             -- kcDataDefn defn: see Note [Finding the LHS patterns]
-         \ tvs' pats' _ ->
-           concatMapM (deriveTyData tvs' fam_tc pats') preds }
-
-deriveFamInst _ = return []
+-- | Process a `deriving` clause
+deriveDerivInfo :: DerivInfo -> TcM [EarlyDerivSpec]
+deriveDerivInfo (DerivInfo { di_rep_tc = rep_tc, di_preds = preds
+                           , di_ctxt = err_ctxt })
+  = addErrCtxt err_ctxt $
+    concatMapM (deriveTyData tvs tc tys) preds
+  where
+    tvs = tyConTyVars rep_tc
+    (tc, tys) = case tyConFamInstSig_maybe rep_tc of
+                        -- data family:
+                  Just (fam_tc, pats, _) -> (fam_tc, pats)
+      -- NB: deriveTyData wants the *user-specified*
+      -- name. See Note [Why we don't pass rep_tc into deriveTyData]
 
-{-
-Note [Finding the LHS patterns]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When kind polymorphism is in play, we need to be careful.  Here is
-Trac #9359:
-  data Cmp a where
-    Sup :: Cmp a
-    V   :: a -> Cmp a
-
-  data family   CmpInterval (a :: Cmp k) (b :: Cmp k) :: *
-  data instance CmpInterval (V c) Sup = Starting c deriving( Show )
-
-So CmpInterval is kind-polymorphic, but the data instance is not
-   CmpInterval :: forall k. Cmp k -> Cmp k -> *
-   data instance CmpInterval * (V (c::*)) Sup = Starting c deriving( Show )
-
-Hence, when deriving the type patterns in deriveFamInst, we must kind
-check the RHS (the data constructor 'Starting c') as well as the LHS,
-so that we correctly see the instantiation to *.
--}
+                  _ -> (rep_tc, mkTyVarTys tvs)     -- datatype
 
 ------------------------------------------------------------------
 deriveStandalone :: LDerivDecl Name -> TcM [EarlyDerivSpec]
@@ -669,8 +664,8 @@ deriveTyData tvs tc tc_args (L loc deriv_pred)
           let (arg_kinds, _)  = splitKindFunTys cls_arg_kind
               n_args_to_drop  = length arg_kinds
               n_args_to_keep  = tyConArity tc - n_args_to_drop
-              args_to_drop    = drop n_args_to_keep tc_args
-              tc_args_to_keep = take n_args_to_keep tc_args
+              (tc_args_to_keep, args_to_drop)
+                              = splitAt n_args_to_keep tc_args
               inst_ty_kind    = typeKind (mkTyConApp tc tc_args_to_keep)
               dropped_tvs     = tyVarsOfTypes args_to_drop
 
index 328a8cf..a4b3870 100644 (file)
@@ -61,7 +61,7 @@ import Util
 import BooleanFormula ( isUnsatisfied, pprBooleanFormulaNice )
 
 import Control.Monad
-import Maybes     ( isNothing, isJust, whenIsJust, catMaybes )
+import Maybes
 import Data.List  ( mapAccumL, partition )
 
 {-
@@ -357,7 +357,7 @@ Gather up the instance declarations from their various sources
 -}
 
 tcInstDecls1    -- Deal with both source-code and imported instance decls
-   :: [LTyClDecl Name]          -- For deriving stuff
+   :: [TyClGroup Name]          -- For deriving stuff
    -> [LInstDecl Name]          -- Source code instance decls
    -> [LDerivDecl Name]         -- Source code stand-alone deriving decls
    -> TcM (TcGblEnv,            -- The full inst env
@@ -373,7 +373,7 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
 
             -- Do class and family instance declarations
        ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
-       ; let (local_infos_s, fam_insts_s) = unzip stuff
+       ; let (local_infos_s, fam_insts_s, datafam_deriv_infos) = unzip3 stuff
              fam_insts    = concat fam_insts_s
              local_infos' = concat local_infos_s
              -- Handwritten instances of the poly-kinded Typeable class are
@@ -398,7 +398,10 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
               <- if isBrackStage th_stage
                  then do { gbl_env <- getGblEnv
                          ; return (gbl_env, emptyBag, emptyValBindsOut) }
-                 else tcDeriving tycl_decls inst_decls deriv_decls
+                 else do { data_deriv_infos <- mkDerivInfos tycl_decls
+                         ; let deriv_infos = concat datafam_deriv_infos ++
+                                             data_deriv_infos
+                         ; tcDeriving deriv_infos deriv_decls }
 
        -- Fail if there are any handwritten instance of poly-kinded Typeable
        ; mapM_ typeable_err typeable_instances
@@ -418,7 +421,7 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls
 
        ; return ( gbl_env
                 , bagToList deriv_inst_info ++ local_infos
-                , deriv_binds)
+                , deriv_binds )
     }}
   where
     -- Separate the Typeable instances from the rest
@@ -485,24 +488,26 @@ the brutal solution will do.
 -}
 
 tcLocalInstDecl :: LInstDecl Name
-                -> TcM ([InstInfo Name], [FamInst])
+                -> TcM ([InstInfo Name], [FamInst], [DerivInfo])
         -- A source-file instance declaration
         -- Type-check all the stuff before the "where"
         --
         -- We check for respectable instance type, and context
 tcLocalInstDecl (L loc (TyFamInstD { tfid_inst = decl }))
   = do { fam_inst <- tcTyFamInstDecl Nothing (L loc decl)
-       ; return ([], [fam_inst]) }
+       ; return ([], [fam_inst], []) }
 
 tcLocalInstDecl (L loc (DataFamInstD { dfid_inst = decl }))
-  = do { fam_inst <- tcDataFamInstDecl Nothing (L loc decl)
-       ; return ([], [fam_inst]) }
+  = do { (fam_inst, m_deriv_info) <- tcDataFamInstDecl Nothing (L loc decl)
+       ; return ([], [fam_inst], maybeToList m_deriv_info) }
 
 tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
-  = do { (insts, fam_insts) <- tcClsInstDecl (L loc decl)
-       ; return (insts, fam_insts) }
+  = do { (insts, fam_insts, deriv_infos) <- tcClsInstDecl (L loc decl)
+       ; return (insts, fam_insts, deriv_infos) }
 
-tcClsInstDecl :: LClsInstDecl Name -> TcM ([InstInfo Name], [FamInst])
+tcClsInstDecl :: LClsInstDecl Name
+              -> TcM ([InstInfo Name], [FamInst], [DerivInfo])
+-- the returned DerivInfos are for any associated data families
 tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                                   , cid_sigs = uprags, cid_tyfam_insts = ats
                                   , cid_overlap_mode = overlap_mode
@@ -522,8 +527,10 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
         ; traceTc "tcLocalInstDecl" (ppr poly_ty)
         ; tyfam_insts0  <- tcExtendTyVarEnv tyvars $
                            mapAndRecoverM (tcTyFamInstDecl mb_info) ats
-        ; datafam_insts <- tcExtendTyVarEnv tyvars $
+        ; datafam_stuff <- tcExtendTyVarEnv tyvars $
                            mapAndRecoverM (tcDataFamInstDecl mb_info) adts
+        ; let (datafam_insts, m_deriv_infos) = unzip datafam_stuff
+              deriv_infos                    = catMaybes m_deriv_infos
 
         -- Check for missing associated types and build them
         -- from their defaults (if available)
@@ -548,7 +555,8 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
                                      , ib_extensions = []
                                      , ib_derived = False } }
 
-        ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts) }
+        ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts
+                 , deriv_infos ) }
 
 
 tcATDefault :: SrcSpan -> TvSubst -> NameSet -> ClassATItem -> TcM [FamInst]
@@ -604,7 +612,7 @@ lot of kinding and type checking code with ordinary algebraic data types (and
 GADTs).
 -}
 
-tcFamInstDeclCombined :: Maybe (Class, VarEnv Type) -- the class & mini_env if applicable
+tcFamInstDeclCombined :: Maybe ClsInfo
                       -> Located Name -> TcM TyCon
 tcFamInstDeclCombined mb_clsinfo fam_tc_lname
   = do { -- Type family instances require -XTypeFamilies
@@ -624,7 +632,7 @@ tcFamInstDeclCombined mb_clsinfo fam_tc_lname
 
        ; return fam_tc }
 
-tcTyFamInstDecl :: Maybe (Class, VarEnv Type) -- the class & mini_env if applicable
+tcTyFamInstDecl :: Maybe ClsInfo
                 -> LTyFamInstDecl Name -> TcM FamInst
   -- "type instance"
 tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
@@ -639,7 +647,7 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
        ; checkTc (isOpenTypeFamilyTyCon fam_tc) (notOpenFamily fam_tc)
 
          -- (1) do the work of verifying the synonym group
-       ; co_ax_branch <- tcTyFamInstEqn (famTyConShape fam_tc) eqn
+       ; co_ax_branch <- tcTyFamInstEqn (famTyConShape fam_tc) mb_clsinfo eqn
 
          -- (2) check for validity
        ; checkValidCoAxBranch mb_clsinfo fam_tc co_ax_branch
@@ -650,15 +658,16 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
        ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
        ; newFamInst SynFamilyInst axiom }
 
-tcDataFamInstDecl :: Maybe (Class, VarEnv Type)
-                  -> LDataFamInstDecl Name -> TcM FamInst
+tcDataFamInstDecl :: Maybe ClsInfo
+                  -> LDataFamInstDecl Name -> TcM (FamInst, Maybe DerivInfo)
   -- "newtype instance" and "data instance"
 tcDataFamInstDecl mb_clsinfo
     (L loc decl@(DataFamInstDecl
        { dfid_pats = pats
        , dfid_tycon = fam_tc_name
        , dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
-                                     , dd_ctxt = ctxt, dd_cons = cons } }))
+                                     , dd_ctxt = ctxt, dd_cons = cons
+                                     , dd_derivs = derivs } }))
   = setSrcSpan loc             $
     tcAddDataFamInstCtxt decl  $
     do { fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_tc_name
@@ -668,7 +677,7 @@ tcDataFamInstDecl mb_clsinfo
        ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)
 
          -- Kind check type patterns
-       ; tcFamTyPats (famTyConShape fam_tc) pats
+       ; tcFamTyPats (famTyConShape fam_tc) mb_clsinfo pats
                      (kcDataDefn defn) $
            \tvs' pats' res_kind -> do
 
@@ -704,6 +713,9 @@ tcDataFamInstDecl mb_clsinfo
                                                (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
                     parent   = FamInstTyCon axiom fam_tc pats'
                     roles    = map (const Nominal) tvs'
+
+                      -- NB: Use the tvs' from the pats. See bullet toward
+                      -- the end of Note [Data type families] in TyCon
                     rep_tc   = buildAlgTyCon rep_tc_name tvs' roles
                                              (fmap unLoc cType) stupid_theta
                                              tc_rhs
@@ -720,7 +732,15 @@ tcDataFamInstDecl mb_clsinfo
 
          -- Remember to check validity; no recursion to worry about here
        ; checkValidTyCon rep_tc
-       ; return fam_inst } }
+
+       ; let m_deriv_info = case derivs of
+               Nothing          -> Nothing
+               Just (L _ preds) ->
+                 Just $ DerivInfo { di_rep_tc = rep_tc
+                                  , di_preds  = preds
+                                  , di_ctxt   = tcMkDataFamInstCtxt decl }
+
+       ; return (fam_inst, m_deriv_info) } }
   where
     -- See Note [Eta reduction for data family axioms]
     --  [a,b,c,d].T [a] c Int c d  ==>  [a,b,c]. T [a] c Int c
index 1595eef..1128a44 100644 (file)
@@ -1230,7 +1230,7 @@ tcTyClsInstDecls tycl_decls inst_decls deriv_decls
       -- Note [AFamDataCon: not promoting data family constructors]
    do { tcg_env <- tcTyAndClassDecls tycl_decls ;
       ; setGblEnv tcg_env $
-        tcInstDecls1 (tyClGroupConcat tycl_decls) inst_decls deriv_decls }
+        tcInstDecls1 tycl_decls inst_decls deriv_decls }
   where
     -- get_cons extracts the *constructor* bindings of the declaration
     get_cons :: LInstDecl Name -> [Name]
index 11dc141..516dca0 100644 (file)
@@ -15,7 +15,7 @@ module TcTyClsDecls (
         -- data/type family instance declarations
         kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
         tcFamTyPats, tcTyFamInstEqn, famTyConShape,
-        tcAddTyFamInstCtxt, tcAddDataFamInstCtxt,
+        tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
         wrongKindOfFamily, dataConCtxt, badDataConTyCon
     ) where
 
@@ -721,7 +721,7 @@ tcFamDecl1 parent
        ; tc_kind <- kcLookupKind tc_name
        ; let fam_tc_shape = (tc_name, length (hsQTvBndrs tvs), tc_kind)
 
-       ; branches <- mapM (tcTyFamInstEqn fam_tc_shape) eqns
+       ; branches <- mapM (tcTyFamInstEqn fam_tc_shape Nothing) eqns
          -- Do not attempt to drop equations dominated by earlier
          -- ones here; in the case of mutual recursion with a data
          -- type, we get a knot-tying failure.  Instead we check
@@ -950,17 +950,18 @@ kcTyFamInstEqn fam_tc_shape
     (L loc (TyFamEqn { tfe_pats = pats, tfe_rhs = hs_ty }))
   = setSrcSpan loc $
     discardResult $
-    tc_fam_ty_pats fam_tc_shape pats (discardResult . (tcCheckLHsType hs_ty))
+    tc_fam_ty_pats fam_tc_shape Nothing -- not an associated type
+                   pats (discardResult . (tcCheckLHsType hs_ty))
 
-tcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn Name -> TcM CoAxBranch
+tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInfo -> LTyFamInstEqn Name -> TcM CoAxBranch
 -- Needs to be here, not in TcInstDcls, because closed families
 -- (typechecked here) have TyFamInstEqns
-tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_)
+tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_) mb_clsinfo
     (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
                      , tfe_pats = pats
                      , tfe_rhs = hs_ty }))
   = setSrcSpan loc $
-    tcFamTyPats fam_tc_shape pats (discardResult . (tcCheckLHsType hs_ty)) $
+    tcFamTyPats fam_tc_shape mb_clsinfo pats (discardResult . (tcCheckLHsType hs_ty)) $
        \tvs' pats' res_kind ->
     do { checkTc (fam_tc_name == eqn_tc_name)
                  (wrongTyFamName fam_tc_name eqn_tc_name)
@@ -1042,6 +1043,7 @@ famTyConShape fam_tc
     , tyConKind fam_tc )
 
 tc_fam_ty_pats :: FamTyConShape
+               -> Maybe ClsInfo
                -> HsWithBndrs Name [LHsType Name] -- Patterns
                -> (TcKind -> TcM ())              -- Kind checker for RHS
                                                   -- result is ignored
@@ -1057,24 +1059,28 @@ tc_fam_ty_pats :: FamTyConShape
 -- In that case, the type variable 'a' will *already be in scope*
 -- (and, if C is poly-kinded, so will its kind parameter).
 
-tc_fam_ty_pats (name, arity, kind)
+tc_fam_ty_pats (name, arity, kind) mb_clsinfo
                (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars
                      , hswb_tvs = tvars, hswb_wcs = wcs })
                kind_checker
   = do { let (fam_kvs, fam_body) = splitForAllTys kind
 
-         -- We wish to check that the pattern has the right number of arguments
-         -- in checkValidFamPats (in TcValidity), so we can do the check *after*
-         -- we're done with the knot. But, the splitKindFunTysN below will panic
-         -- if there are *too many* patterns. So, we do a preliminary check here.
-         -- Note that we don't have enough information at hand to do a full check,
-         -- as that requires the full declared arity of the family, which isn't
-         -- nearby.
+         -- The splitKindFunTysN below will panic
+         -- if there are too many patterns. So, we do a validity check here.
        ; checkTc (length arg_pats == arity) $
          wrongNumberOfParmsErr arity
 
-         -- Instantiate with meta kind vars
-       ; fam_arg_kinds <- mapM (const newMetaKindVar) fam_kvs
+         -- Instantiate with meta kind vars (or instance kinds)
+       ; fam_arg_kinds <- case mb_clsinfo of
+           Nothing            -> mapM (const newMetaKindVar) fam_kvs
+           Just (_, mini_env) -> mapM mk_arg_kind fam_kvs
+             where
+               mk_arg_kind kv
+                 | Just kind <- lookupVarEnv mini_env kv
+                 = return kind
+                 | otherwise
+                 = newMetaKindVar
+
        ; loc <- getSrcSpanM
        ; let (arg_kinds, res_kind)
                  = splitKindFunTysN (length arg_pats) $
@@ -1095,15 +1101,16 @@ tc_fam_ty_pats (name, arity, kind)
 
 -- See Note [tc_fam_ty_pats vs tcFamTyPats]
 tcFamTyPats :: FamTyConShape
+            -> Maybe ClsInfo
             -> HsWithBndrs Name [LHsType Name] -- patterns
             -> (TcKind -> TcM ())              -- kind-checker for RHS
             -> ([TKVar]              -- Kind and type variables
                 -> [TcType]          -- Kind and type arguments
                 -> Kind -> TcM a)
             -> TcM a
-tcFamTyPats fam_shape@(name,_,_) pats kind_checker thing_inside
+tcFamTyPats fam_shape@(name,_,_) mb_clsinfo pats kind_checker thing_inside
   = do { (fam_arg_kinds, typats, res_kind)
-            <- tc_fam_ty_pats fam_shape pats kind_checker
+            <- tc_fam_ty_pats fam_shape mb_clsinfo pats kind_checker
        ; let all_args = fam_arg_kinds ++ typats
 
             -- Find free variables (after zonking) and turn
@@ -2194,18 +2201,23 @@ tcAddTyFamInstCtxt :: TyFamInstDecl Name -> TcM a -> TcM a
 tcAddTyFamInstCtxt decl
   = tcAddFamInstCtxt (ptext (sLit "type instance")) (tyFamInstDeclName decl)
 
+tcMkDataFamInstCtxt :: DataFamInstDecl Name -> SDoc
+tcMkDataFamInstCtxt decl
+  = tcMkFamInstCtxt (pprDataFamInstFlavour decl <+> text "instance")
+                    (unLoc (dfid_tycon decl))
+
 tcAddDataFamInstCtxt :: DataFamInstDecl Name -> TcM a -> TcM a
 tcAddDataFamInstCtxt decl
-  = tcAddFamInstCtxt (pprDataFamInstFlavour decl <+> ptext (sLit "instance"))
-                     (unLoc (dfid_tycon decl))
+  = addErrCtxt (tcMkDataFamInstCtxt decl)
+
+tcMkFamInstCtxt :: SDoc -> Name -> SDoc
+tcMkFamInstCtxt flavour tycon
+  = hsep [ text "In the" <+> flavour <+> text "declaration for"
+         , quotes (ppr tycon) ]
 
 tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
 tcAddFamInstCtxt flavour tycon thing_inside
-  = addErrCtxt ctxt thing_inside
-  where
-     ctxt = hsep [ptext (sLit "In the") <+> flavour
-                  <+> ptext (sLit "declaration for"),
-                  quotes (ppr tycon)]
+  = addErrCtxt (tcMkFamInstCtxt flavour tycon) thing_inside
 
 tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a
 tcAddClosedTypeFamilyDeclCtxt tc
index f9d9bf7..4f20a3d 100644 (file)
@@ -11,7 +11,7 @@ module TcValidity (
   checkValidTheta, checkValidFamPats,
   checkValidInstance, validDerivPred,
   checkInstTermination,
-  checkValidCoAxiom, checkValidCoAxBranch,
+  ClsInfo, checkValidCoAxiom, checkValidCoAxBranch,
   checkConsistentFamInst,
   arityErr, badATErr
   ) where
@@ -130,7 +130,7 @@ unless the instance is available *here*.
 
 Note [When to call checkAmbiguity]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We call checkAmbiguity 
+We call checkAmbiguity
    (a) on user-specified type signatures
    (b) in checkValidType
 
@@ -1145,10 +1145,13 @@ But if the 'b' didn't scope, we would make F's instance too
 poly-kinded.
 -}
 
+-- | Extra information needed when type-checking associated types. The 'Class' is
+-- the enclosing class, and the @VarEnv Type@ maps class variables to their
+-- instance types.
+type ClsInfo       = (Class, VarEnv Type)
+
 checkConsistentFamInst
-               :: Maybe ( Class
-                        , VarEnv Type )  -- ^ Class of associated type
-                                         -- and instantiation of class TyVars
+               :: Maybe ClsInfo
                -> TyCon              -- ^ Family tycon
                -> [TyVar]            -- ^ Type variables of the family instance
                -> [Type]             -- ^ Type patterns from instance
@@ -1268,8 +1271,8 @@ checkValidCoAxiom (CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
 -- Check that a "type instance" is well-formed (which includes decidability
 -- unless -XUndecidableInstances is given).
 --
-checkValidCoAxBranch :: Maybe ( Class, VarEnv Type )
-                    -> TyCon -> CoAxBranch -> TcM ()
+checkValidCoAxBranch :: Maybe ClsInfo
+                     -> TyCon -> CoAxBranch -> TcM ()
 checkValidCoAxBranch mb_clsinfo fam_tc
                     (CoAxBranch { cab_tvs = tvs, cab_lhs = typats
                                 , cab_rhs = rhs, cab_loc = loc })
@@ -1404,4 +1407,3 @@ fv_type (ForAllTy tyvar ty) = filter (/= tyvar) (fv_type ty)
 
 fvTypes :: [Type] -> [TyVar]
 fvTypes tys = concat (map fvType tys)
-
index c10c7ba..9aa0dfd 100644 (file)
@@ -254,6 +254,11 @@ See also Note [Wrappers for data instance tycons] in MkId.hs
   So a data type family is not an injective type function. It's just a
   data type with some axioms that connect it to other data types.
 
+* The tyConTyVars of the representation tycon are the tyvars that the
+  user wrote in the patterns. This is important in TcDeriv, where we
+  bring these tyvars into scope before type-checking the deriving
+  clause. This fact is arranged for in TcInstDecls.tcDataFamInstDecl.
+
 Note [Associated families and their parent class]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 *Associated* families are just like *non-associated* families, except
@@ -673,16 +678,7 @@ data TyConParent
                         -- See Note [Associated families and their parent class]
 
   -- | Type constructors representing an instance of a *data* family.
-  -- Parameters:
-  --
-  --  1) The type family in question
-  --
-  --  2) Instance types; free variables are the 'tyConTyVars'
-  --  of the current 'TyCon' (not the family one). INVARIANT:
-  --  the number of types matches the arity of the family 'TyCon'
-  --
-  --  3) A 'CoTyCon' identifying the representation
-  --  type with the type instance family
+  -- See Note [Data type families] and source comments for more info.
   | FamInstTyCon          -- See Note [Data type families]
         (CoAxiom Unbranched)  -- The coercion axiom.
                -- A *Representational* coercion,
index e1c0055..e3a330e 100644 (file)
 
-<interactive>:10:15:
+<interactive>:10:15: error:
     Type family equations violate injectivity annotation:
       F Char Bool Int = Int
       F Bool Int Char = Int
 
-<interactive>:16:15:
+<interactive>:16:15: error:
     Type family equations violate injectivity annotation:
       I Int Char Bool = Bool
       I Int Int Int = Bool
 
-<interactive>:26:15:
+<interactive>:26:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       IdProxy a = Id a
 
-<interactive>:34:15:
+<interactive>:34:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘'Z’
       P 'Z m = m
 
-<interactive>:40:15:
+<interactive>:40:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘b’ does not appear on injective position.
     In the RHS of type family equation:
       J Int b c = Char
 
-<interactive>:44:15:
+<interactive>:44:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘n’ does not appear on injective position.
     In the RHS of type family equation:
       K ('S n) m = 'S m
 
-<interactive>:49:15:
+<interactive>:49:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       L a = MaybeSyn a
 
-<interactive>:55:41:
+<interactive>:55:41: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k1’ is not inferable from the RHS type variables.
+    Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
       PolyKindVarsF '[] = '[]
 
-<interactive>:60:15:
+<interactive>:60:15: error:
     Type family equation violates injectivity annotation.
     Injective kind variable ‘k1’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
       PolyKindVars '[] = '[]
 
-<interactive>:64:15:
+<interactive>:64:15: error:
     Type family equation violates injectivity annotation.
     Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Fc a b = Int
 
-<interactive>:68:15:
+<interactive>:68:15: error:
     Type family equation violates injectivity annotation.
     Injective type variables ‘a’, ‘b’ do not appear on injective position.
     Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
 
-<interactive>:81:15:
+<interactive>:81:15: error:
     Type family equations violate injectivity annotation:
       F1 [a] = Maybe (GF1 a)
       F1 (Maybe a) = Maybe (GF2 a)
 
-<interactive>:85:15:
+<interactive>:85:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘[a]’
       W1 [a] = a
 
-<interactive>:88:15:
+<interactive>:88:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       W2 [a] = W2 a
 
-<interactive>:92:15:
+<interactive>:92:15: error:
     Type family equations violate injectivity annotation:
       Z1 [a] = (a, a)
       Z1 (Maybe b) = (b, [b])
 
-<interactive>:96:15:
+<interactive>:96:15: error:
     Type family equations violate injectivity annotation:
       G1 [a] = [a]
       G1 (Maybe b) = [(b, b)]
 
-<interactive>:100:15:
+<interactive>:100:15: error:
     Type family equations violate injectivity annotation:
       G3 a Int = (a, Int)
       G3 a Bool = (Bool, a)
 
-<interactive>:104:15:
+<interactive>:104:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘b’ does not appear on injective position.
     In the RHS of type family equation:
       G4 a b = [a]
 
-<interactive>:107:15:
+<interactive>:107:15: error:
     Type family equations violate injectivity annotation:
       G5 [a] = [GF1 a]
       G5 Int = [Bool]
 
-<interactive>:111:15:
+<interactive>:111:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘a’ does not appear on injective position.
     In the RHS of type family equation:
diff --git a/testsuite/tests/indexed-types/should_compile/T10815.hs b/testsuite/tests/indexed-types/should_compile/T10815.hs
new file mode 100644 (file)
index 0000000..08fcd02
--- /dev/null
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}
+
+module T10815 where
+
+import Data.Proxy
+
+type family Any :: k
+
+class kproxy ~ 'KProxy => C (kproxy :: KProxy k) where
+  type F (a :: k)
+  type G a :: k
+
+instance C ('KProxy :: KProxy Bool) where
+  type F a = Int
+  type G a = Any
index 5e7e468..b98f963 100644 (file)
@@ -263,3 +263,4 @@ test('T10634', normal, compile, [''])
 test('T10713', normal, compile, [''])
 test('T10753', normal, compile, [''])
 test('T10806', normal, compile_fail, [''])
+test('T10815', normal, compile, [''])
index e356f80..5850257 100644 (file)
@@ -1,6 +1,7 @@
 
-T9160.hs:18:8:
-    Type indexes must match class instance head
-    Found ‘* -> *’ but expected ‘*’
+T9160.hs:18:12: error:
+    Expecting one more argument to ‘Maybe’
+    Expected kind ‘*’, but ‘Maybe’ has kind ‘* -> *’
+    In the type ‘Maybe’
     In the type instance declaration for ‘F’
     In the instance declaration for ‘C (a :: *)’
index 440ddac..2e0267a 100644 (file)
 [4 of 5] Compiling T6018Afail       ( T6018Afail.hs, T6018Afail.o )
 [5 of 5] Compiling T6018fail        ( T6018fail.hs, T6018fail.o )
 
-T6018Afail.hs:7:15:
+T6018Afail.hs:7:15: error:
     Type family equations violate injectivity annotation:
       G Char Bool Int = Int
       G Bool Int Char = Int
 
-T6018Dfail.hs:7:15:
+T6018Dfail.hs:7:15: error:
     Type family equations violate injectivity annotation:
       T6018Bfail.H Bool Int Char = Int
       T6018Bfail.H Char Bool Int = Int
 
-T6018fail.hs:13:15:
+T6018fail.hs:13:15: error:
     Type family equations violate injectivity annotation:
       F Bool Int Char = Int
       F Char Bool Int = Int
 
-T6018fail.hs:19:15:
+T6018fail.hs:19:15: error:
     Type family equations violate injectivity annotation:
       I Int Int Int = Bool
       I Int Char Bool = Bool
 
-T6018fail.hs:28:15:
+T6018fail.hs:28:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       IdProxy a = Id a
 
-T6018fail.hs:36:15:
+T6018fail.hs:36:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘'Z’
       P 'Z m = m
 
-T6018fail.hs:37:15:
+T6018fail.hs:37:15: error:
     Type family equations violate injectivity annotation:
       P ('S n) m = 'S (P n m)
       P 'Z m = m
 
-T6018fail.hs:42:15:
+T6018fail.hs:42:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘b’ does not appear on injective position.
     In the RHS of type family equation:
       J Int b c = Char
 
-T6018fail.hs:46:15:
+T6018fail.hs:46:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘n’ does not appear on injective position.
     In the RHS of type family equation:
       K ('S n) m = 'S m
 
-T6018fail.hs:51:15:
+T6018fail.hs:51:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       L a = MaybeSyn a
 
-T6018fail.hs:59:10:
+T6018fail.hs:59:10: error:
     Type family equation violates injectivity annotation.
-    Injective kind variable ‘k1’ is not inferable from the RHS type variables.
+    Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
       PolyKindVarsF '[] = '[]
 
-T6018fail.hs:62:15:
+T6018fail.hs:62:15: error:
     Type family equation violates injectivity annotation.
     Injective kind variable ‘k1’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
       PolyKindVars '[] = '[]
 
-T6018fail.hs:66:15:
+T6018fail.hs:66:15: error:
     Type family equation violates injectivity annotation.
     Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Fc a b = Int
 
-T6018fail.hs:70:15:
+T6018fail.hs:70:15: error:
     Type family equation violates injectivity annotation.
     Injective type variables ‘a’, ‘b’ do not appear on injective position.
     Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
     forall (k :: BOX) (a :: k) (b :: k). Gc a b = Int
 
-T6018fail.hs:75:15:
+T6018fail.hs:75:15: error:
     Type family equations violate injectivity annotation:
       F1 (Maybe a) = Maybe (GF2 a)
       F1 [a] = Maybe (GF1 a)
 
-T6018fail.hs:87:15:
+T6018fail.hs:87:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘[a]’
       W1 [a] = a
 
-T6018fail.hs:90:15:
+T6018fail.hs:90:15: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation cannot be a type family:
       W2 [a] = W2 a
 
-T6018fail.hs:95:15:
+T6018fail.hs:95:15: error:
     Type family equations violate injectivity annotation:
       Z1 (Maybe b) = (b, [b])
       Z1 [a] = (a, a)
 
-T6018fail.hs:99:15:
+T6018fail.hs:99:15: error:
     Type family equations violate injectivity annotation:
       G1 (Maybe b) = [(b, b)]
       G1 [a] = [a]
 
-T6018fail.hs:103:15:
+T6018fail.hs:103:15: error:
     Type family equations violate injectivity annotation:
       G3 a Bool = (Bool, a)
       G3 a Int = (a, Int)
 
-T6018fail.hs:106:15:
+T6018fail.hs:106:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘b’ does not appear on injective position.
     In the RHS of type family equation:
       G4 a b = [a]
 
-T6018fail.hs:110:15:
+T6018fail.hs:110:15: error:
     Type family equations violate injectivity annotation:
       G5 Int = [Bool]
       G5 [a] = [GF1 a]
 
-T6018fail.hs:113:15:
+T6018fail.hs:113:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘a’ does not appear on injective position.
     In the RHS of type family equation:
       G6 [a] = [HF1 a]
 
-T6018fail.hs:118:15:
+T6018fail.hs:118:15: error:
     Type family equation violates injectivity annotation.
     Injective type variable ‘c’ does not appear on injective position.
     Injective kind variable ‘k’ is not inferable from the RHS type variables.
     In the RHS of type family equation:
     forall (k :: BOX) a b (c :: k). G7 a b c = [G7a a b c]
 
-T6018fail.hs:129:1:
+T6018fail.hs:129:1: error:
     Type family equations violate injectivity annotation:
       FC Int Bool = Bool
       FC Int Char = Bool
 
-T6018fail.hs:134:1:
+T6018fail.hs:134:1: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
     but these LHS type and kind patterns are not bare variables: ‘*’, ‘Char’