@@ -400,8 +400,9 @@ irTerm top vs env tm@(App _ f a) = do
400400
401401 -- compile Nat-likes as bigints
402402 | Just LikeS <- isLikeNat ist n
403− -> irTerm top vs env $
404− App Complete (P Ref (sUN "prim__addBigInt") Erased) (Constant $ BI 1)
403+ -> irTerm top vs env $ mkApp
404+ (P Ref (sUN "prim__addBigInt") Erased)
405+ (Constant (BI 1) : argsPruned)
405406
406407 | otherwise -- not newtype, plain data ctor
407408 -> buildApp (LV n) argsPruned
@@ -674,17 +675,40 @@ irSC top vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do
674675 detag <- fgetState (opt_detaggable . ist_optimisation cn)
675676 if detag
676677 then irSC top vs (Case up n [ConCase cn a ns sc])
677− else LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
678+ else do
679+ likeNat <- isLikeNat <$> getIState <*> pure cn
680+ case likeNat of
681+ -- the annoying case: LikeS is translated into a default case
682+ -- so we need to change the original DefaultCase to Z-case
683+ -- and reorder it before this one
684+ Just LikeS -> do
685+ zCase <- LConstCase (BI 0) <$> irSC top vs sc'
686+ sCase <- irAlt top vs (LV n) (ConCase cn a ns sc)
687+ return $ LCase up (LV n) [zCase, sCase]
688+
689+ -- the usual case
690+ _ -> LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
678691
679692irSC top vs sc@(Case up n alts) = do
680− -- check that neither alternative needs the newtype optimisation,
681− -- see comment above
682− goneWrong <- or <$> mapM isDetaggable alts
683− when goneWrong
684− $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
685−
686− -- everything okay
687− LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
693+ ist <- getIState
694+
695+ if | [ConCase cns as nss scs, ConCase cnz az nsz scz] <- alts
696+ , Just LikeS <- isLikeNat ist cns
697+ -> do
698+ -- reorder to make the Z case come first
699+ zCase <- LConstCase (BI 0) <$> irSC top vs scz
700+ sCase <- irAlt top vs (LV n) (ConCase cns as nss scs)
701+ return $ LCase up (LV n) [zCase, sCase]
702+
703+ | otherwise -> do
704+ -- check that neither alternative needs the newtype optimisation,
705+ -- see comment above
706+ goneWrong <- or <$> mapM isDetaggable alts
707+ when goneWrong
708+ $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)
709+
710+ -- everything okay
711+ LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts
688712 where
689713 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn
690714 isDetaggable _ = return False