Treat unit types as erased in constructors (#3002)

* Treat unit types as erased in constructors

* Cleanup + dump ttc version

* Update CHANGELOG.md

CHANGELOG.md

@@ -44,6 +44,10 @@
 * `getChar` is now supported on Node.js and `putChar` is supported on both JavaScript backends.
 * Integer-indexed arrays are now supported.
 
+#### Optimizations
+
+* Unit types can now be erased by the optimiser in data types.
+
 ### Compiler changes
 
 * If `IAlternative` expression with `FirstSuccess` rule fails to typecheck,

src/Core/Binary.idr

@@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 20230331 * 100 + 0
+ttcVersion = 20230705 * 100 + 0
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/TTImp/Elab/Utils.idr

@@ -1,6 +1,7 @@
 module TTImp.Elab.Utils
 
 import Core.Case.CaseTree
+import Core.CompileExpr
 import Core.Context
 import Core.Core
 import Core.Env
@@ -32,6 +33,23 @@ detagSafe defs (NTCon _ n _ _ args)
         = elem i ns || notErased (i + 1) ns rest
 detagSafe defs _ = pure False
 
+||| Check if the name at the head of a given Term is a unit type.
+||| This does not evaluate the term, so can return false negatives,
+||| if the unit type is not in the Term directly.
+export
+isUnitType :
+    {auto _ : Ref Ctxt Defs} ->
+    Term vs ->
+    Core Bool
+isUnitType (Ref fc (TyCon {}) n) = do
+    defs <- get Ctxt
+    Just (TCon _ _ _ _ _ _ [con] _) <- lookupDefExact n $ gamma defs
+        | _ => pure False
+    hasFlag (virtualiseFC fc) con (ConType UNIT)
+isUnitType (App _ f _) = isUnitType f
+isUnitType (Bind fc x (Let {}) rhs) = isUnitType rhs
+isUnitType _ = pure False
+
 findErasedFrom : {auto c : Ref Ctxt Defs} ->
                  Defs -> Nat -> NF [] -> Core (List Nat, List Nat)
 findErasedFrom defs pos (NBind fc x (Pi _ c _ aty) scf)
@@ -42,9 +60,9 @@ findErasedFrom defs pos (NBind fc x (Pi _ c _ aty) scf)
          (erest, dtrest) <- findErasedFrom defs (1 + pos) sc
          let dt' = if !(detagSafe defs !(evalClosure defs aty))
                       then (pos :: dtrest) else dtrest
-         pure $ if isErased c
-                   then (pos :: erest, dt')
-                   else (erest, dt')
+         if isErased c || !(isUnitType !(quote defs [] aty))
+            then pure (pos :: erest, dt')
+            else pure (erest, dt')
 findErasedFrom defs pos tm = pure ([], [])
 
 -- Find the argument positions in the given type which are guaranteed to be

src/TTImp/ProcessData.idr

@@ -210,25 +210,25 @@ getDetags fc tys
 getRelevantArg : {auto c : Ref Ctxt Defs} ->
                  Defs -> Nat -> Maybe Nat -> Bool -> NF [] ->
                  Core (Maybe (Bool, Nat))
-getRelevantArg defs i rel world (NBind fc _ (Pi _ rig _ val) sc)
-    = branchZero (getRelevantArg defs (1 + i) rel world
-                              !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))))
-                 (case !(evalClosure defs val) of
-                       -- %World is never inspected, so might as well be deleted from data types,
-                       -- although it needs care when compiling to ensure that the function that
-                       -- returns the IO/%World type isn't erased
-                       (NPrimVal _ $ PrT WorldType) =>
-                           getRelevantArg defs (1 + i) rel False
-                               !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder)))
-                       _ =>
-                       -- if we haven't found a relevant argument yet, make
-                       -- a note of this one and keep going. Otherwise, we
-                       -- have more than one, so give up.
-                           maybe (do sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder))
-                                     getRelevantArg defs (1 + i) (Just i) False sc')
-                                 (const (pure Nothing))
-                                 rel)
-                 rig
+getRelevantArg defs i rel world (NBind fc _ (Pi _ rig _ val) sc) =
+    if isErased rig || !(isUnitType !(quote defs [] val))
+        then getRelevantArg defs (1 + i) rel world
+                !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder)))
+        else case !(evalClosure defs val) of
+                  -- %World is never inspected, so might as well be deleted from data types,
+                  -- although it needs care when compiling to ensure that the function that
+                  -- returns the IO/%World type isn't erased
+                  (NPrimVal _ $ PrT WorldType) =>
+                      getRelevantArg defs (1 + i) rel False
+                          !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder)))
+                  _ =>
+                      -- if we haven't found a relevant argument yet, make
+                      -- a note of this one and keep going. Otherwise, we
+                      -- have more than one, so give up.
+                      maybe (do sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder))
+                                getRelevantArg defs (1 + i) (Just i) False sc')
+                            (const (pure Nothing))
+                            rel
 getRelevantArg defs i rel world tm
     = pure ((world,) <$> rel)
 
@@ -247,25 +247,29 @@ findNewtype [con]
                  _ => Nothing
 findNewtype _ = pure ()
 
-hasArgs : Nat -> Term vs -> Bool
-hasArgs (S k) (Bind _ _ (Pi _ c _ _) sc)
-    = if isErased c
-         then hasArgs (S k) sc
-         else hasArgs k sc
-hasArgs (S k) _ = False
-hasArgs Z (Bind _ _ (Pi _ c _ _) sc)
-    = if isErased c
-         then hasArgs Z sc
-         else False
-hasArgs Z _ = True
+hasArgs : {auto _ : Ref Ctxt Defs} -> Nat -> Term vs -> Core Bool
+hasArgs (S k) (Bind _ _ (Pi _ c _ ty) sc)
+    = if isErased c || !(isUnitType ty)
+        then hasArgs (S k) sc
+        else hasArgs k sc
+hasArgs (S k) _ = pure False
+hasArgs Z (Bind _ _ (Pi _ c _ ty) sc)
+    = if isErased c || !(isUnitType ty)
+        then hasArgs Z sc
+        else pure False
+hasArgs Z _ = pure True
 
 -- get the first non-erased argument
-firstArg : Term vs -> Maybe (Exists Term)
+firstArg :
+    Ref Ctxt Defs =>
+    {vs : _} ->
+    Term vs ->
+    Core (Maybe (Exists Term))
 firstArg (Bind _ _ (Pi _ c _ val) sc)
-    = if isErased c
+    = if isErased c || !(isUnitType val)
          then firstArg sc
-         else Just $ Evidence _ val
-firstArg tm = Nothing
+         else pure $ Just $ Evidence _ val
+firstArg tm = pure Nothing
 
 typeCon : Term vs -> Maybe Name
 typeCon (Ref _ (TyCon _ _) n) = Just n
@@ -273,12 +277,12 @@ typeCon (App _ fn _) = typeCon fn
 typeCon _ = Nothing
 
 shaped : {auto c : Ref Ctxt Defs} ->
-         (forall vs . Term vs -> Bool) ->
+         (forall vs. Term vs -> Core Bool) ->
          List Constructor -> Core (Maybe Name)
 shaped as [] = pure Nothing
 shaped as (c :: cs)
     = do defs <- get Ctxt
-         if as !(normalise defs [] (type c))
+         if !(as !(normalise defs [] (type c)))
             then pure (Just (name c))
             else shaped as cs
 
@@ -331,7 +335,7 @@ calcEnum fc cs
     isNullary : Constructor -> Core Bool
     isNullary c
         = do defs <- get Ctxt
-             pure $ hasArgs 0 !(normalise defs [] (type c))
+             hasArgs 0 !(normalise defs [] (type c))
 
 calcRecord : {auto c : Ref Ctxt Defs} ->
              FC -> List Constructor -> Core Bool
@@ -352,7 +356,7 @@ calcNaty fc tyCon cs@[_, _]
               | Nothing => pure False
          let Just succCon = find (\con => name con == succ) cs
               | Nothing => pure False
-         let Just (Evidence _ succArgTy) = firstArg (type succCon)
+         Just (Evidence _ succArgTy) <- firstArg (type succCon)
               | Nothing => pure False
          let Just succArgCon = typeCon succArgTy
               | Nothing => pure False