@@ -42,66 +42,86 @@ object Lang:
4242 end Node
4343
4444 abstract class Sum extends Node :
45+ sum =>
4546 type Case <: Node
46- class HasInner [I <: Sum ]
4747 object Opaque :
4848 into opaque type T = Any
4949 extension (t : T )
5050 transparent inline def ex (using
5151 inline ng : NotGiven [ReplaceWith [? ]],
52- )(using et : Sum .EffectiveType [Case ])(using
53- ei : Sum .EffectiveInnerType [Sum .this .type ],
54- ): et.T | ei.T =
55- t.asInstanceOf
52+ )(using et : Sum .EffectiveType [Sum .this .type ]): et.T =
53+ // because it will claim unexhaustive no matter what as of writing :(
54+ t.asInstanceOf .runtimeChecked
5655 end ex
5756 end extension
5857 end Opaque
5958 override type T = Opaque .T
6059
61- inline given subtype : [T ] => (inline ng : NotGiven [ReplaceWith [? ]])
62- => (et : Sum .EffectiveType [Case ])
63- => (ei : Sum .EffectiveInnerType [Sum .this .type ])
64- => InlineConversion .ByCast [et.T | ei.T , this .T ] = InlineConversion .ByCast ()
60+ inline given subtype : (inline ng : NotGiven [ReplaceWith [? ]])
61+ => (et : Sum .EffectiveType [Sum .this .type ])
62+ => InlineConversion .ByCast [et.T , Sum .this .T ] = InlineConversion .ByCast ()
63+
64+ abstract class Extends extends Sum , Selectable :
65+ final type Super = sum.type
66+ end Extends
6567 end Sum
6668
6769 object Sum :
68- sealed trait EffectiveInnerType [S <: Sum ] extends Instanceless :
69- type T
70- end EffectiveInnerType
71- object EffectiveInnerType :
72- type Aux [S <: Sum , T0 ] = EffectiveInnerType [S ] { type T = T0 }
73-
74- inline given noInner : [S <: Sum ] => (S : S )
75- => (inline ng : NotGiven [S .HasInner [? ]])
76- => Aux [S , Nothing ] =
77- Instanceless [Aux [S , Nothing ]]
78-
79- inline given hasInner : [S <: Sum , I <: Sum ] => (S : S )
80- => S .HasInner [I ]
81- => (I : I )
82- => (et : Sum .EffectiveType [I .Case ])
83- => (ie : EffectiveInnerType [I ])
84- => Aux [S , et.T | ie.T ] =
85- Instanceless [Aux [S , et.T | ie.T ]]
86- end EffectiveInnerType
87-
88- sealed trait EffectiveType [C <: Sum # Case ] extends Instanceless :
70+ sealed trait EffectiveType [S <: Sum ] extends Instanceless :
8971 type T
9072 end EffectiveType
73+
9174 object EffectiveType :
92- type Aux [C <: Sum # Case , T0 ] = EffectiveType [C ] {
75+ type Aux [S <: Sum , T0 ] = EffectiveType [S ] {
9376 type T = T0
9477 }
9578
96- inline given inst : [C <: Sum # Case ] => (mirror : Mirror .SumOf [C ])
97- => (tc : TransformedCases [mirror.MirroredElemTypes ])
98- => EffectiveType .Aux [C , Tuple .Union [tc.TC ]] =
99- Instanceless [EffectiveType .Aux [C , Tuple .Union [tc.TC ]]]
79+ inline given inst : [S <: Sum ] => (list : EffectiveTypeList [S ]) => (proj : EffectiveTypeProjection [list.Cases ]) => Aux [S , Tuple .Union [proj.T ]] =
80+ Instanceless [Aux [S , Tuple .Union [proj.T ]]]
81+ end inst
82+
83+ sealed trait EffectiveTypeProjection [Tpl <: Tuple ]:
84+ type T <: Tuple
85+ end EffectiveTypeProjection
86+
87+ object EffectiveTypeProjection :
88+ type Aux [Tpl <: Tuple , T0 <: Tuple ] = EffectiveTypeProjection [Tpl ] {
89+ type T = T0
90+ }
91+
92+ object Aux :
93+ inline def apply [Tpl <: Tuple , T <: Tuple ](): Aux [Tpl , T ] = Instanceless [Aux [Tpl , T ]]
94+ end Aux
95+
96+ inline given empty : Aux [EmptyTuple , EmptyTuple ] = Aux ()
97+
98+ inline given cons : [Hd <: Node , Tl <: Tuple ] => (Hd : Hd ) => (rec : EffectiveTypeProjection [Tl ]) => Aux [Hd *: Tl , Hd .T *: rec.T ] = Aux ()
99+ end EffectiveTypeProjection
100100 end EffectiveType
101101
102+ sealed trait EffectiveTypeList [S <: Sum ] extends Instanceless :
103+ type Cases <: Tuple
104+ end EffectiveTypeList
105+
106+ object EffectiveTypeList :
107+ type Aux [S <: Sum , Cases0 <: Tuple ] = EffectiveTypeList [S ] {
108+ type Cases = Cases0
109+ }
110+ inline def apply [S <: Sum , Cases <: Tuple ](): Aux [S , Cases ] = Instanceless [Aux [S , Cases ]]
111+
112+ inline given instBase : [S <: Sum ] => NotGiven [S <:< Sum # Extends ] => (S : S ) => (mirror : Mirror .SumOf [S .Case ]) => (tc : TransformedCases [mirror.MirroredElemTypes ]) => EffectiveTypeList .Aux [S , tc.TC ] =
113+ EffectiveTypeList ()
114+ end instBase
115+
116+ inline given instExtends : [S <: Sum # Extends ] => (S : S ) => (rec : EffectiveTypeList [S .Super ]) => (mirror : Mirror .SumOf [S .Case ]) => (tc : TransformedCases [mirror.MirroredElemTypes ]) => EffectiveTypeList .Aux [S , Tuple .Concat [rec.Cases , tc.TC ]] =
117+ EffectiveTypeList ()
118+ end instExtends
119+ end EffectiveTypeList
120+
102121 sealed trait TransformedCases [Cases <: Tuple ] extends Instanceless :
103122 type TC <: Tuple
104123 end TransformedCases
124+
105125 object TransformedCases :
106126 type Aux [Cases <: Tuple , TC0 <: Tuple ] = TransformedCases [Cases ] {
107127 type TC = TC0
@@ -112,17 +132,23 @@ object Lang:
112132
113133 inline given empty : TransformedCases .Aux [EmptyTuple , EmptyTuple ] =
114134 TransformedCases ()
135+
115136 inline given cons : [Hd <: Node , Tl <: Tuple ]
116137 => (Hd : Hd )
117138 => (inline ng : NotGiven [Hd .Retract ])
118- => (eht : Lang .EffectiveType [Hd . T ])
139+ => (eht : Lang .EffectiveNodeType [Hd ])
119140 => (ttl : TransformedCases [Tl ])
120- => TransformedCases .Aux [Hd *: Tl , eht.To *: ttl.TC ] = TransformedCases ()
141+ => TransformedCases .Aux [Hd *: Tl , eht.To *: ttl.TC ] =
142+ TransformedCases ()
143+ end cons
144+
121145 inline given consRetracted : [Hd <: Node , Tl <: Tuple ]
122146 => (Hd : Hd )
123147 => Hd .Retract
124148 => (ttl : TransformedCases [Tl ])
125- => TransformedCases .Aux [Hd *: Tl , ttl.TC ] = TransformedCases ()
149+ => TransformedCases .Aux [Hd *: Tl , ttl.TC ] =
150+ TransformedCases ()
151+ end consRetracted
126152 end TransformedCases
127153 end Sum
128154
@@ -161,6 +187,7 @@ object Lang:
161187 sealed trait EffectiveNodeType [From <: Node ] extends Instanceless :
162188 type To <: Node
163189 end EffectiveNodeType
190+
164191 object EffectiveNodeType :
165192 type Aux [From <: Node , To0 <: Node ] = EffectiveNodeType [From ] {
166193 type To = To0
@@ -182,6 +209,7 @@ object Lang:
182209 sealed trait EffectiveType [From ] extends Instanceless :
183210 type To
184211 end EffectiveType
212+
185213 object EffectiveType :
186214 type Aux [From , To0 ] = EffectiveType [From ] {
187215 type To = To0
@@ -207,6 +235,7 @@ object Lang:
207235 trait EffectiveTupleType [From <: Tuple ]:
208236 type To <: Tuple
209237 end EffectiveTupleType
238+
210239 object EffectiveTupleType :
211240 type Aux [From <: Tuple , To0 <: Tuple ] = EffectiveTupleType [From ] {
212241 type To = To0
@@ -303,20 +332,23 @@ object Test:
303332
304333 object Ping extends Lang .Sum :
305334 sealed trait Case extends Lang .Node
306- object Pong extends Lang .Term [(k : Int , foo : Foo .T )], Case
307- object Bob extends Lang .Term [(k : Int , foo : Foo .T )], Case
335+ object Case :
336+ object Pong extends Lang .Term [(k : Int , foo : Foo .T )], Case
337+ object Bob extends Lang .Term [(k : Int , foo : Foo .T )], Case
338+ export Case .*
308339 end Ping
309340 end L1
310341 object L1 extends L1
311342
312343 trait L2 extends Lang .Extend [L1 ]:
313344 export up .{Foo as _ , Ping as _ , * }
314345 object Bar extends Lang .Term [(s : String , opt : Option [up.Foo .T ])]
315- object Ping extends Lang .Sum :
316- given HasInner [up.Ping .type ]()
317- export up .Ping .{Case as _ , Opaque as _ , * }
346+ object Ping extends up.Ping .Extends :
318347 sealed trait Case extends Lang .Node
319- object NewCase extends Lang .Term [(s : String , opt : Option [up.Foo .T ])], Case
348+ object Case :
349+ export up .Ping .Case .*
350+ object NewCase extends Lang .Term [(s : String , opt : Option [up.Foo .T ])], Case
351+ export Case .*
320352 end Ping
321353
322354 given up .Foo .ReplaceWith [Bar .type ]()
0 commit comments