Revert "Treat unit types as erased in constructors (#3002)"

This reverts commit 677acf0d84.

CHANGELOG.md

@@ -44,10 +44,6 @@
 * `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 = 20230705 * 100 + 0
+ttcVersion = 20230331 * 100 + 0
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/TTImp/Elab/Utils.idr

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