Address #11471 by putting RuntimeRep in kinds.
authorRichard Eisenberg <eir@cis.upenn.edu>
Thu, 4 Feb 2016 15:42:56 +0000 (10:42 -0500)
committerRichard Eisenberg <eir@cis.upenn.edu>
Wed, 24 Feb 2016 18:31:30 +0000 (13:31 -0500)
See Note [TYPE] in TysPrim. There are still some outstanding
pieces in #11471 though, so this doesn't actually nail the bug.

This commit also contains a few performance improvements:

* Short-cut equality checking of nullary type syns

* Compare types before kinds in eqType

* INLINE coreViewOneStarKind

* Store tycon binders separately from kinds.

This resulted in a ~10% performance improvement in compiling
the Cabal package. No change in functionality other than
performance. (This affects the interface file format, though.)

This commit updates the haddock submodule.

102 files changed:
compiler/basicTypes/DataCon.hs
compiler/basicTypes/MkId.hs
compiler/basicTypes/PatSyn.hs
compiler/coreSyn/CoreLint.hs
compiler/coreSyn/CorePrep.hs
compiler/coreSyn/MkCore.hs
compiler/deSugar/DsBinds.hs
compiler/deSugar/DsForeign.hs
compiler/deSugar/DsUtils.hs
compiler/ghci/RtClosureInspect.hs
compiler/iface/BinIface.hs
compiler/iface/BuildTyCl.hs
compiler/iface/IfaceEnv.hs
compiler/iface/IfaceSyn.hs
compiler/iface/IfaceType.hs
compiler/iface/MkIface.hs
compiler/iface/TcIface.hs
compiler/prelude/PrelNames.hs
compiler/prelude/PrimOp.hs
compiler/prelude/TysPrim.hs
compiler/prelude/TysWiredIn.hs
compiler/prelude/TysWiredIn.hs-boot
compiler/typecheck/Inst.hs
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcDeriv.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInstDcls.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcTypeNats.hs
compiler/typecheck/TcUnify.hs
compiler/typecheck/TcValidity.hs
compiler/types/Kind.hs
compiler/types/TyCoRep.hs
compiler/types/TyCoRep.hs-boot
compiler/types/TyCon.hs
compiler/types/Type.hs
compiler/utils/Util.hs
compiler/vectorise/Vectorise/Exp.hs
compiler/vectorise/Vectorise/Generic/PData.hs
compiler/vectorise/Vectorise/Type/Env.hs
compiler/vectorise/Vectorise/Type/TyConDecl.hs
libraries/base/Data/Data.hs
libraries/base/Data/Typeable/Internal.hs
libraries/base/GHC/Err.hs
libraries/base/GHC/Exts.hs
libraries/base/tests/T11334.hs
libraries/ghc-prim/GHC/Types.hs
testsuite/tests/dependent/should_compile/T11405.hs
testsuite/tests/dependent/should_fail/BadTelescope4.stderr
testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
testsuite/tests/ghci/scripts/T4175.stdout
testsuite/tests/ghci/scripts/T7627.stdout
testsuite/tests/ghci/scripts/T7939.stdout
testsuite/tests/ghci/scripts/T8535.stdout
testsuite/tests/ghci/scripts/T9181.stdout
testsuite/tests/ghci/scripts/ghci020.stdout
testsuite/tests/ghci/should_run/T10145.stdout
testsuite/tests/indexed-types/should_compile/T3017.stderr
testsuite/tests/indexed-types/should_fail/ClosedFam3.stderr
testsuite/tests/indexed-types/should_fail/Overlap4.stderr
testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr
testsuite/tests/indexed-types/should_fail/TyFamArity1.stderr
testsuite/tests/indexed-types/should_fail/TyFamArity2.stderr
testsuite/tests/indexed-types/should_run/T11465a.hs
testsuite/tests/partial-sigs/should_compile/ADT.stderr
testsuite/tests/partial-sigs/should_compile/DataFamilyInstanceLHS.stderr
testsuite/tests/partial-sigs/should_compile/Meltdown.stderr
testsuite/tests/partial-sigs/should_compile/NamedWildcardInDataFamilyInstanceLHS.stderr
testsuite/tests/partial-sigs/should_compile/NamedWildcardInTypeFamilyInstanceLHS.stderr
testsuite/tests/partial-sigs/should_compile/SkipMany.stderr
testsuite/tests/partial-sigs/should_compile/TypeFamilyInstanceLHS.stderr
testsuite/tests/perf/compiler/all.T
testsuite/tests/polykinds/T11399.stderr
testsuite/tests/polykinds/T7328.stderr
testsuite/tests/polykinds/TidyClassKinds.stderr
testsuite/tests/roles/should_compile/Roles1.stderr
testsuite/tests/roles/should_compile/Roles2.stderr
testsuite/tests/roles/should_compile/Roles3.stderr
testsuite/tests/roles/should_compile/T8958.stderr
testsuite/tests/simplCore/should_compile/T9400.stderr
testsuite/tests/simplCore/should_compile/spec-inline.stderr
testsuite/tests/th/TH_Roles2.stderr
testsuite/tests/typecheck/should_compile/tc231.stderr
testsuite/tests/typecheck/should_run/KindInvariant.stderr
testsuite/tests/typecheck/should_run/TypeOf.hs
testsuite/tests/typecheck/should_run/TypeOf.stdout
utils/genprimopcode/Main.hs
utils/haddock

index 8552205..57a9857 100644 (file)
@@ -720,6 +720,7 @@ mkDataCon :: Name
           -> ThetaType      -- ^ Theta-type occuring before the arguments proper
           -> [Type]         -- ^ Original argument types
           -> Type           -- ^ Original result type
+          -> RuntimeRepInfo -- ^ See comments on 'TyCon.RuntimeRepInfo'
           -> TyCon          -- ^ Representation type constructor
           -> ThetaType      -- ^ The "stupid theta", context of the data
                             -- declaration e.g. @data Eq a => T a ...@
@@ -733,7 +734,7 @@ mkDataCon name declared_infix prom_info
           fields
           univ_tvs ex_tvs
           eq_spec theta
-          orig_arg_tys orig_res_ty rep_tycon
+          orig_arg_tys orig_res_ty rep_info rep_tycon
           stupid_theta work_id rep
 -- Warning: mkDataCon is not a good place to check invariants.
 -- If the programmer writes the wrong result type in the decl, thus:
@@ -774,8 +775,15 @@ mkDataCon name declared_infix prom_info
              mkFunTys rep_arg_tys $
              mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
 
-    promoted   -- See Note [Promoted data constructors] in TyCon
-      = mkPromotedDataCon con name prom_info (dataConUserType con) roles
+      -- See Note [Promoted data constructors] in TyCon
+    prom_binders = map (mkNamedBinder Specified)
+                       ((univ_tvs `minusList` map eqSpecTyVar eq_spec) ++
+                        ex_tvs) ++
+                   map mkAnonBinder theta ++
+                   map mkAnonBinder orig_arg_tys
+    prom_res_kind = orig_res_ty
+    promoted
+      = mkPromotedDataCon con name prom_info prom_binders prom_res_kind roles rep_info
 
     roles = map (const Nominal) (univ_tvs ++ ex_tvs) ++
             map (const Representational) orig_arg_tys
@@ -1106,9 +1114,7 @@ isVanillaDataCon dc = dcVanilla dc
 -- | Should this DataCon be allowed in a type even without -XDataKinds?
 -- Currently, only Lifted & Unlifted
 specialPromotedDc :: DataCon -> Bool
-specialPromotedDc dc
-  = dc `hasKey` liftedDataConKey ||
-    dc `hasKey` unliftedDataConKey
+specialPromotedDc = isKindTyCon . dataConTyCon
 
 -- | Was this datacon promotable before GHC 8.0? That is, is it promotable
 -- without -XTypeInType
@@ -1228,7 +1234,7 @@ buildAlgTyCon :: Name
 
 buildAlgTyCon tc_name ktvs roles cType stupid_theta rhs
               is_rec gadt_syn parent
-  = mkAlgTyCon tc_name kind ktvs roles cType stupid_theta
+  = mkAlgTyCon tc_name binders liftedTypeKind ktvs roles cType stupid_theta
                rhs parent is_rec gadt_syn
   where
-    kind = mkPiTypesPreferFunTy ktvs liftedTypeKind
+    binders = mkTyBindersPreferAnon ktvs liftedTypeKind
index a64e922..8ee5013 100644 (file)
@@ -1062,11 +1062,11 @@ dollarId = pcMiscPrelId dollarName ty
              (noCafIdInfo `setUnfoldingInfo` unf)
   where
     fun_ty = mkFunTy alphaTy openBetaTy
-    ty     = mkSpecForAllTys [levity2TyVar, alphaTyVar, openBetaTyVar] $
+    ty     = mkSpecForAllTys [runtimeRep2TyVar, alphaTyVar, openBetaTyVar] $
              mkFunTy fun_ty fun_ty
     unf    = mkInlineUnfolding (Just 2) rhs
     [f,x]  = mkTemplateLocals [fun_ty, alphaTy]
-    rhs    = mkLams [levity2TyVar, alphaTyVar, openBetaTyVar, f, x] $
+    rhs    = mkLams [runtimeRep2TyVar, alphaTyVar, openBetaTyVar, f, x] $
              App (Var f) (Var x)
 
 ------------------------------------------------
@@ -1083,7 +1083,9 @@ proxyHashId
     t       = mkTyVarTy tv
 
 ------------------------------------------------
--- unsafeCoerce# :: forall a b. a -> b
+-- unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+--                         (a :: TYPE r1) (b :: TYPE r2).
+--                         a -> b
 unsafeCoerceId :: Id
 unsafeCoerceId
   = pcMiscPrelId unsafeCoerceName ty info
@@ -1091,14 +1093,13 @@ unsafeCoerceId
     info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
 
-    ty  = mkSpecForAllTys [ levity1TyVar, levity2TyVar
-                          , openAlphaTyVar, openBetaTyVar ]
-                          (mkFunTy openAlphaTy openBetaTy)
+    tvs = [ runtimeRep1TyVar, runtimeRep2TyVar
+          , openAlphaTyVar, openBetaTyVar ]
+
+    ty  = mkSpecForAllTys tvs $ mkFunTy openAlphaTy openBetaTy
 
     [x] = mkTemplateLocals [openAlphaTy]
-    rhs = mkLams [ levity1TyVar, levity2TyVar
-                 , openAlphaTyVar, openBetaTyVar
-                 , x] $
+    rhs = mkLams (tvs ++ [x]) $
           Cast (Var x) (mkUnsafeCo Representational openAlphaTy openBetaTy)
 
 ------------------------------------------------
@@ -1166,13 +1167,13 @@ oneShotId = pcMiscPrelId oneShotName ty info
   where
     info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
-    ty  = mkSpecForAllTys [ levity1TyVar, levity2TyVar
+    ty  = mkSpecForAllTys [ runtimeRep1TyVar, runtimeRep2TyVar
                           , openAlphaTyVar, openBetaTyVar ]
                           (mkFunTy fun_ty fun_ty)
-    fun_ty = mkFunTy alphaTy betaTy
+    fun_ty = mkFunTy openAlphaTy openBetaTy
     [body, x] = mkTemplateLocals [fun_ty, openAlphaTy]
     x' = setOneShotLambda x
-    rhs = mkLams [ levity1TyVar, levity2TyVar
+    rhs = mkLams [ runtimeRep1TyVar, runtimeRep2TyVar
                  , openAlphaTyVar, openBetaTyVar
                  , body, x'] $
           Var body `App` Var x
@@ -1196,7 +1197,7 @@ runRWId = pcMiscPrelId runRWName ty info
     arg_ty  = stateRW `mkFunTy` ret_ty
     -- (State# RealWorld -> (# State# RealWorld, o #))
     --   -> (# State# RealWorld, o #)
-    ty      = mkSpecForAllTys [levity1TyVar, openAlphaTyVar] $
+    ty      = mkSpecForAllTys [runtimeRep1TyVar, openAlphaTyVar] $
               arg_ty `mkFunTy` ret_ty
 
 --------------------------------------------------------------------------------
@@ -1375,7 +1376,7 @@ no further floating will occur. This allows us to safely inline things like
 While the definition of @GHC.Magic.runRW#@, we override its type in @MkId@
 to be open-kinded,
 
-    runRW# :: forall (lev :: Levity). (o :: TYPE lev)
+    runRW# :: forall (r1 :: RuntimeRep). (o :: TYPE r)
            => (State# RealWorld -> (# State# RealWorld, o #))
                               -> (# State# RealWorld, o #)
 
index 6582658..cef9476 100644 (file)
@@ -79,7 +79,7 @@ data PatSyn
              -- Matcher function.
              -- If Bool is True then prov_theta and arg_tys are empty
              -- and type is
-             --   forall (v :: Levity) (r :: TYPE v) univ_tvs.
+             --   forall (p :: RuntimeRep) (r :: TYPE p) univ_tvs.
              --                          req_theta
              --                       => res_ty
              --                       -> (forall ex_tvs. Void# -> r)
@@ -87,7 +87,7 @@ data PatSyn
              --                       -> r
              --
              -- Otherwise type is
-             --   forall (v :: Levity) (r :: TYPE v) univ_tvs.
+             --   forall (p :: RuntimeRep) (r :: TYPE r) univ_tvs.
              --                          req_theta
              --                       => res_ty
              --                       -> (forall ex_tvs. prov_theta => arg_tys -> r)
index 6dbcbe4..f9cb4be 100644 (file)
@@ -988,8 +988,8 @@ lintAndScopeId id linterF
                 (text "Non-local Id binder" <+> ppr id)
                 -- See Note [Checking for global Ids]
        ; (ty, k) <- lintInTy (idType id)
-       ; lintL (not (isLevityPolymorphic k))
-           (text "Levity polymorphic binder:" <+>
+       ; lintL (not (isRuntimeRepPolymorphic k))
+           (text "RuntimeRep-polymorphic binder:" <+>
                  (ppr id <+> dcolon <+> parens (ppr ty <+> dcolon <+> ppr k)))
        ; let id' = setIdType id ty
        ; addInScopeVar id' $ (linterF id') }
index 4708df3..3f9f4c8 100644 (file)
@@ -512,7 +512,7 @@ cpeRhsE env (Var f `App` _{-type-} `App` arg)
   | f `hasKey` lazyIdKey          -- Replace (lazy a) by a
   = cpeRhsE env arg               -- See Note [lazyId magic] in MkId
 
-cpeRhsE env (Var f `App` _levity `App` _type `App` arg)
+cpeRhsE env (Var f `App` _runtimeRep `App` _type `App` arg)
     -- See Note [runRW magic] in MkId
   | f `hasKey` runRWKey           -- Replace (runRW# f) by (f realWorld#),
   = case arg of                   -- beta reducing if possible
index 94a264c..0eccccc 100644 (file)
@@ -322,13 +322,13 @@ mkCoreTup cs  = mkCoreConApps (tupleDataCon Boxed (length cs))
 
 -- | Build a small unboxed tuple holding the specified expressions,
 -- with the given types. The types must be the types of the expressions.
--- Do not include the levity specifiers; this function calculates them
+-- Do not include the RuntimeRep specifiers; this function calculates them
 -- for you.
 mkCoreUbxTup :: [Type] -> [CoreExpr] -> CoreExpr
 mkCoreUbxTup tys exps
   = ASSERT( tys `equalLength` exps)
     mkCoreConApps (tupleDataCon Unboxed (length tys))
-             (map (Type . getLevity "mkCoreUbxTup") tys ++ map Type tys ++ exps)
+             (map (Type . getRuntimeRep "mkCoreUbxTup") tys ++ map Type tys ++ exps)
 
 -- | Make a core tuple of the given boxity
 mkCoreTupBoxity :: Boxity -> [CoreExpr] -> CoreExpr
@@ -588,7 +588,8 @@ mkRuntimeErrorApp
         -> CoreExpr
 
 mkRuntimeErrorApp err_id res_ty err_msg
-  = mkApps (Var err_id) [Type (getLevity "mkRuntimeErrorApp" res_ty), Type res_ty, err_string]
+  = mkApps (Var err_id) [ Type (getRuntimeRep "mkRuntimeErrorApp" res_ty)
+                        , Type res_ty, err_string ]
   where
     err_string = Lit (mkMachString err_msg)
 
@@ -672,21 +673,18 @@ mkRuntimeErrorId name = pc_bottoming_Id1 name runtimeErrorTy
 
 runtimeErrorTy :: Type
 -- The runtime error Ids take a UTF8-encoded string as argument
-runtimeErrorTy = mkSpecSigmaTy [levity1TyVar, openAlphaTyVar] []
+runtimeErrorTy = mkSpecSigmaTy [runtimeRep1TyVar, openAlphaTyVar] []
                                (mkFunTy addrPrimTy openAlphaTy)
 
 {-
 Note [Error and friends have an "open-tyvar" forall]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 'error' and 'undefined' have types
-        error     :: forall (v :: Levity) (a :: TYPE v). String -> a
-        undefined :: forall (v :: Levity) (a :: TYPE v). a
-Notice the levity polymophism. This ensures that
-"error" can be instantiated at
-  * unboxed as well as boxed types
-  * polymorphic types
+        error     :: forall (v :: RuntimeRep) (a :: TYPE v). String -> a
+        undefined :: forall (v :: RuntimeRep) (a :: TYPE v). a
+Notice the runtime-representation polymophism. This ensures that
+"error" can be instantiated at unboxed as well as boxed types.
 This is OK because it never returns, so the return type is irrelevant.
-See Note [Sort-polymorphic tyvars accept foralls] in TcMType.
 
 
 ************************************************************************
index 4f05d07..420090d 100644 (file)
@@ -1067,7 +1067,7 @@ dsEvTerm (EvDelayedError ty msg) = return $ dsEvDelayedError ty msg
 
 dsEvDelayedError :: Type -> FastString -> CoreExpr
 dsEvDelayedError ty msg
-  = Var errorId `mkTyApps` [getLevity "dsEvTerm" ty, ty] `mkApps` [litMsg]
+  = Var errorId `mkTyApps` [getRuntimeRep "dsEvTerm" ty, ty] `mkApps` [litMsg]
   where
     errorId = tYPE_ERROR_ID
     litMsg  = Lit (MachStr (fastStringToByteString msg))
index a87526f..26c84c7 100644 (file)
@@ -198,7 +198,10 @@ dsFCall fn_id co fcall mDeclHeader = do
         ty                     = pFst $ coercionKind co
         (all_bndrs, io_res_ty) = tcSplitPiTys ty
         (named_bndrs, arg_tys) = partitionBindersIntoBinders all_bndrs
-        tvs                    = map (binderVar "dsFCall") named_bndrs
+        tvs                    = ASSERT( fst (span isNamedBinder all_bndrs)
+                                         `equalLength` named_bndrs )
+                                   -- ensure that the named binders all come first
+                                 map (binderVar "dsFCall") named_bndrs
                 -- Must use tcSplit* functions because we want to
                 -- see that (IO t) in the corner
 
@@ -302,6 +305,7 @@ dsPrimCall fn_id co fcall = do
                 -- Must use tcSplit* functions because we want to
                 -- see that (IO t) in the corner
 
+    MASSERT( fst (span isNamedBinder bndrs) `equalLength` tvs )
     args <- newSysLocalsDs arg_tys
 
     ccall_uniq <- newUnique
@@ -412,6 +416,8 @@ dsFExportDynamic :: Id
                  -> CCallConv
                  -> DsM ([Binding], SDoc, SDoc)
 dsFExportDynamic id co0 cconv = do
+    MASSERT( fst (span isNamedBinder bndrs) `equalLength` tvs )
+      -- make sure that the named binders all come first
     fe_id <-  newSysLocalDs ty
     mod <- getModule
     dflags <- getDynFlags
index 0ddfb97..ece50d8 100644 (file)
@@ -343,7 +343,7 @@ sort_alts = sortWith (dataConTag . alt_pat)
 mkPatSynCase :: Id -> Type -> CaseAlt PatSyn -> CoreExpr -> DsM CoreExpr
 mkPatSynCase var ty alt fail = do
     matcher <- dsLExpr $ mkLHsWrap wrapper $
-                         nlHsTyApp matcher [getLevity "mkPatSynCase" ty, ty]
+                         nlHsTyApp matcher [getRuntimeRep "mkPatSynCase" ty, ty]
     let MatchResult _ mkCont = match_result
     cont <- mkCoreLams bndrs <$> mkCont fail
     return $ mkCoreAppsDs (text "patsyn" <+> ppr var) matcher [Var var, ensure_unstrict cont, Lam voidArgId fail]
@@ -469,7 +469,7 @@ mkErrorAppDs err_id ty msg = do
         full_msg = showSDoc dflags (hcat [ppr src_loc, vbar, msg])
         core_msg = Lit (mkMachString full_msg)
         -- mkMachString returns a result of type String#
-    return (mkApps (Var err_id) [Type (getLevity "mkErrorAppDs" ty), Type ty, core_msg])
+    return (mkApps (Var err_id) [Type (getRuntimeRep "mkErrorAppDs" ty), Type ty, core_msg])
 
 {-
 'mkCoreAppDs' and 'mkCoreAppsDs' hand the special-case desugaring of 'seq'.
index 1832ea4..a76a298 100644 (file)
@@ -800,8 +800,8 @@ extractSubTerms recurse clos = liftM thdOf3 . go 0 (nonPtrs clos)
     go ptr_i ws (ty:tys)
       | Just (tc, elem_tys) <- tcSplitTyConApp_maybe ty
       , isUnboxedTupleTyCon tc
-                -- See Note [Unboxed tuple levity vars] in TyCon
-      = do (ptr_i, ws, terms0) <- go ptr_i ws (dropLevityArgs elem_tys)
+                -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
+      = do (ptr_i, ws, terms0) <- go ptr_i ws (dropRuntimeRepArgs elem_tys)
            (ptr_i, ws, terms1) <- go ptr_i ws tys
            return (ptr_i, ws, unboxedTupleTerm ty terms0 : terms1)
       | otherwise
index c0926fc..a7246af 100644 (file)
@@ -344,7 +344,7 @@ putTupleName_ bh tc tup_sort thing_tag
     (sort_tag, arity) = case tup_sort of
       BoxedTuple      -> (0, fromIntegral (tyConArity tc))
       UnboxedTuple    -> (1, fromIntegral (tyConArity tc `div` 2))
-        -- See Note [Unboxed tuple levity vars] in TyCon
+        -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
       ConstraintTuple -> pprPanic "putTupleName:ConstraintTuple" (ppr tc)
 
 -- See Note [Symbol table representation of names]
index 0022e29..87b5f36 100644 (file)
@@ -138,7 +138,7 @@ buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs fie
                 data_con = mkDataCon src_name declared_infix prom_info
                                      src_bangs field_lbls
                                      univ_tvs ex_tvs eq_spec ctxt
-                                     arg_tys res_ty rep_tycon
+                                     arg_tys res_ty NoRRI rep_tycon
                                      stupid_ctxt dc_wrk dc_rep
                 dc_wrk = mkDataConWorkId work_name data_con
                 dc_rep = initUs_ us (mkDataConRep dflags fam_envs wrap_name
@@ -215,7 +215,7 @@ type TcMethInfo = (Name, Type, Maybe (DefMethSpec Type))
 
 buildClass :: Name  -- Name of the class/tycon (they have the same Name)
            -> [TyVar] -> [Role] -> ThetaType
-           -> Kind
+           -> [TyBinder]
            -> [FunDep TyVar]               -- Functional dependencies
            -> [ClassATItem]                -- Associated types
            -> [TcMethInfo]                 -- Method info
@@ -223,7 +223,8 @@ buildClass :: Name  -- Name of the class/tycon (they have the same Name)
            -> RecFlag                      -- Info for type constructor
            -> TcRnIf m n Class
 
-buildClass tycon_name tvs roles sc_theta kind fds at_items sig_stuff mindef tc_isrec
+buildClass tycon_name tvs roles sc_theta binders
+           fds at_items sig_stuff mindef tc_isrec
   = fixM  $ \ rec_clas ->       -- Only name generation inside loop
     do  { traceIf (text "buildClass")
 
@@ -286,7 +287,7 @@ buildClass tycon_name tvs roles sc_theta kind fds at_items sig_stuff mindef tc_i
                                          , tup_sort = ConstraintTuple })
                  else return (mkDataTyConRhs [dict_con])
 
-        ; let { tycon = mkClassTyCon tycon_name kind tvs roles
+        ; let { tycon = mkClassTyCon tycon_name binders tvs roles
                                      rhs rec_clas tc_isrec tc_rep_name
                 -- A class can be recursive, and in the case of newtypes
                 -- this matters.  For example
index 43094f9..20b497b 100644 (file)
@@ -49,7 +49,7 @@ import Data.List     ( partition )
 
 Note [The Name Cache]
 ~~~~~~~~~~~~~~~~~~~~~
-The Name Cache makes sure that, during any invovcation of GHC, each
+The Name Cache makes sure that, during any invocation of GHC, each
 External Name "M.x" has one, and only one globally-agreed Unique.
 
 * The first time we come across M.x we make up a Unique and record that
index 7b6b34c..9113285 100644 (file)
@@ -95,9 +95,9 @@ data IfaceDecl
               ifIdInfo    :: IfaceIdInfo }
 
   | IfaceData { ifName       :: IfaceTopBndr,   -- Type constructor
-                ifKind       :: IfaceType,      -- Kind of type constructor
+                ifBinders    :: [IfaceTyConBinder],
+                ifResKind    :: IfaceType,      -- Result kind of type constructor
                 ifCType      :: Maybe CType,    -- C type for CAPI FFI
-                ifTyVars     :: [IfaceTvBndr],  -- Type variables
                 ifRoles      :: [Role],         -- Roles
                 ifCtxt       :: IfaceContext,   -- The "stupid theta"
                 ifCons       :: IfaceConDecls,  -- Includes new/data/data family info
@@ -109,25 +109,24 @@ data IfaceDecl
     }
 
   | IfaceSynonym { ifName    :: IfaceTopBndr,      -- Type constructor
-                   ifTyVars  :: [IfaceTvBndr],     -- Type variables
                    ifRoles   :: [Role],            -- Roles
-                   ifSynKind :: IfaceKind,         -- Kind of the *tycon*
+                   ifBinders :: [IfaceTyConBinder],
+                   ifResKind :: IfaceKind,         -- Kind of the *result*
                    ifSynRhs  :: IfaceType }
 
   | IfaceFamily  { ifName    :: IfaceTopBndr,      -- Type constructor
-                   ifTyVars  :: [IfaceTvBndr],     -- Type variables
                    ifResVar  :: Maybe IfLclName,   -- Result variable name, used
                                                    -- only for pretty-printing
                                                    -- with --show-iface
-                   ifFamKind :: IfaceKind,         -- Kind of the *tycon*
+                   ifBinders :: [IfaceTyConBinder],
+                   ifResKind :: IfaceKind,         -- Kind of the *tycon*
                    ifFamFlav :: IfaceFamTyConFlav,
                    ifFamInj  :: Injectivity }      -- injectivity information
 
   | IfaceClass { ifCtxt    :: IfaceContext,             -- Superclasses
                  ifName    :: IfaceTopBndr,             -- Name of the class TyCon
-                 ifTyVars  :: [IfaceTvBndr],            -- Type variables
                  ifRoles   :: [Role],                   -- Roles
-                 ifKind    :: IfaceType,                -- Kind of TyCon
+                 ifBinders :: [IfaceTyConBinder],
                  ifFDs     :: [FunDep FastString],      -- Functional dependencies
                  ifATs     :: [IfaceAT],                -- Associated type families
                  ifSigs    :: [IfaceClassOp],           -- Method signatures
@@ -619,11 +618,11 @@ pprIfaceDecl :: ShowSub -> IfaceDecl -> SDoc
 -- NB: pprIfaceDecl is also used for pretty-printing TyThings in GHCi
 --     See Note [Pretty-printing TyThings] in PprTyThing
 pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
-                             ifCtxt = context, ifTyVars = tc_tyvars,
+                             ifCtxt = context,
                              ifRoles = roles, ifCons = condecls,
                              ifParent = parent, ifRec = isrec,
                              ifGadtSyntax = gadt,
-                             ifKind = kind })
+                             ifBinders = binders })
 
   | gadt_style = vcat [ pp_roles
                       , pp_nd <+> pp_lhs <+> pp_where
@@ -641,14 +640,14 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
     pp_cons    = ppr_trim (map show_con cons) :: [SDoc]
 
     pp_lhs = case parent of
-               IfNoParent -> pprIfaceDeclHead context ss tycon kind tc_tyvars
+               IfNoParent -> pprIfaceDeclHead context ss tycon binders Nothing
                _          -> text "instance" <+> pprIfaceTyConParent parent
 
     pp_roles
       | is_data_instance = empty
       | otherwise        = pprRoles (== Representational)
                                     (pprPrefixIfDeclBndr ss tycon)
-                                    tc_bndrs roles
+                                    binders roles
             -- Don't display roles for data family instances (yet)
             -- See discussion on Trac #8672.
 
@@ -658,50 +657,29 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
     ok_con dc = showSub ss dc || any (showSub ss) (ifConFields dc)
 
     show_con dc
-      | ok_con dc = Just $ pprIfaceConDecl ss gadt_style mk_user_con_res_ty fls dc
+      | ok_con dc = Just $ pprIfaceConDecl ss gadt_style fls tycon binders parent dc
       | otherwise = Nothing
     fls = ifaceConDeclFields condecls
 
-    mk_user_con_res_ty :: IfaceEqSpec -> ([IfaceTvBndr], SDoc)
-    -- See Note [Result type of a data family GADT]
-    mk_user_con_res_ty eq_spec
-      | IfDataInstance _ tc tys <- parent
-      = (con_univ_tvs, pprIfaceType (IfaceTyConApp tc (substIfaceTcArgs gadt_subst tys)))
-      | otherwise
-      = (con_univ_tvs, sdocWithDynFlags (ppr_tc_app gadt_subst))
-      where
-        gadt_subst = mkFsEnv eq_spec
-        done_univ_tv (tv,_) = isJust (lookupFsEnv gadt_subst tv)
-        con_univ_tvs = filterOut done_univ_tv tc_tyvars
-
-    ppr_tc_app gadt_subst dflags
-       = pprPrefixIfDeclBndr ss tycon
-         <+> sep [ pprParendIfaceType (substIfaceTyVar gadt_subst tv)
-                 | (tv,_kind)
-                     <- suppressIfaceInvisibles dflags tc_bndrs tc_tyvars ]
-    (tc_bndrs, _, _) = splitIfaceSigmaTy kind
-
     pp_nd = case condecls of
               IfAbstractTyCon d -> text "abstract" <> ppShowIface ss (parens (ppr d))
               IfDataTyCon{}     -> text "data"
               IfNewTyCon{}      -> text "newtype"
 
-    pp_extra = vcat [pprCType ctype, pprRec isrec, text "Kind:" <+> ppr kind]
+    pp_extra = vcat [pprCType ctype, pprRec isrec]
 
 
 pprIfaceDecl ss (IfaceClass { ifATs = ats, ifSigs = sigs, ifRec = isrec
                             , ifCtxt   = context, ifName  = clas
-                            , ifTyVars = tyvars,  ifRoles = roles
+                            , ifRoles = roles
                             , ifFDs    = fds, ifMinDef = minDef
-                            , ifKind   = kind })
-  = vcat [ pprRoles (== Nominal) (pprPrefixIfDeclBndr ss clas) bndrs roles
-         , text "class" <+> pprIfaceDeclHead context ss clas kind tyvars
+                            , ifBinders = binders })
+  = vcat [ pprRoles (== Nominal) (pprPrefixIfDeclBndr ss clas) binders roles
+         , text "class" <+> pprIfaceDeclHead context ss clas binders Nothing
                                 <+> pprFundeps fds <+> pp_where
          , nest 2 (vcat [ vcat asocs, vcat dsigs, pprec
                         , ppShowAllSubs ss (pprMinDef minDef)])]
     where
-      (bndrs, _, _) = splitIfaceSigmaTy kind
-
       pp_where = ppShowRhs ss $ ppUnless (null sigs && null ats) (text "where")
 
       asocs = ppr_trim $ map maybeShowAssoc ats
@@ -726,26 +704,27 @@ pprIfaceDecl ss (IfaceClass { ifATs = ats, ifSigs = sigs, ifRec = isrec
         text "#-}"
 
 pprIfaceDecl ss (IfaceSynonym { ifName    = tc
-                              , ifTyVars  = tv
+                              , ifBinders = binders
                               , ifSynRhs  = mono_ty
-                              , ifSynKind = kind})
-  = hang (text "type" <+> pprIfaceDeclHead [] ss tc kind tv <+> equals)
-       2 (sep [pprIfaceForAll tvs, pprIfaceContextArr theta, ppr tau])
+                              , ifResKind = res_kind})
+  = hang (text "type" <+> pprIfaceDeclHead [] ss tc binders Nothing <+> equals)
+       2 (sep [ pprIfaceForAll tvs, pprIfaceContextArr theta, ppr tau
+              , ppUnless (isIfaceLiftedTypeKind res_kind) (dcolon <+> ppr res_kind) ])
   where
     (tvs, theta, tau) = splitIfaceSigmaTy mono_ty
 
-pprIfaceDecl ss (IfaceFamily { ifName = tycon, ifTyVars = tyvars
-                             , ifFamFlav = rhs, ifFamKind = kind
+pprIfaceDecl ss (IfaceFamily { ifName = tycon
+                             , ifFamFlav = rhs, ifBinders = binders
+                             , ifResKind = res_kind
                              , ifResVar = res_var, ifFamInj = inj })
   | IfaceDataFamilyTyCon <- rhs
-  = text "data family" <+> pprIfaceDeclHead [] ss tycon kind tyvars
+  = text "data family" <+> pprIfaceDeclHead [] ss tycon binders Nothing
 
   | otherwise
-  = hang (text "type family" <+> pprIfaceDeclHead [] ss tycon kind tyvars)
+  = hang (text "type family" <+> pprIfaceDeclHead [] ss tycon binders (Just res_kind))
        2 (pp_inj res_var inj <+> ppShowRhs ss (pp_rhs rhs))
     $$
-    nest 2 ( vcat [ text "Kind:" <+> ppr kind
-                  , ppShowRhs ss (pp_branches rhs) ] )
+    nest 2 (ppShowRhs ss (pp_branches rhs))
   where
     pp_inj Nothing    _   = empty
     pp_inj (Just res) inj
@@ -753,9 +732,9 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon, ifTyVars = tyvars
                                              , pp_inj_cond res injectivity]
        | otherwise = hsep [ equals, ppr res ]
 
-    pp_inj_cond res inj = case filterByList inj tyvars of
+    pp_inj_cond res inj = case filterByList inj binders of
        []  -> empty
-       tvs -> hsep [vbar, ppr res, text "->", interppSP (map fst tvs)]
+       tvs -> hsep [vbar, ppr res, text "->", interppSP (map ifTyConBinderName tvs)]
 
     pp_rhs IfaceDataFamilyTyCon
       = ppShowIface ss (text "data")
@@ -808,7 +787,7 @@ pprCType (Just cType) = text "C type:" <+> ppr cType
 
 -- if, for each role, suppress_if role is True, then suppress the role
 -- output
-pprRoles :: (Role -> Bool) -> SDoc -> [IfaceForAllBndr]
+pprRoles :: (Role -> Bool) -> SDoc -> [IfaceTyConBinder]
          -> [Role] -> SDoc
 pprRoles suppress_if tyCon bndrs roles
   = sdocWithDynFlags $ \dflags ->
@@ -862,15 +841,15 @@ pprIfaceTyConParent (IfDataInstance _ tc tys)
     in pprIfaceTypeApp tc ftys
 
 pprIfaceDeclHead :: IfaceContext -> ShowSub -> OccName
-                 -> IfaceType   -- of the tycon, for invisible-suppression
-                 -> [IfaceTvBndr] -> SDoc
-pprIfaceDeclHead context ss tc_occ kind tyvars
+                 -> [IfaceTyConBinder]   -- of the tycon, for invisible-suppression
+                 -> Maybe IfaceKind
+                 -> SDoc
+pprIfaceDeclHead context ss tc_occ bndrs m_res_kind
   = sdocWithDynFlags $ \ dflags ->
     sep [ pprIfaceContextArr context
         , pprPrefixIfDeclBndr ss tc_occ
-          <+> pprIfaceTvBndrs (suppressIfaceInvisibles dflags bndrs tyvars) ]
-  where
-    (bndrs, _, _) = splitIfaceSigmaTy kind
+          <+> pprIfaceTyConBinders (suppressIfaceInvisibles dflags bndrs bndrs)
+        , maybe empty (\res_kind -> dcolon <+> pprIfaceType res_kind) m_res_kind ]
 
 isVanillaIfaceConDecl :: IfaceConDecl -> Bool
 isVanillaIfaceConDecl (IfCon { ifConExTvs  = ex_tvs
@@ -879,10 +858,12 @@ isVanillaIfaceConDecl (IfCon { ifConExTvs  = ex_tvs
   = (null ex_tvs) && (null eq_spec) && (null ctxt)
 
 pprIfaceConDecl :: ShowSub -> Bool
-                -> (IfaceEqSpec -> ([IfaceTvBndr], SDoc))
                 -> [FieldLbl OccName]
+                -> IfaceTopBndr
+                -> [IfaceTyConBinder]
+                -> IfaceTyConParent
                 -> IfaceConDecl -> SDoc
-pprIfaceConDecl ss gadt_style mk_user_con_res_ty fls
+pprIfaceConDecl ss gadt_style fls tycon tc_binders parent
         (IfCon { ifConOcc = name, ifConInfix = is_infix,
                  ifConExTvs = ex_tvs,
                  ifConEqSpec = eq_spec, ifConCtxt = ctxt, ifConArgTys = arg_tys,
@@ -935,6 +916,25 @@ pprIfaceConDecl ss gadt_style mk_user_con_res_ty fls
         -- DuplicateRecordFields was used for the definition)
         lbl = maybe sel (mkVarOccFS . flLabel) $ find (\ fl -> flSelector fl == sel) fls
 
+    mk_user_con_res_ty :: IfaceEqSpec -> ([IfaceTvBndr], SDoc)
+    -- See Note [Result type of a data family GADT]
+    mk_user_con_res_ty eq_spec
+      | IfDataInstance _ tc tys <- parent
+      = (con_univ_tvs, pprIfaceType (IfaceTyConApp tc (substIfaceTcArgs gadt_subst tys)))
+      | otherwise
+      = (con_univ_tvs, sdocWithDynFlags (ppr_tc_app gadt_subst))
+      where
+        gadt_subst = mkFsEnv eq_spec
+        done_univ_tv (tv,_) = isJust (lookupFsEnv gadt_subst tv)
+        con_univ_tvs = filterOut done_univ_tv (map ifTyConBinderTyVar tc_binders)
+
+    ppr_tc_app gadt_subst dflags
+       = pprPrefixIfDeclBndr ss tycon
+         <+> sep [ pprParendIfaceType (substIfaceTyVar gadt_subst tv)
+                 | (tv,_kind)
+                     <- map ifTyConBinderTyVar $
+                        suppressIfaceInvisibles dflags tc_binders tc_binders ]
+
 instance Outputable IfaceRule where
   ppr (IfaceRule { ifRuleName = name, ifActivation = act, ifRuleBndrs = bndrs,
                    ifRuleHead = fn, ifRuleArgs = args, ifRuleRhs = rhs })
@@ -1149,23 +1149,22 @@ freeNamesIfDecl (IfaceId _s t d i) =
   freeNamesIfIdInfo i &&&
   freeNamesIfIdDetails d
 freeNamesIfDecl d@IfaceData{} =
-  freeNamesIfType (ifKind d) &&&
-  freeNamesIfTvBndrs (ifTyVars d) &&&
+  freeNamesIfTyBinders (ifBinders d) &&&
+  freeNamesIfType (ifResKind d) &&&
   freeNamesIfaceTyConParent (ifParent d) &&&
   freeNamesIfContext (ifCtxt d) &&&
   freeNamesIfConDecls (ifCons d)
 freeNamesIfDecl d@IfaceSynonym{} =
-  freeNamesIfTvBndrs (ifTyVars d) &&&
   freeNamesIfType (ifSynRhs d) &&&
-  freeNamesIfKind (ifSynKind d)
+  freeNamesIfTyBinders (ifBinders d) &&&
+  freeNamesIfKind (ifResKind d)
 freeNamesIfDecl d@IfaceFamily{} =
-  freeNamesIfTvBndrs (ifTyVars d) &&&
   freeNamesIfFamFlav (ifFamFlav d) &&&
-  freeNamesIfKind (ifFamKind d)
+  freeNamesIfTyBinders (ifBinders d) &&&
+  freeNamesIfKind (ifResKind d)
 freeNamesIfDecl d@IfaceClass{} =
-  freeNamesIfTvBndrs (ifTyVars d) &&&
   freeNamesIfContext (ifCtxt d) &&&
-  freeNamesIfType (ifKind d) &&&
+  freeNamesIfTyBinders (ifBinders d) &&&
   fnList freeNamesIfAT     (ifATs d) &&&
   fnList freeNamesIfClsSig (ifSigs d)
 freeNamesIfDecl d@IfaceAxiom{} =
@@ -1305,6 +1304,13 @@ freeNamesIfTvBndrs = fnList freeNamesIfTvBndr
 freeNamesIfForAllBndr :: IfaceForAllBndr -> NameSet
 freeNamesIfForAllBndr (IfaceTv tv _) = freeNamesIfTvBndr tv
 
+freeNamesIfTyBinder :: IfaceTyConBinder -> NameSet
+freeNamesIfTyBinder (IfaceAnon _ ty) = freeNamesIfType ty
+freeNamesIfTyBinder (IfaceNamed b)   = freeNamesIfForAllBndr b
+
+freeNamesIfTyBinders :: [IfaceTyConBinder] -> NameSet
+freeNamesIfTyBinders = fnList freeNamesIfTyBinder
+
 freeNamesIfBndr :: IfaceBndr -> NameSet
 freeNamesIfBndr (IfaceIdBndr b) = freeNamesIfIdBndr b
 freeNamesIfBndr (IfaceTvBndr b) = freeNamesIfTvBndr b
@@ -1475,7 +1481,7 @@ instance Binary IfaceDecl where
         put_ bh a5
         put_ bh a6
 
-    put_ bh (IfaceClass a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) = do
+    put_ bh (IfaceClass a1 a2 a3 a4 a5 a6 a7 a8 a9) = do
         putByte bh 5
         put_ bh a1
         put_ bh (occNameFS a2)
@@ -1486,7 +1492,6 @@ instance Binary IfaceDecl where
         put_ bh a7
         put_ bh a8
         put_ bh a9
-        put_ bh a10
 
     put_ bh (IfaceAxiom a1 a2 a3 a4) = do
         putByte bh 6
@@ -1555,9 +1560,8 @@ instance Binary IfaceDecl where
                     a7 <- get bh
                     a8 <- get bh
                     a9 <- get bh
-                    a10 <- get bh
                     occ <- return $! mkClsOccFS a2
-                    return (IfaceClass a1 occ a3 a4 a5 a6 a7 a8 a9 a10)
+                    return (IfaceClass a1 occ a3 a4 a5 a6 a7 a8 a9)
             6 -> do a1 <- get bh
                     a2 <- get bh
                     a3 <- get bh
index ee7e430..52454ff 100644 (file)
@@ -17,18 +17,21 @@ module IfaceType (
         IfaceTyCon(..), IfaceTyConInfo(..),
         IfaceTyLit(..), IfaceTcArgs(..),
         IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr,
-        IfaceTvBndr, IfaceIdBndr,
+        IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder(..),
         IfaceForAllBndr(..), VisibilityFlag(..),
 
+        ifConstraintKind, ifTyConBinderTyVar, ifTyConBinderName,
+
         -- Equality testing
         IfRnEnv2, emptyIfRnEnv2, eqIfaceType, eqIfaceTypes,
-        eqIfaceTcArgs, eqIfaceTvBndrs,
+        eqIfaceTcArgs, eqIfaceTvBndrs, isIfaceLiftedTypeKind,
 
         -- Conversion from Type -> IfaceType
         toIfaceType, toIfaceTypes, toIfaceKind, toIfaceTyVar,
         toIfaceContext, toIfaceBndr, toIfaceIdBndr,
         toIfaceTyCon, toIfaceTyCon_name,
         toIfaceTcArgs, toIfaceTvBndrs,
+        zipIfaceBinders, toDegenerateBinders,
 
         -- Conversion from IfaceTcArgs -> IfaceType
         tcArgsIfaceTypes,
@@ -39,7 +42,7 @@ module IfaceType (
         -- Printing
         pprIfaceType, pprParendIfaceType,
         pprIfaceContext, pprIfaceContextArr, pprIfaceContextMaybe,
-        pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTvBndrs,
+        pprIfaceIdBndr, pprIfaceLamBndr, pprIfaceTvBndr, pprIfaceTyConBinders,
         pprIfaceBndrs, pprIfaceTcArgs, pprParendIfaceTcArgs,
         pprIfaceForAllPart, pprIfaceForAll, pprIfaceSigmaType,
         pprIfaceCoercion, pprParendIfaceCoercion,
@@ -59,7 +62,6 @@ import DataCon ( isTupleDataCon )
 import TcType
 import DynFlags
 import TyCoRep  -- needs to convert core types to iface types
-import Unique( hasKey )
 import TyCon hiding ( pprPromotionQuote )
 import CoAxiom
 import Id
@@ -67,7 +69,7 @@ import Var
 -- import RnEnv( FastStringEnv, mkFsEnv, lookupFsEnv )
 import TysWiredIn
 import TysPrim
-import PrelNames( funTyConKey, ipClassKey )
+import PrelNames
 import Name
 import BasicTypes
 import Binary
@@ -145,6 +147,11 @@ data IfaceTyLit
 data IfaceForAllBndr
   = IfaceTv IfaceTvBndr VisibilityFlag
 
+data IfaceTyConBinder
+  = IfaceAnon  IfLclName IfaceType   -- like Anon, but it includes a name from
+                                     -- which to produce a tyConTyVar
+  | IfaceNamed IfaceForAllBndr
+
 -- See Note [Suppressing invisible arguments]
 -- We use a new list type (rather than [(IfaceType,Bool)], because
 -- it'll be more compact and faster to parse in interface
@@ -194,6 +201,12 @@ data IfaceUnivCoProv
   | IfaceProofIrrelProv IfaceCoercion
   | IfacePluginProv String
 
+-- this constant is needed for dealing with pretty-printing classes
+ifConstraintKind :: IfaceKind
+ifConstraintKind = IfaceTyConApp (IfaceTyCon { ifaceTyConName = getName constraintKindTyCon
+                                             , ifaceTyConInfo = NoIfaceTyConInfo })
+                                 ITC_Nil
+
 {-
 %************************************************************************
 %*                                                                      *
@@ -205,6 +218,15 @@ data IfaceUnivCoProv
 eqIfaceTvBndr :: IfaceTvBndr -> IfaceTvBndr -> Bool
 eqIfaceTvBndr (occ1, _) (occ2, _) = occ1 == occ2
 
+isIfaceLiftedTypeKind :: IfaceKind -> Bool
+isIfaceLiftedTypeKind (IfaceTyConApp tc ITC_Nil)
+  = isLiftedTypeKindTyConName (ifaceTyConName tc)
+isIfaceLiftedTypeKind (IfaceTyConApp tc
+                       (ITC_Vis (IfaceTyConApp ptr_rep_lifted ITC_Nil) ITC_Nil))
+  =  ifaceTyConName tc      == tYPETyConName
+  && ifaceTyConName ptr_rep_lifted `hasKey` ptrRepLiftedDataConKey
+isIfaceLiftedTypeKind _ = False
+
 splitIfaceSigmaTy :: IfaceType -> ([IfaceForAllBndr], [IfacePredType], IfaceType)
 -- Mainly for printing purposes
 splitIfaceSigmaTy ty
@@ -221,7 +243,7 @@ splitIfaceSigmaTy ty
         = case split_rho ty2 of { (ps, tau) -> (ty1:ps, tau) }
     split_rho tau = ([], tau)
 
-suppressIfaceInvisibles :: DynFlags -> [IfaceForAllBndr] -> [a] -> [a]
+suppressIfaceInvisibles :: DynFlags -> [IfaceTyConBinder] -> [a] -> [a]
 suppressIfaceInvisibles dflags tys xs
   | gopt Opt_PrintExplicitKinds dflags = xs
   | otherwise = suppress tys xs
@@ -232,14 +254,25 @@ suppressIfaceInvisibles dflags tys xs
         | isIfaceInvisBndr k = suppress ks xs
         | otherwise          = a
 
-stripIfaceInvisVars :: DynFlags -> [IfaceForAllBndr] -> [IfaceForAllBndr]
+stripIfaceInvisVars :: DynFlags -> [IfaceTyConBinder] -> [IfaceTyConBinder]
 stripIfaceInvisVars dflags tyvars
   | gopt Opt_PrintExplicitKinds dflags = tyvars
   | otherwise = filterOut isIfaceInvisBndr tyvars
 
-isIfaceInvisBndr :: IfaceForAllBndr -> Bool
-isIfaceInvisBndr (IfaceTv _ Visible) = False
-isIfaceInvisBndr _                   = True
+isIfaceInvisBndr :: IfaceTyConBinder -> Bool
+isIfaceInvisBndr (IfaceNamed (IfaceTv _ Invisible)) = True
+isIfaceInvisBndr (IfaceNamed (IfaceTv _ Specified)) = True
+isIfaceInvisBndr _                                  = False
+
+-- | Extract a IfaceTvBndr from a IfaceTyConBinder
+ifTyConBinderTyVar :: IfaceTyConBinder -> IfaceTvBndr
+ifTyConBinderTyVar (IfaceAnon name ki)         = (name, ki)
+ifTyConBinderTyVar (IfaceNamed (IfaceTv tv _)) = tv
+
+-- | Extract the variable name from a IfaceTyConBinder
+ifTyConBinderName :: IfaceTyConBinder -> IfLclName
+ifTyConBinderName (IfaceAnon name _)                 = name
+ifTyConBinderName (IfaceNamed (IfaceTv (name, _) _)) = name
 
 ifTyVarsOfType :: IfaceType -> UniqSet IfLclName
 ifTyVarsOfType ty
@@ -568,16 +601,15 @@ pprIfaceIdBndr :: (IfLclName, IfaceType) -> SDoc
 pprIfaceIdBndr (name, ty) = parens (ppr name <+> dcolon <+> ppr ty)
 
 pprIfaceTvBndr :: IfaceTvBndr -> SDoc
-pprIfaceTvBndr (tv, IfaceTyConApp tc ITC_Nil)
-  | isLiftedTypeKindTyConName (ifaceTyConName tc) = ppr tv
-pprIfaceTvBndr (tv, IfaceTyConApp tc (ITC_Vis (IfaceTyConApp lifted ITC_Nil) ITC_Nil))
-  | ifaceTyConName tc     == tYPETyConName
-  , ifaceTyConName lifted == liftedDataConName
-  = ppr tv
-pprIfaceTvBndr (tv, kind) = parens (ppr tv <+> dcolon <+> ppr kind)
+pprIfaceTvBndr (tv, ki)
+  | isIfaceLiftedTypeKind ki = ppr tv
+  | otherwise                = parens (ppr tv <+> dcolon <+> ppr ki)
 
-pprIfaceTvBndrs :: [IfaceTvBndr] -> SDoc
-pprIfaceTvBndrs tyvars = sep (map pprIfaceTvBndr tyvars)
+pprIfaceTyConBinders :: [IfaceTyConBinder] -> SDoc
+pprIfaceTyConBinders = sep . map go
+  where
+    go (IfaceAnon name ki)         = pprIfaceTvBndr (name, ki)
+    go (IfaceNamed (IfaceTv tv _)) = pprIfaceTvBndr tv
 
 instance Binary IfaceBndr where
     put_ bh (IfaceIdBndr aa) = do
@@ -786,11 +818,14 @@ pprTyTcApp ctxt_prec tc tys dflags
   = pprIfaceTyList ctxt_prec ty1 ty2
 
   | ifaceTyConName tc == tYPETyConName
-  , ITC_Vis (IfaceTyConApp lev_tc ITC_Nil) ITC_Nil <- tys
-  = let n = ifaceTyConName lev_tc in
-    if n == liftedDataConName then char '*'
-    else if n == unliftedDataConName then char '#'
-         else pprPanic "IfaceType.pprTyTcApp" (ppr lev_tc)
+  , ITC_Vis (IfaceTyConApp ptr_rep ITC_Nil) ITC_Nil <- tys
+  , ifaceTyConName ptr_rep `hasKey` ptrRepLiftedDataConKey
+  = char '*'
+
+  | ifaceTyConName tc == tYPETyConName
+  , ITC_Vis (IfaceTyConApp ptr_rep ITC_Nil) ITC_Nil <- tys
+  , ifaceTyConName ptr_rep `hasKey` ptrRepUnliftedDataConKey
+  = char '#'
 
   | otherwise
   = ppr_iface_tc_app ppr_ty ctxt_prec tc tys_wo_kinds
@@ -826,8 +861,8 @@ ppr_iface_tc_app pp ctxt_prec tc tys
 
 pprTuple :: TupleSort -> IfaceTyConInfo -> IfaceTcArgs -> SDoc
 pprTuple sort info args
-  =   -- drop the levity vars.
-      -- See Note [Unboxed tuple levity vars] in TyCon
+  =   -- drop the RuntimeRep vars.
+      -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
     let tys   = tcArgsIfaceTypes args
         args' = case sort of
                   UnboxedTuple -> drop (length tys `div` 2) tys
@@ -968,6 +1003,21 @@ instance Binary IfaceForAllBndr where
      vis <- get bh
      return (IfaceTv tv vis)
 
+instance Binary IfaceTyConBinder where
+  put_ bh (IfaceAnon n ty) = putByte bh 0 >> put_ bh n >> put_ bh ty
+  put_ bh (IfaceNamed b)   = putByte bh 1 >> put_ bh b
+
+  get bh =
+    do c <- getByte bh
+       case c of
+         0 -> do
+           n  <- get bh
+           ty <- get bh
+           return $! IfaceAnon n ty
+         _ -> do
+           b <- get bh
+           return $! IfaceNamed b
+
 instance Binary IfaceTcArgs where
   put_ bh tk =
     case tk of
@@ -1360,3 +1410,20 @@ toIfaceUnivCoProv (PhantomProv co)    = IfacePhantomProv (toIfaceCoercion co)
 toIfaceUnivCoProv (ProofIrrelProv co) = IfaceProofIrrelProv (toIfaceCoercion co)
 toIfaceUnivCoProv (PluginProv str)    = IfacePluginProv str
 toIfaceUnivCoProv (HoleProv h) = pprPanic "toIfaceUnivCoProv hit a hole" (ppr h)
+
+----------------------
+-- | Zip together tidied tyConTyVars with tyConBinders to make IfaceTyConBinders
+zipIfaceBinders :: [TyVar] -> [TyBinder] -> [IfaceTyConBinder]
+zipIfaceBinders = zipWith go
+  where
+    go tv (Anon _)      = let (name, ki) = toIfaceTvBndr tv in
+                          IfaceAnon name ki
+    go tv (Named _ vis) = IfaceNamed (IfaceTv (toIfaceTvBndr tv) vis)
+
+-- | Make IfaceTyConBinders without tyConTyVars. Used for pretty-printing only
+toDegenerateBinders :: [TyBinder] -> [IfaceTyConBinder]
+toDegenerateBinders = zipWith go [1..]
+  where
+    go :: Int -> TyBinder -> IfaceTyConBinder
+    go n (Anon ty)      = IfaceAnon (mkFastString ("t" ++ show n)) (toIfaceType ty)
+    go _ (Named tv vis) = IfaceNamed (IfaceTv (toIfaceTvBndr tv) vis)
index 8548eb3..4bd5c36 100644 (file)
@@ -76,7 +76,6 @@ import DataCon
 import PatSyn
 import Type
 import TcType
-import TysPrim ( alphaTyVars )
 import InstEnv
 import FamInstEnv
 import TcRnMonad
@@ -1377,28 +1376,28 @@ tyConToIfaceDecl env tycon
   | Just syn_rhs <- synTyConRhs_maybe tycon
   = ( tc_env1
     , IfaceSynonym { ifName    = getOccName tycon,
-                     ifTyVars  = if_tc_tyvars,
                      ifRoles   = tyConRoles tycon,
                      ifSynRhs  = if_syn_type syn_rhs,
-                     ifSynKind = if_kind
+                     ifBinders = if_binders,
+                     ifResKind = if_res_kind
                    })
 
   | Just fam_flav <- famTyConFlav_maybe tycon
   = ( tc_env1
     , IfaceFamily { ifName    = getOccName tycon,
-                    ifTyVars  = if_tc_tyvars,
                     ifResVar  = if_res_var,
                     ifFamFlav = to_if_fam_flav fam_flav,
-                    ifFamKind = if_kind,
+                    ifBinders = if_binders,
+                    ifResKind = if_res_kind,
                     ifFamInj  = familyTyConInjectivityInfo tycon
                   })
 
   | isAlgTyCon tycon
   = ( tc_env1
     , IfaceData { ifName    = getOccName tycon,
-                  ifKind    = if_kind,
+                  ifBinders = if_binders,
+                  ifResKind = if_res_kind,
                   ifCType   = tyConCType tycon,
-                  ifTyVars  = if_tc_tyvars,
                   ifRoles   = tyConRoles tycon,
                   ifCtxt    = tidyToIfaceContext tc_env1 (tyConStupidTheta tycon),
                   ifCons    = ifaceConDecls (algTyConRhs tycon) (algTcFields tycon),
@@ -1410,12 +1409,10 @@ tyConToIfaceDecl env tycon
   -- For pretty printing purposes only.
   = ( env
     , IfaceData { ifName       = getOccName tycon,
-                  ifKind       =
-                    -- These don't have `tyConTyVars`, so we use an empty
-                    -- environment here, instead of `tc_env1` defined below.
-                    tidyToIfaceType emptyTidyEnv (tyConKind tycon),
+                  ifBinders    = if_degenerate_binders,
+                  ifResKind    = if_degenerate_res_kind,
+                    -- These don't have `tyConTyVars`, hence "degenerate"
                   ifCType      = Nothing,
-                  ifTyVars     = funAndPrimTyVars,
                   ifRoles      = tyConRoles tycon,
                   ifCtxt       = [],
                   ifCons       = IfDataTyCon [] False [],
@@ -1427,12 +1424,16 @@ tyConToIfaceDecl env tycon
     -- is one of these TyCons (FunTyCon, PrimTyCon, PromotedDataCon) will cause
     -- an error.
     (tc_env1, tc_tyvars) = tidyTyClTyCoVarBndrs env (tyConTyVars tycon)
-    if_tc_tyvars = toIfaceTvBndrs tc_tyvars
-    if_kind = tidyToIfaceType tc_env1 (tyConKind tycon)
+    if_binders  = zipIfaceBinders tc_tyvars (tyConBinders tycon)
+    if_res_kind = tidyToIfaceType tc_env1 (tyConResKind tycon)
     if_syn_type ty = tidyToIfaceType tc_env1 ty
     if_res_var     = getFS `fmap` tyConFamilyResVar_maybe tycon
 
-    funAndPrimTyVars = toIfaceTvBndrs $ take (tyConArity tycon) alphaTyVars
+      -- use these when you don't have tyConTyVars
+    (degenerate_binders, degenerate_res_kind)
+      = splitPiTys (tidyType env (tyConKind tycon))
+    if_degenerate_binders  = toDegenerateBinders degenerate_binders
+    if_degenerate_res_kind = toIfaceType degenerate_res_kind
 
     parent = case tyConFamInstSig_maybe tycon of
                Just (tc, ty, ax) -> IfDataInstance (coAxiomName ax)
@@ -1522,9 +1523,8 @@ classToIfaceDecl env clas
   = ( env1
     , IfaceClass { ifCtxt   = tidyToIfaceContext env1 sc_theta,
                    ifName   = getOccName tycon,
-                   ifTyVars = toIfaceTvBndrs clas_tyvars',
                    ifRoles  = tyConRoles (classTyCon clas),
-                   ifKind   = tidyToIfaceType env1 (tyConKind tycon),
+                   ifBinders = binders,
                    ifFDs    = map toIfaceFD clas_fds,
                    ifATs    = map toIfaceAT clas_ats,
                    ifSigs   = map toIfaceClassOp op_stuff,
@@ -1536,6 +1536,7 @@ classToIfaceDecl env clas
     tycon = classTyCon clas
 
     (env1, clas_tyvars') = tidyTyCoVarBndrs env clas_tyvars
+    binders = zipIfaceBinders clas_tyvars' (tyConBinders tycon)
 
     toIfaceAT :: ClassATItem -> IfaceAT
     toIfaceAT (ATI tc def)
index 2e8a6ed..8599afa 100644 (file)
@@ -312,20 +312,21 @@ tc_iface_decl _ ignore_prags (IfaceId {ifName = occ_name, ifType = iface_type,
 
 tc_iface_decl _ _ (IfaceData {ifName = occ_name,
                           ifCType = cType,
-                          ifKind = kind,
-                          ifTyVars = tv_bndrs,
+                          ifBinders = binders,
+                          ifResKind = res_kind,
                           ifRoles = roles,
                           ifCtxt = ctxt, ifGadtSyntax = gadt_syn,
                           ifCons = rdr_cons,
                           ifRec = is_rec, ifParent = mb_parent })
-  = bindIfaceTyVars_AT tv_bndrs $ \ tyvars -> do
+  = bindIfaceTyConBinders_AT binders $ \ tyvars binders' -> do
     { tc_name <- lookupIfaceTop occ_name
-    ; kind' <- tcIfaceType kind
+    ; res_kind' <- tcIfaceType res_kind
+
     ; tycon <- fixM $ \ tycon -> do
             { stupid_theta <- tcIfaceCtxt ctxt
             ; parent' <- tc_parent tc_name mb_parent
             ; cons <- tcIfaceDataCons tc_name tycon tyvars rdr_cons
-            ; return (mkAlgTyCon tc_name kind' tyvars roles cType stupid_theta
+            ; return (mkAlgTyCon tc_name binders' res_kind' tyvars roles cType stupid_theta
                                     cons parent' is_rec gadt_syn) }
     ; traceIf (text "tcIfaceDecl4" <+> ppr tycon)
     ; return (ATyCon tycon) }
@@ -341,31 +342,33 @@ tc_iface_decl _ _ (IfaceData {ifName = occ_name,
            ; lhs_tys <- tcIfaceTcArgs arg_tys
            ; return (DataFamInstTyCon ax_unbr fam_tc lhs_tys) }
 
-tc_iface_decl _ _ (IfaceSynonym {ifName = occ_name, ifTyVars = tv_bndrs,
+tc_iface_decl _ _ (IfaceSynonym {ifName = occ_name,
                                       ifRoles = roles,
                                       ifSynRhs = rhs_ty,
-                                      ifSynKind = kind })
-   = bindIfaceTyVars_AT tv_bndrs $ \ tyvars -> do
+                                      ifBinders = binders,
+                                      ifResKind = res_kind })
+   = bindIfaceTyConBinders_AT binders $ \ tyvars binders' -> do
      { tc_name  <- lookupIfaceTop occ_name
-     ; kind     <- tcIfaceType kind     -- Note [Synonym kind loop]
+     ; res_kind' <- tcIfaceType res_kind     -- Note [Synonym kind loop]
      ; rhs      <- forkM (mk_doc tc_name) $
                    tcIfaceType rhs_ty
-     ; let tycon = mkSynonymTyCon tc_name kind tyvars roles rhs
+     ; let tycon = mkSynonymTyCon tc_name binders' res_kind' tyvars roles rhs
      ; return (ATyCon tycon) }
    where
      mk_doc n = text "Type synonym" <+> ppr n
 
-tc_iface_decl parent _ (IfaceFamily {ifName = occ_name, ifTyVars = tv_bndrs,
+tc_iface_decl parent _ (IfaceFamily {ifName = occ_name,
                                      ifFamFlav = fam_flav,
-                                     ifFamKind = kind,
+                                     ifBinders = binders,
+                                     ifResKind = res_kind,
                                      ifResVar = res, ifFamInj = inj })
-   = bindIfaceTyVars_AT tv_bndrs $ \ tyvars -> do
-     { tc_name  <- lookupIfaceTop occ_name
-     ; kind     <- tcIfaceType kind        -- Note [Synonym kind loop]
+   = bindIfaceTyConBinders_AT binders $ \ tyvars binders' -> do
+     { tc_name   <- lookupIfaceTop occ_name
+     ; res_kind' <- tcIfaceType res_kind    -- Note [Synonym kind loop]
      ; rhs      <- forkM (mk_doc tc_name) $
                    tc_fam_flav tc_name fam_flav
      ; res_name <- traverse (newIfaceName . mkTyVarOccFS) res
-     ; let tycon = mkFamilyTyCon tc_name kind tyvars res_name rhs parent inj
+     ; let tycon = mkFamilyTyCon tc_name binders' res_kind' tyvars res_name rhs parent inj
      ; return (ATyCon tycon) }
    where
      mk_doc n = text "Type synonym" <+> ppr n
@@ -386,15 +389,15 @@ tc_iface_decl parent _ (IfaceFamily {ifName = occ_name, ifTyVars = tv_bndrs,
 
 tc_iface_decl _parent ignore_prags
             (IfaceClass {ifCtxt = rdr_ctxt, ifName = tc_occ,
-                         ifTyVars = tv_bndrs, ifRoles = roles, ifKind = kind,
+                         ifRoles = roles,
+                         ifBinders = binders,
                          ifFDs = rdr_fds,
                          ifATs = rdr_ats, ifSigs = rdr_sigs,
                          ifMinDef = mindef_occ, ifRec = tc_isrec })
 -- ToDo: in hs-boot files we should really treat abstract classes specially,
 --       as we do abstract tycons
-  = bindIfaceTvBndrs tv_bndrs $ \ tyvars -> do
+  = bindIfaceTyConBinders binders $ \ tyvars binders' -> do
     { tc_name <- lookupIfaceTop tc_occ
-    ; kind' <- tcIfaceType kind
     ; traceIf (text "tc-iface-class1" <+> ppr tc_occ)
     ; ctxt <- mapM tc_sc rdr_ctxt
     ; traceIf (text "tc-iface-class2" <+> ppr tc_occ)
@@ -405,7 +408,7 @@ tc_iface_decl _parent ignore_prags
     ; cls  <- fixM $ \ cls -> do
               { ats  <- mapM (tc_at cls) rdr_ats
               ; traceIf (text "tc-iface-class4" <+> ppr tc_occ)
-              ; buildClass tc_name tyvars roles ctxt kind' fds ats sigs mindef tc_isrec }
+              ; buildClass tc_name tyvars roles ctxt binders' fds ats sigs mindef tc_isrec }
     ; return (ATyCon (classTyCon cls)) }
   where
    tc_sc pred = forkM (mk_sc_doc pred) (tcIfaceType pred)
@@ -509,7 +512,8 @@ tc_ax_branch prev_branches
              (IfaceAxBranch { ifaxbTyVars = tv_bndrs, ifaxbCoVars = cv_bndrs
                             , ifaxbLHS = lhs, ifaxbRHS = rhs
                             , ifaxbRoles = roles, ifaxbIncomps = incomps })
-  = bindIfaceTyVars_AT tv_bndrs $ \ tvs ->
+  = bindIfaceTyConBinders_AT
+      (map (\b -> IfaceNamed (IfaceTv b Invisible)) tv_bndrs) $ \ tvs _ ->
          -- The _AT variant is needed here; see Note [CoAxBranch type variables] in CoAxiom
     bindIfaceIds cv_bndrs $ \ cvs -> do
     { tc_lhs <- tcIfaceTcArgs lhs
@@ -905,7 +909,7 @@ tcIfaceTupleTy sort info args
                         kind_args = map typeKind args'
                   ; return (mkTyConApp tc (kind_args ++ args')) } }
 
--- See Note [Unboxed tuple levity vars] in TyCon
+-- See Note [Unboxed tuple RuntimeRep vars] in TyCon
 tcTupleTyCon :: Bool    -- True <=> typechecking a *type* (vs. an expr)
              -> TupleSort
              -> Arity   -- the number of args. *not* the tuple arity.
@@ -1024,7 +1028,7 @@ tcIfaceExpr (IfaceTuple sort args)
        ; let con_tys = map exprType args'
              some_con_args = map Type con_tys ++ args'
              con_args = case sort of
-               UnboxedTuple -> map (Type . getLevity "tcIfaceExpr") con_tys ++ some_con_args
+               UnboxedTuple -> map (Type . getRuntimeRep "tcIfaceExpr") con_tys ++ some_con_args
                _            -> some_con_args
                         -- Put the missing type arguments back in
              con_id   = dataConWorkId (tyConSingleDataCon tc)
@@ -1426,21 +1430,39 @@ mk_iface_tyvar name ifKind
    = do { kind <- tcIfaceType ifKind
         ; return (Var.mkTyVar name kind) }
 
-bindIfaceTyVars_AT :: [IfaceTvBndr] -> ([TyVar] -> IfL a) -> IfL a
+bindIfaceTyConBinders :: [IfaceTyConBinder]
+                      -> ([TyVar] -> [TyBinder] -> IfL a) -> IfL a
+bindIfaceTyConBinders [] thing_inside = thing_inside [] []
+bindIfaceTyConBinders (b:bs) thing_inside
+  = bindIfaceTyConBinderX bindIfaceTyVar b $ \ tv'  b'  ->
+    bindIfaceTyConBinders bs               $ \ tvs' bs' ->
+    thing_inside (tv':tvs') (b':bs')
+
+bindIfaceTyConBinders_AT :: [IfaceTyConBinder]
+                         -> ([TyVar] -> [TyBinder] -> IfL a) -> IfL a
 -- Used for type variable in nested associated data/type declarations
 -- where some of the type variables are already in scope
 --    class C a where { data T a b }
 -- Here 'a' is in scope when we look at the 'data T'
-bindIfaceTyVars_AT [] thing_inside
-  = thing_inside []
-bindIfaceTyVars_AT (b : bs) thing_inside
-  = do { bindIfaceTyVar_AT b $ \b' ->
-         bindIfaceTyVars_AT bs $ \bs' ->
-         thing_inside (b':bs') }
-
-bindIfaceTyVar_AT :: IfaceTvBndr -> (TyVar -> IfL a) -> IfL a
-bindIfaceTyVar_AT tv thing
-  = do { mb_tv <- lookupIfaceTyVar tv
-       ; case mb_tv of
-           Just b' -> thing b'
-           Nothing -> bindIfaceTyVar tv thing }
+bindIfaceTyConBinders_AT [] thing_inside
+  = thing_inside [] []
+bindIfaceTyConBinders_AT (b : bs) thing_inside
+  = bindIfaceTyConBinderX bind_tv b  $ \tv'  b'  ->
+    bindIfaceTyConBinders_AT      bs $ \tvs' bs' ->
+    thing_inside (tv':tvs') (b':bs')
+  where
+    bind_tv tv thing
+      = do { mb_tv <- lookupIfaceTyVar tv
+           ; case mb_tv of
+               Just b' -> thing b'
+               Nothing -> bindIfaceTyVar tv thing }
+
+bindIfaceTyConBinderX :: (IfaceTvBndr -> (TyVar -> IfL a) -> IfL a)
+                      -> IfaceTyConBinder
+                      -> (TyVar -> TyBinder -> IfL a) -> IfL a
+bindIfaceTyConBinderX bind_tv (IfaceAnon name ki) thing_inside
+  = bind_tv (name, ki) $ \ tv' ->
+    thing_inside tv' (Anon (tyVarKind tv'))
+bindIfaceTyConBinderX bind_tv (IfaceNamed (IfaceTv tv vis)) thing_inside
+  = bind_tv tv $ \tv' ->
+    thing_inside tv' (Named tv' vis)
index 5c2984b..068f276 100644 (file)
@@ -1617,15 +1617,18 @@ eitherTyConKey                          = mkPreludeTyConUnique 84
 
 -- Kind constructors
 liftedTypeKindTyConKey, tYPETyConKey,
-  unliftedTypeKindTyConKey, constraintKindTyConKey, levityTyConKey,
-  starKindTyConKey, unicodeStarKindTyConKey :: Unique
+  unliftedTypeKindTyConKey, constraintKindTyConKey,
+  starKindTyConKey, unicodeStarKindTyConKey, runtimeRepTyConKey,
+  vecCountTyConKey, vecElemTyConKey :: Unique
 liftedTypeKindTyConKey                  = mkPreludeTyConUnique 87
 tYPETyConKey                            = mkPreludeTyConUnique 88
 unliftedTypeKindTyConKey                = mkPreludeTyConUnique 89
-levityTyConKey                          = mkPreludeTyConUnique 90
 constraintKindTyConKey                  = mkPreludeTyConUnique 92
 starKindTyConKey                        = mkPreludeTyConUnique 93
 unicodeStarKindTyConKey                 = mkPreludeTyConUnique 94
+runtimeRepTyConKey                      = mkPreludeTyConUnique 95
+vecCountTyConKey                        = mkPreludeTyConUnique 96
+vecElemTyConKey                         = mkPreludeTyConUnique 97
 
 pluginTyConKey, frontendPluginTyConKey :: Unique
 pluginTyConKey                          = mkPreludeTyConUnique 102
@@ -1808,11 +1811,6 @@ fingerprintDataConKey                   = mkPreludeDataConUnique 35
 srcLocDataConKey :: Unique
 srcLocDataConKey                        = mkPreludeDataConUnique 37
 
--- Levity
-liftedDataConKey, unliftedDataConKey :: Unique
-liftedDataConKey                        = mkPreludeDataConUnique 39
-unliftedDataConKey                      = mkPreludeDataConUnique 40
-
 trTyConTyConKey, trTyConDataConKey,
   trModuleTyConKey, trModuleDataConKey,
   trNameTyConKey, trNameSDataConKey, trNameDDataConKey,
@@ -1861,6 +1859,26 @@ metaDataDataConKey                      = mkPreludeDataConUnique 68
 metaConsDataConKey                      = mkPreludeDataConUnique 69
 metaSelDataConKey                       = mkPreludeDataConUnique 70
 
+vecRepDataConKey :: Unique
+vecRepDataConKey                        = mkPreludeDataConUnique 71
+
+-- See Note [Wiring in RuntimeRep] in TysWiredIn
+runtimeRepSimpleDataConKeys :: [Unique]
+ptrRepLiftedDataConKey, ptrRepUnliftedDataConKey :: Unique
+runtimeRepSimpleDataConKeys@(
+  ptrRepLiftedDataConKey : ptrRepUnliftedDataConKey : _)
+  = map mkPreludeDataConUnique [72..82]
+
+-- See Note [Wiring in RuntimeRep] in TysWiredIn
+-- VecCount
+vecCountDataConKeys :: [Unique]
+vecCountDataConKeys = map mkPreludeDataConUnique [83..88]
+
+-- See Note [Wiring in RuntimeRep] in TysWiredIn
+-- VecElem
+vecElemDataConKeys :: [Unique]
+vecElemDataConKeys = map mkPreludeDataConUnique [89..98]
+
 ---------------- Template Haskell -------------------
 --      THNames.hs: USES DataUniques 100-150
 -----------------------------------------------------
@@ -2232,5 +2250,5 @@ pretendNameIsInScope :: Name -> Bool
 pretendNameIsInScope n
   = any (n `hasKey`)
     [ starKindTyConKey, liftedTypeKindTyConKey, tYPETyConKey
-    , unliftedTypeKindTyConKey, levityTyConKey, liftedDataConKey
-    , unliftedDataConKey ]
+    , unliftedTypeKindTyConKey
+    , runtimeRepTyConKey, ptrRepLiftedDataConKey, ptrRepUnliftedDataConKey ]
index 66172ac..7b37062 100644 (file)
@@ -30,7 +30,7 @@ import TysWiredIn
 import CmmType
 import Demand
 import OccName          ( OccName, pprOccName, mkVarOccFS )
-import TyCon            ( TyCon, isPrimTyCon, tyConPrimRep, PrimRep(..) )
+import TyCon            ( TyCon, isPrimTyCon, PrimRep(..) )
 import Type
 import BasicTypes       ( Arity, Fixity(..), FixityDirection(..), Boxity(..) )
 import ForeignCall      ( CLabelString )
index d1e42d5..ce25c30 100644 (file)
@@ -15,13 +15,11 @@ module TysPrim(
         mkTemplateTyVars,
         alphaTyVars, alphaTyVar, betaTyVar, gammaTyVar, deltaTyVar,
         alphaTys, alphaTy, betaTy, gammaTy, deltaTy,
-        levity1TyVar, levity2TyVar, levity1Ty, levity2Ty,
+        runtimeRep1TyVar, runtimeRep2TyVar, runtimeRep1Ty, runtimeRep2Ty,
         openAlphaTy, openBetaTy, openAlphaTyVar, openBetaTyVar,
         kKiVar,
 
         -- Kind constructors...
-        tYPETyCon, unliftedTypeKindTyCon, unliftedTypeKind,
-
         tYPETyConName, unliftedTypeKindTyConName,
 
         -- Kinds
@@ -80,7 +78,18 @@ module TysPrim(
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} TysWiredIn ( levityTy, unliftedDataConTy, liftedTypeKind )
+import {-# SOURCE #-} TysWiredIn
+  ( runtimeRepTy, liftedTypeKind
+  , vecRepDataConTyCon, ptrRepUnliftedDataConTyCon
+  , voidRepDataConTy, intRepDataConTy
+  , wordRepDataConTy, int64RepDataConTy, word64RepDataConTy, addrRepDataConTy
+  , floatRepDataConTy, doubleRepDataConTy
+  , vec2DataConTy, vec4DataConTy, vec8DataConTy, vec16DataConTy, vec32DataConTy
+  , vec64DataConTy
+  , int8ElemRepDataConTy, int16ElemRepDataConTy, int32ElemRepDataConTy
+  , int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy
+  , word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy
+  , doubleElemRepDataConTy )
 
 import Var              ( TyVar, KindVar, mkTyVar )
 import Name
@@ -89,6 +98,7 @@ import SrcLoc
 import Unique
 import PrelNames
 import FastString
+import Outputable
 import TyCoRep   -- doesn't need special access, but this is easier to avoid
                  -- import loops
 
@@ -228,17 +238,17 @@ alphaTys = mkTyVarTys alphaTyVars
 alphaTy, betaTy, gammaTy, deltaTy :: Type
 (alphaTy:betaTy:gammaTy:deltaTy:_) = alphaTys
 
-levity1TyVar, levity2TyVar :: TyVar
-(levity1TyVar : levity2TyVar : _)
-  = drop 21 (mkTemplateTyVars (repeat levityTy))  -- selects 'v','w'
+runtimeRep1TyVar, runtimeRep2TyVar :: TyVar
+(runtimeRep1TyVar : runtimeRep2TyVar : _)
+  = drop 16 (mkTemplateTyVars (repeat runtimeRepTy))  -- selects 'q','r'
 
-levity1Ty, levity2Ty :: Type
-levity1Ty = mkTyVarTy levity1TyVar
-levity2Ty = mkTyVarTy levity2TyVar
+runtimeRep1Ty, runtimeRep2Ty :: Type
+runtimeRep1Ty = mkTyVarTy runtimeRep1TyVar
+runtimeRep2Ty = mkTyVarTy runtimeRep2TyVar
 
 openAlphaTyVar, openBetaTyVar :: TyVar
 [openAlphaTyVar,openBetaTyVar]
-  = mkTemplateTyVars [tYPE levity1Ty, tYPE levity2Ty]
+  = mkTemplateTyVars [tYPE runtimeRep1Ty, tYPE runtimeRep2Ty]
 
 openAlphaTy, openBetaTy :: Type
 openAlphaTy = mkTyVarTy openAlphaTyVar
@@ -260,9 +270,9 @@ funTyConName :: Name
 funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
 
 funTyCon :: TyCon
-funTyCon = mkFunTyCon funTyConName kind tc_rep_nm
+funTyCon = mkFunTyCon funTyConName (map Anon [liftedTypeKind, liftedTypeKind])
+                                   tc_rep_nm
   where
-    kind = mkFunTys [liftedTypeKind, liftedTypeKind] liftedTypeKind
         -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
         -- But if we do that we get kind errors when saying
         --      instance Control.Arrow (->)
@@ -274,20 +284,6 @@ funTyCon = mkFunTyCon funTyConName kind tc_rep_nm
 
     tc_rep_nm = mkPrelTyConRepName funTyConName
 
--- One step to remove subkinding.
--- (->) :: * -> * -> *
--- but we should have (and want) the following typing rule for fully applied arrows
---      Gamma |- tau   :: k1    k1 in {*, #}
---      Gamma |- sigma :: k2    k2 in {*, #, (#)}
---      -----------------------------------------
---      Gamma |- tau -> sigma :: *
--- Currently we have the following rule which achieves more or less the same effect
---      Gamma |- tau   :: ??
---      Gamma |- sigma :: ?
---      --------------------------
---      Gamma |- tau -> sigma :: *
--- In the end we don't want subkinding at all.
-
 {-
 ************************************************************************
 *                                                                      *
@@ -299,35 +295,48 @@ Note [TYPE]
 ~~~~~~~~~~~
 There are a few places where we wish to be able to deal interchangeably
 with kind * and kind #. unsafeCoerce#, error, and (->) are some of these
-places. The way we do this is to use levity polymorphism.
+places. The way we do this is to use runtime-representation polymorphism.
 
-We have (levityTyCon, liftedDataCon, unliftedDataCon)
+We have
 
-    data Levity = Lifted | Unlifted
+    data RuntimeRep = PtrRepLifted | PtrRepUnlifted | ...
 
 and a magical constant (tYPETyCon)
 
-    TYPE :: Levity -> TYPE Lifted
+    TYPE :: RuntimeRep -> TYPE PtrRepLifted
 
 We then have synonyms (liftedTypeKindTyCon, unliftedTypeKindTyCon)
 
-    type Type = TYPE Lifted
-    type # = TYPE Unlifted
+    type * = TYPE PtrRepLifted
+    type # = TYPE PtrRepUnlifted
+
+The (...) in the definition for RuntimeRep includes possibilities for
+the unboxed, unlifted representations, isomorphic to the PrimRep type
+in TyCon. RuntimeRep is itself declared in GHC.Types.
+
+An alternative design would be to have
+
+  data RuntimeRep = PtrRep Levity | ...
+  data Levity = Lifted | Unlifted
 
-So, for example, we get
+but this slowed down GHC because every time we looked at *, we had to
+follow a bunch of pointers. When we have unpackable sums, we should
+go back to the stratified representation. This would allow, for example:
 
-    unsafeCoerce# :: forall (v1 :: Levity) (v2 :: Levity)
+    unsafeCoerce# :: forall (r1 :: RuntimeRep) (v2 :: Levity)
                             (a :: TYPE v1) (b :: TYPE v2). a -> b
 
-This replaces the old sub-kinding machinery. We call variables `a` and `b`
-above "levity polymorphic".
+TYPE replaces the old sub-kinding machinery. We call variables `a` and `b`
+above "runtime-representation polymorphic".
+
 -}
 
 tYPETyCon, unliftedTypeKindTyCon :: TyCon
 tYPETyConName, unliftedTypeKindTyConName :: Name
 
 tYPETyCon = mkKindTyCon tYPETyConName
-                        (ForAllTy (Anon levityTy) liftedTypeKind)
+                        [Anon runtimeRepTy]
+                        liftedTypeKind
                         [Nominal]
                         (mkPrelTyConRepName tYPETyConName)
 
@@ -335,9 +344,9 @@ tYPETyCon = mkKindTyCon tYPETyConName
    -- NB: unlifted is wired in because there is no way to parse it in
    -- Haskell. That's the only reason for wiring it in.
 unliftedTypeKindTyCon = mkSynonymTyCon unliftedTypeKindTyConName
-                                       liftedTypeKind
-                                       [] []
-                                       (tYPE unliftedDataConTy)
+                          [] liftedTypeKind
+                          [] []
+                          (tYPE (TyConApp ptrRepUnliftedDataConTyCon []))
 
 --------------------------
 -- ... and now their names
@@ -347,9 +356,6 @@ unliftedTypeKindTyCon = mkSynonymTyCon unliftedTypeKindTyConName
 tYPETyConName             = mkPrimTyConName (fsLit "TYPE") tYPETyConKey tYPETyCon
 unliftedTypeKindTyConName = mkPrimTyConName (fsLit "#") unliftedTypeKindTyConKey unliftedTypeKindTyCon
 
-unliftedTypeKind :: Kind
-unliftedTypeKind = tYPE unliftedDataConTy
-
 mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
 mkPrimTyConName = mkPrimTcName BuiltInSyntax
   -- All of the super kinds and kinds are defined in Prim,
@@ -360,9 +366,9 @@ mkPrimTcName built_in_syntax occ key tycon
   = mkWiredInName gHC_PRIM (mkTcOccFS occ) key (ATyCon tycon) built_in_syntax
 
 -----------------------------
--- | Given a Levity, applies TYPE to it. See Note [TYPE].
+-- | Given a RuntimeRep, applies TYPE to it. See Note [TYPE].
 tYPE :: Type -> Type
-tYPE lev = TyConApp tYPETyCon [lev]
+tYPE rr = TyConApp tYPETyCon [rr]
 
 {-
 ************************************************************************
@@ -375,16 +381,48 @@ tYPE lev = TyConApp tYPETyCon [lev]
 -- only used herein
 pcPrimTyCon :: Name -> [Role] -> PrimRep -> TyCon
 pcPrimTyCon name roles rep
-  = mkPrimTyCon name kind roles rep
+  = mkPrimTyCon name binders result_kind roles
   where
-    kind        = mkFunTys (map (const liftedTypeKind) roles) result_kind
-    result_kind = unliftedTypeKind
+    binders     = map (const (Anon liftedTypeKind)) roles
+    result_kind = tYPE rr
+
+    rr = case rep of
+      VoidRep       -> voidRepDataConTy
+      PtrRep        -> TyConApp ptrRepUnliftedDataConTyCon []
+      IntRep        -> intRepDataConTy
+      WordRep       -> wordRepDataConTy
+      Int64Rep      -> int64RepDataConTy
+      Word64Rep     -> word64RepDataConTy
+      AddrRep       -> addrRepDataConTy
+      FloatRep      -> floatRepDataConTy
+      DoubleRep     -> doubleRepDataConTy
+      VecRep n elem -> TyConApp vecRepDataConTyCon [n', elem']
+        where
+          n' = case n of
+            2  -> vec2DataConTy
+            4  -> vec4DataConTy
+            8  -> vec8DataConTy
+            16 -> vec16DataConTy
+            32 -> vec32DataConTy
+            64 -> vec64DataConTy
+            _  -> pprPanic "Disallowed VecCount" (ppr n)
+
+          elem' = case elem of
+            Int8ElemRep   -> int8ElemRepDataConTy
+            Int16ElemRep  -> int16ElemRepDataConTy
+            Int32ElemRep  -> int32ElemRepDataConTy
+            Int64ElemRep  -> int64ElemRepDataConTy
+            Word8ElemRep  -> word8ElemRepDataConTy
+            Word16ElemRep -> word16ElemRepDataConTy
+            Word32ElemRep -> word32ElemRepDataConTy
+            Word64ElemRep -> word64ElemRepDataConTy
+            FloatElemRep  -> floatElemRepDataConTy
+            DoubleElemRep -> doubleElemRepDataConTy
+
 
 pcPrimTyCon0 :: Name -> PrimRep -> TyCon
 pcPrimTyCon0 name rep
-  = mkPrimTyCon name result_kind [] rep
-  where
-    result_kind = unliftedTypeKind
+  = pcPrimTyCon name [] rep
 
 charPrimTy :: Type
 charPrimTy      = mkTyConTy charPrimTyCon
@@ -627,7 +665,7 @@ RealWorld; it's only used in the type system, to parameterise State#.
 -}
 
 realWorldTyCon :: TyCon
-realWorldTyCon = mkLiftedPrimTyCon realWorldTyConName liftedTypeKind [] PtrRep
+realWorldTyCon = mkLiftedPrimTyCon realWorldTyConName [] liftedTypeKind []
 realWorldTy :: Type
 realWorldTy          = mkTyConTy realWorldTyCon
 realWorldStatePrimTy :: Type
@@ -647,11 +685,12 @@ mkProxyPrimTy :: Type -> Type -> Type
 mkProxyPrimTy k ty = TyConApp proxyPrimTyCon [k, ty]
 
 proxyPrimTyCon :: TyCon
-proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName kind [Nominal,Nominal] VoidRep
-  where kind = ForAllTy (Named kv Specified) $
-               mkFunTy k unliftedTypeKind
-        kv   = kKiVar
-        k    = mkTyVarTy kv
+proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName binders res_kind [Nominal,Nominal]
+  where binders  = [ Named kv Specified
+                   , Anon k ]
+        res_kind = tYPE voidRepDataConTy
+        kv       = kKiVar
+        k        = mkTyVarTy kv
 
 
 {- *********************************************************************
@@ -663,10 +702,12 @@ proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName kind [Nominal,Nominal] VoidRep
 
 eqPrimTyCon :: TyCon  -- The representation type for equality predicates
                       -- See Note [The equality types story]
-eqPrimTyCon  = mkPrimTyCon eqPrimTyConName kind roles VoidRep
-  where kind = ForAllTy (Named kv1 Specified) $
-               ForAllTy (Named kv2 Specified) $
-               mkFunTys [k1, k2] unliftedTypeKind
+eqPrimTyCon  = mkPrimTyCon eqPrimTyConName binders res_kind roles
+  where binders = [ Named kv1 Specified
+                  , Named kv2 Specified
+                  , Anon k1
+                  , Anon k2 ]
+        res_kind = tYPE voidRepDataConTy
         [kv1, kv2] = mkTemplateTyVars [liftedTypeKind, liftedTypeKind]
         k1 = mkTyVarTy kv1
         k2 = mkTyVarTy kv2
@@ -676,11 +717,12 @@ eqPrimTyCon  = mkPrimTyCon eqPrimTyConName kind roles VoidRep
 -- this should only ever appear as the type of a covar. Its role is
 -- interpreted in coercionRole
 eqReprPrimTyCon :: TyCon   -- See Note [The equality types story]
-eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName kind
-                              roles VoidRep
-  where kind = ForAllTy (Named kv1 Specified) $
-               ForAllTy (Named kv2 Specified) $
-               mkFunTys [k1, k2] unliftedTypeKind
+eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName binders res_kind roles
+  where binders = [ Named kv1 Specified
+                  , Named kv2 Specified
+                  , Anon k1
+                  , Anon k2 ]
+        res_kind = tYPE voidRepDataConTy
         [kv1, kv2]    = mkTemplateTyVars [liftedTypeKind, liftedTypeKind]
         k1            = mkTyVarTy kv1
         k2            = mkTyVarTy kv2
@@ -690,12 +732,13 @@ eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName kind
 -- This is only used to make higher-order equalities. Nothing
 -- should ever actually have this type!
 eqPhantPrimTyCon :: TyCon
-eqPhantPrimTyCon = mkPrimTyCon eqPhantPrimTyConName kind
+eqPhantPrimTyCon = mkPrimTyCon eqPhantPrimTyConName binders res_kind
                                [Nominal, Nominal, Phantom, Phantom]
-                               VoidRep
-  where kind = ForAllTy (Named kv1 Specified) $
-               ForAllTy (Named kv2 Specified) $
-               mkFunTys [k1, k2] unliftedTypeKind
+  where binders = [ Named kv1 Specified
+                  , Named kv2 Specified
+                  , Anon k1
+                  , Anon k2 ]
+        res_kind = tYPE voidRepDataConTy
         [kv1, kv2]    = mkTemplateTyVars [liftedTypeKind, liftedTypeKind]
         k1            = mkTyVarTy kv1
         k2            = mkTyVarTy kv2
@@ -920,12 +963,13 @@ anyTy :: Type
 anyTy = mkTyConTy anyTyCon
 
 anyTyCon :: TyCon
-anyTyCon = mkFamilyTyCon anyTyConName kind [kKiVar] Nothing
+anyTyCon = mkFamilyTyCon anyTyConName binders res_kind [kKiVar] Nothing
                          (ClosedSynFamilyTyCon Nothing)
                          Nothing
                          NotInjective
   where
-    kind = ForAllTy (Named kKiVar Specified) (mkTyVarTy kKiVar)
+    binders  = [Named kKiVar Specified]
+    res_kind = mkTyVarTy kKiVar
 
 anyTypeOfKind :: Kind -> Type
 anyTypeOfKind kind = TyConApp anyTyCon [kind]
index b7bd186..6f0fc56 100644 (file)
@@ -88,11 +88,25 @@ module TysWiredIn (
 
         mkWiredInIdName,    -- used in MkId
 
-        -- * Levity
-        levityTy, levityTyCon, liftedDataCon, unliftedDataCon,
-        liftedPromDataCon, unliftedPromDataCon,
-        liftedDataConTy, unliftedDataConTy,
-        liftedDataConName, unliftedDataConName,
+        -- * RuntimeRep and friends
+        runtimeRepTyCon, vecCountTyCon, vecElemTyCon,
+
+        runtimeRepTy, ptrRepLiftedTy,
+
+        vecRepDataConTyCon, ptrRepUnliftedDataConTyCon,
+
+        voidRepDataConTy, intRepDataConTy,
+        wordRepDataConTy, int64RepDataConTy, word64RepDataConTy, addrRepDataConTy,
+        floatRepDataConTy, doubleRepDataConTy, unboxedTupleRepDataConTy,
+
+        vec2DataConTy, vec4DataConTy, vec8DataConTy, vec16DataConTy, vec32DataConTy,
+        vec64DataConTy,
+
+        int8ElemRepDataConTy, int16ElemRepDataConTy, int32ElemRepDataConTy,
+        int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy,
+        word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy,
+        doubleElemRepDataConTy
+
     ) where
 
 #include "HsVersions.h"
@@ -135,6 +149,15 @@ alpha_ty :: [Type]
 alpha_ty = [alphaTy]
 
 {-
+Note [Wiring in RuntimeRep]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The RuntimeRep type (and friends) in GHC.Types has a bunch of constructors,
+making it a pain to wire in. To ease the pain somewhat, we use lists of
+the different bits, like Uniques, Names, DataCons. These lists must be
+kept in sync with each other. The rule is this: use the order as declared
+in GHC.Types. All places where such lists exist should contain a reference
+to this Note, so a search for this Note's name should find all the lists.
+
 ************************************************************************
 *                                                                      *
 \subsection{Wired in type constructors}
@@ -178,7 +201,9 @@ wiredInTyCons = [ unitTyCon     -- Not treated like other tuples, because
               , coercibleTyCon
               , typeNatKindCon
               , typeSymbolKindCon
-              , levityTyCon
+              , runtimeRepTyCon
+              , vecCountTyCon
+              , vecElemTyCon
               , constraintKindTyCon
               , liftedTypeKindTyCon
               , starKindTyCon
@@ -264,10 +289,48 @@ liftedTypeKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Type")
 starKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "*") starKindTyConKey starKindTyCon
 unicodeStarKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "★") unicodeStarKindTyConKey unicodeStarKindTyCon
 
-levityTyConName, liftedDataConName, unliftedDataConName :: Name
-levityTyConName     = mkWiredInTyConName   UserSyntax gHC_TYPES (fsLit "Levity") levityTyConKey levityTyCon
-liftedDataConName   = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Lifted") liftedDataConKey liftedDataCon
-unliftedDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Unlifted") unliftedDataConKey unliftedDataCon
+runtimeRepTyConName, vecRepDataConName :: Name
+runtimeRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "RuntimeRep") runtimeRepTyConKey runtimeRepTyCon
+vecRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "VecRep") vecRepDataConKey vecRepDataCon
+
+-- See Note [Wiring in RuntimeRep]
+runtimeRepSimpleDataConNames :: [Name]
+runtimeRepSimpleDataConNames
+  = zipWith3Lazy mk_special_dc_name
+      [ fsLit "PtrRepLifted", fsLit "PtrRepUnlifted"
+      , fsLit "VoidRep", fsLit "IntRep"
+      , fsLit "WordRep", fsLit "Int64Rep", fsLit "Word64Rep"
+      , fsLit "AddrRep", fsLit "FloatRep", fsLit "DoubleRep"
+      , fsLit "UnboxedTupleRep" ]
+      runtimeRepSimpleDataConKeys
+      runtimeRepSimpleDataCons
+
+vecCountTyConName :: Name
+vecCountTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "VecCount") vecCountTyConKey vecCountTyCon
+
+-- See Note [Wiring in RuntimeRep]
+vecCountDataConNames :: [Name]
+vecCountDataConNames = zipWith3Lazy mk_special_dc_name
+                         [ fsLit "Vec2", fsLit "Vec4", fsLit "Vec8"
+                         , fsLit "Vec16", fsLit "Vec32", fsLit "Vec64" ]
+                         vecCountDataConKeys
+                         vecCountDataCons
+
+vecElemTyConName :: Name
+vecElemTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "VecElem") vecElemTyConKey vecElemTyCon
+
+-- See Note [Wiring in RuntimeRep]
+vecElemDataConNames :: [Name]
+vecElemDataConNames = zipWith3Lazy mk_special_dc_name
+                        [ fsLit "Int8ElemRep", fsLit "Int16ElemRep", fsLit "Int32ElemRep"
+                        , fsLit "Int64ElemRep", fsLit "Word8ElemRep", fsLit "Word16elemRep"
+                        , fsLit "Word32ElemRep", fsLit "Word64ElemRep"
+                        , fsLit "FloatElemRep", fsLit "DoubleElemRep" ]
+                        vecElemDataConKeys
+                        vecElemDataCons
+
+mk_special_dc_name :: FastString -> Unique -> DataCon -> Name
+mk_special_dc_name fs u dc = mkWiredInDataConName UserSyntax gHC_TYPES fs u dc
 
 parrTyConName, parrDataConName :: Name
 parrTyConName   = mkWiredInTyConName   BuiltInSyntax
@@ -304,7 +367,8 @@ pcNonRecDataTyCon = pcTyCon False NonRecursive
 pcTyCon :: Bool -> RecFlag -> Name -> Maybe CType -> [TyVar] -> [DataCon] -> TyCon
 pcTyCon is_enum is_rec name cType tyvars cons
   = mkAlgTyCon name
-                (mkFunTys (map tyVarKind tyvars) liftedTypeKind)
+                (map (mkAnonBinder . tyVarKind) tyvars)
+                liftedTypeKind
                 tyvars
                 (map (const Representational) tyvars)
                 cType
@@ -325,6 +389,7 @@ pcDataConWithFixity :: Bool      -- ^ declared infix?
                     -> TyCon
                     -> DataCon
 pcDataConWithFixity infx n = pcDataConWithFixity' infx n (incrUnique (nameUnique n))
+                                                  NoRRI
 -- The Name's unique is the first of two free uniques;
 -- the first is used for the datacon itself,
 -- the second is used for the "worker name"
@@ -332,12 +397,13 @@ pcDataConWithFixity infx n = pcDataConWithFixity' infx n (incrUnique (nameUnique
 -- To support this the mkPreludeDataConUnique function "allocates"
 -- one DataCon unique per pair of Ints.
 
-pcDataConWithFixity' :: Bool -> Name -> Unique -> [TyVar] -> [TyVar]
+pcDataConWithFixity' :: Bool -> Name -> Unique -> RuntimeRepInfo
+                     -> [TyVar] -> [TyVar]
                      -> [Type] -> TyCon -> DataCon
 -- The Name should be in the DataName name space; it's the name
 -- of the DataCon itself.
 
-pcDataConWithFixity' declared_infix dc_name wrk_key tyvars ex_tyvars arg_tys tycon
+pcDataConWithFixity' declared_infix dc_name wrk_key rri tyvars ex_tyvars arg_tys tycon
   = data_con
   where
     data_con = mkDataCon dc_name declared_infix prom_info
@@ -348,6 +414,7 @@ pcDataConWithFixity' declared_infix dc_name wrk_key tyvars ex_tyvars arg_tys tyc
                 []      -- No equality spec
                 []      -- No theta
                 arg_tys (mkTyConApp tycon (mkTyVarTys tyvars))
+                rri
                 tycon
                 []      -- No stupid theta
                 (mkDataConWorkId wrk_name data_con)
@@ -364,6 +431,12 @@ pcDataConWithFixity' declared_infix dc_name wrk_key tyvars ex_tyvars arg_tys tyc
 
     prom_info = mkPrelTyConRepName dc_name
 
+-- used for RuntimeRep and friends
+pcSpecialDataCon :: Name -> [Type] -> TyCon -> RuntimeRepInfo -> DataCon
+pcSpecialDataCon dc_name arg_tys tycon rri
+  = pcDataConWithFixity' False dc_name (incrUnique (nameUnique dc_name)) rri
+                         [] [] arg_tys tycon
+
 {-
 ************************************************************************
 *                                                                      *
@@ -387,7 +460,7 @@ constraintKindTyCon = pcTyCon False NonRecursive constraintKindTyConName
                               Nothing [] []
 
 liftedTypeKind, constraintKind :: Kind
-liftedTypeKind   = tYPE liftedDataConTy
+liftedTypeKind   = tYPE ptrRepLiftedTy
 constraintKind   = mkTyConApp constraintKindTyCon []
 
 
@@ -536,34 +609,38 @@ unboxedTupleArr = listArray (0,mAX_TUPLE_SIZE) [mk_tuple Unboxed i | i <- [0..mA
 mk_tuple :: Boxity -> Int -> (TyCon,DataCon)
 mk_tuple boxity arity = (tycon, tuple_con)
   where
-        tycon   = mkTupleTyCon tc_name tc_kind tc_arity tyvars tuple_con
+        tycon   = mkTupleTyCon tc_name tc_binders tc_res_kind tc_arity tyvars tuple_con
                                tup_sort flavour
 
-        (tup_sort, modu, tc_kind, tc_arity, tyvars, tyvar_tys, flavour)
+        (tup_sort, modu, tc_binders, tc_res_kind, tc_arity, tyvars, tyvar_tys, flavour)
           = case boxity of
           Boxed ->
             let boxed_tyvars = take arity alphaTyVars in
             ( BoxedTuple
             , gHC_TUPLE
-            , mkFunTys (nOfThem arity liftedTypeKind) liftedTypeKind
+            , nOfThem arity (mkAnonBinder liftedTypeKind)
+            , liftedTypeKind
             , arity
             , boxed_tyvars
             , mkTyVarTys boxed_tyvars
             , VanillaAlgTyCon (mkPrelTyConRepName tc_name)
             )
-            -- See Note [Unboxed tuple levity vars] in TyCon
+            -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
           Unboxed ->
-            let all_tvs = mkTemplateTyVars (replicate arity levityTy ++
+            let all_tvs = mkTemplateTyVars (replicate arity runtimeRepTy ++
                                             map (tYPE . mkTyVarTy) (take arity all_tvs))
                    -- NB: This must be one call to mkTemplateTyVars, to make
                    -- sure that all the uniques are different
-                (lev_tvs, open_tvs) = splitAt arity all_tvs
+                (rr_tvs, open_tvs) = splitAt arity all_tvs
+                res_rep | arity == 0 = voidRepDataConTy
+                              -- See Note [Nullary unboxed tuple] in Type
+                        | otherwise  = unboxedTupleRepDataConTy
             in
             ( UnboxedTuple
             , gHC_PRIM
-            , mkSpecForAllTys lev_tvs $
-              mkFunTys (map tyVarKind open_tvs) $
-              unliftedTypeKind
+            , map (mkNamedBinder Specified) rr_tvs ++
+              map (mkAnonBinder . tyVarKind) open_tvs
+            , tYPE res_rep
             , arity * 2
             , all_tvs
             , mkTyVarTys open_tvs
@@ -616,13 +693,16 @@ heqSCSelId, coercibleSCSelId :: Id
 (heqTyCon, heqClass, heqDataCon, heqSCSelId)
   = (tycon, klass, datacon, sc_sel_id)
   where
-    tycon     = mkClassTyCon heqTyConName kind tvs roles
+    tycon     = mkClassTyCon heqTyConName binders tvs roles
                              rhs klass NonRecursive
                              (mkPrelTyConRepName heqTyConName)
     klass     = mkClass tvs [] [sc_pred] [sc_sel_id] [] [] (mkAnd []) tycon
     datacon   = pcDataCon heqDataConName tvs [sc_pred] tycon
 
-    kind      = mkSpecForAllTys [kv1, kv2] $ mkFunTys [k1, k2] constraintKind
+    binders   = [ mkNamedBinder Specified kv1
+                , mkNamedBinder Specified kv2
+                , mkAnonBinder k1
+                , mkAnonBinder k2 ]
     kv1:kv2:_ = drop 9 alphaTyVars -- gets "j" and "k"
     k1        = mkTyVarTy kv1
     k2        = mkTyVarTy kv2
@@ -637,13 +717,15 @@ heqSCSelId, coercibleSCSelId :: Id
 (coercibleTyCon, coercibleClass, coercibleDataCon, coercibleSCSelId)
   = (tycon, klass, datacon, sc_sel_id)
   where
-    tycon     = mkClassTyCon coercibleTyConName kind tvs roles
+    tycon     = mkClassTyCon coercibleTyConName binders tvs roles
                              rhs klass NonRecursive
                              (mkPrelTyConRepName coercibleTyConName)
     klass     = mkClass tvs [] [sc_pred] [sc_sel_id] [] [] (mkAnd []) tycon
     datacon   = pcDataCon coercibleDataConName tvs [sc_pred] tycon
 
-    kind      = mkSpecForAllTys [kKiVar] $ mkFunTys [k, k] constraintKind
+    binders   = [ mkNamedBinder Specified kKiVar
+                , mkAnonBinder k
+                , mkAnonBinder k ]
     k         = mkTyVarTy kKiVar
     [av,bv]   = mkTemplateTyVars [k, k]
     tvs       = [kKiVar, av, bv]
@@ -656,48 +738,125 @@ heqSCSelId, coercibleSCSelId :: Id
 
 {- *********************************************************************
 *                                                                      *
-                Kinds and levity
+                Kinds and RuntimeRep
 *                                                                      *
 ********************************************************************* -}
 
 -- For information about the usage of the following type, see Note [TYPE]
 -- in module TysPrim
-levityTy :: Type
-levityTy = mkTyConTy levityTyCon
-
-levityTyCon :: TyCon
-levityTyCon = pcTyCon True NonRecursive levityTyConName
-                      Nothing [] [liftedDataCon, unliftedDataCon]
-
-liftedDataCon, unliftedDataCon :: DataCon
-liftedDataCon   = pcDataCon liftedDataConName [] [] levityTyCon
-unliftedDataCon = pcDataCon unliftedDataConName [] [] levityTyCon
-
-liftedPromDataCon, unliftedPromDataCon :: TyCon
-liftedPromDataCon   = promoteDataCon liftedDataCon
-unliftedPromDataCon = promoteDataCon unliftedDataCon
-
-liftedDataConTy, unliftedDataConTy :: Type
-liftedDataConTy   = mkTyConTy liftedPromDataCon
-unliftedDataConTy = mkTyConTy unliftedPromDataCon
+runtimeRepTy :: Type
+runtimeRepTy = mkTyConTy runtimeRepTyCon
 
 liftedTypeKindTyCon, starKindTyCon, unicodeStarKindTyCon :: TyCon
 
    -- See Note [TYPE] in TysPrim
 liftedTypeKindTyCon   = mkSynonymTyCon liftedTypeKindTyConName
-                                       liftedTypeKind
+                                       [] liftedTypeKind
                                        [] []
-                                       (tYPE liftedDataConTy)
+                                       (tYPE ptrRepLiftedTy)
 
 starKindTyCon         = mkSynonymTyCon starKindTyConName
-                                       liftedTypeKind
+                                       [] liftedTypeKind
                                        [] []
-                                       (tYPE liftedDataConTy)
+                                       (tYPE ptrRepLiftedTy)
 
 unicodeStarKindTyCon  = mkSynonymTyCon unicodeStarKindTyConName
-                                       liftedTypeKind
+                                       [] liftedTypeKind
                                        [] []
-                                       (tYPE liftedDataConTy)
+                                       (tYPE ptrRepLiftedTy)
+
+runtimeRepTyCon :: TyCon
+runtimeRepTyCon = pcNonRecDataTyCon runtimeRepTyConName Nothing []
+                          (vecRepDataCon : runtimeRepSimpleDataCons)
+
+vecRepDataCon :: DataCon
+vecRepDataCon = pcSpecialDataCon vecRepDataConName [ mkTyConTy vecCountTyCon
+                                                   , mkTyConTy vecElemTyCon ]
+                                 runtimeRepTyCon
+                                 (RuntimeRep prim_rep_fun)
+  where
+    prim_rep_fun [count, elem]
+      | VecCount n <- tyConRuntimeRepInfo (tyConAppTyCon count)
+      , VecElem  e <- tyConRuntimeRepInfo (tyConAppTyCon elem)
+      = VecRep n e
+    prim_rep_fun args
+      = pprPanic "vecRepDataCon" (ppr args)
+
+vecRepDataConTyCon :: TyCon
+vecRepDataConTyCon = promoteDataCon vecRepDataCon
+
+ptrRepUnliftedDataConTyCon :: TyCon
+ptrRepUnliftedDataConTyCon = promoteDataCon ptrRepUnliftedDataCon
+
+-- See Note [Wiring in RuntimeRep]
+runtimeRepSimpleDataCons :: [DataCon]
+ptrRepLiftedDataCon, ptrRepUnliftedDataCon :: DataCon
+runtimeRepSimpleDataCons@(ptrRepLiftedDataCon : ptrRepUnliftedDataCon : _)
+  = zipWithLazy mk_runtime_rep_dc
+    [ PtrRep, PtrRep, VoidRep, IntRep, WordRep, Int64Rep
+    , Word64Rep, AddrRep, FloatRep, DoubleRep
+    , panic "unboxed tuple PrimRep" ]
+    runtimeRepSimpleDataConNames
+  where
+    mk_runtime_rep_dc primrep name
+      = pcSpecialDataCon name [] runtimeRepTyCon (RuntimeRep (\_ -> primrep))
+
+-- See Note [Wiring in RuntimeRep]
+voidRepDataConTy, intRepDataConTy, wordRepDataConTy, int64RepDataConTy,
+  word64RepDataConTy, addrRepDataConTy, floatRepDataConTy, doubleRepDataConTy,
+  unboxedTupleRepDataConTy :: Type
+[_, _, voidRepDataConTy, intRepDataConTy, wordRepDataConTy, int64RepDataConTy,
+   word64RepDataConTy, addrRepDataConTy, floatRepDataConTy, doubleRepDataConTy,
+   unboxedTupleRepDataConTy] = map (mkTyConTy . promoteDataCon)
+                                   runtimeRepSimpleDataCons
+
+vecCountTyCon :: TyCon
+vecCountTyCon = pcNonRecDataTyCon vecCountTyConName Nothing []
+                        vecCountDataCons
+
+-- See Note [Wiring in RuntimeRep]
+vecCountDataCons :: [DataCon]
+vecCountDataCons = zipWithLazy mk_vec_count_dc
+                     [ 2, 4, 8, 16, 32, 64 ]
+                     vecCountDataConNames
+  where
+    mk_vec_count_dc n name
+      = pcSpecialDataCon name [] vecCountTyCon (VecCount n)
+
+-- See Note [Wiring in RuntimeRep]
+vec2DataConTy, vec4DataConTy, vec8DataConTy, vec16DataConTy, vec32DataConTy,
+  vec64DataConTy :: Type
+[vec2DataConTy, vec4DataConTy, vec8DataConTy, vec16DataConTy, vec32DataConTy,
+  vec64DataConTy] = map (mkTyConTy . promoteDataCon) vecCountDataCons
+
+vecElemTyCon :: TyCon
+vecElemTyCon = pcNonRecDataTyCon vecElemTyConName Nothing [] vecElemDataCons
+
+-- See Note [Wiring in RuntimeRep]
+vecElemDataCons :: [DataCon]
+vecElemDataCons = zipWithLazy mk_vec_elem_dc
+                    [ Int8ElemRep, Int16ElemRep, Int32ElemRep, Int64ElemRep
+                    , Word8ElemRep, Word16ElemRep, Word32ElemRep, Word64ElemRep
+                    , FloatElemRep, DoubleElemRep ]
+                    vecElemDataConNames
+  where
+    mk_vec_elem_dc elem name
+      = pcSpecialDataCon name [] vecElemTyCon (VecElem elem)
+
+-- See Note [Wiring in RuntimeRep]
+int8ElemRepDataConTy, int16ElemRepDataConTy, int32ElemRepDataConTy,
+  int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy,
+  word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy,
+  doubleElemRepDataConTy :: Type
+[int8ElemRepDataConTy, int16ElemRepDataConTy, int32ElemRepDataConTy,
+  int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy,
+  word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy,
+  doubleElemRepDataConTy] = map (mkTyConTy . promoteDataCon)
+                                vecElemDataCons
+
+-- The type ('PtrRepLifted)
+ptrRepLiftedTy :: Type
+ptrRepLiftedTy = mkTyConTy $ promoteDataCon ptrRepLiftedDataCon
 
 {- *********************************************************************
 *                                                                      *
@@ -943,13 +1102,13 @@ done by enumeration\srcloc{lib/prelude/InTup?.hs}.
 -}
 
 -- | Make a tuple type. The list of types should /not/ include any
--- levity specifications.
+-- RuntimeRep specifications.
 mkTupleTy :: Boxity -> [Type] -> Type
 -- Special case for *boxed* 1-tuples, which are represented by the type itself
 mkTupleTy Boxed   [ty] = ty
 mkTupleTy Boxed   tys  = mkTyConApp (tupleTyCon Boxed (length tys)) tys
 mkTupleTy Unboxed tys  = mkTyConApp (tupleTyCon Unboxed (length tys))
-                                        (map (getLevity "mkTupleTy") tys ++ tys)
+                                        (map (getRuntimeRep "mkTupleTy") tys ++ tys)
 
 -- | Build the type of a small tuple that holds the specified type of thing
 mkBoxedTupleTy :: [Type] -> Type
index f7ae635..7216d26 100644 (file)
@@ -1,6 +1,6 @@
 module TysWiredIn where
 
-import TyCon
+import {-# SOURCE #-} TyCon      ( TyCon )
 import {-# SOURCE #-} TyCoRep    (Type, Kind)
 
 
@@ -8,6 +8,22 @@ listTyCon :: TyCon
 typeNatKind, typeSymbolKind :: Type
 mkBoxedTupleTy :: [Type] -> Type
 
-levityTy, unliftedDataConTy :: Type
-
 liftedTypeKind :: Kind
+constraintKind :: Kind
+
+runtimeRepTyCon, vecCountTyCon, vecElemTyCon :: TyCon
+runtimeRepTy :: Type
+
+ptrRepUnliftedDataConTyCon, vecRepDataConTyCon :: TyCon
+
+voidRepDataConTy, intRepDataConTy,
+  wordRepDataConTy, int64RepDataConTy, word64RepDataConTy, addrRepDataConTy,
+  floatRepDataConTy, doubleRepDataConTy, unboxedTupleRepDataConTy :: Type
+
+vec2DataConTy, vec4DataConTy, vec8DataConTy, vec16DataConTy, vec32DataConTy,
+  vec64DataConTy :: Type
+
+int8ElemRepDataConTy, int16ElemRepDataConTy, int32ElemRepDataConTy,
+  int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy,
+  word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy,
+  doubleElemRepDataConTy :: Type
index b3da5ef..498687e 100644 (file)
@@ -14,6 +14,8 @@ module Inst (
        instCall, instDFunType, instStupidTheta,
        newWanted, newWanteds,
 
+       tcInstBinders, tcInstBindersX,
+
        newOverloadedLit, mkOverLit,
 
        newClsInst,
@@ -30,7 +32,7 @@ module Inst (
 #include "HsVersions.h"
 
 import {-# SOURCE #-}   TcExpr( tcPolyExpr, tcSyntaxOp )
-import {-# SOURCE #-}   TcUnify( unifyType, noThing )
+import {-# SOURCE #-}   TcUnify( unifyType, unifyKind, noThing )
 
 import FastString
 import HsSyn
@@ -39,8 +41,7 @@ import TcRnMonad
 import TcEnv
 import TcEvidence
 import InstEnv
-import DataCon     ( dataConWrapId )
-import TysWiredIn  ( heqDataCon )
+import TysWiredIn  ( heqDataCon, coercibleDataCon )
 import CoreSyn     ( isOrphan )
 import FunDeps
 import TcMType
@@ -51,7 +52,9 @@ import Class( Class )
 import MkId( mkDictFunId )
 import Id
 import Name
-import Var      ( EvVar )
+import Var      ( EvVar, mkTyVar )
+import DataCon
+import TyCon
 import VarEnv
 import PrelNames
 import SrcLoc
@@ -329,6 +332,122 @@ instStupidTheta orig theta
 {-
 ************************************************************************
 *                                                                      *
+         Instantiating Kinds
+*                                                                      *
+************************************************************************
+
+-}
+
+---------------------------
+-- | This is used to instantiate binders when type-checking *types* only.
+-- See also Note [Bidirectional type checking]
+tcInstBinders :: [TyBinder] -> TcM (TCvSubst, [TcType])
+tcInstBinders = tcInstBindersX emptyTCvSubst Nothing
+
+-- | This is used to instantiate binders when type-checking *types* only.
+-- The @VarEnv Kind@ gives some known instantiations.
+-- See also Note [Bidirectional type checking]
+tcInstBindersX :: TCvSubst -> Maybe (VarEnv Kind)
+               -> [TyBinder] -> TcM (TCvSubst, [TcType])
+tcInstBindersX subst mb_kind_info bndrs
+  = do { (subst, args) <- mapAccumLM (tcInstBinderX mb_kind_info) subst bndrs
+       ; traceTc "instantiating tybinders:"
+           (vcat $ zipWith (\bndr arg -> ppr bndr <+> text ":=" <+> ppr arg)
+                           bndrs args)
+       ; return (subst, args) }
+
+-- | Used only in *types*
+tcInstBinderX :: Maybe (VarEnv Kind)
+              -> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
+tcInstBinderX mb_kind_info subst binder
+  | Just tv <- binderVar_maybe binder
+  = case lookup_tv tv of
+      Just ki -> return (extendTvSubstAndInScope subst tv ki, ki)
+      Nothing -> do { (subst', tv') <- newMetaTyVarX subst tv
+                    ; return (subst', mkTyVarTy tv') }
+
+     -- This is the *only* constraint currently handled in types.
+  | Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty
+  = do { let origin = TypeEqOrigin { uo_actual   = k1
+                                   , uo_expected = mkCheckExpType k2
+                                   , uo_thing    = Nothing }
+       ; co <- case role of
+                 Nominal          -> unifyKind noThing k1 k2
+                 Representational -> emitWantedEq origin KindLevel role k1 k2
+                 Phantom          -> pprPanic "tcInstBinderX Phantom" (ppr binder)
+       ; arg' <- mk co k1 k2
+       ; return (subst, arg') }
+
+  | isPredTy substed_ty
+  = do { let (env, tidy_ty) = tidyOpenType emptyTidyEnv substed_ty
+       ; addErrTcM (env, text "Illegal constraint in a type:" <+> ppr tidy_ty)
+
+         -- just invent a new variable so that we can continue
+       ; u <- newUnique
+       ; let name = mkSysTvName u (fsLit "dict")
+       ; return (subst, mkTyVarTy $ mkTyVar name substed_ty) }
+
+
+  | otherwise
+  = do { ty <- newFlexiTyVarTy substed_ty
+       ; return (subst, ty) }
+
+  where
+    substed_ty = substTy subst (binderType binder)
+
+    lookup_tv tv = do { env <- mb_kind_info   -- `Maybe` monad
+                      ; lookupVarEnv env tv }
+
+      -- handle boxed equality constraints, because it's so easy
+    get_pred_tys_maybe ty
+      | Just (r, k1, k2) <- getEqPredTys_maybe ty
+      = Just (\co _ _ -> return $ mkCoercionTy co, r, k1, k2)
+      | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
+      = if | tc `hasKey` heqTyConKey
+             -> Just (mkHEqBoxTy, Nominal, k1, k2)
+           | otherwise
+             -> Nothing
+      | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
+      = if | tc `hasKey` eqTyConKey
+             -> Just (mkEqBoxTy, Nominal, k1, k2)
+           | tc `hasKey` coercibleTyConKey
+             -> Just (mkCoercibleBoxTy, Representational, k1, k2)
+           | otherwise
+             -> Nothing
+      | otherwise
+      = Nothing
+
+-------------------------------
+-- | This takes @a ~# b@ and returns @a ~~ b@.
+mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
+-- monadic just for convenience with mkEqBoxTy
+mkHEqBoxTy co ty1 ty2
+  = return $
+    mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
+  where k1 = typeKind ty1
+        k2 = typeKind ty2
+
+-- | This takes @a ~# b@ and returns @a ~ b@.
+mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
+mkEqBoxTy co ty1 ty2
+  = do { eq_tc <- tcLookupTyCon eqTyConName
+       ; let [datacon] = tyConDataCons eq_tc
+       ; hetero <- mkHEqBoxTy co ty1 ty2
+       ; return $ mkTyConApp (promoteDataCon datacon) [k, ty1, ty2, hetero] }
+  where k = typeKind ty1
+
+-- | This takes @a ~R# b@ and returns @Coercible a b@.
+mkCoercibleBoxTy :: TcCoercion -> Type -> Type -> TcM Type
+-- monadic just for convenience with mkEqBoxTy
+mkCoercibleBoxTy co ty1 ty2
+  = do { return $
+         mkTyConApp (promoteDataCon coercibleDataCon)
+                    [k, ty1, ty2, mkCoercionTy co] }
+  where k = typeKind ty1
+
+{-
+************************************************************************
+*                                                                      *
                 Literals
 *                                                                      *
 ************************************************************************
index 43f933b..495a442 100644 (file)
@@ -963,7 +963,7 @@ recoveryCode binder_names sig_fn
       = mkLocalId name forall_a_a
 
 forall_a_a :: TcType
-forall_a_a = mkSpecForAllTys [levity1TyVar, openAlphaTyVar] openAlphaTy
+forall_a_a = mkSpecForAllTys [runtimeRep1TyVar, openAlphaTyVar] openAlphaTy
 
 {- *********************************************************************
 *                                                                      *
index 75996f8..2da3153 100644 (file)
@@ -1134,7 +1134,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
 
       -- the following makes a better distinction between "kind" and "type"
       -- in error messages
-    (bndrs, _) = splitPiTys (tyConKind tc)
+    bndrs      = tyConBinders tc
     kind_loc   = toKindLoc loc
     is_kinds   = map isNamedBinder bndrs
     new_locs | Just KindLevel <- ctLocTypeOrKind_maybe loc
@@ -1962,10 +1962,8 @@ unify_derived loc role    orig_ty1 orig_ty2
                 Nothing   -> bale_out }
     go _ _ = bale_out
 
-     -- no point in having *boxed* deriveds.
     bale_out = emitNewDerivedEq loc role orig_ty1 orig_ty2
 
 maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
 maybeSym IsSwapped  co = mkTcSymCo co
 maybeSym NotSwapped co = co
-
index 56772f2..c2b344d 100644 (file)
@@ -934,7 +934,7 @@ inferConstraints main_cls cls_tys inst_ty rep_tc rep_tc_args
                  ++ sc_constraints
                  ++ arg_constraints) }
   where
-    (tc_binders, _) = splitPiTys (tyConKind rep_tc)
+    tc_binders = tyConBinders rep_tc
     choose_level bndr
       | isNamedBinder bndr = KindLevel
       | otherwise          = TypeLevel
index 2140a79..daae202 100644 (file)
@@ -29,8 +29,8 @@ import DataCon
 import TcEvidence
 import Name
 import RdrName ( lookupGRE_Name, GlobalRdrEnv, mkRdrUnqual )
-import PrelNames ( typeableClassName, hasKey
-                 , liftedDataConKey, unliftedDataConKey )
+import PrelNames ( typeableClassName, hasKey, ptrRepLiftedDataConKey
+                 , ptrRepUnliftedDataConKey )
 import Id
 import Var
 import VarSet
@@ -1366,12 +1366,22 @@ misMatchMsg ct oriented ty1 ty2
   | Just NotSwapped <- oriented
   = misMatchMsg ct (Just IsSwapped) ty2 ty1
 
+  -- These next two cases are when we're about to report, e.g., that
+  -- 'PtrRepLifted doesn't match 'VoidRep. Much better just to say
+  -- lifted vs. unlifted
+  | Just (tc1, []) <- splitTyConApp_maybe ty1
+  , tc1 `hasKey` ptrRepLiftedDataConKey
+  = lifted_vs_unlifted
+
+  | Just (tc2, []) <- splitTyConApp_maybe ty2
+  , tc2 `hasKey` ptrRepLiftedDataConKey
+  = lifted_vs_unlifted
+
   | Just (tc1, []) <- splitTyConApp_maybe ty1
   , Just (tc2, []) <- splitTyConApp_maybe ty2
-  , (tc1 `hasKey` liftedDataConKey && tc2 `hasKey` unliftedDataConKey) ||
-    (tc2 `hasKey` liftedDataConKey && tc1 `hasKey` unliftedDataConKey)
-  = addArising orig $
-    text "Couldn't match a lifted type with an unlifted type"
+  ,    (tc1 `hasKey` ptrRepLiftedDataConKey && tc2 `hasKey` ptrRepUnliftedDataConKey)
+    || (tc1 `hasKey` ptrRepUnliftedDataConKey && tc2 `hasKey` ptrRepLiftedDataConKey)
+  = lifted_vs_unlifted
 
   | otherwise  -- So now we have Nothing or (Just IsSwapped)
                -- For some reason we treat Nothing like IsSwapped
@@ -1406,6 +1416,10 @@ misMatchMsg ct oriented ty1 ty2
                     | null s2   = s1
                     | otherwise = s1 ++ (' ' : s2)
 
+    lifted_vs_unlifted
+      = addArising orig $
+        text "Couldn't match a lifted type with an unlifted type"
+
 mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
                     -> (Bool, Maybe SwapFlag, SDoc)
 -- NotSwapped means (actual, expected), IsSwapped is the reverse
index d54fbc7..6d5fe09 100644 (file)
@@ -361,7 +361,7 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
        ; arg2'  <- tcArg op arg2 arg2_sigma 2
 
        -- Make sure that the argument type has kind '*'
-       --   ($) :: forall (v:Levity) (a:*) (b:TYPE v). (a->b) -> a -> b
+       --   ($) :: forall (r:RuntimeRep) (a:*) (b:TYPE r). (a->b) -> a -> b
        -- Eg we do not want to allow  (D#  $  4.0#)   Trac #5570
        --    (which gives a seg fault)
        --
@@ -378,7 +378,7 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
 
        ; op_id  <- tcLookupId op_name
        ; res_ty <- readExpType res_ty
-       ; let op' = L loc (HsWrap (mkWpTyApps [ getLevity "tcExpr ($)" res_ty
+       ; let op' = L loc (HsWrap (mkWpTyApps [ getRuntimeRep "tcExpr ($)" res_ty
                                              , arg2_sigma
                                              , res_ty])
                                  (HsVar (L lv op_id)))
@@ -443,9 +443,9 @@ tcExpr expr@(ExplicitTuple tup_args boxity) res_ty
              tup_tc = tupleTyCon boxity arity
        ; res_ty <- expTypeToType res_ty
        ; (coi, arg_tys) <- matchExpectedTyConApp tup_tc res_ty
-                           -- Unboxed tuples have levity vars, which we
+                           -- Unboxed tuples have RuntimeRep vars, which we
                            -- don't care about here
-                           -- See Note [Unboxed tuple levity vars] in TyCon
+                           -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
        ; let arg_tys' = case boxity of Unboxed -> drop arity arg_tys
                                        Boxed   -> arg_tys
        ; tup_args1 <- tcTupArgs tup_args arg_tys'
@@ -1663,8 +1663,8 @@ tcSeq loc fun_name args res_ty
         ; (arg1, arg2, arg2_exp_ty) <- case args1 of
             [ty_arg_expr2, term_arg1, term_arg2]
               | Just hs_ty_arg2 <- isLHsTypeExpr_maybe ty_arg_expr2
-              -> do { lev_ty <- newFlexiTyVarTy levityTy
-                    ; ty_arg2 <- tcHsTypeApp hs_ty_arg2 (tYPE lev_ty)
+              -> do { rr_ty <- newFlexiTyVarTy runtimeRepTy
+                    ; ty_arg2 <- tcHsTypeApp hs_ty_arg2 (tYPE rr_ty)
                                    -- see Note [Typing rule for seq]
                     ; _ <- tcSubTypeDS GenSigCtxt noThing ty_arg2 res_ty
                     ; return (term_arg1, term_arg2, mkCheckExpType ty_arg2) }
index 66fe38a..d7d23a2 100644 (file)
@@ -9,7 +9,7 @@ This module is an extension of @HsSyn@ syntax, for use in the type
 checker.
 -}
 
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, TupleSections #-}
 
 module TcHsSyn (
         mkHsConApp, mkHsDictLet, mkHsApp,
@@ -29,7 +29,7 @@ module TcHsSyn (
         zonkTopBndrs, zonkTyBndrsX,
         emptyZonkEnv, mkEmptyZonkEnv,
         zonkTcTypeToType, zonkTcTypeToTypes, zonkTyVarOcc,
-        zonkCoToCo
+        zonkCoToCo, zonkTcKindToKind
   ) where
 
 #include "HsVersions.h"
@@ -44,6 +44,7 @@ import TcEvidence
 import TysPrim
 import TysWiredIn
 import Type
+import TyCoRep  ( TyBinder(..) )
 import Coercion
 import ConLike
 import DataCon
@@ -328,6 +329,15 @@ zonkTyBndrX env tv
        ; let tv' = mkTyVar (tyVarName tv) ki
        ; return (extendTyZonkEnv1 env tv', tv') }
 
+zonkTyBinders :: ZonkEnv -> [TcTyBinder] -> TcM (ZonkEnv, [TyBinder])
+zonkTyBinders = mapAccumLM zonkTyBinder
+
+zonkTyBinder :: ZonkEnv -> TcTyBinder -> TcM (ZonkEnv, TyBinder)
+zonkTyBinder env (Anon ty) = (env, ) <$> (Anon <$> zonkTcTypeToType env ty)
+zonkTyBinder env (Named tv vis)
+  = do { (env', tv') <- zonkTyBndrX env tv
+       ; return (env', Named tv' vis) }
+
 zonkTopExpr :: HsExpr TcId -> TcM (HsExpr Id)
 zonkTopExpr e = zonkExpr emptyZonkEnv e
 
@@ -1582,6 +1592,14 @@ zonkTcTypeToType = mapType zonk_tycomapper
 zonkTcTypeToTypes :: ZonkEnv -> [TcType] -> TcM [Type]
 zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
 
+-- | Used during kind-checking in TcTyClsDecls, where it's more convenient
+-- to keep the binders and result kind separate.
+zonkTcKindToKind :: [TcTyBinder] -> TcKind -> TcM ([TyBinder], Kind)
+zonkTcKindToKind binders res_kind
+  = do { (env, binders') <- zonkTyBinders emptyZonkEnv binders
+       ; res_kind' <- zonkTcTypeToType env res_kind
+       ; return (binders', res_kind') }
+
 zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion
 zonkCoToCo = mapCoercion zonk_tycomapper
 
@@ -1604,7 +1622,7 @@ zonkTypeZapping :: UnboundTyVarZonker
 -- It zaps unbound type variables to (), or some other arbitrary type
 -- Works on both types and kinds
 zonkTypeZapping tv
-  = do { let ty | isLevityVar tv = liftedDataConTy
-                | otherwise      = anyTypeOfKind (tyVarKind tv)
+  = do { let ty | isRuntimeRepVar tv = ptrRepLiftedTy
+                | otherwise          = anyTypeOfKind (tyVarKind tv)
        ; writeMetaTyVar tv ty
        ; return ty }
index c7b1470..5b0d9b9 100644 (file)
@@ -54,6 +54,7 @@ import TcUnify
 import TcIface
 import TcSimplify ( solveEqualities )
 import TcType
+import Inst   ( tcInstBinders, tcInstBindersX )
 import Type
 import Kind
 import RdrName( lookupLocalRdrOcc )
@@ -185,8 +186,8 @@ tcHsSigType ctxt sig_ty
     do { kind <- case expectedKindInCtxt ctxt of
                     AnythingKind -> newMetaKindVar
                     TheKind k    -> return k
-                    OpenKind     -> do { lev <- newFlexiTyVarTy levityTy
-                                       ; return $ tYPE lev }
+                    OpenKind     -> do { rr <- newFlexiTyVarTy runtimeRepTy
+                                       ; return $ tYPE rr }
               -- The kind is checked by checkValidType, and isn't necessarily
               -- of kind * in a Template Haskell quote eg [t| Maybe |]
 
@@ -459,10 +460,10 @@ tc_lhs_type mode (L span ty) exp_kind
 ------------------------------------------
 tc_fun_type :: TcTyMode -> LHsType Name -> LHsType Name -> TcKind -> TcM TcType
 tc_fun_type mode ty1 ty2 exp_kind
-  = do { arg_lev <- newFlexiTyVarTy levityTy
-       ; res_lev <- newFlexiTyVarTy levityTy
-       ; ty1' <- tc_lhs_type mode ty1 (tYPE arg_lev)
-       ; ty2' <- tc_lhs_type mode ty2 (tYPE res_lev)
+  = do { arg_rr <- newFlexiTyVarTy runtimeRepTy
+       ; res_rr <- newFlexiTyVarTy runtimeRepTy
+       ; ty1' <- tc_lhs_type mode ty1 (tYPE arg_rr)
+       ; ty2' <- tc_lhs_type mode ty2 (tYPE res_rr)
        ; checkExpectedKind (mkFunTy ty1' ty2') liftedTypeKind exp_kind }
 
 ------------------------------------------
@@ -657,8 +658,8 @@ tc_tuple :: TcTyMode -> TupleSort -> [LHsType Name] -> TcKind -> TcM TcType
 tc_tuple mode tup_sort tys exp_kind
   = do { arg_kinds <- case tup_sort of
            BoxedTuple      -> return (nOfThem arity liftedTypeKind)
-           UnboxedTuple    -> do { levs <- newFlexiTyVarTys arity levityTy
-                                 ; return $ map tYPE levs }
+           UnboxedTuple    -> do { rrs <- newFlexiTyVarTys arity runtimeRepTy
+                                 ; return $ map tYPE rrs }
            ConstraintTuple -> return (nOfThem arity constraintKind)
        ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
        ; finish_tuple tup_sort tau_tys arg_kinds exp_kind }
@@ -673,8 +674,8 @@ finish_tuple :: TupleSort
 finish_tuple tup_sort tau_tys tau_kinds exp_kind
   = do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
        ; let arg_tys  = case tup_sort of
-                   -- See also Note [Unboxed tuple levity vars] in TyCon
-                 UnboxedTuple    -> map (getLevityFromKind "finish_tuple") tau_kinds
+                   -- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
+                 UnboxedTuple    -> map (getRuntimeRepFromKind "finish_tuple") tau_kinds
                                     ++ tau_tys
                  BoxedTuple      -> tau_tys
                  ConstraintTuple -> tau_tys
@@ -691,7 +692,7 @@ finish_tuple tup_sort tau_tys tau_kinds exp_kind
   where
     arity = length tau_tys
     res_kind = case tup_sort of
-                 UnboxedTuple    -> unliftedTypeKind
+                 UnboxedTuple    -> tYPE unboxedTupleRepDataConTy
                  BoxedTuple      -> liftedTypeKind
                  ConstraintTuple -> constraintKind
 
@@ -712,19 +713,21 @@ bigConstraintTuple arity
 -- the visible ones.
 tcInferArgs :: Outputable fun
             => fun                      -- ^ the function
-            -> TcKind                   -- ^ function kind (zonked)
+            -> [TyBinder]               -- ^ function kind's binders
             -> Maybe (VarEnv Kind)      -- ^ possibly, kind info (see above)
             -> [LHsType Name]           -- ^ args
-            -> TcM (TcKind, [TcType], [LHsType Name], Int)
-               -- ^ (result kind, typechecked args, untypechecked args, n)
-tcInferArgs fun fun_kind mb_kind_info args
-  = do { (res_kind, args', leftovers, n)
-           <- tc_infer_args typeLevelMode fun fun_kind mb_kind_info args 1
+            -> TcM (TCvSubst, [TyBinder], [TcType], [LHsType Name], Int)
+               -- ^ (instantiating subst, un-insted leftover binders,
+               --   typechecked args, untypechecked args, n)
+tcInferArgs fun binders mb_kind_info args
+  = do { (subst, leftover_binders, args', leftovers, n)
+           <- tc_infer_args typeLevelMode fun binders mb_kind_info args 1
         -- now, we need to instantiate any remaining invisible arguments
-       ; let (invis_bndrs, really_res_kind) = splitPiTysInvisible res_kind
-       ; (subst, invis_args)
-           <- tcInstBindersX emptyTCvSubst mb_kind_info invis_bndrs
-       ; return ( substTy subst really_res_kind
+       ; let (invis_bndrs, other_binders) = span isInvisibleBinder leftover_binders
+       ; (subst', invis_args)
+           <- tcInstBindersX subst mb_kind_info invis_bndrs
+       ; return ( subst'
+                , other_binders
                 , args' `chkAppend` invis_args
                 , leftovers, n ) }
 
@@ -733,48 +736,40 @@ tcInferArgs fun fun_kind mb_kind_info args
 tc_infer_args :: Outputable fun
               => TcTyMode
               -> fun                      -- ^ the function
-              -> TcKind                   -- ^ function kind (zonked)
+              -> [TyBinder]               -- ^ function kind's binders (zonked)
               -> Maybe (VarEnv Kind)      -- ^ possibly, kind info (see above)
               -> [LHsType Name]           -- ^ args
               -> Int                      -- ^ number to start arg counter at
-              -> TcM (TcKind, [TcType], [LHsType Name], Int)
-tc_infer_args mode orig_ty ki mb_kind_info orig_args n0
-  = do { traceTc "tcInferApps" (ppr ki $$ ppr orig_args)
-       ; go emptyTCvSubst ki orig_args n0 [] }
+              -> TcM (TCvSubst, [TyBinder], [TcType], [LHsType Name], Int)
+tc_infer_args mode orig_ty binders mb_kind_info orig_args n0
+  = do { traceTc "tcInferApps" (ppr binders $$ ppr orig_args)
+       ; go emptyTCvSubst binders orig_args n0 [] }
   where
-    go subst fun_kind []   n acc
-      = return ( substTyUnchecked subst fun_kind, reverse acc, [], n )
+    go subst binders []   n acc
+      = return ( subst, binders, reverse acc, [], n )
     -- when we call this when checking type family patterns, we really
     -- do want to instantiate all invisible arguments. During other
     -- typechecking, we don't.
 
-    go subst fun_kind all_args n acc
-      | Just fun_kind' <- coreView fun_kind
-      = go subst fun_kind' all_args n acc
+    go subst binders all_args n acc
+      | (inv_binders, other_binders) <- span isInvisibleBinder binders
+      , not (null inv_binders)
+      = do { (subst', args') <- tcInstBindersX subst mb_kind_info inv_binders
+           ; go subst' other_binders all_args n (reverse args' ++ acc) }
 
-      | Just tv <- getTyVar_maybe fun_kind
-      , Just fun_kind' <- lookupTyVar subst tv
-      = go subst fun_kind' all_args n acc
-
-      | (inv_bndrs, res_k) <- splitPiTysInvisible fun_kind
-      , not (null inv_bndrs)
-      = do { (subst', args') <- tcInstBindersX subst mb_kind_info inv_bndrs
-           ; go subst' res_k all_args n (reverse args' ++ acc) }
-
-      | Just (bndr, res_k) <- splitPiTy_maybe fun_kind
-      , arg:args <- all_args  -- this actually has to succeed
-      = ASSERT( isVisibleBinder bndr )
-        do { let mode' | isNamedBinder bndr = kindLevel mode
-                       | otherwise          = mode
+    go subst (binder:binders) (arg:args) n acc
+      = ASSERT( isVisibleBinder binder )
+        do { let mode' | isNamedBinder binder = kindLevel mode
+                       | otherwise            = mode
            ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
-                     tc_lhs_type mode' arg (substTyUnchecked subst $ binderType bndr)
-           ; let subst' = case binderVar_maybe bndr of
+                     tc_lhs_type mode' arg (substTyUnchecked subst $ binderType binder)
+           ; let subst' = case binderVar_maybe binder of
                    Just tv -> extendTvSubst subst tv arg'
                    Nothing -> subst
-           ; go subst' res_k args (n+1) (arg' : acc) }
+           ; go subst' binders args (n+1) (arg' : acc) }
 
-      | otherwise
-      = return (substTy subst fun_kind, reverse acc, all_args, n)
+    go subst [] all_args n acc
+      = return (subst, [], reverse acc, all_args, n)
 
 -- | Applies a type to a list of arguments. Always consumes all the
 -- arguments.
@@ -789,13 +784,13 @@ tcInferApps mode orig_ty ty ki args = go ty ki args 1
   where
     go fun fun_kind []   _ = return (fun, fun_kind)
     go fun fun_kind args n
-      | Just fun_kind' <- coreView fun_kind
-      = go fun fun_kind' args n
-
-      | isPiTy fun_kind
-      = do { (res_kind, args', leftover_args, n')
-                <- tc_infer_args mode orig_ty fun_kind Nothing args n
-           ; go (mkNakedAppTys fun args') res_kind leftover_args n' }
+      | let (binders, res_kind) = splitPiTys fun_kind
+      , not (null binders)
+      = do { (subst, leftover_binders, args', leftover_args, n')
+                <- tc_infer_args mode orig_ty binders Nothing args n
+           ; let fun_kind' = substTyUnchecked subst $
+                             mkForAllTys leftover_binders res_kind
+           ; go (mkNakedAppTys fun args') fun_kind' leftover_args n' }
 
     go fun fun_kind all_args@(arg:args) n
       = do { (co, arg_k, res_k) <- matchExpectedFunKind (length all_args)
@@ -805,110 +800,6 @@ tcInferApps mode orig_ty ty ki args = go ty ki args 1
            ; go (mkNakedAppTy (fun `mkNakedCastTy` co) arg')
                 res_k args (n+1) }
 
----------------------------
--- | This is used to instantiate binders when type-checking *types* only.
--- Precondition: all binders are invisible. See also Note [Bidirectional type checking]
-tcInstBinders :: [TyBinder] -> TcM (TCvSubst, [TcType])
-tcInstBinders = tcInstBindersX emptyTCvSubst Nothing
-
--- | This is used to instantiate binders when type-checking *types* only.
--- Precondition: all binders are invisible.
--- The @VarEnv Kind@ gives some known instantiations.
--- See also Note [Bidirectional type checking]
-tcInstBindersX :: TCvSubst -> Maybe (VarEnv Kind)
-               -> [TyBinder] -> TcM (TCvSubst, [TcType])
-tcInstBindersX subst mb_kind_info bndrs
-  = do { (subst, args) <- mapAccumLM (tcInstBinderX mb_kind_info) subst bndrs
-       ; traceTc "instantiating implicit dependent vars:"
-           (vcat $ zipWith (\bndr arg -> ppr bndr <+> text ":=" <+> ppr arg)
-                           bndrs args)
-       ; return (subst, args) }
-
--- | Used only in *types*
-tcInstBinderX :: Maybe (VarEnv Kind)
-              -> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
-tcInstBinderX mb_kind_info subst binder
-  | Just tv <- binderVar_maybe binder
-  = case lookup_tv tv of
-      Just ki -> return (extendTvSubstAndInScope subst tv ki, ki)
-      Nothing -> do { (subst', tv') <- newMetaTyVarX subst tv
-                    ; return (subst', mkTyVarTy tv') }
-
-     -- This is the *only* constraint currently handled in types.
-  | Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty
-  = do { let origin = TypeEqOrigin { uo_actual   = k1
-                                   , uo_expected = mkCheckExpType k2
-                                   , uo_thing    = Nothing }
-       ; co <- case role of
-                 Nominal          -> unifyKind noThing k1 k2
-                 Representational -> emitWantedEq origin KindLevel role k1 k2
-                 Phantom          -> pprPanic "tcInstBinderX Phantom" (ppr binder)
-       ; arg' <- mk co k1 k2
-       ; return (subst, arg') }
-
-  | otherwise
-  = do { let (env, tidy_ty) = tidyOpenType emptyTidyEnv substed_ty
-       ; addErrTcM (env, text "Illegal constraint in a type:" <+> ppr tidy_ty)
-
-         -- just invent a new variable so that we can continue
-       ; u <- newUnique
-       ; let name = mkSysTvName u (fsLit "dict")
-       ; return (subst, mkTyVarTy $ mkTyVar name substed_ty) }
-
-  where
-    substed_ty = substTy subst (binderType binder)
-
-    lookup_tv tv = do { env <- mb_kind_info   -- `Maybe` monad
-                      ; lookupVarEnv env tv }
-
-      -- handle boxed equality constraints, because it's so easy
-    get_pred_tys_maybe ty
-      | Just (r, k1, k2) <- getEqPredTys_maybe ty
-      = Just (\co _ _ -> return $ mkCoercionTy co, r, k1, k2)
-      | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
-      = if | tc `hasKey` heqTyConKey
-             -> Just (mkHEqBoxTy, Nominal, k1, k2)
-           | otherwise
-             -> Nothing
-      | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
-      = if | tc `hasKey` eqTyConKey
-             -> Just (mkEqBoxTy, Nominal, k1, k2)
-           | tc `hasKey` coercibleTyConKey
-             -> Just (mkCoercibleBoxTy, Representational, k1, k2)
-           | otherwise
-             -> Nothing
-      | otherwise
-      = Nothing
-
--------------------------------
--- | This takes @a ~# b@ and returns @a ~~ b@.
-mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
--- monadic just for convenience with mkEqBoxTy
-mkHEqBoxTy co ty1 ty2
-  = return $
-    mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
-  where k1 = typeKind ty1
-        k2 = typeKind ty2
-
--- | This takes @a ~# b@ and returns @a ~ b@.
-mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
-mkEqBoxTy co ty1 ty2
-  = do { eq_tc <- tcLookupTyCon eqTyConName
-       ; let [datacon] = tyConDataCons eq_tc
-       ; hetero <- mkHEqBoxTy co ty1 ty2
-       ; return $ mkTyConApp (promoteDataCon datacon) [k, ty1, ty2, hetero] }
-  where k = typeKind ty1
-
--- | This takes @a ~R# b@ and returns @Coercible a b@.
-mkCoercibleBoxTy :: TcCoercion -> Type -> Type -> TcM Type
--- monadic just for convenience with mkEqBoxTy
-mkCoercibleBoxTy co ty1 ty2
-  = do { return $
-         mkTyConApp (promoteDataCon coercibleDataCon)
-                    [k, ty1, ty2, mkCoercionTy co] }
-  where k = typeKind ty1
-
-
 --------------------------
 checkExpectedKind :: TcType               -- the type whose kind we're checking
                   -> TcKind               -- the known kind of that type, k
@@ -1283,7 +1174,8 @@ kcHsTyVarBndrs :: Bool    -- ^ True <=> the decl being checked has a CUSK
                -> ([TyVar] -> [TyVar] -> TcM (Kind, r))
                                   -- ^ the result kind, possibly with other info
                                   -- ^ args are implicit vars, explicit vars
-               -> TcM (Kind, r)   -- ^ The full kind of the thing being declared,
+               -> TcM ([TcTyBinder], TcKind, r)
+                                  -- ^ The full kind of the thing being declared,
                                   -- with the other info
 kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns
                             , hsq_explicit = hs_tvs }) thing_inside
@@ -1293,9 +1185,9 @@ kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns
                      -- the names must line up in splitTelescopeTvs
                 else zipWithM newSigTyVar kv_ns meta_kvs
        ; tcExtendTyVarEnv2 (kv_ns `zip` kvs) $
-    do { (full_kind, _, stuff) <- bind_telescope hs_tvs (thing_inside kvs)
+    do { (binders, res_kind, _, stuff) <- bind_telescope hs_tvs (thing_inside kvs)
        ; let qkvs = filter (not . isMetaTyVar) $
-                    tyCoVarsOfTypeWellScoped full_kind
+                    tyCoVarsOfTypeWellScoped (mkForAllTys binders res_kind)
                       -- these have to be the vars made with new_skolem_tv
                       -- above. Thus, they are known to the user and should
                       -- be Specified, not Invisible, when kind-generalizing
@@ -1303,28 +1195,28 @@ kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns
                 -- the free non-meta variables in the returned kind will
                 -- contain both *mentioned* kind vars and *unmentioned* kind
                 -- vars (See case (1) under Note [Typechecking telescopes])
-             gen_kind  = if cusk
-                         then mkSpecForAllTys qkvs $ full_kind
-                         else full_kind
-       ; return (gen_kind, stuff) } }
+             all_binders = if cusk
+                           then map (mkNamedBinder Specified) qkvs ++ binders
+                           else binders
+       ; return (all_binders, res_kind, stuff) } }
   where
       -- there may be dependency between the explicit "ty" vars. So, we have
-      -- to handle them one at a time. We also need to build up a full kind
-      -- here, because this is the place we know whether to use a FunTy or a
-      -- ForAllTy. We prefer using an anonymous binder over a trivial named
+      -- to handle them one at a time. We also produce the TyBinders here,
+      -- because this is the place we know whether to use Anon or Named.
+      -- We prefer using an anonymous binder over a trivial named
       -- binder. If a user wants a trivial named one, use an explicit kind
       -- signature.
     bind_telescope :: [LHsTyVarBndr Name]
                    -> ([TyVar] -> TcM (Kind, r))
-                   -> TcM (Kind, VarSet, r)
+                   -> TcM ([TcTyBinder], TcKind, VarSet, r)
     bind_telescope [] thing
       = do { (res_kind, stuff) <- thing []
-           ; return (res_kind, tyCoVarsOfType res_kind, stuff) }
+           ; return ([], res_kind, tyCoVarsOfType res_kind, stuff) }
     bind_telescope (L _ hs_tv : hs_tvs) thing
       = do { tv_pair@(tv, _) <- kc_hs_tv hs_tv
-           ; (res_kind, fvs, stuff) <- bind_unless_scoped tv_pair $
-                                       bind_telescope hs_tvs $ \tvs ->
-                                       thing (tv:tvs)
+           ; (binders, res_kind, fvs, stuff) <- bind_unless_scoped tv_pair $
+                                                bind_telescope hs_tvs $ \tvs ->
+                                                thing (tv:tvs)
               -- we must be *lazy* in res_kind and fvs (assuming that the
               -- caller of kcHsTyVarBndrs is, too), as sometimes these hold
               -- panics. See kcConDecl.
@@ -1337,7 +1229,7 @@ kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns
                    | otherwise
                    = (mkAnonBinder k, fvs `unionVarSet` k_fvs)
 
-           ; return ( mkForAllTy bndr res_kind, fvs', stuff ) }
+           ; return (bndr : binders, res_kind, fvs', stuff ) }
 
     -- | Bind the tyvar in the env't unless the bool is True
     bind_unless_scoped :: (TcTyVar, Bool) -> TcM a -> TcM a
@@ -1650,30 +1542,28 @@ are kind vars the didn't link up in splitTelescopeTvs.
 -- Extend the env with bindings for the tyvars, taken from
 -- the kind of the tycon/class.  Give it to the thing inside, and
 -- check the result kind matches
-kcLookupKind :: Name -> TcM Kind
+kcLookupKind :: Name -> TcM ([TyBinder], Kind)
 kcLookupKind nm
   = do { tc_ty_thing <- tcLookup nm
        ; case tc_ty_thing of
-           ATcTyCon tc         -> return (tyConKind tc)
-           AGlobal (ATyCon tc) -> return (tyConKind tc)
+           ATcTyCon tc         -> return (tyConBinders tc, tyConResKind tc)
+           AGlobal (ATyCon tc) -> return (tyConBinders tc, tyConResKind tc)
            _                   -> pprPanic "kcLookupKind" (ppr tc_ty_thing) }
 
 -- See Note [Typechecking telescopes]
-splitTelescopeTvs :: Kind         -- of the head of the telescope
+splitTelescopeTvs :: [TyBinder]   -- telescope binders
                   -> LHsQTyVars Name
                   -> ( [TyVar]    -- scoped type variables
                      , NameSet    -- ungeneralized implicit variables (case 2a)
                      , [TyVar]    -- implicit type variables (cases 1 & 2)
                      , [TyVar]    -- explicit type variables (cases 3 & 4)
-                     , [(LHsKind Name, Kind)] -- see Note [Tiresome kind matching]
-                     , Kind )     -- result kind
-splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
-                                    , hsq_explicit = hs_tvs })
-  = let (bndrs, inner_ki) = splitPiTys kind
-        (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, kind_matches, mk_kind)
+                     , [(LHsKind Name, Kind)] ) -- see Note [Tiresome kind matching]
+splitTelescopeTvs bndrs tvbs@(HsQTvs { hsq_implicit = hs_kvs
+                                     , hsq_explicit = hs_tvs })
+  = let (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, kind_matches)
           = mk_tvs [] [] bndrs (mkNameSet hs_kvs) hs_tvs
     in
-    (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, kind_matches, mk_kind inner_ki)
+    (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, kind_matches)
   where
     mk_tvs :: [TyVar]    -- scoped tv accum (reversed)
            -> [TyVar]    -- implicit tv accum (reversed)
@@ -1684,8 +1574,7 @@ splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
               , NameSet           -- Case 2a names
               , [TyVar]           -- implicit tyvars
               , [TyVar]           -- explicit tyvars
-              , [(LHsKind Name, Kind)]  -- tiresome kind matches
-              , Type -> Type )    -- a function to create the result k
+              , [(LHsKind Name, Kind)] ) -- tiresome kind matches
     mk_tvs scoped_tv_acc imp_tv_acc (bndr : bndrs) all_hs_kvs all_hs_tvs
       | Just tv <- binderVar_maybe bndr
       , isInvisibleBinder bndr
@@ -1703,9 +1592,9 @@ splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
      -- a non-CUSK. The kinds *aren't* generalized, so we won't see them
      -- here.
     mk_tvs scoped_tv_acc imp_tv_acc all_bndrs all_hs_kvs all_hs_tvs
-      = let (scoped, exp_tvs, kind_matches, mk_kind)
+      = let (scoped, exp_tvs, kind_matches)
               = mk_tvs2 scoped_tv_acc [] [] all_bndrs all_hs_tvs in
-        (scoped, all_hs_kvs, reverse imp_tv_acc, exp_tvs, kind_matches, mk_kind)
+        (scoped, all_hs_kvs, reverse imp_tv_acc, exp_tvs, kind_matches)
            -- no more Case (1) or (2)
 
     -- This can't handle Case (1) or Case (2) from [Typechecking telescopes]
@@ -1716,8 +1605,7 @@ splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
             -> [LHsTyVarBndr Name]
             -> ( [TyVar]
                , [TyVar]   -- explicit tvs only
-               , [(LHsKind Name, Kind)]  -- tiresome kind matches
-               , Type -> Type )
+               , [(LHsKind Name, Kind)] )  -- tiresome kind matches
     mk_tvs2 scoped_tv_acc exp_tv_acc kind_match_acc (bndr : bndrs) (hs_tv : hs_tvs)
       | Just tv <- binderVar_maybe bndr
       = ASSERT2( isVisibleBinder bndr, err_doc )
@@ -1733,7 +1621,6 @@ splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
       where
         err_doc = vcat [ ppr (bndr : bndrs)
                        , ppr (hs_tv : hs_tvs)
-                       , ppr kind
                        , ppr tvbs ]
 
         kind_match_acc' = case hs_tv of
@@ -1741,11 +1628,10 @@ splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
           L _ (KindedTyVar _ hs_kind) -> (hs_kind, kind) : kind_match_acc
             where kind = binderType bndr
 
-    mk_tvs2 scoped_tv_acc exp_tv_acc kind_match_acc all_bndrs [] -- All done!
+    mk_tvs2 scoped_tv_acc exp_tv_acc kind_match_acc [] [] -- All done!
       = ( reverse scoped_tv_acc
         , reverse exp_tv_acc
-        , kind_match_acc   -- no need to reverse; it's not ordered
-        , mkForAllTys all_bndrs )
+        , kind_match_acc )   -- no need to reverse; it's not ordered
 
     mk_tvs2 _ _ _ all_bndrs all_hs_tvs
       = pprPanic "splitTelescopeTvs 2" (vcat [ ppr all_bndrs
@@ -1762,18 +1648,18 @@ kcTyClTyVars :: Name   -- ^ of the tycon
              -> LHsQTyVars Name
              -> TcM a -> TcM a
 kcTyClTyVars tycon hs_tvs thing_inside
-  = do { kind <- kcLookupKind tycon
-       ; let (scoped_tvs, non_cusk_kv_name_set, all_kvs, all_tvs, _, res_k)
-               = splitTelescopeTvs kind hs_tvs
+  = do { (binders, res_kind) <- kcLookupKind tycon
+       ; let (scoped_tvs, non_cusk_kv_name_set, all_kvs, all_tvs, _)
+               = splitTelescopeTvs binders hs_tvs
        ; traceTc "kcTyClTyVars splitTelescopeTvs:"
            (vcat [ text "Tycon:" <+> ppr tycon
-                 , text "Kind:" <+> ppr kind
+                 , text "Binders:" <+> ppr binders
+                 , text "res_kind:" <+> ppr res_kind
                  , text "hs_tvs:" <+> ppr hs_tvs
                  , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs
                  , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs
                  , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs
-                 , text "non-CUSK kvs:" <+> ppr non_cusk_kv_name_set
-                 , text "res_k:" <+> ppr res_k] )
+                 , text "non-CUSK kvs:" <+> ppr non_cusk_kv_name_set ] )
 
             -- need to look up the non-cusk kvs in order to get their
             -- kinds right, in case the kinds were informed by
@@ -1799,7 +1685,7 @@ kcTyClTyVars tycon hs_tvs thing_inside
          thing_inside }
 
 tcTyClTyVars :: Name -> LHsQTyVars Name      -- LHS of the type or class decl
-             -> ([TyVar] -> [TyVar] -> Kind -> Kind -> TcM a) -> TcM a
+             -> ([TyVar] -> [TyVar] -> [TyBinder] -> Kind -> TcM a) -> TcM a
 -- ^ Used for the type variables of a type or class decl
 -- on the second full pass (type-checking/desugaring) in TcTyClDecls.
 -- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
@@ -1807,7 +1693,7 @@ tcTyClTyVars :: Name -> LHsQTyVars Name      -- LHS of the type or class decl
 -- (tcTyClTyVars T [a,b] thing_inside)
 --   where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
 --   calls thing_inside with arguments
---      [k1,k2] [a,b] (forall (k1:*) (k2:*) (a:k1 -> *) (b:k1). k2 -> *) (k2 -> *)
+--      [k1,k2] [a,b] [k1:*, k2:*, a:k1 -> *, b:k1] (k2 -> *)
 --   having also extended the type environment with bindings
 --   for k1,k2,a,b
 --
@@ -1816,27 +1702,27 @@ tcTyClTyVars :: Name -> LHsQTyVars Name      -- LHS of the type or class decl
 -- The LHsTyVarBndrs is always user-written, and the full, generalised
 -- kind of the tycon is available in the local env.
 tcTyClTyVars tycon hs_tvs thing_inside
-  = do { kind <- kcLookupKind tycon
+  = do { (binders, res_kind) <- kcLookupKind tycon
        ; let ( scoped_tvs, float_kv_name_set, all_kvs
-               , all_tvs, kind_matches, res_k )
-                 = splitTelescopeTvs kind hs_tvs
+               , all_tvs, kind_matches )
+                 = splitTelescopeTvs binders hs_tvs
        ; traceTc "tcTyClTyVars splitTelescopeTvs:"
            (vcat [ text "Tycon:" <+> ppr tycon
-                 , text "Kind:" <+> ppr kind
+                 , text "Binders:" <+> ppr binders
+                 , text "res_kind:" <+> ppr res_kind
                  , text "hs_tvs:" <+> ppr hs_tvs
                  , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs
                  , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs
                  , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs
                  , text "floating kvs:" <+> ppr float_kv_name_set
-                 , text "Tiresome kind matches:" <+> ppr kind_matches
-                 , text "res_k:" <+> ppr res_k] )
+                 , text "Tiresome kind matches:" <+> ppr kind_matches ] )
 
        ; float_kvs <- deal_with_float_kvs float_kv_name_set kind_matches
                                           scoped_tvs all_tvs
 
        ; tcExtendTyVarEnv (float_kvs ++ scoped_tvs) $
            -- the float_kvs are already in the all_kvs
-         thing_inside all_kvs all_tvs kind res_k }
+         thing_inside all_kvs all_tvs binders res_kind }
   where
          -- See Note [Free-floating kind vars]
     deal_with_float_kvs float_kv_name_set kind_matches scoped_tvs all_tvs
@@ -1879,13 +1765,15 @@ tcTyClTyVars tycon hs_tvs thing_inside
                   2 (pprTvBndrs all_tvs) ]
 
 -----------------------------------
-tcDataKindSig :: Kind -> TcM [TyVar]
+tcDataKindSig :: Kind -> TcM ([TyVar], [TyBinder], Kind)
 -- GADT decls can have a (perhaps partial) kind signature
 --      e.g.  data T :: * -> * -> * where ...
 -- This function makes up suitable (kinded) type variables for
 -- the argument kinds, and checks that the result kind is indeed *.
 -- We use it also to make up argument type variables for for data instances.
 -- Never emits constraints.
+-- Returns the new TyVars, the extracted TyBinders, and the new, reduced
+-- result kind (which should always be Type or a synonym thereof)
 tcDataKindSig kind
   = do  { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
         ; span <- getSrcSpanM
@@ -1897,8 +1785,9 @@ tcDataKindSig kind
                             , isNothing (lookupLocalRdrOcc rdr_env occ) ]
                  -- Note [Avoid name clashes for associated data types]
 
-        ; return [ mk_tv span uniq occ kind
-                 | ((kind, occ), uniq) <- arg_kinds `zip` occs `zip` uniqs ] }
+        ; return ( [ mk_tv span uniq occ kind
+                   | ((kind, occ), uniq) <- arg_kinds `zip` occs `zip` uniqs ]
+                 , bndrs, res_kind ) }
   where
     (bndrs, res_kind) = splitPiTys kind
     arg_kinds         = map binderType bndrs
@@ -2121,8 +2010,8 @@ in-scope variables that it should not unify with, but it's fiddly.
 
 -- | Produce an 'TcKind' suitable for a checking a type that can be * or #.
 ekOpen :: TcM TcKind
-ekOpen = do { lev <- newFlexiTyVarTy levityTy
-            ; return (tYPE lev) }
+ekOpen = do { rr <- newFlexiTyVarTy runtimeRepTy
+            ; return (tYPE rr) }
 
 unifyKinds :: [(TcType, TcKind)] -> TcM ([TcType], TcKind)
 unifyKinds act_kinds
index 82c66cc..460089e 100644 (file)
@@ -684,12 +684,13 @@ tcDataFamInstDecl mb_clsinfo
                                              axiom_name eta_tvs [] fam_tc eta_pats
                                              (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
                     parent = DataFamInstTyCon axiom fam_tc pats'
-                    rep_tc_kind = mkPiTypesPreferFunTy full_tvs liftedTypeKind
+                    ty_binders = mkTyBindersPreferAnon full_tvs liftedTypeKind
+
 
                       -- NB: Use the full_tvs from the pats. See bullet toward
                       -- the end of Note [Data type families] in TyCon
                     rep_tc   = mkAlgTyCon rep_tc_name
-                                          rep_tc_kind
+                                          ty_binders liftedTypeKind
                                           full_tvs
                                           (map (const Nominal) full_tvs)
                                           (fmap unLoc cType) stupid_theta
@@ -1275,7 +1276,7 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
         error_rhs dflags = L inst_loc $ HsApp error_fun (error_msg dflags)
         error_fun    = L inst_loc $
                        wrapId (mkWpTyApps
-                                [ getLevity "tcInstanceMethods.tc_default" meth_tau
+                                [ getRuntimeRep "tcInstanceMethods.tc_default" meth_tau
                                 , meth_tau])
                               nO_METHOD_BINDING_ERROR_ID
         error_msg dflags = L inst_loc (HsLit (HsStringPrim ""
index b7a96d9..90f7243 100644 (file)
@@ -2027,7 +2027,7 @@ onlyNamedBndrsApplied tc ks
  = all isNamedBinder used_bndrs &&
    not (any isNamedBinder leftover_bndrs)
  where
-   (bndrs, _)                   = splitPiTys (tyConKind tc)
+   bndrs                        = tyConBinders tc
    (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
 
 doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult
index d058107..e8c120d 100644 (file)
@@ -70,7 +70,7 @@ module TcMType (
   zonkTcTyVar, zonkTcTyVars, zonkTyCoVarsAndFV, zonkTcTypeAndFV,
   zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType, quantifyTyVars,
   defaultKindVar,
-  zonkTcTyCoVarBndr, zonkTcType, zonkTcTypes, zonkCo,
+  zonkTcTyCoVarBndr, zonkTcTyBinder, zonkTcType, zonkTcTypes, zonkCo,
   zonkTyCoVarKind, zonkTcTypeMapper,
 
   zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
@@ -330,10 +330,10 @@ test gadt/gadt-escape1.
 -- | Make an 'ExpType' suitable for inferring a type of kind * or #.
 newOpenInferExpType :: TcM ExpType
 newOpenInferExpType
-  = do { lev <- newFlexiTyVarTy levityTy
+  = do { rr <- newFlexiTyVarTy runtimeRepTy
        ; u <- newUnique
        ; tclvl <- getTcLevel
-       ; let ki = tYPE lev
+       ; let ki = tYPE rr
        ; traceTc "newOpenInferExpType" (ppr u <+> dcolon <+> ppr ki)
        ; ref <- newMutVar Nothing
        ; return (Infer u tclvl ki ref) }
@@ -549,7 +549,6 @@ newFskTyVar fam_ty
   = do { uniq <- newUnique
        ; let name = mkSysTvName uniq (fsLit "fsk")
        ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
-
 {-
 Note [Kind substitution when instantiating]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -754,8 +753,8 @@ newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 -- | Create a tyvar that can be a lifted or unlifted type.
 newOpenFlexiTyVarTy :: TcM TcType
 newOpenFlexiTyVarTy
-  = do { lev <- newFlexiTyVarTy levityTy
-       ; newFlexiTyVarTy (tYPE lev) }
+  = do { rr <- newFlexiTyVarTy runtimeRepTy
+       ; newFlexiTyVarTy (tYPE rr) }
 
 newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
 newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
@@ -904,15 +903,15 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM (Maybe TcTyVar)
 --
 -- This returns a tyvar if it should be quantified over; otherwise,
 -- it returns Nothing. Nothing is
--- returned only if zonkQuantifiedTyVar is passed a Levity meta-tyvar,
--- in order to default to Lifted.
+-- returned only if zonkQuantifiedTyVar is passed a RuntimeRep meta-tyvar,
+-- in order to default to PtrRepLifted.
 zonkQuantifiedTyVar tv = left_only `liftM` zonkQuantifiedTyVarOrType tv
   where left_only :: Either a b -> Maybe a
         left_only (Left x) =  Just x
         left_only (Right _) = Nothing
 
 -- | Like zonkQuantifiedTyVar, but if zonking reveals that the tyvar
--- should become a type (when defaulting a levity var to Lifted), it
+-- should become a type (when defaulting a RuntimeRep var to PtrRepLifted), it
 -- returns the type instead.
 zonkQuantifiedTyVarOrType :: TcTyVar -> TcM (Either TcTyVar TcType)
 zonkQuantifiedTyVarOrType tv
@@ -931,19 +930,19 @@ zonkQuantifiedTyVarOrType tv
                      Flexi -> return ()
                      Indirect ty -> WARN( True, ppr tv $$ ppr ty )
                                     return ()
-             if isLevityVar tv
-             then do { writeMetaTyVar tv liftedDataConTy
-                     ; return (Right liftedDataConTy) }
+             if isRuntimeRepVar tv
+             then do { writeMetaTyVar tv ptrRepLiftedTy
+                     ; return (Right ptrRepLiftedTy) }
              else Left `liftM` skolemiseUnboundMetaTyVar tv vanillaSkolemTv
       _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
 
 -- | Take an (unconstrained) meta tyvar and default it. Works only for
--- kind vars (of type BOX) and levity vars (of type Levity).
+-- kind vars (of type *) and RuntimeRep vars (of type RuntimeRep).
 defaultKindVar :: TcTyVar -> TcM Kind
 defaultKindVar kv
   | ASSERT( isMetaTyVar kv )
-    isLevityVar kv
-  = writeMetaTyVar kv liftedDataConTy >> return liftedDataConTy
+    isRuntimeRepVar kv
+  = writeMetaTyVar kv ptrRepLiftedTy >> return ptrRepLiftedTy
   | otherwise
   = writeMetaTyVar kv liftedTypeKind >> return liftedTypeKind
 
@@ -1283,6 +1282,11 @@ zonkTcTyCoVarBndr tyvar
   = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), ppr tyvar ) do
     updateTyVarKindM zonkTcType tyvar
 
+-- | Zonk a TyBinder
+zonkTcTyBinder :: TcTyBinder -> TcM TcTyBinder
+zonkTcTyBinder (Anon ty)      = Anon <$> zonkTcType ty
+zonkTcTyBinder (Named tv vis) = Named <$> zonkTcTyCoVarBndr tv <*> pure vis
+
 zonkTcTyVar :: TcTyVar -> TcM TcType
 -- Simply look through all Flexis
 zonkTcTyVar tv
index 4d1d09a..bd769bf 100644 (file)
@@ -458,8 +458,8 @@ tc_pat penv (TuplePat pats boxity _) pat_ty thing_inside
               tc = tupleTyCon boxity arity
         ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
                                                penv pat_ty
-                     -- Unboxed tuples have levity vars, which we discard:
-                     -- See Note [Unboxed tuple levity vars] in TyCon
+                     -- Unboxed tuples have RuntimeRep vars, which we discard:
+                     -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
         ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys
                                            Boxed   -> arg_tys
         ; (pats', res) <- tc_lpats penv pats (map mkCheckExpType con_arg_tys)
index 1e83324..b627cd4 100644 (file)
@@ -19,7 +19,7 @@ import TcRnMonad
 import TcEnv
 import TcMType
 import TysPrim
-import TysWiredIn  ( levityTy )
+import TysWiredIn  ( runtimeRepTy )
 import Name
 import SrcLoc
 import PatSyn
@@ -463,13 +463,13 @@ tcPatSynMatcher has_sig (L loc name) lpat
                 (univ_tvs, req_theta, req_ev_binds, req_dicts)
                 (ex_tvs, ex_tys, prov_theta, prov_dicts)
                 (args, arg_tys) pat_ty
-  = do { lev_uniq <- newUnique
-       ; tv_uniq  <- newUnique
-       ; let lev_name = mkInternalName lev_uniq (mkTyVarOcc "rlev") loc
+  = do { rr_uniq <- newUnique
+       ; tv_uniq <- newUnique
+       ; let rr_name  = mkInternalName rr_uniq (mkTyVarOcc "rep") loc
              tv_name  = mkInternalName tv_uniq (mkTyVarOcc "r") loc
-             lev_tv   = mkTcTyVar lev_name levityTy   (SkolemTv False)
-             lev      = mkTyVarTy lev_tv
-             res_tv   = mkTcTyVar tv_name  (tYPE lev) (SkolemTv False)
+             rr_tv    = mkTcTyVar rr_name runtimeRepTy (SkolemTv False)
+             rr       = mkTyVarTy rr_tv
+             res_tv   = mkTcTyVar tv_name  (tYPE rr) (SkolemTv False)
              is_unlifted = null args && null prov_dicts
              res_ty = mkTyVarTy res_tv
              (cont_args, cont_arg_tys)
@@ -487,7 +487,7 @@ tcPatSynMatcher has_sig (L loc name) lpat
        ; fail         <- newSysLocalId (fsLit "fail")  fail_ty
 
        ; let matcher_tau   = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
-             matcher_sigma = mkInvSigmaTy (lev_tv:res_tv:univ_tvs) req_theta matcher_tau
+             matcher_sigma = mkInvSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
              matcher_id    = mkExportedVanillaId matcher_name matcher_sigma
                              -- See Note [Exported LocalIds] in Id
 
@@ -517,7 +517,7 @@ tcPatSynMatcher has_sig (L loc name) lpat
                        , mg_res_ty = res_ty
                        , mg_origin = Generated
                        }
-             match = mkMatch [] (mkHsLams (lev_tv:res_tv:univ_tvs) req_dicts body')
+             match = mkMatch [] (mkHsLams (rr_tv:res_tv:univ_tvs) req_dicts body')
                              (noLoc EmptyLocalBinds)
              mg = MG{ mg_alts = L (getLoc match) [match]
                     , mg_arg_tys = []
index fdc6e5e..a2a04e9 100644 (file)
@@ -1915,7 +1915,7 @@ tcGhciStmts stmts
                        (noLoc $ ExplicitList unitTy Nothing (map mk_item ids)) ;
             mk_item id = let ty_args = [idType id, unitTy] in
                          nlHsApp (nlHsTyApp unsafeCoerceId
-                                   (map (getLevity "tcGhciStmts") ty_args ++ ty_args))
+                                   (map (getRuntimeRep "tcGhciStmts") ty_args ++ ty_args))
                                  (nlHsVar id) ;
             stmts = tc_stmts ++ [noLoc (mkLastStmt ret_expr)]
         } ;
index 053c53b..4e5cceb 100644 (file)
@@ -929,9 +929,9 @@ Note [Flavours with roles]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 The system described in Note [inert_eqs: the inert equalities]
 discusses an abstract
-set of flavours. In GHC, flavours have three components: the flavour proper,
-taken from {Wanted, Derived, Given}; the equality relation (often called
-role), taken from {NomEq, ReprEq}; and the levity, taken from {Lifted, Unlifted}.
+set of flavours. In GHC, flavours have two components: the flavour proper,
+taken from {Wanted, Derived, Given} and the equality relation (often called
+role), taken from {NomEq, ReprEq}.
 When substituting w.r.t. the inert set,
 as described in Note [inert_eqs: the inert equalities],
 we must be careful to respect all components of a flavour.
index be07358..a19ceaa 100644 (file)
@@ -37,7 +37,7 @@ import TcSMonad  as TcS
 import TcType
 import TrieMap       () -- DV: for now
 import Type
-import TysWiredIn    ( liftedDataConTy )
+import TysWiredIn    ( ptrRepLiftedTy )
 import Unify         ( tcMatchTy )
 import Util
 import Var
@@ -1488,24 +1488,24 @@ promoteTyVarTcS tclvl tv
   | otherwise
   = return ()
 
--- | If the tyvar is a levity var, set it to Lifted. Returns whether or
+-- | If the tyvar is a RuntimeRep var, set it to PtrRepLifted. Returns whether or
 -- not this happened.
 defaultTyVar :: TcTyVar -> TcM ()
 -- Precondition: MetaTyVars only
 -- See Note [DefaultTyVar]
 defaultTyVar the_tv
-  | isLevityVar the_tv
-  = do { traceTc "defaultTyVar levity" (ppr the_tv)
-       ; writeMetaTyVar the_tv liftedDataConTy }
+  | isRuntimeRepVar the_tv
+  = do { traceTc "defaultTyVar RuntimeRep" (ppr the_tv)
+       ; writeMetaTyVar the_tv ptrRepLiftedTy }
 
   | otherwise = return ()    -- The common case
 
 -- | Like 'defaultTyVar', but in the TcS monad.
 defaultTyVarTcS :: TcTyVar -> TcS Bool
 defaultTyVarTcS the_tv
-  | isLevityVar the_tv
-  = do { traceTcS "defaultTyVarTcS levity" (ppr the_tv)
-       ; unifyTyVar the_tv liftedDataConTy
+  | isRuntimeRepVar the_tv
+  = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
+       ; unifyTyVar the_tv ptrRepLiftedTy
        ; return True }
   | otherwise
   = return False  -- the common case
@@ -1591,13 +1591,13 @@ There are two caveats:
 Note [DefaultTyVar]
 ~~~~~~~~~~~~~~~~~~~
 defaultTyVar is used on any un-instantiated meta type variables to
-default any levity variables to Lifted.  This is important
+default any RuntimeRep variables to PtrRepLifted.  This is important
 to ensure that instance declarations match.  For example consider
 
      instance Show (a->b)
      foo x = show (\_ -> True)
 
-Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
+Then we'll get a constraint (Show (p ->q)) where p has kind (TYPE r),
 and that won't match the typeKind (*) in the instance decl.  See tests
 tc217 and tc175.
 
@@ -1607,7 +1607,7 @@ hand.  However we aren't ready to default them fully to () or
 whatever, because the type-class defaulting rules have yet to run.
 
 An alternate implementation would be to emit a derived constraint setting
-the levity variable to Lifted, but this seems unnecessarily indirect.
+the RuntimeRep variable to PtrRepLifted, but this seems unnecessarily indirect.
 
 Note [Promote _and_ default when inferring]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
index 921da07..ac2ad01 100644 (file)
@@ -1309,14 +1309,9 @@ reifyTyCon tc
 
   | isTypeFamilyTyCon tc
   = do { let tvs      = tyConTyVars tc
-             kind     = tyConKind tc
+             res_kind = tyConResKind tc
              resVar   = famTcResVar tc
 
-             -- we need the *result kind* (see #8884)
-             (kvs, mono_kind) = splitForAllTys kind
-                                -- tyConArity includes *kind* params
-             (_, res_kind)    = splitFunTysN (tyConArity tc - length kvs)
-                                             mono_kind
        ; kind' <- reifyKind res_kind
        ; let (resultSig, injectivity) =
                  case resVar of
@@ -1351,13 +1346,8 @@ reifyTyCon tc
 
   | isDataFamilyTyCon tc
   = do { let tvs      = tyConTyVars tc
-             kind     = tyConKind tc
+             res_kind = tyConResKind tc
 
-             -- we need the *result kind* (see #8884)
-             (kvs, mono_kind) = splitForAllTys kind
-                                -- tyConArity includes *kind* params
-             (_, res_kind)    = splitFunTysN (tyConArity tc - length kvs)
-                                             mono_kind
        ; kind' <- fmap Just (reifyKind res_kind)
 
        ; tvs' <- reifyTyVars tvs (Just tc)
@@ -1732,8 +1722,9 @@ reify_tc_app tc tys
   = do { tys' <- reifyTypes (filterOutInvisibleTypes tc tys)
        ; maybe_sig_t (mkThAppTs r_tc tys') }
   where
-    arity   = tyConArity tc
-    tc_kind = tyConKind tc
+    arity       = tyConArity tc
+    tc_binders  = tyConBinders tc
+    tc_res_kind = tyConResKind tc
 
     r_tc | isTupleTyCon tc                = if isPromotedDataCon tc
                                             then TH.PromotedTupleT arity
@@ -1756,18 +1747,15 @@ reify_tc_app tc tys
       = return th_type
 
     needs_kind_sig
-      | Just result_ki <- peel_off_n_args tc_kind (length tys)
-      = not $ isEmptyVarSet $ filterVarSet isTyVar $ tyCoVarsOfType result_ki
-      | otherwise
+      | GT <- compareLength tys tc_binders
+      , tcIsTyVarTy tc_res_kind
       = True
-
-    peel_off_n_args :: Kind -> Arity -> Maybe Kind
-    peel_off_n_args k 0 = Just k
-    peel_off_n_args k n
-      | Just (_, res_k) <- splitPiTy_maybe k
-      = peel_off_n_args res_k (n-1)
       | otherwise
-      = Nothing
+      = not $
+        isEmptyVarSet $
+        filterVarSet isTyVar $
+        tyCoVarsOfType $
+        mkForAllTys (dropList tys tc_binders) tc_res_kind
 
 reifyPred :: TyCoRep.PredType -> TcM TH.Pred
 reifyPred ty
index e68efd0..6fee012 100644 (file)
@@ -126,8 +126,8 @@ tcTyClGroup tyclds
   = do {    -- Step 1: kind-check this group and returns the final
             -- (possibly-polymorphic) kind of each TyCon and Class
             -- See Note [Kind checking for type and class decls]
-         names_w_poly_kinds <- kcTyClGroup tyclds
-       ; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds)
+         tc_tycons <- kcTyClGroup tyclds
+       ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
 
             -- Step 2: type-check all groups together, returning
             -- the final TyCons and Classes
@@ -143,13 +143,12 @@ tcTyClGroup tyclds
                  -- NB: if the decls mention any ill-staged data cons
                  -- (see Note [Recusion and promoting data constructors])
                  -- we will have failed already in kcTyClGroup, so no worries here
-           ; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
+           ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
 
                  -- Also extend the local type envt with bindings giving
                  -- the (polymorphic) kind of each knot-tied TyCon or Class
                  -- See Note [Type checking recursive type and class declarations]
-             tcExtendKindEnv2 [ mkTcTyConPair name kind m_arity
-                              | (name, kind, m_arity) <-  names_w_poly_kinds ] $
+             tcExtendKindEnv2 (map mkTcTyConPair tc_tycons)              $
 
                  -- Kind and type check declarations for this group
              mapM (tcTyClDecl rec_flags) decls }
@@ -169,8 +168,12 @@ tcTyClGroup tyclds
            -- they may be mentioned in interface files
        ; tcExtendTyConEnv tyclss $
          tcAddImplicits tyclss }
+  where
+    ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
+                                  , ppr (tyConBinders tc) <> comma
+                                  , ppr (tyConResKind tc) ])
 
-zipRecTyClss :: [(Name, Kind, Maybe Arity)]
+zipRecTyClss :: [TcTyCon]
              -> [TyCon]           -- Knot-tied
              -> [(Name,TyThing)]
 -- Build a name-TyThing mapping for the TyCons bound by decls
@@ -178,8 +181,8 @@ zipRecTyClss :: [(Name, Kind, Maybe Arity)]
 -- The TyThings in the result list must have a visible ATyCon,
 -- because typechecking types (in, say, tcTyClDecl) looks at
 -- this outer constructor
-zipRecTyClss kind_pairs rec_tycons
-  = [ (name, ATyCon (get name)) | (name, _kind, _m_arity) <- kind_pairs ]
+zipRecTyClss tc_tycons rec_tycons
+  = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
   where
     rec_tc_env :: NameEnv TyCon
     rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
@@ -260,7 +263,7 @@ See also Note [Kind checking recursive type and class declarations]
 
 -}
 
-kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind,Maybe Arity)]
+kcTyClGroup :: TyClGroup Name -> TcM [TcTyCon]
 -- Kind check this group, kind generalize, and return the resulting local env
 -- This bindds the TyCons and Classes of the group, but not the DataCons
 -- See Note [Kind checking for type and class decls]
@@ -303,24 +306,29 @@ kcTyClGroup (TyClGroup { group_tyclds = decls })
         ; return res }
 
   where
-    generalise :: TcTypeEnv -> Name -> TcM (Name, Kind, Maybe Arity)
+    generalise :: TcTypeEnv -> Name -> TcM TcTyCon
     -- For polymorphic things this is a no-op
     generalise kind_env name
-      = do { let (kc_kind, kc_unsat) = case lookupNameEnv kind_env name of
-                   Just (ATcTyCon tc) -> ( tyConKind tc
-                                         , if mightBeUnsaturatedTyCon tc
-                                           then Nothing
-                                           else Just $ tyConArity tc )
-                   _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
-           ; kvs <- kindGeneralize kc_kind
-           ; kc_kind' <- zonkTcTypeToType emptyZonkEnv kc_kind
+      = do { let tc = case lookupNameEnv kind_env name of
+                        Just (ATcTyCon tc) -> tc
+                        _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
+                 kc_binders  = tyConBinders tc
+                 kc_res_kind = tyConResKind tc
+           ; kvs <- kindGeneralize (mkForAllTys kc_binders kc_res_kind)
+           ; (kc_binders', kc_res_kind') <- zonkTcKindToKind kc_binders kc_res_kind
 
                       -- Make sure kc_kind' has the final, zonked kind variables
-           ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
-           ; return (name, mkInvForAllTys kvs kc_kind', kc_unsat) }
+           ; traceTc "Generalise kind" $
+             vcat [ ppr name, ppr kc_binders, ppr kc_res_kind
+                  , ppr kvs, ppr kc_binders', ppr kc_res_kind' ]
+
+           ; return (mkTcTyCon name
+                               (map (mkNamedBinder Invisible) kvs ++ kc_binders')
+                               kc_res_kind'
+                               (mightBeUnsaturatedTyCon tc)) }
 
     generaliseTCD :: TcTypeEnv
-                  -> LTyClDecl Name -> TcM [(Name, Kind, Maybe Arity)]
+                  -> LTyClDecl Name -> TcM [TcTyCon]
     generaliseTCD kind_env (L _ decl)
       | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
       = do { first <- generalise kind_env name
@@ -336,19 +344,15 @@ kcTyClGroup (TyClGroup { group_tyclds = decls })
            ; return [res] }
 
     generaliseFamDecl :: TcTypeEnv
-                      -> FamilyDecl Name -> TcM (Name, Kind, Maybe Arity)
+                      -> FamilyDecl Name -> TcM TcTyCon
     generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
       = generalise kind_env name
 
-mkTcTyConPair :: Name -> TcKind
-              -> Maybe Arity  -- ^ Nothing <=> tycon can be unsaturated
-              -> (Name, TcTyThing)
+mkTcTyConPair :: TcTyCon -> (Name, TcTyThing)
 -- Makes a binding to put in the local envt, binding
--- a name to a TcTyCon with the specified kind
-mkTcTyConPair name kind Nothing
-  = (name, ATcTyCon (mkTcTyCon name kind True 0))
-mkTcTyConPair name kind (Just arity)
-  = (name, ATcTyCon (mkTcTyCon name kind False arity))
+-- a name to a TcTyCon
+mkTcTyConPair tc
+  = (getName tc, ATcTyCon tc)
 
 mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)]
 mk_thing_env [] = []
@@ -388,26 +392,28 @@ getInitialKind :: TyClDecl Name
 -- No family instances are passed to getInitialKinds
 
 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
-  = do { (cl_kind, inner_prs) <-
+  = do { (cl_binders, cl_kind, inner_prs) <-
            kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $ \_ _ ->
            do { inner_prs <- getFamDeclInitialKinds ats
               ; return (constraintKind, inner_prs) }
-       ; cl_kind <- zonkTcType cl_kind
-       ; let main_pr = mkTcTyConPair name cl_kind Nothing
+       ; cl_binders <- mapM zonkTcTyBinder cl_binders
+       ; cl_kind    <- zonkTcType cl_kind
+       ; let main_pr = mkTcTyConPair (mkTcTyCon name cl_binders cl_kind True)
        ; return (main_pr : inner_prs) }
 
 getInitialKind decl@(DataDecl { tcdLName = L _ name
                               , tcdTyVars = ktvs
                               , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                          , dd_cons = cons } })
-  = do  { (decl_kind, _) <-
+  = do  { (decl_binders, decl_kind, _) <-
            kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $ \_ _ ->
            do { res_k <- case m_sig of
                            Just ksig -> tcLHsKind ksig
                            Nothing   -> return liftedTypeKind
               ; return (res_k, ()) }
-        ; decl_kind <- zonkTcType decl_kind
-        ; let main_pr = mkTcTyConPair name decl_kind Nothing
+        ; decl_binders <- mapM zonkTcTyBinder decl_binders
+        ; decl_kind    <- zonkTcType decl_kind
+        ; let main_pr = mkTcTyConPair (mkTcTyCon name decl_binders decl_kind True)
               inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
                           | L _ con' <- cons, con <- getConNames con' ]
         ; return (main_pr : inner_prs) }
@@ -431,7 +437,7 @@ getFamDeclInitialKind decl@(FamilyDecl { fdLName     = L _ name
                                        , fdTyVars    = ktvs
                                        , fdResultSig = L _ resultSig
                                        , fdInfo      = info })
-  = do { (fam_kind, _) <-
+  = do { (fam_binders, fam_kind, _) <-
            kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $ \_ _ ->
            do { res_k <- case resultSig of
                       KindSig ki                        -> tcLHsKind ki
@@ -442,42 +448,43 @@ getFamDeclInitialKind decl@(FamilyDecl { fdLName     = L _ name
                         -- by default
                         | otherwise                -> newMetaKindVar
               ; return (res_k, ()) }
-       ; fam_kind <- zonkTcType fam_kind
-       ; return [ mkTcTyConPair name fam_kind m_arity ] }
+       ; fam_binders <- mapM zonkTcTyBinder fam_binders
+       ; fam_kind    <- zonkTcType fam_kind
+       ; return [ mkTcTyConPair (mkTcTyCon name fam_binders fam_kind unsat) ] }
   where
-    m_arity = case info of
-      DataFamily         -> Nothing
-      OpenTypeFamily     -> Just (length $ hsQTvExplicit ktvs)
-      ClosedTypeFamily _ -> Just (length $ hsQTvExplicit ktvs)
+    unsat = case info of
+      DataFamily         -> True
+      OpenTypeFamily     -> False
+      ClosedTypeFamily _ -> False
 
 ----------------
 kcSynDecls :: [SCC (LTyClDecl Name)]
            -> TcM TcLclEnv -- Kind bindings
 kcSynDecls [] = getLclEnv
 kcSynDecls (group : groups)
-  = do  { (n,k,arity) <- kcSynDecl1 group
-        ; tcExtendKindEnv2 [ mkTcTyConPair n k (Just arity) ] $
+  = do  { tc <- kcSynDecl1 group
+        ; tcExtendKindEnv2 [ mkTcTyConPair tc ] $
           kcSynDecls groups }
 
 kcSynDecl1 :: SCC (LTyClDecl Name)
-           -> TcM (Name,TcKind,Arity) -- Kind bindings
+           -> TcM TcTyCon -- Kind bindings
 kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
 kcSynDecl1 (CyclicSCC decls)       = do { recSynErr decls; failM }
                                      -- Fail here to avoid error cascade
                                      -- of out-of-scope tycons
 
-kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind, Arity)
+kcSynDecl :: TyClDecl Name -> TcM TcTyCon
 kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
                         , tcdRhs = rhs })
   -- Returns a possibly-unzonked kind
   = tcAddDeclCtxt decl $
-    do { (syn_kind, _) <-
+    do { (syn_binders, syn_kind, _) <-
            kcHsTyVarBndrs (hsDeclHasCusk decl) hs_tvs $ \_ _ ->
            do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
               ; (_, rhs_kind) <- tcLHsType rhs
               ; traceTc "kcd2" (ppr name)
               ; return (rhs_kind, ()) }
-       ; return (name, syn_kind, length $ hsQTvExplicit hs_tvs) }
+       ; return (mkTcTyCon name syn_binders syn_kind False) }
 kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
 
 ------------------------------------------------------------------------
@@ -525,10 +532,11 @@ kcTyClDecl (FamDecl (FamilyDecl { fdLName  = L _ fam_tc_name
 -- do anything here
   = case fd_info of
       ClosedTypeFamily (Just eqns) ->
-        do { tc_kind <- kcLookupKind fam_tc_name
+        do { (tc_binders, tc_res_kind) <- kcLookupKind fam_tc_name
            ; let fam_tc_shape = ( fam_tc_name
                                 , length $ hsQTvExplicit hs_tvs
-                                , tc_kind )
+                                , tc_binders
+                                , tc_res_kind )
            ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns }
       _ -> return ()
 
@@ -676,15 +684,15 @@ tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
 tcTyClDecl1 _parent rec_info
             (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
   = ASSERT( isNothing _parent )
-    tcTyClTyVars tc_name tvs $ \ kvs' tvs' full_kind res_kind ->
-    tcTySynRhs rec_info tc_name (kvs' ++ tvs') full_kind res_kind rhs
+    tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind ->
+    tcTySynRhs rec_info tc_name (kvs' ++ tvs') binders res_kind rhs
 
   -- "data/newtype" declaration
 tcTyClDecl1 _parent rec_info
             (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
   = ASSERT( isNothing _parent )
-    tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_kind res_kind ->
-    tcDataDefn rec_info tc_name (kvs' ++ tvs') tycon_kind res_kind defn
+    tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_binders res_kind ->
+    tcDataDefn rec_info tc_name (kvs' ++ tvs') tycon_binders res_kind defn
 
 tcTyClDecl1 _parent rec_info
             (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
@@ -693,13 +701,13 @@ tcTyClDecl1 _parent rec_info
             , tcdATs = ats, tcdATDefs = at_defs })
   = ASSERT( isNothing _parent )
     do { clas <- fixM $ \ clas ->
-            tcTyClTyVars class_name tvs $ \ kvs' tvs' full_kind res_kind ->
+            tcTyClTyVars class_name tvs $ \ kvs' tvs' binders res_kind ->
             do { MASSERT( isConstraintKind res_kind )
                  -- This little knot is just so we can get
                  -- hold of the name of the class TyCon, which we
                  -- need to look up its recursiveness
                ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr kvs' $$
-                                          ppr tvs' $$ ppr full_kind)
+                                          ppr tvs' $$ ppr binders)
                ; let tycon_name = tyConName (classTyCon clas)
                      tc_isrec = rti_is_rec rec_info tycon_name
                      roles = rti_roles rec_info tycon_name
@@ -712,7 +720,7 @@ tcTyClDecl1 _parent rec_info
                ; at_stuff <- tcClassATs class_name clas ats at_defs
                ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
                ; clas <- buildClass
-                            class_name (kvs' ++ tvs') roles ctxt' full_kind
+                            class_name (kvs' ++ tvs') roles ctxt' binders
                             fds' at_stuff
                             sig_stuff mindef tc_isrec
                ; traceTc "tcClassDecl" (ppr fundeps $$ ppr (kvs' ++ tvs') $$
@@ -730,25 +738,26 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
                               , fdTyVars = tvs, fdResultSig = L _ sig
                               , fdInjectivityAnn = inj })
   | DataFamily <- fam_info
-  = tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_kind res_kind -> do
+  = tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> do
   { traceTc "data family:" (ppr tc_name)
   ; checkFamFlag tc_name
-  ; extra_tvs   <- tcDataKindSig res_kind
+  ; (extra_tvs, extra_binders, real_res_kind) <- tcDataKindSig res_kind
   ; tc_rep_name <- newTyConRepName tc_name
   ; let final_tvs = (kvs' ++ tvs') `chkAppend` extra_tvs -- we may not need these
-        tycon = mkFamilyTyCon tc_name tycon_kind final_tvs
+        tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
+                              real_res_kind final_tvs
                               (resultVariableName sig)
                               (DataFamilyTyCon tc_rep_name)
                               parent NotInjective
   ; return tycon }
 
   | OpenTypeFamily <- fam_info
-  = tcTyClTyVars tc_name tvs $ \ kvs' tvs' full_kind _res_kind -> do
+  = tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> do
   { traceTc "open type family:" (ppr tc_name)
   ; checkFamFlag tc_name
   ; let all_tvs = kvs' ++ tvs'
   ; inj' <- tcInjectivity all_tvs inj
-  ; let tycon = mkFamilyTyCon tc_name full_kind all_tvs
+  ; let tycon = mkFamilyTyCon tc_name binders res_kind all_tvs
                                (resultVariableName sig) OpenSynFamilyTyCon
                                parent inj'
   ; return tycon }
@@ -759,11 +768,12 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
     do { traceTc "Closed type family:" (ppr tc_name)
          -- the variables in the header scope only over the injectivity
          -- declaration but this is not involved here
-       ; (tvs', inj', kind) <- tcTyClTyVars tc_name tvs
-                               $ \ kvs' tvs' full_kind _res_kind ->
-                               do { let all_tvs = kvs' ++ tvs'
-                                  ; inj' <- tcInjectivity all_tvs inj
-                                  ; return (all_tvs, inj', full_kind) }
+       ; (tvs', inj', binders, res_kind)
+            <- tcTyClTyVars tc_name tvs
+               $ \ kvs' tvs' binders res_kind ->
+               do { let all_tvs = kvs' ++ tvs'
+                  ; inj' <- tcInjectivity all_tvs inj
+                  ; return (all_tvs, inj', binders, res_kind) }
 
        ; checkFamFlag tc_name -- make sure we have -XTypeFamilies
 
@@ -771,14 +781,14 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
          -- but eqns might be empty in the Just case as well
        ; case mb_eqns of
            Nothing   ->
-               return $ mkFamilyTyCon tc_name kind tvs'
+               return $ mkFamilyTyCon tc_name binders res_kind tvs'
                                       (resultVariableName sig)
                                       AbstractClosedSynFamilyTyCon parent
                                       inj'
            Just eqns -> do {
 
          -- Process the equations, creating CoAxBranches
-       ; let fam_tc_shape = (tc_name, length $ hsQTvExplicit tvs, kind)
+       ; let fam_tc_shape = (tc_name, length $ hsQTvExplicit tvs, binders, res_kind)
 
        ; branches <- mapM (tcTyFamInstEqn fam_tc_shape Nothing) eqns
          -- Do not attempt to drop equations dominated by earlier
@@ -800,7 +810,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
               | null eqns = Nothing   -- mkBranchedCoAxiom fails on empty list
               | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
 
-             fam_tc = mkFamilyTyCon tc_name kind tvs' (resultVariableName sig)
+             fam_tc = mkFamilyTyCon tc_name binders res_kind tvs' (resultVariableName sig)
                       (ClosedSynFamilyTyCon mb_co_ax) parent inj'
 
          -- We check for instance validity later, when doing validity
@@ -856,27 +866,27 @@ tcInjectivity tvs (Just (L loc (InjectivityAnn _ lInjNames)))
 
 tcTySynRhs :: RecTyInfo
            -> Name
-           -> [TyVar] -> Kind -> Kind
+           -> [TyVar] -> [TyBinder] -> Kind
            -> LHsType Name -> TcM TyCon
-tcTySynRhs rec_info tc_name tvs full_kind res_kind hs_ty
+tcTySynRhs rec_info tc_name tvs binders res_kind hs_ty
   = do { env <- getLclEnv
        ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
        ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
        ; let roles = rti_roles rec_info tc_name
-             tycon = mkSynonymTyCon tc_name full_kind tvs roles rhs_ty
+             tycon = mkSynonymTyCon tc_name binders res_kind tvs roles rhs_ty
        ; return tycon }
 
 tcDataDefn :: RecTyInfo -> Name
-           -> [TyVar] -> Kind -> Kind
+           -> [TyVar] -> [TyBinder] -> Kind
            -> HsDataDefn Name -> TcM TyCon
   -- NB: not used for newtype/data instances (whether associated or not)
 tcDataDefn rec_info     -- Knot-tied; don't look at this eagerly
-           tc_name tvs tycon_kind res_kind
+           tc_name tvs tycon_binders res_kind
          (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                      , dd_ctxt = ctxt, dd_kindSig = mb_ksig
                      , dd_cons = cons })
- =  do { extra_tvs <- tcDataKindSig res_kind
+ =  do { (extra_tvs, extra_bndrs, real_res_kind) <- tcDataKindSig res_kind
        ; let final_tvs  = tvs `chkAppend` extra_tvs
              roles      = rti_roles rec_info tc_name
 
@@ -897,7 +907,8 @@ tcDataDefn rec_info     -- Knot-tied; don't look at this eagerly
              ; data_cons <- tcConDecls new_or_data tycon (final_tvs, res_ty) cons
              ; tc_rhs    <- mk_tc_rhs is_boot tycon data_cons
              ; tc_rep_nm <- newTyConRepName tc_name
-             ; return (mkAlgTyCon tc_name tycon_kind final_tvs roles
+             ; return (mkAlgTyCon tc_name (tycon_binders `chkAppend` extra_bndrs)
+                                  real_res_kind final_tvs roles
                                   (fmap unLoc cType)
                                   stupid_theta tc_rhs
                                   (VanillaAlgTyCon tc_rep_nm)
@@ -987,7 +998,7 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
     setSrcSpan loc $
     tcAddFamInstCtxt (text "default type instance") tc_name $
     do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
-       ; let shape@(fam_tc_name, fam_arity, _) = famTyConShape fam_tc
+       ; let shape@(fam_tc_name, fam_arity, _, _) = famTyConShape fam_tc
 
        -- Kind of family check
        ; ASSERT( fam_tc_name == tc_name )
@@ -1053,7 +1064,7 @@ kcTyFamInstEqn fam_tc_shape
 tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInfo -> LTyFamInstEqn Name -> TcM CoAxBranch
 -- Needs to be here, not in TcInstDcls, because closed families
 -- (typechecked here) have TyFamInstEqns
-tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_) mb_clsinfo
+tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_) mb_clsinfo
     (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
                      , tfe_pats  = pats
                      , tfe_rhs   = hs_ty }))
@@ -1130,13 +1141,15 @@ two bad things could happen:
 -}
 
 -----------------
-type FamTyConShape = (Name, Arity, Kind) -- See Note [Type-checking type patterns]
+type FamTyConShape = (Name, Arity, [TyBinder], Kind)
+  -- See Note [Type-checking type patterns]
 
 famTyConShape :: TyCon -> FamTyConShape
 famTyConShape fam_tc
   = ( tyConName fam_tc
     , length $ filterOutInvisibleTyVars fam_tc (tyConTyVars fam_tc)
-    , tyConKind fam_tc )
+    , tyConBinders fam_tc
+    , tyConResKind fam_tc )
 
 tc_fam_ty_pats :: FamTyConShape
                -> Maybe ClsInfo
@@ -1155,21 +1168,24 @@ tc_fam_ty_pats :: FamTyConShape
 -- In that case, the type variable 'a' will *already be in scope*
 -- (and, if C is poly-kinded, so will its kind parameter).
 
-tc_fam_ty_pats (name, _, kind) mb_clsinfo
+tc_fam_ty_pats (name, _, binders, res_kind) mb_clsinfo
                (HsIB { hsib_body = arg_pats, hsib_vars = tv_names })
                kind_checker
   = do { -- Kind-check and quantify
          -- See Note [Quantifying over family patterns]
-         (_, (res_kind, typats)) <- tcImplicitTKBndrs tv_names $
-         do { (res_kind, args, leftovers, n)
-                <- tcInferArgs name kind (snd <$> mb_clsinfo) arg_pats
+         (_, (insted_res_kind, typats)) <- tcImplicitTKBndrs tv_names $
+         do { (insting_subst, _leftover_binders, args, leftovers, n)
+                <- tcInferArgs name binders (snd <$> mb_clsinfo) arg_pats
             ; case leftovers of
                 hs_ty:_ -> addErrTc $ too_many_args hs_ty n
                 _       -> return ()
-            ; kind_checker res_kind
-            ; return ((res_kind, args), emptyVarSet) }
+              -- don't worry about leftover_binders; TcValidity catches them
+
+            ; let insted_res_kind = substTyUnchecked insting_subst res_kind
+            ; kind_checker insted_res_kind
+            ; return ((insted_res_kind, args), emptyVarSet) }
 
-       ; return (typats, res_kind) }
+       ; return (typats, insted_res_kind) }
   where
     too_many_args hs_ty n
       = hang (text "Too many parameters to" <+> ppr name <> colon)
@@ -1186,7 +1202,7 @@ tcFamTyPats :: FamTyConShape
                 -> [TcType]          -- Kind and type arguments
                 -> Kind -> TcM a)  -- NB: You can use solveEqualities here.
             -> TcM a
-tcFamTyPats fam_shape@(name,_,_) mb_clsinfo pats kind_checker thing_inside
+tcFamTyPats fam_shape@(name,_,_,_) mb_clsinfo pats kind_checker thing_inside
   = do { (typats, res_kind)
             <- solveEqualities $  -- See Note [Constraints in patterns]
                tc_fam_ty_pats fam_shape mb_clsinfo pats kind_checker
index 00b3a0f..972cbae 100644 (file)
@@ -22,7 +22,7 @@ module TcType (
   -- Types
   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
   TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
-  TcKind, TcCoVar, TcTyCoVar, TcTyBinder,
+  TcKind, TcCoVar, TcTyCoVar, TcTyBinder, TcTyCon,
 
   ExpType(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
 
@@ -121,7 +121,7 @@ module TcType (
   --------------------------------
   -- Rexported from Kind
   Kind, typeKind,
-  unliftedTypeKind, liftedTypeKind,
+  liftedTypeKind,
   constraintKind,
   isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,
 
@@ -140,7 +140,7 @@ module TcType (
   mkClassPred,
   isDictLikeTy,
   tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy,
-  isLevityVar, isLevityPolymorphic, isLevityPolymorphic_maybe,
+  isRuntimeRepVar, isRuntimeRepPolymorphic,
   isVisibleBinder, isInvisibleBinder,
 
   -- Type substitutions
@@ -269,6 +269,7 @@ type TcTyCoVar = Var    -- Either a TcTyVar or a CoVar
         -- a cannot occur inside a MutTyVar in T; that is,
         -- T is "flattened" before quantifying over a
 type TcTyBinder = TyBinder
+type TcTyCon = TyCon   -- these can be the TcTyCon constructor
 
 -- These types do not have boxy type variables in them
 type TcPredType     = PredType
@@ -1375,9 +1376,8 @@ tc_eq_type view_fun orig_ty1 orig_ty2 = go Visible orig_env orig_ty1 orig_ty2
        -- the repeat Visible is necessary because tycons can legitimately
        -- be oversaturated
       where
-        k          = tyConKind tc
-        (bndrs, _) = splitPiTys k
-        viss       = map binderVisibility bndrs
+        bndrs = tyConBinders tc
+        viss  = map binderVisibility bndrs
 
     check :: VisibilityFlag -> Bool -> Maybe VisibilityFlag
     check _   True  = Nothing
index e7fb85f..e6a6c7e 100644 (file)
@@ -100,7 +100,8 @@ typeNatExpTyCon = mkTypeNatFunTyCon2 name
 typeNatLeqTyCon :: TyCon
 typeNatLeqTyCon =
   mkFamilyTyCon name
-    (mkFunTys [ typeNatKind, typeNatKind ] boolTy)
+    (map mkAnonBinder [ typeNatKind, typeNatKind ])
+    boolTy
     (mkTemplateTyVars [ typeNatKind, typeNatKind ])
     Nothing
     (BuiltInSynFamTyCon ops)
@@ -119,7 +120,8 @@ typeNatLeqTyCon =
 typeNatCmpTyCon :: TyCon
 typeNatCmpTyCon =
   mkFamilyTyCon name
-    (mkFunTys [ typeNatKind, typeNatKind ] orderingKind)
+    (map mkAnonBinder [ typeNatKind, typeNatKind ])
+    orderingKind
     (mkTemplateTyVars [ typeNatKind, typeNatKind ])
     Nothing
     (BuiltInSynFamTyCon ops)
@@ -138,7 +140,8 @@ typeNatCmpTyCon =
 typeSymbolCmpTyCon :: TyCon
 typeSymbolCmpTyCon =
   mkFamilyTyCon name
-    (mkFunTys [ typeSymbolKind, typeSymbolKind ] orderingKind)
+    (map mkAnonBinder [ typeSymbolKind, typeSymbolKind ])
+    orderingKind
     (mkTemplateTyVars [ typeSymbolKind, typeSymbolKind ])
     Nothing
     (BuiltInSynFamTyCon ops)
@@ -162,7 +165,8 @@ typeSymbolCmpTyCon =
 mkTypeNatFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
 mkTypeNatFunTyCon2 op tcb =
   mkFamilyTyCon op
-    (mkFunTys [ typeNatKind, typeNatKind ] typeNatKind)
+    (map mkAnonBinder [ typeNatKind, typeNatKind ])
+    typeNatKind
     (mkTemplateTyVars [ typeNatKind, typeNatKind ])
     Nothing
     (BuiltInSynFamTyCon tcb)
index e25ff21..77651c8 100644 (file)
@@ -381,16 +381,9 @@ matchExpectedTyConApp tc orig_ty
     -- because that'll make types that are utterly ill-kinded.
     -- This happened in Trac #7368
     defer
-      = ASSERT2( classifiesTypeWithValues res_kind, ppr tc )
-        do { (k_subst, kvs') <- newMetaTyVars kvs
-           ; let arg_kinds' = substTys k_subst arg_kinds
-                 kappa_tys  = mkTyVarTys kvs'
-           ; tau_tys <- mapM newFlexiTyVarTy arg_kinds'
-           ; co <- unifyType noThing (mkTyConApp tc (kappa_tys ++ tau_tys)) orig_ty
-           ; return (co, kappa_tys ++ tau_tys) }
-
-    (bndrs, res_kind)     = splitPiTys (tyConKind tc)
-    (kvs, arg_kinds)      = partitionBinders bndrs
+      = do { (_subst, args) <- tcInstBinders (tyConBinders tc)
+           ; co <- unifyType noThing (mkTyConApp tc args) orig_ty
+           ; return (co, args) }
 
 ----------------------
 matchExpectedAppTy :: TcRhoType                         -- orig_ty
@@ -1181,13 +1174,13 @@ uType origin t_or_k orig_ty1 orig_ty2
         do { cos <- zipWith3M (uType origin) t_or_ks tys1 tys2
            ; return $ mkTyConAppCo Nominal tc1 cos }
       where
-        (bndrs, _) = splitPiTys (tyConKind tc1)
+        bndrs      = tyConBinders tc1
         t_or_ks    = case t_or_k of
                        KindLevel -> repeat KindLevel
                        TypeLevel -> map (\bndr -> if isNamedBinder bndr
                                                   then KindLevel
-                                                  else TypeLevel)
-                                        bndrs
+                                                  else TypeLevel) bndrs ++
+                                    repeat TypeLevel
 
     go (LitTy m) ty@(LitTy n)
       | m == n
index 56cb348..319c15d 100644 (file)
@@ -945,7 +945,7 @@ tyConArityErr tc tks
 
     -- tc_type_arity = number of *type* args expected
     -- tc_type_args  = number of *type* args encountered
-    tc_type_arity = count isVisibleBinder $ fst $ splitPiTys (tyConKind tc)
+    tc_type_arity = count isVisibleBinder $ tyConBinders tc
     tc_type_args  = length vis_tks
 
 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
@@ -1583,7 +1583,7 @@ checkValidFamPats mb_clsinfo fam_tc tvs cvs ty_pats
        ; checkConsistentFamInst mb_clsinfo fam_tc tvs ty_pats }
   where
      fam_arity = tyConArity fam_tc
-     fam_bndrs = take fam_arity $ fst $ splitPiTys (tyConKind fam_tc)
+     fam_bndrs = tyConBinders fam_tc
 
 
 checkValidTypePat :: Type -> TcM ()
index 1ce0bbf..ac7fc58 100644 (file)
@@ -14,7 +14,7 @@ module Kind (
 
         classifiesTypeWithValues,
         isStarKind, isStarKindSynonymTyCon,
-        isLevityPolymorphic, isLevityPolymorphic_maybe
+        isRuntimeRepPolymorphic
        ) where
 
 #include "HsVersions.h"
@@ -23,9 +23,8 @@ import {-# SOURCE #-} Type       ( typeKind, coreViewOneStarKind )
 
 import TyCoRep
 import TyCon
-import Var
+import VarSet ( isEmptyVarSet )
 import PrelNames
-import Data.Maybe
 import Util  ( (<&&>) )
 
 {-
@@ -78,19 +77,11 @@ returnsTyCon _  _                  = False
 returnsConstraintKind :: Kind -> Bool
 returnsConstraintKind = returnsTyCon constraintKindTyConKey
 
--- | Tests whether the given type looks like "TYPE v", where v is a variable.
-isLevityPolymorphic :: Kind -> Bool
-isLevityPolymorphic = isJust . isLevityPolymorphic_maybe
-
--- | Retrieves a levity variable in the given kind, if the kind is of the
--- form "TYPE v".
-isLevityPolymorphic_maybe :: Kind -> Maybe TyVar
-isLevityPolymorphic_maybe k
-  | Just k' <- coreViewOneStarKind k = isLevityPolymorphic_maybe k'
-isLevityPolymorphic_maybe (TyConApp tc [TyVarTy v])
-  | tc `hasKey` tYPETyConKey
-  = Just v
-isLevityPolymorphic_maybe _ = Nothing
+-- | Tests whether the given type (which should look like "TYPE ...") has any
+-- free variables
+isRuntimeRepPolymorphic :: Kind -> Bool
+isRuntimeRepPolymorphic k
+  = not $ isEmptyVarSet $ tyCoVarsOfType k
 
 --------------------------------------------
 --            Kinding for arrow (->)
@@ -98,7 +89,7 @@ isLevityPolymorphic_maybe _ = Nothing
 --     arg -> res
 
 okArrowArgKind, okArrowResultKind :: Kind -> Bool
-okArrowArgKind = classifiesTypeWithValues <&&> (not . isLevityPolymorphic)
+okArrowArgKind = classifiesTypeWithValues <&&> (not . isRuntimeRepPolymorphic)
 okArrowResultKind = classifiesTypeWithValues
 
 -----------------------------------------
@@ -119,8 +110,9 @@ classifiesTypeWithValues _ = False
 -- | Is this kind equivalent to *?
 isStarKind :: Kind -> Bool
 isStarKind k | Just k' <- coreViewOneStarKind k = isStarKind k'
-isStarKind (TyConApp tc [TyConApp l []]) = tc `hasKey` tYPETyConKey
-                                        && l `hasKey` liftedDataConKey
+isStarKind (TyConApp tc [TyConApp ptr_rep []])
+  =  tc      `hasKey` tYPETyConKey
+  && ptr_rep `hasKey` ptrRepLiftedDataConKey
 isStarKind _ = False
                               -- See Note [Kind Constraint and kind *]
 
index ad583ea..5624730 100644 (file)
@@ -37,10 +37,10 @@ module TyCoRep (
 
         -- Functions over types
         mkTyConTy, mkTyVarTy, mkTyVarTys,
-        mkFunTy, mkFunTys,
+        mkFunTy, mkFunTys, mkForAllTys,
         isLiftedTypeKind, isUnliftedTypeKind,
-        isCoercionType, isLevityTy, isLevityVar,
-        isLevityKindedTy, dropLevityArgs,
+        isCoercionType, isRuntimeRepTy, isRuntimeRepVar,
+        isRuntimeRepKindedTy, dropRuntimeRepArgs,
         sameVis,
 
         -- Functions over binders
@@ -465,6 +465,10 @@ mkFunTy arg res = ForAllTy (Anon arg) res
 mkFunTys :: [Type] -> Type -> Type
 mkFunTys tys ty = foldr mkFunTy ty tys
 
+-- | Wraps foralls over the type using the provided 'TyVar's from left to right
+mkForAllTys :: [TyBinder] -> Type -> Type
+mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
+
 -- | Does this type classify a core Coercion?
 isCoercionType :: Type -> Bool
 isCoercionType (TyConApp tc tys)
@@ -514,39 +518,47 @@ mkTyConTy tycon = TyConApp tycon []
 Some basic functions, put here to break loops eg with the pretty printer
 -}
 
+-- | This version considers Constraint to be distinct from *.
 isLiftedTypeKind :: Kind -> Bool
 isLiftedTypeKind ki | Just ki' <- coreView ki = isLiftedTypeKind ki'
-isLiftedTypeKind (TyConApp tc [TyConApp lev []])
-  = tc `hasKey` tYPETyConKey && lev `hasKey` liftedDataConKey
+isLiftedTypeKind (TyConApp tc [TyConApp ptr_rep []])
+  =  tc      `hasKey` tYPETyConKey
+  && ptr_rep `hasKey` ptrRepLiftedDataConKey
 isLiftedTypeKind _                = False
 
 isUnliftedTypeKind :: Kind -> Bool
 isUnliftedTypeKind ki | Just ki' <- coreView ki = isUnliftedTypeKind ki'
-isUnliftedTypeKind (TyConApp tc [TyConApp lev []])
-  = tc `hasKey` tYPETyConKey && lev `hasKey` unliftedDataConKey
+isUnliftedTypeKind (TyConApp tc [TyConApp ptr_rep []])
+  | tc       `hasKey` tYPETyConKey
+  , ptr_rep  `hasKey` ptrRepLiftedDataConKey
+  = False
+isUnliftedTypeKind (TyConApp tc [arg])
+  = tc `hasKey` tYPETyConKey && isEmptyVarSet (tyCoVarsOfType arg)
+      -- all other possibilities are unlifted
 isUnliftedTypeKind _ = False
 
--- | Is this the type 'Levity'?
-isLevityTy :: Type -> Bool
-isLevityTy ty | Just ty' <- coreView ty = isLevityTy ty'
-isLevityTy (TyConApp tc []) = tc `hasKey` levityTyConKey
-isLevityTy _ = False
+-- | Is this the type 'RuntimeRep'?
+isRuntimeRepTy :: Type -> Bool
+isRuntimeRepTy ty | Just ty' <- coreView ty = isRuntimeRepTy ty'
+isRuntimeRepTy (TyConApp tc []) = tc `hasKey` runtimeRepTyConKey
+isRuntimeRepTy _ = False
 
--- | Is this a type of kind Levity? (e.g. Lifted, Unlifted)
-isLevityKindedTy :: Type -> Bool
-isLevityKindedTy = isLevityTy . typeKind
+-- | Is this a type of kind RuntimeRep? (e.g. PtrRep)
+isRuntimeRepKindedTy :: Type -> Bool
+isRuntimeRepKindedTy = isRuntimeRepTy . typeKind
 
--- | Is a tyvar of type 'Levity'?
-isLevityVar :: TyVar -> Bool
-isLevityVar = isLevityTy . tyVarKind
+-- | Is a tyvar of type 'RuntimeRep'?
+isRuntimeRepVar :: TyVar -> Bool
+isRuntimeRepVar = isRuntimeRepTy . tyVarKind
 
--- | Drops prefix of Levity constructors in 'TyConApp's. Useful for e.g.
--- dropping 'Lifted and 'Unlifted arguments of unboxed tuple TyCon applications:
+-- | Drops prefix of RuntimeRep constructors in 'TyConApp's. Useful for e.g.
+-- dropping 'PtrRep arguments of unboxed tuple TyCon applications:
 --
---   dropLevityArgs ['Lifted, 'Unlifted, String, Int#] == [String, Int#]
+--   dropRuntimeRepArgs [ 'PtrRepLifted, 'PtrRepUnlifted
+--                      , String, Int# ] == [String, Int#]
 --
-dropLevityArgs :: [Type] -> [Type]
-dropLevityArgs = dropWhile isLevityKindedTy
+dropRuntimeRepArgs :: [Type] -> [Type]
+dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy
 
 {-
 %************************************************************************
@@ -2657,11 +2669,14 @@ pprTyTcApp p tc tys
   = text "(TypeError ...)"   -- Suppress detail unles you _really_ want to see
 
   | tc `hasKey` tYPETyConKey
-  , [TyConApp lev_tc []] <- tys
-  = if | lev_tc `hasKey` liftedDataConKey   ->
-           unicodeSyntax (char '★') (char '*')
-       | lev_tc `hasKey` unliftedDataConKey -> char '#'
-       | otherwise                          -> ppr_deflt
+  , [TyConApp ptr_rep []] <- tys
+  , ptr_rep `hasKey` ptrRepLiftedDataConKey
+  = unicodeSyntax (char '★') (char '*')
+
+  | tc `hasKey` tYPETyConKey
+  , [TyConApp ptr_rep []] <- tys
+  , ptr_rep `hasKey` ptrRepUnliftedDataConKey
+  = char '#'
 
   | otherwise
   = ppr_deflt
@@ -2669,27 +2684,33 @@ pprTyTcApp p tc tys
     ppr_deflt = pprTcAppTy p ppr_type tc tys
 
 pprTcAppTy :: TyPrec -> (TyPrec -> Type -> SDoc) -> TyCon -> [Type] -> SDoc
-pprTcAppTy = pprTcApp id
+pprTcAppTy p pp tc tys
+  = getPprStyle $ \style -> pprTcApp style id p pp tc tys
 
 pprTcAppCo :: TyPrec -> (TyPrec -> Coercion -> SDoc)
            -> TyCon -> [Coercion] -> SDoc
-pprTcAppCo = pprTcApp (pFst . coercionKind)
+pprTcAppCo p pp tc cos
+  = getPprStyle $ \style ->
+    pprTcApp style (pFst . coercionKind) p pp tc cos
 
-pprTcApp :: (a -> Type) -> TyPrec -> (TyPrec -> a -> SDoc) -> TyCon -> [a] -> SDoc
+pprTcApp :: PprStyle
+         -> (a -> Type) -> TyPrec -> (TyPrec -> a -> SDoc) -> TyCon -> [a] -> SDoc
 -- Used for both types and coercions, hence polymorphism
-pprTcApp _ _ pp tc [ty]
+pprTcApp _ _ pp tc [ty]
   | tc `hasKey` listTyConKey = pprPromotionQuote tc <> brackets   (pp TopPrec ty)
   | tc `hasKey` parrTyConKey = pprPromotionQuote tc <> paBrackets (pp TopPrec ty)
 
-pprTcApp to_type p pp tc tys
-  | Just sort <- tyConTuple_maybe tc
+pprTcApp style to_type p pp tc tys
+  | not (debugStyle style)
+  , Just sort <- tyConTuple_maybe tc
   , let arity = tyConArity tc
   , arity == length tys
   , let num_to_drop = case sort of UnboxedTuple -> arity `div` 2
                                    _            -> 0
   = pprTupleApp p pp tc sort (drop num_to_drop tys)
 
-  | Just dc <- isPromotedDataCon_maybe tc
+  | not (debugStyle style)
+  , Just dc <- isPromotedDataCon_maybe tc
   , let dc_tc = dataConTyCon dc
   , Just tup_sort <- tyConTuple_maybe dc_tc
   , let arity = tyConArity dc_tc    -- E.g. 3 for (,,) k1 k2 k3 t1 t2 t3
@@ -2700,7 +2721,6 @@ pprTcApp to_type p pp tc tys
 
   | otherwise
   = sdocWithDynFlags $ \dflags ->
-    getPprStyle $ \style ->
     pprTcApp_help to_type p pp tc tys dflags style
   where
 
index 76a5abf..5236bcc 100644 (file)
@@ -11,6 +11,8 @@ data LeftOrRight
 data UnivCoProvenance
 data TCvSubst
 
+mkForAllTys :: [TyBinder] -> Type -> Type
+
 type PredType = Type
 type Kind = Type
 type ThetaType = [PredType]
index e6fe351..5d01732 100644 (file)
@@ -15,6 +15,7 @@ module TyCon(
         AlgTyConRhs(..), visibleDataCons,
         AlgTyConFlav(..), isNoParent,
         FamTyConFlav(..), Role(..), Injectivity(..),
+        RuntimeRepInfo(..),
 
         -- ** Field labels
         tyConFieldLabels, tyConFieldLabelEnv,
@@ -82,6 +83,8 @@ module TyCon(
         newTyConRhs, newTyConEtadArity, newTyConEtadRhs,
         unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe,
         algTcFields,
+        tyConRuntimeRepInfo,
+        tyConBinders, tyConResKind,
 
         -- ** Manipulating TyCons
         expandSynTyCon_maybe,
@@ -96,7 +99,7 @@ module TyCon(
 
         -- * Primitive representations of Types
         PrimRep(..), PrimElemRep(..),
-        tyConPrimRep, isVoidRep, isGcPtrRep,
+        isVoidRep, isGcPtrRep,
         primRepSizeW, primElemRepSizeB,
         primRepIsFloat,
 
@@ -107,7 +110,9 @@ module TyCon(
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} TyCoRep ( Kind, Type, PredType )
+import {-# SOURCE #-} TyCoRep ( Kind, Type, PredType, TyBinder, mkForAllTys )
+import {-# SOURCE #-} TysWiredIn  ( runtimeRepTyCon, constraintKind
+                                  , vecCountTyCon, vecElemTyCon, liftedTypeKind )
 import {-# SOURCE #-} DataCon ( DataCon, dataConExTyVars, dataConFieldLabels )
 
 import Binary
@@ -127,6 +132,7 @@ import FieldLabel
 import Constants
 import Util
 import Unique( tyConRepNameUnique, dataConRepNameUnique )
+import UniqSet
 import Module
 
 import qualified Data.Data as Data
@@ -322,12 +328,13 @@ it's worth noting that (~#)'s parameters are at role N. Promoted data
 constructors' type arguments are at role R. All kind arguments are at role
 N.
 
-Note [Unboxed tuple levity vars]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The contents of an unboxed tuple may be boxed or unboxed. Accordingly,
-the kind of the unboxed tuple constructor is sort-polymorphic. For example,
+Note [Unboxed tuple RuntimeRep vars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The contents of an unboxed tuple may have any representation. Accordingly,
+the kind of the unboxed tuple constructor is runtime-representation
+polymorphic. For example,
 
-   (#,#) :: forall (v :: Levity) (w :: Levity). TYPE v -> TYPE w -> #
+   (#,#) :: forall (q :: RuntimeRep) (r :: RuntimeRep). TYPE q -> TYPE r -> #
 
 These extra tyvars (v and w) cause some delicate processing around tuples,
 where we used to be able to assume that the tycon arity and the
@@ -390,6 +397,13 @@ data TyCon
 
         tyConName   :: Name,     -- ^ Name of the constructor
 
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+                                    -- length tyConBinders == tyConArity.
+                                    -- This is a cached value and is redundant with
+                                    -- the tyConKind.
+
+        tyConResKind :: Kind,       -- ^ Cached result kind
+
         tyConKind   :: Kind,     -- ^ Kind of this TyCon (full kind, not just
                                  -- the return kind)
 
@@ -420,6 +434,13 @@ data TyCon
 
         tyConName    :: Name,    -- ^ Name of the constructor
 
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+                                    -- length tyConBinders == tyConArity.
+                                    -- This is a cached value and is redundant with
+                                    -- the tyConKind.
+
+        tyConResKind :: Kind,       -- ^ Cached result kind
+
         tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
                                  -- the return kind)
 
@@ -483,6 +504,13 @@ data TyCon
 
         tyConName    :: Name,    -- ^ Name of the constructor
 
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+                                    -- length tyConBinders == tyConArity.
+                                    -- This is a cached value and is redundant with
+                                    -- the tyConKind.
+
+        tyConResKind :: Kind,     -- ^ Cached result kind.
+
         tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
                                  -- the return kind)
 
@@ -511,6 +539,13 @@ data TyCon
 
         tyConName    :: Name,    -- ^ Name of the constructor
 
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+                                    -- length tyConBinders == tyConArity.
+                                    -- This is a cached value and is redundant with
+                                    -- the tyConKind.
+
+        tyConResKind :: Kind,     -- ^ Cached result kind
+
         tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
                                  -- the return kind)
 
@@ -558,6 +593,13 @@ data TyCon
 
         tyConName     :: Name,   -- ^ Name of the constructor
 
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+                                    -- length tyConBinders == tyConArity.
+                                    -- This is a cached value and is redundant with
+                                    -- the tyConKind.
+
+        tyConResKind   :: Kind,      -- ^ Cached result kind
+
         tyConKind     :: Kind,   -- ^ Kind of this TyCon (full kind, not just
                                  -- the return kind)
 
@@ -569,11 +611,6 @@ data TyCon
                                  -- This list has the same length as tyConTyVars
                                  -- See also Note [TyCon Role signatures]
 
-        primTyConRep  :: PrimRep,-- ^ Many primitive tycons are unboxed, but
-                                 -- some are boxed (represented by
-                                 -- pointers). This 'PrimRep' holds that
-                                 -- information.  Only relevant if tyConKind = #
-
         isUnlifted   :: Bool,    -- ^ Most primitive tycons are unlifted (may
                                  -- not contain bottom) but other are lifted,
                                  -- e.g. @RealWorld@
@@ -585,13 +622,19 @@ data TyCon
 
   -- | Represents promoted data constructor.
   | PromotedDataCon {          -- See Note [Promoted data constructors]
-        tyConUnique :: Unique, -- ^ Same Unique as the data constructor
-        tyConName   :: Name,   -- ^ Same Name as the data constructor
-        tyConArity  :: Arity,
-        tyConKind   :: Kind,   -- ^ Translated type of the data constructor
-        tcRoles     :: [Role], -- ^ Roles: N for kind vars, R for type vars
-        dataCon     :: DataCon,-- ^ Corresponding data constructor
-        tcRepName   :: TyConRepName
+        tyConUnique   :: Unique, -- ^ Same Unique as the data constructor
+        tyConName     :: Name,   -- ^ Same Name as the data constructor
+        tyConArity    :: Arity,
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+                                    -- length tyConBinders == tyConArity.
+                                    -- This is a cached value and is redundant with
+                                    -- the tyConKind.
+        tyConResKind   :: Kind,   -- ^ Cached result kind
+        tyConKind     :: Kind,   -- ^ Type of the data constructor
+        tcRoles       :: [Role], -- ^ Roles: N for kind vars, R for type vars
+        dataCon       :: DataCon,-- ^ Corresponding data constructor
+        tcRepName     :: TyConRepName,
+        promDcRepInfo :: RuntimeRepInfo  -- ^ See comments with 'RuntimeRepInfo'
     }
 
   -- | These exist only during a recursive type/class type-checking knot.
@@ -600,6 +643,12 @@ data TyCon
       tyConName   :: Name,
       tyConUnsat  :: Bool,  -- ^ can this tycon be unsaturated?
       tyConArity  :: Arity,
+      tyConBinders :: [TyBinder],   -- ^ The TyBinders for this TyCon's kind.
+                                    -- length tyConBinders == tyConArity.
+                                    -- This is a cached value and is redundant with
+                                    -- the tyConKind.
+      tyConResKind :: Kind,          -- ^ Cached result kind
+
       tyConKind   :: Kind
       }
   deriving Typeable
@@ -668,6 +717,19 @@ data AlgTyConRhs
                              -- again check Trac #1072.
     }
 
+-- | Some promoted datacons signify extra info relevant to GHC. For example,
+-- the @IntRep@ constructor of @RuntimeRep@ corresponds to the 'IntRep'
+-- constructor of 'PrimRep'. This data structure allows us to store this
+-- information right in the 'TyCon'. The other approach would be to look
+-- up things like @RuntimeRep@'s @PrimRep@ by known-key every time.
+data RuntimeRepInfo
+  = NoRRI       -- ^ an ordinary promoted data con
+  | RuntimeRep ([Type] -> PrimRep)
+      -- ^ A constructor of @RuntimeRep@. The argument to the function should
+      -- be the list of arguments to the promoted datacon.
+  | VecCount Int         -- ^ A constructor of @VecCount@
+  | VecElem PrimElemRep  -- ^ A constructor of @VecElem@
+
 -- | Extract those 'DataCon's that we are able to learn about.  Note
 -- that visibility in this sense does not correspond to visibility in
 -- the context of any particular user program!
@@ -1132,14 +1194,16 @@ So we compromise, and move their Kind calculation to the call site.
 -- | Given the name of the function type constructor and it's kind, create the
 -- corresponding 'TyCon'. It is reccomended to use 'TyCoRep.funTyCon' if you want
 -- this functionality
-mkFunTyCon :: Name -> Kind -> Name -> TyCon
-mkFunTyCon name kind rep_nm
+mkFunTyCon :: Name -> [TyBinder] -> Name -> TyCon
+mkFunTyCon name binders rep_nm
   = FunTyCon {
-        tyConUnique = nameUnique name,
-        tyConName   = name,
-        tyConKind   = kind,
-        tyConArity  = 2,
-        tcRepName   = rep_nm
+        tyConUnique  = nameUnique name,
+        tyConName    = name,
+        tyConBinders = binders,
+        tyConResKind = liftedTypeKind,
+        tyConKind    = mkForAllTys binders liftedTypeKind,
+        tyConArity   = 2,
+        tcRepName    = rep_nm
     }
 
 -- | This is the making of an algebraic 'TyCon'. Notably, you have to
@@ -1147,7 +1211,8 @@ mkFunTyCon name kind rep_nm
 -- type constructor - you can get hold of it easily (see Generics
 -- module)
 mkAlgTyCon :: Name
-           -> Kind              -- ^ Kind of the resulting 'TyCon'
+           -> [TyBinder]        -- ^ Binders of the resulting 'TyCon'
+           -> Kind              -- ^ Result kind
            -> [TyVar]           -- ^ 'TyVar's scoped over: see 'tyConTyVars'.
                                 --   Arity is inferred from the length of this
                                 --   list
@@ -1161,11 +1226,13 @@ mkAlgTyCon :: Name
            -> RecFlag           -- ^ Is the 'TyCon' recursive?
            -> Bool              -- ^ Was the 'TyCon' declared with GADT syntax?
            -> TyCon
-mkAlgTyCon name kind tyvars roles cType stupid rhs parent is_rec gadt_syn
+mkAlgTyCon name binders res_kind tyvars roles cType stupid rhs parent is_rec gadt_syn
   = AlgTyCon {
         tyConName        = name,
         tyConUnique      = nameUnique name,
-        tyConKind        = kind,
+        tyConBinders     = binders,
+        tyConResKind     = res_kind,
+        tyConKind        = mkForAllTys binders res_kind,
         tyConArity       = length tyvars,
         tyConTyVars      = tyvars,
         tcRoles          = roles,
@@ -1179,26 +1246,30 @@ mkAlgTyCon name kind tyvars roles cType stupid rhs parent is_rec gadt_syn
     }
 
 -- | Simpler specialization of 'mkAlgTyCon' for classes
-mkClassTyCon :: Name -> Kind -> [TyVar] -> [Role] -> AlgTyConRhs -> Class
+mkClassTyCon :: Name -> [TyBinder]
+             -> [TyVar] -> [Role] -> AlgTyConRhs -> Class
              -> RecFlag -> Name -> TyCon
-mkClassTyCon name kind tyvars roles rhs clas is_rec tc_rep_name
-  = mkAlgTyCon name kind tyvars roles Nothing [] rhs
+mkClassTyCon name binders tyvars roles rhs clas is_rec tc_rep_name
+  = mkAlgTyCon name binders constraintKind tyvars roles Nothing [] rhs
                (ClassTyCon clas tc_rep_name)
                is_rec False
 
 mkTupleTyCon :: Name
-             -> Kind    -- ^ Kind of the resulting 'TyCon'
+             -> [TyBinder]
+             -> Kind    -- ^ Result kind of the 'TyCon'
              -> Arity   -- ^ Arity of the tuple
              -> [TyVar] -- ^ 'TyVar's scoped over: see 'tyConTyVars'
              -> DataCon
              -> TupleSort    -- ^ Whether the tuple is boxed or unboxed
              -> AlgTyConFlav
              -> TyCon
-mkTupleTyCon name kind arity tyvars con sort parent
+mkTupleTyCon name binders res_kind arity tyvars con sort parent
   = AlgTyCon {
         tyConName        = name,
         tyConUnique      = nameUnique name,
-        tyConKind        = kind,
+        tyConBinders     = binders,
+        tyConResKind     = res_kind,
+        tyConKind        = mkForAllTys binders res_kind,
         tyConArity       = arity,
         tyConTyVars      = tyvars,
         tcRoles          = replicate arity Representational,
@@ -1218,75 +1289,91 @@ mkTupleTyCon name kind arity tyvars con sort parent
 -- TcErrors sometimes calls typeKind.
 -- See also Note [Kind checking recursive type and class declarations]
 -- in TcTyClsDecls.
-mkTcTyCon :: Name -> Kind -> Bool -- ^ Can this be unsaturated?
-          -> Arity
+mkTcTyCon :: Name -> [TyBinder] -> Kind  -- ^ /result/ kind only
+          -> Bool  -- ^ Can this be unsaturated?
           -> TyCon
-mkTcTyCon name kind unsat arity
+mkTcTyCon name binders res_kind unsat
   = TcTyCon { tyConUnique  = getUnique name
             , tyConName    = name
-            , tyConKind    = kind
+            , tyConBinders = binders
+            , tyConResKind = res_kind
+            , tyConKind    = mkForAllTys binders res_kind
             , tyConUnsat   = unsat
-            , tyConArity   = arity }
+            , tyConArity   = length binders }
 
 -- | Create an unlifted primitive 'TyCon', such as @Int#@
-mkPrimTyCon :: Name  -> Kind -> [Role] -> PrimRep -> TyCon
-mkPrimTyCon name kind roles rep
-  = mkPrimTyCon' name kind roles rep True (Just $ mkPrelTyConRepName name)
+mkPrimTyCon :: Name -> [TyBinder]
+            -> Kind   -- ^ /result/ kind
+            -> [Role] -> TyCon
+mkPrimTyCon name binders res_kind roles
+  = mkPrimTyCon' name binders res_kind roles True (Just $ mkPrelTyConRepName name)
 
 -- | Kind constructors
-mkKindTyCon :: Name -> Kind -> [Role] -> Name -> TyCon
-mkKindTyCon name kind roles rep_nm
+mkKindTyCon :: Name -> [TyBinder]
+            -> Kind  -- ^ /result/ kind
+            -> [Role] -> Name -> TyCon
+mkKindTyCon name binders res_kind roles rep_nm
   = tc
   where
-    tc = mkPrimTyCon' name kind roles PtrRep False (Just rep_nm)
-      -- PtrRep because kinds have kind *.
+    tc = mkPrimTyCon' name binders res_kind roles False (Just rep_nm)
 
 -- | Create a lifted primitive 'TyCon' such as @RealWorld@
-mkLiftedPrimTyCon :: Name  -> Kind -> [Role] -> PrimRep -> TyCon
-mkLiftedPrimTyCon name kind roles rep
-  = mkPrimTyCon' name kind roles rep False Nothing
-
-mkPrimTyCon' :: Name  -> Kind -> [Role] -> PrimRep
+mkLiftedPrimTyCon :: Name -> [TyBinder]
+                  -> Kind   -- ^ /result/ kind
+                  -> [Role] -> TyCon
+mkLiftedPrimTyCon name binders res_kind roles
+  = mkPrimTyCon' name binders res_kind roles False Nothing
+
+mkPrimTyCon' :: Name -> [TyBinder]
+             -> Kind    -- ^ /result/ kind
+             -> [Role]
              -> Bool -> Maybe TyConRepName -> TyCon
-mkPrimTyCon' name kind roles rep is_unlifted rep_nm
+mkPrimTyCon' name binders res_kind roles is_unlifted rep_nm
   = PrimTyCon {
         tyConName    = name,
         tyConUnique  = nameUnique name,
-        tyConKind    = kind,
+        tyConBinders = binders,
+        tyConResKind = res_kind,
+        tyConKind    = mkForAllTys binders res_kind,
         tyConArity   = length roles,
         tcRoles      = roles,
-        primTyConRep = rep,
         isUnlifted   = is_unlifted,
         primRepName  = rep_nm
     }
 
 -- | Create a type synonym 'TyCon'
-mkSynonymTyCon :: Name -> Kind -> [TyVar] -> [Role] -> Type -> TyCon
-mkSynonymTyCon name kind tyvars roles rhs
+mkSynonymTyCon :: Name -> [TyBinder] -> Kind   -- ^ /result/ kind
+               -> [TyVar] -> [Role] -> Type -> TyCon
+mkSynonymTyCon name binders res_kind tyvars roles rhs
   = SynonymTyCon {
-        tyConName   = name,
-        tyConUnique = nameUnique name,
-        tyConKind   = kind,
-        tyConArity  = length tyvars,
-        tyConTyVars = tyvars,
-        tcRoles     = roles,
-        synTcRhs    = rhs
+        tyConName    = name,
+        tyConUnique  = nameUnique name,
+        tyConBinders = binders,
+        tyConResKind = res_kind,
+        tyConKind    = mkForAllTys binders res_kind,
+        tyConArity   = length tyvars,
+        tyConTyVars  = tyvars,
+        tcRoles      = roles,
+        synTcRhs     = rhs
     }
 
 -- | Create a type family 'TyCon'
-mkFamilyTyCon:: Name -> Kind -> [TyVar] -> Maybe Name -> FamTyConFlav
-             -> Maybe Class -> Injectivity -> TyCon
-mkFamilyTyCon name kind tyvars resVar flav parent inj
+mkFamilyTyCon :: Name -> [TyBinder] -> Kind  -- ^ /result/ kind
+              -> [TyVar] -> Maybe Name -> FamTyConFlav
+              -> Maybe Class -> Injectivity -> TyCon
+mkFamilyTyCon name binders res_kind tyvars resVar flav parent inj
   = FamilyTyCon
-      { tyConUnique = nameUnique name
-      , tyConName   = name
-      , tyConKind   = kind
-      , tyConArity  = length tyvars
-      , tyConTyVars = tyvars
-      , famTcResVar = resVar
-      , famTcFlav   = flav
-      , famTcParent = parent
-      , famTcInj    = inj
+      { tyConUnique  = nameUnique name
+      , tyConName    = name
+      , tyConBinders = binders
+      , tyConResKind = res_kind
+      , tyConKind    = mkForAllTys binders res_kind
+      , tyConArity   = length tyvars
+      , tyConTyVars  = tyvars
+      , famTcResVar  = resVar
+      , famTcFlav    = flav
+      , famTcParent  = parent
+      , famTcInj     = inj
       }
 
 
@@ -1294,16 +1381,20 @@ mkFamilyTyCon name kind tyvars resVar flav parent inj
 -- Somewhat dodgily, we give it the same Name
 -- as the data constructor itself; when we pretty-print
 -- the TyCon we add a quote; see the Outputable TyCon instance
-mkPromotedDataCon :: DataCon -> Name -> TyConRepName -> Kind -> [Role] -> TyCon
-mkPromotedDataCon con name rep_name kind roles
+mkPromotedDataCon :: DataCon -> Name -> TyConRepName -> [TyBinder] -> Kind -> [Role]
+                  -> RuntimeRepInfo -> TyCon
+mkPromotedDataCon con name rep_name binders res_kind roles rep_info
   = PromotedDataCon {
-        tyConUnique = nameUnique name,
-        tyConName   = name,
-        tyConArity  = arity,
-        tcRoles     = roles,
-        tyConKind   = kind,
-        dataCon     = con,
-        tcRepName   = rep_name
+        tyConUnique   = nameUnique name,
+        tyConName     = name,
+        tyConArity    = arity,
+        tcRoles       = roles,
+        tyConBinders  = binders,
+        tyConResKind  = res_kind,
+        tyConKind     = mkForAllTys binders res_kind,
+        dataCon       = con,
+        tcRepName     = rep_name,
+        promDcRepInfo = rep_info
   }
   where
     arity = length roles
@@ -1321,16 +1412,8 @@ isAbstractTyCon _ = False
 -- Used when recovering from errors
 makeTyConAbstract :: TyCon -> TyCon
 makeTyConAbstract tc
-  = PrimTyCon { tyConName        = name,
-                tyConUnique      = nameUnique name,
-                tyConKind        = tyConKind tc,
-                tyConArity       = tyConArity tc,
-                tcRoles          = tyConRoles tc,
-                primTyConRep     = PtrRep,
-                isUnlifted       = False,
-                primRepName      = Nothing }
-  where
-    name = tyConName tc
+  = mkTcTyCon (tyConName tc) (tyConBinders tc) (tyConResKind tc)
+              (mightBeUnsaturatedTyCon tc)
 
 -- | Does this 'TyCon' represent something that cannot be defined in Haskell?
 isPrimTyCon :: TyCon -> Bool
@@ -1642,12 +1725,18 @@ isPromotedDataCon_maybe _ = Nothing
 -- | Is this tycon really meant for use at the kind level? That is,
 -- should it be permitted without -XDataKinds?
 isKindTyCon :: TyCon -> Bool
-isKindTyCon tc = isLiftedTypeKindTyConName (tyConName tc) ||
-                 tc `hasKey` constraintKindTyConKey ||
-                 tc `hasKey` tYPETyConKey ||
-                 tc `hasKey` levityTyConKey ||
-                 tc `hasKey` liftedDataConKey ||
-                 tc `hasKey` unliftedDataConKey
+isKindTyCon tc = getUnique tc `elementOfUniqSet` kindTyConKeys
+
+-- | These TyCons should be allowed at the kind level, even without
+-- -XDataKinds.
+kindTyConKeys :: UniqSet Unique
+kindTyConKeys = unionManyUniqSets
+  ( mkUniqSet [ liftedTypeKindTyConKey, starKindTyConKey, unicodeStarKindTyConKey
+              , constraintKindTyConKey, tYPETyConKey ]
+  : map (mkUniqSet . tycon_with_datacons) [ runtimeRepTyCon
+                                          , vecCountTyCon, vecElemTyCon ] )
+  where
+    tycon_with_datacons tc = getUnique tc : map getUnique (tyConDataCons tc)
 
 isLiftedTypeKindTyConName :: Name -> Bool
 isLiftedTypeKindTyConName
@@ -1855,11 +1944,6 @@ newTyConCo tc = case newTyConCo_maybe tc of
                  Just co -> co
                  Nothing -> pprPanic "newTyConCo" (ppr tc)
 
--- | Find the primitive representation of a 'TyCon'
-tyConPrimRep :: TyCon -> PrimRep
-tyConPrimRep (PrimTyCon {primTyConRep = rep}) = rep
-tyConPrimRep tc = ASSERT(not (isUnboxedTupleTyCon tc)) PtrRep
-
 -- | Find the \"stupid theta\" of the 'TyCon'. A \"stupid theta\" is the context
 -- to the left of an algebraic type declaration, e.g. @Eq a@ in the declaration
 -- @data Eq a => T a ...@
@@ -1929,6 +2013,12 @@ tyConFamilyCoercion_maybe (AlgTyCon {algTcParent = DataFamInstTyCon ax _ _ })
   = Just ax
 tyConFamilyCoercion_maybe _ = Nothing
 
+-- | Extract any 'RuntimeRepInfo' from this TyCon
+tyConRuntimeRepInfo :: TyCon -> RuntimeRepInfo
+tyConRuntimeRepInfo (PromotedDataCon { promDcRepInfo = rri }) = rri
+tyConRuntimeRepInfo _                                         = NoRRI
+  -- could panic in that second case. But Douglas Adams told me not to.
+
 {-
 ************************************************************************
 *                                                                      *
index 824aa9d..bca64c2 100644 (file)
@@ -41,7 +41,7 @@ module Type (
         splitForAllTy_maybe, splitForAllTys, splitForAllTy,
         splitPiTy_maybe, splitPiTys, splitPiTy,
         splitNamedPiTys,
-        mkPiType, mkPiTypes, mkPiTypesPreferFunTy,
+        mkPiType, mkPiTypes, mkTyBindersPreferAnon,
         piResultTy, piResultTys,
         applyTysX, dropForAlls,
 
@@ -58,7 +58,6 @@ module Type (
         splitPiTysInvisible, filterOutInvisibleTypes,
         filterOutInvisibleTyVars, partitionInvisibles,
         synTyConResKind,
-        tyConBinders,
 
         -- Analyzing types
         TyCoMapper(..), mapType, mapCoercion,
@@ -103,9 +102,9 @@ module Type (
         -- (Lifting and boxity)
         isUnliftedType, isUnboxedTupleType, isAlgType, isClosedAlgType,
         isPrimitiveType, isStrictType,
-        isLevityTy, isLevityVar, isLevityKindedTy,
-        dropLevityArgs,
-        getLevity, getLevityFromKind,
+        isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
+        dropRuntimeRepArgs,
+        getRuntimeRep, getRuntimeRepFromKind,
 
         -- * Main data types representing Kinds
         Kind,
@@ -114,7 +113,7 @@ module Type (
         typeKind,
 
         -- ** Common Kind
-        liftedTypeKind, unliftedTypeKind,
+        liftedTypeKind,
 
         -- * Type free variables
         tyCoVarsOfType, tyCoVarsOfTypes, tyCoVarsOfTypeAcc,
@@ -143,7 +142,7 @@ module Type (
         tyConsOfType,
 
         -- * Type representation for the code generator
-        typePrimRep, typeRepArity,
+        typePrimRep, typeRepArity, kindPrimRep, tyConPrimRep,
 
         -- * Main type substitution data types
         TvSubstEnv,     -- Representation widely visible
@@ -310,7 +309,8 @@ coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc t
 coreView _ = Nothing
 
 -- | Like 'coreView', but it also "expands" @Constraint@ to become
--- @TYPE Lifted@.
+-- @TYPE PtrRepLifted@.
+{-# INLINE coreViewOneStarKind #-}
 coreViewOneStarKind :: Type -> Maybe Type
 coreViewOneStarKind ty
   | Just ty' <- coreView ty   = Just ty'
@@ -1077,27 +1077,28 @@ mkCastTy ty co = -- NB: don't check if the coercion "from" type matches here;
       = split_apps (t2:args) t1 co
     split_apps args (TyConApp tc tc_args) co
       | mightBeUnsaturatedTyCon tc
-      = affix_co (tyConKind tc) (mkTyConTy tc) (tc_args `chkAppend` args) co
+      = affix_co (tyConBinders tc) (mkTyConTy tc) (tc_args `chkAppend` args) co
       | otherwise -- not decomposable... but it may still be oversaturated
       = let (non_decomp_args, decomp_args) = splitAt (tyConArity tc) tc_args
             saturated_tc = mkTyConApp tc non_decomp_args
         in
-        affix_co (typeKind saturated_tc) saturated_tc (decomp_args `chkAppend` args) co
+        affix_co (fst $ splitPiTys $ typeKind saturated_tc)
+                 saturated_tc (decomp_args `chkAppend` args) co
 
     split_apps args (ForAllTy (Anon arg) res) co
-      = affix_co (tyConKind funTyCon) (mkTyConTy funTyCon)
+      = affix_co (tyConBinders funTyCon) (mkTyConTy funTyCon)
                  (arg : res : args) co
     split_apps args ty co
-      = affix_co (typeKind ty) ty args co
+      = affix_co (fst $ splitPiTys $ typeKind ty)
+                 ty args co
 
     -- having broken everything apart, this figures out the point at which there
     -- are no more dependent quantifications, and puts the cast there
     affix_co _ ty [] co = no_double_casts ty co
-    affix_co kind ty args co
+    affix_co bndrs ty args co
       -- if kind contains any dependent quantifications, we can't push.
       -- apply arguments until it doesn't
-      = let (bndrs, _inner_ki) = splitPiTys kind
-            (no_dep_bndrs, some_dep_bndrs) = spanEnd isAnonBinder bndrs
+      = let (no_dep_bndrs, some_dep_bndrs) = spanEnd isAnonBinder bndrs
             (some_dep_args, rest_args) = splitAtList some_dep_bndrs args
             dep_subst = zipTyBinderSubst some_dep_bndrs some_dep_args
             used_no_dep_bndrs = takeList rest_args no_dep_bndrs
@@ -1212,10 +1213,10 @@ repType ty
       | isUnboxedTupleTyCon tc
       = if null tys
          then UnaryRep voidPrimTy -- See Note [Nullary unboxed tuple]
-         else UbxTupleRep (concatMap (flattenRepType . go rec_nts) non_levity_tys)
+         else UbxTupleRep (concatMap (flattenRepType . go rec_nts) non_rr_tys)
       where
-          -- See Note [Unboxed tuple levity vars] in TyCon
-        non_levity_tys = dropLevityArgs tys
+          -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
+        non_rr_tys = dropRuntimeRepArgs tys
 
     go rec_nts (CastTy ty _)
       = go rec_nts ty
@@ -1230,16 +1231,31 @@ repType ty
 
 -- | Discovers the primitive representation of a more abstract 'UnaryType'
 typePrimRep :: UnaryType -> PrimRep
-typePrimRep ty
-  = case repType ty of
-      UbxTupleRep _ -> pprPanic "typePrimRep: UbxTupleRep" (ppr ty)
-      UnaryRep rep -> go rep
-    where go (TyConApp tc _)   = tyConPrimRep tc
-          go (ForAllTy _ _)    = PtrRep
-          go (AppTy _ _)       = PtrRep      -- See Note [AppTy rep]
-          go (TyVarTy _)       = PtrRep
-          go (CastTy ty _)     = go ty
-          go _                 = pprPanic "typePrimRep: UnaryRep" (ppr ty)
+typePrimRep ty = kindPrimRep (typeKind ty)
+
+-- | Find the primitive representation of a 'TyCon'. Defined here to
+-- avoid module loops. Call this only on unlifted tycons.
+tyConPrimRep :: TyCon -> PrimRep
+tyConPrimRep tc = kindPrimRep res_kind
+  where
+    res_kind = tyConResKind tc
+
+-- | Take a kind (of shape @TYPE rr@) and produce the 'PrimRep' of values
+-- of types of this kind.
+kindPrimRep :: Kind -> PrimRep
+kindPrimRep ki | Just ki' <- coreViewOneStarKind ki = kindPrimRep ki'
+kindPrimRep (TyConApp typ [runtime_rep])
+  = ASSERT( typ `hasKey` tYPETyConKey )
+    go runtime_rep
+  where
+    go rr | Just rr' <- coreView rr = go rr'
+    go (TyConApp rr_dc args)
+      | RuntimeRep fun <- tyConRuntimeRepInfo rr_dc
+      = fun args
+    go rr = pprPanic "kindPrimRep.go" (ppr rr)
+kindPrimRep ki = WARN( True
+                     , text "kindPrimRep defaulting to PtrRep on" <+> ppr ki )
+                 PtrRep  -- this can happen legitimately for, e.g., Any
 
 typeRepArity :: Arity -> Type -> RepArity
 typeRepArity 0 _ = 0
@@ -1250,7 +1266,8 @@ typeRepArity n ty = case repType ty of
 isVoidTy :: Type -> Bool
 -- True if the type has zero width
 isVoidTy ty = case repType ty of
-                UnaryRep (TyConApp tc _) -> isVoidRep (tyConPrimRep tc)
+                UnaryRep (TyConApp tc _) -> isUnliftedTyCon tc &&
+                                            isVoidRep (tyConPrimRep tc)
                 _                        -> False
 
 {-
@@ -1274,10 +1291,6 @@ mkNamedForAllTy :: TyVar -> VisibilityFlag -> Type -> Type
 mkNamedForAllTy tv vis = ASSERT( isTyVar tv )
                          ForAllTy (Named tv vis)
 
--- | Wraps foralls over the type using the provided 'TyVar's from left to right
-mkForAllTys :: [TyBinder] -> Type -> Type
-mkForAllTys tyvars ty = foldr ForAllTy ty tyvars
-
 -- | Like mkForAllTys, but assumes all variables are dependent and invisible,
 -- a common case
 mkInvForAllTys :: [TyVar] -> Type -> Type
@@ -1309,23 +1322,23 @@ mkPiType v ty
 
 mkPiTypes vs ty = foldr mkPiType ty vs
 
--- | Given a list of type-level vars, makes ForAllTys, preferring
+-- | Given a list of type-level vars and a result type, makes TyBinders, preferring
 -- anonymous binders if the variable is, in fact, not dependent.
 -- All binders are /visible/.
-mkPiTypesPreferFunTy :: [TyVar] -> Type -> Type
-mkPiTypesPreferFunTy vars inner_ty = fst $ go vars inner_ty
+mkTyBindersPreferAnon :: [TyVar] -> Type -> [TyBinder]
+mkTyBindersPreferAnon vars inner_ty = fst $ go vars inner_ty
   where
-    go :: [TyVar] -> Type -> (Type, VarSet) -- also returns the free vars
-    go []     ty = (ty, tyCoVarsOfType ty)
-    go (v:vs) ty | v `elemVarSet` fvs
-                 = ( mkForAllTy (Named v Visible) qty
+    go :: [TyVar] -> Type -> ([TyBinder], VarSet) -- also returns the free vars
+    go [] ty = ([], tyCoVarsOfType ty)
+    go (v:vs) ty |  v `elemVarSet` fvs
+                 = ( Named v Visible : binders
                    , fvs `delVarSet` v `unionVarSet` kind_vars )
                  | otherwise
-                 = ( mkForAllTy (Anon (tyVarKind v)) qty
+                 = ( Anon (tyVarKind v) : binders
                    , fvs `unionVarSet` kind_vars )
       where
-        (qty, fvs) = go vs ty
-        kind_vars  = tyCoVarsOfType $ tyVarKind v
+        (binders, fvs) = go vs ty
+        kind_vars      = tyCoVarsOfType $ tyVarKind v
 
 -- | Take a ForAllTy apart, returning the list of tyvars and the result type.
 -- This always succeeds, even if it returns only an empty list. Note that the
@@ -1454,9 +1467,6 @@ splitPiTysInvisible ty = split ty ty []
      split orig_ty _ bndrs
        = (reverse bndrs, orig_ty)
 
-tyConBinders :: TyCon -> [TyBinder]
-tyConBinders = fst . splitPiTys . tyConKind
-
 applyTysX :: [TyVar] -> Type -> [Type] -> Type
 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
 -- Assumes that (/\tvs. body_ty) is closed
@@ -1917,25 +1927,26 @@ isUnliftedType (ForAllTy (Named {}) ty) = isUnliftedType ty
 isUnliftedType (TyConApp tc _)          = isUnliftedTyCon tc
 isUnliftedType _                        = False
 
--- | Extract the levity classifier of a type. Panics if this is not possible.
-getLevity :: String   -- ^ Printed in case of an error
-          -> Type -> Type
-getLevity err ty = getLevityFromKind err (typeKind ty)
+-- | Extract the RuntimeRep classifier of a type. Panics if this is not possible.
+getRuntimeRep :: String   -- ^ Printed in case of an error
+              -> Type -> Type
+getRuntimeRep err ty = getRuntimeRepFromKind err (typeKind ty)
 
--- | Extract the levity classifier of a type from its kind.
--- For example, getLevityFromKind * = Lifted; getLevityFromKind # = Unlifted.
+-- | Extract the RuntimeRep classifier of a type from its kind.
+-- For example, getRuntimeRepFromKind * = PtrRepLifted;
+--              getRuntimeRepFromKind # = PtrRepUnlifted.
 -- Panics if this is not possible.
-getLevityFromKind :: String  -- ^ Printed in case of an error
-                  -> Type -> Type
-getLevityFromKind err = go
+getRuntimeRepFromKind :: String  -- ^ Printed in case of an error
+                      -> Type -> Type
+getRuntimeRepFromKind err = go
   where
     go k | Just k' <- coreViewOneStarKind k = go k'
     go k
       | Just (tc, [arg]) <- splitTyConApp_maybe k
       , tc `hasKey` tYPETyConKey
       = arg
-    go k = pprPanic "getLevity" (text err $$
-                                 ppr k <+> dcolon <+> ppr (typeKind k))
+    go k = pprPanic "getRuntimeRep" (text err $$
+                                     ppr k <+> dcolon <+> ppr (typeKind k))
 
 isUnboxedTupleType :: Type -> Bool
 isUnboxedTupleType ty = case tyConAppTyCon_maybe ty of
@@ -2065,11 +2076,17 @@ cmpTypes ts1 ts2 = cmpTypesX rn_env ts1 ts2
 
 cmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
     -- See Note [Non-trivial definitional equality] in TyCoRep
-cmpTypeX env orig_t1 orig_t2 = go env k1 k2 `thenCmp` go env orig_t1 orig_t2
+cmpTypeX env orig_t1 orig_t2
+  = go env orig_t1 orig_t2 `thenCmp` go env k1 k2
+      -- NB: this ordering appears to be faster than the other
   where
     k1 = typeKind orig_t1
     k2 = typeKind orig_t2
 
+      -- short-cut to handle comparing * against *.
+      -- appears to have a roughly 1% improvement in compile times
+    go _ (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 = EQ
+
     go env t1 t2 | Just t1' <- coreViewOneStarKind t1 = go env t1' t2
     go env t1 t2 | Just t2' <- coreViewOneStarKind t2 = go env t1 t2'
 
index 8cafbfb..ff0f45f 100644 (file)
@@ -14,6 +14,8 @@ module Util (
         zipEqual, zipWithEqual, zipWith3Equal, zipWith4Equal,
         zipLazy, stretchZipWith, zipWithAndUnzip,
 
+        zipWithLazy, zipWith3Lazy,
+
         filterByList, filterByLists, partitionByList,
 
         unzipWith,
@@ -322,6 +324,20 @@ zipLazy :: [a] -> [b] -> [(a,b)]
 zipLazy []     _       = []
 zipLazy (x:xs) ~(y:ys) = (x,y) : zipLazy xs ys
 
+-- | 'zipWithLazy' is like 'zipWith' but is lazy in the second list.
+-- The length of the output is always the same as the length of the first
+-- list.
+zipWithLazy :: (a -> b -> c) -> [a] -> [b] -> [c]
+zipWithLazy _ []     _       = []
+zipWithLazy f (a:as) ~(b:bs) = f a b : zipWithLazy f as bs
+
+-- | 'zipWith3Lazy' is like 'zipWith3' but is lazy in the second and third lists.
+-- The length of the output is always the same as the length of the first
+-- list.
+zipWith3Lazy :: (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
+zipWith3Lazy _ []     _       _       = []
+zipWith3Lazy f (a:as) ~(b:bs) ~(c:cs) = f a b c : zipWith3Lazy f as bs cs
+
 -- | 'filterByList' takes a list of Bools and a list of some elements and
 -- filters out these elements for which the corresponding value in the list of
 -- Bools is False. This function does not check whether the lists have equal
index 5f283c6..9daa16a 100644 (file)
@@ -360,7 +360,7 @@ vectExpr (_, AnnApp (_, AnnApp (_, AnnVar v) (_, AnnType ty)) err)
   | v == pAT_ERROR_ID
   = do
     { (vty, lty) <- vectAndLiftType ty
-    ; return (mkCoreApps (Var v) [Type (getLevity "vectExpr" vty), Type vty, err'], mkCoreApps (Var v) [Type lty, err'])
+    ; return (mkCoreApps (Var v) [Type (getRuntimeRep "vectExpr" vty), Type vty, err'], mkCoreApps (Var v) [Type lty, err'])
     }
   where
     err' = deAnnotate err
index a8bffbe..4f31128 100644 (file)
@@ -51,7 +51,8 @@ buildDataFamInst name' fam_tc vect_tc rhs
             rep_ty   = mkTyConApp rep_tc tys'
             pat_tys  = [mkTyConApp vect_tc tys']
             rep_tc   = mkAlgTyCon name'
-                           (mkPiTypesPreferFunTy tyvars' liftedTypeKind)
+                           (mkTyBindersPreferAnon tyvars' liftedTypeKind)
+                           liftedTypeKind
                            tyvars'
                            (map (const Nominal) tyvars')
                            Nothing
index 7b00a5c..0bcdf0c 100644 (file)
@@ -360,7 +360,7 @@ vectTypeEnv tycons vectTypeDecls vectClassDecls
         origName  = tyConName origTyCon
         vectName  = tyConName vectTyCon
 
-        mkSyn canonName ty = mkSynonymTyCon canonName (typeKind ty) [] [] ty
+        mkSyn canonName ty = mkSynonymTyCon canonName [] (typeKind ty) [] [] ty
 
         defDataCons
           | isAbstract = return ()
index 03e7d27..4847aa8 100644 (file)
@@ -64,7 +64,7 @@ vectTyConDecl tycon name'
                      (tyConTyVars tycon)        -- keep original type vars
                      (map (const Nominal) (tyConRoles tycon)) -- all role are N for safety
                      theta'                     -- superclasses
-                     (tyConKind tycon)          -- keep original kind
+                     (tyConBinders tycon)       -- keep original kind
                      (snd . classTvsFds $ cls)  -- keep the original functional dependencies
                      []                         -- no associated types (for the moment)
                      methods'                   -- method info
@@ -103,7 +103,8 @@ vectTyConDecl tycon name'
        ; tc_rep_name <- mkDerivedName mkTyConRepOcc name'
        ; return $ mkAlgTyCon
                     name'                   -- new name
-                    (tyConKind tycon)       -- keep original kind
+                    (tyConBinders tycon)
+                    (tyConResKind tycon)    -- keep original kind
                     (tyConTyVars tycon)     -- keep original type vars
                     (map (const Nominal) (tyConRoles tycon)) -- all roles are N for safety
                     Nothing
index 88191c1..cc94bac 100644 (file)
@@ -114,7 +114,7 @@ import Data.Monoid
 import Data.Ord
 import Data.Typeable
 import Data.Version( Version(..) )
-import GHC.Base hiding (Any)
+import GHC.Base hiding (Any, IntRep, FloatRep)
 import GHC.List
 import GHC.Num
 import GHC.Read
index efec62f..87e5c88 100644 (file)
@@ -10,6 +10,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeApplications #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -249,18 +250,6 @@ tyConOf = typeRepTyCon . typeRep
 tcFun :: TyCon
 tcFun = tyConOf (Proxy :: Proxy (Int -> Int))
 
-tcList :: TyCon
-tcList = tyConOf (Proxy :: Proxy [])
-
-tcTYPE :: TyCon
-tcTYPE = tyConOf (Proxy :: Proxy TYPE)
-
-tc'Lifted :: TyCon
-tc'Lifted = tyConOf (Proxy :: Proxy 'Lifted)
-
-tc'Unlifted :: TyCon
-tc'Unlifted = tyConOf (Proxy :: Proxy 'Unlifted)
-
 -- | Adds a TypeRep argument to a TypeRep.
 mkAppTy :: TypeRep -> TypeRep -> TypeRep
 {-# INLINE mkAppTy #-}
@@ -364,10 +353,19 @@ instance Show TypeRep where
   showsPrec p (TypeRep _ tycon kinds tys) =
     case tys of
       [] -> showsPrec p tycon
-      [x@(TypeRep _ argCon _ _)]
+      [x]
         | tycon == tcList -> showChar '[' . shows x . showChar ']'
-        | tycon == tcTYPE && argCon == tc'Lifted   -> showChar '*'
-        | tycon == tcTYPE && argCon == tc'Unlifted -> showChar '#'
+        where
+          tcList = tyConOf @[] Proxy
+      [TypeRep _ ptrRepCon _ []]
+        | tycon == tcTYPE && ptrRepCon == tc'PtrRepLifted
+          -> showChar '*'
+        | tycon == tcTYPE && ptrRepCon == tc'PtrRepUnlifted
+          -> showChar '#'
+        where
+          tcTYPE            = tyConOf @TYPE            Proxy
+          tc'PtrRepLifted   = tyConOf @'PtrRepLifted   Proxy
+          tc'PtrRepUnlifted = tyConOf @'PtrRepUnlifted Proxy
       [a,r] | tycon == tcFun  -> showParen (p > 8) $
                                  showsPrec 9 a .
                                  showString " -> " .
index 88b9c39..4231fce 100644 (file)
@@ -24,7 +24,7 @@
 
 module GHC.Err( absentErr, error, errorWithoutStackTrace, undefined ) where
 import GHC.CString ()
-import GHC.Types (Char, Levity)
+import GHC.Types (Char, RuntimeRep)
 import GHC.Stack.Types
 import GHC.Prim
 import GHC.Integer ()   -- Make sure Integer is compiled first
@@ -33,7 +33,7 @@ import GHC.Integer ()   -- Make sure Integer is compiled first
 import {-# SOURCE #-} GHC.Exception( errorCallWithCallStackException )
 
 -- | 'error' stops execution and displays an error message.
-error :: forall (v :: Levity). forall (a :: TYPE v).
+error :: forall (r :: RuntimeRep). forall (a :: TYPE r).
          HasCallStack => [Char] -> a
 error s = raise# (errorCallWithCallStackException s ?callStack)
           -- Bleh, we should be using 'GHC.Stack.callStack' instead of
@@ -44,7 +44,7 @@ error s = raise# (errorCallWithCallStackException s ?callStack)
 -- | A variant of 'error' that does not produce a stack trace.
 --
 -- @since 4.9.0.0
-errorWithoutStackTrace :: forall (v :: Levity). forall (a :: TYPE v).
+errorWithoutStackTrace :: forall (r :: RuntimeRep). forall (a :: TYPE r).
                           [Char] -> a
 errorWithoutStackTrace s =
   -- we don't have withFrozenCallStack yet, so we just inline the definition
@@ -74,7 +74,7 @@ errorWithoutStackTrace s =
 -- It is expected that compilers will recognize this and insert error
 -- messages which are more appropriate to the context in which 'undefined'
 -- appears.
-undefined :: forall (v :: Levity). forall (a :: TYPE v).
+undefined :: forall (r :: RuntimeRep). forall (a :: TYPE r).
              HasCallStack => a
 undefined =  error "Prelude.undefined"
 
index 31e70eb..21f7bfd 100755 (executable)
@@ -56,8 +56,8 @@ module GHC.Exts
         -- * Equality
         type (~~),
 
-        -- * Levity polymorphism
-        GHC.Prim.TYPE, Levity(..),
+        -- * Representation polymorphism
+        GHC.Prim.TYPE, RuntimeRep(..), VecCount(..), VecElem(..),
 
         -- * Transform comprehensions
         Down(..), groupWith, sortWith, the,
index 22864d9..2b4ac56 100644 (file)
@@ -7,5 +7,5 @@ import GHC.Types
 main :: IO ()
 main = do
   print (typeOf (Proxy :: Proxy 'Just))
-  print (typeOf (Proxy :: Proxy (TYPE 'Lifted)))
-  print (typeOf (Proxy :: Proxy (TYPE 'Unlifted)))
+  print (typeOf (Proxy :: Proxy (TYPE 'PtrRepLifted)))
+  print (typeOf (Proxy :: Proxy (TYPE 'PtrRepUnlifted)))
index 727811b..6f9e09f 100644 (file)
@@ -30,10 +30,11 @@ module GHC.Types (
         SPEC(..),
         Nat, Symbol,
         type (~~), Coercible,
-        TYPE, Levity(..), Type, type (*), type (★), Constraint,
+        TYPE, RuntimeRep(..), Type, type (*), type (★), Constraint,
           -- The historical type * should ideally be written as
           -- `type *`, without the parentheses. But that's a true
           -- pain to parse, and for little gain.
+        VecCount(..), VecElem(..),
 
         -- * Runtime type representation
         Module(..), TrName(..), TyCon(..)
@@ -57,13 +58,13 @@ infixr 5 :
 data Constraint
 
 -- | The kind of types with values. For example @Int :: Type@.
-type Type = TYPE 'Lifted
+type Type = TYPE 'PtrRepLifted
 
 -- | A backward-compatible (pre-GHC 8.0) synonym for 'Type'
-type * = TYPE 'Lifted
+type * = TYPE 'PtrRepLifted
 
 -- | A unicode backward-compatible (pre-GHC 8.0) synonym for 'Type'
-type ★ = TYPE 'Lifted
+type ★ = TYPE 'PtrRepLifted
 
 {- *********************************************************************
 *                                                                      *
@@ -330,17 +331,59 @@ you're reading this in 2023 then things went wrong). See #8326.
 -- loops should be aggressively specialized.
 data SPEC = SPEC | SPEC2
 
--- | GHC divides all proper types (that is, types that can perhaps be
--- inhabited, as distinct from type constructors or type-level data)
--- into two worlds: lifted types and unlifted types. For example,
--- @Int@ is lifted while @Int#@ is unlifted. Certain operations need
--- to be polymorphic in this distinction. A classic example is 'unsafeCoerce#',
--- which needs to be able to coerce between lifted and unlifted types.
--- To achieve this, we use kind polymorphism: lifted types have kind
--- @TYPE Lifted@ and unlifted ones have kind @TYPE Unlifted@. 'Levity'
--- is the kind of 'Lifted' and 'Unlifted'. @*@ is a synonym for @TYPE Lifted@
--- and @#@ is a synonym for @TYPE Unlifted@.
-data Levity = Lifted | Unlifted
+
+{- *********************************************************************
+*                                                                      *
+                    RuntimeRep
+*                                                                      *
+********************************************************************* -}
+
+
+-- | GHC maintains a property that the kind of all inhabited types
+-- (as distinct from type constructors or type-level data) tells us
+-- the runtime representation of values of that type. This datatype
+-- encodes the choice of runtime value.
+-- Note that 'TYPE' is parameterised by 'RuntimeRep'; this is precisely
+-- what we mean by the fact that a type's kind encodes the runtime
+-- representation.
+--
+-- For boxed values (that is, values that are represented by a pointer),
+-- a further distinction is made, between lifted types (that contain ⊥),
+-- and unlifted ones (that don't).
+data RuntimeRep = VecRep VecCount VecElem   -- ^ a SIMD vector type
+                | PtrRepLifted    -- ^ lifted; represented by a pointer
+                | PtrRepUnlifted  -- ^ unlifted; represented by a pointer
+                | VoidRep         -- ^ erased entirely
+                | IntRep          -- ^ signed, word-sized value
+                | WordRep         -- ^ unsigned, word-sized value
+                | Int64Rep        -- ^ signed, 64-bit value (on 32-bit only)
+                | Word64Rep       -- ^ unsigned, 64-bit value (on 32-bit only)
+                | AddrRep         -- ^ A pointer, but /not/ to a Haskell value
+                | FloatRep        -- ^ a 32-bit floating point number
+                | DoubleRep       -- ^ a 64-bit floating point number
+                | UnboxedTupleRep -- ^ An unboxed tuple; this doesn't specify a concrete rep
+
+-- See also Note [Wiring in RuntimeRep] in TysWiredIn
+
+-- | Length of a SIMD vector type
+data VecCount = Vec2
+              | Vec4
+              | Vec8
+              | Vec16
+              | Vec32
+              | Vec64
+
+-- | Element of a SIMD vector type
+data VecElem = Int8ElemRep
+             | Int16ElemRep
+             | Int32ElemRep
+             | Int64ElemRep
+             | Word8ElemRep
+             | Word16ElemRep
+             | Word32ElemRep
+             | Word64ElemRep
+             | FloatElemRep
+             | DoubleElemRep
 
 {- *********************************************************************
 *                                                                      *
index f80d994..cdb713f 100644 (file)
@@ -5,5 +5,5 @@ module T11405 where
 import GHC.Exts
 import GHC.Stack
 
-x :: forall (v :: Levity) (a :: TYPE v). (?callStack :: CallStack) => a
+x :: forall (v :: RuntimeRep) (a :: TYPE v). (?callStack :: CallStack) => a
 x = undefined
index 158aec6..2394f89 100644 (file)
@@ -1,12 +1,12 @@
 
 BadTelescope4.hs:9:1: error:
-    • These kind and type variables: (a :: k1)
+    • These kind and type variables: (a :: k)
                                      (c :: Proxy b)
                                      (d :: Proxy a)
                                      (x :: SameKind b d)
       are out of dependency order. Perhaps try this ordering:
-        k1
-        (a :: k1)
+        k
+        (a :: k)
         (b :: Proxy a)
         (c :: Proxy b)
         (d :: Proxy a)
index 09845ed..bbec037 100644 (file)
@@ -5,4 +5,4 @@ module TypeSkolEscape where
 import GHC.Types
 import GHC.Exts
 
-type Bad = forall (v :: Levity) (a :: TYPE v). a
+type Bad = forall (v :: RuntimeRep) (a :: TYPE v). a
index 1574c01..a4ce1e4 100644 (file)
@@ -1,7 +1,7 @@
 
 TypeSkolEscape.hs:8:1: error:
-    Quantified type's kind mentions quantified type variable
-    (skolem escape)
-         type: forall (v1 :: Levity) (a1 :: TYPE v1). a1
-      of kind: TYPE v
-    In the type synonym declaration for ‘Bad’
+    • Quantified type's kind mentions quantified type variable
+      (skolem escape)
+           type: forall (v1 :: RuntimeRep) (a1 :: TYPE v1). a1
+        of kind: TYPE v
+    • In the type synonym declaration for ‘Bad’
index ef5b5c6..e1ef925 100644 (file)
@@ -1,6 +1,4 @@
-type family A a b
-  Kind: * -> * -> *
-       -- Defined at T4175.hs:7:1
+type family A a b :: *         -- Defined at T4175.hs:7:1
 type instance A (B a) b = ()   -- Defined at T4175.hs:10:15
 type instance A (Maybe a) a = a        -- Defined at T4175.hs:9:15
 type instance A Int Int = ()   -- Defined at T4175.hs:8:15
@@ -9,13 +7,11 @@ instance G B -- Defined at T4175.hs:34:10
 data instance B () = MkB       -- Defined at T4175.hs:13:15
 type instance A (B a) b = ()   -- Defined at T4175.hs:10:15
 class C a where
-  type family D a b
-    Kind: * -> * -> *
+  type family D a b :: *
        -- Defined at T4175.hs:16:5
 type instance D () () = Bool   -- Defined at T4175.hs:22:10
 type instance D Int () = String        -- Defined at T4175.hs:19:10
-type family E a
-  Kind: * -> *
+type family E a :: *
   where
       E () = Bool
       E Int = String
index 4b16acc..ee6dfa4 100644 (file)
@@ -29,11 +29,11 @@ data (#,#) (c :: TYPE a) (d :: TYPE b) = (#,#) c d
        -- Defined in ‘GHC.Prim’
 (,) :: a -> b -> (a, b)
 (#,#)
-  :: forall (a :: GHC.Types.Levity) (b :: GHC.Types.Levity) (c :: TYPE
-                                                                    a) (d :: TYPE b).
+  :: forall (a :: GHC.Types.RuntimeRep) (b :: GHC.Types.RuntimeRep) (c :: TYPE
+                                                                            a) (d :: TYPE b).
      c -> d -> (# c, d #)
 (  ,  ) :: a -> b -> (a, b)
 (#  ,  #)
-  :: forall (a :: GHC.Types.Levity) (b :: GHC.Types.Levity) (c :: TYPE
-                                                                    a) (d :: TYPE b).
+  :: forall (a :: GHC.Types.RuntimeRep) (b :: GHC.Types.RuntimeRep) (c :: TYPE
+                                                                            a) (d :: TYPE b).
      c -> d -> (# c, d #)
index 1e6c5b7..2b2c8b7 100644 (file)
@@ -1,32 +1,25 @@
 class Foo (a :: k) where
-  type family Bar (a :: k) b
-    Kind: forall k1. k1 -> * -> *
+  type family Bar (a :: k) b :: *
        -- Defined at T7939.hs:6:4
 Bar :: k -> * -> *
-type family F a
-  Kind: * -> *
-       -- Defined at T7939.hs:8:1
+type family F a :: *   -- Defined at T7939.hs:8:1
 type instance F Int = Bool     -- Defined at T7939.hs:9:15
 F :: * -> *
-type family G a
-  Kind: * -> *
+type family G a :: *
   where G Int = Bool
        -- Defined at T7939.hs:11:1
 G :: * -> *
-type family H (a :: Bool)
-  Kind: Bool -> Bool
+type family H (a :: Bool) :: Bool
   where H 'False = 'True
        -- Defined at T7939.hs:14:1
 H :: Bool -> Bool
-type family J (a :: [k])
-  Kind: forall k1. [k1] -> Bool
+type family J (a :: [k]) :: Bool
   where
     [k] J k '[] = 'False
     [k, (h :: k), (t :: [k])] J k (h : t) = 'True
        -- Defined at T7939.hs:17:1
 J :: [k] -> Bool
-type family K (a1 :: [a])
-  Kind: forall a2. [a2] -> Maybe a2
+type family K (a1 :: [a]) :: Maybe a
   where
     [a] K a '[] = 'Nothing
     [a, (h :: a), (t :: [a])] K a (h : t) = 'Just h
index 2f35e23..6eb08cd 100644 (file)
@@ -1,4 +1,4 @@
-data (->) a b  -- Defined in ‘GHC.Prim’
+data (->) t1 t2        -- Defined in ‘GHC.Prim’
 infixr 0 `(->)`
 instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
index 3482d54..43bbbac 100644 (file)
@@ -1,23 +1,23 @@
 type family (GHC.TypeLits.*) (a :: GHC.Types.Nat)
                              (b :: GHC.Types.Nat)
-  Kind: GHC.Types.Nat -> GHC.Types.Nat -> GHC.Types.Nat
+            :: GHC.Types.Nat
 type family (GHC.TypeLits.+) (a :: GHC.Types.Nat)
                              (b :: GHC.Types.Nat)
-  Kind: GHC.Types.Nat -> GHC.Types.Nat -> GHC.Types.Nat
+            :: GHC.Types.Nat
 type family (GHC.TypeLits.-) (a :: GHC.Types.Nat)
                              (b :: GHC.Types.Nat)
-  Kind: GHC.Types.Nat -> GHC.Types.Nat -> GHC.Types.Nat
+            :: GHC.Types.Nat
 type (GHC.TypeLits.<=) (x :: GHC.Types.Nat) (y :: GHC.Types.Nat) =
-  (x GHC.TypeLits.<=? y) ~ 'True
+  (x GHC.TypeLits.<=? y) ~ 'True :: Constraint
 type family (GHC.TypeLits.<=?) (a :: GHC.Types.Nat)
                                (b :: GHC.Types.Nat)
-  Kind: GHC.Types.Nat -> GHC.Types.Nat -> Bool
+            :: Bool
 type family GHC.TypeLits.CmpNat (a :: GHC.Types.Nat)
                                 (b :: GHC.Types.Nat)
-  Kind: GHC.Types.Nat -> GHC.Types.Nat -> Ordering
+            :: Ordering
 type family GHC.TypeLits.CmpSymbol (a :: GHC.Types.Symbol)
                                    (b :: GHC.Types.Symbol)
-  Kind: GHC.Types.Symbol -> GHC.Types.Symbol -> Ordering
+            :: Ordering
 data GHC.TypeLits.ErrorMessage where
   GHC.TypeLits.Text :: GHC.Types.Symbol -> GHC.TypeLits.ErrorMessage
   GHC.TypeLits.ShowType :: t -> GHC.TypeLits.ErrorMessage
@@ -38,10 +38,10 @@ data GHC.TypeLits.SomeSymbol where
   GHC.TypeLits.SomeSymbol :: GHC.TypeLits.KnownSymbol n =>
                              (Data.Proxy.Proxy n) -> GHC.TypeLits.SomeSymbol
 type family GHC.TypeLits.TypeError (a :: GHC.TypeLits.ErrorMessage)
-  Kind: forall b1. GHC.TypeLits.ErrorMessage -> b1
+            :: b
 type family (GHC.TypeLits.^) (a :: GHC.Types.Nat)
                              (b :: GHC.Types.Nat)
-  Kind: GHC.Types.Nat -> GHC.Types.Nat -> GHC.Types.Nat
+            :: GHC.Types.Nat
 GHC.TypeLits.natVal ::
   GHC.TypeLits.KnownNat n => proxy n -> Integer
 GHC.TypeLits.natVal' ::
index 2f35e23..6eb08cd 100644 (file)
@@ -1,4 +1,4 @@
-data (->) a b  -- Defined in ‘GHC.Prim’
+data (->) t1 t2        -- Defined in ‘GHC.Prim’
 infixr 0 `(->)`
 instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
index 2f35e23..6eb08cd 100644 (file)
@@ -1,4 +1,4 @@
-data (->) a b  -- Defined in ‘GHC.Prim’
+data (->) t1 t2        -- Defined in ‘GHC.Prim’
 infixr 0 `(->)`
 instance Monad ((->) r) -- Defined in ‘GHC.Base’
 instance Functor ((->) r) -- Defined in ‘GHC.Base’
index 68214e9..3000395 100644 (file)
@@ -7,13 +7,11 @@ TYPE SIGNATURES
     forall c t t1. (Elem c ~ (t, t1), Coll c, Num t1, Num t) => c -> c
 TYPE CONSTRUCTORS
   class Coll c where
-    type family Elem c open
-      Kind: * -> *
+    type family Elem c :: * open
     empty :: c
     insert :: Elem c -> c -> c
     {-# MINIMAL empty, insert #-}
   data ListColl a = L [a]
-    Kind: * -> *
 COERCION AXIOMS
   axiom Foo.D:R:ElemListColl ::
     Elem (ListColl a) = a -- Defined at T3017.hs:13:9
index 04eedb1..ba1f46e 100644 (file)
@@ -1,40 +1,31 @@
 
-ClosedFam3.hs-boot:5:1:
+ClosedFam3.hs-boot:5:1: error:
     Type constructor ‘Foo’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type family Foo a
-                   Kind: * -> *
+    Main module: type family Foo a :: *
                    where
-                     Foo Int = Bool
-                     Foo Double = Char
-    Boot file:   type family Foo a
-                   Kind: * -> *
-                   where
-                     Foo Int = Bool
+                       Foo Int = Bool
+                       Foo Double = Char
+    Boot file:   type family Foo a :: *
+                   where Foo Int = Bool
 
-ClosedFam3.hs-boot:8:1:
+ClosedFam3.hs-boot:8:1: error:
     Type constructor ‘Bar’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type family Bar a
-                   Kind: * -> *
+    Main module: type family Bar a :: *
                    where
-                     Bar Int = Bool
-                     Bar Double = Double
-    Boot file:   type family Bar a
-                   Kind: * -> *
+                       Bar Int = Bool
+                       Bar Double = Double
+    Boot file:   type family Bar a :: *
                    where
-                     Bar Int = Bool
-                     Bar Double = Char
+                       Bar Int = Bool
+                       Bar Double = Char
 
-ClosedFam3.hs-boot:12:1:
+ClosedFam3.hs-boot:12:1: error:
     Type constructor ‘Baz’ has conflicting definitions in the module
     and its hs-boot file
-    Main module: type family Baz a
-                   Kind: * -> *
-                   where
-                     Baz Int = Bool
-    Boot file:   type family Baz (a :: k)
-                   Kind: forall k1. k1 -> *
-                   where
-                     Baz * Int = Bool
+    Main module: type family Baz a :: *
+                   where Baz Int = Bool
+    Boot file:   type family Baz (a :: k) :: *
+                   where Baz * Int = Bool
     The types have different kinds
index d64036c..937a18d 100644 (file)
@@ -1,5 +1,6 @@
 
-Overlap4.hs:7:3:
-    Number of parameters must match family declaration; expected 2
-    In the equations for closed type family ‘F’
-    In the type family declaration for ‘F’
+Overlap4.hs:7:12: error:
+    • Expecting one more argument to ‘Maybe’
+      Expected a type, but ‘Maybe’ has kind ‘* -> *’
+    • In the type ‘Maybe’
+      In the type family declaration for ‘F’
index 8637eaa..b0c91af 100644 (file)
@@ -1,5 +1,4 @@
 
 SimpleFail1a.hs:4:1: error:
-    • Expecting one more argument to ‘T1 Int’
-      Expected a type, but ‘T1 Int’ has kind ‘* -> *’
+    • Number of parameters must match family declaration; expected 2
     • In the data instance declaration for ‘T1’
index b99c8d9..8b3d5f5 100644 (file)
@@ -1,4 +1,6 @@
 
-TyFamArity1.hs:4:15:
-    Number of parameters must match family declaration; expected 2
-    In the type instance declaration for ‘T’
+TyFamArity1.hs:4:23: error:
+    • Expecting one more argument to ‘IO’
+      Expected a type, but ‘IO’ has kind ‘* -> *’
+    • In the type ‘IO’
+      In the type instance declaration for ‘T’