[Git][ghc/ghc][wip/T21623] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sat Sep 17 18:48:14 UTC 2022
Simon Peyton Jones pushed to branch wip/T21623 at Glasgow Haskell Compiler / GHC
Commits:
5924c88f by Simon Peyton Jones at 2022-09-17T19:48:23+01:00
Wibbles
- - - - -
12 changed files:
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Hs/Type.hs
- testsuite/tests/callarity/unittest/CallArity1.hs
- testsuite/tests/roles/should_compile/Roles14.stderr
- testsuite/tests/roles/should_compile/Roles3.stderr
- testsuite/tests/roles/should_compile/Roles4.stderr
- testsuite/tests/roles/should_compile/T8958.stderr
- testsuite/tests/saks/should_compile/saks007.hs
- testsuite/tests/stranal/should_compile/T18982.stderr
- testsuite/tests/typecheck/should_compile/T17021a.hs
Changes:
=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -592,6 +592,31 @@ but dcRepArity does. For example:
Note [DataCon user type variable binders]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A DataCon has two different sets of type variables:
+
+* dcUserTyVarBinders, for the type variables binders in the order in which they
+ originally arose in the user-written type signature.
+
+ - They are the forall'd binders of the data con /wrapper/, which the user calls.
+
+ - Their order *does* matter for TypeApplications, so they are full TyVarBinders,
+ complete with visibilities.
+
+* dcUnivTyVars and dcExTyCoVars, for the "true underlying" (i.e. of the data
+ con worker) universal type variable and existential type/coercion variables,
+ respectively.
+
+ - They (i.e. univ ++ ex) are the forall'd variables of the data con /worker/
+
+ - Their order is irrelevant for the purposes of TypeApplications,
+ and as a consequence, they do not come equipped with visibilities
+ (that is, they are TyVars/TyCoVars instead of ForAllTyBinders).
+
+Often (dcUnivTyVars ++ dcExTyCoVars) = dcUserTyVarBinder; but they may differ
+for two reasons, coming next:
+
+--- Reason (R1): Order of quantification in GADT syntax ---
+
In System FC, data constructor type signatures always quantify over all of
their universal type variables, followed by their existential type variables.
Normally, this isn't a problem, as most datatypes naturally quantify their type
@@ -634,27 +659,27 @@ according to the rules of TypeApplications, in the absence of `forall` GHC
performs a stable topological sort on the type variables in the user-written
type signature, which would place `b` before `a`.
-But as noted above, enacting this behavior is not entirely trivial, as System
-FC demands the variables go in universal-then-existential order under the hood.
-Our solution is thus to equip DataCon with two different sets of type
-variables:
+--- Reason (R2): GADTs introduce new existentials ---
-* dcUnivTyVars and dcExTyCoVars, for the universal type variable and existential
- type/coercion variables, respectively. Their order is irrelevant for the
- purposes of TypeApplications, and as a consequence, they do not come equipped
- with visibilities (that is, they are TyVars/TyCoVars instead of
- ForAllTyBinders).
+GADTs may also introduce extra existentials. Consider
+ data T a b where
+ MkT :: forall c d. c -> T [c] d
-* dcUserTyVarBinders, for the type variables binders in the order in which they
- originally arose in the user-written type signature. Their order *does* matter
- for TypeApplications, so they are full TyVarBinders, complete with
- visibilities.
+Then we make up a fresh universal, say 'a', to be the first argument to T in
+the result, and get this type for the "true underlying" worker data con:
+
+ MkT :: forall a d. forall c. (a ~# [c]) => c -> T a d
-This encoding has some redundancy. The set of tyvars in dcUserTyVarBinders
+(We don't need to make up a fresh tyvar for the second arg; 'd' will do.)
+
+End of Reasons
+
+Invariant: the set of tyvars in dcUserTyVarBinders
consists precisely of:
* The set of tyvars in dcUnivTyVars whose type variables do not appear in
dcEqSpec, unioned with:
+
* The set of tyvars (*not* covars) in dcExTyCoVars
No covars here because because they're not user-written
@@ -1687,7 +1712,6 @@ dataConUnconstrainedTyVars (MkData { dcUnivTyVars = univ_tvs
, dcExTyCoVars = ex_tvs
, dcEqSpec = eq_spec })
= [ univ_tv | univ_tv <- univ_tvs
- , not (isConstraintLikeKind (typeKind (tyVarKind univ_tv)))
, not (univ_tv `elemUnVarSet` eq_spec_tvs) ]
++ ex_tvs
where
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -657,11 +657,11 @@ See #15710 about that.
Note [Unused coercion variable in ForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
- \(co:t1 ~ t2). e
+ \(co:t1 ~# t2). e
-What type should we give to this expression?
- (1) forall (co:t1 ~ t2) -> t
- (2) (t1 ~ t2) -> t
+What type should we give to the above expression?
+ (1) forall (co:t1 ~# t2) -> t
+ (2) (t1 ~# t2) -> t
If co is used in t, (1) should be the right choice.
if co is not used in t, we would like to have (1) and (2) equivalent.
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -2517,8 +2517,7 @@ seqTypes (ty:tys) = seqType ty `seq` seqTypes tys
Note [Kinding rules for types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In typeKind we consider Constraint and (TYPE LiftedRep) to be identical.
-We then have
+Here are the kinding rules for types
t1 : TYPE rep1
t2 : TYPE rep2
=====================================
compiler/GHC/Hs/Type.hs
=====================================
@@ -115,6 +115,7 @@ import GHC.Types.Basic
import GHC.Types.SrcLoc
import GHC.Utils.Outputable
import GHC.Utils.Misc (count)
+import GHC.Utils.Trace
import Data.Maybe
import Data.Data (Data)
@@ -1138,7 +1139,8 @@ ppr_mono_ty (HsQualTy { hst_ctxt = ctxt, hst_body = ty })
ppr_mono_ty (HsBangTy _ b ty) = ppr b <> ppr_mono_lty ty
ppr_mono_ty (HsRecTy _ flds) = pprConDeclFields flds
-ppr_mono_ty (HsTyVar _ prom (L _ name)) = pprOccWithTick Prefix prom name
+ppr_mono_ty (HsTyVar _ prom (L _ name)) = pprTrace "ppr_mono" (ppr name) $
+ pprOccWithTick Prefix prom name
ppr_mono_ty (HsFunTy _ mult ty1 ty2) = ppr_fun_ty mult ty1 ty2
ppr_mono_ty (HsTupleTy _ con tys)
-- Special-case unary boxed tuples so that they are pretty-printed as
=====================================
testsuite/tests/callarity/unittest/CallArity1.hs
=====================================
@@ -3,7 +3,7 @@ import GHC.Core
import GHC.Core.Utils
import GHC.Types.Id
import GHC.Core.Type
-import GHC.Core.Multiplicity ( pattern Many )
+import GHC.Core.Multiplicity ( pattern ManyTy )
import GHC.Core.Make
import GHC.Core.Opt.CallArity (callArityRHS)
import GHC.Types.Id.Make
@@ -192,7 +192,7 @@ mkLApps v = mkApps (Var v) . map mkLit
mkACase = mkIfThenElse (mkVarApps (Var scrutf) [scruta])
mkTestId :: Int -> String -> Type -> Id
-mkTestId i s ty = mkSysLocal (mkFastString s) (mkBuiltinUnique i) Many ty
+mkTestId i s ty = mkSysLocal (mkFastString s) (mkBuiltinUnique i) ManyTy ty
mkTestIds :: [String] -> [Type] -> [Id]
mkTestIds ns tys = zipWith3 mkTestId [0..] ns tys
=====================================
testsuite/tests/roles/should_compile/Roles14.stderr
=====================================
@@ -6,7 +6,7 @@ TYPE CONSTRUCTORS
COERCION AXIOMS
axiom Roles12.N:C2 :: C2 a = a -> a
Dependent modules: []
-Dependent packages: [base-4.16.0.0]
+Dependent packages: [base-4.17.0.0]
==================== Typechecker ====================
Roles12.$tcC2
@@ -17,14 +17,13 @@ Roles12.$tc'C:C2
= GHC.Types.TyCon
7087988437584478859##64 11477953550142401435##64 Roles12.$trModule
(GHC.Types.TrNameS "'C:C2"#) 1# $krep
+$krep [InlPrag=[~]]
+ = GHC.Types.KindRepTyConApp Roles12.$tcC2 ((:) $krep [])
$krep [InlPrag=[~]] = GHC.Types.KindRepVar 0
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp GHC.Types.$tcConstraint []
-$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp Roles12.$tcC2 ((:) $krep [])
+ = GHC.Types.KindRepFun GHC.Types.krep$* GHC.Types.krep$Constraint
Roles12.$trModule
= GHC.Types.Module
(GHC.Types.TrNameS "main"#) (GHC.Types.TrNameS "Roles12"#)
=====================================
testsuite/tests/roles/should_compile/Roles3.stderr
=====================================
@@ -21,7 +21,7 @@ COERCION AXIOMS
axiom Roles3.N:C3 :: C3 a b = a -> F3 b -> F3 b
axiom Roles3.N:C4 :: C4 a b = a -> F4 b -> F4 b
Dependent modules: []
-Dependent packages: [base-4.16.0.0]
+Dependent packages: [base-4.17.0.0]
==================== Typechecker ====================
Roles3.$tcC4
@@ -48,24 +48,23 @@ Roles3.$tc'C:C1
= GHC.Types.TyCon
4508088879886988796##64 13962145553903222779##64 Roles3.$trModule
(GHC.Types.TrNameS "'C:C1"#) 1# $krep
+$krep [InlPrag=[~]]
+ = GHC.Types.KindRepTyConApp
+ GHC.Types.$tc~ ((:) GHC.Types.krep$* ((:) $krep ((:) $krep [])))
+$krep [InlPrag=[~]]
+ = GHC.Types.KindRepTyConApp Roles3.$tcC2 ((:) $krep ((:) $krep []))
+$krep [InlPrag=[~]]
+ = GHC.Types.KindRepTyConApp Roles3.$tcC1 ((:) $krep [])
$krep [InlPrag=[~]] = GHC.Types.KindRepVar 0
$krep [InlPrag=[~]] = GHC.Types.KindRepVar 1
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
-$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
+$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp GHC.Types.$tcConstraint []
+ = GHC.Types.KindRepFun GHC.Types.krep$* GHC.Types.krep$Constraint
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp
- GHC.Types.$tc~ ((:) GHC.Types.krep$* ((:) $krep ((:) $krep [])))
-$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp Roles3.$tcC2 ((:) $krep ((:) $krep []))
-$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp Roles3.$tcC1 ((:) $krep [])
Roles3.$trModule
= GHC.Types.Module
(GHC.Types.TrNameS "main"#) (GHC.Types.TrNameS "Roles3"#)
=====================================
testsuite/tests/roles/should_compile/Roles4.stderr
=====================================
@@ -9,7 +9,7 @@ COERCION AXIOMS
axiom Roles4.N:C1 :: C1 a = a -> a
axiom Roles4.N:C3 :: C3 a = a -> Syn1 a
Dependent modules: []
-Dependent packages: [base-4.16.0.0]
+Dependent packages: [base-4.17.0.0]
==================== Typechecker ====================
Roles4.$tcC3
@@ -28,20 +28,19 @@ Roles4.$tc'C:C1
= GHC.Types.TyCon
3870707671502302648##64 10631907186261837450##64 Roles4.$trModule
(GHC.Types.TrNameS "'C:C1"#) 1# $krep
+$krep [InlPrag=[~]]
+ = GHC.Types.KindRepTyConApp Roles4.$tcC3 ((:) $krep [])
+$krep [InlPrag=[~]]
+ = GHC.Types.KindRepTyConApp Roles4.$tcC1 ((:) $krep [])
$krep [InlPrag=[~]] = GHC.Types.KindRepVar 0
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
-$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp GHC.Types.$tcList ((:) $krep [])
-$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp GHC.Types.$tcConstraint []
$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp Roles4.$tcC3 ((:) $krep [])
+ = GHC.Types.KindRepFun GHC.Types.krep$* GHC.Types.krep$Constraint
$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp Roles4.$tcC1 ((:) $krep [])
+ = GHC.Types.KindRepTyConApp GHC.Types.$tcList ((:) $krep [])
Roles4.$trModule
= GHC.Types.Module
(GHC.Types.TrNameS "main"#) (GHC.Types.TrNameS "Roles4"#)
=====================================
testsuite/tests/roles/should_compile/T8958.stderr
=====================================
@@ -16,7 +16,7 @@ CLASS INSTANCES
-- Defined at T8958.hs:11:10
instance [incoherent] Nominal a -- Defined at T8958.hs:8:10
Dependent modules: []
-Dependent packages: [base-4.16.0.0]
+Dependent packages: [base-4.17.0.0]
==================== Typechecker ====================
T8958.$tcMap
@@ -46,7 +46,8 @@ T8958.$tc'C:Nominal
$krep [InlPrag=[~]] = GHC.Types.KindRepVar 0
$krep [InlPrag=[~]] = GHC.Types.KindRepVar 1
$krep [InlPrag=[~]] = GHC.Types.KindRepFun $krep $krep
-$krep [InlPrag=[~]] = GHC.Types.KindRepFun GHC.Types.krep$* $krep
+$krep [InlPrag=[~]]
+ = GHC.Types.KindRepFun GHC.Types.krep$* GHC.Types.krep$Constraint
$krep [InlPrag=[~]]
= GHC.Types.KindRepTyConApp
GHC.Tuple.$tc(,)
@@ -61,9 +62,6 @@ $krep [InlPrag=[~]]
= GHC.Types.KindRepTyConApp
GHC.Types.$tcList
((:) @GHC.Types.KindRep $krep [] @GHC.Types.KindRep)
-$krep [InlPrag=[~]]
- = GHC.Types.KindRepTyConApp
- GHC.Types.$tcConstraint [] @GHC.Types.KindRep
$krep [InlPrag=[~]]
= GHC.Types.KindRepTyConApp
T8958.$tcRepresentational
=====================================
testsuite/tests/saks/should_compile/saks007.hs
=====================================
@@ -13,3 +13,28 @@ type X :: forall k1 k2. (F k1 ~ G k2) => k1 -> k2 -> Type
data X a b where
MkX :: X Integer Maybe -- OK: F Type ~ G (Type -> Type)
-- True ~ True
+
+
+{-
+Let co :: F Type ~ G (Type->Type)
+
+Wrapper data con type:
+ $WMkX :: X @Type @(Type->Type) @(Eq# co) Integer Maybe
+
+Worker data con's type:
+ MkX :: forall k1 k2 (c :: F k1 ~ G k2) (a :: k1) (b :: k2)
+ -> forall . -- No existentials
+ ( k1 ~# Type, k2 ~# Type->Type -- EqSpec
+ , a ~# Integer, b ~# Maybe )
+ => X k1 k2 c a b
+
+f :: forall k. (k ~ Type) => forall (a::k). a->a
+
+
+f :: forall (cv :: a ~# b) => ....ty|>co....
+
+
+X @kk1 @kk2 @(d :: F kk1 ~ G kk2) Integer Maybe
+
+
+-}
\ No newline at end of file
=====================================
testsuite/tests/stranal/should_compile/T18982.stderr
=====================================
@@ -4,15 +4,15 @@ Result size of Tidy Core = {terms: 311, types: 214, coercions: 4, joins: 0/0}
-- RHS size: {terms: 8, types: 9, coercions: 1, joins: 0/0}
T18982.$WExGADT :: forall e. (e ~ Int) => e %1 -> Int %1 -> ExGADT Int
-T18982.$WExGADT = \ (@e) (dt :: e ~ Int) (dt :: e) (dt :: Int) -> T18982.ExGADT @Int @e @~(<Int>_N :: Int GHC.Prim.~# Int) dt dt dt
+T18982.$WExGADT = \ (@e) (conrep :: e ~ Int) (conrep :: e) (conrep :: Int) -> T18982.ExGADT @Int @e @~(<Int>_N :: Int GHC.Prim.~# Int) conrep conrep conrep
-- RHS size: {terms: 3, types: 2, coercions: 1, joins: 0/0}
T18982.$WGADT :: Int %1 -> GADT Int
-T18982.$WGADT = \ (dt :: Int) -> T18982.GADT @Int @~(<Int>_N :: Int GHC.Prim.~# Int) dt
+T18982.$WGADT = \ (conrep :: Int) -> T18982.GADT @Int @~(<Int>_N :: Int GHC.Prim.~# Int) conrep
-- RHS size: {terms: 7, types: 6, coercions: 0, joins: 0/0}
T18982.$WEx :: forall e a. e %1 -> a %1 -> Ex a
-T18982.$WEx = \ (@e) (@a) (dt :: e) (dt :: a) -> T18982.Ex @a @e dt dt
+T18982.$WEx = \ (@e) (@a) (conrep :: e) (conrep :: a) -> T18982.Ex @a @e conrep conrep
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18982.$trModule4 :: GHC.Prim.Addr#
@@ -72,7 +72,7 @@ T18982.$tcBox1 = GHC.Types.TrNameS T18982.$tcBox2
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
T18982.$tcBox :: GHC.Types.TyCon
-T18982.$tcBox = GHC.Types.TyCon 16948648223906549518## 2491460178135962649## T18982.$trModule T18982.$tcBox1 0# GHC.Types.krep$*Arr*
+T18982.$tcBox = GHC.Types.TyCon 16948648223906549518##64 2491460178135962649##64 T18982.$trModule T18982.$tcBox1 0# GHC.Types.krep$*Arr*
-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
$krep7 :: [GHC.Types.KindRep]
@@ -96,7 +96,7 @@ T18982.$tc'Box2 = GHC.Types.TrNameS T18982.$tc'Box3
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'Box :: GHC.Types.TyCon
-T18982.$tc'Box = GHC.Types.TyCon 1412068769125067428## 8727214667407894081## T18982.$trModule T18982.$tc'Box2 1# T18982.$tc'Box1
+T18982.$tc'Box = GHC.Types.TyCon 1412068769125067428##64 8727214667407894081##64 T18982.$trModule T18982.$tc'Box2 1# T18982.$tc'Box1
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18982.$tcEx2 :: GHC.Prim.Addr#
@@ -108,7 +108,7 @@ T18982.$tcEx1 = GHC.Types.TrNameS T18982.$tcEx2
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
T18982.$tcEx :: GHC.Types.TyCon
-T18982.$tcEx = GHC.Types.TyCon 4376661818164435927## 18005417598910668817## T18982.$trModule T18982.$tcEx1 0# GHC.Types.krep$*Arr*
+T18982.$tcEx = GHC.Types.TyCon 4376661818164435927##64 18005417598910668817##64 T18982.$trModule T18982.$tcEx1 0# GHC.Types.krep$*Arr*
-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
$krep9 :: [GHC.Types.KindRep]
@@ -136,7 +136,7 @@ T18982.$tc'Ex2 = GHC.Types.TrNameS T18982.$tc'Ex3
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'Ex :: GHC.Types.TyCon
-T18982.$tc'Ex = GHC.Types.TyCon 14609381081172201359## 3077219645053200509## T18982.$trModule T18982.$tc'Ex2 2# T18982.$tc'Ex1
+T18982.$tc'Ex = GHC.Types.TyCon 14609381081172201359##64 3077219645053200509##64 T18982.$trModule T18982.$tc'Ex2 2# T18982.$tc'Ex1
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18982.$tcGADT2 :: GHC.Prim.Addr#
@@ -148,7 +148,7 @@ T18982.$tcGADT1 = GHC.Types.TrNameS T18982.$tcGADT2
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
T18982.$tcGADT :: GHC.Types.TyCon
-T18982.$tcGADT = GHC.Types.TyCon 9243924476135839950## 5096619276488416461## T18982.$trModule T18982.$tcGADT1 0# GHC.Types.krep$*Arr*
+T18982.$tcGADT = GHC.Types.TyCon 9243924476135839950##64 5096619276488416461##64 T18982.$trModule T18982.$tcGADT1 0# GHC.Types.krep$*Arr*
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep12 :: GHC.Types.KindRep
@@ -168,7 +168,7 @@ T18982.$tc'GADT2 = GHC.Types.TrNameS T18982.$tc'GADT3
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'GADT :: GHC.Types.TyCon
-T18982.$tc'GADT = GHC.Types.TyCon 2077850259354179864## 16731205864486799217## T18982.$trModule T18982.$tc'GADT2 0# T18982.$tc'GADT1
+T18982.$tc'GADT = GHC.Types.TyCon 2077850259354179864##64 16731205864486799217##64 T18982.$trModule T18982.$tc'GADT2 0# T18982.$tc'GADT1
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18982.$tcExGADT2 :: GHC.Prim.Addr#
@@ -180,7 +180,7 @@ T18982.$tcExGADT1 = GHC.Types.TrNameS T18982.$tcExGADT2
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
T18982.$tcExGADT :: GHC.Types.TyCon
-T18982.$tcExGADT = GHC.Types.TyCon 6470898418160489500## 10361108917441214060## T18982.$trModule T18982.$tcExGADT1 0# GHC.Types.krep$*Arr*
+T18982.$tcExGADT = GHC.Types.TyCon 6470898418160489500##64 10361108917441214060##64 T18982.$trModule T18982.$tcExGADT1 0# GHC.Types.krep$*Arr*
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
$krep13 :: GHC.Types.KindRep
@@ -208,10 +208,10 @@ T18982.$tc'ExGADT2 = GHC.Types.TrNameS T18982.$tc'ExGADT3
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'ExGADT :: GHC.Types.TyCon
-T18982.$tc'ExGADT = GHC.Types.TyCon 8468257409157161049## 5503123603717080600## T18982.$trModule T18982.$tc'ExGADT2 1# T18982.$tc'ExGADT1
+T18982.$tc'ExGADT = GHC.Types.TyCon 8468257409157161049##64 5503123603717080600##64 T18982.$trModule T18982.$tc'ExGADT2 1# T18982.$tc'ExGADT1
-- RHS size: {terms: 11, types: 10, coercions: 0, joins: 0/0}
-T18982.$wi :: forall {a} {e}. (a GHC.Prim.~# Int) -> e -> GHC.Prim.Int# -> GHC.Prim.Int#
+T18982.$wi :: forall {a} {e}. (a GHC.Prim.~# Int) => e -> GHC.Prim.Int# -> GHC.Prim.Int#
T18982.$wi = \ (@a) (@e) (ww :: a GHC.Prim.~# Int) (ww1 :: e) (ww2 :: GHC.Prim.Int#) -> case ww1 of { __DEFAULT -> GHC.Prim.+# ww2 1# }
-- RHS size: {terms: 15, types: 22, coercions: 1, joins: 0/0}
@@ -219,7 +219,7 @@ i :: forall a. ExGADT a -> Int
i = \ (@a) (ds :: ExGADT a) -> case ds of { ExGADT @e ww ww1 ww2 ww3 -> case ww3 of { GHC.Types.I# ww4 -> case T18982.$wi @a @e @~(ww :: a GHC.Prim.~# Int) ww2 ww4 of ww5 { __DEFAULT -> GHC.Types.I# ww5 } } }
-- RHS size: {terms: 6, types: 7, coercions: 0, joins: 0/0}
-T18982.$wh :: forall {a}. (a GHC.Prim.~# Int) -> GHC.Prim.Int# -> GHC.Prim.Int#
+T18982.$wh :: forall {a}. (a GHC.Prim.~# Int) => GHC.Prim.Int# -> GHC.Prim.Int#
T18982.$wh = \ (@a) (ww :: a GHC.Prim.~# Int) (ww1 :: GHC.Prim.Int#) -> GHC.Prim.+# ww1 1#
-- RHS size: {terms: 14, types: 15, coercions: 1, joins: 0/0}
=====================================
testsuite/tests/typecheck/should_compile/T17021a.hs
=====================================
@@ -9,8 +9,16 @@ import GHC.Exts
type family Id x where
Id x = x
-type LevId :: TYPE (Id LiftedRep) -> TYPE (Id LiftedRep)
-newtype LevId x = MkLevId x
+--type LevId :: TYPE (Id LiftedRep) -> TYPE (Id LiftedRep)
+--newtype LevId x = MkLevId x
-type LevId2 :: (r ~ Id LiftedRep) => TYPE r -> TYPE r
+otype LevId2 :: (r ~ Id LiftedRep) => TYPE r -> TYPE r
newtype LevId2 x = MkLevId2 x
+
+{-
+MkLevId2 :: forall (r :: RuntimeRep).
+ forall (c :: r ~ Id LiftedRep) -> -- c is a TyVar
+ forall (x :: TYPE r).
+ x -> LevId2 @r @c x
+
+-}
\ No newline at end of file
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5924c88f91db71653fb83ffe2bd7afa828605c5e
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5924c88f91db71653fb83ffe2bd7afa828605c5e
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20220917/dd858388/attachment-0001.html>
More information about the ghc-commits
mailing list