reflection.induction: handle erased constructors (#478)

Inspired by cmcmA20/cubical-mini#48. Also adds
`work-on-types` so that the macro works at all when `--erasure` is used
(see agda/agda#6124).

Author: ncfavier

src/1Lab/Reflection.lagda.md

@@ -103,6 +103,9 @@ private module P where
   -- "blocking" constraints.
     noConstraints : ∀ {a} {A : Type a} → TC A → TC A
 
+  -- Run the given computation at the type level, allowing use of erased things.
+    work-on-types : ∀ {a} {A : Type a} → TC A → TC A
+
   -- Run the given TC action and return the first component. Resets to
   -- the old TC state if the second component is 'false', or keep the
   -- new TC state if it is 'true'.
@@ -158,6 +161,7 @@ private module P where
   {-# BUILTIN AGDATCMASKEXPANDLAST     askExpandLast              #-}
   {-# BUILTIN AGDATCMASKREDUCEDEFS     askReduceDefs              #-}
   {-# BUILTIN AGDATCMNOCONSTRAINTS     noConstraints              #-}
+  {-# BUILTIN AGDATCMWORKONTYPES       work-on-types              #-}
   {-# BUILTIN AGDATCMRUNSPECULATIVE    run-speculative            #-}
   {-# BUILTIN AGDATCMGETINSTANCES      get-instances              #-}
   {-# BUILTIN AGDATCMDECLAREDATA       declareData                #-}

src/1Lab/Reflection/Deriving/Show.agda

@@ -105,7 +105,7 @@ private
 
   -- Create the clause of shows-prec for a constructor.
   show-clause : Constructor → TC Clause
-  show-clause (conhead conm _ args _) = do
+  show-clause (conhead conm _ _ args _) = do
     let
       -- We'll only show the visible arguments to the constructor.
       -- Moreover, since Agda can infer the types in the telescope

src/1Lab/Reflection/Induction.agda

@@ -235,15 +235,17 @@ private
           -- Otherwise, add m : T to the telescope and replace the corresponding
           -- constructor with m henceforth.
           method ← ("P" <>_) <$> render-name c
+          q ← get-con-quantity c
+          let argC = arg (arginfo visible (modality relevant q))
           let
             ps = raise 1 ps
             P = raise 1 P
             rs = (c' , var 0 []) ∷ raise 1 rs
-          extend-context method (argN methodT) (go ps P rs cs) <&>
-            ×-map₁₂ ((method , argN methodT) ∷_) (α ∷_)
+          extend-context method (argC methodT) (go ps P rs cs) <&>
+            ×-map₁₂ ((method , argC methodT) ∷_) (α ∷_)
 
 make-elim-with : Elim-options → Name → Name → TC ⊤
-make-elim-with opts elim D = withNormalisation true do
+make-elim-with opts elim D = work-on-types $ withNormalisation true do
   DT ← get-type D >>= normalise -- D : (ps : Γ) (is : Ξ) → Type _
   data-type pars cs ← get-definition D
     where _ → typeError [ "not a data type: " , nameErr D ]

src/1Lab/Reflection/Signature.agda

@@ -22,6 +22,12 @@ get-record-type n = get-definition n >>= λ where
   (record-type conm fields) → pure (conm , fields)
   _ → typeError [ "get-record-type: definition " , nameErr n , " is not a record type." ]
 
+-- Look up a constructor's quantity in the signature.
+get-con-quantity : Name → TC Quantity
+get-con-quantity n = get-definition n >>= λ where
+  (data-cons _ q) → pure q
+  _ → typeError [ "get-con-erasure: definition " , nameErr n , " is not a constructor." ]
+
 -- Representation of a data/record constructor.
 record Constructor : Type where
   constructor conhead
@@ -32,6 +38,9 @@ record Constructor : Type where
     -- Name of the data type:
     con-data      : Name
 
+    -- Quantity of the constructor.
+    con-quantity  : Quantity
+
     -- Argument telescope for the constructor, with the datatype's
     -- parameters removed.
     con-arguments : Telescope
@@ -55,22 +64,23 @@ get-type-constructors n = datatype <|> recordtype where
   datatype = do
     (npars , cons) ← get-data-type n
     for cons λ qn → do
+      q ← get-con-quantity qn
       (args , ty) ← pi-view <$> get-type qn
-      pure (conhead qn n (drop npars args) ty)
+      pure (conhead qn n q (drop npars args) ty)
 
   recordtype = do
     (c  , _)    ← get-record-type n
     (np , _)    ← pi-view <$> get-type n
     (args , ty) ← pi-view <$> get-type c
-    pure ((conhead c n (drop (length np) args) ty) ∷ [])
+    pure ((conhead c n quantity-ω (drop (length np) args) ty) ∷ [])
 
 -- Look up a constructor in the signature.
 get-constructor : Name → TC Constructor
 get-constructor n = get-definition n >>= λ where
-  (data-cons t _) → do
+  (data-cons t q) → do
     (npars , cons) ← get-data-type t
     (args , ty)    ← pi-view <$> get-type n
-    pure (conhead n t (drop npars args) ty)
+    pure (conhead n t q (drop npars args) ty)
   _ → typeError [ "get-constructor: " , nameErr n , " is not a data constructor." ]
 
 -- If a term reduces to an application of a record type, return