[ new ] constructor plus trivial impl for Interpolation (#2871)

* [ new ] constructor plus trivial impl for Interpolation

* [ doc ] update CHANGELOG

* [ test ] adjust expected test output

CHANGELOG.md

@@ -63,6 +63,8 @@
 * Improved performance of functions `isNL`, `isSpace`, and `isHexDigit`.
 
 * Implements `Foldable` and `Traversable` for pairs, right-biased as `Functor`.
+* Added a constructor (`MkInterpolation`) to `Interpolation`.
+* Added an `Interpolation` implementation for `Void`.
 
 #### Base
 

libs/prelude/Prelude/Interpolation.idr

@@ -1,5 +1,7 @@
 module Prelude.Interpolation
 
+import Builtin
+
 ||| Interpolated strings are of the form `"xxxx \{ expr } yyyy"`.
 ||| In this example the string `"xxxx "` is concatenated with `expr` and
 ||| `" yyyy"`, since `expr` is not necessarily a string, the generated
@@ -11,9 +13,14 @@ module Prelude.Interpolation
 ||| an instance of `Interpolation` for a type.
 public export
 interface Interpolation a where
+  constructor MkInterpolation
   interpolate : a -> String
 
 ||| The interpolation instance for Strings is the identity
 export
 Interpolation String where
   interpolate x = x
+
+export
+Interpolation Void where
+  interpolate _ impossible

tests/idris2/record019/expected

@@ -12,6 +12,6 @@ LOG declare.record.parameters:50: Decided to bind the following extra parameters
 
 LOG declare.record.parameters:60: We elaborated Main.EtaProof in a non-empty local context.
   Dropped: [b, a]
-  Remaining type: (p : ($resolved2700 a[1] b[0])) -> Type
+  Remaining type: (p : ($resolved2702 a[1] b[0])) -> Type
 
 LOG declare.record.parameters:30: Unelaborated type: (%pi RigW Explicit Nothing Main.Product %type)