From 6d2dd935c4e53704f63c524aef2c5f8b7882d2fd Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Fri, 15 Jan 2021 20:19:20 +0300
Subject: [PATCH] Special variants of `DPair` as records (#922)

---
 libs/base/Data/DPair.idr | 73 +++++-----------------------------------
 1 file changed, 8 insertions(+), 65 deletions(-)

diff --git a/libs/base/Data/DPair.idr b/libs/base/Data/DPair.idr
index 9e2b06160f..5de0625c92 100644
--- a/libs/base/Data/DPair.idr
+++ b/libs/base/Data/DPair.idr
@@ -16,37 +16,10 @@ namespace Exists
   ||| @type The type of the type-level value in the proof.
   ||| @this The dependent type that requires an instance of `type`.
   public export
-  data Exists : (this : type -> Type) -> Type where
-    Evidence : (0 value : type)
-            -> (prf : this value)
-            -> Exists this
-
-  ||| Return the type-level value (evidence) required by the dependent type.
-  |||
-  ||| We need to be in the Erased setting for this to work.
-  |||
-  ||| @type The type-level value's type.
-  ||| @pred The dependent type that requires an instance of `type`.
-  ||| @prf  That there is a value that satisfies `prf`.
-  public export
-  0
-  fst : {0 type : Type}
-     -> {0 pred : type -> Type}
-     -> (1 prf  : Exists pred)
-     -> type
-  fst (Evidence value _) = value
-
-  ||| Return the dependently typed value.
-  |||
-  ||| @type The type-level value's type.
-  ||| @pred The dependent type that requires an instance of `type`.
-  ||| @prf  That there is a value that satisfies `prf`.
-  public export
-  snd : {0 type : Type}
-     -> {0 pred : type -> Type}
-     -> (1 prf  : Exists pred)
-     -> pred (Exists.fst prf)
-  snd (Evidence value prf) = prf
+  record Exists {0 type : _} this where
+    constructor Evidence
+    0 fst : type
+    snd : this fst
 
 namespace Subset
 
@@ -60,37 +33,7 @@ namespace Subset
   ||| @type The type-level value's type.
   ||| @pred The dependent type that requires an instance of `type`.
   public export
-  data Subset : (type : Type)
-             -> (pred : type -> Type)
-             -> Type
-    where
-      Element : (value : type)
-             -> (0 prf : pred value)
-             -> Subset type pred
-
-  ||| Return the type-level value (evidence) required by the dependent type.
-  |||
-  ||| @type The type-level value's type.
-  ||| @pred The dependent type that requires an instance of `type`.
-  ||| @prf  That there is a value that satisfies `prf`.
-  public export
-  fst : {0 type : Type}
-     -> {0 pred : type -> Type}
-     -> (1 prf  : Subset type pred)
-     -> type
-  fst (Element value prf) = value
-
-  ||| Return the dependently typed value.
-  |||
-  ||| We need to be in the erased setting for this to work.
-  |||
-  ||| @type The type-level value's type.
-  ||| @pred The dependent type that requires an instance of `type`.
-  ||| @prf  That there is a value that satisfies `prf`.
-  public export
-  0
-  snd : {0 type : Type}
-     -> {0 pred : type -> Type}
-     -> (1 value : Subset type pred)
-     -> pred (Subset.fst value)
-  snd (Element value prf) = prf
+  record Subset type pred where
+    constructor Element
+    fst : type
+    0 snd : pred fst