Commit 8f99cd67 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Ben Gamari

Fix #13963.

This commit fixes several things:

1. RuntimeRep arg suppression was overeager for *visibly*-quantified
RuntimeReps, which should remain.

2. The choice of whether to used a Named TyConBinder or an anonymous
was sometimes wrong. Now, we do an extra little pass right before
constructing the tycon to fix these.

3. TyCons that normally cannot appear unsaturated can appear unsaturated
in :kind. But this fact was not propagated into the type checker.
It now is.
parent 86e1db7d
......@@ -681,11 +681,13 @@ defaultRuntimeRepVars = go emptyFsEnv
go :: FastStringEnv () -> IfaceType -> IfaceType
go subs (IfaceForAllTy bndr ty)
| isRuntimeRep var_kind
, isInvisibleArgFlag (binderArgFlag bndr) -- don't default *visible* quantification
-- or we get the mess in #13963
= let subs' = extendFsEnv subs var ()
in go subs' ty
| otherwise
= IfaceForAllTy (TvBndr (var, go subs var_kind) (binderArgFlag bndr))
(go subs ty)
(go subs ty)
where
var :: IfLclName
(var, var_kind) = binderVar bndr
......
......@@ -30,7 +30,7 @@ module TcHsType (
kcHsTyVarBndrs,
tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC,
tcLHsType, tcCheckLHsType,
tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
tcHsContext, tcLHsPredType, tcInferApps,
solveEqualities, -- useful re-export
......@@ -88,7 +88,7 @@ import PrelNames hiding ( wildCardName )
import qualified GHC.LanguageExtensions as LangExt
import Maybes
import Data.List ( partition, zipWith4 )
import Data.List ( partition, zipWith4, mapAccumR )
import Control.Monad
{-
......@@ -333,6 +333,13 @@ tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
-- Called from outside: set the context
tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
-- Like tcLHsType, but use it in a context where type synonyms and type families
-- do not need to be saturated, like in a GHCi :kind call
tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
tcLHsTypeUnsaturated ty = addTypeCtxt ty (tc_infer_lhs_type mode ty)
where
mode = allowUnsaturated typeLevelMode
---------------------------
-- | Should we generalise the kind of this type signature?
-- We *should* generalise if the type is closed
......@@ -392,15 +399,21 @@ concern things that the renamer can't handle.
-- differentiates only between types and kinds, but this will likely
-- grow, at least to include the distinction between patterns and
-- not-patterns.
newtype TcTyMode
= TcTyMode { mode_level :: TypeOrKind -- True <=> type, False <=> kind
data TcTyMode
= TcTyMode { mode_level :: TypeOrKind
, mode_unsat :: Bool -- True <=> allow unsaturated type families
}
-- The mode_unsat field is solely so that type families/synonyms can be unsaturated
-- in GHCi :kind calls
typeLevelMode :: TcTyMode
typeLevelMode = TcTyMode { mode_level = TypeLevel }
typeLevelMode = TcTyMode { mode_level = TypeLevel, mode_unsat = False }
kindLevelMode :: TcTyMode
kindLevelMode = TcTyMode { mode_level = KindLevel }
kindLevelMode = TcTyMode { mode_level = KindLevel, mode_unsat = False }
allowUnsaturated :: TcTyMode -> TcTyMode
allowUnsaturated mode = mode { mode_unsat = True }
-- switch to kind level
kindLevel :: TcTyMode -> TcTyMode
......@@ -1041,7 +1054,8 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
-> TcTyCon -- a non-loopy version of the tycon
-> TcM (TcType, TcKind)
handle_tyfams tc tc_tc
| mightBeUnsaturatedTyCon tc_tc
| mightBeUnsaturatedTyCon tc_tc || mode_unsat mode
-- This is where mode_unsat is used
= do { traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
; return (ty, tc_kind) }
......@@ -1835,8 +1849,8 @@ tcTyClTyVars tycon_name thing_inside
; let scoped_tvs = tcTyConScopedTyVars tycon
-- these are all zonked:
binders = tyConBinders tycon
res_kind = tyConResKind tycon
binders = correct_binders (tyConBinders tycon) res_kind
-- See Note [Free-floating kind vars]
; zonked_scoped_tvs <- mapM zonkTcTyVarToTyVar scoped_tvs
......@@ -1849,6 +1863,39 @@ tcTyClTyVars tycon_name thing_inside
; traceTc "tcTyClTyVars" (ppr tycon_name <+> ppr binders)
; tcExtendTyVarEnv scoped_tvs $
thing_inside binders res_kind }
where
-- Given some TyConBinders and a TyCon's result kind, make sure that the
-- correct any wrong Named/Anon choices. For example, consider
-- type Syn k = forall (a :: k). Proxy a
-- At first, it looks like k should be named -- after all, it appears on the RHS.
-- However, the correct kind for Syn is (* -> *).
-- (Why? Because k is the kind of a type, so k's kind is *. And the RHS also has
-- kind *.) See also #13963.
correct_binders :: [TyConBinder] -> Kind -> [TyConBinder]
correct_binders binders kind
= binders'
where
(_, binders') = mapAccumR go (tyCoVarsOfType kind) binders
go :: TyCoVarSet -> TyConBinder -> (TyCoVarSet, TyConBinder)
go fvs binder
| isNamedTyConBinder binder
, not (tv `elemVarSet` fvs)
= (new_fvs, mkAnonTyConBinder tv)
| not (isNamedTyConBinder binder)
, tv `elemVarSet` fvs
= (new_fvs, mkNamedTyConBinder Required tv)
-- always Required, because it was anonymous (i.e. visible) previously
| otherwise
= (new_fvs, binder)
where
tv = binderVar binder
new_fvs = fvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv)
-----------------------------------
tcDataKindSig :: Bool -- ^ Do we require the result to be *?
......
......@@ -2255,7 +2255,7 @@ tcRnType hsc_env normalise rdr_type
; traceTc "tcRnType" (vcat [ppr wcs, ppr rn_type])
; (ty, kind) <- solveEqualities $
tcWildCardBinders wcs $ \ _ ->
tcLHsType rn_type
tcLHsTypeUnsaturated rn_type
-- Do kind generalisation; see Note [Kind-generalise in tcRnType]
; kvs <- kindGeneralize kind
......
:set -XTypeInType -XRankNTypes
import GHC.Exts (TYPE, RuntimeRep(LiftedRep))
type Pair (a :: TYPE rep) (b :: TYPE rep') rep'' = forall (r :: TYPE rep''). (a -> b -> r)
:kind Pair
:kind Pair Int
:kind Pair Int Float
:kind Pair Int Float LiftedRep
Pair :: TYPE rep -> TYPE rep' -> RuntimeRep -> *
Pair Int :: * -> RuntimeRep -> *
Pair Int Float :: RuntimeRep -> *
Pair Int Float LiftedRep :: *
......@@ -258,3 +258,4 @@ test('T13591', expect_broken(13591), ghci_script, ['T13591.script'])
test('T13699', normal, ghci_script, ['T13699.script'])
test('T13988', normal, ghci_script, ['T13988.script'])
test('T13407', normal, ghci_script, ['T13407.script'])
test('T13963', normal, ghci_script, ['T13963.script'])
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