@@ -66,7 +66,7 @@ genNetwork =
6666 SCons ( h :: Sing h ) ( _ :: Sing hs ) ->
6767 withSingI h $
6868 case h of
69− D1Sing l -> withKnownNat l $
69+ D1Sing l@SNat ->
7070 Gen.choice [
7171 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
7272 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
@@ -87,7 +87,7 @@ genNetwork =
8787 pure (SomeNetwork (Reshape :~> rest :: Network ( Reshape ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
8888 _ -> Gen.discard -- Doesn't occur
8989 ]
90− D2Sing r c -> withKnownNat r $ withKnownNat c $
90+ D2Sing r@SNat c@SNat ->
9191 Gen.choice [
9292 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
9393 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
@@ -215,7 +215,7 @@ genNetwork =
215215 pure (SomeNetwork (Pooling :~> rest :: Network ( Pooling kernelRows kernelCols strideRows strideCols ': layers ) ( ('D2 inRows inCols) ': h ': hs )))
216216 _ -> Gen.discard -- Can't occur
217217 ]
218− D3Sing r c d -> withKnownNat d $ withKnownNat r $ withKnownNat c $
218+ D3Sing SNat SNat SNat ->
219219 Gen.choice [
220220 pure (SomeNetwork (Tanh :~> rest :: Network ( Tanh ': layers ) ( h ': h ': hs )))
221221 , pure (SomeNetwork (Logit :~> rest :: Network ( Logit ': layers ) ( h ': h ': hs )))
@@ -247,7 +247,7 @@ prop_auto_diff = withTests 10000 . property $ do
247247oneUp :: forall shape m. ( Monad m, SingI shape ) => Gen.Gen m (S shape)
248248oneUp =
249249 case ( sing :: Sing shape ) of
250− D1Sing l -> withKnownNat l $
250+ D1Sing SNat ->
251251 let x = 0 :: S ( shape )
252252 in case x of
253253 ( S1D x' ) -> do
@@ -259,7 +259,7 @@ oneUp =
259259 VS.freeze ex'
260260 maybe Gen.discard pure . fromStorable $ nx
261261
262− D2Sing r c -> withKnownNat r $ withKnownNat c $
262+ D2Sing SNat SNat ->
263263 let x = 0 :: S ( shape )
264264 in case x of
265265 ( S2D x' ) -> do
@@ -271,7 +271,7 @@ oneUp =
271271 VS.freeze ex'
272272 maybe Gen.discard pure . fromStorable $ nx
273273
274− D3Sing r c d -> withKnownNat r $ withKnownNat c $ withKnownNat d $
274+ D3Sing SNat SNat SNat ->
275275 let x = 0 :: S ( shape )
276276 in case x of
277277 ( S3D x' ) -> do