Build #1 for fin-0.3
| Package | fin-0.3 |
|---|
| Install | InstallOk |
|---|---|
| Docs | Ok |
| Tests | NotTried |
| Time submitted | 2023-03-21 15:18:22.926070839 UTC |
|---|---|
| Compiler | ghc-9.2.4 |
| OS | linux |
| Arch | x86_64 |
| Dependencies | QuickCheck-2.14.2, base-4.16.3.0, boring-0.2.1, dec-0.0.5, deepseq-1.4.6.1, hashable-1.4.2.0, some-1.0.5, universe-base-1.1.3.1 |
| Flags | none |
Code Coverage
No Code Coverage was submitted for this report.
Build log
[view raw]
Resolving dependencies... Starting data-array-byte-0.1.0.1 Starting some-1.0.5 Starting tagged-0.8.7 Starting splitmix-0.1.0.4 Building data-array-byte-0.1.0.1 Building some-1.0.5 Building splitmix-0.1.0.4 Building tagged-0.8.7 Completed splitmix-0.1.0.4 Starting random-1.2.1.1 Completed data-array-byte-0.1.0.1 Starting hashable-1.4.2.0 Building random-1.2.1.1 Completed some-1.0.5 Building hashable-1.4.2.0 Completed tagged-0.8.7 Starting boring-0.2.1 Starting universe-base-1.1.3.1 Building boring-0.2.1 Building universe-base-1.1.3.1 Completed boring-0.2.1 Starting dec-0.0.5 Building dec-0.0.5 Completed universe-base-1.1.3.1 Completed hashable-1.4.2.0 Completed dec-0.0.5 Completed random-1.2.1.1 Starting QuickCheck-2.14.2 Building QuickCheck-2.14.2 Completed QuickCheck-2.14.2 Starting fin-0.3 Building fin-0.3 Completed fin-0.3
Test log
[view raw]
Resolving dependencies...
Build profile: -w ghc-9.2.4 -O0
In order, the following will be built (use -v for more details):
- boring-0.2.1 (lib:boring) (requires build)
- some-1.0.5 (lib:some) (requires build)
- dec-0.0.5 (lib:dec) (requires build)
- fin-0.3 (first run)
Starting boring-0.2.1 (all, legacy fallback)
Starting some-1.0.5 (all, legacy fallback)
Building boring-0.2.1 (all, legacy fallback)
Building some-1.0.5 (all, legacy fallback)
Installing boring-0.2.1 (all, legacy fallback)
Installing some-1.0.5 (all, legacy fallback)
Completed boring-0.2.1 (all, legacy fallback)
Starting dec-0.0.5 (all, legacy fallback)
Completed some-1.0.5 (all, legacy fallback)
Building dec-0.0.5 (all, legacy fallback)
Installing dec-0.0.5 (all, legacy fallback)
Completed dec-0.0.5 (all, legacy fallback)
Configuring fin-0.3...
Preprocessing library for fin-0.3..
Building library for fin-0.3..
[1 of 7] Compiling Data.Nat ( src/Data/Nat.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Nat.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Nat.dyn_o )
[2 of 7] Compiling TrustworthyCompat ( src/TrustworthyCompat.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/TrustworthyCompat.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/TrustworthyCompat.dyn_o )
[3 of 7] Compiling Data.Type.Nat ( src/Data/Type/Nat.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Type/Nat.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Type/Nat.dyn_o )
[4 of 7] Compiling Data.Type.Nat.LE ( src/Data/Type/Nat/LE.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Type/Nat/LE.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Type/Nat/LE.dyn_o )
[5 of 7] Compiling Data.Type.Nat.LT ( src/Data/Type/Nat/LT.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Type/Nat/LT.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Type/Nat/LT.dyn_o )
[6 of 7] Compiling Data.Type.Nat.LE.ReflStep ( src/Data/Type/Nat/LE/ReflStep.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Type/Nat/LE/ReflStep.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Type/Nat/LE/ReflStep.dyn_o )
[7 of 7] Compiling Data.Fin ( src/Data/Fin.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Fin.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/Data/Fin.dyn_o )
Preprocessing test suite 'inspection' for fin-0.3..
Building test suite 'inspection' for fin-0.3..
[1 of 1] Compiling Main ( test/Inspection.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/inspection/inspection-tmp/Main.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.2.4/fin-0.3/noopt/build/inspection/inspection-tmp/Main.dyn_o )
test/Inspection.hs:11:1: warning: [-Wunused-imports]
The import of Data.Fin is redundant
except perhaps to import instances from Data.Fin
To import instances alone, use: import Data.Fin()
|
11 | import Data.Fin (Fin (..))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
test/Inspection.hs:16:1: warning: [-Wunused-imports]
The import of GHC.Generics is redundant
except perhaps to import instances from GHC.Generics
To import instances alone, use: import GHC.Generics()
|
16 | import GHC.Generics (Generic)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
test/Inspection.hs:51:1: lhsInline === rhs failed:
LHS:
lhsInline :: Int
[LclIdX,
Unf=Unf{Src=InlineStable, TopLvl=True, Value=False, ConLike=False,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)
Tmpl= lhsInline_s5S5
`cast` (N:Tagged[0] <Nat>_N <Nat5>_P <Int>_R
:: Coercible (*) (Tagged @{Nat} Nat5 Int) Int)}]
lhsInline
= lhsInline_s5S5
`cast` (N:Tagged[0] <Nat>_N <Nat5>_P <Int>_R
:: Coercible (*) (Tagged @{Nat} Nat5 Int) Int)
$dSNatI_a1Ti :: SNatI ('S Nat0)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Ti = $fSNatIS @'Z $fSNatIZ
$dSNatI_a1Th :: SNatI ('S Nat1)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Th = $fSNatIS @('S Nat0) $dSNatI_a1Ti
$dSNatI_a1Tg :: SNatI ('S Nat2)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Tg = $fSNatIS @('S Nat1) $dSNatI_a1Th
$dSNatI_a1Tf :: SNatI ('S Nat3)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Tf = $fSNatIS @('S Nat2) $dSNatI_a1Tg
$dSNatI_a1Qy :: SNatI Nat5
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Qy = $fSNatIS @('S Nat3) $dSNatI_a1Tf
poly_f_s5T0
:: forall {m :: Nat}. Tagged @{Nat} m Int -> Tagged @{Nat} m Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 60}]
poly_f_s5T0
= \ (@(m :: Nat)) ->
hpc<Main,98> \ (x [Dmd=1L] :: Tagged @{Nat} m Int) -> x
poly_g_s5Td :: Int -> Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 60}]
poly_g_s5Td = hpc<Main,99> $fEnumInt_$csucc
poly_g_s5T4
:: forall {m :: Nat}. Tagged @{Nat} m Int -> Tagged @{Nat} m Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 20 60}]
poly_g_s5T4
= \ (@(m :: Nat)) ->
hpc<Main,100> $fFunctorTagged_$cfmap @Nat @m @Int @Int poly_g_s5Td
lvl_s5TH :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
lvl_s5TH = I# 0#
lvl_s5TI
:: forall {m :: Nat}.
SNatI m =>
Tagged @{Nat} m Int -> Tagged @{Nat} m Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 60 60}]
lvl_s5TI
= \ (@(m :: Nat)) ->
hpc<Main,101>
\ _ [Occ=Dead, Dmd=A] (eta_B0 :: Tagged @{Nat} m Int) ->
poly_f_s5T0 @m (poly_g_s5T4 @m eta_B0)
lhsInline_s5S5 :: Tagged @{Nat} Nat5 Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 40 0}]
lhsInline_s5S5
= hpc<Main,104>
hpc<Main,103>
hpc<Main,102>
induction1
@Nat5
@(Tagged @{Nat})
@Int
$dSNatI_a1Qy
((hpc<Main,97> hpc<Main,96> lvl_s5TH)
`cast` (Sym (N:Tagged[0] <Nat>_N <'Z>_P <Int>_R)
:: Coercible (*) Int (Tagged @{Nat} 'Z Int)))
(lvl_s5TI
`cast` (forall (m :: <Nat>_N).
<SNatI m>_R
%<'Many>_N ->_R <Tagged @{Nat} m Int>_R
%<'Many>_N ->_R N:Tagged[0] <Nat>_N <m>_P <Int>_R
; Sym (N:Tagged[0] <Nat>_N <'S m>_P <Int>_R)
:: Coercible
(*)
(forall {m :: Nat}.
SNatI m =>
Tagged @{Nat} m Int -> Tagged @{Nat} m Int)
(forall {m :: Nat}.
SNatI m =>
Tagged @{Nat} m Int -> Tagged @{Nat} ('S m) Int)))
RHS:
rhs :: Int
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 10}]
rhs = hpc<Main,78> hpc<Main,77> I# 5#
test/Inspection.hs:52:1: lhsNormal === rhs failed expectedly.
test/Inspection.hs:65:1: lhsProof ==- rhsProof failed:
LHS:
lhsProof
= ... hpc<Main,76>
hpc<Main,75>
hpc<Main,73>
case N.proofMultNOne @n $dSNatI_a4d4 of { Refl co_a4du ->
(hpc<Main,74> x)
`cast` ((Fin (Sym co))_R
:: Coercible (*) (Fin (N.Mult n N.Nat1)) (Fin n))
}
RHS:
rhsProof
= ... hpc<Main,72>
hpc<Main,71>
case Unsafe.Coerce.unsafeEqualityProof
@(*) @(Fin (N.Mult n N.Nat1)) @(Fin n)
of
{ Unsafe.Coerce.UnsafeRefl co ->
(hpc<Main,70> x)
`cast` (Sub (Sym co)
:: Coercible (*) (Fin (N.Mult n N.Nat1)) (Fin n))
}
test/Inspection.hs:91:1: lhsFold === rhsFold failed:
LHS:
lhsFold :: Int
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 50 0}]
lhsFold
= hpc<Main,59>
hpc<Main,58>
hpc<Main,52>
hpc<Main,51>
unfoldedFix
@Nat5
@([Int] -> Int)
@(Proxy @{Nat})
$dSNatI_a1Qy
lvl_s5Tx
(hpc<Main,50> lvl_s5Ty)
(hpc<Main,57> lvl_s5TG)
$dSNatI_a1Ti :: SNatI ('S Nat0)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Ti = $fSNatIS @'Z $fSNatIZ
$dSNatI_a1Th :: SNatI ('S Nat1)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Th = $fSNatIS @('S Nat0) $dSNatI_a1Ti
$dSNatI_a1Tg :: SNatI ('S Nat2)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Tg = $fSNatIS @('S Nat1) $dSNatI_a1Th
$dSNatI_a1Tf :: SNatI ('S Nat3)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Tf = $fSNatIS @('S Nat2) $dSNatI_a1Tg
$dSNatI_a1Qy :: SNatI Nat5
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Qy = $fSNatIS @('S Nat3) $dSNatI_a1Tf
lvl_s5St :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
lvl_s5St = I# 1#
lvl_s5Tl :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
lvl_s5Tl = I# 2#
lvl_s5Tm :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
lvl_s5Tm = I# 3#
lvl_s5Tn :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
lvl_s5Tn = I# 4#
_f [Dmd=LCL(C1(L))] :: Int -> Int -> Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 60}]
_f = hpc<Main,48> $fNumInt_$c+
z :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 10}]
z = hpc<Main,49> I# 0#
lvl_s5Tx :: Proxy @{Nat} Nat5
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 10}]
lvl_s5Tx = (hpc<Main,47> Proxy) @Nat @Nat5
lvl_s5Ty :: ([Int] -> Int) -> [Int] -> Int
[LclId,
Arity=2,
Str=<MCM(L)><1L>,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [60 30] 70 0}]
lvl_s5Ty
= \ (_go [Dmd=MCM(L)] :: [Int] -> Int)
(ds_X1G [Dmd=1L] :: [Int]) ->
hpc<Main,46>
case ds_X1G of {
[] -> hpc<Main,41> z;
: x [Dmd=ML] xs [Dmd=ML] ->
hpc<Main,45>
_f (hpc<Main,42> x) (hpc<Main,44> _go (hpc<Main,43> xs))
}
lvl_s5TN :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 0}]
lvl_s5TN = hpc<Main,56> lvl_s5Tn
lvl_s5TD :: [Int]
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
lvl_s5TD = : @Int lvl_s5TN ([] @Int)
lvl_s5TO :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 0}]
lvl_s5TO = hpc<Main,55> lvl_s5Tm
lvl_s5TE :: [Int]
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
lvl_s5TE = : @Int lvl_s5TO lvl_s5TD
lvl_s5TP :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 0}]
lvl_s5TP = hpc<Main,54> lvl_s5Tl
lvl_s5TF :: [Int]
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
lvl_s5TF = : @Int lvl_s5TP lvl_s5TE
lvl_s5TQ :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 0}]
lvl_s5TQ = hpc<Main,53> lvl_s5St
lvl_s5TG :: [Int]
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
lvl_s5TG = : @Int lvl_s5TQ lvl_s5TF
RHS:
rhsFold :: Int
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 10}]
rhsFold = hpc<Main,40> hpc<Main,39> I# 10#
test/Inspection.hs:92:1: lhsFold' === rhsFold failed expectedly.
test/Inspection.hs:100:1: lhsUnfold === rhsUnfold failed:
LHS:
lhsUnfold :: forall a. (a -> a) -> a
[LclIdX,
Arity=1,
Str=<ML>,
Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=False)
Tmpl= \ (@a) (f [Occ=Once1] :: a -> a) ->
hpc<Main,38>
hpc<Main,37>
unfoldedFix
@Nat3 @a @(Proxy @{Nat}) $dSNatI_a1Tg lvl_s5Ss (hpc<Main,36> f)}]
lhsUnfold
= \ (@a) (f [Dmd=ML] :: a -> a) ->
hpc<Main,38>
hpc<Main,37>
unfoldedFix
@Nat3 @a @(Proxy @{Nat}) $dSNatI_a1Tg lvl_s5Ss (hpc<Main,36> f)
$dSNatI_a1Ti :: SNatI ('S Nat0)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Ti = $fSNatIS @'Z $fSNatIZ
$dSNatI_a1Th :: SNatI ('S Nat1)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Th = $fSNatIS @('S Nat0) $dSNatI_a1Ti
$dSNatI_a1Tg :: SNatI ('S Nat2)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Tg = $fSNatIS @('S Nat1) $dSNatI_a1Th
lvl_s5Ss :: Proxy @{Nat} Nat3
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 10}]
lvl_s5Ss = (hpc<Main,35> Proxy) @Nat @Nat3
RHS:
rhsUnfold :: forall a. (a -> a) -> a
[LclIdX,
Arity=1,
Str=<SCS(L)>,
Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=False)
Tmpl= \ (@a) (f :: a -> a) ->
hpc<Main,34>
hpc<Main,33>
f (hpc<Main,32>
f (hpc<Main,31> f (hpc<Main,30> hpc<Main,29> fix @a f)))}]
rhsUnfold
= \ (@a) (f [Dmd=SCS(L)] :: a -> a) ->
hpc<Main,34>
hpc<Main,33>
f (hpc<Main,32>
f (hpc<Main,31> f (hpc<Main,30> hpc<Main,29> fix @a f)))
test/Inspection.hs:117:1: lhsPower5 === rhsPower5 failed:
LHS:
lhsPower5 :: Int -> Int
[LclIdX,
Unf=Unf{Src=InlineStable, TopLvl=True, Value=False, ConLike=False,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)
Tmpl= lhsPower5_s5RB
`cast` (<Int>_R
%<'Many>_N ->_R N:Tagged[0] <Nat>_N <Nat5>_P <Int>_R
:: Coercible (*) (Int -> Tagged @{Nat} Nat5 Int) (Int -> Int))}]
lhsPower5
= lhsPower5_s5RB
`cast` (<Int>_R
%<'Many>_N ->_R N:Tagged[0] <Nat>_N <Nat5>_P <Int>_R
:: Coercible (*) (Int -> Tagged @{Nat} Nat5 Int) (Int -> Int))
$dSNatI_a1Ti :: SNatI ('S Nat0)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Ti = $fSNatIS @'Z $fSNatIZ
$dSNatI_a1Th :: SNatI ('S Nat1)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Th = $fSNatIS @('S Nat0) $dSNatI_a1Ti
$dSNatI_a1Tg :: SNatI ('S Nat2)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Tg = $fSNatIS @('S Nat1) $dSNatI_a1Th
$dSNatI_a1Tf :: SNatI ('S Nat3)
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Tf = $fSNatIS @('S Nat2) $dSNatI_a1Tg
$dSNatI_a1Qy :: SNatI Nat5
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$dSNatI_a1Qy = $fSNatIS @('S Nat3) $dSNatI_a1Tf
lvl_s5St :: Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
lvl_s5St = I# 1#
lhsPower5_s5RB :: Int -> Tagged @{Nat} Nat5 Int
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 100 60}]
lhsPower5_s5RB
= hpc<Main,28>
hpc<Main,27>
\ (k [Dmd=LP(L)] :: Int) ->
hpc<Main,25>
hpc<Main,24>
hpc<Main,23>
hpc<Main,22>
hpc<Main,21>
hpc<Main,15>
induction1
@Nat5
@(Tagged @{Nat})
@Int
$dSNatI_a1Qy
((hpc<Main,14> hpc<Main,13> lvl_s5St)
`cast` (Sym (N:Tagged[0] <Nat>_N <'Z>_P <Int>_R)
:: Coercible (*) Int (Tagged @{Nat} 'Z Int)))
((\ (@(m :: Nat)) ->
hpc<Main,20>
\ _ [Occ=Dead, Dmd=A]
(ds_d5f5 [Dmd=1P(L)] :: Tagged @{Nat} m Int) ->
hpc<Main,19>
hpc<Main,18>
hpc<Main,16>
hpc<Main,17>
$fNumInt_$c*
(ds_d5f5
`cast` (N:Tagged[0] <Nat>_N <m>_P <Int>_R
:: Coercible (*) (Tagged @{Nat} m Int) Int))
k)
`cast` (forall (m :: <Nat>_N).
<SNatI m>_R
%<'Many>_N ->_R <Tagged @{Nat} m Int>_R
%<'Many>_N ->_R Sym (N:Tagged[0] <Nat>_N <'S m>_P <Int>_R)
:: Coercible
(*)
(forall {m :: Nat}. SNatI m => Tagged @{Nat} m Int -> Int)
(forall {m :: Nat}.
SNatI m =>
Tagged @{Nat} m Int -> Tagged @{Nat} ('S m) Int)))
RHS:
rhsPower5 :: Int -> Int
[LclIdX,
Arity=1,
Str=<1P(L)>,
Cpr=1,
Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=False)
Tmpl= \ (k [Occ=Once1!] :: Int) ->
hpc<Main,12>
hpc<Main,11>
hpc<Main,9>
hpc<Main,7>
hpc<Main,5>
hpc<Main,3>
case k of { I# x ->
hpc<Main,4>
hpc<Main,6>
hpc<Main,8> hpc<Main,10> I# (*# (*# (*# (*# x x) x) x) x)
}}]
rhsPower5
= \ (k [Dmd=1P(L)] :: Int) ->
hpc<Main,12>
hpc<Main,11>
hpc<Main,9>
hpc<Main,7>
hpc<Main,5>
hpc<Main,3>
case k of { I# x ->
hpc<Main,4>
hpc<Main,6>
hpc<Main,8> hpc<Main,10> I# (*# (*# (*# (*# x x) x) x) x)
}
test/Inspection.hs: error:
inspection testing unsuccessful
expected failures: 2
unexpected failures: 5