@@ -417,9 +417,13 @@ irTerm top vs env tm@(App _ f a) = do
417417 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]
418418
419419 -- compile Nat-likes as bigints
420+ -- not sure if prim applications must be saturated
421+ -- let's wrap it in a lambda just to be sure
420422 | Just LikeS <- isLikeNat ist n
421− -> irTerm top vs env $
422− App Complete (P Ref (sUN "prim__addBigInt") Erased) (Constant $ BI 1)
423+ -> LLam [sMN 0 "nh"] <$>
424+ (irTerm top vs env $
425+ mkApp (P Ref (sUN "prim__addBigInt") Erased)
426+ [Constant $ BI 1, P Ref (sMN 0 "nh") Erased])
423427
424428 -- not a newtype, just apply to a constructor
425429 | otherwise
@@ -527,23 +531,23 @@ isLikeNat ist cn
527531
528532 | Just cTy <- lookupTyExact cn $ tt_ctxt ist
529533 , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy
530− , Just (z, s) <- natLikeCtors tyN cTy
534+ , Just (z, s) <- natLikeCtors tyN
531535 = if | cn == z -> Just LikeZ
532536 | cn == s -> Just LikeS
533537 | otherwise -> error $ "isLikeNat: constructor not found in its own family: " ++ show (cn, tyN)
534538
535539 | otherwise = Nothing
536540 where
537− natLikeCtors :: Name -> Type -> Maybe (Name, Name)
538− natLikeCtors tyN cTy = case lookupCtxtExact tyN $ idris_datatypes ist of
541+ natLikeCtors :: Name -> Maybe (Name, Name)
542+ natLikeCtors tyN = case lookupCtxtExact tyN $ idris_datatypes ist of
539543 Just TI{con_names = [z, s]}
540544 | 0 <- getUsedCount z
541− , looksLikeS tyN s cTy
545+ , looksLikeS s
542546 -> Just (z, s)
543547
544548 Just TI{con_names = [s, z]}
545549 | 0 <- getUsedCount z
546− , looksLikeS tyN s cTy
550+ , looksLikeS s
547551 -> Just (z, s)
548552
549553 _ -> Nothing
@@ -554,11 +558,13 @@ isLikeNat ist cn
554558 $ lookupCtxtExact n
555559 $ idris_callgraph ist
556560
557− looksLikeS :: Name -> Name -> Type -> Bool
558− looksLikeS tyN cn cTy
561+ looksLikeS :: Name -> Bool
562+ looksLikeS cn
559563 | Just [(i, _)] <- fmap usedpos $ lookupCtxtExact cn $ idris_callgraph ist
564+ , Just cTy <- lookupTyExact cn $ tt_ctxt ist
560565 , [recTy] <- [recTy | (j, (_n, recTy)) <- zip [0..] (getArgTys cTy), j == i]
561566 , (P TCon{} recTyN _, _) <- unApply recTy
567+ , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy
562568 , recTyN == tyN
563569 = True
564570