Commit 75bf11c0 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix binder visiblity for default methods

Trac #13998 showed that default methods were getting bogus tyvar
binder visiblity info; and that it matters in the code genreated
by the default-method fill-in mechanism

* The actual fix: in TcTyDecls.mkDefaultMethodType, make TyVarBinders
  with the right visibility info by getting TyConBinders from the
  class TyCon.  (Previously we made up visiblity info, but that
  caused #13998.)

* Define TyCon.tyConTyVarBinders :: [TyConBinder] -> [TyVarBinder]
  which can build correct forall binders for
    a) default methods (Trac #13998)
    b) data constructors
  This was originally BuildTyCl.mkDataConUnivTyVarBinders

* Move mkTyVarBinder, mkTyVarBinders from Type to Var
parent 746ab0b4
......@@ -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)
{-
************************************************************************
* *
......
......@@ -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
......
......@@ -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,
......
......@@ -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
......
......@@ -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
......
......@@ -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)
{-
************************************************************************
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
{-# 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
......@@ -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, [''])
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