[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