Commit 2059bf44 authored by Alexis King's avatar Alexis King

Add another Note; rename some things; various minor refactorings

parent c2971b08
Pipeline #18899 failed with stages
in 109 minutes and 59 seconds
......@@ -16,10 +16,10 @@ module GHC.Builtin.Types (
mkWiredInTyConName, -- This is used in GHC.Builtin.Types.Literals to define the
-- built-in functions for evaluation.
pcNewTyCon, -- Used in GHC.Builtin.Types.Arrows for the ArrowEnv newtype.
mkWiredInIdName, -- used in GHC.Types.Id.Make
pcDataCon, -- used in FIXME: where is it used?
mkWiredInDataConName,
-- * All wired in things
wiredInTyCons, isBuiltInOcc_maybe,
......@@ -66,7 +66,7 @@ module GHC.Builtin.Types (
consDataCon_RDR, consDataCon, consDataConName,
promotedNilDataCon, promotedConsDataCon,
mkListTy, mkPromotedListTy,
extractPromotedList, isPromotedListTy,
extractPromotedList, extractPromotedList_maybe,
-- * Maybe
maybeTyCon, maybeTyConName,
......@@ -159,6 +159,7 @@ import GHC.Core.DataCon
import {-# SOURCE #-} GHC.Core.ConLike
import GHC.Core.TyCon
import GHC.Core.Class ( Class, mkClass )
import GHC.Core.FamInstEnv ( mkNewTypeCoAxiom )
import GHC.Types.Name.Reader
import GHC.Types.Name as Name
import GHC.Types.Name.Env ( NameEnv, mkNameEnv, lookupNameEnv, lookupNameEnv_NF )
......@@ -554,6 +555,41 @@ pcTyCon name cType tyvars cons
(VanillaAlgTyCon (mkPrelTyConRepName name))
False -- Not in GADT syntax
-- | Like 'pcTyCon', but for a newtype rather than a datatype. Assumes
-- the DataCon has the same OccName as the TyCon.
pcNewTyCon :: Name -- ^ name of the TyCon
-> Unique -- ^ known key for the DataCon
-> Unique -- ^ known key for the coercion
-> [TyVar] -- ^ tyvars
-> Type -- ^ representation type
-> TyCon
pcNewTyCon name data_key co_ax_key tvs rhs_ty = ty_con
where
ty_con = mkAlgTyCon name
(mkAnonTyConBinders VisArg tvs)
liftedTypeKind
(map (const Representational) tvs)
Nothing
[] -- No stupid theta
rhs
(VanillaAlgTyCon (mkPrelTyConRepName name))
False -- Not in GADT syntax
rhs = NewTyCon data_con rhs_ty (tvs, rhs_ty) co_ax False
data_con = pcDataCon data_name tvs [rhs_ty] ty_con
data_name = mkWiredInDataConName UserSyntax
(nameModule name)
(occNameFS (nameOccName name))
data_key
data_con
co_ax_name = mkWiredInName (nameModule name)
(mkNewTyCoOcc (nameOccName name))
co_ax_key
(ACoAxiom (toBranchedAxiom co_ax))
UserSyntax
co_ax = mkNewTypeCoAxiom co_ax_name ty_con tvs [Representational] rhs_ty
pcDataCon :: Name -> [TyVar] -> [Type] -> TyCon -> DataCon
pcDataCon n univs = pcDataConWithFixity False n univs
[] -- no ex_tvs
......@@ -1757,11 +1793,11 @@ extractPromotedList tys = go tys
| otherwise
= pprPanic "extractPromotedList" (ppr tys)
isPromotedListTy :: Type -> Maybe [Type]
isPromotedListTy list_ty
extractPromotedList_maybe :: Type -> Maybe [Type]
extractPromotedList_maybe list_ty
| Just (tc, [_k, t, ts]) <- splitTyConApp_maybe list_ty
, tc `hasKey` consDataConKey
= (t :) <$> isPromotedListTy ts
= (t :) <$> extractPromotedList_maybe ts
| Just (tc, [_k]) <- splitTyConApp_maybe list_ty
, tc `hasKey` nilDataConKey
......
......@@ -19,13 +19,12 @@ import GHC.Builtin.Names ( gHC_DESUGAR
, arrowEnvTyConKey
, arrowEnvDataConKey
, arrowEnvCoAxiomKey
, arrowStackTupTyFamKey
, arrowEnvTupTyFamKey )
, arrowStackTupTyConKey
, arrowEnvTupTyConKey )
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim ( mkTemplateAnonTyConBinders, alphaTyVar, alphaTy )
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom
import GHC.Core.FamInstEnv
import GHC.Core.TyCon
import GHC.Core.Type
import GHC.Data.FastString ( fsLit )
......@@ -33,47 +32,82 @@ import GHC.Data.Pair
import GHC.Tc.Utils.TcType ( tcEqType )
import GHC.Types.Name
{- Note [Arrow type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This module defines two wired-in type families, ArrowStackTup and
ArrowEnvTup, both of which build tuple types from promoted lists:
type ArrowStackTup :: [Type] -> Type
type family ArrowStackTup stk where
ArrowStackTup '[] = ()
ArrowStackTup '[a] = a
ArrowStackTup '[a, b] = (a, b)
ArrowStackTup '[a, b, c] = (a, b, c)
...
type ArrowEnvTup :: Type -> [Type] -> Type
type family ArrowEnvTup env stk = r | r -> env, stk where
ArrowEnvTup env '[] = ArrowEnv env
ArrowEnvTup env '[a] = (ArrowEnv env, a)
ArrowEnvTup env '[a, b] = (ArrowEnv env, a, b)
ArrowEnvTup env '[a, b, c] = (ArrowEnv env, a, b, c)
...
These type families are used to assist in typechecking arrow notation;
see Note [Command typing] in GHC.Tc.Gen.Arrow.
The definitions of these families live in GHC.Desugar, which also
contains the definition of the ArrowEnv newtype:
newtype ArrowEnv env = ArrowEnv env
This newtype’s only purpose is to allow ArrowEnvTup to be injective:
without the wrapping its first equation would overlap with all others.
This is crucial, since it allows information about the shape of the
stack to propagate bidirectionally. See Note [Control operator typing]
in GHC.Tc.Gen.Arrow for the details. -}
arrowTyCons :: [TyCon]
arrowTyCons = [arrowEnvTyCon, arrowStackTupTyCon, arrowEnvTupTyCon]
arrowCoAxiomRules :: [CoAxiomRule]
arrowCoAxiomRules = [axArrowStackTupDef, axArrowEnvTupDef]
-- -------------------------------------------------------------------
-- | > newtype ArrowEnv env = ArrowEnv env
--
-- This newtype’s sole purpose is to allow @ArrowEnvTup@ to be
-- injective; see Note [Arrow type families].
arrowEnvTyCon :: TyCon
arrowEnvCoAxiom :: CoAxiom Unbranched
(arrowEnvTyCon, arrowEnvCoAxiom) = (ty_con, co_ax)
arrowEnvTyCon = pcNewTyCon ty_name arrowEnvDataConKey arrowEnvCoAxiomKey
[alphaTyVar] alphaTy
where
ty_con = mkAlgTyCon name
(mkAnonTyConBinders VisArg tvs)
liftedTypeKind
[Representational]
Nothing
[] -- No stupid theta
rhs
(VanillaAlgTyCon (mkPrelTyConRepName name))
False -- Not in GADT syntax
name = mkWiredInTyConName UserSyntax gHC_DESUGAR (fsLit "ArrowEnv")
arrowEnvTyConKey arrowEnvTyCon
tvs = [alphaTyVar]
rhs_ty = alphaTy
rhs = NewTyCon data_con rhs_ty (tvs, rhs_ty) co_ax False
co_ax_name = mkWiredInName gHC_DESUGAR (mkNewTyCoOcc (nameOccName name))
arrowEnvCoAxiomKey (ACoAxiom (toBranchedAxiom co_ax)) UserSyntax
co_ax = mkNewTypeCoAxiom co_ax_name arrowEnvTyCon tvs
[Representational] rhs_ty
data_con = pcDataCon data_name tvs [rhs_ty] arrowEnvTyCon
data_name = mkWiredInDataConName UserSyntax gHC_DESUGAR (fsLit "ArrowEnv")
arrowEnvDataConKey data_con
ty_name = mkWiredInTyConName UserSyntax gHC_DESUGAR (fsLit "ArrowEnv")
arrowEnvTyConKey arrowEnvTyCon
mkArrowEnvTy :: Type -> Type
mkArrowEnvTy ty = mkTyConApp arrowEnvTyCon [ty]
mkArrowEnvCo :: Type -> CoercionR
mkArrowEnvCo ty = mkUnbranchedAxInstCo Representational arrowEnvCoAxiom [ty] []
mkArrowEnvCo ty
= mkUnbranchedAxInstCo Representational (newTyConCo arrowEnvTyCon) [ty] []
-- -------------------------------------------------------------------
-- | A wired-in type family used to convert the command stack type to
-- a tuple in the typing rule for arrow application. Has the following
-- infinitely-long definition:
--
-- > type ArrowStackTup :: [Type] -> Type
-- > type family ArrowStackTup stk where
-- > ArrowStackTup '[] = ()
-- > ArrowStackTup '[a] = a
-- > ArrowStackTup '[a, b] = (a, b)
-- > ArrowStackTup '[a, b, c] = (a, b, c)
-- > ...
--
-- Also see Note [Arrow type families].
arrowStackTupTyCon :: TyCon
arrowStackTupTyCon =
mkFamilyTyCon name
......@@ -85,7 +119,7 @@ arrowStackTupTyCon =
NotInjective
where
name = mkWiredInTyConName UserSyntax gHC_DESUGAR (fsLit "ArrowStackTup")
arrowStackTupTyFamKey arrowStackTupTyCon
arrowStackTupTyConKey arrowStackTupTyCon
tcb = BuiltInSynFamily
{ sfMatchFam = matchFamArrowStackTup
, sfInteractTop = \_ _ -> []
......@@ -93,7 +127,7 @@ arrowStackTupTyCon =
matchFamArrowStackTup tys = do
[stk_ty] <- pure tys
stk_tys <- isPromotedListTy stk_ty
stk_tys <- extractPromotedList_maybe stk_ty
pure (axArrowStackTupDef, [stk_ty], mkBoxedTupleTy stk_tys)
mkArrowStackTupTy :: Type -> Type
......@@ -106,7 +140,7 @@ axArrowStackTupDef = CoAxiomRule
, coaxrRole = Nominal
, coaxrProves = \cs -> do
[Pair ty1 ty2] <- pure cs
tys2 <- isPromotedListTy ty2
tys2 <- extractPromotedList_maybe ty2
pure (mkArrowStackTupTy ty1 `Pair` mkBoxedTupleTy tys2)
}
......@@ -115,6 +149,22 @@ mkArrowStackTupCo stk_tys
= mkAxiomRuleCo axArrowStackTupDef
[ mkNomReflCo $ mkPromotedListTy liftedTypeKind stk_tys ]
-- -------------------------------------------------------------------
-- | A wired-in type family used to convert the command environment
-- and command stack types to a tuple in the typing rule for arrow
-- control operators. Has the following infinitely-long definition:
--
-- > type ArrowEnvTup :: Type -> [Type] -> Type
-- > type family ArrowEnvTup env stk = r | r -> env, stk where
-- > ArrowEnvTup env '[] = ArrowEnv env
-- > ArrowEnvTup env '[a] = (ArrowEnv env, a)
-- > ArrowEnvTup env '[a, b] = (ArrowEnv env, a, b)
-- > ArrowEnvTup env '[a, b, c] = (ArrowEnv env, a, b, c)
-- > ...
--
-- Also see Note [Arrow type families] and Note [Control operator typing]
-- in GHC.Tc.Gen.Arrow.
arrowEnvTupTyCon :: TyCon
arrowEnvTupTyCon =
mkFamilyTyCon name
......@@ -126,7 +176,7 @@ arrowEnvTupTyCon =
(Injective [True, True])
where
name = mkWiredInTyConName UserSyntax gHC_DESUGAR (fsLit "ArrowEnvTup")
arrowEnvTupTyFamKey arrowEnvTupTyCon
arrowEnvTupTyConKey arrowEnvTupTyCon
tcb = BuiltInSynFamily
{ sfMatchFam = matchFamArrowEnvTup
, sfInteractTop = interactTopArrowEnvTup
......@@ -134,7 +184,7 @@ arrowEnvTupTyCon =
matchFamArrowEnvTup tys = do
[env_ty, stk_ty] <- pure tys
stk_tys <- isPromotedListTy stk_ty
stk_tys <- extractPromotedList_maybe stk_ty
let rhs_ty = mkBoxedTupleTy (mkArrowEnvTy env_ty : stk_tys)
pure (axArrowEnvTupDef, [env_ty, stk_ty], rhs_ty)
......@@ -173,7 +223,7 @@ axArrowEnvTupDef = CoAxiomRule
, coaxrRole = Nominal
, coaxrProves = \cs -> do
[Pair env_ty1 env_ty2, Pair stk_ty1 stk_ty2] <- pure cs
stk_tys2 <- isPromotedListTy stk_ty2
stk_tys2 <- extractPromotedList_maybe stk_ty2
let rhs_ty = mkBoxedTupleTy (mkArrowEnvTy env_ty2 : stk_tys2)
pure (mkArrowEnvTupTy env_ty1 stk_ty1 `Pair` rhs_ty)
}
......
......@@ -104,8 +104,8 @@ There are a few steps to adding a built-in type family:
* Define the type family somewhere
Finally, you will need to define the type family somewhere, likely in @base@.
Currently, all of the built-in type families are defined in GHC.TypeLits or
GHC.TypeNats, so those are likely candidates.
Currently, all of the built-in type families are defined in GHC.Desugar,
GHC.TypeLits, or GHC.TypeNats, so those are likely candidates.
Since the behavior of your built-in type family is specified in GHC.Builtin.Types.Literals,
you should give an open type family definition with no instances, like so:
......@@ -120,7 +120,7 @@ There are a few steps to adding a built-in type family:
type family. For instance:
- The T9181 test prints the :browse contents of GHC.TypeLits, so if you added
a test there, the expected output of T9181 will need to change.
a type there, the expected output of T9181 will need to change.
- The TcTypeNatSimple and TcTypeSymbolSimple tests have compile-time unit
tests, as well as TcTypeNatSimpleRun and TcTypeSymbolSimpleRun, which have
runtime unit tests. Consider adding further unit tests to those if your
......
......@@ -136,7 +136,6 @@ knownKeyNames
concat [ wired_tycon_kk_names funTyCon
, concatMap wired_tycon_kk_names primTyCons
, concatMap wired_tycon_kk_names wiredInTyCons
, concatMap wired_tycon_kk_names arrowTyCons
, concatMap wired_tycon_kk_names typeNatTyCons
, map idName wiredInIds
......
......@@ -8,6 +8,8 @@ Desugaring arrow commands
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.HsToCore.Arrows ( dsProcExpr ) where
#include "HsVersions.h"
......
......@@ -331,9 +331,9 @@ tcProc pat cmd exp_ty
************************************************************************
-}
-- See Note [Arrow overview]
type CmdType = (CmdArgType, TcTauType) -- cmd_type
type CmdArgType = TcTauType -- carg_type, a type-level list
-- See Note [Arrow overview] and Note [Command typing]
type CmdType = (CmdStkType, TcTauType) -- (stk_ty, res_ty)
type CmdStkType = TcTauType -- stk_ty, a type-level list
data CmdEnv
= CmdEnv {
......@@ -431,7 +431,7 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (stk_ty, res_ty)
= addErrCtxt (cmdCtxt cmd) $
do { arg_ty <- select_arrow_scope newOpenFlexiTyVarTy
; let args_ty = mkArrowStackTupTy (consTy arg_ty stk_ty)
; let args_ty = mkArrowStackTupTy (mkConsTy arg_ty stk_ty)
fun_ty = mkCmdArrTy env args_ty res_ty
; fun' <- select_arrow_scope (tcLExpr fun (mkCheckExpType fun_ty))
......@@ -460,7 +460,7 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (stk_ty, res_ty)
tc_cmd env cmd@(HsCmdApp x fun arg) (stk_ty, res_ty)
= addErrCtxt (cmdCtxt cmd) $
do { arg_ty <- newOpenFlexiTyVarTy
; fun' <- tcCmd env fun (consTy arg_ty stk_ty, res_ty)
; fun' <- tcCmd env fun (mkConsTy arg_ty stk_ty, res_ty)
; arg' <- tcLExpr arg (mkCheckExpType arg_ty)
; return (HsCmdApp x fun' arg') }
......@@ -658,8 +658,8 @@ tc_arr_rhs env rhs = do { ty <- newFlexiTyVarTy liftedTypeKind
nilTy :: Type
nilTy = mkTyConApp promotedNilDataCon [liftedTypeKind]
consTy :: Type -> Type -> Type
consTy ty tys = mkTyConApp promotedConsDataCon [liftedTypeKind, ty, tys]
mkConsTy :: Type -> Type -> Type
mkConsTy ty tys = mkTyConApp promotedConsDataCon [liftedTypeKind, ty, tys]
matchConsTy :: TcType -> TcM (TcCoercionN, TcType, TcType)
matchConsTy tys = do
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment