diff options
| -rw-r--r-- | compiler/basicTypes/Var.hs | 11 | ||||
| -rw-r--r-- | compiler/iface/BuildTyCl.hs | 70 | ||||
| -rw-r--r-- | compiler/iface/TcIface.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcPatSyn.hs | 3 | ||||
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcTyDecls.hs | 14 | ||||
| -rw-r--r-- | compiler/typecheck/TcType.hs | 2 | ||||
| -rw-r--r-- | compiler/types/Class.hs | 4 | ||||
| -rw-r--r-- | compiler/types/TyCoRep.hs | 54 | ||||
| -rw-r--r-- | compiler/types/TyCon.hs | 72 | ||||
| -rw-r--r-- | compiler/types/Type.hs | 8 | ||||
| -rw-r--r-- | testsuite/tests/deriving/should_compile/T13998.hs | 43 | ||||
| -rw-r--r-- | testsuite/tests/deriving/should_compile/all.T | 1 |
13 files changed, 177 insertions, 109 deletions
diff --git a/compiler/basicTypes/Var.hs b/compiler/basicTypes/Var.hs index 87c4fe2240..58e8d525d0 100644 --- a/compiler/basicTypes/Var.hs +++ b/compiler/basicTypes/Var.hs @@ -64,6 +64,7 @@ module Var ( TyVarBndr(..), ArgFlag(..), TyVarBinder, binderVar, binderVars, binderArgFlag, binderKind, isVisibleArgFlag, isInvisibleArgFlag, sameVis, + mkTyVarBinder, mkTyVarBinders, -- ** Constructing TyVar's mkTyVar, mkTcTyVar, @@ -374,7 +375,7 @@ updateVarTypeM f id = do { ty' <- f (varType id) -- Is something required to appear in source Haskell ('Required'), -- permitted by request ('Specified') (visible type application), or -- prohibited entirely from appearing in source Haskell ('Inferred')? --- See Note [TyBinders and ArgFlags] in TyCoRep +-- See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility] in TyCoRep data ArgFlag = Required | Specified | Inferred deriving (Eq, Data) @@ -429,6 +430,14 @@ binderArgFlag (TvBndr _ argf) = argf binderKind :: TyVarBndr TyVar argf -> Kind binderKind (TvBndr tv _) = tyVarKind tv +-- | Make a named binder +mkTyVarBinder :: ArgFlag -> Var -> TyVarBinder +mkTyVarBinder vis var = TvBndr var vis + +-- | Make many named binders +mkTyVarBinders :: ArgFlag -> [TyVar] -> [TyVarBinder] +mkTyVarBinders vis = map (mkTyVarBinder vis) + {- ************************************************************************ * * diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs index 76b7793859..a5b724994c 100644 --- a/compiler/iface/BuildTyCl.hs +++ b/compiler/iface/BuildTyCl.hs @@ -6,7 +6,7 @@ {-# LANGUAGE CPP #-} module BuildTyCl ( - buildDataCon, mkDataConUnivTyVarBinders, + buildDataCon, buildPatSyn, TcMethInfo, buildClass, mkNewTyConRhs, mkDataTyConRhs, @@ -119,7 +119,6 @@ buildDataCon :: FamInstEnvs -- a) makes the worker Id -- b) makes the wrapper Id if necessary, including -- allocating its unique (hence monadic) --- c) Sorts out the TyVarBinders. See mkDataConUnivTyBinders buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs field_lbls univ_tvs ex_tvs eq_spec ctxt arg_tys res_ty rep_tycon = do { wrap_name <- newImplicitBinder src_name mkDataConWrapperOcc @@ -165,69 +164,6 @@ mkDataConStupidTheta tycon arg_tys univ_tvs tyCoVarsOfType pred `intersectVarSet` arg_tyvars -mkDataConUnivTyVarBinders :: [TyConBinder] -- From the TyCon - -> [TyVarBinder] -- For the DataCon --- See Note [Building the TyBinders for a DataCon] -mkDataConUnivTyVarBinders tc_bndrs - = map mk_binder tc_bndrs - where - mk_binder (TvBndr tv tc_vis) = mkTyVarBinder vis tv - where - vis = case tc_vis of - AnonTCB -> Specified - NamedTCB Required -> Specified - NamedTCB vis -> vis - -{- Note [Building the TyBinders for a DataCon] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A DataCon needs to keep track of the visibility of its universals and -existentials, so that visible type application can work properly. This -is done by storing the universal and existential TyVarBinders. -See Note [TyVarBinders in DataCons] in DataCon. - -During construction of a DataCon, we often start from the TyBinders of -the parent TyCon. For example - data Maybe a = Nothing | Just a -The DataCons start from the TyBinders of the parent TyCon. - -But the ultimate TyBinders for the DataCon are *different* than those -of the DataCon. Here is an example: - - data App a b = MkApp (a b) -- App :: forall {k}. (k->*) -> k -> * - -The TyCon has - - tyConTyVars = [ k:*, a:k->*, b:k] - tyConTyBinders = [ Named (TvBndr (k :: *) Inferred), Anon (k->*), Anon k ] - -The TyBinders for App line up with App's kind, given above. - -But the DataCon MkApp has the type - MkApp :: forall {k} (a:k->*) (b:k). a b -> App k a b - -That is, its TyBinders should be - - dataConUnivTyVarBinders = [ TvBndr (k:*) Inferred - , TvBndr (a:k->*) Specified - , TvBndr (b:k) Specified ] - -So we want to take the TyCon's TyBinders and the TyCon's TyVars and -merge them, pulling - - variable names from the TyVars - - visibilities from the TyBinders - - but changing Anon/Required to Specified - -The last part about Required->Specified comes from this: - data T k (a:k) b = MkT (a b) -Here k is Required in T's kind, but we don't have Required binders in -the TyBinders for a term (see Note [No Required TyBinder in terms] -in TyCoRep), so we change it to Specified when making MkT's TyBinders - -This merging operation is done by mkDataConUnivTyBinders. In contrast, -the TyBinders passed to mkDataCon are the final TyBinders stored in the -DataCon (mkDataCon does no further work). --} - ------------------------------------------------------ buildPatSyn :: Name -> Bool -> (Id,Bool) -> Maybe (Id, Bool) @@ -310,7 +246,7 @@ buildClass tycon_name binders roles fds Nothing do { traceIf (text "buildClass") ; tc_rep_name <- newTyConRepName tycon_name - ; let univ_bndrs = mkDataConUnivTyVarBinders binders + ; let univ_bndrs = tyConTyVarBinders binders univ_tvs = binderVars univ_bndrs tycon = mkClassTyCon tycon_name binders roles AbstractTyCon rec_clas tc_rep_name @@ -359,7 +295,7 @@ buildClass tycon_name binders roles fds op_names = [op | (op,_,_) <- sig_stuff] arg_tys = sc_theta ++ op_tys rec_tycon = classTyCon rec_clas - univ_bndrs = mkDataConUnivTyVarBinders binders + univ_bndrs = tyConTyVarBinders binders univ_tvs = binderVars univ_bndrs ; rep_nm <- newTyConRepName datacon_name diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs index 1477f462fc..418994d752 100644 --- a/compiler/iface/TcIface.hs +++ b/compiler/iface/TcIface.hs @@ -893,7 +893,7 @@ tcIfaceDataCons tycon_name tycon tc_tybinders if_cons ; mkNewTyConRhs tycon_name tycon data_con } where univ_tv_bndrs :: [TyVarBinder] - univ_tv_bndrs = mkDataConUnivTyVarBinders tc_tybinders + univ_tv_bndrs = tyConTyVarBinders tc_tybinders tc_con_decl (IfCon { ifConInfix = is_infix, ifConExTvs = ex_bndrs, diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 8f99a23b08..36b63842e3 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -15,8 +15,7 @@ module TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl import HsSyn import TcPat -import Type( mkTyVarBinders, mkEmptyTCvSubst - , tidyTyVarBinders, tidyTypes, tidyType ) +import Type( mkEmptyTCvSubst, tidyTyVarBinders, tidyTypes, tidyType ) import TcRnMonad import TcSigs( emptyPragEnv, completeSigFromId ) import TcEnv diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 4e7c99cde8..5acf207dc6 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -1564,7 +1564,7 @@ tcConDecl rep_tycon tmpl_bndrs res_tmpl ; buildDataCon fam_envs name is_infix rep_nm stricts Nothing field_lbls - (mkDataConUnivTyVarBinders tmpl_bndrs) + (tyConTyVarBinders tmpl_bndrs) ex_tvs [{- no eq_preds -}] ctxt arg_tys res_tmpl rep_tycon diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs index 68e15fbd48..41482cca8e 100644 --- a/compiler/typecheck/TcTyDecls.hs +++ b/compiler/typecheck/TcTyDecls.hs @@ -771,10 +771,18 @@ mkDefaultMethodIds tycons mkDefaultMethodType :: Class -> Id -> DefMethSpec Type -> Type -- Returns the top-level type of the default method mkDefaultMethodType _ sel_id VanillaDM = idType sel_id -mkDefaultMethodType cls _ (GenericDM dm_ty) = mkSpecSigmaTy cls_tvs [pred] dm_ty +mkDefaultMethodType cls _ (GenericDM dm_ty) = mkSigmaTy tv_bndrs [pred] dm_ty where - cls_tvs = classTyVars cls - pred = mkClassPred cls (mkTyVarTys cls_tvs) + pred = mkClassPred cls (mkTyVarTys (binderVars cls_bndrs)) + cls_bndrs = tyConBinders (classTyCon cls) + tv_bndrs = tyConTyVarBinders cls_bndrs + -- NB: the Class doesn't have TyConBinders; we reach into its + -- TyCon to get those. We /do/ need the TyConBinders because + -- we need the correct visiblity: these default methods are + -- used in code generated by the the fill-in for missing + -- methods in instances (TcInstDcls.mkDefMethBind), and + -- then typechecked. So we need the right visibilty info + -- (Trac #13998) {- ************************************************************************ diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index e12b70b6d1..00bcea263c 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -1728,7 +1728,7 @@ tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2 -- be oversaturated where bndrs = tyConBinders tc - viss = map (isVisibleArgFlag . tyConBinderArgFlag) bndrs + viss = map isVisibleTyConBinder bndrs tc_vis False _ = repeat False -- if we're not in a visible context, our args -- aren't either diff --git a/compiler/types/Class.hs b/compiler/types/Class.hs index ae1047ebde..b981a4998e 100644 --- a/compiler/types/Class.hs +++ b/compiler/types/Class.hs @@ -60,6 +60,10 @@ data Class classTyVars :: [TyVar], -- The class kind and type variables; -- identical to those of the TyCon + -- If you want visiblity info, look at the classTyCon + -- This field is redundant because it's duplicated in the + -- classTyCon, but classTyVars is used quite often, so maybe + -- it's a bit faster to cache it here classFunDeps :: [FunDep TyVar], -- The functional dependencies diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 5ac63e5b04..f5d33748e7 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -457,28 +457,38 @@ words, if `x` is either a function or a polytype, `x arg` makes sense (for an appropriate `arg`). -Note [TyBinders and ArgFlags] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A ForAllTy contains a TyVarBinder. Each TyVarBinder is equipped -with a ArgFlag, which says whether or not arguments for this -binder should be visible (explicit) in source Haskell. - ------------------------------------------------------------------------ - Occurrences look like this - TyBinder GHC displays type as in Haskell souce code ------------------------------------------------------------------------ -In the type of a term - Anon: f :: type -> type Arg required: f x - Named Inferred: f :: forall {a}. type Arg not allowed: f - Named Specified: f :: forall a. type Arg optional: f or f @Int - Named Required: Illegal: See Note [No Required TyBinder in terms] - -In the kind of a type - Anon: T :: kind -> kind Required: T * - Named Inferred: T :: forall {k}. kind Arg not allowed: T - Named Specified: T :: forall k. kind Arg not allowed[1]: T - Named Required: T :: forall k -> kind Required: T * ------------------------------------------------------------------------- +Note [TyVarBndrs, TyVarBinders, TyConBinders, and visiblity] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +* A ForAllTy (used for both types and kinds) contains a TyVarBinder. + Each TyVarBinder + TvBndr a tvis + is equipped with tvis::ArgFlag, which says whether or not arguments + for this binder should be visible (explicit) in source Haskell. + +* A TyCon contains a list of TyConBinders. Each TyConBinder + TvBndr a cvis + is equipped with cvis::TyConBndrVis, which says whether or not type + and kind arguments for this TyCon should be visible (explicit) in + source Haskell. + +This table summarises the visiblity rules: +--------------------------------------------------------------------------------------- +| Occurrences look like this +| GHC displays type as in Haskell souce code +|----------------------------------------------------------------------- +| TvBndr a tvis :: TyVarBinder, in the binder of ForAllTy for a term +| tvis :: ArgFlag +| tvis = Inferred: f :: forall {a}. type Arg not allowed: f +| tvis = Specified: f :: forall a. type Arg optional: f or f @Int +| tvis = Required: Illegal: See Note [No Required TyBinder in terms] +| +| TvBndr k cvis :: TyConBinder, in the TyConBinders of a TyCon +| cvis :: TyConBndrVis +| cvis = AnonTCB: T :: kind -> kind Required: T * +| cvis = NamedTCB Inferred: T :: forall {k}. kind Arg not allowed: T +| cvis = NamedTCB Specified: T :: forall k. kind Arg not allowed[1]: T +| cvis = NamedTCB Required: T :: forall k -> kind Required: T * +--------------------------------------------------------------------------------------- [1] In types, in the Specified case, it would make sense to allow optional kind applications, thus (T @*), but we have not diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs index 1be318d96a..d717ba66d3 100644 --- a/compiler/types/TyCon.hs +++ b/compiler/types/TyCon.hs @@ -94,7 +94,7 @@ module TyCon( newTyConDataCon_maybe, algTcFields, tyConRuntimeRepInfo, - tyConBinders, tyConResKind, + tyConBinders, tyConResKind, tyConTyVarBinders, tcTyConScopedTyVars, -- ** Manipulating TyCons @@ -428,6 +428,72 @@ mkTyConKind bndrs res_kind = foldr mk res_kind bndrs mk (TvBndr tv AnonTCB) k = mkFunKind (tyVarKind tv) k mk (TvBndr tv (NamedTCB vis)) k = mkForAllKind tv vis k +tyConTyVarBinders :: [TyConBinder] -- From the TyCon + -> [TyVarBinder] -- Suitable for the foralls of a term function +-- See Note [Building TyVarBinders from TyConBinders] +tyConTyVarBinders tc_bndrs + = map mk_binder tc_bndrs + where + mk_binder (TvBndr tv tc_vis) = mkTyVarBinder vis tv + where + vis = case tc_vis of + AnonTCB -> Specified + NamedTCB Required -> Specified + NamedTCB vis -> vis + +{- Note [Building TyVarBinders from TyConBinders] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We sometimes need to build the quantified type of a value from +the TyConBinders of a type or class. For that we need not +TyConBinders but TyVarBinders (used in forall-type) E.g: + + * From data T a = MkT (Maybe a) + we are going to make a data constructor with type + MkT :: forall a. Maybe a -> T a + See the TyVarBinders passed to buildDataCon + + * From class C a where { op :: a -> Maybe a } + we are going to make a default method + $dmop :: forall a. C a => a -> Maybe a + See the TyVarBindres passed to mkSigmaTy in mkDefaultMethodType + +Both of these are user-callable. (NB: default methods are not callable +directly by the user but rather via the code generated by 'deriving', +which uses visible type application; see mkDefMethBind.) + +Since they are user-callable we must get their type-argument visibility +information right; and that info is in the TyConBinders. +Here is an example: + + data App a b = MkApp (a b) -- App :: forall {k}. (k->*) -> k -> * + +The TyCon has + + tyConTyBinders = [ Named (TvBndr (k :: *) Inferred), Anon (k->*), Anon k ] + +The TyConBinders for App line up with App's kind, given above. + +But the DataCon MkApp has the type + MkApp :: forall {k} (a:k->*) (b:k). a b -> App k a b + +That is, its TyVarBinders should be + + dataConUnivTyVarBinders = [ TvBndr (k:*) Inferred + , TvBndr (a:k->*) Specified + , TvBndr (b:k) Specified ] + +So tyConTyVarBinders conversts TyCon's TyConBinders into TyVarBinders: + - variable names from the TyConBinders + - but changing Anon/Required to Specified + +The last part about Required->Specified comes from this: + data T k (a:k) b = MkT (a b) +Here k is Required in T's kind, but we don't have Required binders in +the TyBinders for a term (see Note [No Required TyBinder in terms] +in TyCoRep), so we change it to Specified when making MkT's TyBinders +-} + + {- Note [The binders/kind/arity fields of a TyCon] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ All TyCons have this group of fields @@ -451,8 +517,8 @@ They fit together like so: Note that that are three binders here, including the kind variable k. - See Note [TyBinders and ArgFlags] in TyCoRep for what - the visibility flag means. +- See Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility] in TyCoRep + for what the visibility flag means. * Each TyConBinder tyConBinders has a TyVar, and that TyVar may scope over some other part of the TyCon's definition. Eg diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 8621e6cd52..0764d144b7 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -1486,14 +1486,6 @@ isTauTy (CoercionTy _) = False -- Not sure about this %************************************************************************ -} --- | Make a named binder -mkTyVarBinder :: ArgFlag -> Var -> TyVarBinder -mkTyVarBinder vis var = TvBndr var vis - --- | Make many named binders -mkTyVarBinders :: ArgFlag -> [TyVar] -> [TyVarBinder] -mkTyVarBinders vis = map (mkTyVarBinder vis) - -- | Make an anonymous binder mkAnonBinder :: Type -> TyBinder mkAnonBinder = Anon diff --git a/testsuite/tests/deriving/should_compile/T13998.hs b/testsuite/tests/deriving/should_compile/T13998.hs new file mode 100644 index 0000000000..565d4a35f7 --- /dev/null +++ b/testsuite/tests/deriving/should_compile/T13998.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE GADTs #-} + +module T13998 where + +import Data.Type.Equality + +class EqForall f where + eqForall :: f a -> f a -> Bool + +class EqForall f => EqForallPoly f where + eqForallPoly :: f a -> f b -> Bool + default eqForallPoly :: TestEquality f => f a -> f b -> Bool + eqForallPoly = defaultEqForallPoly + +defaultEqForallPoly :: (TestEquality f, EqForall f) => f a -> f b -> Bool +defaultEqForallPoly x y = case testEquality x y of + Nothing -> False + Just Refl -> eqForall x y + + +data Atom = AtomInt | AtomString | AtomBool + +data Value (a :: Atom) where + ValueInt :: Int -> Value 'AtomInt + ValueString :: String -> Value 'AtomString + ValueBool :: Bool -> Value 'AtomBool + +instance TestEquality Value where + testEquality (ValueInt _) (ValueInt _) = Just Refl + testEquality (ValueString _) (ValueString _) = Just Refl + testEquality (ValueBool _) (ValueBool _) = Just Refl + testEquality _ _ = Nothing + +instance EqForall Value where + eqForall (ValueInt a) (ValueInt b) = a == b + eqForall (ValueString a) (ValueString b) = a == b + eqForall (ValueBool a) (ValueBool b) = a == b + +instance EqForallPoly Value diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T index 7c7b29070b..0025d25dee 100644 --- a/testsuite/tests/deriving/should_compile/all.T +++ b/testsuite/tests/deriving/should_compile/all.T @@ -93,3 +93,4 @@ test('drv-empty-data', [normalise_errmsg_fun(just_the_deriving)],compile, ['-ddu test('drv-phantom', [normalise_errmsg_fun(just_the_deriving)],compile, ['-ddump-deriv -dsuppress-uniques']) test('T13813', normal, compile, ['']) test('T13919', normal, compile, ['']) +test('T13998', normal, compile, ['']) |