[commit: ghc] wip/rae: Fix #12176 by being a bit more careful instantiating. (ba0598b)

git at git.haskell.org git at git.haskell.org
Wed Jul 19 12:04:08 UTC 2017


Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/rae
Link       : http://ghc.haskell.org/trac/ghc/changeset/ba0598b791359fb72e5c7c588ba0d5bcfcda1c42/ghc

>---------------------------------------------------------------

commit ba0598b791359fb72e5c7c588ba0d5bcfcda1c42
Author: Richard Eisenberg <rae at cs.brynmawr.edu>
Date:   Tue Jul 18 19:44:17 2017 -0400

    Fix #12176 by being a bit more careful instantiating.
    
    Previously, looking up a TyCon that said "no" to mightBeUnsaturated
    would then instantiate all of its invisible binders. But this is
    wrong for vanilla type synonyms, whose RHS kind might legitimately
    start with invisible binders. So a little more care is taken now,
    only to instantiate those invisible binders that need to be (so that
    the TyCon isn't unsaturated).


>---------------------------------------------------------------

ba0598b791359fb72e5c7c588ba0d5bcfcda1c42
 compiler/typecheck/TcCanonical.hs                  |  4 +-
 compiler/typecheck/TcHsType.hs                     | 50 ++++++++++++++--------
 testsuite/tests/dependent/should_compile/T12176.hs | 18 ++++++++
 testsuite/tests/dependent/should_compile/all.T     |  1 +
 4 files changed, 53 insertions(+), 20 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index e38c045..cb2becd 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -24,7 +24,7 @@ import FamInstEnv ( FamInstEnvs )
 import FamInst ( tcTopNormaliseNewTypeTF_maybe )
 import Var
 import VarEnv( mkInScopeSet )
-import VarSet( extendVarSetList )
+import VarSet
 import Outputable
 import DynFlags( DynFlags )
 import NameSet
@@ -683,7 +683,7 @@ can_eq_nc_forall ev eq_rel s1 s2
             go _ _ _ = panic "cna_eq_nc_forall"  -- case (s:ss) []
 
             empty_subst2 = mkEmptyTCvSubst $ mkInScopeSet $
-                           free_tvs2 `extendVarSetList` skol_tvs
+                           free_tvs2 `unionVarSet` closeOverKinds (mkVarSet skol_tvs)
 
       ; (implic, _ev_binds, all_co) <- buildImplication skol_info skol_tvs [] $
                                        go skol_tvs empty_subst2 bndrs2
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 205224c..a2e98a8 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -922,30 +922,42 @@ checkExpectedKind hs_ty ty act_kind exp_kind
                        , TcKind ) -- its new kind
     instantiate ty act_ki exp_ki
       = let (exp_bndrs, _) = splitPiTysInvisible exp_ki in
-        instantiateTyN (length exp_bndrs) ty act_ki
-
--- | Instantiate a type to have at most @n@ invisible arguments.
-instantiateTyN :: Int    -- ^ @n@
-               -> TcType -- ^ the type
-               -> TcKind -- ^ its kind
-               -> TcM (TcType, TcKind)   -- ^ The inst'ed type with kind
-instantiateTyN n ty ki
-  = let (bndrs, inner_ki)            = splitPiTysInvisible ki
-        num_to_inst                  = length bndrs - n
-           -- NB: splitAt is forgiving with invalid numbers
-        (inst_bndrs, leftover_bndrs) = splitAt num_to_inst bndrs
+        instantiateTyUntilN (length exp_bndrs) ty act_ki
+
+-- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation
+-- occurs. If @n@ is too big, then all available invisible arguments are instantiated.
+-- (In other words, this function is very forgiving about bad values of @n at .)
+instantiateTyN :: Int                              -- ^ @n@
+               -> TcType                           -- ^ the type
+               -> [TyBinder] -> TcKind             -- ^ its kind
+               -> TcM (TcType, TcKind)             -- ^ The inst'ed type with kind
+instantiateTyN n ty bndrs inner_ki
+  = let   -- NB: splitAt is forgiving with invalid numbers
+        (inst_bndrs, leftover_bndrs) = splitAt n bndrs
+        ki          = mkPiTys bndrs inner_ki
         empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ki))
     in
-    if num_to_inst <= 0 then return (ty, ki) else
+    if n <= 0 then return (ty, ki) else
     do { (subst, inst_args) <- tcInstBinders empty_subst Nothing inst_bndrs
        ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
              ki'        = substTy subst rebuilt_ki
        ; traceTc "instantiateTyN" (vcat [ ppr ty <+> dcolon <+> ppr ki
+                                        , ppr n
                                         , ppr subst
                                         , ppr rebuilt_ki
                                         , ppr ki' ])
        ; return (mkNakedAppTys ty inst_args, ki') }
 
+-- | Instantiate a type to have at most @n@ invisible arguments.
+instantiateTyUntilN :: Int         -- ^ @n@
+                    -> TcType      -- ^ the type
+                    -> TcKind      -- ^ its kind
+                    -> TcM (TcType, TcKind)   -- ^ The inst'ed type with kind
+instantiateTyUntilN n ty ki
+  = let (bndrs, inner_ki) = splitPiTysInvisible ki
+        num_to_inst       = length bndrs - n
+    in
+    instantiateTyN num_to_inst ty bndrs inner_ki
 
 ---------------------------
 tcHsContext :: LHsContext GhcRn -> TcM [PredType]
@@ -1018,8 +1030,8 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
 
     -- if we are type-checking a type family tycon, we must instantiate
     -- any invisible arguments right away. Otherwise, we get #11246
-    handle_tyfams :: TyCon   -- the tycon to instantiate (might be loopy)
-                  -> TyCon   -- a non-loopy version of the tycon
+    handle_tyfams :: TyCon     -- the tycon to instantiate (might be loopy)
+                  -> TcTyCon   -- a non-loopy version of the tycon
                   -> TcM (TcType, TcKind)
     handle_tyfams tc tc_tc
       | mightBeUnsaturatedTyCon tc_tc
@@ -1027,7 +1039,8 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
            ; return (ty, tc_kind) }
 
       | otherwise
-      = do { (tc_ty, kind) <- instantiateTyN 0 ty tc_kind
+      = do { (tc_ty, kind) <- instantiateTyN (length (tyConBinders tc_tc))
+                                             ty tc_kind_bndrs tc_inner_ki
            -- tc and tc_ty must not be traced here, because that would
            -- force the evaluation of a potentially knot-tied variable (tc),
            -- and the typechecker would hang, as per #11708
@@ -1035,8 +1048,9 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
                                        , ppr kind ])
            ; return (tc_ty, kind) }
       where
-        ty      = mkNakedTyConApp tc []
-        tc_kind = tyConKind tc_tc
+        ty                           = mkNakedTyConApp tc []
+        tc_kind                      = tyConKind tc_tc
+        (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
 
     get_loopy_tc :: Name -> TyCon -> TcM TyCon
     -- Return the knot-tied global TyCon if there is one
diff --git a/testsuite/tests/dependent/should_compile/T12176.hs b/testsuite/tests/dependent/should_compile/T12176.hs
new file mode 100644
index 0000000..0e34006
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T12176.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE RankNTypes, TypeInType, GADTs, TypeFamilies #-}
+
+module T12176 where
+
+import Data.Kind
+
+data Proxy :: forall k. k -> Type where
+  MkProxy :: forall k (a :: k). Proxy a
+
+data X where
+  MkX :: forall (k :: Type) (a :: k). Proxy a -> X
+
+type Expr = (MkX :: forall (a :: Bool). Proxy a -> X)
+
+type family Foo (x :: forall (a :: k). Proxy a -> X) where
+  Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)
+
+type Bug = Foo Expr  -- this failed with #12176
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 8a9b221..b854f1d 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -24,3 +24,4 @@ test('T11719', normal, compile, [''])
 test('T11966', normal, compile, [''])
 test('T12442', normal, compile, [''])
 test('T13538', normal, compile, [''])
+test('T12176', normal, compile, [''])



More information about the ghc-commits mailing list