@@ -417,9 +417,13 @@ irTerm top vs env tm@(App _ f a) = do
417 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]
417 -> return . padLams $ \[vn] -> LApp False (LV n) [LV vn]
419 -- compile Nat-likes as bigints
419 -- 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
420 | Just LikeS <- isLikeNat ist n
422 | Just LikeS <- isLikeNat ist n
423+ -> LLam [sMN 0 "nh"] <$>
421− -> irTerm top vs env $
424+ (irTerm top vs env $
422− App Complete (P Ref (sUN "prim__addBigInt") Erased) (Constant $ BI 1)
425+ mkApp (P Ref (sUN "prim__addBigInt") Erased)
426+ [Constant $ BI 1, P Ref (sMN 0 "nh") Erased])
424 -- not a newtype, just apply to a constructor
428 -- not a newtype, just apply to a constructor
425 | otherwise
429 | otherwise
@@ -527,23 +531,23 @@ isLikeNat ist cn
528 | Just cTy <- lookupTyExact cn $ tt_ctxt ist
532 | Just cTy <- lookupTyExact cn $ tt_ctxt ist
529 , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy
533 , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy
530− , Just (z, s) <- natLikeCtors tyN cTy
534+ , Just (z, s) <- natLikeCtors tyN
531 = if | cn == z -> Just LikeZ
535 = if | cn == z -> Just LikeZ
532 | cn == s -> Just LikeS
536 | cn == s -> Just LikeS
533 | otherwise -> error $ "isLikeNat: constructor not found in its own family: " ++ show (cn, tyN)
537 | otherwise -> error $ "isLikeNat: constructor not found in its own family: " ++ show (cn, tyN)
535 | otherwise = Nothing
539 | otherwise = Nothing
537− natLikeCtors :: Name -> Type -> Maybe (Name, Name)
541+ natLikeCtors :: Name -> Maybe (Name, Name)
538− natLikeCtors tyN cTy = case lookupCtxtExact tyN $ idris_datatypes ist of
542+ natLikeCtors tyN = case lookupCtxtExact tyN $ idris_datatypes ist of
539 Just TI{con_names = [z, s]}
543 Just TI{con_names = [z, s]}
540 | 0 <- getUsedCount z
544 | 0 <- getUsedCount z
541− , looksLikeS tyN s cTy
545+ , looksLikeS s
542 -> Just (z, s)
546 -> Just (z, s)
544 Just TI{con_names = [s, z]}
548 Just TI{con_names = [s, z]}
545 | 0 <- getUsedCount z
549 | 0 <- getUsedCount z
546− , looksLikeS tyN s cTy
550+ , looksLikeS s
547 -> Just (z, s)
551 -> Just (z, s)
549 _ -> Nothing
553 _ -> Nothing
@@ -554,11 +558,13 @@ isLikeNat ist cn
554 $ lookupCtxtExact n
558 $ lookupCtxtExact n
555 $ idris_callgraph ist
559 $ idris_callgraph ist
557− looksLikeS :: Name -> Name -> Type -> Bool
561+ looksLikeS :: Name -> Bool
558− looksLikeS tyN cn cTy
562+ looksLikeS cn
559 | Just [(i, _)] <- fmap usedpos $ lookupCtxtExact cn $ idris_callgraph ist
563 | Just [(i, _)] <- fmap usedpos $ lookupCtxtExact cn $ idris_callgraph ist
564+ , Just cTy <- lookupTyExact cn $ tt_ctxt ist
560 , [recTy] <- [recTy | (j, (_n, recTy)) <- zip [0..] (getArgTys cTy), j == i]
565 , [recTy] <- [recTy | (j, (_n, recTy)) <- zip [0..] (getArgTys cTy), j == i]
561 , (P TCon{} recTyN _, _) <- unApply recTy
566 , (P TCon{} recTyN _, _) <- unApply recTy
567+ , (P TCon{} tyN _, _) <- unApply $ getRetTy cTy
562 , recTyN == tyN
568 , recTyN == tyN