Fix #14060 by more conservatively annotating TH-reified types
authorRyan Scott <ryan.gl.scott@gmail.com>
Tue, 15 Aug 2017 00:53:57 +0000 (20:53 -0400)
committerBen Gamari <ben@smart-cactus.org>
Tue, 15 Aug 2017 01:32:11 +0000 (21:32 -0400)
Before, TH was quite generous in applying kind annotations to reified
type constructors whose result kind happened to mention type variables.
This could result in agonizingly large reified types, so this patch aims
to quell this a bit by adopting a more nuanced algorithm for determining
when a tycon application deserves a kind annotation.

This implements the algorithm laid out in
https://ghc.haskell.org/trac/ghc/ticket/14060#comment:1. I've updated
`Note [Kind annotations on TyConApps]` to reflect the new wisdom.
Essentially, instead of only checking if the result kind contains free
variables, we also check if any of those variables do not appear free in
injective positions in the argument kinds—only then do we put on a kind
annotation.

Bumps `haddock` submodule.

Test Plan: make test TEST=T14060

Reviewers: goldfire, austin, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie

GHC Trac Issues: #14060

Differential Revision: https://phabricator.haskell.org/D3807

15 files changed:
compiler/iface/MkIface.hs
compiler/typecheck/FamInst.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcValidity.hs
compiler/types/TyCon.hs
compiler/types/Unify.hs
testsuite/tests/th/T12403.stdout
testsuite/tests/th/T12478_1.stdout
testsuite/tests/th/T14060.hs [new file with mode: 0644]
testsuite/tests/th/T14060.stdout [new file with mode: 0644]
testsuite/tests/th/T8953.stderr
testsuite/tests/th/all.T
utils/haddock

index 78787c9..94ace18 100644 (file)
@@ -1565,7 +1565,7 @@ tyConToIfaceDecl env tycon
                     ifFamFlav = to_if_fam_flav fam_flav,
                     ifBinders = if_binders,
                     ifResKind = if_res_kind,
-                    ifFamInj  = familyTyConInjectivityInfo tycon
+                    ifFamInj  = tyConInjectivityInfo tycon
                   })
 
   | isAlgTyCon tycon
index 87a602c..a869ff4 100644 (file)
@@ -720,7 +720,7 @@ checkForInjectivityConflicts :: FamInstEnvs -> FamInst -> TcM Bool
 checkForInjectivityConflicts instEnvs famInst
     | isTypeFamilyTyCon tycon
     -- type family is injective in at least one argument
-    , Injective inj <- familyTyConInjectivityInfo tycon = do
+    , Injective inj <- tyConInjectivityInfo tycon = do
     { let axiom = coAxiomSingleBranch fi_ax
           conflicts = lookupFamInstEnvInjectivityConflicts inj instEnvs famInst
           -- see Note [Verifying injectivity annotation] in FamInstEnv
@@ -808,7 +808,7 @@ injTyVarsOfType (TyVarTy v)
   = unitVarSet v `unionVarSet` injTyVarsOfType (tyVarKind v)
 injTyVarsOfType (TyConApp tc tys)
   | isTypeFamilyTyCon tc
-   = case familyTyConInjectivityInfo tc of
+   = case tyConInjectivityInfo tc of
         NotInjective  -> emptyVarSet
         Injective inj -> injTyVarsOfTypes (filterByList inj tys)
   | otherwise
index 69e84a4..cbe24ca 100644 (file)
@@ -1174,7 +1174,7 @@ improveLocalFunEqs work_ev inerts fam_tc args fsk
     rhs           = lookupFlattenTyVar ieqs fsk
     work_loc      = ctEvLoc work_ev
     work_pred     = ctEvPred work_ev
-    fam_inj_info  = familyTyConInjectivityInfo fam_tc
+    fam_inj_info  = tyConInjectivityInfo fam_tc
 
     --------------------
     improvement_eqns :: [FunDepEqn CtLoc]
@@ -1743,7 +1743,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
 
   -- see Note [Type inference for type families with injectivity]
   | isOpenTypeFamilyTyCon fam_tc
-  , Injective injective_args <- familyTyConInjectivityInfo fam_tc
+  , Injective injective_args <- tyConInjectivityInfo fam_tc
   , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc
   = -- it is possible to have several compatible equations in an open type
     -- family but we only want to derive equalities from one such equation.
@@ -1755,7 +1755,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
          take 1 improvs }
 
   | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
-  , Injective injective_args <- familyTyConInjectivityInfo fam_tc
+  , Injective injective_args <- tyConInjectivityInfo fam_tc
   = concatMapM (injImproveEqns injective_args) $
     buildImprovementData (fromBranches (co_ax_branches ax))
                          cab_tvs cab_lhs cab_rhs Just
index ff20e30..8189a78 100644 (file)
@@ -1028,8 +1028,8 @@ checkBootTyCon is_boot tc1 tc2
             = eqClosedFamilyAx ax1 ax2
         eqFamFlav (BuiltInSynFamTyCon {}) (BuiltInSynFamTyCon {}) = tc1 == tc2
         eqFamFlav _ _ = False
-        injInfo1 = familyTyConInjectivityInfo tc1
-        injInfo2 = familyTyConInjectivityInfo tc2
+        injInfo1 = tyConInjectivityInfo tc1
+        injInfo2 = tyConInjectivityInfo tc2
     in
     -- check equality of roles, family flavours and injectivity annotations
     -- (NB: Type family roles are always nominal. But the check is
index 77c97f7..6df78f8 100644 (file)
@@ -52,6 +52,7 @@ import GHCi
 import HscMain
         -- These imports are the reason that TcSplice
         -- is very high up the module hierarchy
+import FV
 import RnSplice( traceSplice, SpliceInfo(..) )
 import RdrName
 import HscTypes
@@ -97,7 +98,7 @@ import GHC.Serialized
 import ErrUtils
 import Util
 import Unique
-import VarSet           ( isEmptyVarSet, filterVarSet, mkVarSet, elemVarSet )
+import VarSet
 import Data.List        ( find )
 import Data.Maybe
 import FastString
@@ -1380,7 +1381,7 @@ reifyTyCon tc
                    Nothing   -> (TH.KindSig kind', Nothing)
                    Just name ->
                      let thName   = reifyName name
-                         injAnnot = familyTyConInjectivityInfo tc
+                         injAnnot = tyConInjectivityInfo tc
                          sig = TH.TyVarSig (TH.KindedTV thName kind')
                          inj = case injAnnot of
                                  NotInjective -> Nothing
@@ -1682,7 +1683,7 @@ reifyType (AppTy t1 t2)     = do { [r1,r2] <- reifyTypes [t1,t2] ; return (r1 `T
 reifyType ty@(FunTy t1 t2)
   | isPredTy t1 = reify_for_all ty  -- Types like ((?x::Int) => Char -> Char)
   | otherwise   = do { [r1,r2] <- reifyTypes [t1,t2] ; return (TH.ArrowT `TH.AppT` r1 `TH.AppT` r2) }
-reifyType ty@(CastTy {})    = noTH (sLit "kind casts") (ppr ty)
+reifyType (CastTy t _)      = reifyType t -- Casts are ignored in TH
 reifyType ty@(CoercionTy {})= noTH (sLit "coercions in types") (ppr ty)
 
 reify_for_all :: TyCoRep.Type -> TcM TH.Type
@@ -1779,13 +1780,67 @@ For example:
    type instance F Bool = (Proxy :: (* -> *) -> *)
 
 It's hard to figure out where these annotations should appear, so we do this:
-Suppose the tycon is applied to n arguments. We strip off the first n
-arguments of the tycon's kind. If there are any variables left in the result
-kind, we put on a kind annotation. But we must be slightly careful: it's
-possible that the tycon's kind will have fewer than n arguments, in the case
-that the concrete application instantiates a result kind variable with an
-arrow kind. So, if we run out of arguments, we conservatively put on a kind
-annotation anyway. This should be a rare case, indeed. Here is an example:
+Suppose we have a tycon application (T ty1 ... tyn). Assuming that T is not
+oversatured (more on this later), we can assume T's declaration is of the form
+T (tvb1 :: s1) ... (tvbn :: sn) :: p. If any kind variable that
+is free in p is not free in an injective position in tvb1 ... tvbn,
+then we put on a kind annotation, since we would not otherwise be able to infer
+the kind of the whole tycon application.
+
+The injective positions in a tyvar binder are the injective positions in the
+kind of its tyvar, provided the tyvar binder is either:
+
+* Anonymous. For example, in the promoted data constructor '(:):
+
+    '(:) :: forall a. a -> [a] -> [a]
+
+  The second and third tyvar binders (of kinds `a` and `[a]`) are both
+  anonymous, so if we had '(:) 'True '[], then the inferred kinds of 'True and
+  '[] would contribute to the inferred kind of '(:) 'True '[].
+* Has required visibility. For example, in the type family:
+
+    type family Wurble k (a :: k) :: k
+    Wurble :: forall k -> k -> k
+
+  The first tyvar binder (of kind `forall k`) has required visibility, so if
+  we had Wurble (Maybe a) Nothing, then the inferred kind of Maybe a would
+  contribute to the inferred kind of Wurble (Maybe a) Nothing.
+
+An injective position in a type is one that does not occur as an argument to
+a non-injective type constructor (e.g., non-injective type families). See
+injectiveVarsOfType.
+
+How can be sure that this is correct? That is, how can we be sure that in the
+event that we leave off a kind annotation, that one could infer the kind of the
+tycon application from its arguments? It's essentially a proof by induction: if
+we can infer the kinds of every subtree of a type, then the whole tycon
+application will have an inferrable kind--unless, of course, the remainder of
+the tycon application's kind has uninstantiated kind variables.
+
+An earlier implementation of this algorithm only checked if p contained any
+free variables. But this was unsatisfactory, since a datatype like this:
+
+  data Foo = Foo (Proxy '[False, True])
+
+Would be reified like this:
+
+  data Foo = Foo (Proxy ('(:) False ('(:) True ('[] :: [Bool])
+                                     :: [Bool]) :: [Bool]))
+
+Which has a rather excessive amount of kind annotations. With the current
+algorithm, we instead reify Foo to this:
+
+  data Foo = Foo (Proxy ('(:) False ('(:) True ('[] :: [Bool]))))
+
+Since in the case of '[], the kind p is [a], and there are no arguments in the
+kind of '[]. On the other hand, in the case of '(:) True '[], the kind p is
+(forall a. [a]), but a occurs free in the first and second arguments of the
+full kind of '(:), which is (forall a. a -> [a] -> [a]). (See Trac #14060.)
+
+What happens if T is oversaturated? That is, if T's kind has fewer than n
+arguments, in the case that the concrete application instantiates a result
+kind variable with an arrow kind? If we run out of arguments, we do not attach
+a kind annotation. This should be a rare case, indeed. Here is an example:
 
    data T1 :: k1 -> k2 -> *
    data T2 :: k1 -> k2 -> *
@@ -1799,10 +1854,14 @@ Here G's kind is (forall k. k -> k), and the desugared RHS of that last
 instance of F is (G (* -> (* -> *) -> *) (T1 * (* -> *)) Bool). According to
 the algorithm above, there are 3 arguments to G so we should peel off 3
 arguments in G's kind. But G's kind has only two arguments. This is the
-rare special case, and we conservatively choose to put the annotation
-in.
+rare special case, and we choose not to annotate the application of G with
+a kind signature. After all, we needn't do this, since that instance would
+be reified as:
 
-See #8953 and test th/T8953.
+   type instance F Char = G (T1 :: * -> (* -> *) -> *) Bool
+
+So the kind of G isn't ambiguous anymore due to the explicit kind annotation
+on its argument. See #8953 and test th/T8953.
 -}
 
 reify_tc_app :: TyCon -> [Type.Type] -> TcM TH.Type
@@ -1841,12 +1900,45 @@ reify_tc_app tc tys
 
     needs_kind_sig
       | GT <- compareLength tys tc_binders
-      = tcIsTyVarTy tc_res_kind
+      = False
       | otherwise
-      = not . isEmptyVarSet $
-        filterVarSet isTyVar $
-        tyCoVarsOfType $
-        mkTyConKind (dropList tys tc_binders) tc_res_kind
+      = let (dropped_binders, remaining_binders)
+              = splitAtList  tys tc_binders
+            result_kind  = mkTyConKind remaining_binders tc_res_kind
+            result_vars  = tyCoVarsOfType result_kind
+            dropped_vars = fvVarSet $
+                           mapUnionFV injectiveVarsOfBinder dropped_binders
+
+        in not (subVarSet result_vars dropped_vars)
+
+    injectiveVarsOfBinder :: TyConBinder -> FV
+    injectiveVarsOfBinder (TvBndr tv vis) =
+      case vis of
+        AnonTCB           -> injectiveVarsOfType (tyVarKind tv)
+        NamedTCB Required -> FV.unitFV tv `unionFV`
+                             injectiveVarsOfType (tyVarKind tv)
+        NamedTCB _        -> emptyFV
+
+    injectiveVarsOfType :: Type -> FV
+    injectiveVarsOfType = go
+      where
+        go ty                | Just ty' <- coreView ty
+                             = go ty'
+        go (TyVarTy v)       = FV.unitFV v `unionFV` go (tyVarKind v)
+        go (AppTy f a)       = go f `unionFV` go a
+        go (FunTy ty1 ty2)   = go ty1 `unionFV` go ty2
+        go (TyConApp tc tys) =
+          case tyConInjectivityInfo tc of
+            NotInjective  -> emptyFV
+            Injective inj -> mapUnionFV go $
+                             filterByList (inj ++ repeat True) tys
+                             -- Oversaturated arguments to a tycon are
+                             -- always injective, hence the repeat True
+        go (ForAllTy tvb ty) = tyCoFVsBndr tvb $ go (tyVarKind (binderVar tvb))
+                                                 `unionFV` go ty
+        go LitTy{}           = emptyFV
+        go (CastTy ty _)     = go ty
+        go CoercionTy{}      = emptyFV
 
 reifyPred :: TyCoRep.PredType -> TcM TH.Pred
 reifyPred ty
index d8e2519..bd4938e 100644 (file)
@@ -1614,7 +1614,7 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
        ; foldlM_ check_branch_compat [] branch_list }
   where
     branch_list = fromBranches branches
-    injectivity = familyTyConInjectivityInfo fam_tc
+    injectivity = tyConInjectivityInfo fam_tc
 
     check_branch_compat :: [CoAxBranch]    -- previous branches in reverse order
                         -> CoAxBranch      -- current branch
index 95207c4..63e199c 100644 (file)
@@ -59,7 +59,7 @@ module TyCon(
         isFamilyTyCon, isOpenFamilyTyCon,
         isTypeFamilyTyCon, isDataFamilyTyCon,
         isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
-        familyTyConInjectivityInfo,
+        tyConInjectivityInfo,
         isBuiltInSynFamTyCon_maybe,
         isUnliftedTyCon,
         isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs,
@@ -1925,11 +1925,17 @@ isClosedSynFamilyTyConWithAxiom_maybe
   (FamilyTyCon {famTcFlav = ClosedSynFamilyTyCon mb}) = mb
 isClosedSynFamilyTyConWithAxiom_maybe _               = Nothing
 
--- | Try to read the injectivity information from a FamilyTyCon.
--- For every other TyCon this function panics.
-familyTyConInjectivityInfo :: TyCon -> Injectivity
-familyTyConInjectivityInfo (FamilyTyCon { famTcInj = inj }) = inj
-familyTyConInjectivityInfo _ = panic "familyTyConInjectivityInfo"
+-- | @'tyConInjectivityInfo' tc@ returns @'Injective' is@ is @tc@ is an
+-- injective tycon (where @is@ states for which 'tyConBinders' @tc@ is
+-- injective), or 'NotInjective' otherwise.
+tyConInjectivityInfo :: TyCon -> Injectivity
+tyConInjectivityInfo tc
+  | FamilyTyCon { famTcInj = inj } <- tc
+  = inj
+  | isInjectiveTyCon tc Nominal
+  = Injective (replicate (tyConArity tc) True)
+  | otherwise
+  = NotInjective
 
 isBuiltInSynFamTyCon_maybe :: TyCon -> Maybe BuiltInSynFamily
 isBuiltInSynFamTyCon_maybe
index c9c78f7..80cccb3 100644 (file)
@@ -804,7 +804,7 @@ unify_ty env ty1 ty2 _kco
   = if isInjectiveTyCon tc1 Nominal
     then unify_tys env tys1 tys2
     else do { let inj | isTypeFamilyTyCon tc1
-                      = case familyTyConInjectivityInfo tc1 of
+                      = case tyConInjectivityInfo tc1 of
                                NotInjective -> repeat False
                                Injective bs -> bs
                       | otherwise
index 386b1c0..9b75e8b 100644 (file)
@@ -1,5 +1 @@
-data Main.T
-    = Main.T ((# , #) GHC.Types.Int
-                      GHC.Types.Int :: GHC.Prim.TYPE (GHC.Types.TupleRep ((GHC.Types.:) GHC.Types.LiftedRep
-                                                                                        ((GHC.Types.:) GHC.Types.LiftedRep
-                                                                                                       GHC.Types.[]))))
+data Main.T = Main.T ((# , #) GHC.Types.Int GHC.Types.Int)
index f94db59..8437f92 100644 (file)
@@ -1 +1 @@
-TyConI (DataD [] Main.T [] Nothing [NormalC Main.T [(Bang NoSourceUnpackedness NoSourceStrictness,SigT (AppT (AppT (UnboxedSumT 2) (ConT GHC.Types.Int)) (ConT GHC.Types.Char)) (AppT (ConT GHC.Prim.TYPE) (AppT (ConT GHC.Types.SumRep) (AppT (AppT (ConT GHC.Types.:) (ConT GHC.Types.LiftedRep)) (AppT (AppT (ConT GHC.Types.:) (ConT GHC.Types.LiftedRep)) (ConT GHC.Types.[]))))))]] [])
+TyConI (DataD [] Main.T [] Nothing [NormalC Main.T [(Bang NoSourceUnpackedness NoSourceStrictness,AppT (AppT (UnboxedSumT 2) (ConT GHC.Types.Int)) (ConT GHC.Types.Char))]] [])
diff --git a/testsuite/tests/th/T14060.hs b/testsuite/tests/th/T14060.hs
new file mode 100644 (file)
index 0000000..5527b25
--- /dev/null
@@ -0,0 +1,38 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeInType #-}
+module Main where
+
+import Data.Kind
+import Data.Proxy
+import Language.Haskell.TH hiding (Type)
+
+-- Anonymous tyvar binder example
+newtype Foo1 = Foo1 (Proxy '[False, True, False])
+
+-- Required (dependent) tyvar binder example
+type family Wurble k (a :: k) :: k
+newtype Foo2 a = Foo2 (Proxy (Wurble (Maybe a) Nothing))
+
+-- Non-injective type family example
+type family Foo3Fam1 (a :: Type) :: Type where
+  Foo3Fam1 a = a
+type family Foo3Fam2 (a :: Foo3Fam1 b) :: b
+newtype Foo3 = Foo3 (Proxy (Foo3Fam2 Int))
+
+-- Injective type family example
+type family Foo4Fam1 (a :: Type) = (r :: Type) | r -> a where
+  Foo4Fam1 a = a
+type family Foo4Fam2 (a :: Foo4Fam1 b) :: b
+newtype Foo4 = Foo4 (Proxy (Foo4Fam2 Int))
+
+$(return [])
+
+main :: IO ()
+main = do
+  putStrLn $(reify ''Foo1 >>= stringE . pprint)
+  putStrLn $(reify ''Foo2 >>= stringE . pprint)
+  putStrLn $(reify ''Foo3 >>= stringE . pprint)
+  putStrLn $(reify ''Foo4 >>= stringE . pprint)
diff --git a/testsuite/tests/th/T14060.stdout b/testsuite/tests/th/T14060.stdout
new file mode 100644 (file)
index 0000000..c7668cf
--- /dev/null
@@ -0,0 +1,11 @@
+newtype Main.Foo1
+  = Main.Foo1 (Data.Proxy.Proxy ('(:) 'GHC.Types.False
+                                      ('(:) 'GHC.Types.True
+                                            ('(:) 'GHC.Types.False ('[] :: [GHC.Types.Bool])))))
+newtype Main.Foo2 (a_0 :: *)
+  = Main.Foo2 (Data.Proxy.Proxy (Main.Wurble (GHC.Base.Maybe a_0)
+                                             ('GHC.Base.Nothing :: GHC.Base.Maybe a_0)))
+newtype Main.Foo3
+  = Main.Foo3 (Data.Proxy.Proxy (Main.Foo3Fam2 GHC.Types.Int :: *))
+newtype Main.Foo4
+  = Main.Foo4 (Data.Proxy.Proxy (Main.Foo4Fam2 GHC.Types.Int))
index c18589d..c724a8e 100644 (file)
@@ -11,9 +11,9 @@ class T8953.PC (a_0 :: k_1)
 instance T8953.PC (a_2 :: *)
 instance T8953.PC (Data.Proxy.Proxy :: (k_3 -> *) -> *)
 type family T8953.F (a_0 :: *) :: k_1
-type instance T8953.F GHC.Types.Char = (T8953.G (T8953.T1 :: * ->
-                                                             (* -> *) -> *)
-                                                GHC.Types.Bool :: (* -> *) -> *)
+type instance T8953.F GHC.Types.Char = T8953.G (T8953.T1 :: * ->
+                                                            (* -> *) -> *)
+                                               GHC.Types.Bool
 type family T8953.G (a_0 :: k_1) :: k_1
 type instance T8953.G (T8953.T1 :: k1_2 ->
                                    k2_3 -> *) = (T8953.T2 :: k1_2 -> k2_3 -> *)
index 29a6334..5d61fa4 100644 (file)
@@ -393,3 +393,4 @@ test('T13837', normal, compile_fail, ['-v0 -dsuppress-uniques'])
 test('T13856', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
 test('T13887', normal, compile_and_run, ['-v0'])
 test('T13968', normal, compile_fail, ['-v0'])
+test('T14060', normal, compile_and_run, ['-v0'])
index 7cecbd9..c8a01b8 160000 (submodule)
@@ -1 +1 @@
-Subproject commit 7cecbd969298d5aa576750864a69fa5f70f71c32
+Subproject commit c8a01b83be52e45d3890db173ffe7b09ccd4f351