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] _N _P _R :: Coercible (*) (Tagged @{Nat} Nat5 Int) Int)}] lhsInline = lhsInline_s5S5 `cast` (N:Tagged[0] _N _P _R :: Coercible (*) (Tagged @{Nat} Nat5 Int) Int) $dSNatI_a1Ti :: SNatI ('S Nat0) [LclId, Unf=Unf{Src=, 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=, 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=, 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=, 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=, 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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 60}] poly_f_s5T0 = \ (@(m :: Nat)) -> hpc \ (x [Dmd=1L] :: Tagged @{Nat} m Int) -> x poly_g_s5Td :: Int -> Int [LclId, Unf=Unf{Src=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 60}] poly_g_s5Td = hpc $fEnumInt_$csucc poly_g_s5T4 :: forall {m :: Nat}. Tagged @{Nat} m Int -> Tagged @{Nat} m Int [LclId, Unf=Unf{Src=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 20 60}] poly_g_s5T4 = \ (@(m :: Nat)) -> hpc $fFunctorTagged_$cfmap @Nat @m @Int @Int poly_g_s5Td lvl_s5TH :: Int [LclId, Unf=Unf{Src=, 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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 60 60}] lvl_s5TI = \ (@(m :: Nat)) -> hpc \ _ [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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 40 0}] lhsInline_s5S5 = hpc hpc hpc induction1 @Nat5 @(Tagged @{Nat}) @Int $dSNatI_a1Qy ((hpc hpc lvl_s5TH) `cast` (Sym (N:Tagged[0] _N <'Z>_P _R) :: Coercible (*) Int (Tagged @{Nat} 'Z Int))) (lvl_s5TI `cast` (forall (m :: _N). _R %<'Many>_N ->_R _R %<'Many>_N ->_R N:Tagged[0] _N _P _R ; Sym (N:Tagged[0] _N <'S m>_P _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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 10}] rhs = hpc hpc I# 5# test/Inspection.hs:52:1: lhsNormal === rhs failed expectedly. test/Inspection.hs:65:1: lhsProof ==- rhsProof failed: LHS: lhsProof = ... hpc hpc hpc case N.proofMultNOne @n $dSNatI_a4d4 of { Refl co_a4du -> (hpc x) `cast` ((Fin (Sym co))_R :: Coercible (*) (Fin (N.Mult n N.Nat1)) (Fin n)) } RHS: rhsProof = ... hpc hpc case Unsafe.Coerce.unsafeEqualityProof @(*) @(Fin (N.Mult n N.Nat1)) @(Fin n) of { Unsafe.Coerce.UnsafeRefl co -> (hpc 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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 50 0}] lhsFold = hpc hpc hpc hpc unfoldedFix @Nat5 @([Int] -> Int) @(Proxy @{Nat}) $dSNatI_a1Qy lvl_s5Tx (hpc lvl_s5Ty) (hpc lvl_s5TG) $dSNatI_a1Ti :: SNatI ('S Nat0) [LclId, Unf=Unf{Src=, 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=, 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=, 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=, 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=, 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=, 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=, 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=, 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=, 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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 60}] _f = hpc $fNumInt_$c+ z :: Int [LclId, Unf=Unf{Src=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 10}] z = hpc I# 0# lvl_s5Tx :: Proxy @{Nat} Nat5 [LclId, Unf=Unf{Src=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 10}] lvl_s5Tx = (hpc Proxy) @Nat @Nat5 lvl_s5Ty :: ([Int] -> Int) -> [Int] -> Int [LclId, Arity=2, Str=<1L>, Unf=Unf{Src=, 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 case ds_X1G of { [] -> hpc z; : x [Dmd=ML] xs [Dmd=ML] -> hpc _f (hpc x) (hpc _go (hpc xs)) } lvl_s5TN :: Int [LclId, Unf=Unf{Src=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 0}] lvl_s5TN = hpc lvl_s5Tn lvl_s5TD :: [Int] [LclId, Unf=Unf{Src=, 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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 0}] lvl_s5TO = hpc lvl_s5Tm lvl_s5TE :: [Int] [LclId, Unf=Unf{Src=, 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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 0}] lvl_s5TP = hpc lvl_s5Tl lvl_s5TF :: [Int] [LclId, Unf=Unf{Src=, 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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 0}] lvl_s5TQ = hpc lvl_s5St lvl_s5TG :: [Int] [LclId, Unf=Unf{Src=, 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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 10}] rhsFold = hpc hpc 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=, 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 hpc unfoldedFix @Nat3 @a @(Proxy @{Nat}) $dSNatI_a1Tg lvl_s5Ss (hpc f)}] lhsUnfold = \ (@a) (f [Dmd=ML] :: a -> a) -> hpc hpc unfoldedFix @Nat3 @a @(Proxy @{Nat}) $dSNatI_a1Tg lvl_s5Ss (hpc f) $dSNatI_a1Ti :: SNatI ('S Nat0) [LclId, Unf=Unf{Src=, 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=, 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=, 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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 0 10}] lvl_s5Ss = (hpc Proxy) @Nat @Nat3 RHS: rhsUnfold :: forall a. (a -> a) -> a [LclIdX, Arity=1, Str=, 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 hpc f (hpc f (hpc f (hpc hpc fix @a f)))}] rhsUnfold = \ (@a) (f [Dmd=SCS(L)] :: a -> a) -> hpc hpc f (hpc f (hpc f (hpc hpc 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` (_R %<'Many>_N ->_R N:Tagged[0] _N _P _R :: Coercible (*) (Int -> Tagged @{Nat} Nat5 Int) (Int -> Int))}] lhsPower5 = lhsPower5_s5RB `cast` (_R %<'Many>_N ->_R N:Tagged[0] _N _P _R :: Coercible (*) (Int -> Tagged @{Nat} Nat5 Int) (Int -> Int)) $dSNatI_a1Ti :: SNatI ('S Nat0) [LclId, Unf=Unf{Src=, 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=, 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=, 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=, 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=, 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=, 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=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 100 60}] lhsPower5_s5RB = hpc hpc \ (k [Dmd=LP(L)] :: Int) -> hpc hpc hpc hpc hpc hpc induction1 @Nat5 @(Tagged @{Nat}) @Int $dSNatI_a1Qy ((hpc hpc lvl_s5St) `cast` (Sym (N:Tagged[0] _N <'Z>_P _R) :: Coercible (*) Int (Tagged @{Nat} 'Z Int))) ((\ (@(m :: Nat)) -> hpc \ _ [Occ=Dead, Dmd=A] (ds_d5f5 [Dmd=1P(L)] :: Tagged @{Nat} m Int) -> hpc hpc hpc hpc $fNumInt_$c* (ds_d5f5 `cast` (N:Tagged[0] _N _P _R :: Coercible (*) (Tagged @{Nat} m Int) Int)) k) `cast` (forall (m :: _N). _R %<'Many>_N ->_R _R %<'Many>_N ->_R Sym (N:Tagged[0] _N <'S m>_P _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 hpc hpc hpc hpc hpc case k of { I# x -> hpc hpc hpc hpc I# (*# (*# (*# (*# x x) x) x) x) }}] rhsPower5 = \ (k [Dmd=1P(L)] :: Int) -> hpc hpc hpc hpc hpc hpc case k of { I# x -> hpc hpc hpc hpc I# (*# (*# (*# (*# x x) x) x) x) } test/Inspection.hs: error: inspection testing unsuccessful expected failures: 2 unexpected failures: 5