@@ -131,6 +131,57 @@ pattern DefaultUniArray uniA =
131131pattern DefaultUniPair uniA uniB =
132132 DefaultUniProtoPair `DefaultUniApply ` uniA `DefaultUniApply ` uniB
133133
134+ -- Removing 'LoopBreaker' didn't change anything at the time this comment was written, but we kept
135+ -- it, because it hopefully provides some additional assurance that 'geqL' will not get elaborated
136+ -- as a recursive definition.
137+ instance AllBuiltinArgs DefaultUni (GEqL DefaultUni ) a => GEqL DefaultUni a where
138+ geqL DefaultUniInteger a2 = do
139+ DefaultUniInteger <- pure a2
140+ pure Refl
141+ geqL DefaultUniByteString a2 = do
142+ DefaultUniByteString <- pure a2
143+ pure Refl
144+ geqL DefaultUniString a2 = do
145+ DefaultUniString <- pure a2
146+ pure Refl
147+ geqL DefaultUniUnit a2 = do
148+ DefaultUniUnit <- pure a2
149+ pure Refl
150+ geqL DefaultUniBool a2 = do
151+ DefaultUniBool <- pure a2
152+ pure Refl
153+ geqL (DefaultUniProtoList `DefaultUniApply ` a1) listA2 = do
154+ DefaultUniProtoList `DefaultUniApply ` a2 <- pure listA2
155+ Refl <- geqL (LoopBreaker a1) (LoopBreaker a2)
156+ pure Refl
157+ geqL (DefaultUniProtoArray `DefaultUniApply ` a1) arrayA2 = do
158+ DefaultUniProtoArray `DefaultUniApply ` a2 <- pure arrayA2
159+ Refl <- geqL (LoopBreaker a1) (LoopBreaker a2)
160+ pure Refl
161+ geqL (DefaultUniProtoPair `DefaultUniApply ` a1 `DefaultUniApply ` b1) pairA2 = do
162+ DefaultUniProtoPair `DefaultUniApply ` a2 `DefaultUniApply ` b2 <- pure pairA2
163+ Refl <- geqL (LoopBreaker a1) (LoopBreaker a2)
164+ Refl <- geqL (LoopBreaker b1) (LoopBreaker b2)
165+ pure Refl
166+ geqL (f `DefaultUniApply ` _ `DefaultUniApply ` _ `DefaultUniApply ` _) _ =
167+ noMoreTypeFunctions f
168+ geqL DefaultUniData a2 = do
169+ DefaultUniData <- pure a2
170+ pure Refl
171+ geqL DefaultUniBLS12_381_G1_Element a2 = do
172+ DefaultUniBLS12_381_G1_Element <- pure a2
173+ pure Refl
174+ geqL DefaultUniBLS12_381_G2_Element a2 = do
175+ DefaultUniBLS12_381_G2_Element <- pure a2
176+ pure Refl
177+ geqL DefaultUniBLS12_381_MlResult a2 = do
178+ DefaultUniBLS12_381_MlResult <- pure a2
179+ pure Refl
180+ geqL DefaultUniValue a2 = do
181+ DefaultUniValue <- pure a2
182+ pure Refl
183+ {-# INLINE geqL #-}
184+
134185instance GEq DefaultUni where
135186 -- We define 'geq' manually instead of using 'deriveGEq', because the latter creates a single
136187 -- recursive definition and we want two instead. The reason why we want two is because this
@@ -140,59 +191,63 @@ instance GEq DefaultUni where
140191 -- (we're not really sure if this is a reliable solution, but if it stops working, we won't miss
141192 -- very much and we've failed to settle on any other approach).
142193 --
143- -- This trick gives us a 1% speedup across validation benchmarks (some are up to 4% faster) and
144- -- a more sensible generated Core where things like @geq DefaulUniBool@ are reduced away.
145- geq = geqStep where
146- geqStep :: DefaultUni a1 -> DefaultUni a2 -> Maybe a1 :~: a2 )
147- geqStep DefaultUniInteger a2 = do
148- DefaultUniInteger <- Just a2
149- Just Refl
150- geqStep DefaultUniByteString a2 = do
151- DefaultUniByteString <- Just a2
152- Just Refl
153- geqStep DefaultUniString a2 = do
154- DefaultUniString <- Just a2
155- Just Refl
156- geqStep DefaultUniUnit a2 = do
157- DefaultUniUnit <- Just a2
158- Just Refl
159- geqStep DefaultUniBool a2 = do
160- DefaultUniBool <- Just a2
161- Just Refl
162- geqStep DefaultUniProtoList a2 = do
163- DefaultUniProtoList <- Just a2
164- Just Refl
165- geqStep DefaultUniProtoArray a2 = do
166- DefaultUniProtoArray <- Just a2
167- Just Refl
168- geqStep DefaultUniProtoPair a2 = do
169- DefaultUniProtoPair <- Just a2
170- Just Refl
171- geqStep (DefaultUniApply f1 x1) a2 = do
172- DefaultUniApply f2 x2 <- Just a2
173- Refl <- geqRec f1 f2
174- Refl <- geqRec x1 x2
175- Just Refl
176- geqStep DefaultUniData a2 = do
177- DefaultUniData <- Just a2
178- Just Refl
179- geqStep DefaultUniBLS12_381_G1_Element a2 = do
180- DefaultUniBLS12_381_G1_Element <- Just a2
181- Just Refl
182- geqStep DefaultUniBLS12_381_G2_Element a2 = do
183- DefaultUniBLS12_381_G2_Element <- Just a2
184- Just Refl
185- geqStep DefaultUniBLS12_381_MlResult a2 = do
186- DefaultUniBLS12_381_MlResult <- Just a2
187- Just Refl
188- geqStep DefaultUniValue a2 = do
189- DefaultUniValue <- Just a2
190- Just Refl
191- {-# INLINE geqStep #-}
192-
193- geqRec :: DefaultUni a1 -> DefaultUni a2 -> Maybe a1 :~: a2 )
194- geqRec = geqStep
195- {-# OPAQUE geqRec #-}
194+ -- On the critical path this definition should only be used for builtins that perform equality
195+ -- checking of statically unknown runtime type tags ('MkCons' is one such builtin for
196+ -- example). All other builtins should use 'geqL' (the latter is internal to 'readKnownConstant'
197+ -- and is therefore hidden from the person adding a new builtin).
198+ --
199+ -- We use @NOINLINE@ instead of @OPAQUE@, because we don't actually care about the recursive
200+ -- definition not being inlined, we just want it to be chosen as the loop breaker.
201+ geq = goStep where
202+ goStep , goRec :: DefaultUni a1 -> DefaultUni a2 -> Maybe a1 :~: a2 )
203+ goStep DefaultUniInteger a2 = do
204+ DefaultUniInteger <- pure a2
205+ pure Refl
206+ goStep DefaultUniByteString a2 = do
207+ DefaultUniByteString <- pure a2
208+ pure Refl
209+ goStep DefaultUniString a2 = do
210+ DefaultUniString <- pure a2
211+ pure Refl
212+ goStep DefaultUniUnit a2 = do
213+ DefaultUniUnit <- pure a2
214+ pure Refl
215+ goStep DefaultUniBool a2 = do
216+ DefaultUniBool <- pure a2
217+ pure Refl
218+ goStep DefaultUniProtoList a2 = do
219+ DefaultUniProtoList <- pure a2
220+ pure Refl
221+ goStep DefaultUniProtoArray a2 = do
222+ DefaultUniProtoArray <- pure a2
223+ pure Refl
224+ goStep DefaultUniProtoPair a2 = do
225+ DefaultUniProtoPair <- pure a2
226+ pure Refl
227+ goStep (DefaultUniApply f1 x1) a2 = do
228+ DefaultUniApply f2 x2 <- pure a2
229+ Refl <- goRec f1 f2
230+ Refl <- goRec x1 x2
231+ pure Refl
232+ goStep DefaultUniData a2 = do
233+ DefaultUniData <- pure a2
234+ pure Refl
235+ goStep DefaultUniBLS12_381_G1_Element a2 = do
236+ DefaultUniBLS12_381_G1_Element <- pure a2
237+ pure Refl
238+ goStep DefaultUniBLS12_381_G2_Element a2 = do
239+ DefaultUniBLS12_381_G2_Element <- pure a2
240+ pure Refl
241+ goStep DefaultUniBLS12_381_MlResult a2 = do
242+ DefaultUniBLS12_381_MlResult <- pure a2
243+ pure Refl
244+ goStep DefaultUniValue a2 = do
245+ DefaultUniValue <- pure a2
246+ pure Refl
247+ {-# INLINE goStep #-}
248+
249+ goRec = goStep
250+ {-# NOINLINE goRec #-}
196251
197252-- | For pleasing the coverage checker.
198253noMoreTypeFunctions :: DefaultUni (Esc (f :: a -> b -> c -> d )) -> any
0 commit comments