Add noNewtype option to data types

CHANGELOG.md

@@ -6,6 +6,10 @@ Compiler updates:
 * Data types with a single constructor, with a single unerased arguments,
   are translated to just that argument, to save repeated packing and unpacking.
   (c.f. `newtype` in Haskell)
+  + A data type can opt out of this behaviour by specifying `noNewtype` in its
+    options list. `noNewtype` allows code generators to apply special handling
+    to the generated constructor/deconstructor, for a newtype-like data type,
+    that would otherwise be optimised away.
 * 0-multiplicity constructor arguments are now properly erased, not just
   given a placeholder null value.
 

src/Idris/Parser.idr

@@ -924,6 +924,8 @@ dataOpt
          pure (SearchBy ns)
   <|> do exactIdent "external"
          pure External
+  <|> do exactIdent "noNewtype"
+         pure NoNewtype
 
 dataBody : FileName -> Int -> FilePos -> Name -> IndentInfo -> PTerm ->
            EmptyRule PDataDecl

src/TTImp/ProcessData.idr

@@ -29,6 +29,8 @@ processDataOpt fc ndef UniqueSearch
     = setUniqueSearch fc ndef True
 processDataOpt fc ndef External
     = setExternal fc ndef True
+processDataOpt fc ndef NoNewtype
+    = pure ()
 
 checkRetType : {auto c : Ref Ctxt Defs} ->
                Env Term vars -> NF vars ->
@@ -330,7 +332,12 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
 
          let ddef = MkData (MkCon dfc n arity fullty) cons
          addData vars vis tidx ddef
-         findNewtype cons
+
+         -- Flag data type as a newtype, if possible (See `findNewtype` for criteria).
+         -- Skip optimisation if the data type has specified `noNewtype` in its
+         -- options list.
+         when (not (NoNewtype `elem` opts)) $
+              findNewtype cons
 
          -- Type is defined mutually with every data type undefined at the
          -- point it was declared, and every data type undefined right now

src/TTImp/TTImp.idr

@@ -232,6 +232,7 @@ mutual
        NoHints : DataOpt -- Don't generate search hints for constructors
        UniqueSearch : DataOpt -- auto implicit search must check result is unique
        External : DataOpt -- implemented externally
+       NoNewtype : DataOpt -- don't apply newtype optimisation
 
   export
   Eq DataOpt where
@@ -239,6 +240,7 @@ mutual
     (==) NoHints NoHints = True
     (==) UniqueSearch UniqueSearch = True
     (==) External External = True
+    (==) NoNewtype NoNewtype = True
     (==) _ _ = False
 
   public export
@@ -837,6 +839,7 @@ mutual
     toBuf b NoHints = tag 1
     toBuf b UniqueSearch = tag 2
     toBuf b External = tag 3
+    toBuf b NoNewtype = tag 4
 
     fromBuf b
         = case !getTag of
@@ -845,6 +848,7 @@ mutual
                1 => pure NoHints
                2 => pure UniqueSearch
                3 => pure External
+               4 => pure NoNewtype
                _ => corrupt "DataOpt"
 
   export