Commit 2316a90d authored by Simon Peyton Jones's avatar Simon Peyton Jones

More fixes to kind polymorphism, fixes Trac #6035, #6036

* Significant refactoring in tcFamPats and tcConDecl

* It seems that we have to allow KindVars (not just
  TcKindVars during kind unification.  See
  Note [Unifying kind variables] in TcUnify.

* Be consistent about zonkQuantifiedTyVars

* Split the TcType->TcType zonker (in TcMType)
   from the TcType->Type   zonker (in TcHsSyn)
  The clever parameterisation was doing my head in,
  and it's only a small function

* Remove some dead code (tcTyVarBndrsGen)
parent 2a119043
......@@ -45,7 +45,7 @@ import Var
import TcRnMonad
import TcType
import TcMType
import TcHsSyn ( mkZonkTcTyVar )
import TcHsSyn ( zonkTcTypeToType, mkEmptyZonkEnv )
import TcUnify
import TcEnv
......@@ -1131,7 +1131,7 @@ zonkTerm = foldTermM (TermFoldM
zonkRttiType :: TcType -> TcM Type
-- Zonk the type, replacing any unbound Meta tyvars
-- by skolems, safely out of Meta-tyvar-land
zonkRttiType = zonkType (mkZonkTcTyVar zonk_unbound_meta mkTyVarTy)
zonkRttiType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_meta)
where
zonk_unbound_meta tv
= ASSERT( isTcTyVar tv )
......
......@@ -254,14 +254,15 @@ addLocalFamInst :: (FamInstEnv,[FamInst]) -> FamInst -> TcM (FamInstEnv, [FamIns
addLocalFamInst (home_fie, my_fis) fam_inst
-- home_fie includes home package and this module
-- my_fies is just the ones from this module
= do { isGHCi <- getIsGHCi
= do { traceTc "addLocalFamInst" (ppr fam_inst)
; isGHCi <- getIsGHCi
-- In GHCi, we *override* any identical instances
-- that are also defined in the interactive context
; let (home_fie', my_fis')
| isGHCi = (deleteFromFamInstEnv home_fie fam_inst,
filterOut (identicalFamInst fam_inst) my_fis)
| otherwise = (home_fie, my_fis)
; let (home_fie', my_fis')
| isGHCi = ( deleteFromFamInstEnv home_fie fam_inst
, filterOut (identicalFamInst fam_inst) my_fis)
| otherwise = (home_fie, my_fis)
-- Load imported instances, so that we report
-- overlaps correctly
......
......@@ -26,9 +26,10 @@ module TcHsSyn (
-- re-exported from TcMonad
TcId, TcIdSet,
zonkTopDecls, zonkTopExpr, zonkTopLExpr, mkZonkTcTyVar,
zonkId, zonkTopBndrs,
emptyZonkEnv, mkTyVarZonkEnv, zonkTcTypeToType, zonkTcTypeToTypes
zonkTopDecls, zonkTopExpr, zonkTopLExpr,
zonkTopBndrs, zonkTyBndrsX,
emptyZonkEnv, mkEmptyZonkEnv, mkTyVarZonkEnv,
zonkTcTypeToType, zonkTcTypeToTypes
) where
#include "HsVersions.h"
......@@ -37,8 +38,9 @@ import HsSyn
import Id
import TcRnMonad
import PrelNames
import TypeRep -- We can see the representation of types
import TcType
import TcMType
import TcMType ( defaultKindVarToStar, zonkQuantifiedTyVar, writeMetaTyVar )
import TcEvidence
import TysPrim
import TysWiredIn
......@@ -161,14 +163,6 @@ hsOverLitName (HsIsString {}) = fromStringName
%* *
%************************************************************************
\begin{code}
-- zonkId is used *during* typechecking just to zonk the Id's type
zonkId :: TcId -> TcM TcId
zonkId id
= zonkTcType (idType id) `thenM` \ ty' ->
returnM (Id.setIdType id ty')
\end{code}
The rest of the zonking is done *after* typechecking.
The main zonking pass runs over the bindings
......@@ -195,7 +189,7 @@ data ZonkEnv
= ZonkEnv
UnboundTyVarZonker
(TyVarEnv TyVar) --
(IdEnv Var) -- What variables are in scope
(IdEnv Var) -- What variables are in scope
-- Maps an Id or EvVar to its zonked version; both have the same Name
-- Note that all evidence (coercion variables as well as dictionaries)
-- are kept in the ZonkEnv
......@@ -207,7 +201,10 @@ instance Outputable ZonkEnv where
emptyZonkEnv :: ZonkEnv
emptyZonkEnv = ZonkEnv zonkTypeZapping emptyVarEnv emptyVarEnv
emptyZonkEnv = mkEmptyZonkEnv zonkTypeZapping
mkEmptyZonkEnv :: UnboundTyVarZonker -> ZonkEnv
mkEmptyZonkEnv zonker = ZonkEnv zonker emptyVarEnv emptyVarEnv
extendIdZonkEnv :: ZonkEnv -> [Var] -> ZonkEnv
extendIdZonkEnv (ZonkEnv zonk_ty ty_env id_env) ids
......@@ -1041,7 +1038,7 @@ zonkRule env (HsRule name act (vars{-::[RuleBndr TcId]-}) lhs fv_lhs rhs fv_rhs)
; let final_bndrs :: [RuleBndr Var]
final_bndrs = map (RuleBndr . noLoc)
(varSetElemsKvsFirst unbound_tkvs)
(varSetElemsKvsFirst unbound_tkvs)
++ new_bndrs
; return $
......@@ -1249,37 +1246,58 @@ DV, TODO: followup on this note mentioning new examples I will add to perf/
\begin{code}
mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
-> (TcTyVar -> Type) -- What to do for an immutable var
-> TcTyVar -> TcM TcType
mkZonkTcTyVar unbound_mvar_fn unbound_ivar_fn
= zonk_tv
where
zonk_tv tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
SkolemTv {} -> return (unbound_ivar_fn tv)
RuntimeUnk {} -> return (unbound_ivar_fn tv)
FlatSkol ty -> zonkType zonk_tv ty
zonkTyVarOcc :: ZonkEnv -> TyVar -> TcM TcType
zonkTyVarOcc env@(ZonkEnv zonk_unbound_tyvar tv_env _) tv
| isTcTyVar tv
= case tcTyVarDetails tv of
SkolemTv {} -> lookup_in_env
RuntimeUnk {} -> lookup_in_env
FlatSkol ty -> zonkTcTypeToType env ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
Flexi -> do { kind <- {-# SCC "zonkKind1" #-}
zonkType zonk_tv (tyVarKind tv)
; unbound_mvar_fn (setTyVarKind tv kind) }
Indirect ty -> do { zty <- zonkType zonk_tv ty
zonkTcTypeToType env (tyVarKind tv)
; zonk_unbound_tyvar (setTyVarKind tv kind) }
Indirect ty -> do { zty <- zonkTcTypeToType env ty
-- Small optimisation: shortern-out indirect steps
-- so that the old type may be more easily collected.
; writeMutVar ref (Indirect zty)
; return zty } }
| otherwise
= lookup_in_env
where
lookup_in_env -- Look up in the env just as we do for Ids
= case lookupVarEnv tv_env tv of
Nothing -> return (mkTyVarTy tv)
Just tv' -> return (mkTyVarTy tv')
zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
zonkTcTypeToType (ZonkEnv zonk_unbound_tyvar tv_env _id_env)
= zonkType (mkZonkTcTyVar zonk_unbound_tyvar zonk_bound_tyvar)
zonkTcTypeToType env ty
= go ty
where
zonk_bound_tyvar tv -- Look up in the env just as we do for Ids
= case lookupVarEnv tv_env tv of
Nothing -> mkTyVarTy tv
Just tv' -> mkTyVarTy tv'
go (TyConApp tc tys) = do tys' <- mapM go tys
return (TyConApp tc tys')
go (LitTy n) = return (LitTy n)
go (FunTy arg res) = do arg' <- go arg
res' <- go res
return (FunTy arg' res')
go (AppTy fun arg) = do fun' <- go fun
arg' <- go arg
return (mkAppTy fun' arg')
-- NB the mkAppTy; we might have instantiated a
-- type variable to a type constructor, so we need
-- to pull the TyConApp to the top.
-- The two interesting cases!
go (TyVarTy tv) = zonkTyVarOcc env tv
go (ForAllTy tv ty) = ASSERT( isImmutableTyVar tv ) do
do { (env', tv') <- zonkTyBndrX env tv
; ty' <- zonkTcTypeToType env' ty
; return (ForAllTy tv' ty') }
zonkTcTypeToTypes :: ZonkEnv -> [TcType] -> TcM [Type]
zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
......
......@@ -24,7 +24,7 @@ module TcHsType (
-- Kind-checking types
-- No kind generalisation, no checkValidType
tcHsTyVarBndrs, tcHsTyVarBndrsGen ,
tcHsTyVarBndrs,
tcHsLiftedType,
tcLHsType, tcCheckLHsType,
tcHsContext, tcInferApps, tcHsArgTys,
......@@ -177,8 +177,8 @@ tcHsSigTypeNC ctxt (L loc hs_ty)
-- The kind is checked by checkValidType, and isn't necessarily
-- of kind * in a Template Haskell quote eg [t| Maybe |]
-- Generalise here: see Note [ generalisation]
; ty <- tcCheckHsTypeAndGen hs_ty kind
-- Generalise here: see Note [Kind generalisation]
-- Zonk to expose kind information to checkValidType
; ty <- zonkTcType ty
......@@ -826,28 +826,9 @@ tcHsTyVarBndr (L _ hs_tv)
{ kind <- case hs_tv of
UserTyVar {} -> newMetaKindVar
KindedTyVar _ (HsBSig kind _) -> tcLHsKind kind
; return (mkTyVar name kind) } } }
; return (mkTcTyVar name kind (SkolemTv False)) } } }
------------------
tcHsTyVarBndrsGen :: [LHsTyVarBndr Name]
-> TcM (TcTyVarSet, r) -- Result + free tyvars of thing inside
-> TcM ([TyVar], r) -- Generalised kind variables
-- + zonked tyvars + result result
-- tcHsTyVarBndrsGen [(f :: ?k -> *), (a :: ?k)] thing_inside
-- Returns with tyvars [(k :: BOX), (f :: k -> *), (a :: k)]
tcHsTyVarBndrsGen hs_tvs thing_inside
= do { traceTc "tcHsTyVarBndrsGen" (ppr hs_tvs)
; (tvs, (ftvs, res)) <- tcHsTyVarBndrs hs_tvs $ \ tvs ->
do { res <- thing_inside
; return (tvs, res) }
; let kinds = map tyVarKind tvs
; kvs' <- kindGeneralize (tyVarsOfTypes kinds `unionVarSet`
(ftvs `delVarSetList` tvs))
; zonked_kinds <- mapM zonkTcKind kinds
; let tvs' = zipWith setTyVarKind tvs zonked_kinds
-- See Note [Kinds of quantified type variables]
; traceTc "tcTyVarBndrsGen" (ppr (hs_tvs, kvs', tvs))
; return (kvs' ++ tvs', res) }
-------------------
kindGeneralize :: TyVarSet -> TcM [KindVar]
......@@ -856,6 +837,9 @@ kindGeneralize tkvs
; tidy_env <- tcInitTidyEnv
; tkvs <- zonkTyVarsAndFV tkvs
; let kvs_to_quantify = varSetElems (tkvs `minusVarSet` gbl_tvs)
-- Any type varaibles in tkvs will be in scope,
-- and hence in gbl_tvs, so after removing gbl_tvs
-- we should only have kind variables left
(_, tidy_kvs_to_quantify) = tidyTyVarBndrs tidy_env kvs_to_quantify
-- We do not get a later chance to tidy!
......@@ -1317,8 +1301,8 @@ tc_lhs_kind (L span ki) = setSrcSpan span (tc_hs_kind ki)
-- The main worker
tc_hs_kind :: HsKind Name -> TcM Kind
tc_hs_kind k@(HsTyVar _) = tc_app k []
tc_hs_kind k@(HsAppTy _ _) = tc_app k []
tc_hs_kind k@(HsTyVar _) = tc_kind_app k []
tc_hs_kind k@(HsAppTy _ _) = tc_kind_app k []
tc_hs_kind (HsParTy ki) = tc_lhs_kind ki
......@@ -1343,17 +1327,17 @@ tc_hs_kind (HsTupleTy _ kis) =
tc_hs_kind k = panic ("tc_hs_kind: " ++ showPpr k)
-- Special case for kind application
tc_app :: HsKind Name -> [LHsKind Name] -> TcM Kind
tc_app (HsAppTy ki1 ki2) kis = tc_app (unLoc ki1) (ki2:kis)
tc_app (HsTyVar tc) kis = do { arg_kis <- mapM tc_lhs_kind kis
; tc_var_app tc arg_kis }
tc_app ki _ = failWithTc (quotes (ppr ki) <+>
tc_kind_app :: HsKind Name -> [LHsKind Name] -> TcM Kind
tc_kind_app (HsAppTy ki1 ki2) kis = tc_kind_app (unLoc ki1) (ki2:kis)
tc_kind_app (HsTyVar tc) kis = do { arg_kis <- mapM tc_lhs_kind kis
; tc_kind_var_app tc arg_kis }
tc_kind_app ki _ = failWithTc (quotes (ppr ki) <+>
ptext (sLit "is not a kind constructor"))
tc_var_app :: Name -> [Kind] -> TcM Kind
tc_kind_var_app :: Name -> [Kind] -> TcM Kind
-- Special case for * and Constraint kinds
-- They are kinds already, so we don't need to promote them
tc_var_app name arg_kis
tc_kind_var_app name arg_kis
| name == liftedTypeKindTyConName
|| name == constraintKindTyConName
= do { unless (null arg_kis)
......@@ -1361,10 +1345,10 @@ tc_var_app name arg_kis
; thing <- tcLookup name
; case thing of
AGlobal (ATyCon tc) -> return (mkTyConApp tc [])
_ -> panic "tc_var_app 1" }
_ -> panic "tc_kind_var_app 1" }
-- General case
tc_var_app name arg_kis
tc_kind_var_app name arg_kis
= do { (_errs, mb_thing) <- tryTc (tcLookup name)
; case mb_thing of
Just (AGlobal (ATyCon tc))
......@@ -1378,11 +1362,16 @@ tc_var_app name arg_kis
Nothing -> err tc "is not promotable" }
-- A lexically scoped kind variable
-- Kind variables always have kind BOX, so cannot be applied to anything
Just (ATyVar _ kind_var)
| null arg_kis -> return (mkAppTys (mkTyVarTy kind_var) arg_kis)
| otherwise -> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr name)
<+> ptext (sLit "cannot appear in a function position"))
| not (isKindVar kind_var)
-> failWithTc (ptext (sLit "Type variable") <+> quotes (ppr kind_var)
<+> ptext (sLit "used bas a kind"))
| not (null arg_kis) -- Kind variables always have kind BOX,
-- so cannot be applied to anything
-> failWithTc (ptext (sLit "Kind variable") <+> quotes (ppr name)
<+> ptext (sLit "cannot appear in a function position"))
| otherwise
-> return (mkAppTys (mkTyVarTy kind_var) arg_kis)
-- It is in scope, but not what we expected
Just thing -> wrongThingErr "promoted type" thing name
......@@ -1391,7 +1380,7 @@ tc_var_app name arg_kis
Nothing
-> -- ASSERT2 ( isTyConName name, ppr name )
do { env <- getLclEnv
; traceTc "tc_var_app" (ppr name $$ ppr (tcl_env env))
; traceTc "tc_kind_var_app" (ppr name $$ ppr (tcl_env env))
; failWithTc (ptext (sLit "Promoted kind") <+>
quotes (ppr name) <+>
ptext (sLit "used in a mutually recursive group")) } }
......
......@@ -59,16 +59,15 @@ module TcMType (
--------------------------------
-- Zonking
zonkType, zonkKind, zonkTcPredType,
zonkTcPredType,
skolemiseSigTv, skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV,
zonkQuantifiedTyVar, zonkQuantifiedTyVars,
zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcKind, defaultKindVarToStar, zonkCt, zonkCts,
zonkImplication, zonkEvVar, zonkWC,
zonkImplication, zonkEvVar, zonkWC, zonkId,
zonkTcTypeAndSubst,
tcGetGlobalTyVars,
) where
......@@ -491,50 +490,10 @@ zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
----------------- Types
zonkTcType :: TcType -> TcM TcType
-- Simply look through all Flexis
zonkTcType ty = zonkType zonkTcTyVar ty
zonkTcTyVar :: TcTyVar -> TcM TcType
-- Simply look through all Flexis
zonkTcTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv ) do
case tcTyVarDetails tv of
SkolemTv {} -> zonk_kind_and_return
RuntimeUnk {} -> zonk_kind_and_return
FlatSkol ty -> zonkTcType ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
Flexi -> zonk_kind_and_return
Indirect ty -> zonkTcType ty }
where
zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
; return (TyVarTy z_tv) }
zonkTyVarKind :: TyVar -> TcM TyVar
zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
; return (setTyVarKind tv kind') }
zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
-- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
where
zonk_tv tv
= do { z_tv <- updateTyVarKindM zonkTcKind tv
; ASSERT ( isTcTyVar tv )
case tcTyVarDetails tv of
SkolemTv {} -> return (TyVarTy z_tv)
RuntimeUnk {} -> return (TyVarTy z_tv)
FlatSkol ty -> zonkType zonk_tv ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
Flexi -> zonk_flexi z_tv
Indirect ty -> zonkType zonk_tv ty } }
zonk_flexi tv
= case lookupTyVar subst tv of
Just ty -> zonkType zonk_tv ty
Nothing -> return (TyVarTy tv)
zonkTcTypes :: [TcType] -> TcM [TcType]
zonkTcTypes tys = mapM zonkTcType tys
......@@ -777,23 +736,25 @@ simplifier knows how to deal with.
%************************************************************************
%* *
\subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
\subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
%* *
%* For internal use only! *
%* *
%************************************************************************
\begin{code}
-- zonkId is used *during* typechecking just to zonk the Id's type
zonkId :: TcId -> TcM TcId
zonkId id
= do { ty' <- zonkTcType (idType id)
; return (Id.setIdType id ty') }
-- For unbound, mutable tyvars, zonkType uses the function given to it
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
-- type variable and zonks the kind too
zonkKind :: (TcTyVar -> TcM Kind) -> TcKind -> TcM Kind
zonkKind = zonkType
zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars
-> TcType -> TcM Type
zonkType zonk_tc_tyvar ty
zonkTcType :: TcType -> TcM TcType
zonkTcType ty
= go ty
where
go (TyConApp tc tys) = do tys' <- mapM go tys
......@@ -813,7 +774,7 @@ zonkType zonk_tc_tyvar ty
-- to pull the TyConApp to the top.
-- The two interesting cases!
go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
| otherwise = TyVarTy <$> updateTyVarKindM go tyvar
-- Ordinary (non Tc) tyvars occur inside quantified types
......@@ -821,6 +782,22 @@ zonkType zonk_tc_tyvar ty
ty' <- go ty
tyvar' <- updateTyVarKindM go tyvar
return (ForAllTy tyvar' ty')
zonkTcTyVar :: TcTyVar -> TcM TcType
-- Simply look through all Flexis
zonkTcTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv ) do
case tcTyVarDetails tv of
SkolemTv {} -> zonk_kind_and_return
RuntimeUnk {} -> zonk_kind_and_return
FlatSkol ty -> zonkTcType ty
MetaTv _ ref -> do { cts <- readMutVar ref
; case cts of
Flexi -> zonk_kind_and_return
Indirect ty -> zonkTcType ty }
where
zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
; return (TyVarTy z_tv) }
\end{code}
......
......@@ -757,17 +757,27 @@ tcFamTyPats fam_tc (HsBSig arg_pats (kvars, tvars)) kind_checker thing_inside
-- Kind-check and quantify
-- See Note [Quantifying over family patterns]
; (tkvs, typats) <- tcExtendTyVarEnv (map mkKindSigVar kvars) $
tcHsTyVarBndrsGen (map (noLoc . UserTyVar) tvars) $
do { typats <- tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds
; kind_checker res_kind
; return (tyVarsOfTypes typats, typats) }
; all_args' <- zonkTcTypeToTypes emptyZonkEnv (fam_arg_kinds ++ typats)
; res_kind' <- zonkTcTypeToType emptyZonkEnv res_kind
; traceTc "tcFamPats" (ppr tkvs $$ ppr all_args' $$ ppr res_kind')
; tcExtendTyVarEnv tkvs $
thing_inside tkvs all_args' res_kind' }
; typats <- tcExtendTyVarEnv (map mkKindSigVar kvars) $
tcHsTyVarBndrs (map (noLoc . UserTyVar) tvars) $ \ _ ->
do { kind_checker res_kind
; tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds }
; let all_args = fam_arg_kinds ++ typats
-- Find free variables (after zonking)
; tkvs <- zonkTyVarsAndFV (tyVarsOfTypes all_args)
-- Turn them into skolems, so that we don't subsequently
-- replace a meta kind var with AnyK
; qtkvs <- zonkQuantifiedTyVars (varSetElems tkvs)
-- Zonk the patterns etc into the Type world
; (ze, qtkvs') <- zonkTyBndrsX emptyZonkEnv qtkvs
; all_args' <- zonkTcTypeToTypes ze all_args
; res_kind' <- zonkTcTypeToType ze res_kind
; traceTc "tcFamPats" (ppr qtkvs' $$ ppr all_args' $$ ppr res_kind')
; tcExtendTyVarEnv qtkvs' $
thing_inside qtkvs' all_args' res_kind' }
\end{code}
Note [Quantifying over family patterns]
......@@ -810,7 +820,7 @@ Then in the family instance we want to
Notice that in the third step we quantify over all the visibly-mentioned
type variables (a,b), but also over the implicitly mentioned kind varaibles
(k, k'). In this case one is bound explicitly but often there will be
none. The rold of the kind signature (a :: Maybe k) is to add a constraint
none. The role of the kind signature (a :: Maybe k) is to add a constraint
that 'a' must have that kind, and to bring 'k' into scope.
Note [Associated type instances]
......@@ -867,18 +877,18 @@ dataDeclChecks tc_name new_or_data stupid_theta cons
-- Check that the stupid theta is empty for a GADT-style declaration
; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
-- Check that a newtype has exactly one constructor
-- Do this before checking for empty data decls, so that
-- we don't suggest -XEmptyDataDecls for newtypes
; checkTc (new_or_data == DataType || isSingleton cons)
-- Check that a newtype has exactly one constructor
-- Do this before checking for empty data decls, so that
-- we don't suggest -XEmptyDataDecls for newtypes
; checkTc (new_or_data == DataType || isSingleton cons)
(newtypeConError tc_name (length cons))
-- Check that there's at least one condecl,
-- or else we're reading an hs-boot file, or -XEmptyDataDecls
; empty_data_decls <- xoptM Opt_EmptyDataDecls
; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file?
; checkTc (not (null cons) || empty_data_decls || is_boot)
(emptyConDeclsErr tc_name) }
-- Check that there's at least one condecl,
-- or else we're reading an hs-boot file, or -XEmptyDataDecls
; empty_data_decls <- xoptM Opt_EmptyDataDecls
; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file?
; checkTc (not (null cons) || empty_data_decls || is_boot)
(emptyConDeclsErr tc_name) }
-----------------------------------
tcConDecls :: NewOrData -> Bool -> TyCon -> ([TyVar], Type)
......@@ -895,46 +905,50 @@ tcConDecl :: NewOrData
tcConDecl new_or_data existential_ok rep_tycon res_tmpl -- Data types
con@(ConDecl { con_name = name
, con_qvars = tvs, con_cxt = ctxt
, con_details = details, con_res = res_ty })
, con_qvars = hs_tvs, con_cxt = hs_ctxt
, con_details = details, con_res = hs_res_ty })
= addErrCtxt (dataConCtxt name) $
do { traceTc "tcConDecl 1" (ppr name)
; (tvs', (ctxt', arg_tys', res_ty', is_infix, field_lbls, stricts))
<- tcHsTyVarBndrsGen tvs $
do { ctxt' <- tcHsContext ctxt
; (tvs, ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts)
<- tcHsTyVarBndrs hs_tvs $ \ tvs ->
do { ctxt <- tcHsContext hs_ctxt
; details' <- tcConArgs new_or_data details
; res_ty' <- tcConRes res_ty
; res_ty <- tcConRes hs_res_ty
; let (is_infix, field_lbls, btys') = details'
(arg_tys', stricts) = unzip btys'
ftvs = tyVarsOfTypes ctxt' `unionVarSet`
tyVarsOfTypes arg_tys' `unionVarSet`
case res_ty' of
ResTyH98 -> emptyVarSet
ResTyGADT ty -> tyVarsOfType ty
; return (ftvs, (ctxt', arg_tys', res_ty', is_infix, field_lbls, stricts)) }
-- Substitute, to account for the kind
-- unifications done by tcHsTyVarBndrsGen
; traceTc "tcConDecl 2" (ppr name)
; let ze = mkTyVarZonkEnv tvs'
; arg_tys' <- zonkTcTypeToTypes ze arg_tys'
; ctxt' <- zonkTcTypeToTypes ze ctxt'
; res_ty' <- case res_ty' of
ResTyH98 -> return ResTyH98
ResTyGADT ty -> ResTyGADT <$> zonkTcTypeToType ze ty
(arg_tys, stricts) = unzip btys'
; return (tvs, ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts) }
; let pretend_res_ty = case res_ty of
ResTyH98 -> unitTy
ResTyGADT ty -> ty
pretend_con_ty = mkSigmaTy tvs ctxt (mkFunTys arg_tys pretend_res_ty)
-- This pretend_con_ty stuff is just a convenient way to get the
-- free kind variables of the type, for kindGeneralize to work on
-- Generalise the kind variables (returning quantifed TcKindVars)
-- and quanify the type variables (substiting their kinds)
; kvs <- kindGeneralize (tyVarsOfType pretend_con_ty)
; tvs <- zonkQuantifiedTyVars tvs
-- Zonk to Types
; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv (kvs ++ tvs)
; arg_tys <- zonkTcTypeToTypes ze arg_tys
; ctxt <- zonkTcTypeToTypes ze ctxt
; res_ty <- case res_ty of
ResTyH98 -> return ResTyH98
ResTyGADT ty -> ResTyGADT <$> zonkTcTypeToType ze ty
; checkTc (existential_ok || conRepresentibleWithH98Syntax con)
(badExistential name)
; let (univ_tvs, ex_tvs, eq_preds, res_ty'')
= rejigConRes res_tmpl tvs' res_ty'
; let (univ_tvs, ex_tvs, eq_preds, res_ty')
= rejigConRes res_tmpl qtkvs res_ty
; traceTc "tcConDecl 3" (ppr name)
; buildDataCon (unLoc name) is_infix
stricts field_lbls
univ_tvs ex_tvs eq_preds ctxt' arg_tys'
res_ty'' rep_tycon
univ_tvs ex_tvs eq_preds ctxt arg_tys
res_ty' rep_tycon
-- NB: we put data_tc, the type constructor gotten from the
-- constructor type signature into the data constructor;
-- that way checkValidDataCon can complain if it's wrong.
......@@ -1418,9 +1432,9 @@ checkValidClass cls
-- type variable. What a mess!
check_at_defs (fam_tc, defs)
= do mapM_ (\(ATD _tvs pats rhs _loc) -> checkValidFamInst pats rhs) defs
tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $
mapM_ (check_loc_at_def fam_tc) defs
= do { mapM_ (\(ATD _tvs pats rhs _loc) -> checkValidFamInst pats rhs) defs
; tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $
mapM_ (check_loc_at_def fam_tc) defs }
check_loc_at_def fam_tc (ATD _tvs pats _rhs loc)
-- Set the location for each of the default declarations
......
......@@ -1087,8 +1087,12 @@ unifyKind :: TcKind -- k1 (actual)
-> TcM Ordering -- Returns the relation between the kinds
-- LT <=> k1 is a sub-kind of k2
unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2
unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1
-- unifyKind deals with the top-level sub-kinding story
-- but recurses into the simpler unifyKindEq for any sub-terms
-- The sub-kinding stuff only applies at top level
unifyKind (TyVarTy kv1) k2 = uKVar False unifyKind EQ kv1 k2
unifyKind k1 (TyVarTy kv2) = uKVar True unifyKind EQ kv2 k1
unifyKind k1 k2 -- See Note [Expanding synonyms during unification]
| Just k1' <- tcView k1 = unifyKind k1' k2
......@@ -1103,24 +1107,44 @@ unifyKind k1@(TyConApp kc1 []) k2@(TyConApp kc2 [])
unifyKind k1 k2 = do { unifyKindEq k1 k2; return EQ }
-- In all other cases, let unifyKindEq do the work
uKVar :: Bool -> MetaKindVar -> TcKind -> TcM Ordering
uKVar isFlipped kv1 k2
| isMetaTyVar kv1
uKVar :: Bool -> (TcKind -> TcKind -> TcM a) -> a
-> MetaKindVar -> TcKind -> TcM a
uKVar isFlipped unify_kind eq_res kv1 k2
| isTcTyVar kv1, isMetaTyVar kv1 -- See Note [Unifying kind variables]
= do { mb_k1 <- readMetaTyVar kv1
; case mb_k1 of
Flexi -> uUnboundKVar kv1 k2 >> return EQ
Indirect k1 -> unifyKind k1 k2 }
| TyVarTy kv2 <- k2, isMetaTyVar kv2
= uKVar (not isFlipped) kv2 (TyVarTy kv1)
| TyVarTy kv2 <- k2, kv1 == kv2 = return EQ
Flexi -> do { uUnboundKVar kv1 k2; return eq_res }
Indirect k1 -> if isFlipped then unify_kind k2 k1
else unify_kind k1 k2 }
| TyVarTy kv2 <- k2, kv1 == kv2
= return eq_res
| TyVarTy kv2 <- k2, isTcTyVar kv1, isMetaTyVar kv2
= uKVar (not isFlipped) unify_kind eq_res kv2 (TyVarTy kv1)
| otherwise = if isFlipped
then unifyKindMisMatch k2 (TyVarTy kv1)
else unifyKindMisMatch (TyVarTy kv1) k2
{- Note [Unifying kind variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Rather hackily, kind variables can be TyVars not just TcTyVars.
Main reason is in
data instance T (D (x :: k)) = ...con-decls...
Here we bring into scope a kind variable 'k', and use it in the
con-decls. BUT the con-decls will be finished and frozen, and
are not amenable to subsequent substitution, so it makes sense
to have the *final* kind-variable (a KindVar, not a TcKindVar) in
scope. So at least during kind unification we can encounter a
KindVar.
Hence the isTcTyVar tests before using isMetaTyVar.
-}
---------------------------
unifyKindEq :: TcKind -> TcKind -> TcM ()
unifyKindEq (TyVarTy kv1) k2 = uKVarEq False kv1 k2
unifyKindEq k1 (TyVarTy kv2) = uKVarEq True kv2 k1
unifyKindEq (TyVarTy kv1) k2 = uKVar False unifyKindEq () kv1 k2
unifyKindEq k1 (TyVarTy kv2) = uKVar True unifyKindEq () kv2 k1
unifyKindEq (FunTy a1 r1) (FunTy a2 r2)
= do { unifyKindEq a1 a2; unifyKindEq r1 r2 }
......@@ -1134,28 +1158,11 @@ unifyKindEq (TyConApp kc1 k1s) (TyConApp kc2 k2s)
unifyKindEq k1 k2 = unifyKindMisMatch k1 k2
----------------
-- For better error messages, we record whether we've flipped the kinds
-- during the process.
uKVarEq :: Bool -> MetaKindVar -> TcKind -> TcM ()
uKVarEq isFlipped kv1 k2
| isMetaTyVar kv1
= do { mb_k1 <- readMetaTyVar kv1
; case mb_k1 of
Flexi -> uUnboundKVar kv1 k2
Indirect k1 -> unifyKindEq k1 k2 }
| TyVarTy kv2 <- k2, isMetaTyVar kv2
= uKVarEq (not isFlipped) kv2 (TyVarTy kv1)
| TyVarTy kv2 <- k2, kv1 == kv2 = return ()
| otherwise = if isFlipped
then unifyKindMisMatch k2 (TyVarTy kv1)
else unifyKindMisMatch (TyVarTy kv1) k2
----------------
uUnboundKVar :: MetaKindVar -> TcKind -> TcM ()
uUnboundKVar kv1 k2@(TyVarTy kv2)
| kv1 == kv2 = return ()
| isMetaTyVar kv2 -- Distinct kind variables
| isTcTyVar kv2, isMetaTyVar kv2 -- Distinct kind variables
= do { mb_k2 <- readMetaTyVar kv2
; case mb_k2 of
Indirect k2 -> uUnboundKVar kv1 k2
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment