Commit 2d4db40a authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Fix #10815 by kind-checking type patterns against known kinds.

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.
parent a8406f81
......@@ -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
......
......@@ -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
......
......@@ -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]
......
......@@ -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
......
......@@ -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)
......@@ -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,
......
<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])