==================== Tidy Core ==================== 2017-09-15 00:00:05.9794125 UTC Result size of Tidy Core = {terms: 1,482, types: 4,058, coercions: 7,986, joins: 0/0} -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$s$WSNat2 :: Integer CoreDump.Tensor.GenerateSing.$s$WSNat2 = 0 -- RHS size: {terms: 39, types: 12, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$s$WSNat1 :: GHC.Natural.Natural CoreDump.Tensor.GenerateSing.$s$WSNat1 = case CoreDump.Tensor.GenerateSing.$s$WSNat2 of { integer-gmp-1.0.1.0:GHC.Integer.Type.S# i# -> case GHC.Prim.tagToEnum# @ Bool (GHC.Prim.>=# i# 0#) of { False -> GHC.Natural.underflowError @ GHC.Natural.Natural; True -> GHC.Natural.NatS# (GHC.Prim.int2Word# i#) }; integer-gmp-1.0.1.0:GHC.Integer.Type.Jp# dt -> case GHC.Prim.uncheckedIShiftRL# (GHC.Prim.sizeofByteArray# dt) 3# of { __DEFAULT -> case GHC.Prim.sizeofByteArray# dt of { __DEFAULT -> GHC.Natural.NatJ# dt; 0# -> GHC.Natural.underflowError @ GHC.Natural.Natural }; 1# -> case GHC.Prim.indexWordArray# dt 0# of wild2 { __DEFAULT -> GHC.Natural.NatS# wild2 } }; integer-gmp-1.0.1.0:GHC.Integer.Type.Jn# ipv -> GHC.Natural.underflowError @ GHC.Natural.Natural } -- RHS size: {terms: 2, types: 1, coercions: 7, joins: 0/0} $s$WSNat12 :: singletons-2.3.1:Data.Singletons.TypeLits.Internal.R:SingNatn 0 $s$WSNat12 = singletons-2.3.1:Data.Singletons.TypeLits.Internal.SNat @ 0 (CoreDump.Tensor.GenerateSing.$s$WSNat1 `cast` ) -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$s$WSNat5 :: Integer CoreDump.Tensor.GenerateSing.$s$WSNat5 = 3 -- RHS size: {terms: 39, types: 12, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$s$WSNat4 :: GHC.Natural.Natural CoreDump.Tensor.GenerateSing.$s$WSNat4 = case CoreDump.Tensor.GenerateSing.$s$WSNat5 of { integer-gmp-1.0.1.0:GHC.Integer.Type.S# i# -> case GHC.Prim.tagToEnum# @ Bool (GHC.Prim.>=# i# 0#) of { False -> GHC.Natural.underflowError @ GHC.Natural.Natural; True -> GHC.Natural.NatS# (GHC.Prim.int2Word# i#) }; integer-gmp-1.0.1.0:GHC.Integer.Type.Jp# dt -> case GHC.Prim.uncheckedIShiftRL# (GHC.Prim.sizeofByteArray# dt) 3# of { __DEFAULT -> case GHC.Prim.sizeofByteArray# dt of { __DEFAULT -> GHC.Natural.NatJ# dt; 0# -> GHC.Natural.underflowError @ GHC.Natural.Natural }; 1# -> case GHC.Prim.indexWordArray# dt 0# of wild2 { __DEFAULT -> GHC.Natural.NatS# wild2 } }; integer-gmp-1.0.1.0:GHC.Integer.Type.Jn# ipv -> GHC.Natural.underflowError @ GHC.Natural.Natural } -- RHS size: {terms: 2, types: 1, coercions: 7, joins: 0/0} $s$WSNat13 :: singletons-2.3.1:Data.Singletons.TypeLits.Internal.R:SingNatn 3 $s$WSNat13 = singletons-2.3.1:Data.Singletons.TypeLits.Internal.SNat @ 3 (CoreDump.Tensor.GenerateSing.$s$WSNat4 `cast` ) -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$s$WSNat8 :: Integer CoreDump.Tensor.GenerateSing.$s$WSNat8 = 2 -- RHS size: {terms: 39, types: 12, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$s$WSNat7 :: GHC.Natural.Natural CoreDump.Tensor.GenerateSing.$s$WSNat7 = case CoreDump.Tensor.GenerateSing.$s$WSNat8 of { integer-gmp-1.0.1.0:GHC.Integer.Type.S# i# -> case GHC.Prim.tagToEnum# @ Bool (GHC.Prim.>=# i# 0#) of { False -> GHC.Natural.underflowError @ GHC.Natural.Natural; True -> GHC.Natural.NatS# (GHC.Prim.int2Word# i#) }; integer-gmp-1.0.1.0:GHC.Integer.Type.Jp# dt -> case GHC.Prim.uncheckedIShiftRL# (GHC.Prim.sizeofByteArray# dt) 3# of { __DEFAULT -> case GHC.Prim.sizeofByteArray# dt of { __DEFAULT -> GHC.Natural.NatJ# dt; 0# -> GHC.Natural.underflowError @ GHC.Natural.Natural }; 1# -> case GHC.Prim.indexWordArray# dt 0# of wild2 { __DEFAULT -> GHC.Natural.NatS# wild2 } }; integer-gmp-1.0.1.0:GHC.Integer.Type.Jn# ipv -> GHC.Natural.underflowError @ GHC.Natural.Natural } -- RHS size: {terms: 2, types: 1, coercions: 7, joins: 0/0} $s$WSNat14 :: singletons-2.3.1:Data.Singletons.TypeLits.Internal.R:SingNatn 2 $s$WSNat14 = singletons-2.3.1:Data.Singletons.TypeLits.Internal.SNat @ 2 (CoreDump.Tensor.GenerateSing.$s$WSNat7 `cast` ) -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$s$WSNat11 :: Integer CoreDump.Tensor.GenerateSing.$s$WSNat11 = 1 -- RHS size: {terms: 39, types: 12, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$s$WSNat10 :: GHC.Natural.Natural CoreDump.Tensor.GenerateSing.$s$WSNat10 = case CoreDump.Tensor.GenerateSing.$s$WSNat11 of { integer-gmp-1.0.1.0:GHC.Integer.Type.S# i# -> case GHC.Prim.tagToEnum# @ Bool (GHC.Prim.>=# i# 0#) of { False -> GHC.Natural.underflowError @ GHC.Natural.Natural; True -> GHC.Natural.NatS# (GHC.Prim.int2Word# i#) }; integer-gmp-1.0.1.0:GHC.Integer.Type.Jp# dt -> case GHC.Prim.uncheckedIShiftRL# (GHC.Prim.sizeofByteArray# dt) 3# of { __DEFAULT -> case GHC.Prim.sizeofByteArray# dt of { __DEFAULT -> GHC.Natural.NatJ# dt; 0# -> GHC.Natural.underflowError @ GHC.Natural.Natural }; 1# -> case GHC.Prim.indexWordArray# dt 0# of wild2 { __DEFAULT -> GHC.Natural.NatS# wild2 } }; integer-gmp-1.0.1.0:GHC.Integer.Type.Jn# ipv -> GHC.Natural.underflowError @ GHC.Natural.Natural } -- RHS size: {terms: 2, types: 1, coercions: 7, joins: 0/0} $s$WSNat15 :: singletons-2.3.1:Data.Singletons.TypeLits.Internal.R:SingNatn 1 $s$WSNat15 = singletons-2.3.1:Data.Singletons.TypeLits.Internal.SNat @ 1 (CoreDump.Tensor.GenerateSing.$s$WSNat10 `cast` ) -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$trModule4 :: GHC.Prim.Addr# CoreDump.Tensor.GenerateSing.$trModule4 = "main"# -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$trModule3 :: GHC.Types.TrName CoreDump.Tensor.GenerateSing.$trModule3 = GHC.Types.TrNameS CoreDump.Tensor.GenerateSing.$trModule4 -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$trModule2 :: GHC.Prim.Addr# CoreDump.Tensor.GenerateSing.$trModule2 = "CoreDump.Tensor.GenerateSing"# -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$trModule1 :: GHC.Types.TrName CoreDump.Tensor.GenerateSing.$trModule1 = GHC.Types.TrNameS CoreDump.Tensor.GenerateSing.$trModule2 -- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0} CoreDump.Tensor.GenerateSing.$trModule :: GHC.Types.Module CoreDump.Tensor.GenerateSing.$trModule = GHC.Types.Module CoreDump.Tensor.GenerateSing.$trModule3 CoreDump.Tensor.GenerateSing.$trModule1 -- RHS size: {terms: 1, types: 14, coercions: 5, joins: 0/0} $dSingI :: ('[0] :: [Nat]) ~~ ('[0] :: [Nat]) $dSingI = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0] @ '[0] @~ -- RHS size: {terms: 4, types: 10, coercions: 72, joins: 0/0} $dSingI1 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0] $dSingI1 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0] @ 0 @ '[] ($dSingI `cast` ) ($s$WSNat12 `cast` ) ((singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingI[][]1 @ Nat) `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI2 :: ('[0, 0] :: [Nat]) ~~ ('[0, 0] :: [Nat]) $dSingI2 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 0] @ '[0, 0] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI3 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 0] $dSingI3 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 0] @ 0 @ '[0] ($dSingI2 `cast` ) ($s$WSNat12 `cast` ) ($dSingI1 `cast` ) -- RHS size: {terms: 1, types: 14, coercions: 5, joins: 0/0} $dSingI4 :: ('[3] :: [Nat]) ~~ ('[3] :: [Nat]) $dSingI4 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[3] @ '[3] @~ -- RHS size: {terms: 4, types: 10, coercions: 72, joins: 0/0} $dSingI5 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[3] $dSingI5 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[3] @ 3 @ '[] ($dSingI4 `cast` ) ($s$WSNat13 `cast` ) ((singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingI[][]1 @ Nat) `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI6 :: ('[0, 3] :: [Nat]) ~~ ('[0, 3] :: [Nat]) $dSingI6 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 3] @ '[0, 3] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI7 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 3] $dSingI7 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 3] @ 0 @ '[3] ($dSingI6 `cast` ) ($s$WSNat12 `cast` ) ($dSingI5 `cast` ) -- RHS size: {terms: 1, types: 14, coercions: 5, joins: 0/0} $dSingI8 :: ('[2] :: [Nat]) ~~ ('[2] :: [Nat]) $dSingI8 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[2] @ '[2] @~ -- RHS size: {terms: 4, types: 10, coercions: 72, joins: 0/0} $dSingI9 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[2] $dSingI9 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[2] @ 2 @ '[] ($dSingI8 `cast` ) ($s$WSNat14 `cast` ) ((singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingI[][]1 @ Nat) `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI10 :: ('[2, 2] :: [Nat]) ~~ ('[2, 2] :: [Nat]) $dSingI10 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[2, 2] @ '[2, 2] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI11 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[2, 2] $dSingI11 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[2, 2] @ 2 @ '[2] ($dSingI10 `cast` ) ($s$WSNat14 `cast` ) ($dSingI9 `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI12 :: ('[0, 2] :: [Nat]) ~~ ('[0, 2] :: [Nat]) $dSingI12 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 2] @ '[0, 2] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI13 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 2] $dSingI13 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 2] @ 0 @ '[2] ($dSingI12 `cast` ) ($s$WSNat12 `cast` ) ($dSingI9 `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI14 :: ('[2, 0] :: [Nat]) ~~ ('[2, 0] :: [Nat]) $dSingI14 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[2, 0] @ '[2, 0] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI15 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[2, 0] $dSingI15 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[2, 0] @ 2 @ '[0] ($dSingI14 `cast` ) ($s$WSNat14 `cast` ) ($dSingI1 `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI16 :: ('[2, 3] :: [Nat]) ~~ ('[2, 3] :: [Nat]) $dSingI16 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[2, 3] @ '[2, 3] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI17 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[2, 3] $dSingI17 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[2, 3] @ 2 @ '[3] ($dSingI16 `cast` ) ($s$WSNat14 `cast` ) ($dSingI5 `cast` ) -- RHS size: {terms: 1, types: 14, coercions: 5, joins: 0/0} $dSingI18 :: ('[1] :: [Nat]) ~~ ('[1] :: [Nat]) $dSingI18 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1] @ '[1] @~ -- RHS size: {terms: 4, types: 10, coercions: 72, joins: 0/0} $dSingI19 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1] $dSingI19 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1] @ 1 @ '[] ($dSingI18 `cast` ) ($s$WSNat15 `cast` ) ((singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingI[][]1 @ Nat) `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI20 :: ('[2, 1] :: [Nat]) ~~ ('[2, 1] :: [Nat]) $dSingI20 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[2, 1] @ '[2, 1] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI21 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[2, 1] $dSingI21 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[2, 1] @ 2 @ '[1] ($dSingI20 `cast` ) ($s$WSNat14 `cast` ) ($dSingI19 `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI22 :: ('[0, 1] :: [Nat]) ~~ ('[0, 1] :: [Nat]) $dSingI22 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 1] @ '[0, 1] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI23 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 1] $dSingI23 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 1] @ 0 @ '[1] ($dSingI22 `cast` ) ($s$WSNat12 `cast` ) ($dSingI19 `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI24 :: ('[1, 3] :: [Nat]) ~~ ('[1, 3] :: [Nat]) $dSingI24 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 3] @ '[1, 3] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI25 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 3] $dSingI25 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 3] @ 1 @ '[3] ($dSingI24 `cast` ) ($s$WSNat15 `cast` ) ($dSingI5 `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI26 :: ('[1, 2] :: [Nat]) ~~ ('[1, 2] :: [Nat]) $dSingI26 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 2] @ '[1, 2] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI27 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 2] $dSingI27 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 2] @ 1 @ '[2] ($dSingI26 `cast` ) ($s$WSNat15 `cast` ) ($dSingI9 `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI28 :: ('[1, 1] :: [Nat]) ~~ ('[1, 1] :: [Nat]) $dSingI28 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 1] @ '[1, 1] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI29 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 1] $dSingI29 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 1] @ 1 @ '[1] ($dSingI28 `cast` ) ($s$WSNat15 `cast` ) ($dSingI19 `cast` ) -- RHS size: {terms: 1, types: 20, coercions: 8, joins: 0/0} $dSingI30 :: ('[1, 0] :: [Nat]) ~~ ('[1, 0] :: [Nat]) $dSingI30 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 0] @ '[1, 0] @~ -- RHS size: {terms: 4, types: 15, coercions: 123, joins: 0/0} $dSingI31 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 0] $dSingI31 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 0] @ 1 @ '[0] ($dSingI30 `cast` ) ($s$WSNat15 `cast` ) ($dSingI1 `cast` ) -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0} loc :: [Char] loc = GHC.CString.unpackCString# CoreDump.Tensor.GenerateSing.$trModule4 -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0} loc1 :: [Char] loc1 = GHC.CString.unpackCString# CoreDump.Tensor.GenerateSing.$trModule2 -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0} loc2 :: GHC.Prim.Addr# loc2 = "tests\\CoreDump\\Tensor\\GenerateSing.hs"# -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0} loc3 :: [Char] loc3 = GHC.CString.unpackCString# loc2 -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0} loc4 :: Int loc4 = GHC.Types.I# 18# -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0} loc5 :: Int loc5 = GHC.Types.I# 26# -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0} loc6 :: Int loc6 = GHC.Types.I# 35# -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0} $dIP :: GHC.Prim.Addr# $dIP = "undefined"# -- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0} $dIP1 :: [Char] $dIP1 = GHC.CString.unpackCString# $dIP -- RHS size: {terms: 8, types: 0, coercions: 0, joins: 0/0} $dIP2 :: GHC.Stack.Types.SrcLoc $dIP2 = GHC.Stack.Types.SrcLoc loc loc1 loc3 loc4 loc5 loc4 loc6 -- RHS size: {terms: 4, types: 0, coercions: 0, joins: 0/0} $dIP3 :: GHC.Stack.Types.CallStack $dIP3 = GHC.Stack.Types.PushCallStack $dIP1 $dIP2 GHC.Stack.Types.EmptyCallStack -- RHS size: {terms: 2, types: 2, coercions: 4, joins: 0/0} lvl :: Float lvl = undefined @ 'GHC.Types.LiftedRep @ Float ($dIP3 `cast` ) -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0} lvl1 :: Integer lvl1 = 12 -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0} lvl2 :: Integer lvl2 = 4 -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl3 :: ('[1, 2, 3] :: [Nat]) ~~ ('[1, 2, 3] :: [Nat]) lvl3 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 2, 3] @ '[1, 2, 3] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl4 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 2, 3] lvl4 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 2, 3] @ 1 @ '[2, 3] (lvl3 `cast` ) ($s$WSNat15 `cast` ) ($dSingI17 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl5 :: ('[1, 2, 2] :: [Nat]) ~~ ('[1, 2, 2] :: [Nat]) lvl5 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 2, 2] @ '[1, 2, 2] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl6 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 2, 2] lvl6 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 2, 2] @ 1 @ '[2, 2] (lvl5 `cast` ) ($s$WSNat15 `cast` ) ($dSingI11 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl7 :: ('[1, 2, 1] :: [Nat]) ~~ ('[1, 2, 1] :: [Nat]) lvl7 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 2, 1] @ '[1, 2, 1] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl8 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 2, 1] lvl8 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 2, 1] @ 1 @ '[2, 1] (lvl7 `cast` ) ($s$WSNat15 `cast` ) ($dSingI21 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl9 :: ('[1, 2, 0] :: [Nat]) ~~ ('[1, 2, 0] :: [Nat]) lvl9 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 2, 0] @ '[1, 2, 0] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl10 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 2, 0] lvl10 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 2, 0] @ 1 @ '[2, 0] (lvl9 `cast` ) ($s$WSNat15 `cast` ) ($dSingI15 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl11 :: ('[1, 1, 3] :: [Nat]) ~~ ('[1, 1, 3] :: [Nat]) lvl11 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 1, 3] @ '[1, 1, 3] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl12 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 1, 3] lvl12 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 1, 3] @ 1 @ '[1, 3] (lvl11 `cast` ) ($s$WSNat15 `cast` ) ($dSingI25 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl13 :: ('[1, 1, 2] :: [Nat]) ~~ ('[1, 1, 2] :: [Nat]) lvl13 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 1, 2] @ '[1, 1, 2] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl14 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 1, 2] lvl14 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 1, 2] @ 1 @ '[1, 2] (lvl13 `cast` ) ($s$WSNat15 `cast` ) ($dSingI27 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl15 :: ('[1, 1, 1] :: [Nat]) ~~ ('[1, 1, 1] :: [Nat]) lvl15 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 1, 1] @ '[1, 1, 1] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl16 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 1, 1] lvl16 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 1, 1] @ 1 @ '[1, 1] (lvl15 `cast` ) ($s$WSNat15 `cast` ) ($dSingI29 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl17 :: ('[1, 1, 0] :: [Nat]) ~~ ('[1, 1, 0] :: [Nat]) lvl17 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 1, 0] @ '[1, 1, 0] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl18 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 1, 0] lvl18 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 1, 0] @ 1 @ '[1, 0] (lvl17 `cast` ) ($s$WSNat15 `cast` ) ($dSingI31 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl19 :: ('[1, 0, 3] :: [Nat]) ~~ ('[1, 0, 3] :: [Nat]) lvl19 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 0, 3] @ '[1, 0, 3] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl20 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 0, 3] lvl20 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 0, 3] @ 1 @ '[0, 3] (lvl19 `cast` ) ($s$WSNat15 `cast` ) ($dSingI7 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl21 :: ('[1, 0, 2] :: [Nat]) ~~ ('[1, 0, 2] :: [Nat]) lvl21 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 0, 2] @ '[1, 0, 2] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl22 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 0, 2] lvl22 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 0, 2] @ 1 @ '[0, 2] (lvl21 `cast` ) ($s$WSNat15 `cast` ) ($dSingI13 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl23 :: ('[1, 0, 1] :: [Nat]) ~~ ('[1, 0, 1] :: [Nat]) lvl23 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 0, 1] @ '[1, 0, 1] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl24 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 0, 1] lvl24 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 0, 1] @ 1 @ '[0, 1] (lvl23 `cast` ) ($s$WSNat15 `cast` ) ($dSingI23 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl25 :: ('[1, 0, 0] :: [Nat]) ~~ ('[1, 0, 0] :: [Nat]) lvl25 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[1, 0, 0] @ '[1, 0, 0] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl26 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[1, 0, 0] lvl26 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[1, 0, 0] @ 1 @ '[0, 0] (lvl25 `cast` ) ($s$WSNat15 `cast` ) ($dSingI3 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl27 :: ('[0, 2, 3] :: [Nat]) ~~ ('[0, 2, 3] :: [Nat]) lvl27 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 2, 3] @ '[0, 2, 3] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl28 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 2, 3] lvl28 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 2, 3] @ 0 @ '[2, 3] (lvl27 `cast` ) ($s$WSNat12 `cast` ) ($dSingI17 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl29 :: ('[0, 2, 2] :: [Nat]) ~~ ('[0, 2, 2] :: [Nat]) lvl29 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 2, 2] @ '[0, 2, 2] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl30 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 2, 2] lvl30 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 2, 2] @ 0 @ '[2, 2] (lvl29 `cast` ) ($s$WSNat12 `cast` ) ($dSingI11 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl31 :: ('[0, 2, 1] :: [Nat]) ~~ ('[0, 2, 1] :: [Nat]) lvl31 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 2, 1] @ '[0, 2, 1] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl32 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 2, 1] lvl32 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 2, 1] @ 0 @ '[2, 1] (lvl31 `cast` ) ($s$WSNat12 `cast` ) ($dSingI21 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl33 :: ('[0, 2, 0] :: [Nat]) ~~ ('[0, 2, 0] :: [Nat]) lvl33 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 2, 0] @ '[0, 2, 0] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl34 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 2, 0] lvl34 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 2, 0] @ 0 @ '[2, 0] (lvl33 `cast` ) ($s$WSNat12 `cast` ) ($dSingI15 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl35 :: ('[0, 1, 3] :: [Nat]) ~~ ('[0, 1, 3] :: [Nat]) lvl35 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 1, 3] @ '[0, 1, 3] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl36 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 1, 3] lvl36 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 1, 3] @ 0 @ '[1, 3] (lvl35 `cast` ) ($s$WSNat12 `cast` ) ($dSingI25 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl37 :: ('[0, 1, 2] :: [Nat]) ~~ ('[0, 1, 2] :: [Nat]) lvl37 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 1, 2] @ '[0, 1, 2] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl38 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 1, 2] lvl38 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 1, 2] @ 0 @ '[1, 2] (lvl37 `cast` ) ($s$WSNat12 `cast` ) ($dSingI27 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl39 :: ('[0, 1, 1] :: [Nat]) ~~ ('[0, 1, 1] :: [Nat]) lvl39 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 1, 1] @ '[0, 1, 1] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl40 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 1, 1] lvl40 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 1, 1] @ 0 @ '[1, 1] (lvl39 `cast` ) ($s$WSNat12 `cast` ) ($dSingI29 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl41 :: ('[0, 1, 0] :: [Nat]) ~~ ('[0, 1, 0] :: [Nat]) lvl41 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 1, 0] @ '[0, 1, 0] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl42 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 1, 0] lvl42 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 1, 0] @ 0 @ '[1, 0] (lvl41 `cast` ) ($s$WSNat12 `cast` ) ($dSingI31 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl43 :: ('[0, 0, 3] :: [Nat]) ~~ ('[0, 0, 3] :: [Nat]) lvl43 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 0, 3] @ '[0, 0, 3] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl44 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 0, 3] lvl44 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 0, 3] @ 0 @ '[0, 3] (lvl43 `cast` ) ($s$WSNat12 `cast` ) ($dSingI7 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl45 :: ('[0, 0, 2] :: [Nat]) ~~ ('[0, 0, 2] :: [Nat]) lvl45 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 0, 2] @ '[0, 0, 2] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl46 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 0, 2] lvl46 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 0, 2] @ 0 @ '[0, 2] (lvl45 `cast` ) ($s$WSNat12 `cast` ) ($dSingI13 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl47 :: ('[0, 0, 1] :: [Nat]) ~~ ('[0, 0, 1] :: [Nat]) lvl47 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 0, 1] @ '[0, 0, 1] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl48 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 0, 1] lvl48 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 0, 1] @ 0 @ '[0, 1] (lvl47 `cast` ) ($s$WSNat12 `cast` ) ($dSingI23 `cast` ) -- RHS size: {terms: 1, types: 26, coercions: 11, joins: 0/0} lvl49 :: ('[0, 0, 0] :: [Nat]) ~~ ('[0, 0, 0] :: [Nat]) lvl49 = GHC.Types.Eq# @ [Nat] @ [Nat] @ '[0, 0, 0] @ '[0, 0, 0] @~ -- RHS size: {terms: 4, types: 21, coercions: 156, joins: 0/0} lvl50 :: singletons-2.3.1:Data.Singletons.Prelude.Instances.R:Sing[]z Nat '[0, 0, 0] lvl50 = singletons-2.3.1:Data.Singletons.Prelude.Instances.SCons @ Nat @ '[0, 0, 0] @ 0 @ '[0, 0] (lvl49 `cast` ) ($s$WSNat12 `cast` ) ($dSingI3 `cast` ) -- RHS size: {terms: 961, types: 888, coercions: 2,066, joins: 0/0} generateSing_ :: Tensor '[2, 3, 4] Float generateSing_ = case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 0, 0] (lvl50 `cast` )) `cast` of { [] -> case lvl of wild1 { }; : i ds -> case ds of { [] -> case lvl of wild2 { }; : j ds1 -> case ds1 of { [] -> case lvl of wild3 { }; : k ds2 -> case ds2 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j lvl2)) k) of wild4 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 0, 1] (lvl48 `cast` )) `cast` of { [] -> case lvl of wild6 { }; : i1 ds3 -> case ds3 of { [] -> case lvl of wild7 { }; : j1 ds4 -> case ds4 of { [] -> case lvl of wild8 { }; : k1 ds5 -> case ds5 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i1 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j1 lvl2)) k1) of wild9 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 0, 2] (lvl46 `cast` )) `cast` of { [] -> case lvl of wild11 { }; : i2 ds6 -> case ds6 of { [] -> case lvl of wild12 { }; : j2 ds7 -> case ds7 of { [] -> case lvl of wild13 { }; : k2 ds8 -> case ds8 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i2 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j2 lvl2)) k2) of wild14 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 0, 3] (lvl44 `cast` )) `cast` of { [] -> case lvl of wild16 { }; : i3 ds9 -> case ds9 of { [] -> case lvl of wild17 { }; : j3 ds10 -> case ds10 of { [] -> case lvl of wild18 { }; : k3 ds11 -> case ds11 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i3 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j3 lvl2)) k3) of wild19 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 1, 0] (lvl42 `cast` )) `cast` of { [] -> case lvl of wild21 { }; : i4 ds12 -> case ds12 of { [] -> case lvl of wild22 { }; : j4 ds13 -> case ds13 of { [] -> case lvl of wild23 { }; : k4 ds14 -> case ds14 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i4 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j4 lvl2)) k4) of wild24 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 1, 1] (lvl40 `cast` )) `cast` of { [] -> case lvl of wild26 { }; : i5 ds15 -> case ds15 of { [] -> case lvl of wild27 { }; : j5 ds16 -> case ds16 of { [] -> case lvl of wild28 { }; : k5 ds17 -> case ds17 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i5 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j5 lvl2)) k5) of wild29 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 1, 2] (lvl38 `cast` )) `cast` of { [] -> case lvl of wild31 { }; : i6 ds18 -> case ds18 of { [] -> case lvl of wild32 { }; : j6 ds19 -> case ds19 of { [] -> case lvl of wild33 { }; : k6 ds20 -> case ds20 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i6 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j6 lvl2)) k6) of wild34 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 1, 3] (lvl36 `cast` )) `cast` of { [] -> case lvl of wild36 { }; : i7 ds21 -> case ds21 of { [] -> case lvl of wild37 { }; : j7 ds22 -> case ds22 of { [] -> case lvl of wild38 { }; : k7 ds23 -> case ds23 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i7 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j7 lvl2)) k7) of wild39 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 2, 0] (lvl34 `cast` )) `cast` of { [] -> case lvl of wild41 { }; : i8 ds24 -> case ds24 of { [] -> case lvl of wild42 { }; : j8 ds25 -> case ds25 of { [] -> case lvl of wild43 { }; : k8 ds26 -> case ds26 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i8 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j8 lvl2)) k8) of wild44 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 2, 1] (lvl32 `cast` )) `cast` of { [] -> case lvl of wild46 { }; : i9 ds27 -> case ds27 of { [] -> case lvl of wild47 { }; : j9 ds28 -> case ds28 of { [] -> case lvl of wild48 { }; : k9 ds29 -> case ds29 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i9 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j9 lvl2)) k9) of wild49 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 2, 2] (lvl30 `cast` )) `cast` of { [] -> case lvl of wild51 { }; : i10 ds30 -> case ds30 of { [] -> case lvl of wild52 { }; : j10 ds31 -> case ds31 of { [] -> case lvl of wild53 { }; : k10 ds32 -> case ds32 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i10 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j10 lvl2)) k10) of wild54 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[0, 2, 3] (lvl28 `cast` )) `cast` of { [] -> case lvl of wild56 { }; : i11 ds33 -> case ds33 of { [] -> case lvl of wild57 { }; : j11 ds34 -> case ds34 of { [] -> case lvl of wild58 { }; : k11 ds35 -> case ds35 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i11 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j11 lvl2)) k11) of wild59 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 0, 0] (lvl26 `cast` )) `cast` of { [] -> case lvl of wild61 { }; : i12 ds36 -> case ds36 of { [] -> case lvl of wild62 { }; : j12 ds37 -> case ds37 of { [] -> case lvl of wild63 { }; : k12 ds38 -> case ds38 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i12 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j12 lvl2)) k12) of wild64 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 0, 1] (lvl24 `cast` )) `cast` of { [] -> case lvl of wild66 { }; : i13 ds39 -> case ds39 of { [] -> case lvl of wild67 { }; : j13 ds40 -> case ds40 of { [] -> case lvl of wild68 { }; : k13 ds41 -> case ds41 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i13 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j13 lvl2)) k13) of wild69 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 0, 2] (lvl22 `cast` )) `cast` of { [] -> case lvl of wild71 { }; : i14 ds42 -> case ds42 of { [] -> case lvl of wild72 { }; : j14 ds43 -> case ds43 of { [] -> case lvl of wild73 { }; : k14 ds44 -> case ds44 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i14 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j14 lvl2)) k14) of wild74 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 0, 3] (lvl20 `cast` )) `cast` of { [] -> case lvl of wild76 { }; : i15 ds45 -> case ds45 of { [] -> case lvl of wild77 { }; : j15 ds46 -> case ds46 of { [] -> case lvl of wild78 { }; : k15 ds47 -> case ds47 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i15 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j15 lvl2)) k15) of wild79 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 1, 0] (lvl18 `cast` )) `cast` of { [] -> case lvl of wild81 { }; : i16 ds48 -> case ds48 of { [] -> case lvl of wild82 { }; : j16 ds49 -> case ds49 of { [] -> case lvl of wild83 { }; : k16 ds50 -> case ds50 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i16 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j16 lvl2)) k16) of wild84 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 1, 1] (lvl16 `cast` )) `cast` of { [] -> case lvl of wild86 { }; : i17 ds51 -> case ds51 of { [] -> case lvl of wild87 { }; : j17 ds52 -> case ds52 of { [] -> case lvl of wild88 { }; : k17 ds53 -> case ds53 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i17 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j17 lvl2)) k17) of wild89 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 1, 2] (lvl14 `cast` )) `cast` of { [] -> case lvl of wild91 { }; : i18 ds54 -> case ds54 of { [] -> case lvl of wild92 { }; : j18 ds55 -> case ds55 of { [] -> case lvl of wild93 { }; : k18 ds56 -> case ds56 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i18 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j18 lvl2)) k18) of wild94 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 1, 3] (lvl12 `cast` )) `cast` of { [] -> case lvl of wild96 { }; : i19 ds57 -> case ds57 of { [] -> case lvl of wild97 { }; : j19 ds58 -> case ds58 of { [] -> case lvl of wild98 { }; : k19 ds59 -> case ds59 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i19 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j19 lvl2)) k19) of wild99 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 2, 0] (lvl10 `cast` )) `cast` of { [] -> case lvl of wild101 { }; : i20 ds60 -> case ds60 of { [] -> case lvl of wild102 { }; : j20 ds61 -> case ds61 of { [] -> case lvl of wild103 { }; : k20 ds62 -> case ds62 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i20 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j20 lvl2)) k20) of wild104 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 2, 1] (lvl8 `cast` )) `cast` of { [] -> case lvl of wild106 { }; : i21 ds63 -> case ds63 of { [] -> case lvl of wild107 { }; : j21 ds64 -> case ds64 of { [] -> case lvl of wild108 { }; : k21 ds65 -> case ds65 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i21 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j21 lvl2)) k21) of wild109 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 2, 2] (lvl6 `cast` )) `cast` of { [] -> case lvl of wild111 { }; : i22 ds66 -> case ds66 of { [] -> case lvl of wild112 { }; : j22 ds67 -> case ds67 of { [] -> case lvl of wild113 { }; : k22 ds68 -> case ds68 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i22 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j22 lvl2)) k22) of wild114 { __DEFAULT -> case (singletons-2.3.1:Data.Singletons.Prelude.Instances.$fSingKindNonEmpty_$cfromSing1 @ Nat singletons-2.3.1:Data.Singletons.TypeLits.Internal.$fSingKindNat @ '[1, 2, 3] (lvl4 `cast` )) `cast` of { [] -> case lvl of wild116 { }; : i23 ds69 -> case ds69 of { [] -> case lvl of wild117 { }; : j23 ds70 -> case ds70 of { [] -> case lvl of wild118 { }; : k23 ds71 -> case ds71 of { [] -> case integer-gmp-1.0.1.0:GHC.Integer.Type.doubleFromInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.plusInteger (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger i23 lvl1) (integer-gmp-1.0.1.0:GHC.Integer.Type.timesInteger j23 lvl2)) k23) of wild119 { __DEFAULT -> (TensorInstances.Tensor'2'3'4'Float (GHC.Prim.double2Float# wild4) (GHC.Prim.double2Float# wild9) (GHC.Prim.double2Float# wild14) (GHC.Prim.double2Float# wild19) (GHC.Prim.double2Float# wild24) (GHC.Prim.double2Float# wild29) (GHC.Prim.double2Float# wild34) (GHC.Prim.double2Float# wild39) (GHC.Prim.double2Float# wild44) (GHC.Prim.double2Float# wild49) (GHC.Prim.double2Float# wild54) (GHC.Prim.double2Float# wild59) (GHC.Prim.double2Float# wild64) (GHC.Prim.double2Float# wild69) (GHC.Prim.double2Float# wild74) (GHC.Prim.double2Float# wild79) (GHC.Prim.double2Float# wild84) (GHC.Prim.double2Float# wild89) (GHC.Prim.double2Float# wild94) (GHC.Prim.double2Float# wild99) (GHC.Prim.double2Float# wild104) (GHC.Prim.double2Float# wild109) (GHC.Prim.double2Float# wild114) (GHC.Prim.double2Float# wild119)) `cast` }; : ipv ipv1 -> case lvl of wild119 { } } } } } }; : ipv ipv1 -> case lvl of wild114 { } } } } } }; : ipv ipv1 -> case lvl of wild109 { } } } } } }; : ipv ipv1 -> case lvl of wild104 { } } } } } }; : ipv ipv1 -> case lvl of wild99 { } } } } } }; : ipv ipv1 -> case lvl of wild94 { } } } } } }; : ipv ipv1 -> case lvl of wild89 { } } } } } }; : ipv ipv1 -> case lvl of wild84 { } } } } } }; : ipv ipv1 -> case lvl of wild79 { } } } } } }; : ipv ipv1 -> case lvl of wild74 { } } } } } }; : ipv ipv1 -> case lvl of wild69 { } } } } } }; : ipv ipv1 -> case lvl of wild64 { } } } } } }; : ipv ipv1 -> case lvl of wild59 { } } } } } }; : ipv ipv1 -> case lvl of wild54 { } } } } } }; : ipv ipv1 -> case lvl of wild49 { } } } } } }; : ipv ipv1 -> case lvl of wild44 { } } } } } }; : ipv ipv1 -> case lvl of wild39 { } } } } } }; : ipv ipv1 -> case lvl of wild34 { } } } } } }; : ipv ipv1 -> case lvl of wild29 { } } } } } }; : ipv ipv1 -> case lvl of wild24 { } } } } } }; : ipv ipv1 -> case lvl of wild19 { } } } } } }; : ipv ipv1 -> case lvl of wild14 { } } } } } }; : ipv ipv1 -> case lvl of wild9 { } } } } } }; : ipv ipv1 -> case lvl of wild4 { } } } } }