Fix binder visiblity for default methods
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 26 Jul 2017 07:51:47 +0000 (08:51 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 26 Jul 2017 11:33:42 +0000 (12:33 +0100)
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

13 files changed:
compiler/basicTypes/Var.hs
compiler/iface/BuildTyCl.hs
compiler/iface/TcIface.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcTyDecls.hs
compiler/typecheck/TcType.hs
compiler/types/Class.hs
compiler/types/TyCoRep.hs
compiler/types/TyCon.hs
compiler/types/Type.hs
testsuite/tests/deriving/should_compile/T13998.hs [new file with mode: 0644]
testsuite/tests/deriving/should_compile/all.T

index 87c4fe2..58e8d52 100644 (file)
@@ -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)
+
 {-
 ************************************************************************
 *                                                                      *
index 76b7793..a5b7249 100644 (file)
@@ -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
index 1477f46..418994d 100644 (file)
@@ -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,
index 8f99a23..36b6384 100644 (file)
@@ -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
index 4e7c99c..5acf207 100644 (file)
@@ -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
index 68e15fb..41482cc 100644 (file)
@@ -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)
 
 {-
 ************************************************************************
index e12b70b..00bcea2 100644 (file)
@@ -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
 
index ae1047e..b981a49 100644 (file)
@@ -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
 
index 5ac63e5..f5d3374 100644 (file)
@@ -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
index 1be318d..d717ba6 100644 (file)
@@ -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
index 8621e6c..0764d14 100644 (file)
@@ -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 (file)
index 0000000..565d4a3
--- /dev/null
@@ -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
index 7c7b290..0025d25 100644 (file)
@@ -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, [''])